1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: univ.ml 11596 2008-11-16 15:34:06Z letouzey $ *)
11
(* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
12
(* Extension with algebraic universes by HH [Sep 2001] *)
13
(* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *)
15
(* Universes are stratified by a partial ordering $\le$.
16
Let $\~{}$ be the associated equivalence. We also have a strict ordering
17
$<$ between equivalence classes, and we maintain that $<$ is acyclic,
18
and contained in $\le$ in the sense that $[U]<[V]$ implies $U\le V$.
20
At every moment, we have a finite number of universes, and we
21
maintain the ordering in the presence of assertions $U<V$ and $U\le V$.
23
The equivalence $\~{}$ is represented by a tree structure, as in the
24
union-find algorithm. The assertions $<$ and $\le$ are represented by
30
(* An algebraic universe [universe] is either a universe variable
31
[universe_level] or a formal universe known to be greater than some
32
universe variables and strictly greater than some (other) universe
35
Universes variables denote universes initially present in the term
36
to type-check and non variable algebraic universes denote the
37
universes inferred while type-checking: it is either the successor
38
of a universe present in the initial term to type-check or the
39
maximum of two algebraic universes
44
| Level of Names.dir_path * int
46
(* A specialized comparison function: we compare the [int] part first.
47
This way, most of the time, the [dir_path] part is not considered. *)
49
let cmp_univ_level u v = match u,v with
53
| Level (dp1,i1), Level (dp2,i2) ->
55
else if i1 > i2 then 1
59
| Atom of universe_level
60
| Max of universe_level list * universe_level list
62
module UniverseOrdered = struct
63
type t = universe_level
64
let compare = cmp_univ_level
67
let string_of_univ_level = function
69
| Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
71
let make_univ (m,n) = Atom (Level (m,n))
73
let pr_uni_level u = str (string_of_univ_level u)
79
str "(" ++ pr_uni_level u ++ str ")+1"
82
(prlist_with_sep pr_coma pr_uni_level gel ++
83
(if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++
84
prlist_with_sep pr_coma
85
(fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl) ++
88
(* Returns the formal universe that lies juste above the universe variable u.
89
Used to type the sort u. *)
94
anomaly ("Cannot take the successor of a non variable universe:\n"^
95
"(maybe a bugged tactic)")
97
(* Returns the formal universe that is greater than the universes u and v.
98
Used to type the products. *)
102
if cmp_univ_level u v = 0 then Atom u else Max ([u;v],[])
103
| u, Max ([],[]) -> u
104
| Max ([],[]), v -> v
105
| Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
106
| Max (gel,gtl), Atom v -> Max (list_add_set v gel,gtl)
107
| Max (gel,gtl), Max (gel',gtl') ->
108
let gel'' = list_union gel gel' in
109
let gtl'' = list_union gtl gtl' in
110
Max (list_subtract gel'' gtl'',gtl'')
112
(* Comparison on this type is pointer equality *)
114
{ univ: universe_level; lt: universe_level list; le: universe_level list }
116
let terminal u = {univ=u; lt=[]; le=[]}
118
(* A universe_level is either an alias for another one, or a canonical one,
119
for which we know the universes that are above *)
121
Canonical of canonical_arc
122
| Equiv of universe_level * universe_level
124
module UniverseMap = Map.Make(UniverseOrdered)
126
type universes = univ_entry UniverseMap.t
128
let enter_equiv_arc u v g =
129
UniverseMap.add u (Equiv(u,v)) g
132
UniverseMap.add ca.univ (Canonical ca) g
134
let declare_univ u g =
135
if not (UniverseMap.mem u g) then
136
enter_arc (terminal u) g
140
(* The lower predicative level of the hierarchy that contains (impredicative)
141
Prop and singleton inductive types *)
142
let type0m_univ = Max ([],[])
144
let is_type0m_univ = function
145
| Max ([],[]) -> true
148
(* The level of predicative Set *)
149
let type0_univ = Atom Set
151
let is_type0_univ = function
153
| Max ([Set],[]) -> warning "Non canonical Set"; true
156
let is_univ_variable = function
157
| Atom a when a<>Set -> true
160
(* When typing [Prop] and [Set], there is no constraint on the level,
161
hence the definition of [type1_univ], the type of [Prop] *)
163
let type1_univ = Max ([],[Set])
165
let initial_universes = UniverseMap.empty
167
(* Every universe_level has a unique canonical arc representative *)
169
(* repr : universes -> universe_level -> canonical_arc *)
170
(* canonical representative : we follow the Equiv links *)
174
try UniverseMap.find u g
175
with Not_found -> anomalylabstrm "Univ.repr"
176
(str"Universe " ++ pr_uni_level u ++ str" undefined")
179
| Equiv(_,v) -> repr_rec v
180
| Canonical arc -> arc
184
let can g = List.map (repr g)
186
(* transitive closure : we follow the Less links *)
188
(* collect : canonical_arc -> canonical_arc list * canonical_arc list *)
189
(* collect u = (V,W) iff V={v canonical | u<v} W={w canonical | u<=w}-V *)
190
(* i.e. collect does the transitive upward closure of what is known about u *)
192
let rec coll_rec lt le = function
193
| [],[] -> (lt, list_subtractq le lt)
195
if List.memq arcv lt then
196
coll_rec lt le (lt',le')
198
coll_rec (arcv::lt) le ((can g (arcv.lt@arcv.le))@lt',le')
200
if (List.memq arcw lt) or (List.memq arcw le) then
201
coll_rec lt le ([],le')
203
coll_rec lt (arcw::le) (can g arcw.lt, (can g arcw.le)@le')
205
coll_rec [] [] ([],[arcu])
207
(* reprleq : canonical_arc -> canonical_arc list *)
208
(* All canonical arcv such that arcu<=arcv with arcv#arcu *)
210
let rec searchrec w = function
213
let arcv = repr g v in
214
if List.memq arcv w || arcu==arcv then
217
searchrec (arcv :: w) vl
222
(* between : universe_level -> canonical_arc -> canonical_arc list *)
223
(* between u v = {w|u<=w<=v, w canonical} *)
224
(* between is the most costly operation *)
226
let between g u arcv =
227
(* good are all w | u <= w <= v *)
228
(* bad are all w | u <= w ~<= v *)
229
(* find good and bad nodes in {w | u <= w} *)
230
(* explore b u = (b or "u is good") *)
231
let rec explore ((good, bad, b) as input) arcu =
232
if List.memq arcu good then
233
(good, bad, true) (* b or true *)
234
else if List.memq arcu bad then
235
input (* (good, bad, b or false) *)
237
let leq = reprleq g arcu in
238
(* is some universe >= u good ? *)
239
let good, bad, b_leq =
240
List.fold_left explore (good, bad, false) leq
243
arcu::good, bad, true (* b or true *)
245
good, arcu::bad, b (* b or false *)
247
let good,_,_ = explore ([arcv],[],false) (repr g u) in
250
(* We assume compare(u,v) = LE with v canonical (see compare below).
251
In this case List.hd(between g u v) = repr u
252
Otherwise, between g u v = []
256
type order = EQ | LT | LE | NLE
258
(* compare : universe_level -> universe_level -> order *)
261
and arcv = repr g v in
265
let (lt,leq) = collect g arcu in
266
if List.memq arcv lt then
268
else if List.memq arcv leq then
273
(* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
274
compare(u,v) = LT or LE => compare(v,u) = NLE
275
compare(u,v) = NLE => compare(v,u) = NLE or LE or LT
277
Adding u>=v is consistent iff compare(v,u) # LT
278
and then it is redundant iff compare(u,v) # NLE
279
Adding u>v is consistent iff compare(v,u) = NLE
280
and then it is redundant iff compare(u,v) = LT *)
282
let compare_eq g u v =
283
let g = declare_univ u g in
284
let g = declare_univ v g in
288
type check_function = universes -> universe -> universe -> bool
290
let incl_list cmp l1 l2 =
291
List.for_all (fun x1 -> List.exists (fun x2 -> cmp x1 x2) l2) l1
293
let compare_list cmp l1 l2 =
294
incl_list cmp l1 l2 && incl_list cmp l2 l1
296
let rec check_eq g u v =
298
| Atom ul, Atom vl -> compare_eq g ul vl
299
| Max(ule,ult), Max(vle,vlt) ->
300
(* TODO: remove elements of lt in le! *)
301
compare_list (compare_eq g) ule vle &&
302
compare_list (compare_eq g) ult vlt
303
| _ -> anomaly "check_eq" (* not complete! (Atom(u) = Max([u],[]) *)
308
let compare_greater g strict u v =
309
let g = declare_univ u g in
310
let g = declare_univ v g in
311
if not strict && compare_eq g v Set then true else
312
match compare g v u with
313
| (EQ|LE) -> not strict
317
let compare_greater g strict u v =
318
let b = compare_greater g strict u v in
319
ppnl(str (if b then if strict then ">" else ">=" else "NOT >="));
322
let rec check_greater g strict u v =
324
| Atom ul, Atom vl -> compare_greater g strict ul vl
325
| Atom ul, Max(le,lt) ->
326
List.for_all (fun vl -> compare_greater g strict ul vl) le &&
327
List.for_all (fun vl -> compare_greater g true ul vl) lt
328
| _ -> anomaly "check_greater"
330
let check_geq g = check_greater g false
332
(* setlt : universe_level -> universe_level -> unit *)
335
let arcu = repr g u in
336
enter_arc {arcu with lt=v::arcu.lt} g
338
(* checks that non-redundant *)
339
let setlt_if g u v = match compare g u v with
343
(* setleq : universe_level -> universe_level -> unit *)
346
let arcu = repr g u in
347
enter_arc {arcu with le=v::arcu.le} g
350
(* checks that non-redundant *)
351
let setleq_if g u v = match compare g u v with
352
| NLE -> setleq g u v
355
(* merge : universe_level -> universe_level -> unit *)
356
(* we assume compare(u,v) = LE *)
357
(* merge u v forces u ~ v with repr u as canonical repr *)
359
match between g u (repr g v) with
360
| arcu::v -> (* arcu is chosen as canonical and all others (v) are *)
361
(* redirected to it *)
362
let redirect (g,w,w') arcv =
363
let g' = enter_equiv_arc arcv.univ arcu.univ g in
364
(g',list_unionq arcv.lt w,arcv.le@w')
366
let (g',w,w') = List.fold_left redirect (g,[],[]) v in
367
let g'' = List.fold_left (fun g -> setlt_if g arcu.univ) g' w in
368
let g''' = List.fold_left (fun g -> setleq_if g arcu.univ) g'' w' in
370
| [] -> anomaly "Univ.between"
372
(* merge_disc : universe_level -> universe_level -> unit *)
373
(* we assume compare(u,v) = compare(v,u) = NLE *)
374
(* merge_disc u v forces u ~ v with repr u as canonical repr *)
375
let merge_disc g u v =
376
let arcu = repr g u in
377
let arcv = repr g v in
378
let g' = enter_equiv_arc arcv.univ arcu.univ g in
379
let g'' = List.fold_left (fun g -> setlt_if g arcu.univ) g' arcv.lt in
380
let g''' = List.fold_left (fun g -> setleq_if g arcu.univ) g'' arcv.le in
383
(* Universe inconsistency: error raised when trying to enforce a relation
384
that would create a cycle in the graph of universes. *)
386
type order_request = Lt | Le | Eq
388
exception UniverseInconsistency of order_request * universe * universe
390
let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v))
392
(* enforce_univ_leq : universe_level -> universe_level -> unit *)
393
(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
394
let enforce_univ_leq u v g =
395
let g = declare_univ u g in
396
let g = declare_univ v g in
397
match compare g u v with
399
(match compare g v u with
400
| LT -> error_inconsistency Le u v
402
| NLE -> setleq g u v
403
| EQ -> anomaly "Univ.compare")
406
(* enforc_univ_eq : universe_level -> universe_level -> unit *)
407
(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
408
let enforce_univ_eq u v g =
409
let g = declare_univ u g in
410
let g = declare_univ v g in
411
match compare g u v with
413
| LT -> error_inconsistency Eq u v
416
(match compare g v u with
417
| LT -> error_inconsistency Eq u v
419
| NLE -> merge_disc g u v
420
| EQ -> anomaly "Univ.compare")
422
(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
423
let enforce_univ_lt u v g =
424
let g = declare_univ u g in
425
let g = declare_univ v g in
426
match compare g u v with
429
| EQ -> error_inconsistency Lt u v
431
(match compare g v u with
433
| _ -> error_inconsistency Lt u v)
436
let enforce_univ_relation g = function
437
| Equiv (u,v) -> enforce_univ_eq u v g
438
| Canonical {univ=u; lt=lt; le=le} ->
439
let g' = List.fold_right (enforce_univ_lt u) lt g in
440
List.fold_right (enforce_univ_leq u) le g'
443
(* Merging 2 universe graphs *)
445
let merge_universes sp u1 u2 =
446
UniverseMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2
450
(* Constraints and sets of consrtaints. *)
452
type constraint_type = Lt | Leq | Eq
454
type univ_constraint = universe_level * constraint_type * universe_level
456
let enforce_constraint cst g =
458
| (u,Lt,v) -> enforce_univ_lt u v g
459
| (u,Leq,v) -> enforce_univ_leq u v g
460
| (u,Eq,v) -> enforce_univ_eq u v g
463
module Constraint = Set.Make(
465
type t = univ_constraint
466
let compare = Pervasives.compare
469
type constraints = Constraint.t
471
type constraint_function =
472
universe -> universe -> constraints -> constraints
474
let constraint_add_leq v u c =
475
if v = Set then c else Constraint.add (v,Leq,u) c
477
let enforce_geq u v c =
479
| Atom u, Atom v -> constraint_add_leq v u c
480
| Atom u, Max (gel,gtl) ->
481
let d = List.fold_right (fun v -> constraint_add_leq v u) gel c in
482
List.fold_right (fun v -> Constraint.add (v,Lt,u)) gtl d
483
| _ -> anomaly "A universe bound can only be a variable"
485
let enforce_eq u v c =
487
| Atom u, Atom v -> Constraint.add (u,Eq,v) c
488
| _ -> anomaly "A universe comparison can only happen between variables"
490
let merge_constraints c g =
491
Constraint.fold enforce_constraint c g
493
(**********************************************************************)
494
(* Tools for sort-polymorphic inductive types *)
496
(* Temporary inductive type levels *)
499
let n = ref 0 in fun () -> incr n; Level (Names.make_dirpath [],!n)
501
let fresh_local_univ () = Atom (fresh_level ())
503
(* Miscellaneous functions to remove or test local univ assumed to
504
occur only in the le constraints *)
506
let make_max = function
508
| (le,lt) -> Max (le,lt)
510
let remove_large_constraint u = function
511
| Atom u' as x -> if u = u' then Max ([],[]) else x
512
| Max (le,lt) -> make_max (list_remove u le,lt)
514
let is_direct_constraint u = function
516
| Max (le,lt) -> List.mem u le
519
Solve a system of universe constraint of the form
521
u_s11, ..., u_s1p1, w1 <= u1
523
u_sn1, ..., u_snpn, wn <= un
527
- the ui (1 <= i <= n) are universe variables,
528
- the sjk select subsets of the ui for each equations,
529
- the wi are arbitrary complex universes that do not mention the ui.
532
let is_direct_sort_constraint s v = match s with
533
| Some u -> is_direct_constraint u v
536
let solve_constraints_system levels level_bounds =
538
Array.map (Option.map (function Atom u -> u | _ -> anomaly "expects Atom"))
540
let v = Array.copy level_bounds in
541
let nind = Array.length v in
544
if i<>j & is_direct_sort_constraint levels.(j) v.(i) then
545
v.(i) <- sup v.(i) level_bounds.(j)
548
match levels.(j) with
549
| Some u -> v.(i) <- remove_large_constraint u v.(i)
555
let subst_large_constraint u u' v =
558
if is_direct_constraint u v then sup u' (remove_large_constraint u v)
561
anomaly "expect a universe level"
563
let subst_large_constraints =
564
List.fold_right (fun (u,u') -> subst_large_constraint u u')
566
let no_upper_constraints u cst =
568
| Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst
569
| Max _ -> anomaly "no_upper_constraints"
571
(* Pretty-printing *)
573
let num_universes g =
574
UniverseMap.fold (fun _ _ -> succ) g 0
577
let reln_len = function
579
| Canonical {lt=lt;le=le} -> List.length lt + List.length le
581
UniverseMap.fold (fun _ a n -> n + (reln_len a)) g 0
583
let pr_arc = function
584
| Canonical {univ=u; lt=[]; le=[]} ->
586
| Canonical {univ=u; lt=lt; le=le} ->
587
pr_uni_level u ++ str " " ++
589
(prlist_with_sep pr_spc (fun v -> str "< " ++ pr_uni_level v) lt ++
590
(if lt <> [] & le <> [] then spc () else mt()) ++
591
prlist_with_sep pr_spc (fun v -> str "<= " ++ pr_uni_level v) le) ++
594
pr_uni_level u ++ str " = " ++ pr_uni_level v ++ fnl ()
597
let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in
598
prlist (function (_,a) -> pr_arc a) graph
600
let pr_constraints c =
601
Constraint.fold (fun (u1,op,u2) pp_std ->
602
let op_str = match op with
606
in pp_std ++ pr_uni_level u1 ++ str op_str ++
607
pr_uni_level u2 ++ fnl () ) c (str "")
609
(* Dumping constrains to a file *)
611
let dump_universes output g =
612
let dump_arc _ = function
613
| Canonical {univ=u; lt=lt; le=le} ->
614
let u_str = string_of_univ_level u in
617
Printf.fprintf output "%s < %s ;\n" u_str
618
(string_of_univ_level v))
622
Printf.fprintf output "%s <= %s ;\n" u_str
623
(string_of_univ_level v))
626
Printf.fprintf output "%s = %s ;\n"
627
(string_of_univ_level u) (string_of_univ_level v)
629
UniverseMap.iter dump_arc g
637
type u = Names.dir_path -> Names.dir_path
638
let hash_aux hdir = function
640
| Level (d,n) -> Level (hdir d,n)
641
let hash_sub hdir = function
642
| Atom u -> Atom (hash_aux hdir u)
644
Max (List.map (hash_aux hdir) gel, List.map (hash_aux hdir) gtl)
647
| Atom u, Atom v -> u == v
648
| Max (gel,gtl), Max (gel',gtl') ->
649
(list_for_all2eq (==) gel gel') &&
650
(list_for_all2eq (==) gtl gtl')
652
let hash = Hashtbl.hash
656
let _,_,hdir,_,_,_ = Names.hcons_names() in
657
Hashcons.simple_hcons Huniv.f hdir u
added
removed
kernel/univ.ml
