Skip to content

Commit c1ea948

Browse files
yannl35133yannl35133
committed
Conversion mod qgraph
1 parent 0a46fb6 commit c1ea948

File tree

13 files changed

+188
-154
lines changed

13 files changed

+188
-154
lines changed

‎checker/mod_checking.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -223,8 +223,8 @@ let rec check_mexpr env opac mse mp_mse res = match mse with
223223
| MEapply (f,mp) ->
224224
let sign, delta = check_mexpr env opac f mp_mse res in
225225
let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
226-
let state = (Environ.universes env, Conversion.checked_universes) in
227-
let _ : UGraph.t = Subtyping.check_subtypes state env mp (MPbound farg_id) farg_b in
226+
let state = ((Environ.qualities env, Environ.universes env), Conversion.checked_universes) in
227+
let _ : QGraph.t * UGraph.t = Subtyping.check_subtypes state env mp (MPbound farg_id) farg_b in
228228
let subst = Mod_subst.map_mbid farg_id mp (Mod_subst.empty_delta_resolver mp) in
229229
Modops.subst_signature subst mp_mse fbody_b, Mod_subst.subst_codom_delta_resolver subst delta
230230
| MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation")
@@ -259,9 +259,9 @@ let rec check_module env opac mp mb opacify =
259259
| Some (sign,delta) ->
260260
let mtb1 = mk_mtb sign delta
261261
and mtb2 = mk_mtb (mod_type mb) delta_mb in
262-
let state = (Environ.universes env, Conversion.checked_universes) in
262+
let state = ((Environ.qualities env, Environ.universes env), Conversion.checked_universes) in
263263
let env = Modops.add_module mp (module_body_of_type mtb1) env in
264-
let _ : UGraph.t = Subtyping.check_subtypes state env mp mp mtb2 in
264+
let _ : QGraph.t * UGraph.t = Subtyping.check_subtypes state env mp mp mtb2 in
265265
()
266266
in
267267
opac

‎engine/univSubst.ml‎

Lines changed: 53 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -84,50 +84,73 @@ let enforce_leq u v c =
8484
else enforce_leq (Universe.repr u) (Universe.repr v) c
8585

8686
let get_algebraic = function
87-
| Prop | SProp | QSort _ -> assert false
87+
| Prop | SProp -> assert false
8888
| Set -> Universe.type0
89-
| Type u -> u
89+
| QSort (_, u) | Type u -> u
9090

91-
let enforce_eq_sort s1 s2 cst = match s1, s2 with
91+
let is_impredicative_sort = function
92+
| Prop | SProp -> true
93+
| _ -> false
94+
(* Only used for universe level comparisons, so impredicative set is still fine *)
95+
96+
let enforce_eq_sort s1 s2 (qcsts, ucsts as cst) = match s1, s2 with
97+
| QSort (q1, u1), s2 ->
98+
let q2 = quality s2 in
99+
let qcsts = QCumulConstraints.add QCumulConstraint.(QVar q1, Eq, q2) qcsts in
100+
let ucsts = if is_impredicative_sort s2 then ucsts else enforce_eq u1 (get_algebraic s2) ucsts in
101+
(qcsts, ucsts)
102+
| s1, QSort (q2, u2) ->
103+
let q1 = quality s1 in
104+
let qcsts = QCumulConstraints.add QCumulConstraint.(q1, Eq, QVar q2) qcsts in
105+
let ucsts = if is_impredicative_sort s2 then ucsts else enforce_eq (get_algebraic s1) u2 ucsts in
106+
(qcsts, ucsts)
92107
| (SProp, SProp) | (Prop, Prop) | (Set, Set) -> cst
93-
| (((Prop | Set | Type _ | QSort _) as s1), (Prop | SProp as s2))
94-
| ((Prop | SProp as s1), ((Prop | Set | Type _ | QSort _) as s2)) ->
108+
| (((Prop | Set | Type _) as s1), (Prop | SProp as s2))
109+
| ((Prop | SProp as s1), ((Prop | Set | Type _) as s2)) ->
95110
raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
96111
| (Set | Type _), (Set | Type _) ->
97-
enforce_eq (get_algebraic s1) (get_algebraic s2) cst
98-
| QSort (q1, u1), QSort (q2, u2) ->
99-
if QVar.equal q1 q2 then enforce_eq u1 u2 cst
100-
else raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
101-
| (QSort _, (Set | Type _)) | ((Set | Type _), QSort _) ->
102-
raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
112+
let ucsts' = enforce_eq (get_algebraic s1) (get_algebraic s2) ucsts in
113+
if ucsts == ucsts' then cst else (qcsts, ucsts')
103114

