aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/reduction.ml')
-rw-r--r--kernel/reduction.ml85
1 files changed, 61 insertions, 24 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4ff90dd70d..0754e9d4cc 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -138,10 +138,10 @@ let nf_betaiota env t =
let whd_betaiotazeta env x =
match kind x with
| (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
- Prod _|Lambda _|Fix _|CoFix _|Int _|Float _) -> x
+ Prod _|Lambda _|Fix _|CoFix _|Int _|Float _|Array _) -> x
| App (c, _) ->
begin match kind c with
- | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ | Float _ -> x
+ | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ | Float _ | Array _ -> x
| Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
| Case _ | Fix _ | CoFix _ | Proj _ ->
whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x)
@@ -152,10 +152,10 @@ let whd_betaiotazeta env x =
let whd_all env t =
match kind t with
| (Sort _|Meta _|Evar _|Ind _|Construct _|
- Prod _|Lambda _|Fix _|CoFix _|Int _|Float _) -> t
+ Prod _|Lambda _|Fix _|CoFix _|Int _|Float _|Array _) -> t
| App (c, _) ->
begin match kind c with
- | Ind _ | Construct _ | Evar _ | Meta _ | Int _ | Float _ -> t
+ | Ind _ | Construct _ | Evar _ | Meta _ | Int _ | Float _ | Array _ -> t
| Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
| Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
whd_val (create_clos_infos all env) (create_tab ()) (inject t)
@@ -166,10 +166,10 @@ let whd_all env t =
let whd_allnolet env t =
match kind t with
| (Sort _|Meta _|Evar _|Ind _|Construct _|
- Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _|Float _) -> t
+ Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _|Float _|Array _) -> t
| App (c, _) ->
begin match kind c with
- | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ | Float _ -> t
+ | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ | Float _ | Array _ -> t
| Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
| Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t)
@@ -209,12 +209,16 @@ type conv_pb =
let is_cumul = function CUMUL -> true | CONV -> false
-type 'a universe_compare =
- { (* Might raise NotConvertible *)
- compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
- compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
- compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
- Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
+type 'a universe_compare = {
+ (* used in reduction *)
+ compare_graph : 'a -> UGraph.t;
+
+ (* Might raise NotConvertible *)
+ compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+ compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+ compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
+ Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+}
type 'a universe_state = 'a * 'a universe_compare
@@ -302,7 +306,6 @@ let unfold_ref_with_args infos tab fl v =
type conv_tab = {
cnv_inf : clos_infos;
- relevances : Sorts.relevance Range.t;
lft_tab : clos_tab;
rgt_tab : clos_tab;
}
@@ -313,13 +316,13 @@ type conv_tab = {
passed to each respective side of the conversion function below. *)
let push_relevance infos r =
- { infos with relevances = Range.cons r.Context.binder_relevance infos.relevances }
+ { infos with cnv_inf = CClosure.push_relevance infos.cnv_inf r }
let push_relevances infos nas =
- { infos with relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) infos.relevances nas }
+ { infos with cnv_inf = CClosure.push_relevances infos.cnv_inf nas }
let rec skip_pattern infos relevances n c1 c2 =
- if Int.equal n 0 then {infos with relevances}, c1, c2
+ if Int.equal n 0 then {infos with cnv_inf = CClosure.set_info_relevances infos.cnv_inf relevances}, c1, c2
else match kind c1, kind c2 with
| Lambda (x, _, c1), Lambda (_, _, c2) ->
skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2
@@ -327,11 +330,11 @@ let rec skip_pattern infos relevances n c1 c2 =
let skip_pattern infos n c1 c2 =
if Int.equal n 0 then infos, c1, c2
- else skip_pattern infos infos.relevances n c1 c2
+ else skip_pattern infos (info_relevances infos.cnv_inf) n c1 c2
let is_irrelevant infos lft c =
let env = info_env infos.cnv_inf in
- try Relevanceops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false
+ try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
@@ -633,13 +636,31 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if Float64.equal f1 f2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
+ | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) ->
+ (if not (eq_ind ci1.ci_ind ci2.ci_ind) then raise NotConvertible);
+ let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in
+ let ccnv = ccnv CONV l2r infos el1 el2 in
+ let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in
+ Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv)
+ br1 br2 cuniv
+
+ | FArray (u1,t1,ty1), FArray (u2,t2,ty2) ->
+ let len = Parray.length_int t1 in
+ if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible;
+ let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+ let el1 = el_stack lft1 v1 in
+ let el2 = el_stack lft2 v2 in
+ let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
+ let cuniv = Parray.fold_left2 (fun u v1 v2 -> ccnv CONV l2r infos el1 el2 v1 v2 u) cuniv t1 t2 in
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+
(* 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
- | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
- | FProd _ | FEvar _ | FInt _ | FFloat _), _ -> raise NotConvertible
+ | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ | FCaseInvert _
+ | FProd _ | FEvar _ | FInt _ | FFloat _ | FArray _), _ -> raise NotConvertible
and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in
@@ -711,10 +732,10 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
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
+ let graph = (snd univs).compare_graph (fst univs) in
+ let infos = create_clos_infos ~univs:graph ~evars reds env in
let infos = {
cnv_inf = infos;
- relevances = Range.empty;
lft_tab = create_tab ();
rgt_tab = create_tab ();
} in
@@ -759,10 +780,25 @@ let check_inductive_instances cv_pb variance u1 u2 univs =
else raise NotConvertible
let checked_universes =
- { compare_sorts = checked_sort_cmp_universes;
+ { compare_graph = (fun x -> x);
+ compare_sorts = checked_sort_cmp_universes;
compare_instances = check_convert_instances;
compare_cumul_instances = check_inductive_instances; }
+let () =
+ let conv infos tab a b =
+ try
+ let univs = info_univs infos in
+ let infos = { cnv_inf = infos; lft_tab = tab; rgt_tab = tab; } in
+ let univs', _ = ccnv CONV false infos el_id el_id a b
+ (univs, checked_universes)
+ in
+ assert (univs==univs');
+ true
+ with NotConvertible -> false
+ in
+ CClosure.set_conv conv
+
let infer_eq (univs, cstrs as cuniv) u u' =
if UGraph.check_eq univs u u' then cuniv
else
@@ -807,7 +843,8 @@ let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') =
(univs, Univ.Constraint.union csts csts')
let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
- { compare_sorts = infer_cmp_universes;
+ { compare_graph = (fun (x,_) -> x);
+ compare_sorts = infer_cmp_universes;
compare_instances = infer_convert_instances;
compare_cumul_instances = infer_inductive_instances; }
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:57:05 +0000