Merge branch 'v8.5'

10 files changed, 116 insertions, 55 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 881d3ca797..bd75111a2c 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -380,7 +380,7 @@ and module_body =
     (** algebraic type, kept if it's relevant for extraction *)
     mod_type_alg : module_expression option;
     (** set of all constraints in the module  *)
-    mod_constraints : Univ.constraints;
+    mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : delta_resolver;
     mod_retroknowledge : action list }
diff --git a/checker/environ.ml b/checker/environ.ml
index 6dbc44d6b8..f8f5c29b79 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -84,13 +84,20 @@ let push_rec_types (lna,typarray,_) env =
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 (* Universe constraints *)
-let add_constraints c env =
-  if c == Univ.Constraint.empty then
-    env
-  else
-    let s = env.env_stratification in
+let map_universes f env =
+  let s = env.env_stratification in
     { env with env_stratification =
-      { s with env_universes = Univ.merge_constraints c s.env_universes } }
+	 { s with env_universes = f s.env_universes } }
+
+let add_constraints c env =
+  if c == Univ.Constraint.empty then env
+  else map_universes (Univ.merge_constraints c) env
+			   
+let push_context ?(strict=false) ctx env =
+  map_universes (Univ.merge_context strict ctx) env
+
+let push_context_set ?(strict=false) ctx env =
+  map_universes (Univ.merge_context_set strict ctx) env
 
 let check_constraints cst env =
   Univ.check_constraints cst env.env_stratification.env_universes
diff --git a/checker/environ.mli b/checker/environ.mli
index f3b2dd839a..87f143d1bb 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -39,6 +39,8 @@ val push_rec_types : name array * constr array * 'a -> env -> env
 (* Universes *)
 val universes : env -> Univ.universes
 val add_constraints : Univ.constraints -> env -> env
+val push_context : ?strict:bool -> Univ.universe_context -> env -> env
+val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val check_constraints : Univ.constraints -> env -> bool
 
 (* Constants *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 998e23c6e8..3ea5ed0d34 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -18,19 +18,27 @@ let refresh_arity ar =
   let ctxt, hd = decompose_prod_assum ar in
   match hd with
       Sort (Type u) when not (Univ.is_univ_variable u) ->
-        let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in
-        mkArity (ctxt,Prop Null), 
-	  Univ.enforce_leq u u' Univ.empty_constraint
-    | _ -> ar, Univ.empty_constraint
+      let ul = Univ.Level.make empty_dirpath 1 in
+      let u' = Univ.Universe.make ul in
+      let cst = Univ.enforce_leq u u' Univ.empty_constraint in
+      let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
+        mkArity (ctxt,Prop Null), ctx
+    | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn); pp_flush ();
-  let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in
+  let env' =
+    if cb.const_polymorphic then
+      let inst = Univ.make_abstract_instance cb.const_universes in
+      let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in
+        push_context ~strict:false ctx env
+    else push_context ~strict:true cb.const_universes env
+  in
   let envty, ty = 
     match cb.const_type with
       RegularArity ty ->
         let ty', cu = refresh_arity ty in
-        let envty = add_constraints cu env' in
+        let envty = push_context_set cu env' in
         let _ = infer_type envty ty' in envty, ty
     | TemplateArity(ctxt,par) ->
         let _ = check_ctxt env' ctxt in
@@ -69,7 +77,7 @@ let mk_mtb mp sign delta =
     mod_expr = Abstract;
     mod_type = sign;
     mod_type_alg = None;
-    mod_constraints = Univ.Constraint.empty;
+    mod_constraints = Univ.ContextSet.empty;
     mod_delta = delta;
     mod_retroknowledge = []; }
 
diff --git a/checker/modops.ml b/checker/modops.ml
index 8ccf118d3b..7f07f8bf84 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -83,12 +83,13 @@ let strengthen_const mp_from l cb resolver =
     | Def _ -> cb
     | _ ->
       let con = Constant.make2 mp_from l in
-      (* let con =  constant_of_delta resolver con in*)
       let u = 
-	if cb.const_polymorphic then Univ.UContext.instance cb.const_universes 
+	if cb.const_polymorphic then
+	  Univ.make_abstract_instance cb.const_universes
 	else Univ.Instance.empty
       in