104-
let enforce_leq_sort s1 s2 cst = match s1, s2 with
115+
let enforce_leq_sort s1 s2 (qcsts, ucsts as cst) = match s1, s2 with
116+
| QSort (q1, u1), s2 ->
117+
let q2 = quality s2 in
118+
let qcsts = QCumulConstraints.add QCumulConstraint.(QVar q1, Leq, q2) qcsts in
119+
let ucsts = if is_impredicative_sort s2 then ucsts else enforce_eq u1 (get_algebraic s2) ucsts in
120+
(qcsts, ucsts)
121+
| s1, QSort (q2, u2) ->
122+
let q1 = quality s1 in
123+
let qcsts = QCumulConstraints.add QCumulConstraint.(q1, Leq, QVar q2) qcsts in
124+
let ucsts = if is_impredicative_sort s2 then ucsts else enforce_eq (get_algebraic s1) u2 ucsts in
125+
(qcsts, ucsts)
105126
| (SProp, SProp) | (Prop, Prop) | (Set, Set) -> cst
106127
| (Prop, (Set | Type _)) -> cst
107-
| (((Prop | Set | Type _ | QSort _) as s1), (Prop | SProp as s2))
108-
| ((SProp as s1), ((Prop | Set | Type _ | QSort _) as s2)) ->
128+
| (((Prop | Set | Type _) as s1), (Prop | SProp as s2))
129+
| ((SProp as s1), ((Prop | Set | Type _) as s2)) ->
109130
raise (UGraph.UniverseInconsistency (None, (Le, s1, s2, None)))
110131
| (Set | Type _), (Set | Type _) ->
111-
enforce_leq (get_algebraic s1) (get_algebraic s2) cst
112-
| QSort (q1, u1), QSort (q2, u2) ->
113-
if QVar.equal q1 q2 then enforce_leq u1 u2 cst
114-
else raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
115-
| (QSort _, (Set | Type _)) | ((Prop | Set | Type _), QSort _) ->
116-
raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
132+
let ucsts' = enforce_leq (get_algebraic s1) (get_algebraic s2) ucsts in
133+
if ucsts == ucsts' then cst else (qcsts, ucsts')
117134

118135
let enforce_leq_alg_sort s1 s2 g = match s1, s2 with
119-
| (SProp, SProp) | (Prop, Prop) | (Set, Set) -> Constraints.empty, g
120-
| (Prop, (Set | Type _)) -> Constraints.empty, g
121-
| (((Prop | Set | Type _ | QSort _) as s1), (Prop | SProp as s2))
122-
| ((SProp as s1), ((Prop | Set | Type _ | QSort _) as s2)) ->
136+
| QSort (q1, u1), s2 ->
137+
let q2 = quality s2 in
138+
let qcsts = QCumulConstraints.singleton QCumulConstraint.(QVar q1, Leq, q2) in
139+
let ucsts, g = if is_impredicative_sort s2 then Constraints.empty, g else UGraph.enforce_leq_alg u1 (get_algebraic s2) g in
140+
(qcsts, ucsts), g
141+
| s1, QSort (q2, u2) ->
142+
let q1 = quality s1 in
143+
let qcsts = QCumulConstraints.singleton QCumulConstraint.(q1, Leq, QVar q2) in
144+
let ucsts, g = if is_impredicative_sort s2 then Constraints.empty, g else UGraph.enforce_leq_alg (get_algebraic s1) u2 g in
145+
(qcsts, ucsts), g
146+
| (SProp, SProp) | (Prop, Prop) | (Set, Set) -> QUConstraints.empty, g
147+
| (Prop, (Set | Type _)) -> QUConstraints.empty, g
148+
| (((Prop | Set | Type _) as s1), (Prop | SProp as s2))
149+
| ((SProp as s1), ((Prop | Set | Type _) as s2)) ->
123150
raise (UGraph.UniverseInconsistency (None, (Le, s1, s2, None)))
124151
| (Set | Type _), (Set | Type _) ->
125-
UGraph.enforce_leq_alg (get_algebraic s1) (get_algebraic s2) g
126-
| QSort (q1, u1), QSort (q2, u2) ->
127-
if QVar.equal q1 q2 then UGraph.enforce_leq_alg u1 u2 g
128-
else raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
129-
| (QSort _, (Set | Type _)) | ((Prop | Set | Type _), QSort _) ->
130-
raise (UGraph.UniverseInconsistency (None, (Eq, s1, s2, None)))
152+
let ucsts, g = UGraph.enforce_leq_alg (get_algebraic s1) (get_algebraic s2) g in
153+
(QCumulConstraints.empty, ucsts), g
131154

