aboutsummaryrefslogtreecommitdiff
path: root/engine/eConstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.ml')
-rw-r--r--engine/eConstr.ml72
1 files changed, 36 insertions, 36 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index d30cb74d7a..6810626ad3 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -285,7 +285,7 @@ let map sigma f c = match kind sigma c with
else mkLetIn (na, b', t', k')
| App (b,l) ->
let b' = f b in
- let l' = Array.smartmap f l in
+ let l' = Array.Smart.map f l in
if b'==b && l'==l then c
else mkApp (b', l')
| Proj (p,t) ->
@@ -293,23 +293,23 @@ let map sigma f c = match kind sigma c with
if t' == t then c
else mkProj (p, t')
| Evar (e,l) ->
- let l' = Array.smartmap f l in
+ let l' = Array.Smart.map f l in
if l'==l then c
else mkEvar (e, l')
| Case (ci,p,b,bl) ->
let b' = f b in
let p' = f p in
- let bl' = Array.smartmap f bl in
+ let bl' = Array.Smart.map f bl in
if b'==b && p'==p && bl'==bl then c
else mkCase (ci, p', b', bl')
| Fix (ln,(lna,tl,bl)) ->
- let tl' = Array.smartmap f tl in
- let bl' = Array.smartmap f bl in
+ let tl' = Array.Smart.map f tl in
+ let bl' = Array.Smart.map f bl in
if tl'==tl && bl'==bl then c
else mkFix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
- let tl' = Array.smartmap f tl in
- let bl' = Array.smartmap f bl in
+ let tl' = Array.Smart.map f tl in
+ let bl' = Array.Smart.map f bl in
if tl'==tl && bl'==bl then c
else mkCoFix (ln,(lna,tl',bl'))
@@ -339,7 +339,7 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with
else mkLetIn (na, b', t', c')
| App (c, al) ->
let c' = f l c in
- let al' = CArray.Fun1.smartmap f l al in
+ let al' = Array.Fun1.Smart.map f l al in
if c' == c && al' == al then c0
else mkApp (c', al')
| Proj (p, t) ->
@@ -347,25 +347,25 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with
if t' == t then c0
else mkProj (p, t')
| Evar (e, al) ->
- let al' = CArray.Fun1.smartmap f l al in
+ let al' = Array.Fun1.Smart.map f l al in
if al' == al then c0
else mkEvar (e, al')
| Case (ci, p, c, bl) ->
let p' = f l p in
let c' = f l c in
- let bl' = CArray.Fun1.smartmap f l bl in
+ let bl' = Array.Fun1.Smart.map f l bl in
if p' == p && c' == c && bl' == bl then c0
else mkCase (ci, p', c', bl')
| Fix (ln, (lna, tl, bl)) ->
- let tl' = CArray.Fun1.smartmap f l tl in
+ let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
- let bl' = CArray.Fun1.smartmap f l' bl in
+ let bl' = Array.Fun1.Smart.map f l' bl in
if tl' == tl && bl' == bl then c0
else mkFix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
- let tl' = CArray.Fun1.smartmap f l tl in
+ let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
- let bl' = CArray.Fun1.smartmap f l' bl in
+ let bl' = Array.Fun1.Smart.map f l' bl in
mkCoFix (ln,(lna,tl',bl'))
let iter sigma f c = match kind sigma c with
@@ -391,9 +391,9 @@ let iter_with_full_binders sigma g f n c =
| Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
| Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
| LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
- | App (c,l) -> f n c; CArray.Fun1.iter f n l
- | Evar (_,l) -> CArray.Fun1.iter f n l
- | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+ | App (c,l) -> f n c; Array.Fun1.iter f n l
+ | Evar (_,l) -> Array.Fun1.iter f n l
+ | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
| Proj (p,c) -> f n c
| Fix (_,(lna,tl,bl)) ->
Array.iter (f n) tl;
@@ -446,28 +446,28 @@ let compare_constr sigma cmp c1 c2 =
compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
- let open Universes in
+ let open UnivProblem in
if not nargs_ok then enforce_eq_instances_univs false u u' cstrs
else
CArray.fold_left3
(fun cstrs v u u' ->
let open Univ.Variance in
match v with
- | Irrelevant -> Constraints.add (UWeak (u,u')) cstrs
+ | Irrelevant -> Set.add (UWeak (u,u')) cstrs
| Covariant ->
let u = Univ.Universe.make u in
let u' = Univ.Universe.make u' in
(match cv_pb with
- | Reduction.CONV -> Constraints.add (UEq (u,u')) cstrs
- | Reduction.CUMUL -> Constraints.add (ULe (u,u')) cstrs)
+ | Reduction.CONV -> Set.add (UEq (u,u')) cstrs
+ | Reduction.CUMUL -> Set.add (ULe (u,u')) cstrs)
| Invariant ->
let u = Univ.Universe.make u in
let u' = Univ.Universe.make u' in
- Constraints.add (UEq (u,u')) cstrs)
+ Set.add (UEq (u,u')) cstrs)
cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
- let open Universes in
+ let open UnivProblem in
match mind.Declarations.mind_universes with
| Declarations.Monomorphic_ind _ ->
assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
@@ -480,7 +480,7 @@ let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
- let open Universes in
+ let open UnivProblem in
match mind.Declarations.mind_universes with
| Declarations.Monomorphic_ind _ ->
cstrs
@@ -491,7 +491,7 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
if not (Int.equal num_cnstr_args nargs)
then enforce_eq_instances_univs false u1 u2 cstrs
else
- Array.fold_left2 (fun cstrs u1 u2 -> Universes.(Constraints.add (UWeak (u1,u2)) cstrs))
+ Array.fold_left2 (fun cstrs u1 u2 -> UnivProblem.(Set.add (UWeak (u1,u2)) cstrs))
cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2)
let eq_universes env sigma cstrs cv_pb ref nargs l l' =
@@ -499,8 +499,8 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' =
else
let l = Evd.normalize_universe_instance sigma l
and l' = Evd.normalize_universe_instance sigma l' in
- let open Universes in
let open GlobRef in
+ let open UnivProblem in
match ref with
| VarRef _ -> assert false (* variables don't have instances *)
| ConstRef _ ->
@@ -515,11 +515,11 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' =
true
let test_constr_universes env sigma leq m n =
- let open Universes in
+ let open UnivProblem in
let kind c = kind_upto sigma c in
- if m == n then Some Constraints.empty
+ if m == n then Some Set.empty
else
- let cstrs = ref Constraints.empty in
+ let cstrs = ref Set.empty in
let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in
let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l'
and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in
@@ -527,7 +527,7 @@ let test_constr_universes env sigma leq m n =
let s1 = ESorts.kind sigma (ESorts.make s1) in
let s2 = ESorts.kind sigma (ESorts.make s2) in
if Sorts.equal s1 s2 then true
- else (cstrs := Constraints.add
+ else (cstrs := Set.add
(UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
true)
in
@@ -536,7 +536,7 @@ let test_constr_universes env sigma leq m n =
let s2 = ESorts.kind sigma (ESorts.make s2) in
if Sorts.equal s1 s2 then true
else
- (cstrs := Constraints.add
+ (cstrs := Set.add
(ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
true)
in
@@ -574,15 +574,15 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
| _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n
let eq_constr_universes_proj env sigma m n =
- let open Universes in
- if m == n then Some Constraints.empty
+ let open UnivProblem in
+ if m == n then Some Set.empty
else
- let cstrs = ref Constraints.empty in
+ let cstrs = ref Set.empty in
let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in
let eq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
- (cstrs := Constraints.add
+ (cstrs := Set.add
(UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs;
true)
in
@@ -783,7 +783,7 @@ let of_existential : Constr.existential -> existential =
let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
-let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
+let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_ctxt n e)
let map_rel_context_in_env f env sign =
let rec aux env acc = function
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:50:36 +0000