diff options
| -rw-r--r-- | ltac/tacinterp.ml | 4 | ||||
| -rw-r--r-- | plugins/quote/quote.ml | 4 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 43 | ||||
| -rw-r--r-- | pretyping/patternops.mli | 3 | ||||
| -rw-r--r-- | tactics/hints.ml | 10 |
5 files changed, 40 insertions, 24 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 8f5ac7e76..85d4ac06e 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -691,7 +691,7 @@ let interp_pure_open_constr ist = let interp_typed_pattern ist env sigma (_,c,_) = let sigma, c = interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in - pattern_of_constr env sigma c + pattern_of_constr env sigma (EConstr.of_constr c) (* Interprets a constr expression *) let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = @@ -736,7 +736,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = try Inl (coerce_to_evaluable_ref env x) with CannotCoerceTo _ -> let c = coerce_to_closed_constr env x in - Inr (pattern_of_constr env sigma c) in + Inr (pattern_of_constr env sigma (EConstr.of_constr c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id) with Not_found -> error_global_not_found ~loc (qualid_of_ident id)) diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index afc7e6665..a13948f77 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -212,9 +212,9 @@ let compute_rhs bodyi index_of_f = let i = destRel (Array.last args) in PMeta (Some (coerce_meta_in i)) | App (f,args) -> - PApp (pattern_of_constr (Global.env()) Evd.empty f, Array.map aux args) + PApp (pattern_of_constr (Global.env()) Evd.empty (EConstr.of_constr f), Array.map aux args) | Cast (c,_,_) -> aux c - | _ -> pattern_of_constr (Global.env())(*FIXME*) Evd.empty c + | _ -> pattern_of_constr (Global.env())(*FIXME*) Evd.empty (EConstr.of_constr c) in aux bodyi diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 938b6b18e..d473f41bd 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -114,17 +114,27 @@ let rec head_pattern_bound t = | PLambda _ -> raise BoundPattern | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type") -let head_of_constr_reference c = match kind_of_term c with +let head_of_constr_reference sigma c = match EConstr.kind sigma c with | Const (sp,_) -> ConstRef sp | Construct (sp,_) -> ConstructRef sp | Ind (sp,_) -> IndRef sp | Var id -> VarRef id | _ -> anomaly (Pp.str "Not a rigid reference") +let local_assum (na, t) = + let open Context.Rel.Declaration in + let inj = EConstr.Unsafe.to_constr in + LocalAssum (na, inj t) + +let local_def (na, b, t) = + let open Context.Rel.Declaration in + let inj = EConstr.Unsafe.to_constr in + LocalDef (na, inj b, inj t) + let pattern_of_constr env sigma t = + let open EConstr in let rec pattern_of_constr env t = - let open Context.Rel.Declaration in - match kind_of_term t with + match EConstr.kind sigma t with | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id @@ -133,14 +143,14 @@ let pattern_of_constr env sigma t = | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c, - pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) + pattern_of_constr (push_rel (local_def (na,c,t)) env) b) | Prod (na,c,b) -> PProd (na,pattern_of_constr env c, - pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) + pattern_of_constr (push_rel (local_assum (na, c)) env) b) | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c, - pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) + pattern_of_constr (push_rel (local_assum (na, c)) env) b) | App (f,a) -> (match - match kind_of_term f with + match EConstr.kind sigma f with | Evar (evk,args) -> (match snd (Evd.evar_source evk sigma) with Evar_kinds.MatchingVar (true,id) -> Some id @@ -153,17 +163,17 @@ let pattern_of_constr env sigma t = | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) | Proj (p, c) -> - pattern_of_constr env (Retyping.expand_projection env sigma p (EConstr.of_constr c) []) + pattern_of_constr env (EConstr.of_constr (Retyping.expand_projection env sigma p c [])) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> - let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + let ty = existential_type sigma ev in let () = ignore (pattern_of_constr env ty) in assert (not b); PMeta (Some id) | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> - let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + let ty = existential_type sigma ev in let () = ignore (pattern_of_constr env ty) in PMeta None) | Case (ci,p,a,br) -> @@ -178,8 +188,13 @@ let pattern_of_constr env sigma t = in PCase (cip, pattern_of_constr env p, pattern_of_constr env a, Array.to_list (Array.mapi branch_of_constr br)) - | Fix f -> PFix f - | CoFix f -> PCoFix f in + | Fix (idx, (nas, cs, ts)) -> + let inj c = EConstr.to_constr sigma c in + PFix (idx, (nas, Array.map inj cs, Array.map inj ts)) + | CoFix (idx, (nas, cs, ts)) -> + let inj c = EConstr.to_constr sigma c in + PCoFix (idx, (nas, Array.map inj cs, Array.map inj ts)) + in pattern_of_constr env t (* To process patterns, we need a translation without typing at all. *) @@ -220,7 +235,7 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in - pattern_of_constr env sigma c + pattern_of_constr env sigma (EConstr.of_constr c) with Not_found (* List.index failed *) -> let vars = List.map_filter (function Name id -> Some id | _ -> None) vars in @@ -245,7 +260,7 @@ let rec subst_pattern subst pat = | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else - pattern_of_constr (Global.env()) Evd.empty t + pattern_of_constr (Global.env()) Evd.empty (EConstr.of_constr t) | PVar _ | PEvar _ | PRel _ -> pat diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 1f63565d6..93d2c859a 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -7,6 +7,7 @@ (************************************************************************) open Term +open EConstr open Globnames open Glob_term open Mod_subst @@ -32,7 +33,7 @@ val head_pattern_bound : constr_pattern -> global_reference (** [head_of_constr_reference c] assumes [r] denotes a reference and returns its label; raises an anomaly otherwise *) -val head_of_constr_reference : Term.constr -> global_reference +val head_of_constr_reference : Evd.evar_map -> constr -> global_reference (** [pattern_of_constr c] translates a term [c] with metavariables into a pattern; currently, no destructor (Cases, Fix, Cofix) and no diff --git a/tactics/hints.ml b/tactics/hints.ml index 63d10573a..b2aa02191 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -746,7 +746,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = Patternops.pattern_of_constr env sigma cty in + let pat = Patternops.pattern_of_constr env sigma (EConstr.of_constr cty) in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -767,7 +767,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, let sigma' = Evd.merge_context_set univ_flexible sigma ctx in let ce = mk_clenv_from_env env sigma' None (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = Patternops.pattern_of_constr env ce.evd c' in + let pat = Patternops.pattern_of_constr env ce.evd (EConstr.of_constr c') in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -911,11 +911,11 @@ let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in - let hd = head_of_constr_reference (head_constr sigma t) in + let hd = head_of_constr_reference sigma (EConstr.of_constr (head_constr sigma t)) in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; poly = poly; - pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce)); + pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.of_constr (clenv_type ce))); name = name; db = None; secvars = secvars_of_constr env c; @@ -1013,7 +1013,7 @@ let subst_autohint (subst, obj) = let subst_key gr = let (lab'', elab') = subst_global subst gr in let gr' = - (try head_of_constr_reference (head_constr_bound Evd.empty (** FIXME *) elab') + (try head_of_constr_reference Evd.empty (EConstr.of_constr (head_constr_bound Evd.empty (** FIXME *) elab')) with Bound -> lab'') in if gr' == gr then gr else gr' in |