summaryrefslogtreecommitdiff
path: root/plugins/ltac/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
-rw-r--r--plugins/ltac/tacinterp.ml99
1 files changed, 61 insertions, 38 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index c6c4f469..b9e892e5 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -12,6 +12,7 @@ open Constrintern
open Patternops
open Pp
open CAst
+open Namegen
open Genredexpr
open Glob_term
open Glob_ops
@@ -35,7 +36,8 @@ open Stdarg
open Tacarg
open Printer
open Pretyping
-open Misctypes
+open Tactypes
+open Tactics
open Locus
open Tacintern
open Taccoerce
@@ -140,16 +142,6 @@ let extract_trace ist = match TacStore.get ist.extra f_trace with
| None -> []
| Some l -> l
-module Value = struct
-
- include Taccoerce.Value
-
- let of_closure ist tac =
- let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
- of_tacvalue closure
-
-end
-
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
let catching_error call_trace fail (e, info) =
@@ -291,6 +283,12 @@ let debugging_exception_step ist signal_anomaly e pp =
debugging_step ist (fun () ->
pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
+let ensure_freshness env =
+ (* We anonymize declarations which we know will not be used *)
+ (* This assumes that the original context had no rels *)
+ process_rel_context
+ (fun d e -> EConstr.push_rel (Context.Rel.Declaration.set_name Anonymous d) e) env
+
(* Raise Not_found if not in interpretation sign *)
let try_interp_ltac_var coerce ist env {loc;v=id} =
let v = Id.Map.find id ist.lfun in
@@ -311,11 +309,11 @@ let interp_name ist env sigma = function
| Name id -> Name (interp_ident ist env sigma id)
let interp_intro_pattern_var loc ist env sigma id =
- try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id)
+ try try_interp_ltac_var (coerce_to_intro_pattern sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found -> IntroNaming (IntroIdentifier id)
let interp_intro_pattern_naming_var loc ist env sigma id =
- try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id)
+ try try_interp_ltac_var (coerce_to_intro_pattern_naming sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found -> IntroIdentifier id
let interp_int ist ({loc;v=id} as locid) =
@@ -356,11 +354,11 @@ let interp_hyp_list ist env sigma l =
let interp_reference ist env sigma = function
| ArgArg (_,r) -> r
| ArgVar {loc;v=id} ->
- try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id)
+ try try_interp_ltac_var (coerce_to_reference sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
try
VarRef (get_id (Environ.lookup_named id env))
- with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id)
+ with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
let try_interp_evaluable env (loc, id) =
let v = Environ.lookup_named id env in
@@ -376,14 +374,14 @@ let interp_evaluable ist env sigma = function
with Not_found ->
match r with
| EvalConstRef _ -> r
- | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id)
+ | _ -> error_global_not_found (qualid_of_ident ?loc id)
end
| ArgArg (r,None) -> r
| ArgVar {loc;v=id} ->
try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
try try_interp_evaluable env (loc, id)
- with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id)
+ with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
(* Interprets an hypothesis name *)
let interp_occurrences ist occs =
@@ -450,7 +448,7 @@ let default_fresh_id = Id.of_string "H"
let interp_fresh_id ist env sigma l =
let extract_ident ist env sigma id =
- try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma)
+ try try_interp_ltac_var (coerce_to_ident_not_fresh sigma)
ist (Some (env,sigma)) (make id)
with Not_found -> id in
let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in
@@ -473,7 +471,7 @@ let interp_fresh_id ist env sigma l =
(* Extract the uconstr list from lfun *)
let extract_ltac_constr_context ist env sigma =
let add_uconstr id v map =
- try Id.Map.add id (coerce_to_uconstr env v) map
+ try Id.Map.add id (coerce_to_uconstr v) map
with CannotCoerceTo _ -> map
in
let add_constr id v map =
@@ -642,7 +640,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
(try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
- error_global_not_found (make ?loc @@ qualid_of_ident id))
+ error_global_not_found (qualid_of_ident ?loc id))
| Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
| Inr c -> Inr (interp_typed_pattern ist env sigma c) in
interp_occurrences ist occs, p
@@ -689,13 +687,11 @@ let interp_may_eval f ist env sigma = function
| ConstrContext ({loc;v=s},c) ->
(try
let (sigma,ic) = f ist env sigma c in
- let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
+ let ctxt = try_interp_ltac_var coerce_to_constr_context ist (Some (env, sigma)) (make ?loc s) in
let ctxt = EConstr.Unsafe.to_constr ctxt in
- let evdref = ref sigma in
- let ic = EConstr.Unsafe.to_constr ic in
+ let ic = EConstr.Unsafe.to_constr ic in
let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
- let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
- !evdref , c
+ Typing.solve_evars env sigma (EConstr.of_constr c)
with
| Not_found ->
user_err ?loc ~hdr:"interp_may_eval"
@@ -800,7 +796,7 @@ and interp_or_and_intro_pattern ist env sigma = function
and interp_intro_pattern_list_as_list ist env sigma = function
| [{loc;v=IntroNaming (IntroIdentifier id)}] as l ->
- (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
+ (try sigma, coerce_to_intro_pattern_list ?loc sigma (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ ->
List.fold_left_map (interp_intro_pattern ist env) sigma l)
| l -> List.fold_left_map (interp_intro_pattern ist env) sigma l
@@ -843,7 +839,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function
| AnonHyp n -> AnonHyp n
| NamedHyp id ->
try try_interp_ltac_var
- (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id)
+ (coerce_to_decl_or_quant_hyp sigma) ist (Some (env,sigma)) (make id)
with Not_found -> NamedHyp id
let interp_binding ist env sigma {loc;v=(b,c)} =
@@ -926,7 +922,7 @@ let interp_destruction_arg ist gl arg =
if Tactics.is_quantified_hypothesis id gl then
keep,ElimOnIdent (make ?loc id)
else
- let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (make ?loc @@ Ident id,None))) in
+ let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (qualid_of_ident ?loc id,None))) in
let f env sigma =
let (sigma,c) = interp_open_constr ist env sigma c in
(sigma, (c,NoBindings))
@@ -1126,17 +1122,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias (loc,(s,l)) ->
- let (ids, body) = Tacenv.interp_alias s in
+ let alias = Tacenv.interp_alias s in
let (>>=) = Ftactic.bind in
let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
let tac l =
let addvar x v accu = Id.Map.add x v accu in
- let lfun = List.fold_right2 addvar ids l ist.lfun in
+ let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
let ist = {
lfun = lfun;
extra = TacStore.set ist.extra f_trace trace; } in
- val_interp ist body >>= fun v ->
+ val_interp ist alias.Tacenv.alias_body >>= fun v ->
Ftactic.lift (tactic_of_value ist v)
in
let tac =
@@ -1148,7 +1144,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
some more elaborate solution will have to be used. *)
in
let tac =
- let len1 = List.length ids in
+ let len1 = List.length alias.Tacenv.alias_args in
let len2 = List.length l in
if len1 = len2 then tac
else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
@@ -1308,7 +1304,7 @@ and tactic_of_value ist vle =
match appl with
UnnamedAppl -> "An unnamed user-defined tactic"
| GlbAppl apps ->
- let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in
+ let nms = List.map (fun (kn,_) -> string_of_qualid (Tacenv.shortest_qualid_of_tactic kn)) apps in
match nms with
[] -> assert false
| kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *)
@@ -1748,15 +1744,15 @@ and interp_atomic ist tac : unit Proofview.tactic =
| AllOccurrences | NoOccurrences -> true
| _ -> false
in
- let c_interp patvars sigma =
+ let c_interp patvars env sigma =
let lfun' = Id.Map.fold (fun id c lfun ->
Id.Map.add id (Value.of_constr c) lfun)
patvars ist.lfun
in
let ist = { ist with lfun = lfun' } in
if is_onhyps && is_onconcl
- then interp_type ist (pf_env gl) sigma c
- else interp_constr ist (pf_env gl) sigma c
+ then interp_type ist env sigma c
+ else interp_constr ist env sigma c
in
Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
end
@@ -1769,11 +1765,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
let sigma = project gl in
let op = interp_typed_pattern ist env sigma op in
let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in
- let c_interp patvars sigma =
+ let c_interp patvars env sigma =
let lfun' = Id.Map.fold (fun id c lfun ->
Id.Map.add id (Value.of_constr c) lfun)
patvars ist.lfun
in
+ let env = ensure_freshness env in
let ist = { ist with lfun = lfun' } in
try
interp_constr ist env sigma c
@@ -1861,6 +1858,31 @@ let eval_tactic_ist ist t =
Proofview.tclLIFT db_initialize <*>
interp_tactic ist t
+(** FFI *)
+
+module Value = struct
+
+ include Taccoerce.Value
+
+ let of_closure ist tac =
+ let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
+ of_tacvalue closure
+
+ (** Apply toplevel tactic values *)
+ let apply (f : value) (args: value list) =
+ let fold arg (i, vars, lfun) =
+ let id = Id.of_string ("x" ^ string_of_int i) in
+ let x = Reference (ArgVar CAst.(make id)) in
+ (succ i, x :: vars, Id.Map.add id arg lfun)
+ in
+ let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
+ let lfun = Id.Map.add (Id.of_string "F") f lfun in
+ let ist = { (default_ist ()) with lfun = lfun; } in
+ let tac = TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+ eval_tactic_ist ist tac
+
+end
+
(* globalization + interpretation *)
@@ -2009,7 +2031,8 @@ let interp_redexp env sigma r =
let _ =
let eval lfun env sigma ty tac =
- let ist = { lfun = lfun; extra = TacStore.empty; } in
+ let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
+ let ist = { lfun = lfun; extra; } in
let tac = interp_tactic ist tac in
let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
(EConstr.of_constr c, sigma)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 21:15:23 +0000