132155
let enforce_univ_constraint (u,d,v) =
133156
match d with

‎engine/univSubst.mli‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -50,8 +50,8 @@ val pr_universe_subst : (Level.t -> Pp.t) -> universe_subst -> Pp.t
5050
val enforce_eq : Universe.t constraint_function
5151
val enforce_leq : Universe.t constraint_function
5252

53-
val enforce_eq_sort : Sorts.t -> Sorts.t -> Univ.Constraints.t -> Univ.Constraints.t
54-
val enforce_leq_sort : Sorts.t -> Sorts.t -> Univ.Constraints.t -> Univ.Constraints.t
53+
val enforce_eq_sort : Sorts.t -> Sorts.t -> Sorts.QUConstraints.t -> Sorts.QUConstraints.t
54+
val enforce_leq_sort : Sorts.t -> Sorts.t -> Sorts.QUConstraints.t -> Sorts.QUConstraints.t
5555

5656
(** Picks an arbitrary set of constraints sufficient to ensure [u <= v]. *)
57-
val enforce_leq_alg_sort : Sorts.t -> Sorts.t -> UGraph.t -> Univ.Constraints.t * UGraph.t
57+
val enforce_leq_alg_sort : Sorts.t -> Sorts.t -> UGraph.t -> Sorts.QUConstraints.t * UGraph.t

‎kernel/conversion.ml‎

Lines changed: 45 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -149,28 +149,28 @@ type conv_pb =
149149
| CUMUL
150150

151151
type ('a, 'err) universe_compare = {
152-
compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;
153-
compare_instances: env -> flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
154-
compare_cumul_instances : env -> conv_pb -> UVars.Variance.t array ->
152+
compare_sorts : conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;
153+
compare_instances: flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
154+
compare_cumul_instances : conv_pb -> UVars.Variance.t array ->
155155
UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
156156
}
157157

158158
type ('a, 'err) universe_state = 'a * ('a, 'err) universe_compare
159159

160160
type ('a, 'err) generic_conversion_function = ('a, 'err) universe_state -> constr -> constr -> ('a, 'err option) result
161161

162-
let sort_cmp_universes env pb s0 s1 (u, check) =
163-
(check.compare_sorts env pb s0 s1 u, check)
162+
let sort_cmp_universes pb s0 s1 (u, check) =
163+
(check.compare_sorts pb s0 s1 u, check)
164164

