Univs: update checker

9 files changed, 83 insertions, 21 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 881d3ca79..bd75111a2 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 6dbc44d6b..f8f5c29b7 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 f3b2dd839..87f143d1b 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 998e23c6e..78fff1bbe 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -69,7 +69,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 8ccf118d3..7f07f8bf8 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/safe_typing.ml b/checker/safe_typing.ml
index dd9482313..d3bc8373a 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 3bcb3bc95..50c0367bb 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,6 +560,8 @@ let repr g u =
   in
   repr_rec u
 
+let get_set_arc g = repr g Level.set
+
 (* [safe_repr] also search for the canonical representative, but
    if the graph doesn't contain the searched universe, we add it. *)
 
@@ -573,6 +576,24 @@ let safe_repr g u =
     let can = terminal u in
     enter_arc can g, can
 
+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 =
@@ -970,7 +991,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. *)
@@ -1158,6 +1179,7 @@ struct
   type t = LSet.t constrained
   let empty = LSet.empty, Constraint.empty
   let constraints (_, cst) = cst
+  let levels (ctx, _) = ctx
 end
 type universe_context_set = ContextSet.t
 
@@ -1207,6 +1229,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 +1263,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 742ef91ae..459adfcd6 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,7 +124,7 @@ 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 } *)
@@ -193,6 +200,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 +229,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 45220bd05..34de511c8 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 *)