diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cbv.ml | 8 | ||||
| -rw-r--r-- | pretyping/inferCumulativity.ml | 10 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 56 |
4 files changed, 42 insertions, 34 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 7cfb30f4c1..a2155697ec 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -134,7 +134,7 @@ let mkSTACK = function | STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk) | v,stk -> STACK(0,v,stk) -type cbv_infos = { infos : cbv_value infos; sigma : Evd.evar_map } +type cbv_infos = { tab : cbv_value infos_tab; infos : cbv_value infos; sigma : Evd.evar_map } (* Change: zeta reduction cannot be avoided in CBV *) @@ -318,7 +318,7 @@ let rec norm_head info env t stack = and norm_head_ref k info env stack normt = if red_set_ref (info_flags info.infos) normt then - match ref_value_cache info.infos normt with + match ref_value_cache info.infos info.tab normt with | Some body -> if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); strip_appl (shift_value k body) stack @@ -455,8 +455,8 @@ let cbv_norm infos constr = (* constant bodies are normalized at the first expansion *) let create_cbv_infos flgs env sigma = let infos = create - (fun old_info c -> cbv_stack_term { infos = old_info; sigma } TOP (subs_id 0) c) + (fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) flgs env (Reductionops.safe_evar_value sigma) in - { infos; sigma } + { tab = CClosure.create_tab (); infos; sigma } diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index 20883f6f6b..eb283a0220 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -83,10 +83,12 @@ let infer_table_key infos variances c = infer_generic_instance_eq variances u | VarKey _ | RelKey _ -> variances +let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk + let rec infer_fterm cv_pb infos variances hd stk = Control.check_for_interrupt (); - let open CClosure in let hd,stk = whd_stack infos hd stk in + let open CClosure in match fterm_of hd with | FAtom a -> begin match kind a with @@ -116,7 +118,7 @@ let rec infer_fterm cv_pb infos variances hd stk = if Instance.is_empty u then variances else let nargs = stack_args_size stk in - infer_inductive_instance cv_pb (info_env infos) variances ind nargs u + infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u in infer_stack infos variances stk | FConstruct (ctor,u) -> @@ -124,7 +126,7 @@ let rec infer_fterm cv_pb infos variances hd stk = if Instance.is_empty u then variances else let nargs = stack_args_size stk in - infer_constructor_instance_eq (info_env infos) variances ctor nargs u + infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u in infer_stack infos variances stk | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) -> @@ -161,7 +163,7 @@ and infer_vect infos variances v = let infer_term cv_pb env variances c = let open CClosure in - let infos = create_clos_infos all env in + let infos = (create_clos_infos all env, create_tab ()) in infer_fterm cv_pb infos variances (CClosure.inject c) [] let infer_arity_constructor is_arity env variances arcn = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 221771f4e4..9e3e68f059 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1236,6 +1236,7 @@ let clos_norm_flags flgs env sigma t = let evars ev = safe_evar_value sigma ev in EConstr.of_constr (CClosure.norm_val (CClosure.create_clos_infos ~evars flgs env) + (CClosure.create_tab ()) (CClosure.inject (EConstr.Unsafe.to_constr t))) with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") @@ -1244,6 +1245,7 @@ let clos_whd_flags flgs env sigma t = let evars ev = safe_evar_value sigma ev in EConstr.of_constr (CClosure.whd_val (CClosure.create_clos_infos ~evars flgs env) + (CClosure.create_tab ()) (CClosure.inject (EConstr.Unsafe.to_constr t))) with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 542bf775fb..4c834f2f8f 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -59,19 +59,21 @@ let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv = let ar = inductive_type_knowing_parameters env !evdref ind argjv in hnf_prod_appvect env !evdref (EConstr.of_constr ar) (Array.map j_val argjv) } | hj::restjl -> - match EConstr.kind !evdref (whd_all env !evdref typ) with - | Prod (_,c1,c2) -> - if Evarconv.e_cumul env evdref hj.uj_type c1 then - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - else - error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv - | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product !evdref ev in - evdref := evd'; - let (_,_,c2) = destProd evd' t in - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - | _ -> - error_cant_apply_not_functional env !evdref funj argjv + let (c1,c2) = + match EConstr.kind !evdref (whd_all env !evdref typ) with + | Prod (_,c1,c2) -> (c1,c2) + | Evar ev -> + let (evd',t) = Evardefine.define_evar_as_product !evdref ev in + evdref := evd'; + let (_,c1,c2) = destProd evd' t in + (c1,c2) + | _ -> + error_cant_apply_not_functional env !evdref funj argjv + in + if Evarconv.e_cumul env evdref hj.uj_type c1 then + apply_rec (n+1) (subst1 hj.uj_val c2) restjl + else + error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv in apply_rec 1 funj.uj_type (Array.to_list argjv) @@ -81,19 +83,21 @@ let e_judge_of_apply env evdref funj argjv = { uj_val = mkApp (j_val funj, Array.map j_val argjv); uj_type = typ } | hj::restjl -> - match EConstr.kind !evdref (whd_all env !evdref typ) with - | Prod (_,c1,c2) -> - if Evarconv.e_cumul env evdref hj.uj_type c1 then - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - else - error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv - | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product !evdref ev in - evdref := evd'; - let (_,_,c2) = destProd evd' t in - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - | _ -> - error_cant_apply_not_functional env !evdref funj argjv + let (c1,c2) = + match EConstr.kind !evdref (whd_all env !evdref typ) with + | Prod (_,c1,c2) -> (c1,c2) + | Evar ev -> + let (evd',t) = Evardefine.define_evar_as_product !evdref ev in + evdref := evd'; + let (_,c1,c2) = destProd evd' t in + (c1,c2) + | _ -> + error_cant_apply_not_functional env !evdref funj argjv + in + if Evarconv.e_cumul env evdref hj.uj_type c1 then + apply_rec (n+1) (subst1 hj.uj_val c2) restjl + else + error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv in apply_rec 1 funj.uj_type (Array.to_list argjv) |