165165
(* [flex] should be true for constants, false for inductive types and
166166
constructors. *)
167-
let convert_instances env ~flex u u' (s, check) =
168-
(check.compare_instances env ~flex u u' s, check)
167+
let convert_instances ~flex u u' (s, check) =
168+
(check.compare_instances ~flex u u' s, check)
169169

170170
exception MustExpand
171171

172-
let convert_instances_cumul env pb var u u' (s, check) =
173-
(check.compare_cumul_instances env pb var u u' s, check)
172+
let convert_instances_cumul pb var u u' (s, check) =
173+
(check.compare_cumul_instances pb var u u' s, check)
174174

175175
let get_cumulativity_constraints cv_pb variance u u' =
176176
match cv_pb with
@@ -209,8 +209,8 @@ let fail_check (infos : 'err conv_tab) (state, check) = match state with
209209
| Result.Error None -> raise NotConvertible
210210
| Result.Error (Some err) -> raise (NotConvertibleTrace (infos.err_ret err))
211211

212-
let convert_inductives env cv_pb ind nargs u1 u2 (s, check) =
213-
convert_inductives_gen (check.compare_instances env ~flex:false) (check.compare_cumul_instances env)
212+
let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
213+
convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
214214
cv_pb ind nargs u1 u2 s, check
215215

216216
let constructor_cumulativity_arguments (mind, ind, ctor) =
@@ -231,8 +231,8 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u
231231
let variance = Array.make (snd (UVars.Instance.length u1)) UVars.Variance.Irrelevant in
232232
cmp_cumul CONV variance u1 u2 s
233233

234-
let convert_constructors env ctor nargs u1 u2 (s, check) =
235-
convert_constructors_gen (check.compare_instances env ~flex:false) (check.compare_cumul_instances env)
234+
let convert_constructors ctor nargs u1 u2 (s, check) =
235+
convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
236236
ctor nargs u1 u2 s, check
237237

238238
let conv_table_key infos ~nargs k1 k2 cuniv =
@@ -244,7 +244,7 @@ let conv_table_key infos ~nargs k1 k2 cuniv =
244244
else
245245
let flex = evaluable_constant cst (info_env infos.cnv_inf)
246246
&& RedFlags.red_set (info_flags infos.cnv_inf) (RedFlags.fCONST cst)
247-
in fail_check infos @@ convert_instances (info_env infos.cnv_inf) ~flex u u' cuniv
247+
in fail_check infos @@ convert_instances ~flex u u' cuniv
248248
| VarKey id, VarKey id' when Id.equal id id' -> cuniv
249249
| RelKey n, RelKey n' when Int.equal n n' -> cuniv
250250
| _ -> raise NotConvertible
@@ -404,7 +404,7 @@ and eqwhnf cv_pb l2r infos (lft1, (hd1, v1) as appr1) (lft2, (hd2, v2) as appr2)
404404
if not (is_empty_stack v1 && is_empty_stack v2) then
405405
(* May happen because we convert application right to left *)
406406
raise NotConvertible;
407-
fail_check infos @@ sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
407+
fail_check infos @@ sort_cmp_universes cv_pb s1 s2 cuniv
408408
| (Meta n, Meta m) ->
409409
if Int.equal n m
410410
then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -625,12 +625,12 @@ and eqwhnf cv_pb l2r infos (lft1, (hd1, v1) as appr1) (lft2, (hd2, v2) as appr2)
625625
| (FInd (ind1,u1 as pind1), FInd (ind2,u2 as pind2)) ->
626626
if Ind.CanOrd.equal ind1 ind2 then
627627
if UVars.Instance.is_empty u1 || UVars.Instance.is_empty u2 then
628-
let cuniv = fail_check infos @@ convert_instances (info_env infos.cnv_inf) ~flex:false u1 u2 cuniv in
628+
let cuniv = fail_check infos @@ convert_instances ~flex:false u1 u2 cuniv in
629629
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
630630
else
631631
let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
632632
let nargs = same_args_size v1 v2 in
633-
match fail_check infos @@ convert_inductives (info_env infos.cnv_inf) cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
633+
match fail_check infos @@ convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
634634
| cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
635635
| exception MustExpand ->
636636
let env = info_env infos.cnv_inf in
@@ -648,11 +648,11 @@ and eqwhnf cv_pb l2r infos (lft1, (hd1, v1) as appr1) (lft2, (hd2, v2) as appr2)
648648
let v2 = append_stack args2 v2 in
649649
if Int.equal j1 j2 && Ind.CanOrd.equal ind1 ind2 then
650650
if UVars.Instance.is_empty u1 || UVars.Instance.is_empty u2 then
651-
let cuniv = fail_check infos @@ convert_instances (info_env infos.cnv_inf) ~flex:false u1 u2 cuniv in
651+
let cuniv = fail_check infos @@ convert_instances ~flex:false u1 u2 cuniv in
652652
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
653653
else
654654
let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
655-
match fail_check infos @@ convert_constructors (info_env infos.cnv_inf) (mind, snd ind1, j1) nargs u1 u2 cuniv with
655+
match fail_check infos @@ convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
656656
| cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
657657
| exception MustExpand ->
658658
let env = info_env infos.cnv_inf in
@@ -746,7 +746,7 @@ and eqwhnf cv_pb l2r infos (lft1, (hd1, v1) as appr1) (lft2, (hd2, v2) as appr2)
746746
let nargs = inductive_cumulativity_arguments ind in
747747
let u1 = CClosure.usubst_instance e1 u1 in
748748
let u2 = CClosure.usubst_instance e2 u2 in
749-
fail_check infos @@ convert_inductives (info_env infos.cnv_inf) CONV ind nargs u1 u2 cuniv
749+
fail_check infos @@ convert_inductives CONV ind nargs u1 u2 cuniv
750750
in
751751
let pms1 = mk_clos_vect e1 pms1 in
752752
let pms2 = mk_clos_vect e2 pms2 in
@@ -758,7 +758,7 @@ and eqwhnf cv_pb l2r infos (lft1, (hd1, v1) as appr1) (lft2, (hd2, v2) as appr2)
758758
| FArray (u1,t1,ty1), FArray (u2,t2,ty2) ->
759759
let len = Parray.length_int t1 in
760760
if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible;
761-
let cuniv = fail_check infos @@ convert_instances_cumul (info_env infos.cnv_inf) CONV [|UVars.Variance.Irrelevant|] u1 u2 cuniv in
761+
let cuniv = fail_check infos @@ convert_instances_cumul CONV [|UVars.Variance.Irrelevant|] u1 u2 cuniv in
762762
let el1 = el_stack lft1 v1 in
763763
let el2 = el_stack lft2 v2 in
764764
let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
@@ -834,13 +834,13 @@ and convert_stacks ?(mask = [||]) l2r infos lft1 lft2 stk1 stk2 cuniv =
834834
let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in
835835
let cu =
836836
if UVars.Instance.is_empty u1 || UVars.Instance.is_empty u2 then
837-
convert_instances (info_env infos.cnv_inf) ~flex:false u1 u2 cu
837+
convert_instances ~flex:false u1 u2 cu
838838
else
839839
let u1 = CClosure.usubst_instance e1 u1 in
840840
let u2 = CClosure.usubst_instance e2 u2 in
841841
match mind.Declarations.mind_variance with
842-
| None -> convert_instances (info_env infos.cnv_inf) ~flex:false u1 u2 cu
843-
| Some variances -> convert_instances_cumul (info_env infos.cnv_inf) CONV variances u1 u2 cu
842+
| None -> convert_instances ~flex:false u1 u2 cu
843+
| Some variances -> convert_instances_cumul CONV variances u1 u2 cu
844844
in
845845
let cu = fail_check infos cu in
846846
let pms1 = mk_clos_vect e1 pms1 in
@@ -951,30 +951,30 @@ let clos_gen_conv (type err) ~typed trans cv_pb l2r evars env graph univs t1 t2
951951
| NotConvertibleTrace _ -> assert false
952952
end ()
953953

954-
let check_eq univs elims u u' =
954+
let check_eq (elims, univs as state) u u' =
955955
if UGraph.check_eq_sort elims univs u u'
956-
then Result.Ok univs
956+
then Result.Ok state
957957
else Result.Error None
958958

959-
let check_leq univs elims u u' =
959+
let check_leq (elims, univs as state) u u' =
960960
if UGraph.check_leq_sort elims univs u u'
961-
then Result.Ok univs
961+
then Result.Ok state
962962
else Result.Error None
963963

964-
let checked_sort_cmp_universes env pb s0 s1 univs =
964+
let checked_sort_cmp_universes pb s0 s1 state =
965965
match pb with
966-
| CUMUL -> check_leq univs (Environ.qualities env) s0 s1
967-
| CONV -> check_eq univs (Environ.qualities env) s0 s1
966+
| CUMUL -> check_leq state s0 s1
967+
| CONV -> check_eq state s0 s1
968968

969-
let check_convert_instances env ~flex:_ u u' univs =
970-
if UGraph.check_eq_instances (Environ.qualities env) univs u u' then Result.Ok univs
969+
let check_convert_instances ~flex:_ u u' (elims, univs as state) =
970+
if UGraph.check_eq_instances elims univs u u' then Result.Ok state
971971
else Result.Error None
972972

973973
(* general conversion and inference functions *)
974-
let check_inductive_instances env cv_pb variance u1 u2 univs =
974+
let check_inductive_instances cv_pb variance u1 u2 (elims, univs as state) =
975975
let qcsts, ucsts = get_cumulativity_constraints cv_pb variance u1 u2 in
976-
if QGraph.check_constraints (Sorts.QCumulConstraints.to_elims qcsts) (Environ.qualities env) && UGraph.check_constraints ucsts univs
977-
then Result.Ok univs
976+
if QGraph.check_constraints (Sorts.QCumulConstraints.to_elims qcsts) elims && UGraph.check_constraints ucsts univs
977+
then Result.Ok state
978978
else Result.Error None
979979

980980
let checked_universes =
@@ -986,12 +986,12 @@ let () =
986986
let conv infos tab a b =
987987
try
988988
let box = Empty.abort in
989-
let univs = info_univs infos in
989+
let state = info_elims infos, info_univs infos in
990990
let infos = { cnv_inf = infos; cnv_typ = true; lft_tab = tab; rgt_tab = tab; err_ret = box } in
991-
let univs', _ = ccnv CONV false infos el_id el_id a b
992-
(univs, checked_universes)
991+
let state', _ = ccnv CONV false infos el_id el_id a b
992+
(state, checked_universes)
993993
in
994-
assert (univs==univs');
994+
assert (state==state');
995995
true
996996
with
997997
| NotConvertible -> false
@@ -1002,22 +1002,23 @@ let () =
10021002
let gen_conv ~typed cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=default_evar_handler env) t1 t2 =
10031003
let univs = Environ.universes env in
10041004
let elims = Environ.qualities env in
1005+
let state = elims, univs in
10051006
let b =
10061007
if cv_pb = CUMUL then leq_constr_univs elims univs t1 t2
10071008
else eq_constr_univs elims univs t1 t2
10081009
in
10091010
if b then Result.Ok ()
1010-
else match clos_gen_conv ~typed reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 with
1011-
| Result.Ok (_ : UGraph.t * (UGraph.t, Empty.t) universe_compare)-> Result.Ok ()
1011+
else match clos_gen_conv ~typed reds cv_pb l2r evars env univs (state, checked_universes) t1 t2 with
1012+
| Result.Ok (_ : 'a * ('a, Empty.t) universe_compare)-> Result.Ok ()
10121013
| Result.Error None -> Result.Error ()
10131014
| Result.Error (Some e) -> Empty.abort e
10141015

10151016
let conv = gen_conv ~typed:false CONV
10161017
let conv_leq = gen_conv ~typed:false CUMUL
10171018

1018-
let generic_conv cv_pb ~l2r reds env ?(evars=default_evar_handler env) univs t1 t2 =
1019+
let generic_conv cv_pb ~l2r reds env ?(evars=default_evar_handler env) state t1 t2 =
10191020
let graph = Environ.universes env in
1020-
match clos_gen_conv ~typed:false reds cv_pb l2r evars env graph univs t1 t2 with
1021+
match clos_gen_conv ~typed:false reds cv_pb l2r evars env graph state t1 t2 with
10211022
| Result.Ok (s, _) -> Result.Ok s
10221023
| Result.Error e -> Result.Error e
10231024

0 commit comments

Comments
 (0)