aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/reduction.ml')
-rw-r--r--kernel/reduction.ml96
1 files changed, 48 insertions, 48 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1a286bb16c..fc5e32cf5c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -239,11 +239,11 @@ let in_whnf (t,stk) =
| FLOCKED -> assert false
(* Conversion between [lft1]term1 and [lft2]term2 *)
-let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv =
- eqappr cv_pb 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 cv_pb infos (lft1,st1) (lft2,st2) cuniv =
+and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
Util.check_for_interrupt ();
(* First head reduce both terms *)
let rec whd_both (t1,stk1) (t2,stk2) =
@@ -267,13 +267,13 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
sort_cmp cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
if n=m
- then convert_stacks 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 ev1=ev2 then
- let u1 = convert_stacks infos lft1 lft2 v1 v2 cuniv in
- convert_vect infos el1 el2
+ let u1 = 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) u1
else raise NotConvertible
@@ -281,19 +281,19 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
(* 2 index known to be bound to no constant *)
| (FRel n, FRel m) ->
if reloc_rel n el1 = reloc_rel m el2
- then convert_stacks 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 (* try first intensional equality *)
if eq_table_key fl1 fl2
- then convert_stacks infos lft1 lft2 v1 v2 cuniv
+ then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
with NotConvertible ->
(* else the oracle tells which constant is to be expanded *)
let (app1,app2) =
- if Conv_oracle.oracle_order fl1 fl2 then
+ if Conv_oracle.oracle_order l2r fl1 fl2 then
match unfold_reference infos fl1 with
| Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
| None ->
@@ -307,7 +307,7 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
(match unfold_reference infos fl1 with
| Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
| None -> raise NotConvertible) in
- eqappr cv_pb infos app1 app2 cuniv)
+ eqappr cv_pb l2r infos app1 app2 cuniv)
(* other constructors *)
| (FLambda _, FLambda _) ->
@@ -317,40 +317,40 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
anomaly "conversion was given ill-typed terms (FLambda)";
let (_,ty1,bd1) = destFLambda mk_clos hd1 in
let (_,ty2,bd2) = destFLambda mk_clos hd2 in
- let u1 = ccnv CONV infos el1 el2 ty1 ty2 cuniv in
- ccnv CONV infos (el_lift el1) (el_lift el2) bd1 bd2 u1
+ let u1 = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
+ ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 u1
| (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly "conversion was given ill-typed terms (FProd)";
(* Luo's system *)
- let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
- ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1
+ let u1 = 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 u1
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
if v1 <> [] then
anomaly "conversion was given unreduced term (FLambda)";
let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
- eqappr CONV infos
+ eqappr CONV l2r infos
(el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
| (_, FLambda _) ->
if v2 <> [] then
anomaly "conversion was given unreduced term (FLambda)";
let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
- eqappr CONV 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, _) ->
(match unfold_reference infos fl1 with
| Some def1 ->
- eqappr cv_pb infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
+ eqappr cv_pb l2r infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
| None -> raise NotConvertible)
| (_, FFlex fl2) ->
(match unfold_reference infos fl2 with
| Some def2 ->
- eqappr cv_pb infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
+ eqappr cv_pb l2r infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
| None -> raise NotConvertible)
(* Inductive types: MutInd MutConstruct Fix Cofix *)
@@ -358,13 +358,13 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
| (FInd ind1, FInd ind2) ->
if eq_ind ind1 ind2
then
- convert_stacks infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
if j1 = j2 && eq_ind ind1 ind2
then
- convert_stacks infos lft1 lft2 v1 v2 cuniv
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
@@ -375,11 +375,11 @@ and eqappr cv_pb 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 u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
+ let u1 = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
let u2 =
- convert_vect infos
+ convert_vect l2r infos
(el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
- convert_stacks infos lft1 lft2 v1 v2 u2
+ convert_stacks l2r infos lft1 lft2 v1 v2 u2
else raise NotConvertible
| (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
@@ -390,11 +390,11 @@ and eqappr cv_pb 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 u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
+ let u1 = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
let u2 =
- convert_vect infos
+ convert_vect l2r infos
(el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
- convert_stacks infos lft1 lft2 v1 v2 u2
+ convert_stacks l2r infos lft1 lft2 v1 v2 u2
else raise NotConvertible
(* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
@@ -405,13 +405,13 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
(* In all other cases, terms are not convertible *)
| _ -> raise NotConvertible
-and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
+and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
compare_stacks
- (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c)
+ (fun (l1,t1) (l2,t2) c -> ccnv CONV l2r infos l1 l2 t1 t2 c)
(eq_ind)
lft1 stk1 lft2 stk2 cuniv
-and convert_vect 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 lv1 = lv2
@@ -419,34 +419,34 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
let rec fold n univ =
if n >= lv1 then univ
else
- let u1 = ccnv CONV infos lft1 lft2 v1.(n) v2.(n) univ in
+ let u1 = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) univ in
fold (n+1) u1 in
fold 0 cuniv
else raise NotConvertible
-let clos_fconv trans cv_pb evars env t1 t2 =
+let clos_fconv trans cv_pb l2r evars env t1 t2 =
let infos = trans, create_clos_infos ~evars betaiotazeta env in
- ccnv cv_pb infos el_id el_id (inject t1) (inject t2) empty_constraint
+ ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) empty_constraint
-let trans_fconv reds cv_pb evars env t1 t2 =
+let trans_fconv reds cv_pb l2r evars env t1 t2 =
if eq_constr t1 t2 then empty_constraint
- else clos_fconv reds cv_pb evars env t1 t2
+ else clos_fconv reds cv_pb l2r evars env t1 t2
-let trans_conv_cmp conv reds = trans_fconv reds conv (fun _->None)
-let trans_conv ?(evars=fun _->None) reds = trans_fconv reds CONV evars
-let trans_conv_leq ?(evars=fun _->None) reds = trans_fconv reds CUMUL evars
+let trans_conv_cmp ?(l2r=false) conv reds = trans_fconv reds conv l2r (fun _->None)
+let trans_conv ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CONV l2r evars
+let trans_conv_leq ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CUMUL l2r evars
let fconv = trans_fconv (Idpred.full, Cpred.full)
-let conv_cmp cv_pb = fconv cv_pb (fun _->None)
-let conv ?(evars=fun _->None) = fconv CONV evars
-let conv_leq ?(evars=fun _->None) = fconv CUMUL evars
+let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None)
+let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars
+let conv_leq ?(l2r=false) ?(evars=fun _->None) = fconv CUMUL l2r evars
-let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
+let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
array_fold_left2_i
(fun i c t1 t2 ->
let c' =
- try conv_leq ~evars env t1 t2
+ try conv_leq ~l2r ~evars env t1 t2
with NotConvertible -> raise (NotConvertibleVect i) in
union_constraints c c')
empty_constraint
@@ -455,26 +455,26 @@ let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
(* option for conversion *)
-let vm_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
+let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
let set_vm_conv f = vm_conv := f
let vm_conv cv_pb env t1 t2 =
try
!vm_conv cv_pb env t1 t2
with Not_found | Invalid_argument _ ->
(* If compilation fails, fall-back to closure conversion *)
- fconv cv_pb (fun _->None) env t1 t2
+ fconv cv_pb false (fun _->None) env t1 t2
-let default_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
+let default_conv = ref (fun cv_pb ?(l2r=false) -> fconv cv_pb l2r (fun _->None))
let set_default_conv f = default_conv := f
-let default_conv cv_pb env t1 t2 =
+let default_conv cv_pb ?(l2r=false) env t1 t2 =
try
- !default_conv cv_pb env t1 t2
+ !default_conv ~l2r cv_pb env t1 t2
with Not_found | Invalid_argument _ ->
(* If compilation fails, fall-back to closure conversion *)
- fconv cv_pb (fun _->None) env t1 t2
+ fconv cv_pb false (fun _->None) env t1 t2
let default_conv_leq = default_conv CUMUL
(*
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 14:28:02 +0000