diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 45 |
1 files changed, 20 insertions, 25 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 518d2f60..8911a2f3 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Libnames open Globnames open Termops @@ -49,7 +49,7 @@ let error_not_evaluable r = let is_evaluable_const env cst = is_transparent env (ConstKey cst) && - (evaluable_constant cst env || is_projection cst env) + evaluable_constant cst env let is_evaluable_var env id = is_transparent env (VarKey id) && evaluable_named id env @@ -416,7 +416,7 @@ exception Partial reduction is solved by the expanded fix term. *) let solve_arity_problem env sigma fxminargs c = let evm = ref sigma in - let set_fix i = evm := Evd.define i (Constr.mkVar vfx) !evm in + let set_fix i = evm := Evd.define i (mkVar vfx) !evm in let rec check strict c = let c' = whd_betaiotazeta sigma c in let (h,rcargs) = decompose_app_vect sigma c' in @@ -539,7 +539,7 @@ let reduce_mind_case_use_function func env sigma mia = let match_eval_ref env sigma constr stack = match EConstr.kind sigma constr with | Const (sp, u) -> - reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + reduction_effect_hook env sigma sp (lazy (EConstr.to_constr sigma (applist (constr,stack)))); if is_evaluable env (EvalConstRef sp) then Some (EvalConst sp, u) else None | Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, EInstance.empty) @@ -550,7 +550,7 @@ let match_eval_ref env sigma constr stack = let match_eval_ref_value env sigma constr stack = match EConstr.kind sigma constr with | Const (sp, u) -> - reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + reduction_effect_hook env sigma sp (lazy (EConstr.to_constr sigma (applist (constr,stack)))); if is_evaluable env (EvalConstRef sp) then let u = EInstance.kind sigma u in @@ -558,8 +558,6 @@ let match_eval_ref_value env sigma constr stack = else None | Proj (p, c) when not (Projection.unfolded p) -> - reduction_effect_hook env sigma (EConstr.to_constr sigma constr) - (lazy (EConstr.to_constr sigma (applist (constr,stack)))); if is_evaluable env (EvalConstRef (Projection.constant p)) then Some (mkProj (Projection.unfold p, c)) else None @@ -597,12 +595,11 @@ let recargs = function | EvalVar _ | EvalRel _ | EvalEvar _ -> None | EvalConst c -> ReductionBehaviour.get (ConstRef c) -let reduce_projection env sigma pb (recarg'hd,stack') stack = +let reduce_projection env sigma p ~npars (recarg'hd,stack') stack = (match EConstr.kind sigma recarg'hd with | Construct _ -> - let proj_narg = - pb.Declarations.proj_npars + pb.Declarations.proj_arg - in Reduced (List.nth stack' proj_narg, stack) + let proj_narg = npars + Projection.arg p in + Reduced (List.nth stack' proj_narg, stack) | _ -> NotReducible) let reduce_proj env sigma whfun whfun' c = @@ -613,10 +610,8 @@ let reduce_proj env sigma whfun whfun' c = let constr, cargs = whfun c' in (match EConstr.kind sigma constr with | Construct _ -> - let proj_narg = - let pb = lookup_projection proj env in - pb.Declarations.proj_npars + pb.Declarations.proj_arg - in List.nth cargs proj_narg + let proj_narg = Projection.npars proj + Projection.arg proj in + List.nth cargs proj_narg | _ -> raise Redelimination) | Case (n,p,c,brs) -> let c' = redrec c in @@ -641,7 +636,7 @@ let whd_nothing_for_iota env sigma s = | _ -> s) | Evar ev -> s | Meta ev -> - (try whrec (EConstr.of_constr (Evd.meta_value sigma ev), stack) + (try whrec (Evd.meta_value sigma ev, stack) with Not_found -> s) | Const (const, u) when is_transparent_constant full_transparent_state const -> let u = EInstance.kind sigma u in @@ -765,22 +760,22 @@ and whd_simpl_stack env sigma = (try let unf = Projection.unfolded p in if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then - let pb = lookup_projection p env in + let npars = Projection.npars p in (match unf, ReductionBehaviour.get (ConstRef (Projection.constant p)) with | false, Some (l, n, f) when List.mem `ReductionNeverUnfold f -> (* simpl never *) s' | false, Some (l, n, f) when not (List.is_empty l) -> let l' = List.map_filter (fun i -> - let idx = (i - (pb.Declarations.proj_npars + 1)) in + let idx = (i - (npars + 1)) in if idx < 0 then None else Some idx) l in let stack = reduce_params env sigma stack l' in - (match reduce_projection env sigma pb + (match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with | Reduced s' -> redrec (applist s') | NotReducible -> s') | _ -> - match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack with + match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with | Reduced s' -> redrec (applist s') | NotReducible -> s') else s' @@ -852,8 +847,8 @@ let try_red_product env sigma c = | Construct _ -> c | _ -> redrec env c in - let pb = lookup_projection p env in - (match reduce_projection env sigma pb (whd_betaiotazeta_stack sigma c') [] with + let npars = Projection.npars p in + (match reduce_projection env sigma p ~npars (whd_betaiotazeta_stack sigma c') [] with | Reduced s -> simpfun (applist s) | NotReducible -> raise Redelimination) | _ -> @@ -946,8 +941,8 @@ let whd_simpl_orelse_delta_but_fix env sigma c = (match EConstr.kind sigma constr with | Const (c', _) -> Constant.equal (Projection.constant p) c' | _ -> false) -> - let pb = Environ.lookup_projection p env in - if List.length stack <= pb.Declarations.proj_npars then + let npars = Projection.npars p in + if List.length stack <= npars then (** Do not show the eta-expanded form *) s' else redrec (applist (c, stack)) @@ -1279,7 +1274,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = error_cannot_recognize ref | _ -> try - if eq_gr (fst (global_of_constr sigma c)) ref + if GlobRef.equal (fst (global_of_constr sigma c)) ref then it_mkProd_or_LetIn t l else raise Not_found with Not_found -> |