aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/reduction.ml')
-rw-r--r--kernel/reduction.ml173
1 files changed, 93 insertions, 80 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2bf9f43a5a..41d6c05eb5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -18,7 +18,7 @@
open CErrors
open Util
open Names
-open Term
+open Constr
open Vars
open Environ
open CClosure
@@ -57,12 +57,14 @@ let compare_stack_shape stk1 stk2 =
Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
- | (_,_) -> false in
+ | [], _ :: _
+ | (Zproj _ | ZcaseT _ | Zfix _) :: _, _ -> false
+ in
compare_rec 0 stk1 stk2
type lft_constr_stack_elt =
Zlapp of (lift * fconstr) array
- | Zlproj of constant * lift
+ | Zlproj of Constant.t * lift
| Zlfix of (lift * fconstr) * lft_constr_stack
| Zlcase of case_info * lift * fconstr * fconstr array
and lft_constr_stack = lft_constr_stack_elt list
@@ -107,11 +109,11 @@ let pure_stack lfts stk =
(****************************************************************************)
let whd_betaiota env t =
- match kind_of_term t with
+ match kind t with
| (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _) -> t
| App (c, _) ->
- begin match kind_of_term c with
+ begin match kind c with
| Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t
| _ -> whd_val (create_clos_infos betaiota env) (inject t)
end
@@ -121,37 +123,46 @@ let nf_betaiota env t =
norm_val (create_clos_infos betaiota env) (inject t)
let whd_betaiotazeta env x =
- match kind_of_term x with
- | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
+ match kind x with
+ | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _) -> x
| App (c, _) ->
- begin match kind_of_term c with
+ begin match kind c with
| Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
- | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+ | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
+ | Case _ | Fix _ | CoFix _ | Proj _ ->
+ whd_val (create_clos_infos betaiotazeta env) (inject x)
end
- | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+ | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ ->
+ whd_val (create_clos_infos betaiotazeta env) (inject x)
let whd_all env t =
- match kind_of_term t with
+ match kind t with
| (Sort _|Meta _|Evar _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _) -> t
| App (c, _) ->
- begin match kind_of_term c with
+ begin match kind c with
| Ind _ | Construct _ | Evar _ | Meta _ -> t
- | _ -> whd_val (create_clos_infos all env) (inject t)
+ | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
+ | Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
+ whd_val (create_clos_infos all env) (inject t)
end
- | _ -> whd_val (create_clos_infos all env) (inject t)
+ | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ ->
+ whd_val (create_clos_infos all env) (inject t)
let whd_allnolet env t =
- match kind_of_term t with
+ match kind t with
| (Sort _|Meta _|Evar _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
| App (c, _) ->
- begin match kind_of_term c with
+ begin match kind c with
| Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
- | _ -> whd_val (create_clos_infos allnolet env) (inject t)
+ | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
+ | Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
+ whd_val (create_clos_infos allnolet env) (inject t)
end
- | _ -> whd_val (create_clos_infos allnolet env) (inject t)
+ | Rel _ | Cast _ | Case _ | Proj _ | Const _ | Var _ ->
+ whd_val (create_clos_infos allnolet env) (inject t)
(********************************************************************)
(* Conversion *)
@@ -189,7 +200,7 @@ let is_cumul = function CUMUL -> true | CONV -> false
type 'a universe_compare =
{ (* Might raise NotConvertible *)
- compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
+ compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
Univ.Instance.t -> int -> 'a -> 'a;
@@ -239,7 +250,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
| (Zlapp a1,Zlapp a2) ->
Array.fold_right2 f a1 a2 cu1
| (Zlproj (c1,l1),Zlproj (c2,l2)) ->
- if not (eq_constant c1 c2) then
+ if not (Constant.equal c1 c2) then
raise NotConvertible
else cu1
| (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
@@ -309,11 +320,11 @@ let unfold_projection infos p c =
else None
(* Conversion between [lft1]term1 and [lft2]term2 *)
-let rec ccnv env cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
- eqappr env cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
+ eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
-and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
+and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
Control.check_for_interrupt ();
(* First head reduce both terms *)
let whd = whd_stack (infos_with_reds infos betaiotazeta) in
@@ -331,20 +342,20 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
match (fterm_of hd1, fterm_of hd2) with
(* case of leaves *)
| (FAtom a1, FAtom a2) ->
- (match kind_of_term a1, kind_of_term a2 with
+ (match kind a1, kind a2 with
| (Sort s1, Sort s2) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
if Int.equal n m
- then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| _ -> raise NotConvertible)
| (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
if Evar.equal ev1 ev2 then
- let cuniv = convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv in
- convert_vect env l2r infos el1 el2
+ let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
+ convert_vect l2r infos el1 el2
(Array.map (mk_clos env1) args1)
(Array.map (mk_clos env2) args2) cuniv
else raise NotConvertible
@@ -352,14 +363,14 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* 2 index known to be bound to no constant *)
| (FRel n, FRel m) ->
if Int.equal (reloc_rel n el1) (reloc_rel m el2)
- then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try
let cuniv = conv_table_key infos fl1 fl2 cuniv in
- convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with NotConvertible | Univ.UniverseInconsistency _ ->
(* else the oracle tells which constant is to be expanded *)
let oracle = CClosure.oracle_of_infos infos in
@@ -379,7 +390,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| Some def1 -> ((lft1, (def1, v1)), appr2)
| None -> raise NotConvertible)
in
- eqappr env cv_pb l2r infos app1 app2 cuniv)
+ eqappr cv_pb l2r infos app1 app2 cuniv)
| (FProj (p1,c1), FProj (p2, c2)) ->
(* Projections: prefer unfolding to first-order unification,
@@ -387,42 +398,42 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
form *)
(match unfold_projection infos p1 c1 with
| Some (def1,s1) ->
- eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
+ eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
| None ->
match unfold_projection infos p2 c2 with
| Some (def2,s2) ->
- eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
+ eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
| None ->
if Constant.equal (Projection.constant p1) (Projection.constant p2)
&& compare_stack_shape v1 v2 then
- let u1 = ccnv env CONV l2r infos el1 el2 c1 c2 cuniv in
- convert_stacks env l2r infos lft1 lft2 v1 v2 u1
+ let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
+ convert_stacks l2r infos lft1 lft2 v1 v2 u1
else (* Two projections in WHNF: unfold *)
raise NotConvertible)
| (FProj (p1,c1), t2) ->
(match unfold_projection infos p1 c1 with
| Some (def1,s1) ->
- eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
+ eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
| None ->
(match t2 with
| FFlex fl2 ->
(match unfold_reference infos fl2 with
| Some def2 ->
- eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
+ eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
| None -> raise NotConvertible)
| _ -> raise NotConvertible))
| (t1, FProj (p2,c2)) ->
(match unfold_projection infos p2 c2 with
| Some (def2,s2) ->
- eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
+ eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
| None ->
(match t1 with
| FFlex fl1 ->
(match unfold_reference infos fl1 with
| Some def1 ->
- eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
+ eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
| None -> raise NotConvertible)
| _ -> raise NotConvertible))
@@ -434,15 +445,15 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
anomaly (Pp.str "conversion was given ill-typed terms (FLambda).");
let (_,ty1,bd1) = destFLambda mk_clos hd1 in
let (_,ty2,bd2) = destFLambda mk_clos hd2 in
- let cuniv = ccnv env CONV l2r infos el1 el2 ty1 ty2 cuniv in
- ccnv env CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
+ let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
+ ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
| (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
(* Luo's system *)
- let cuniv = ccnv env CONV l2r infos el1 el2 c1 c'1 cuniv in
- ccnv env cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
+ let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
+ ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
@@ -452,7 +463,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
anomaly (Pp.str "conversion was given unreduced term (FLambda).")
in
let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
- eqappr env CONV l2r infos
+ eqappr CONV l2r infos
(el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
| (_, FLambda _) ->
let () = match v2 with
@@ -461,34 +472,34 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
anomaly (Pp.str "conversion was given unreduced term (FLambda).")
in
let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
- eqappr env CONV l2r infos
+ eqappr CONV l2r infos
(el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
(* only one constant, defined var or defined rel *)
| (FFlex fl1, c2) ->
(match unfold_reference infos fl1 with
| Some def1 ->
- eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
+ eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
| None ->
match c2 with
| FConstruct ((ind2,j2),u2) ->
(try
let v2, v1 =
eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
- in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| _ -> raise NotConvertible)
| (c1, FFlex fl2) ->
(match unfold_reference infos fl2 with
| Some def2 ->
- eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
+ eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
| None ->
match c1 with
| FConstruct ((ind1,j1),u1) ->
(try let v1, v2 =
eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
- in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| _ -> raise NotConvertible)
@@ -497,9 +508,9 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if eq_ind ind1 ind2 then
if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
let cuniv = convert_instances ~flex:false u1 u2 cuniv in
- convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
- let mind = Environ.lookup_mind (fst ind1) env in
+ let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
let cuniv =
match mind.Declarations.mind_universes with
| Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
@@ -508,16 +519,16 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
u2 (CClosure.stack_args_size v2) cuniv
in
- convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
if Int.equal j1 j2 && eq_ind ind1 ind2 then
if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
let cuniv = convert_instances ~flex:false u1 u2 cuniv in
- convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
- let mind = Environ.lookup_mind (fst ind1) env in
+ let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
let cuniv =
match mind.Declarations.mind_universes with
| Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
@@ -527,7 +538,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
u2 (CClosure.stack_args_size v2) cuniv
in
- convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
(* Eta expansion of records *)
@@ -535,14 +546,14 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(try
let v1, v2 =
eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
- in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| (_, FConstruct ((ind2,j2),u2)) ->
(try
let v2, v1 =
eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
- in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) ->
@@ -553,11 +564,11 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let fty2 = Array.map (mk_clos e2) tys2 in
let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
- let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in
+ let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
let cuniv =
- convert_vect env l2r infos
+ convert_vect l2r infos
(el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
- convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
@@ -568,28 +579,28 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let fty2 = Array.map (mk_clos e2) tys2 in
let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
- let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in
+ let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
let cuniv =
- convert_vect env l2r infos
+ convert_vect l2r infos
(el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
- convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
(* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
| ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
| (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
- | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
+ | (FLOCKED,_) | (_,FLOCKED) ) | (FCast _, _) | (_, FCast _) -> assert false
- (* In all other cases, terms are not convertible *)
- | _ -> raise NotConvertible
+ | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
+ | FProd _ | FEvar _), _ -> raise NotConvertible
-and convert_stacks env l2r infos lft1 lft2 stk1 stk2 cuniv =
+and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
compare_stacks
- (fun (l1,t1) (l2,t2) cuniv -> ccnv env CONV l2r infos l1 l2 t1 t2 cuniv)
+ (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv)
(eq_ind)
lft1 stk1 lft2 stk2 cuniv
-and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv =
+and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
let lv1 = Array.length v1 in
let lv2 = Array.length v2 in
if Int.equal lv1 lv2
@@ -597,7 +608,7 @@ and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv =
let rec fold n cuniv =
if n >= lv1 then cuniv
else
- let cuniv = ccnv env CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
+ let cuniv = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
fold (n+1) cuniv in
fold 0 cuniv
else raise NotConvertible
@@ -605,7 +616,7 @@ and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv =
let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
let infos = create_clos_infos ~evars reds env in
- ccnv env cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
+ ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
let check_eq univs u u' =
@@ -615,6 +626,7 @@ let check_leq univs u u' =
if not (UGraph.check_leq univs u u') then raise NotConvertible
let check_sort_cmp_universes env pb s0 s1 univs =
+ let open Sorts in
match (s0,s1) with
| (Prop c1, Prop c2) when is_cumul pb ->
begin match c1, c2 with
@@ -734,6 +746,7 @@ let infer_leq (univs, cstrs as cuniv) u u' =
univs, cstrs'
let infer_cmp_universes env pb s0 s1 univs =
+ let open Sorts in
match (s0,s1) with
| (Prop c1, Prop c2) when is_cumul pb ->
begin match c1, c2 with
@@ -869,7 +882,7 @@ let warn_bytecode_compiler_failed =
(fun () -> strbrk "Bytecode compiler failed, " ++
strbrk "falling back to standard conversion")
-let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f
+let set_vm_conv (f:conv_pb -> types kernel_conversion_function) = vm_conv := f
let vm_conv cv_pb env t1 t2 =
try
!vm_conv cv_pb env t1 t2
@@ -895,9 +908,9 @@ let conv env t1 t2 =
let beta_applist c l =
let rec app subst c l =
- match kind_of_term c, l with
+ match kind c, l with
| Lambda(_,_,c), arg::l -> app (arg::subst) c l
- | _ -> applist (substl subst c, l) in
+ | _ -> Term.applist (substl subst c, l) in
app [] c l
let beta_appvect c v = beta_applist c (Array.to_list v)
@@ -905,7 +918,7 @@ let beta_appvect c v = beta_applist c (Array.to_list v)
let beta_app c a = beta_applist c [a]
(* Compatibility *)
-let betazeta_appvect = lambda_appvect_assum
+let betazeta_appvect = Term.lambda_appvect_assum
(********************************************************************)
(* Special-Purpose Reduction *)
@@ -918,7 +931,7 @@ let betazeta_appvect = lambda_appvect_assum
* error message. *)
let hnf_prod_app env t n =
- match kind_of_term (whd_all env t) with
+ match kind (whd_all env t) with
| Prod (_,_,b) -> subst1 n b
| _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.")
@@ -930,7 +943,7 @@ let hnf_prod_applist env t nl =
let dest_prod env =
let rec decrec env m c =
let t = whd_all env c in
- match kind_of_term t with
+ match kind t with
| Prod (n,a,c0) ->
let d = LocalAssum (n,a) in
decrec (push_rel d env) (Context.Rel.add d m) c0
@@ -942,7 +955,7 @@ let dest_prod env =
let dest_prod_assum env =
let rec prodec_rec env l ty =
let rty = whd_allnolet env ty in
- match kind_of_term rty with
+ match kind rty with
| Prod (x,t,c) ->
let d = LocalAssum (x,t) in
prodec_rec (push_rel d env) (Context.Rel.add d l) c
@@ -952,7 +965,7 @@ let dest_prod_assum env =
| Cast (c,_,_) -> prodec_rec env l c
| _ ->
let rty' = whd_all env rty in
- if Term.eq_constr rty' rty then l, rty
+ if Constr.equal rty' rty then l, rty
else prodec_rec env l rty'
in
prodec_rec env Context.Rel.empty
@@ -960,7 +973,7 @@ let dest_prod_assum env =
let dest_lam_assum env =
let rec lamec_rec env l ty =
let rty = whd_allnolet env ty in
- match kind_of_term rty with
+ match kind rty with
| Lambda (x,t,c) ->
let d = LocalAssum (x,t) in
lamec_rec (push_rel d env) (Context.Rel.add d l) c
@@ -976,7 +989,7 @@ exception NotArity
let dest_arity env c =
let l, c = dest_prod_assum env c in
- match kind_of_term c with
+ match kind c with
| Sort s -> l,s
| _ -> raise NotArity
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 18:37:26 +0000