MAJ commentaires et inversion du sens du graphe de contraintes pour extensibilité aux contraintes numériques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6992 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 130 insertions, 128 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index fb372d2f8..07bf61002 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -8,21 +8,33 @@
 
 (* $Id$ *)
 
-(* Universes are stratified by a partial ordering $\ge$.
+(* Universes are stratified by a partial ordering $\le$.
    Let $\~{}$ be the associated equivalence. We also have a strict ordering
-   $>$ between equivalence classes, and we maintain that $>$ is acyclic,
-   and contained in $\ge$ in the sense that $[U]>[V]$ implies $U\ge V$.
+   $<$ between equivalence classes, and we maintain that $<$ is acyclic,
+   and contained in $\le$ in the sense that $[U]<[V]$ implies $U\le V$.
 
    At every moment, we have a finite number of universes, and we
-   maintain the ordering in the presence of assertions $U>V$ and $U\ge V$.
+   maintain the ordering in the presence of assertions $U<V$ and $U\le V$.
 
    The equivalence $\~{}$ is represented by a tree structure, as in the
-   union-find algorithm. The assertions $>$ and $\ge$ are represented by
+   union-find algorithm. The assertions $<$ and $\le$ are represented by
    adjacency lists *)
 
 open Pp
 open Util
 
+(* An algebraic universe [universe] is either a universe variable
+   [universe_level] or a formal universe known to be greater than some
+   universe variables and strictly greater than some (other) universe
+   variables
+
+   Universes variables denote universes initially present in the term
+   to type-check and non variable algebraic universes denote the
+   universes inferred while type-checking: it is either the successor
+   of a universe present in the initial term to type-check or the
+   maximum of two algebraic universes
+ *)
+
 type universe_level =
     { u_mod : Names.dir_path;
       u_num : int }
@@ -41,19 +53,13 @@ let string_of_univ_level u =
 
 let make_univ (m,n) = Variable { u_mod=m; u_num=n }
 
-let string_of_univ = function
-  | Variable u -> string_of_univ_level u
-  | Max (gel,gtl) -> 
-      "max("^
-      (String.concat ","
-	 ((List.map string_of_univ_level gel)@
-	  (List.map (fun u -> "("^(string_of_univ_level u)^")+1") gtl)))^")"
-
 let pr_uni_level u = str (string_of_univ_level u)
 
 let pr_uni = function
   | Variable u -> 
       pr_uni_level u
+  | Max ([],[]) ->
+      int 1
   | Max (gel,gtl) ->
       str "max(" ++ 
       prlist_with_sep pr_coma pr_uni_level gel ++
@@ -62,8 +68,7 @@ let pr_uni = function
 	(fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl ++
       str ")"
 
-(* Returns a fresh universe, juste above u. Does not create new universes
-   for Type_0 (the sort of Prop and Set).
+(* Returns the formal universe that lies juste above the universe variable u.
    Used to type the sort u. *)
 let super = function
   | Variable u -> 
@@ -73,8 +78,7 @@ let super = function
        "you are probably typing a type already known to be the type\n"^
        "of a user-provided term; if you really need this, please report")
 
-(* returns the least upper bound of universes u and v. If they are not
-   constrained, then a new universe is created.
+(* Returns the formal universe that is greater than the universes u and v.
    Used to type the products. *)
 let sup u v = 
   match u,v with
@@ -86,12 +90,12 @@ let sup u v =
 
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
-    { univ: universe_level; gt: universe_level list; ge: universe_level list }
+    { univ: universe_level; lt: universe_level list; le: universe_level list }
 
-let terminal u = {univ=u; gt=[]; ge=[]}
+let terminal u = {univ=u; lt=[]; le=[]}
 
-(* A universe is either an alias for another one, or a canonical one,
-   for which we know the universes that are smaller *)
+(* A universe_level is either an alias for another one, or a canonical one,
+   for which we know the universes that are above *)
 type univ_entry =
     Canonical of canonical_arc
   | Equiv of universe_level * universe_level
@@ -118,9 +122,9 @@ let declare_univ u g =
 let initial_universes = UniverseMap.empty
 let prop_univ = Max ([],[])
 
-(* Every universe has a unique canonical arc representative *)
+(* Every universe_level has a unique canonical arc representative *)
 
-(* repr : universes -> universe -> canonical_arc *)
+(* repr : universes -> universe_level -> canonical_arc *)
 (* canonical representative : we follow the Equiv links *)
 let repr g u = 
   let rec repr_rec u =
@@ -137,30 +141,30 @@ let repr g u =
 
 let can g = List.map (repr g)
 
-(* transitive closure : we follow the Greater links *)
+(* transitive closure : we follow the Less links *)
 
 (* collect : canonical_arc -> canonical_arc list * canonical_arc list *)
-(* collect u = (V,W) iff V={v canonical | u>v} W={w canonical | u>=w}-V *)
-(* i.e. collect does the transitive closure of what is known about u *)
-let collect g arcu = 
-  let rec coll_rec gt ge = function
-    | [],[] -> (gt, list_subtractq ge gt)
-    | arcv::gt', ge' ->
-	if List.memq arcv gt then 
-	  coll_rec gt ge (gt',ge')
+(* collect u = (V,W) iff V={v canonical | u<v} W={w canonical | u<=w}-V *)
+(* i.e. collect does the transitive upward closure of what is known about u *)
+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 
+	  coll_rec lt le (lt',le')
 	else
-          coll_rec (arcv::gt) ge ((can g (arcv.gt@arcv.ge))@gt',ge')
-    | [], arcw::ge' -> 
-	if (List.memq arcw gt) or (List.memq arcw ge) then 
-	  coll_rec gt ge ([],ge')
+          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 
+	  coll_rec lt le ([],le')
 	else
-          coll_rec gt (arcw::ge) (can g arcw.gt, (can g arcw.ge)@ge')
+          coll_rec lt (arcw::le) (can g arcw.lt, (can g arcw.le)@le')
   in 
   coll_rec [] [] ([],[arcu])
 
-(* reprgeq : canonical_arc -> canonical_arc list *)
-(* All canonical arcv such that arcu>=arcc with arcv#arcu *)
-let reprgeq g arcu =
+(* reprleq : canonical_arc -> canonical_arc list *)
+(* All canonical arcv such that arcu<=arcv with arcv#arcu *)
+let reprleq g arcu =
   let rec searchrec w = function
     | [] -> w
     | v :: vl ->
@@ -170,17 +174,17 @@ let reprgeq g arcu =
         else 
 	  searchrec (arcv :: w) vl
   in 
-  searchrec [] arcu.ge
+  searchrec [] arcu.le
 
 
-(* between : universe -> canonical_arc -> canonical_arc list *)
-(* between u v = {w|u>=w>=v, w canonical}          *)     
+(* between : universe_level -> canonical_arc -> canonical_arc list *)
+(* between u v = {w|u<=w<=v, w canonical}          *)     
 (* between is the most costly operation *)
 
 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} *)
+  (* good are all w | u <= w <= v  *)
+  (* bad are all w | u <= w ~<= v *)
+    (* find good and bad nodes in {w | u <= w} *)
     (* explore b u = (b or "u is good") *)
   let rec explore ((good, bad, b) as input) arcu =
     if List.memq arcu good then
@@ -188,12 +192,12 @@ let between g u arcv =
     else if List.memq arcu bad then
       input    (* (good, bad, b or false) *)
     else 
-      let childs = reprgeq g arcu in 
-	(* are any children of u good ? *)
-      let good, bad, b_childs = 
-	List.fold_left explore (good, bad, false) childs 
+      let leq = reprleq g arcu in 
+	(* is some universe >= u good ? *)
+      let good, bad, b_leq = 
+	List.fold_left explore (good, bad, false) leq
       in
-	if b_childs then
+	if b_leq then
 	  arcu::good, bad, true (* b or true *)
 	else 
 	  good, arcu::bad, b    (* b or false *)
@@ -201,64 +205,64 @@ let between g u arcv =
   let good,_,_ = explore ([arcv],[],false) (repr g u) in
     good
       
-(* We assume  compare(u,v) = GE with v canonical (see compare below).
+(* 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 = [] 
  *)
 
 
-type order = EQ | GT | GE | NGE
+type order = EQ | LT | LE | NLE
 
-(* compare : universe -> universe -> order *)
+(* compare : universe_level -> universe_level -> order *)
 let compare g u v = 
   let arcu = repr g u 
   and arcv = repr g v in
   if arcu==arcv then 
     EQ
   else 
-    let (gt,geq) = collect g arcu in
-    if List.memq arcv gt then 
-      GT
-    else if List.memq arcv geq then 
-      GE
+    let (lt,leq) = collect g arcu in
+    if List.memq arcv lt then 
+      LT
+    else if List.memq arcv leq then 
+      LE
     else 
-      NGE
+      NLE
 
 (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
-                compare(u,v) = GT or GE => compare(v,u) = NGE
-                compare(u,v) = NGE => compare(v,u) = NGE or GE or GT
+                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) # GT 
-    and then it is redundant iff compare(u,v) # NGE
-   Adding u>v is consistent iff compare(v,u) = NGE 
-    and then it is redundant iff compare(u,v) = GT *)
+   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 
+    and then it is redundant iff compare(u,v) = LT *)
 
 
-(* setgt : universe -> universe -> unit *)
+(* setlt : universe_level -> universe_level -> unit *)
 (* forces u > v *)
-let setgt g u v =
+let setlt g u v =
   let arcu = repr g u in
-  enter_arc {arcu with gt=v::arcu.gt} g
+  enter_arc {arcu with lt=v::arcu.lt} g
 
-(* checks that non-redondant *)
-let setgt_if g u v = match compare g u v with
-  | GT -> g
-  | _ -> setgt g u v
+(* checks that non-redundant *)
+let setlt_if g u v = match compare g u v with
+  | LT -> g
+  | _ -> setlt g u v
 
-(* setgeq : universe -> universe -> unit *)
+(* setleq : universe_level -> universe_level -> unit *)
 (* forces u >= v *)
-let setgeq g u v =
+let setleq g u v =
   let arcu = repr g u in
-  enter_arc {arcu with ge=v::arcu.ge} g
+  enter_arc {arcu with le=v::arcu.le} g
 
 
-(* checks that non-redondant *)
-let setgeq_if g u v = match compare g u v with
-  | NGE -> setgeq g u v
+(* checks that non-redundant *)
+let setleq_if g u v = match compare g u v with
+  | NLE -> setleq g u v
   | _ -> g
 
-(* merge : universe -> universe -> unit *)
-(* we assume  compare(u,v) = GE *)
+(* merge : universe_level -> universe_level -> unit *)
+(* we assume  compare(u,v) = LE *)
 (* merge u v  forces u ~ v with repr u as canonical repr *)
 let merge g u v =
   match between g u (repr g v) with
@@ -266,23 +270,23 @@ 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.gt w,arcv.ge@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 -> setgt_if g arcu.univ) g' w in
-	let g''' = List.fold_left (fun g -> setgeq_if g arcu.univ) g'' w' in
+	let g'' = List.fold_left (fun g -> setlt_if g arcu.univ) g' w in
+	let g''' = List.fold_left (fun g -> setleq_if g arcu.univ) g'' w' in
 	g'''
     | [] -> anomaly "Univ.between"
 
-(* merge_disc : universe -> universe -> unit *)
-(* we assume  compare(u,v) = compare(v,u) = NGE *)
+(* merge_disc : universe_level -> universe_level -> unit *)
+(* we assume  compare(u,v) = compare(v,u) = NLE *)
 (* merge_disc u v  forces u ~ v with repr u as canonical repr *)
 let merge_disc g u v =
   let arcu = repr g u in
   let arcv = repr g v in
   let g' = enter_equiv_arc arcv.univ arcu.univ g in
-  let g'' = List.fold_left (fun g -> setgt_if g arcu.univ) g' arcv.gt in
-  let g''' = List.fold_left (fun g -> setgeq_if g arcu.univ) g'' arcv.ge in
+  let g'' = List.fold_left (fun g -> setlt_if g arcu.univ) g' arcv.lt in
+  let g''' = List.fold_left (fun g -> setleq_if g arcu.univ) g'' arcv.le in
   g'''
 
 (* Universe inconsistency: error raised when trying to enforce a relation
@@ -292,55 +296,55 @@ exception UniverseInconsistency
 
 let error_inconsistency () = raise UniverseInconsistency
 
-(* enforcegeq : universe -> universe -> unit *)
-(* enforcegeq u v will force u>=v if possible, will fail otherwise *)
-let enforce_univ_geq u v g =
+(* enforce_univ_leq : universe_level -> universe_level -> unit *)
+(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
+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
-    | NGE -> 
+    | NLE -> 
 	(match compare g v u with
-           | GT -> error_inconsistency()
-           | GE -> merge g v u
-           | NGE -> setgeq g u v
+           | LT -> error_inconsistency()
+           | LE -> merge g v u
+           | NLE -> setleq g u v
            | EQ -> anomaly "Univ.compare")
     | _ -> g
 
-(* enforceq : universe -> universe -> unit *)
-(* enforceq u v will force u=v if possible, will fail otherwise *)
+(* enforc_univ_eq : universe_level -> universe_level -> unit *)
+(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
 let enforce_univ_eq u v g =
   let g = declare_univ u g in
   let g = declare_univ v g in
   match compare g u v with
     | EQ -> g
-    | GT -> error_inconsistency()
-    | GE -> merge g u v
-    | NGE -> 
+    | LT -> error_inconsistency()
+    | LE -> merge g u v
+    | NLE -> 
 	(match compare g v u with
-           | GT -> error_inconsistency()
-           | GE -> merge g v u
-           | NGE -> merge_disc g u v
+           | LT -> error_inconsistency()
+           | LE -> merge g v u
+           | NLE -> merge_disc g u v
            | EQ -> anomaly "Univ.compare")
 
-(* enforcegt u v will force u>v if possible, will fail otherwise *)
-let enforce_univ_gt 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 = declare_univ u g in
   let g = declare_univ v g in
   match compare g u v with
-    | GT -> g
-    | GE -> setgt g u v
+    | LT -> g
+    | LE -> setlt g u v
     | EQ -> error_inconsistency()
-    | NGE -> 
+    | NLE -> 
 	(match compare g v u with
-           | NGE -> setgt g u v
+           | NLE -> setlt g u v
            | _ -> error_inconsistency())
 
 (*
 let enforce_univ_relation g = function 
   | Equiv (u,v) -> enforce_univ_eq u v g
-  | Canonical {univ=u; gt=gt; ge=ge} ->
-      let g' = List.fold_right (enforce_univ_gt u) gt g in
-      List.fold_right (enforce_univ_geq u) ge g'
+  | Canonical {univ=u; lt=lt; le=le} ->
+      let g' = List.fold_right (enforce_univ_lt u) lt g in
+      List.fold_right (enforce_univ_leq u) le g'
 *)
 
 (* Merging 2 universe graphs *)
@@ -352,14 +356,14 @@ let merge_universes sp u1 u2 =
 
 (* Constraints and sets of consrtaints. *)
 
-type constraint_type = Gt | Geq | Eq
+type constraint_type = Lt | Leq | Eq
 
 type univ_constraint = universe_level * constraint_type * universe_level
 
 let enforce_constraint cst g =
   match cst with
-    | (u,Gt,v) -> enforce_univ_gt u v g
-    | (u,Geq,v) -> enforce_univ_geq u v g
+    | (u,Lt,v) -> enforce_univ_lt u v g
+    | (u,Leq,v) -> enforce_univ_leq u v g
     | (u,Eq,v) -> enforce_univ_eq u v g
 
 
@@ -374,15 +378,13 @@ type constraints = Constraint.t
 type constraint_function = 
     universe -> universe -> constraints -> constraints
 
-let enforce_gt u v c = Constraint.add (u,Gt,v) c
-
 let enforce_geq u v c =
   match u with
     | Variable u -> (match v with
-	| Variable v -> Constraint.add (u,Geq,v) c
+	| Variable v -> Constraint.add (v,Leq,u) c
 	| Max (l1, l2) ->
-	    let d = List.fold_right (fun v -> Constraint.add (u,Geq,v)) l1 c in
-	    List.fold_right (fun v -> Constraint.add (u,Gt,v)) l2 d) 
+	    let d = List.fold_right (fun v -> Constraint.add (v,Leq,u)) l1 c in
+	    List.fold_right (fun v -> Constraint.add (v,Lt,u)) l2 d) 
     | Max _ -> anomaly "A universe bound can only be a variable"
 
 let enforce_eq u v c =
@@ -401,18 +403,18 @@ let num_universes g =
 let num_edges g =
   let reln_len = function
     | Equiv _ -> 1
-    | Canonical {gt=gt;ge=ge} -> List.length gt + List.length ge
+    | 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 
-  | Canonical {univ=u; gt=[]; ge=[]} ->
+  | Canonical {univ=u; lt=[]; le=[]} ->
       mt ()
-  | Canonical {univ=u; gt=gt; ge=ge} ->
+  | Canonical {univ=u; lt=lt; le=le} ->
       pr_uni_level u ++ str " " ++
       v 0
-        (prlist_with_sep pr_spc (fun v -> str "> " ++ pr_uni_level v) gt ++
-         prlist_with_sep pr_spc (fun v -> str ">= " ++ pr_uni_level v) ge) ++
+        (prlist_with_sep pr_spc (fun v -> str "< " ++ pr_uni_level v) lt ++
+         prlist_with_sep pr_spc (fun v -> str "<= " ++ pr_uni_level v) le) ++
       fnl ()
   | Equiv (u,v) -> 
       pr_uni_level u  ++ str " = " ++ pr_uni_level v ++ fnl ()
@@ -426,18 +428,18 @@ let pr_universes g =
 
 let dump_universes output g = 
   let dump_arc _ = function
-    | Canonical {univ=u; gt=gt; ge=ge} -> 
+    | Canonical {univ=u; lt=lt; le=le} -> 
 	let u_str = string_of_univ_level u in
 	  List.iter 
 	    (fun v -> 
 	       Printf.fprintf output "%s > %s ;\n" u_str
 		 (string_of_univ_level v)) 
-	    gt;
+	    lt;
 	  List.iter 
 	    (fun v -> 
 	       Printf.fprintf output "%s >= %s ;\n" u_str
 		 (string_of_univ_level v)) 
-	    ge
+	    le
     | Equiv (u,v) ->
 	Printf.fprintf output "%s = %s ;\n"
 	  (string_of_univ_level u) (string_of_univ_level v)