diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 224 |
1 files changed, 124 insertions, 100 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 38d1c70b..fc5e32cf 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1,12 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reduction.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* Created under Benjamin Werner account by Bruno Barras to implement + a call-by-value conversion algorithm and a lazy reduction machine + with sharing, Nov 1996 *) +(* Addition of zeta-reduction (let-in contraction) by Hugo Herbelin, Oct 2000 *) +(* Irreversibility of opacity by Bruno Barras *) +(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *) +(* Equal inductive types by Jacek Chrzaszcz as part of the module + system, Aug 2002 *) open Util open Names @@ -190,9 +197,9 @@ let sort_cmp pb s0 s1 cuniv = | (_, _) -> raise NotConvertible -let conv_sort env s0 s1 = sort_cmp CONV s0 s1 Constraint.empty +let conv_sort env s0 s1 = sort_cmp CONV s0 s1 empty_constraint -let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty +let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 empty_constraint let rec no_arg_available = function | [] -> true @@ -232,14 +239,14 @@ 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) = + let rec whd_both (t1,stk1) (t2,stk2) = let st1' = whd_stack (snd infos) t1 stk1 in let st2' = whd_stack (snd infos) t2 stk2 in (* Now, whd_stack on term2 might have modified st1 (due to sharing), @@ -260,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 @@ -274,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 -> @@ -300,79 +307,95 @@ 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) - - (* 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 - | 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 - | None -> raise NotConvertible) + eqappr cv_pb l2r infos app1 app2 cuniv) (* other constructors *) | (FLambda _, FLambda _) -> + (* Inconsistency: we tolerate that v1, v2 contain shift and update but + we throw them away *) if not (is_empty_stack v1 && is_empty_stack v2) then 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 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 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 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 l2r infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv + | None -> raise NotConvertible) (* Inductive types: MutInd MutConstruct Fix Cofix *) - | (FInd ind1, FInd ind2) -> - if eq_ind ind1 ind2 - then - convert_stacks 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 - else raise NotConvertible - - | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) -> - if op1 = op2 - then - let n = Array.length cl1 in - let fty1 = Array.map (mk_clos e1) tys1 in - 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 u2 = - convert_vect infos - (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in - convert_stacks infos lft1 lft2 v1 v2 u2 - else raise NotConvertible - - | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) -> - if op1 = op2 - then - let n = Array.length cl1 in - let fty1 = Array.map (mk_clos e1) tys1 in - 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 u2 = - convert_vect infos - (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in - convert_stacks infos lft1 lft2 v1 v2 u2 - else raise NotConvertible + | (FInd ind1, FInd ind2) -> + if eq_ind ind1 ind2 + then + 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 l2r infos lft1 lft2 v1 v2 cuniv + else raise NotConvertible + + | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) -> + if op1 = op2 + then + let n = Array.length cl1 in + let fty1 = Array.map (mk_clos e1) tys1 in + 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 l2r infos el1 el2 fty1 fty2 cuniv in + let u2 = + convert_vect l2r infos + (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in + convert_stacks l2r infos lft1 lft2 v1 v2 u2 + else raise NotConvertible + + | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) -> + if op1 = op2 + then + let n = Array.length cl1 in + let fty1 = Array.map (mk_clos e1) tys1 in + 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 l2r infos el1 el2 fty1 fty2 cuniv in + let u2 = + convert_vect l2r infos + (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in + 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 *) | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) @@ -382,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 @@ -396,62 +419,62 @@ 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 ELID ELID (inject t1) (inject t2) Constraint.empty + 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 = - if eq_constr t1 t2 then Constraint.empty - else clos_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 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 - Constraint.union c c') - Constraint.empty + union_constraints c c') + empty_constraint 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 (* @@ -511,15 +534,16 @@ let dest_prod_assum env = in prodec_rec env empty_rel_context +exception NotArity + let dest_arity env c = let l, c = dest_prod_assum env c in match kind_of_term c with | Sort s -> l,s - | _ -> error "not an arity" + | _ -> raise NotArity let is_arity env c = try let _ = dest_arity env c in true - with UserError _ -> false - + with NotArity -> false |