Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 84 insertions, 87 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 3d254ce6..16544eca 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: univ.ml 11596 2008-11-16 15:34:06Z letouzey $ *)
+(* $Id$ *)
 
 (* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
 (* Extension with algebraic universes by HH [Sep 2001] *)
@@ -55,40 +55,38 @@ let cmp_univ_level u v = match u,v with
       else if i1 > i2 then 1
       else compare dp1 dp2
 
+let string_of_univ_level = function
+  | Set -> "Set"
+  | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
+
+module UniverseLMap =
+ Map.Make (struct type t = universe_level let compare = cmp_univ_level end)
+
 type universe =
   | Atom of universe_level
   | Max of universe_level list * universe_level list
-  
-module UniverseOrdered = struct
-  type t = universe_level
-  let compare = cmp_univ_level
-end
-
-let string_of_univ_level = function
-  | Set -> "0"
-  | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
 
 let make_univ (m,n) = Atom (Level (m,n))
 
 let pr_uni_level u = str (string_of_univ_level u)
 
 let pr_uni = function
-  | Atom u -> 
+  | Atom u ->
       pr_uni_level u
   | Max ([],[u]) ->
       str "(" ++ pr_uni_level u ++ str ")+1"
   | Max (gel,gtl) ->
       str "max(" ++ hov 0
-       (prlist_with_sep pr_coma pr_uni_level gel ++
-	  (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++
-	prlist_with_sep pr_coma
+       (prlist_with_sep pr_comma pr_uni_level gel ++
+	  (if gel <> [] & gtl <> [] then pr_comma () else mt ()) ++
+	prlist_with_sep pr_comma
 	  (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl) ++
       str ")"
 
 (* Returns the formal universe that lies juste above the universe variable u.
    Used to type the sort u. *)
 let super = function
-  | Atom u -> 
+  | Atom u ->
       Max ([],[u])
   | Max _ ->
       anomaly ("Cannot take the successor of a non variable universe:\n"^
@@ -121,18 +119,17 @@ type univ_entry =
     Canonical of canonical_arc
   | Equiv of universe_level * universe_level
 
-module UniverseMap = Map.Make(UniverseOrdered)
 
-type universes = univ_entry UniverseMap.t
-		   
+type universes = univ_entry UniverseLMap.t
+
 let enter_equiv_arc u v g =
-  UniverseMap.add u (Equiv(u,v)) g
+  UniverseLMap.add u (Equiv(u,v)) g
 
 let enter_arc ca g =
-  UniverseMap.add ca.univ (Canonical ca) g
+  UniverseLMap.add ca.univ (Canonical ca) g
 
 let declare_univ u g =
-  if not (UniverseMap.mem u g) then
+  if not (UniverseLMap.mem u g) then
     enter_arc (terminal u) g
   else
     g
@@ -162,20 +159,20 @@ let is_univ_variable = function
 
 let type1_univ = Max ([],[Set])
 
-let initial_universes = UniverseMap.empty
+let initial_universes = UniverseLMap.empty
 
 (* Every universe_level has a unique canonical arc representative *)
 
 (* repr : universes -> universe_level -> canonical_arc *)
 (* canonical representative : we follow the Equiv links *)
-let repr g u = 
+let repr g u =
   let rec repr_rec u =
     let a =
-      try UniverseMap.find u g
+      try UniverseLMap.find u g
       with Not_found -> anomalylabstrm "Univ.repr"
-	  (str"Universe " ++ pr_uni_level u ++ str" undefined") 
+	  (str"Universe " ++ pr_uni_level u ++ str" undefined")
     in
-    match a with 
+    match a with
       | Equiv(_,v) -> repr_rec v
       | Canonical arc -> arc
   in
@@ -192,16 +189,16 @@ let collect g arcu =
   let rec coll_rec lt le = function
     | [],[] -> (lt, list_subtractq le lt)
     | arcv::lt', le' ->
-	if List.memq arcv lt then 
+	if List.memq arcv lt then
 	  coll_rec lt le (lt',le')
 	else
           coll_rec (arcv::lt) le ((can g (arcv.lt@arcv.le))@lt',le')
-    | [], arcw::le' -> 
-	if (List.memq arcw lt) or (List.memq arcw le) then 
+    | [], arcw::le' ->
+	if (List.memq arcw lt) or (List.memq arcw le) then
 	  coll_rec lt le ([],le')
 	else
           coll_rec lt (arcw::le) (can g arcw.lt, (can g arcw.le)@le')
-  in 
+  in
   coll_rec [] [] ([],[arcu])
 
 (* reprleq : canonical_arc -> canonical_arc list *)
@@ -211,19 +208,19 @@ let reprleq g arcu =
     | [] -> w
     | v :: vl ->
 	let arcv = repr g v in
-        if List.memq arcv w || arcu==arcv then 
+        if List.memq arcv w || arcu==arcv then
 	  searchrec w vl
-        else 
+        else
 	  searchrec (arcv :: w) vl
-  in 
+  in
   searchrec [] arcu.le
 
 
 (* between : universe_level -> canonical_arc -> canonical_arc list *)
-(* between u v = {w|u<=w<=v, w canonical}          *)     
+(* between u v = {w|u<=w<=v, w canonical}          *)
 (* between is the most costly operation *)
 
-let between g u arcv = 
+let between g u arcv =
   (* good are all w | u <= w <= v  *)
   (* bad are all w | u <= w ~<= v *)
     (* find good and bad nodes in {w | u <= w} *)
@@ -233,50 +230,50 @@ let between g u arcv =
       (good, bad, true) (* b or true *)
     else if List.memq arcu bad then
       input    (* (good, bad, b or false) *)
-    else 
-      let leq = reprleq g arcu in 
+    else
+      let leq = reprleq g arcu in
 	(* is some universe >= u good ? *)
-      let good, bad, b_leq = 
+      let good, bad, b_leq =
 	List.fold_left explore (good, bad, false) leq
       in
 	if b_leq then
 	  arcu::good, bad, true (* b or true *)
-	else 
+	else
 	  good, arcu::bad, b    (* b or false *)
   in
   let good,_,_ = explore ([arcv],[],false) (repr g u) in
     good
-      
+
 (* We assume  compare(u,v) = LE with v canonical (see compare below).
    In this case List.hd(between g u v) = repr u
-   Otherwise, between g u v = [] 
+   Otherwise, between g u v = []
  *)
 
 
 type order = EQ | LT | LE | NLE
 
 (* compare : universe_level -> universe_level -> order *)
-let compare g u v = 
-  let arcu = repr g u 
+let compare g u v =
+  let arcu = repr g u
   and arcv = repr g v in
-  if arcu==arcv then 
+  if arcu==arcv then
     EQ
-  else 
+  else
     let (lt,leq) = collect g arcu in
-    if List.memq arcv lt then 
+    if List.memq arcv lt then
       LT
-    else if List.memq arcv leq then 
+    else if List.memq arcv leq then
       LE
-    else 
+    else
       NLE
 
 (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
                 compare(u,v) = LT or LE => compare(v,u) = NLE
                 compare(u,v) = NLE => compare(v,u) = NLE or LE or LT
 
-   Adding u>=v is consistent iff compare(v,u) # LT 
+   Adding u>=v is consistent iff compare(v,u) # LT
     and then it is redundant iff compare(u,v) # NLE
-   Adding u>v is consistent iff compare(v,u) = NLE 
+   Adding u>v is consistent iff compare(v,u) = NLE
     and then it is redundant iff compare(u,v) = LT *)
 
 let compare_eq g u v =
@@ -288,7 +285,7 @@ let compare_eq g u v =
 type check_function = universes -> universe -> universe -> bool
 
 let incl_list cmp l1 l2 =
-  List.for_all (fun x1 -> List.exists (fun x2 -> cmp x1 x2) l2) l1 
+  List.for_all (fun x1 -> List.exists (fun x2 -> cmp x1 x2) l2) l1
 
 let compare_list cmp l1 l2 =
   incl_list cmp l1 l2 && incl_list cmp l2 l1
@@ -361,7 +358,7 @@ let merge g u v =
                  (* redirected to it *)
 	let redirect (g,w,w') arcv =
  	  let g' = enter_equiv_arc arcv.univ arcu.univ g in
- 	  (g',list_unionq arcv.lt w,arcv.le@w') 
+ 	  (g',list_unionq arcv.lt w,arcv.le@w')
 	in
 	let (g',w,w') = List.fold_left redirect (g,[],[]) v in
 	let g'' = List.fold_left (fun g -> setlt_if g arcu.univ) g' w in
@@ -395,7 +392,7 @@ let enforce_univ_leq u v g =
   let g = declare_univ u g in
   let g = declare_univ v g in
   match compare g u v with
-    | NLE -> 
+    | NLE ->
 	(match compare g v u with
            | LT -> error_inconsistency Le u v
            | LE -> merge g v u
@@ -412,7 +409,7 @@ let enforce_univ_eq u v g =
     | EQ -> g
     | LT -> error_inconsistency Eq u v
     | LE -> merge g u v
-    | NLE -> 
+    | NLE ->
 	(match compare g v u with
            | LT -> error_inconsistency Eq u v
            | LE -> merge g v u
@@ -427,13 +424,13 @@ let enforce_univ_lt u v g =
     | LT -> g
     | LE -> setlt g u v
     | EQ -> error_inconsistency Lt u v
-    | NLE -> 
+    | NLE ->
 	(match compare g v u with
            | NLE -> setlt g u v
            | _ -> error_inconsistency Lt u v)
 
 (*
-let enforce_univ_relation g = function 
+let enforce_univ_relation g = function
   | Equiv (u,v) -> enforce_univ_eq u v g
   | Canonical {univ=u; lt=lt; le=le} ->
       let g' = List.fold_right (enforce_univ_lt u) lt g in
@@ -443,7 +440,7 @@ let enforce_univ_relation g = function
 (* Merging 2 universe graphs *)
 (*
 let merge_universes sp u1 u2 =
-  UniverseMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2
+  UniverseLMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2
 *)
 
 
@@ -461,14 +458,14 @@ let enforce_constraint cst g =
 
 
 module Constraint = Set.Make(
-  struct 
-    type t = univ_constraint 
-    let compare = Pervasives.compare 
+  struct
+    type t = univ_constraint
+    let compare = Pervasives.compare
   end)
-		      
+
 type constraints = Constraint.t
 
-type constraint_function = 
+type constraint_function =
     universe -> universe -> constraints -> constraints
 
 let constraint_add_leq v u c =
@@ -515,17 +512,17 @@ let is_direct_constraint u = function
   | Atom u' -> u = u'
   | Max (le,lt) -> List.mem u le
 
-(* 
+(*
    Solve a system of universe constraint of the form
 
    u_s11, ..., u_s1p1, w1 <= u1
    ...
    u_sn1, ..., u_snpn, wn <= un
 
-where 
+where
 
   - the ui (1 <= i <= n) are universe variables,
-  - the sjk select subsets of the ui for each equations, 
+  - the sjk select subsets of the ui for each equations,
   - the wi are arbitrary complex universes that do not mention the ui.
 *)
 
@@ -534,7 +531,7 @@ let is_direct_sort_constraint s v = match s with
   | None -> false
 
 let solve_constraints_system levels level_bounds =
-  let levels = 
+  let levels =
     Array.map (Option.map (function Atom u -> u | _ -> anomaly "expects Atom"))
       levels in
   let v = Array.copy level_bounds in
@@ -553,7 +550,7 @@ let solve_constraints_system levels level_bounds =
   v
 
 let subst_large_constraint u u' v =
-  match u with 
+  match u with
   | Atom u ->
       if is_direct_constraint u v then sup u' (remove_large_constraint u v)
       else v
@@ -571,16 +568,16 @@ let no_upper_constraints u cst =
 (* Pretty-printing *)
 
 let num_universes g =
-  UniverseMap.fold (fun _ _ -> succ) g 0
+  UniverseLMap.fold (fun _ _ -> succ) g 0
 
 let num_edges g =
   let reln_len = function
     | Equiv _ -> 1
     | Canonical {lt=lt;le=le} -> List.length lt + List.length le
   in
-  UniverseMap.fold (fun _ a n -> n + (reln_len a)) g 0
-    
-let pr_arc = function 
+  UniverseLMap.fold (fun _ a n -> n + (reln_len a)) g 0
+
+let pr_arc = function
   | Canonical {univ=u; lt=[]; le=[]} ->
       mt ()
   | Canonical {univ=u; lt=lt; le=le} ->
@@ -590,43 +587,43 @@ let pr_arc = function
 	 (if lt <> [] & le <> [] then spc () else mt()) ++
          prlist_with_sep pr_spc (fun v -> str "<= " ++ pr_uni_level v) le) ++
       fnl ()
-  | Equiv (u,v) -> 
+  | Equiv (u,v) ->
       pr_uni_level u  ++ str " = " ++ pr_uni_level v ++ fnl ()
 
 let pr_universes g =
-  let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in
+  let graph = UniverseLMap.fold (fun k a l -> (k,a)::l) g [] in
   prlist (function (_,a) -> pr_arc a) graph
-    
+
 let pr_constraints c =
-  Constraint.fold (fun (u1,op,u2) pp_std -> 
-		     let op_str = match op with 
+  Constraint.fold (fun (u1,op,u2) pp_std ->
+		     let op_str = match op with
 		       | Lt -> " < "
 		       | Leq -> " <= "
 		       | Eq -> " = "
 		     in pp_std ++  pr_uni_level u1 ++ str op_str ++
 			  pr_uni_level u2 ++ fnl () )  c (str "")
-    
-(* Dumping constrains to a file *)
 
-let dump_universes output g = 
+(* Dumping constraints to a file *)
+
+let dump_universes output g =
   let dump_arc _ = function
-    | Canonical {univ=u; lt=lt; le=le} -> 
+    | Canonical {univ=u; lt=lt; le=le} ->
 	let u_str = string_of_univ_level u in
-	  List.iter 
-	    (fun v -> 
+	  List.iter
+	    (fun v ->
 	       Printf.fprintf output "%s < %s ;\n" u_str
-		 (string_of_univ_level v)) 
+		 (string_of_univ_level v))
 	    lt;
-	  List.iter 
-	    (fun v -> 
+	  List.iter
+	    (fun v ->
 	       Printf.fprintf output "%s <= %s ;\n" u_str
-		 (string_of_univ_level v)) 
+		 (string_of_univ_level v))
 	    le
     | Equiv (u,v) ->
 	Printf.fprintf output "%s = %s ;\n"
 	  (string_of_univ_level u) (string_of_univ_level v)
   in
-    UniverseMap.iter dump_arc g 
+    UniverseLMap.iter dump_arc g
 
 (* Hash-consing *)