aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml30
-rw-r--r--engine/eConstr.mli8
-rw-r--r--engine/evarutil.ml2
-rw-r--r--engine/evd.ml3
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/namegen.ml4
-rw-r--r--engine/termops.ml21
-rw-r--r--engine/univProblem.ml2
-rw-r--r--engine/univSubst.ml6
9 files changed, 48 insertions, 30 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 42c9359ff0..32eb63a818 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -69,7 +69,7 @@ let mkInd i = of_kind (Ind (in_punivs i))
let mkConstructU pc = of_kind (Construct pc)
let mkConstruct c = of_kind (Construct (in_punivs c))
let mkConstructUi ((ind,u),i) = of_kind (Construct ((ind,i),u))
-let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
+let mkCase (ci, c, iv, r, p) = of_kind (Case (ci, c, iv, r, p))
let mkFix f = of_kind (Fix f)
let mkCoFix f = of_kind (CoFix f)
let mkProj (p, c) = of_kind (Proj (p, c))
@@ -194,7 +194,7 @@ let destCoFix sigma c = match kind sigma c with
| _ -> raise DestKO
let destCase sigma c = match kind sigma c with
-| Case (ci, t, c, p) -> (ci, t, c, p)
+| Case (ci, t, iv, c, p) -> (ci, t, iv, c, p)
| _ -> raise DestKO
let destProj sigma c = match kind sigma c with
@@ -356,7 +356,7 @@ let iter_with_full_binders sigma g f 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; Array.Fun1.iter f n l
| Evar (_,l) -> List.iter (fun c -> f n c) l
- | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
+ | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
| Proj (p,c) -> f n c
| Fix (_,(lna,tl,bl)) ->
Array.iter (f n) tl;
@@ -380,7 +380,7 @@ let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
let eq_constr sigma c1 c2 =
let kind c = kind sigma c in
- let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+ let eq_inst _ i1 i2 = EInstance.equal sigma i1 i2 in
let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
let rec eq_constr nargs c1 c2 =
compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2
@@ -390,13 +390,13 @@ let eq_constr sigma c1 c2 =
let eq_constr_nounivs sigma c1 c2 =
let kind c = kind sigma c in
let rec eq_constr nargs c1 c2 =
- compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
+ compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
in
eq_constr 0 c1 c2
let compare_constr sigma cmp c1 c2 =
let kind c = kind sigma c in
- let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+ let eq_inst _ i1 i2 = EInstance.equal sigma i1 i2 in
let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
let cmp nargs c1 c2 = cmp c1 c2 in
compare_gen kind eq_inst eq_sorts cmp 0 c1 c2
@@ -442,22 +442,22 @@ let cmp_constructors (mind, ind, cns as spec) nargs 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' =
+let eq_universes env sigma cstrs cv_pb refargs l l' =
if EInstance.is_empty l then (assert (EInstance.is_empty l'); true)
else
let l = EInstance.kind sigma l
and l' = EInstance.kind sigma l' in
let open GlobRef in
let open UnivProblem in
- match ref with
- | VarRef _ -> assert false (* variables don't have instances *)
- | ConstRef _ ->
+ match refargs with
+ | None | Some (ConstRef _, _) ->
cstrs := enforce_eq_instances_univs true l l' !cstrs; true
- | IndRef ind ->
+ | Some (VarRef _, _) -> assert false (* variables don't have instances *)
+ | Some (IndRef ind, nargs) ->
let mind = Environ.lookup_mind (fst ind) env in
cstrs := cmp_inductives cv_pb (mind,snd ind) nargs l l' !cstrs;
true
- | ConstructRef ((mi,ind),ctor) ->
+ | Some (ConstructRef ((mi,ind),ctor), nargs) ->
let mind = Environ.lookup_mind mi env in
cstrs := cmp_constructors (mind,ind,ctor) nargs l l' !cstrs;
true
@@ -469,8 +469,8 @@ let test_constr_universes env sigma leq m n =
else
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
+ let eq_universes refargs l l' = eq_universes env sigma cstrs Reduction.CONV refargs l l'
+ and leq_universes refargs l l' = eq_universes env sigma cstrs cv_pb refargs l l' in
let eq_sorts s1 s2 =
let s1 = ESorts.kind sigma s1 in
let s2 = ESorts.kind sigma s2 in
@@ -777,5 +777,7 @@ let to_named_context =
= fun Refl x -> x
in
gen unsafe_eq
+let to_case_invert = unsafe_to_case_invert
+
let eq = unsafe_eq
end
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index aea441b90b..2bf8f69af7 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -128,7 +128,7 @@ val mkIndU : inductive * EInstance.t -> t
val mkConstruct : constructor -> t
val mkConstructU : constructor * EInstance.t -> t
val mkConstructUi : (inductive * EInstance.t) * int -> t
-val mkCase : case_info * t * t * t array -> t
+val mkCase : case_info * t * (t,EInstance.t) case_invert * t * t array -> t
val mkFix : (t, t) pfixpoint -> t
val mkCoFix : (t, t) pcofixpoint -> t
val mkArrow : t -> Sorts.relevance -> t -> t
@@ -198,7 +198,7 @@ val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
val destEvar : Evd.evar_map -> t -> t pexistential
val destInd : Evd.evar_map -> t -> inductive * EInstance.t
val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
-val destCase : Evd.evar_map -> t -> case_info * t * t * t array
+val destCase : Evd.evar_map -> t -> case_info * t * (t,EInstance.t) case_invert * t * t array
val destProj : Evd.evar_map -> t -> Projection.t * t
val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
@@ -341,6 +341,8 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, typ
val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
+val of_case_invert : (Constr.t,Univ.Instance.t) case_invert -> (t,EInstance.t) case_invert
+
(** {5 Unsafe operations} *)
module Unsafe :
@@ -365,6 +367,8 @@ sig
val to_instance : EInstance.t -> Univ.Instance.t
(** Physical identity. Does not care for normalization. *)
+ val to_case_invert : (t,EInstance.t) case_invert -> (Constr.t,Univ.Instance.t) case_invert
+
val eq : (t, Constr.t) eq
(** Use for transparent cast between types. *)
end
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index eea7e38f87..3458743c0e 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -143,7 +143,7 @@ let head_evar sigma c =
let c = EConstr.Unsafe.to_constr c in
let rec hrec c = match kind c with
| Evar (evk,_) -> evk
- | Case (_,_,c,_) -> hrec c
+ | Case (_,_,_,c,_) -> hrec c
| App (c,_) -> hrec c
| Cast (c,_,_) -> hrec c
| Proj (p, c) -> hrec c
diff --git a/engine/evd.ml b/engine/evd.ml
index f0ee8ae68f..c570f75c6b 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1398,6 +1398,9 @@ module MiniEConstr = struct
let unsafe_to_rel_decl d = d
let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
+ let unsafe_to_case_invert x = x
+ let of_case_invert x = x
+
end
(** The following functions return the set of evars immediately
diff --git a/engine/evd.mli b/engine/evd.mli
index d9b7bd76e7..679173ca72 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -732,6 +732,8 @@ module MiniEConstr : sig
(Constr.t, Constr.types) Context.Named.Declaration.pt
val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt ->
(Constr.t, Constr.types) Context.Rel.Declaration.pt
+ val of_case_invert : (constr,Univ.Instance.t) case_invert -> (econstr,EInstance.t) case_invert
+ val unsafe_to_case_invert : (econstr,EInstance.t) case_invert -> (constr,Univ.Instance.t) case_invert
val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt ->
(t, t) Context.Rel.Declaration.pt
val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt ->
diff --git a/engine/namegen.ml b/engine/namegen.ml
index c4472050f8..1cf5be10ae 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
Some (Nametab.basename_of_global (global_of_constr c))
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
- | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ | Float _ -> None
+ | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ -> None
in
hdrec c
@@ -163,7 +163,7 @@ let hdchar env sigma c =
let id = match lna.(i).binder_name with Name id -> id | _ -> assert false in
lowercase_first_char id
| Evar _ (* We could do better... *)
- | Meta _ | Case (_, _, _, _) -> "y"
+ | Meta _ | Case _ -> "y"
| Int _ -> "i"
| Float _ -> "f"
in
diff --git a/engine/termops.ml b/engine/termops.ml
index c51e753d46..f6d0807823 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -639,13 +639,14 @@ let map_constr_with_binders_left_to_right sigma g f l c =
let al' = List.map_left (f l) al in
if List.for_all2 (==) al' al then c
else mkEvar (e, al')
- | Case (ci,p,b,bl) ->
+ | Case (ci,p,iv,b,bl) ->
(* In v8 concrete syntax, predicate is after the term to match! *)
let b' = f l b in
+ let iv' = map_invert (f l) iv in
let p' = f l p in
let bl' = Array.map_left (f l) bl in
- if b' == b && p' == p && bl' == bl then c
- else mkCase (ci, p', b', bl')
+ if b' == b && p' == p && iv' == iv && bl' == bl then c
+ else mkCase (ci, p', iv', b', bl')
| Fix (ln,(lna,tl,bl as fx)) ->
let l' = fold_rec_types g fx l in
let (tl', bl') = map_left2 (f l) tl (f l') bl in
@@ -709,18 +710,20 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
| Evar (e,al) ->
let al' = List.map (f l) al in
if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
- | Case (ci,p,c,bl) when userview ->
+ | Case (ci,p,iv,c,bl) when userview ->
let p' = map_return_predicate_with_full_binders sigma g f l ci p in
+ let iv' = map_invert (f l) iv in
let c' = f l c in
let bl' = map_branches_with_full_binders sigma g f l ci bl in
- if p==p' && c==c' && bl'==bl then cstr else
- mkCase (ci, p', c', bl')
- | Case (ci,p,c,bl) ->
+ if p==p' && iv'==iv && c==c' && bl'==bl then cstr else
+ mkCase (ci, p', iv', c', bl')
+ | Case (ci,p,iv,c,bl) ->
let p' = f l p in
+ let iv' = map_invert (f l) iv in
let c' = f l c in
let bl' = Array.map (f l) bl in
- if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else
- mkCase (ci, p', c', bl')
+ if p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
+ mkCase (ci, p', iv', c', bl')
| Fix (ln,(lna,tl,bl as fx)) ->
let tl' = Array.map (f l) tl in
let l' = fold_rec_types g fx l in
diff --git a/engine/univProblem.ml b/engine/univProblem.ml
index 08ff9efa5b..8d6689933c 100644
--- a/engine/univProblem.ml
+++ b/engine/univProblem.ml
@@ -150,7 +150,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
[kind1,kind2], because [kind1] and [kind2] may be different,
typically evaluating [m] and [n] in different evar maps. *)
let cstrs = ref accu in
- let eq_universes _ _ = UGraph.check_eq_instances univs in
+ let eq_universes _ = UGraph.check_eq_instances univs in
let eq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 92211d5f3d..f06aeaf54e 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -146,7 +146,11 @@ let nf_evars_and_universes_opt_subst f subst =
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')
+ if u' == u then c else mkSort (sort_of_univ u')
+ | Case (ci,p,CaseInvert {univs;args},t,br) ->
+ let univs' = Instance.subst_fn lsubst univs in
+ if univs' == univs then Constr.map aux c
+ else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br))
| _ -> Constr.map aux c
in aux
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:30:38 +0000