diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/quote/g_quote.ml4 | 13 | ||||
| -rw-r--r-- | plugins/quote/quote.ml | 16 |
2 files changed, 27 insertions, 2 deletions
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 808cbbf274..bdeb9844be 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -10,9 +10,22 @@ (* $Id$ *) +open Util +open Tacexpr open Quote +let make_cont k x = + let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> fst k)) in + let x = TacDynamic(dummy_loc, Pretyping.constr_in x) in + let tac = <:tactic<let cont := $k in cont $x>> in + Tacinterp.interp tac + TACTIC EXTEND quote [ "quote" ident(f) ] -> [ quote f [] ] | [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] +| [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] -> + [ gen_quote (make_cont k) c f [] ] +| [ "quote" ident(f) "[" ne_ident_list(lc) "]" + "in" constr(c) "using" tactic(k) ] -> + [ gen_quote (make_cont k) c f lc ] END diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index c2193fb489..16cc3a7316 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -438,8 +438,8 @@ let quote_terms ivs lc gl = (lp, (btree_of_array (Array.of_list (List.rev !varlist)) ivs.return_type )) -(*s actually we could "quote" a list of terms instead of the conclusion of - current goal. Ring for example needs that, but Ring doesn't use Quote +(*s actually we could "quote" a list of terms instead of a single + term. Ring for example needs that, but Ring doesn't use Quote yet. *) let quote f lid gl = @@ -454,6 +454,18 @@ let quote f lid gl = | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl +let gen_quote cont c f lid gl = + let f = pf_global gl f in + let cl = List.map (pf_global gl) lid in + let ivs = compute_ivs gl f cl in + let (p, vm) = match quote_terms ivs [c] gl with + | [p], vm -> (p,vm) + | _ -> assert false + in + match ivs.variable_lhs with + | None -> cont (mkApp (f, [| p |])) gl + | Some _ -> cont (mkApp (f, [| vm; p |])) gl + (*i Just testing ... |