diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 205 |
1 files changed, 93 insertions, 112 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 97c3e1b3..1ae89347 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -15,16 +15,15 @@ (* Equal inductive types by Jacek Chrzaszcz as part of the module system, Aug 2002 *) -open Errors +open CErrors open Util open Names open Term open Vars -open Context -open Univ open Environ -open Closure +open CClosure open Esubst +open Context.Rel.Declaration let rec is_empty_stack = function [] -> true @@ -54,8 +53,7 @@ let compare_stack_shape stk1 stk2 = | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1, - (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) -> + | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) -> 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 @@ -89,9 +87,8 @@ let pure_stack lfts stk = let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,e),(l,pstk)) -> - (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk) - | (Zcase(ci,p,br),(l,pstk)) -> - (l,Zlcase(ci,l,p,br)::pstk)) in + (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk)) + in snd (pure_rec lfts stk) (****************************************************************************) @@ -110,46 +107,32 @@ let whd_betaiotazeta env x = Prod _|Lambda _|Fix _|CoFix _) -> x | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) -let whd_betadeltaiota env t = +let whd_all env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t - | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t) + | _ -> whd_val (create_clos_infos all env) (inject t) -let whd_betadeltaiota_nolet env t = +let whd_allnolet env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t - | _ -> whd_val (create_clos_infos betadeltaiotanolet env) (inject t) - -(* Beta *) - -let beta_appvect c v = - let rec stacklam env t stack = - match kind_of_term t, stack with - Lambda(_,_,c), arg::stacktl -> stacklam (arg::env) c stacktl - | _ -> applist (substl env t, stack) in - stacklam [] c (Array.to_list v) - -let betazeta_appvect n c v = - let rec stacklam n env t stack = - if Int.equal n 0 then applist (substl env t, stack) else - match kind_of_term t, stack with - Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack - | _ -> anomaly (Pp.str "Not enough lambda/let's") in - stacklam n [] c (Array.to_list v) + | _ -> whd_val (create_clos_infos allnolet env) (inject t) (********************************************************************) (* Conversion *) (********************************************************************) (* Conversion utility functions *) -type 'a conversion_function = env -> 'a -> 'a -> unit -type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function -type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit -type 'a trans_universe_conversion_function = - Names.transparent_state -> 'a universe_conversion_function + +(* functions of this type are called from the kernel *) +type 'a kernel_conversion_function = env -> 'a -> 'a -> unit + +(* functions of this type can be called from outside the kernel *) +type 'a extended_conversion_function = + ?l2r:bool -> ?reds:Names.transparent_state -> env -> + ?evars:((existential->constr option) * UGraph.t) -> + 'a -> 'a -> unit exception NotConvertible exception NotConvertibleVect of int @@ -180,7 +163,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare env pb s0 s1 u, check) @@ -193,7 +176,7 @@ let convert_instances ~flex u u' (s, check) = let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else match k1, k2 with - | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' -> + | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' -> if Univ.Instance.equal u u' then cuniv else let flex = evaluable_constant cst (info_env infos) @@ -235,7 +218,6 @@ let rec no_arg_available = function | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -248,7 +230,6 @@ let rec no_nth_arg_available n = function if n >= k then no_nth_arg_available (n-k) stk else false | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -258,13 +239,12 @@ let rec no_case_available = function | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk | Zproj (_,_,p) :: _ -> false - | Zcase _ :: _ -> false | ZcaseT _ :: _ -> false | Zfix _ :: _ -> true let in_whnf (t,stk) = match fterm_of t with - | (FLetIn _ | FCase _ | FCaseT _ | FApp _ + | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false | FLambda _ -> no_arg_available stk | FConstruct _ -> no_case_available stk @@ -336,9 +316,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (try let cuniv = conv_table_key infos fl1 fl2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with NotConvertible -> + with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) - let oracle = Closure.oracle_of_infos infos in + let oracle = CClosure.oracle_of_infos infos in let (app1,app2) = if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then match unfold_reference infos fl1 with @@ -530,8 +510,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) - | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) - | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) + | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) + | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false (* In all other cases, terms are not convertible *) @@ -556,17 +536,17 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = fold 0 cuniv else raise NotConvertible -let clos_fconv trans cv_pb l2r evars env univs t1 t2 = - let reds = Closure.RedFlags.red_add_transparent betaiotazeta trans in +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 cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs let check_eq univs u u' = - if not (check_eq univs u u') then raise NotConvertible + if not (UGraph.check_eq univs u u') then raise NotConvertible let check_leq univs u u' = - if not (check_leq univs u u') then raise NotConvertible + if not (UGraph.check_leq univs u u') then raise NotConvertible let check_sort_cmp_universes env pb s0 s1 univs = match (s0,s1) with @@ -593,7 +573,7 @@ let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs let check_convert_instances ~flex u u' univs = - if Univ.Instance.check_eq univs u u' then univs + if UGraph.check_eq_instances univs u u' then univs else raise NotConvertible let checked_universes = @@ -601,12 +581,12 @@ let checked_universes = compare_instances = check_convert_instances } let infer_eq (univs, cstrs as cuniv) u u' = - if Univ.check_eq univs u u' then cuniv + if UGraph.check_eq univs u u' then cuniv else univs, (Univ.enforce_eq u u' cstrs) let infer_leq (univs, cstrs as cuniv) u u' = - if Univ.check_leq univs u u' then cuniv + if UGraph.check_leq univs u u' then cuniv else let cstrs' = Univ.enforce_leq u u' cstrs in univs, cstrs' @@ -635,57 +615,35 @@ let infer_cmp_universes env pb s0 s1 univs = let infer_convert_instances ~flex u u' (univs,cstrs) = (univs, Univ.enforce_eq_instances u u' cstrs) -let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare = +let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; compare_instances = infer_convert_instances } -let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 = +let gen_conv cv_pb l2r reds env evars univs t1 t2 = let b = if cv_pb = CUMUL then leq_constr_univs univs t1 t2 else eq_constr_univs univs t1 t2 in if b then () else - let _ = clos_fconv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in + let _ = clos_gen_conv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in () (* Profiling *) -let trans_fconv_universes = +let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = + let evars, univs = evars in if Flags.profile then - let trans_fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in - Profile.profile8 trans_fconv_universes_key trans_fconv_universes - else trans_fconv_universes - -let trans_fconv reds cv_pb l2r evars env = - trans_fconv_universes reds cv_pb l2r evars env (universes env) - -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 trans_conv_universes ?(l2r=false) ?(evars=fun _->None) reds = - trans_fconv_universes reds CONV l2r evars -let trans_conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = - trans_fconv_universes reds CUMUL l2r evars - -let fconv = trans_fconv full_transparent_state + let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in + Profile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs + else gen_conv cv_pb l2r reds env evars univs -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 = gen_conv CONV -let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = - Array.fold_left2_i - (fun i _ t1 t2 -> - try conv_leq ~l2r ~evars env t1 t2 - with NotConvertible -> raise (NotConvertibleVect i)) - () - v1 - v2 +let conv_leq = gen_conv CUMUL let generic_conv cv_pb ~l2r evars reds env univs t1 t2 = let (s, _) = - clos_fconv reds cv_pb l2r evars env univs t1 t2 + clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in s let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = @@ -696,7 +654,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = if b then cstrs else let univs = ((univs, Univ.Constraint.empty), inferred_universes) in - let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in + let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in cstrs (* Profiling *) @@ -715,18 +673,25 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta infer_conv_universes CUMUL l2r evars ts env univs t1 t2 (* This reference avoids always having to link C code with the kernel *) -let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None)) -let set_vm_conv f = vm_conv := f +let vm_conv = ref (fun cv_pb env -> + gen_conv cv_pb env ~evars:((fun _->None), universes env)) + +let warn_bytecode_compiler_failed = + let open Pp in + CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler" + (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 vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> - (Pp.msg_warning - (Pp.str "Bytecode compilation failed, falling back to default conversion"); - fconv cv_pb false (fun _->None) env t1 t2) + warn_bytecode_compiler_failed (); + gen_conv cv_pb env t1 t2 let default_conv cv_pb ?(l2r=false) env t1 t2 = - fconv cv_pb false (fun _ -> None) env t1 t2 + gen_conv cv_pb env t1 t2 let default_conv_leq = default_conv CUMUL (* @@ -739,18 +704,34 @@ let conv env t1 t2 = Profile.profile4 convleqkey conv env t1 t2;; *) +(* Application with on-the-fly reduction *) + +let beta_applist c l = + let rec app subst c l = + match kind_of_term c, l with + | Lambda(_,_,c), arg::l -> app (arg::subst) c l + | _ -> applist (substl subst c, l) in + app [] c l + +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 + (********************************************************************) (* Special-Purpose Reduction *) (********************************************************************) (* pseudo-reduction rule: - * [hnf_prod_app env s (Prod(_,B)) N --> B[N] + * [hnf_prod_app env (Prod(_,B)) N --> B[N] * with an HNF on the first argument to produce a product. * if this does not work, then we use the string S as part of our * error message. *) let hnf_prod_app env t n = - match kind_of_term (whd_betadeltaiota env t) with + match kind_of_term (whd_all env t) with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") @@ -761,48 +742,48 @@ let hnf_prod_applist env t nl = let dest_prod env = let rec decrec env m c = - let t = whd_betadeltaiota env c in + let t = whd_all env c in match kind_of_term t with | Prod (n,a,c0) -> - let d = (n,None,a) in - decrec (push_rel d env) (add_rel_decl d m) c0 + let d = LocalAssum (n,a) in + decrec (push_rel d env) (Context.Rel.add d m) c0 | _ -> m,t in - decrec env empty_rel_context + decrec env Context.Rel.empty (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet env ty in match kind_of_term rty with | Prod (x,t,c) -> - let d = (x,None,t) in - prodec_rec (push_rel d env) (add_rel_decl d l) c + let d = LocalAssum (x,t) in + prodec_rec (push_rel d env) (Context.Rel.add d l) c | LetIn (x,b,t,c) -> - let d = (x,Some b,t) in - prodec_rec (push_rel d env) (add_rel_decl d l) c + let d = LocalDef (x,b,t) in + prodec_rec (push_rel d env) (Context.Rel.add d l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> - let rty' = whd_betadeltaiota env rty in + let rty' = whd_all env rty in if Term.eq_constr rty' rty then l, rty else prodec_rec env l rty' in - prodec_rec env empty_rel_context + prodec_rec env Context.Rel.empty let dest_lam_assum env = let rec lamec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet env ty in match kind_of_term rty with | Lambda (x,t,c) -> - let d = (x,None,t) in - lamec_rec (push_rel d env) (add_rel_decl d l) c + let d = LocalAssum (x,t) in + lamec_rec (push_rel d env) (Context.Rel.add d l) c | LetIn (x,b,t,c) -> - let d = (x,Some b,t) in - lamec_rec (push_rel d env) (add_rel_decl d l) c + let d = LocalDef (x,b,t) in + lamec_rec (push_rel d env) (Context.Rel.add d l) c | Cast (c,_,_) -> lamec_rec env l c | _ -> l,rty in - lamec_rec env empty_rel_context + lamec_rec env Context.Rel.empty exception NotArity |