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
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 Sorts
open Util
open Pp
open Constr
open Univ
let enforce_univ_constraint (u,d,v) =
match d with
| Eq -> enforce_eq u v
| Le -> enforce_leq u v
| Lt -> enforce_leq (super u) v
let subst_univs_level fn l =
try Some (fn l)
with Not_found -> None
let subst_univs_constraint fn (u,d,v as c) cstrs =
let u' = subst_univs_level fn u in
let v' = subst_univs_level fn v in
match u', v' with
| None, None -> Constraint.add c cstrs
| Some u, None -> enforce_univ_constraint (u,d,Universe.make v) cstrs
| None, Some v -> enforce_univ_constraint (Universe.make u,d,v) cstrs
| Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
let subst_univs_constraints subst csts =
Constraint.fold
(fun c cstrs -> subst_univs_constraint subst c cstrs)
csts Constraint.empty
let level_subst_of f =
fun l ->
try let u = f l in
match Universe.level u with
| None -> l
| Some l -> l
with Not_found -> l
let subst_univs_fn_constr f c =
let changed = ref false in
let fu = Univ.subst_univs_universe f in
let fi = Univ.Instance.subst_fn (level_subst_of f) in
let rec aux t =
match kind t with
| Sort (Sorts.Type u) ->
let u' = fu u in
if u' == u then t else
(changed := true; mkSort (Sorts.sort_of_univ u'))
| Const (c, u) ->
let u' = fi u in
if u' == u then t
else (changed := true; mkConstU (c, u'))
| Ind (i, u) ->
let u' = fi u in
if u' == u then t
else (changed := true; mkIndU (i, u'))
| Construct (c, u) ->
let u' = fi u in
if u' == u then t
else (changed := true; mkConstructU (c, u'))
| _ -> map aux t
in
let c' = aux c in
if !changed then c' else c
let subst_univs_constr subst c =
if Univ.is_empty_subst subst then c
else
let f = Univ.make_subst subst in
subst_univs_fn_constr f c
let subst_univs_constr =
if Flags.profile then
let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
CProfile.profile2 subst_univs_constr_key subst_univs_constr
else subst_univs_constr
let normalize_univ_variable ~find =
let rec aux cur =
let b = find cur in
let b' = subst_univs_universe aux b in
if Universe.equal b' b then b
else b'
in aux
let normalize_univ_variable_opt_subst ectx =
let find l =
match Univ.LMap.find l ectx with
| Some b -> b
| None -> raise Not_found
in
normalize_univ_variable ~find
let normalize_univ_variable_subst subst =
let find l = Univ.LMap.find l subst in
normalize_univ_variable ~find
let normalize_universe_opt_subst subst =
let normlevel = normalize_univ_variable_opt_subst subst in
subst_univs_universe normlevel
let normalize_universe_subst subst =
let normlevel = normalize_univ_variable_subst subst in
subst_univs_universe normlevel
let normalize_opt_subst ctx =
let normalize = normalize_universe_opt_subst ctx in
Univ.LMap.mapi (fun u -> function
| None -> None
| Some v -> Some (normalize v)) ctx
type universe_opt_subst = Universe.t option universe_map
let subst_univs_fn_puniverses f (c, u as cu) =
let u' = Instance.subst_fn f u in
if u' == u then cu else (c, u')
let nf_evars_and_universes_opt_subst f subst =
let subst = normalize_univ_variable_opt_subst subst in
let lsubst = level_subst_of subst in
let rec aux c =
match kind c with
| Evar (evk, args) ->
let args = Array.map aux args in
(match try f (evk, args) with Not_found -> None with
| None -> mkEvar (evk, args)
| Some c -> aux c)
| Const pu ->
let pu' = subst_univs_fn_puniverses lsubst pu in
if pu' == pu then c else mkConstU pu'
| Ind pu ->
let pu' = subst_univs_fn_puniverses lsubst pu in
if pu' == pu then c else mkIndU pu'
| Construct pu ->
let pu' = subst_univs_fn_puniverses lsubst pu in
if pu' == pu then c else mkConstructU pu'
| Sort (Type u) ->
let u' = Univ.subst_univs_universe subst u in
if u' == u then c else mkSort (sort_of_univ u')
| _ -> Constr.map aux c
in aux
let make_opt_subst s =
fun x ->
(match Univ.LMap.find x s with
| Some u -> u
| None -> raise Not_found)
let subst_opt_univs_constr s =
let f = make_opt_subst s in
subst_univs_fn_constr f
let normalize_univ_variables ctx =
let ctx = normalize_opt_subst ctx in
let undef, def, subst =
Univ.LMap.fold (fun u v (undef, def, subst) ->
match v with
| None -> (Univ.LSet.add u undef, def, subst)
| Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst))
ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty)
in ctx, undef, def, subst
let pr_universe_body = function
| None -> mt ()
| Some v -> str" := " ++ Univ.Universe.pr v
let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
|
