From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- kernel/univ.ml | 406 ++++++++++++++++++++++++++++++++++----------------------- 1 file changed, 244 insertions(+), 162 deletions(-) (limited to 'kernel/univ.ml') diff --git a/kernel/univ.ml b/kernel/univ.ml index 5e9fbd81..23e50282 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,29 +6,41 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: univ.ml,v 1.17.10.3 2005/09/08 12:27:46 herbelin Exp $ *) +(* $Id: univ.ml 8673 2006-03-29 21:21:52Z herbelin $ *) -(* 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$ 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 } + | Base + | Level of Names.dir_path * int type universe = - | Variable of universe_level + | Atom of universe_level | Max of universe_level list * universe_level list module UniverseOrdered = struct @@ -36,61 +48,60 @@ module UniverseOrdered = struct let compare = Pervasives.compare end -let string_of_univ_level u = - Names.string_of_dirpath u.u_mod^"."^string_of_int u.u_num +let string_of_univ_level = function + | Base -> "0" + | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n -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 make_univ (m,n) = Atom (Level (m,n)) let pr_uni_level u = str (string_of_univ_level u) let pr_uni = function - | Variable u -> + | Atom u -> pr_uni_level u + | Max ([],[Base]) -> + int 1 | Max (gel,gtl) -> - str "max(" ++ - prlist_with_sep pr_coma pr_uni_level gel ++ - (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++ - prlist_with_sep pr_coma - (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") 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 + (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 -> + | Atom u -> Max ([],[u]) | Max _ -> - anomaly ("Cannot take the successor of a non variable universes\n"^ + anomaly ("Cannot take the successor of a non variable universes:\n"^ "(maybe a bugged tactic)") -(* 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 = +let sup u v = match u,v with - | Variable u, Variable v -> Max ((if u = v then [u] else [u;v]),[]) - | Variable u, Max (gel,gtl) -> Max (list_add_set u gel,gtl) - | Max (gel,gtl), Variable v -> Max (list_add_set v gel,gtl) + | Atom u, Atom v -> if u = v then Atom u else Max ([u;v],[]) + | u, Max ([],[]) -> u + | Max ([],[]), v -> v + | Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl) + | Max (gel,gtl), Atom v -> Max (list_add_set v gel,gtl) | Max (gel,gtl), Max (gel',gtl') -> - Max (list_union gel gel',list_union gtl gtl') + let gel'' = list_union gel gel' in + let gtl'' = list_union gtl gtl' in + Max (list_subtract gel'' gtl'',gtl'') + +let sup_array ls = Array.fold_right sup ls (Max ([],[])) (* 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 @@ -111,15 +122,23 @@ let declare_univ u g = else g -(* When typing Prop and Set, there is no constraint on the level, - hence the definition of prop_univ *) +(* The level of Set *) +let base_univ = Atom Base + +let is_base = function + | Atom Base -> true + | Max ([Base],[]) -> warning "Non canonical Set"; true + | u -> false + +(* When typing [Prop] and [Set], there is no constraint on the level, + hence the definition of [prop_univ], the type of [Prop] *) let initial_universes = UniverseMap.empty -let prop_univ = Max ([],[]) +let prop_univ = Max ([],[Base]) -(* 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 = @@ -136,30 +155,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 (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 -> @@ -169,17 +188,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 @@ -187,12 +206,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 *) @@ -200,64 +219,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 @@ -265,23 +284,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 @@ -291,55 +310,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 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 *) @@ -351,14 +370,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 @@ -373,25 +392,84 @@ type constraints = Constraint.t type constraint_function = universe -> universe -> constraints -> constraints -let enforce_gt u v c = Constraint.add (u,Gt,v) c +let constraint_add_leq v u c = + if v = Base then c else Constraint.add (v,Leq,u) c let enforce_geq u v c = - match u with - | Variable u -> (match v with - | Variable v -> Constraint.add (u,Geq,v) 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) - | Max _ -> anomaly "A universe bound can only be a variable" + match u, v with + | Atom u, Atom v -> constraint_add_leq v u c + | Atom u, Max (gel,gtl) -> + let d = List.fold_right (fun v -> constraint_add_leq v u) gel c in + List.fold_right (fun v -> Constraint.add (v,Lt,u)) gtl d + | _ -> anomaly "A universe bound can only be a variable" let enforce_eq u v c = match (u,v) with - | Variable u, Variable v -> Constraint.add (u,Eq,v) c + | Atom u, Atom v -> Constraint.add (u,Eq,v) c | _ -> anomaly "A universe comparison can only happen between variables" let merge_constraints c g = Constraint.fold enforce_constraint c g +(**********************************************************************) +(* Tools for sort-polymorphic inductive types *) + +(* Temporary inductive type levels *) + +let fresh_level = + let n = ref 0 in fun () -> incr n; Level (Names.make_dirpath [],!n) + +let fresh_local_univ () = Atom (fresh_level ()) + +(* Miscellaneous functions to remove or test local univ assumed to + occur only in the le constraints *) + +let make_max = function + | ([u],[]) -> Atom u + | (le,lt) -> Max (le,lt) + +let remove_constraint u = function + | Atom u' as x -> if u = u' then Max ([],[]) else x + | Max (le,lt) -> make_max (list_remove u le,lt) + +let is_empty_universe = function + | Max ([],[]) -> true + | _ -> false + +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 + + - the ui (1 <= i <= n) are universe variables, + - the sjk select subsets of the ui for each equations, + - the wi are arbitrary complex universes that do not mention the ui. +*) + +let solve_constraints_system levels level_bounds = + let levels = + Array.map (function Atom u -> u | _ -> anomaly "expects Atom") levels in + let v = Array.copy level_bounds in + let nind = Array.length v in + for i=0 to nind-1 do + for j=0 to nind-1 do + if i<>j & is_direct_constraint levels.(j) v.(i) then + v.(i) <- sup v.(i) v.(j) + done; + for j=0 to nind-1 do + v.(i) <- remove_constraint levels.(j) v.(i) + done + done; + v + (* Pretty-printing *) let num_universes g = @@ -400,19 +478,19 @@ 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 ++ - (if ge <> [] & gt <> [] then spc () else mt ()) ++ - 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 ++ + (if lt <> [] & le <> [] then spc () else mt()) ++ + 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,44 +504,48 @@ 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) in UniverseMap.iter dump_arc g +(* Hash-consing *) + module Huniv = Hashcons.Make( struct type t = universe type u = Names.dir_path -> Names.dir_path - let hash_aux hdir u = { u with u_mod=hdir u.u_mod } + let hash_aux hdir = function + | Base -> Base + | Level (d,n) -> Level (hdir d,n) let hash_sub hdir = function - | Variable u -> Variable (hash_aux hdir u) + | Atom u -> Atom (hash_aux hdir u) | Max (gel,gtl) -> Max (List.map (hash_aux hdir) gel, List.map (hash_aux hdir) gtl) let equal u v = match u, v with - | Variable u, Variable v -> u == v + | Atom u, Atom v -> u == v | Max (gel,gtl), Max (gel',gtl') -> - (List.for_all2 (==) gel gel') && (List.for_all2 (==) gtl gtl') + (list_for_all2eq (==) gel gel') && + (list_for_all2eq (==) gtl gtl') | _ -> false let hash = Hashtbl.hash end) let hcons1_univ u = - let _,hdir,_,_,_ = Names.hcons_names() in + let _,_,hdir,_,_,_ = Names.hcons_names() in Hashcons.simple_hcons Huniv.f hdir u - -- cgit v1.2.3