1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Univ
type t = {
subst: Universe.t option Level.Map.t;
algs : Level.Set.t;
}
let empty = {
subst = Level.Map.empty;
algs = Level.Set.empty;
}
let is_empty {subst} = Level.Map.is_empty subst
let domain {subst} = Level.Map.domain subst
let mem l {subst} = Level.Map.mem l subst
let fold f {subst} acc =
Level.Map.fold (fun l v acc -> f l ~is_defined:(Option.has_some v) acc)
subst acc
let is_algebraic l {algs} = Level.Set.mem l algs
let make_nonalgebraic_variable {subst;algs} l =
{ subst; algs = Level.Set.remove l algs }
let make_all_undefined_nonalgebraic {subst;algs=_} =
{ subst; algs = Level.Set.empty }
let fix_undefined_variables us =
Level.Map.fold (fun u v ({subst; algs} as acc) ->
match v with
| None -> { subst = Level.Map.remove u subst; algs = Level.Set.remove u algs }
| Some _ -> acc)
us.subst us
let add l ~algebraic {subst; algs} =
let subst = Level.Map.update l
(function
| None -> Some None
| Some _ -> assert false)
subst
in
let algs = if algebraic then Level.Set.add l algs else algs in
{ subst; algs }
let add_levels levels ~algebraic subst =
Level.Set.fold (fun l subst -> add l ~algebraic subst) levels subst
let define l v {subst;algs} =
(* XXX update algs? *)
let subst =
try Level.Map.modify l (fun _ old -> assert (Option.is_empty old); Some v) subst
with Not_found -> assert false
in
{ subst; algs }
let constrain_variables diff us ctx =
(* XXX update algs? *)
Level.Set.fold (fun l ((univs,cstrs),{subst;algs} as acc) ->
match Level.Map.find_opt l subst with
| None | Some None -> acc
| Some (Some u) -> match Universe.level u with
| None -> acc
| Some u ->
((Level.Set.add l univs, Constraints.add (l, Eq, u) cstrs),
{subst = Level.Map.remove l subst; algs}))
diff
(ctx,us)
let biased_union {subst=lsubst;algs=lalgs} {subst=rsubst; algs=ralgs} =
let subst =
Level.Map.union (fun _k l r ->
match l, r with
| Some _, _ -> Some l
| None, None -> Some l
| _, _ -> Some r) lsubst rsubst
in
{ subst; algs = Level.Set.union lalgs ralgs }
let normalize_univ_variable ~find =
let rec aux cur =
find cur |>
Option.map (fun b ->
let b' = UnivSubst.subst_univs_universe aux b in
if Universe.equal b' b then b
else b')
in aux
let normalize_univ_variable ectx =
let find l = Option.flatten (Univ.Level.Map.find_opt l ectx.subst) in
normalize_univ_variable ~find
let normalize_universe subst =
let normlevel = normalize_univ_variable subst in
UnivSubst.subst_univs_universe normlevel
let normalize ctx =
let normalize = normalize_universe ctx in
let subst =
Univ.Level.Map.mapi (fun u -> function
| None -> None
| Some v -> Some (normalize v)) ctx.subst
in
{subst; algs = ctx.algs}
let normalize_univ_variables ctx =
let ctx = normalize ctx in
let def, subst =
Univ.Level.Map.fold (fun u v (def, subst) ->
match v with
| None -> (def, subst)
| Some b -> (Univ.Level.Set.add u def, Univ.Level.Map.add u b subst))
ctx.subst (Univ.Level.Set.empty, Univ.Level.Map.empty)
in
let subst l = Level.Map.find_opt l subst in
ctx, def, subst
let pr prl {subst; algs} =
let open Pp in
let ppsubst = Level.Map.pr prl (function
| None -> mt()
| Some x -> str " := " ++ Universe.pr prl x)
subst
in
str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
h (Level.Set.pr prl algs) ++ fnl() ++
str"FLEXIBLE UNIVERSES:"++brk(0,1)++
h ppsubst
|
