Imported Upstream version 8.5~beta1+dfsg

1 files changed, 379 insertions, 46 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
index d6a9b56f..7aaf2ffe 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,60 +8,189 @@
 
 (** Universes. *)
 
-type universe_level
-type universe
+module Level :
+sig
+  type t
+  (** Type of universe levels. A universe level is essentially a unique name
+      that will be associated to constraints later on. *)
 
-module UniverseLSet : Set.S with type elt = universe_level
+  val set : t
+  val prop : t
+  (** The set and prop universe levels. *)
 
-(** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... 
-   Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
+  val is_small : t -> bool
+  (** Is the universe set or prop? *)
+
+  val compare : t -> t -> int
+  (** Comparison function *)
+
+  val equal : t -> t -> bool
+  (** Equality function *)
+
+  val hash : t -> int
+
+  val make : Names.DirPath.t -> int -> t
+  (** Create a new universe level from a unique identifier and an associated
+      module path. *)
+
+  val pr : t -> Pp.std_ppcmds
+  (** Pretty-printing *)
+
+  val var : int -> t
+
+  val var_index : t -> int option
+end
+
+type universe_level = Level.t
+(** Alias name. *)
+
+(** Sets of universe levels *)
+module LSet : 
+sig 
+  include CSig.SetS with type elt = universe_level
+	      
+  val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+  (** Pretty-printing *)
+end
+
+type universe_set = LSet.t
+
+module Universe :
+sig
+  type t
+  (** Type of universes. A universe is defined as a set of level expressions.
+      A level expression is built from levels and successors of level expressions, i.e.:
+      le ::= l + n, n \in N.
+
+      A universe is said atomic if it consists of a single level expression with
+      no increment, and algebraic otherwise (think the least upper bound of a set of
+      level expressions).
+  *)
 
-val type0m_univ : universe  (** image of Prop in the universes hierarchy *)
-val type0_univ : universe  (** image of Set in the universes hierarchy *)
-val type1_univ : universe  (** the universe of the type of Prop/Set *)
+  val compare : t -> t -> int
+  (** Comparison function *)
 
-val make_universe_level : Names.dir_path * int -> universe_level
-val make_universe : universe_level -> universe
-val make_univ : Names.dir_path * int -> universe
+  val equal : t -> t -> bool
+  (** Equality function on formal universes *)
+
+  val hash : t -> int
+  (** Hash function *)
+
+  val make : Level.t -> t
+  (** Create a universe representing the given level. *)
+
+  val pr : t -> Pp.std_ppcmds
+  (** Pretty-printing *)
+
+  val pr_with : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+
+  val is_level : t -> bool
+  (** Test if the universe is a level or an algebraic universe. *)
+
+  val level : t -> Level.t option
+  (** Try to get a level out of a universe, returns [None] if it
+      is an algebraic universe. *)
+
+  val levels : t -> LSet.t
+  (** Get the levels inside the universe, forgetting about increments *)
+
+  val super : t -> t
+  (** The universe strictly above *)
+    
+  val sup   : t -> t -> t
+  (** The l.u.b. of 2 universes *)
+
+  val type0m : t  
+  (** image of Prop in the universes hierarchy *)
+  
+  val type0 : t  
+  (** image of Set in the universes hierarchy *)
+  
+  val type1 : t 
+  (** the universe of the type of Prop/Set *)
+end
+
+type universe = Universe.t
+
+(** Alias name. *)
+
+val pr_uni : universe -> Pp.std_ppcmds
+	      
+(** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... 
+   Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
+val type0m_univ : universe
+val type0_univ : universe
+val type1_univ : universe
 
 val is_type0_univ : universe -> bool
 val is_type0m_univ : universe -> bool
 val is_univ_variable : universe -> bool
+val is_small_univ : universe -> bool
+
+val sup : universe -> universe -> universe
+val super : universe -> universe
 
 val universe_level : universe -> universe_level option
-val compare_levels : universe_level -> universe_level -> int
 
-(** The type of a universe *)
-val super : universe -> universe
+(** [univ_level_mem l u] Is l is mentionned in u ? *)
+
+val univ_level_mem : universe_level -> universe -> bool
 
-(** The max of 2 universes *)
-val sup   : universe -> universe -> universe
+(** [univ_level_rem u v min] removes [u] from [v], resulting in [min]
+    if [v] was exactly [u]. *)
+
+val univ_level_rem : universe_level -> universe -> universe -> universe
 
 (** {6 Graphs of universes. } *)
 
 type universes
 
-type check_function = universes -> universe -> universe -> bool
-val check_geq : check_function
-val check_eq : check_function
+type 'a check_function = universes -> 'a -> 'a -> bool
+val check_leq : universe check_function
+val check_eq : universe check_function
 
 (** The empty graph of universes *)
+val empty_universes : universes
+
+(** The initial graph of universes: Prop < Set *)
 val initial_universes : universes
+
 val is_initial_universes : universes -> bool
 
+val sort_universes : universes -> universes
+
+(** Adds a universe to the graph, ensuring it is >= Prop. *)
+val add_universe : universe_level -> universes -> universes
+
 (** {6 Constraints. } *)
 
-type constraints
+type constraint_type = Lt | Le | Eq
+type univ_constraint = universe_level * constraint_type * universe_level
+
+module Constraint : sig
+ include Set.S with type elt = univ_constraint
+end
+
+type constraints = Constraint.t
 
 val empty_constraint : constraints
-val union_constraints : constraints -> constraints -> constraints
+val union_constraint : constraints -> constraints -> constraints
+val eq_constraint : constraints -> constraints -> bool
+
+(** A value with universe constraints. *)
+type 'a constrained = 'a * constraints
 
-val is_empty_constraint : constraints -> bool
+(** Constrained *)
+val constraints_of : 'a constrained -> constraints
 
-type constraint_function = universe -> universe -> constraints -> constraints
+(** Enforcing constraints. *)
 
-val enforce_geq : constraint_function
-val enforce_eq : constraint_function
+type 'a constraint_function = 'a -> 'a -> constraints -> constraints
+
+val enforce_eq : universe constraint_function
+val enforce_leq : universe constraint_function
+val enforce_eq_level : universe_level constraint_function
+val enforce_leq_level : universe_level constraint_function
 
 (** {6 ... } *)
 (** Merge of constraints in a universes graph.
@@ -69,38 +198,231 @@ val enforce_eq : constraint_function
   universes graph. It raises the exception [UniverseInconsistency] if the
   constraints are not satisfiable. *)
 
-type constraint_type = Lt | Le | Eq
+(** Type explanation is used to decorate error messages to provide
+  useful explanation why a given constraint is rejected. It is composed
+  of a path of universes and relation kinds [(r1,u1);..;(rn,un)] means
+   .. <(r1) u1 <(r2) ... <(rn) un (where <(ri) is the relation symbol
+  denoted by ri, currently only < and <=). The lowest end of the chain
+  is supposed known (see UniverseInconsistency exn). The upper end may
+  differ from the second univ of UniverseInconsistency because all
+  universes in the path are canonical. Note that each step does not
+  necessarily correspond to an actual constraint, but reflect how the
+  system stores the graph and may result from combination of several
+  constraints...
+*)
+type explanation = (constraint_type * universe) list
+type univ_inconsistency = constraint_type * universe * universe * explanation option
+
+exception UniverseInconsistency of univ_inconsistency
+
+val enforce_constraint : univ_constraint -> universes -> universes
+val merge_constraints : constraints -> universes -> universes
 
-exception UniverseInconsistency of constraint_type * universe * universe
+val constraints_of_universes : universes -> constraints
 
-val merge_constraints : constraints -> universes -> universes
-val normalize_universes : universes -> universes
-val sort_universes : universes -> universes
+val check_constraint  : universes -> univ_constraint -> bool
+val check_constraints : constraints -> universes -> bool
+
+(** {6 Support for universe polymorphism } *)
+
+(** Polymorphic maps from universe levels to 'a *)
+module LMap : 
+sig
+  include CMap.ExtS with type key = universe_level and module Set := LSet
+
+  val union : 'a t -> 'a t -> 'a t
+  (** [union x y] favors the bindings in the first map. *)
+
+  val diff : 'a t -> 'a t -> 'a t
+  (** [diff x y] removes bindings from x that appear in y (whatever the value). *)
 
-(** {6 Support for sort-polymorphic inductive types } *)
+  val subst_union : 'a option t -> 'a option t -> 'a option t
+  (** [subst_union x y] favors the bindings of the first map that are [Some],
+      otherwise takes y's bindings. *)
 
-val fresh_local_univ : unit -> universe
+  val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+  (** Pretty-printing *)
+end
 
-val solve_constraints_system : universe option array -> universe array ->
-  universe array
+type 'a universe_map = 'a LMap.t
 
-val subst_large_constraint : universe -> universe -> universe -> universe
+(** {6 Substitution} *)
 
-val subst_large_constraints :
-  (universe * universe) list -> universe -> universe
+type universe_subst_fn = universe_level -> universe
+type universe_level_subst_fn = universe_level -> universe_level
 
-val no_upper_constraints : universe -> constraints -> bool
+(** A full substitution, might involve algebraic universes *)
+type universe_subst = universe universe_map
+type universe_level_subst = universe_level universe_map
 
-(** Is u mentionned in v (or equals to v) ? *)
+val level_subst_of : universe_subst_fn -> universe_level_subst_fn
 
-val univ_depends : universe -> universe -> bool
+(** {6 Universe instances} *)
+
+module Instance : 
+sig
+  type t
+  (** A universe instance represents a vector of argument universes
+      to a polymorphic definition (constant, inductive or constructor). *)
+
+  val empty : t
+  val is_empty : t -> bool
+
+  val of_array : Level.t array -> t
+  val to_array : t -> Level.t array
+
+  val append : t -> t -> t
+  (** To concatenate two instances, used for discharge *)
+
+  val equal : t -> t -> bool
+  (** Equality *)
+
+  val length : t -> int
+  (** Instance length *)
+
+  val hcons : t -> t
+  (** Hash-consing. *)
+
+  val hash : t -> int
+  (** Hash value *)
+
+  val share : t -> t * int
+  (** Simultaneous hash-consing and hash-value computation *)
+
+  val subst_fn : universe_level_subst_fn -> t -> t
+  (** Substitution by a level-to-level function. *)
+
+  val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+  (** Pretty-printing, no comments *)
+
+  val levels : t -> LSet.t
+  (** The set of levels in the instance *)
+
+  val check_eq : t check_function 
+  (** Check equality of instances w.r.t. a universe graph *)
+end
+
+type universe_instance = Instance.t
+
+val enforce_eq_instances : universe_instance constraint_function
+
+type 'a puniverses = 'a * universe_instance
+val out_punivs : 'a puniverses -> 'a
+val in_punivs : 'a -> 'a puniverses
+
+val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
+
+(** A vector of universe levels with universe constraints,
+    representiong local universe variables and associated constraints *)
+
+module UContext :
+sig 
+  type t
+
+  val make : Instance.t constrained -> t
+
+  val empty : t
+  val is_empty : t -> bool
+    
+  val instance : t -> Instance.t
+  val constraints : t -> constraints
+
+  val dest : t -> Instance.t * constraints
+
+  (** Keeps the order of the instances *)
+  val union : t -> t -> t
+
+end
+
+type universe_context = UContext.t
+
+(** Universe contexts (as sets) *)
+
+module ContextSet :
+sig 
+  type t = universe_set constrained
+
+  val empty : t
+  val is_empty : t -> bool
+
+  val singleton : universe_level -> t
+  val of_instance : Instance.t -> t
+  val of_set : universe_set -> t
+
+  val union : t -> t -> t
+
+  val append : t -> t -> t
+  (** Variant of {!union} which is more efficient when the left argument is
+      much smaller than the right one. *)
+
+  val diff : t -> t -> t
+  val add_universe : universe_level -> t -> t
+  val add_constraints : constraints -> t -> t
+  val add_instance : Instance.t -> t -> t
+
+  (** Arbitrary choice of linear order of the variables *)
+  val to_context : t -> universe_context
+  val of_context : universe_context -> t
+
+  val constraints : t -> constraints
+  val levels : t -> universe_set
+end
+
+(** A set of universes with universe constraints.
+    We linearize the set to a list after typechecking. 
+    Beware, representation could change.
+*)
+type universe_context_set = ContextSet.t
+
+(** A value in a universe context (resp. context set). *)
+type 'a in_universe_context = 'a * universe_context
+type 'a in_universe_context_set = 'a * universe_context_set
+
+val empty_level_subst : universe_level_subst
+val is_empty_level_subst : universe_level_subst -> bool
+
+(** Substitution of universes. *)
+val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
+val subst_univs_level_universe : universe_level_subst -> universe -> universe
+val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
+val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance
+
+(** Level to universe substitutions. *)
+
+val empty_subst : universe_subst
+val is_empty_subst : universe_subst -> bool
+val make_subst : universe_subst -> universe_subst_fn
+
+val subst_univs_universe : universe_subst_fn -> universe -> universe
+val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
+
+(** Substitution of instances *)
+val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
+val subst_instance_universe : universe_instance -> universe -> universe
+val subst_instance_constraints : universe_instance -> constraints -> constraints
+
+val make_instance_subst : universe_instance -> universe_level_subst
+val make_inverse_instance_subst : universe_instance -> universe_level_subst
+
+val abstract_universes : bool -> universe_context -> universe_level_subst * universe_context
+
+(** Get the instantiated graph. *)
+val instantiate_univ_context : universe_context -> universe_context
+
+val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
 
 (** {6 Pretty-printing of universes. } *)
 
-val pr_uni_level : universe_level -> Pp.std_ppcmds
-val pr_uni : universe -> Pp.std_ppcmds
-val pr_universes : universes -> Pp.std_ppcmds
-val pr_constraints : constraints -> Pp.std_ppcmds
+val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
+val pr_constraint_type : constraint_type -> Pp.std_ppcmds
+val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds
+val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds
+val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds
+val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> 
+  univ_inconsistency -> Pp.std_ppcmds
+
+val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds
+val pr_universe_subst : universe_subst -> Pp.std_ppcmds
 
 (** {6 Dumping to a file } *)
 
@@ -110,6 +432,17 @@ val dump_universes :
 
 (** {6 Hash-consing } *)
 
-val hcons_univlevel : universe_level -> universe_level
 val hcons_univ : universe -> universe
 val hcons_constraints : constraints -> constraints
+val hcons_universe_set : universe_set -> universe_set
+val hcons_universe_context : universe_context -> universe_context
+val hcons_universe_context_set : universe_context_set -> universe_context_set 
+
+(******)
+
+(* deprecated: use qualified names instead *)
+val compare_levels : universe_level -> universe_level -> int
+val eq_levels : universe_level -> universe_level -> bool
+
+(** deprecated: Equality of formal universe expressions. *)
+val equal_universes : universe -> universe -> bool