-      { cb with const_body = Def (Declarations.from_val (Const (con,u))) }
+      { cb with
+	const_body = Def (Declarations.from_val (Const (con,u))) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 8ddeea2a20..384d883ea3 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -175,7 +175,7 @@ let sort_cmp env univ pb s0 s1 =
         then begin
           if !Flags.debug then begin
             let op = match pb with CONV -> "=" | CUMUL -> "<=" in
-            Printf.eprintf "cort_cmp: %s\n%!" Pp.(string_of_ppcmds
+            Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds
               (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
                ++ Univ.pr_universes univ))
           end;
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index dd94823135..d3bc8373a5 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -27,7 +27,7 @@ let set_engagement c =
 (* full_add_module adds module with universes and constraints *)
 let full_add_module dp mb univs digest =
   let env = !genv in
-  let env = add_constraints mb.mod_constraints env in
+  let env = push_context_set ~strict:true mb.mod_constraints env in
   let env = add_constraints univs env in
   let env = Modops.add_module mb env in
   genv := add_digest env dp digest
@@ -84,7 +84,7 @@ let import file clib univs digest =
   let mb = clib.comp_mod in
   Mod_checking.check_module
     (add_constraints univs
-      (add_constraints mb.mod_constraints env)) mb.mod_mp mb;
+      (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb;
   stamp_library file digest;
   full_add_module clib.comp_name mb univs digest
 
diff --git a/checker/univ.ml b/checker/univ.ml
index 3bcb3bc950..648e478176 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -244,7 +244,8 @@ module Level = struct
 
   let set = make Set
   let prop = make Prop
-
+  let var i = make (Var i)
+		  
   let is_small x = 
     match data x with
     | Level _ -> false
@@ -281,8 +282,8 @@ module Level = struct
 end
 
 (** Level sets and maps *)
-module LSet = Set.Make (Level)
-module LMap = Map.Make (Level)
+module LMap = HMap.Make (Level)
+module LSet = LMap.Set
 
 type 'a universe_map = 'a LMap.t
 
@@ -559,20 +560,26 @@ let repr g u =
   in
   repr_rec u
 
-(* [safe_repr] also search for the canonical representative, but
-   if the graph doesn't contain the searched universe, we add it. *)
-
-let safe_repr g u =
-  let rec safe_repr_rec u =
-    match UMap.find u g with
-      | Equiv v -> safe_repr_rec v
-      | Canonical arc -> arc
-  in
-  try g, safe_repr_rec u
-  with Not_found ->
-    let can = terminal u in
-    enter_arc can g, can
+let get_set_arc g = repr g Level.set
 
+exception AlreadyDeclared
+	    
+let add_universe vlev strict g =
+  try
+    let _arcv = UMap.find vlev g in
+      raise AlreadyDeclared
+  with Not_found -> 
+    let v = terminal vlev in
+    let arc =
+      let arc = get_set_arc g in
+	if strict then
+	  { arc with lt=vlev::arc.lt}
+	else 
+	  { arc with le=vlev::arc.le}
+    in
+    let g = enter_arc arc g in
+      enter_arc v g
+		       
 (* reprleq : canonical_arc -> canonical_arc list *)
 (* All canonical arcv such that arcu<=arcv with arcv#arcu *)
 let reprleq g arcu =
@@ -739,8 +746,8 @@ let is_lt g arcu arcv =
 (** First, checks on universe levels *)
 
 let check_equal g u v =
-  let g, arcu = safe_repr g u in
-  let _, arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   arcu == arcv
 
 let check_eq_level g u v = u == v || check_equal g u v
@@ -749,8 +756,8 @@ let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
 
 let check_smaller g strict u v =
-  let g, arcu = safe_repr g u in
-  let g, arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   if strict then
     is_lt g arcu arcv
   else
@@ -900,8 +907,8 @@ let error_inconsistency o u v =
 (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
 
 let enforce_univ_eq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastEQ -> g
     | FastLT -> error_inconsistency Eq v u
@@ -916,8 +923,8 @@ let enforce_univ_eq u v g =
 (* enforce_univ_leq : Level.t -> Level.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
 let enforce_univ_leq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   if is_leq g arcu arcv then g
   else
     match fast_compare g arcv arcu with
@@ -928,8 +935,8 @@ let enforce_univ_leq u v g =
 
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastLT -> g
     | FastLE -> fst (setlt g arcu arcv)
@@ -941,7 +948,10 @@ let enforce_univ_lt u v g =
       | FastLE | FastLT -> error_inconsistency Lt u v
 
 (* Prop = Set is forbidden here. *)
-let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+let initial_universes =
+  let g = enter_arc (terminal Level.set) UMap.empty in
+  let g = enter_arc (terminal Level.prop) g in
+    enforce_univ_lt Level.prop Level.set g
 
 (* Constraints and sets of constraints. *)    
 
@@ -970,7 +980,7 @@ module Constraint = Set.Make(UConstraintOrd)
 let empty_constraint = Constraint.empty
 let merge_constraints c g =
   Constraint.fold enforce_constraint c g
-
+		  
 type constraints = Constraint.t
 
 (** A value with universe constraints. *)
@@ -1146,7 +1156,7 @@ struct
 
   (** Universe contexts (variables as a list) *)
   let empty = (Instance.empty, Constraint.empty)
-
+  let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
 end
@@ -1158,6 +1168,8 @@ struct
   type t = LSet.t constrained
   let empty = LSet.empty, Constraint.empty
   let constraints (_, cst) = cst
+  let levels (ctx, _) = ctx
+  let make ctx cst = (ctx, cst)
 end
 type universe_context_set = ContextSet.t
 
@@ -1207,6 +1219,9 @@ let subst_instance_constraints s csts =
     (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
     csts Constraint.empty 
 
+let make_abstract_instance (ctx, _) = 
+  Array.mapi (fun i l -> Level.var i) ctx
+
 (** Substitute instance inst for ctx in csts *)
 let instantiate_univ_context (ctx, csts) = 
   (ctx, subst_instance_constraints ctx csts)
@@ -1238,6 +1253,20 @@ let subst_univs_universe fn ul =
 	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u))
 	  substs nosubst
 
+let merge_context strict ctx g =
+  let g = Array.fold_left
+   (* Be lenient, module typing reintroduces universes and 
+      constraints due to includes *)
+	    (fun g v -> try add_universe v strict g with AlreadyDeclared -> g)
+	    g (UContext.instance ctx)
+  in merge_constraints (UContext.constraints ctx) g
+
+let merge_context_set strict ctx g =
+  let g = LSet.fold
+	    (fun v g -> try add_universe v strict g with AlreadyDeclared -> g)
+	    (ContextSet.levels ctx) g
+  in merge_constraints (ContextSet.constraints ctx) g
+
 (** Pretty-printing *)
 
 let pr_arc = function
diff --git a/checker/univ.mli b/checker/univ.mli
index 742ef91aed..02c1bbdb91 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -74,6 +74,13 @@ val check_eq : universe check_function
 (** The initial graph of universes: Prop < Set *)
 val initial_universes : universes
 
+(** Adds a universe to the graph, ensuring it is >= or > Set.
+   @raises AlreadyDeclared if the level is already declared in the graph. *)
+
+exception AlreadyDeclared
+
+val add_universe : universe_level -> bool -> universes -> universes
+
 (** {6 Constraints. } *)
 
 type constraint_type = Lt | Le | Eq
@@ -117,14 +124,14 @@ type univ_inconsistency = constraint_type * universe * universe
 exception UniverseInconsistency of univ_inconsistency
 
 val merge_constraints : constraints -> universes -> universes
-
+						    
 val check_constraints : constraints -> universes -> bool
 
 (** {6 Support for universe polymorphism } *)
 
 (** Polymorphic maps from universe levels to 'a *)
 module LMap : Map.S with type key = universe_level
-
+module LSet : CSig.SetS with type elt = universe_level
 type 'a universe_map = 'a LMap.t
 
 (** {6 Substitution} *)
@@ -177,7 +184,7 @@ sig
   type t
 
   val empty : t
-
+  val make : universe_instance constrained -> t
   val instance : t -> Instance.t
   val constraints : t -> constraints
 
@@ -186,6 +193,7 @@ end
 module ContextSet :
   sig 
     type t
+    val make : LSet.t -> constraints -> t
     val empty : t
     val constraints : t -> constraints
   end
@@ -193,6 +201,9 @@ module ContextSet :
 type universe_context = UContext.t
 type universe_context_set = ContextSet.t
 
+val merge_context : bool -> universe_context -> universes -> universes
+val merge_context_set : bool -> universe_context_set -> universes -> universes
+
 val empty_level_subst : universe_level_subst
 val is_empty_level_subst : universe_level_subst -> bool
 
@@ -219,6 +230,9 @@ val subst_instance_constraints : universe_instance -> constraints -> constraints
 val instantiate_univ_context : universe_context -> universe_context
 val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
 
+(** Build the relative instance corresponding to the context *)
+val make_abstract_instance : universe_context -> universe_instance
+									    
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : universes -> Pp.std_ppcmds
diff --git a/checker/values.ml b/checker/values.ml
index 45220bd051..34de511c8a 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 8b7e75b4b94a2d8506a62508e0374c0a checker/cic.mli
+MD5 76312d06933f47498a1981a6261c9f75 checker/cic.mli
 
 *)
 
@@ -307,10 +307,10 @@ and v_impl =
 and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *)
 and v_module =
   Tuple ("module_body",
-         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
+         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
 and v_modtype =
   Tuple ("module_type_body",
-         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
+         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
 
 (** kernel/safe_typing *)