author | haftmann |
Mon, 12 Oct 2020 07:25:38 +0000 | |
changeset 72450 | 24bd1316eaae |
parent 72436 | d62d84634b06 |
child 74561 | 8e6c973003c8 |
permissions | -rw-r--r-- |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
1 |
(* Title: HOL/Eisbach/method_closure.ML |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
2 |
Author: Daniel Matichuk, NICTA/UNSW |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
3 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
4 |
Facilities for treating method syntax as a closure, with abstraction |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
5 |
over terms, facts and other methods. |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
6 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
7 |
The 'method' command allows to define new proof methods by combining |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
8 |
existing ones with their usual syntax. |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
9 |
*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
10 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
11 |
signature METHOD_CLOSURE = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
12 |
sig |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
13 |
val apply_method: Proof.context -> string -> term list -> thm list list -> |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
14 |
(Proof.context -> Method.method) list -> Proof.context -> thm list -> context_tactic |
61910 | 15 |
val method: binding -> (binding * typ option * mixfix) list -> binding list -> |
16 |
binding list -> binding list -> Token.src -> local_theory -> string * local_theory |
|
17 |
val method_cmd: binding -> (binding * string option * mixfix) list -> binding list -> |
|
18 |
binding list -> binding list -> Token.src -> local_theory -> string * local_theory |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
19 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
20 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
21 |
structure Method_Closure: METHOD_CLOSURE = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
22 |
struct |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
23 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
24 |
(* auxiliary data for method definition *) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
25 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
26 |
structure Method_Definition = Proof_Data |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
27 |
( |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
28 |
type T = |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
29 |
(Proof.context -> Method.method) Symtab.table * (*dynamic methods*) |
63186
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
30 |
(term list -> Proof.context -> Method.method) Symtab.table (*recursive methods*); |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
31 |
fun init _ : T = (Symtab.empty, Symtab.empty); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
32 |
); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
33 |
|
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
34 |
fun lookup_dynamic_method ctxt full_name = |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
35 |
(case Symtab.lookup (#1 (Method_Definition.get ctxt)) full_name of |
62074 | 36 |
SOME m => m ctxt |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
37 |
| NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
38 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
39 |
val update_dynamic_method = Method_Definition.map o apfst o Symtab.update; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
40 |
|
63186
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
41 |
fun get_recursive_method full_name ts ctxt = |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
42 |
(case Symtab.lookup (#2 (Method_Definition.get ctxt)) full_name of |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
43 |
SOME m => m ts ctxt |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
44 |
| NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name)); |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
45 |
|
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
46 |
val put_recursive_method = Method_Definition.map o apsnd o Symtab.update; |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
47 |
|
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
48 |
|
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
49 |
(* stored method closures *) |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
50 |
|
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
51 |
type closure = {vars: term list, named_thms: string list, methods: string list, body: Method.text}; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
52 |
|
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
53 |
structure Data = Generic_Data |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
54 |
( |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
55 |
type T = closure Symtab.table; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
56 |
val empty: T = Symtab.empty; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
57 |
val extend = I; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
58 |
fun merge data : T = Symtab.merge (K true) data; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
59 |
); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
60 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
61 |
fun get_closure ctxt name = |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
62 |
(case Symtab.lookup (Data.get (Context.Proof ctxt)) name of |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
63 |
SOME closure => closure |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
64 |
| NONE => error ("Unknown Eisbach method: " ^ quote name)); |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
65 |
|
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
66 |
fun put_closure binding (closure: closure) lthy = |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
67 |
let |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
68 |
val name = Local_Theory.full_name lthy binding; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
69 |
in |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
70 |
lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
71 |
Data.map |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
72 |
(Symtab.update (name, |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
73 |
{vars = map (Morphism.term phi) (#vars closure), |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
74 |
named_thms = #named_thms closure, |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
75 |
methods = #methods closure, |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
76 |
body = (Method.map_source o map) (Token.transform phi) (#body closure)}))) |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
77 |
end; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
78 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
79 |
|
63527 | 80 |
(* instantiate and evaluate method text *) |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
81 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
82 |
fun method_instantiate vars body ts ctxt = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
83 |
let |
62076
1add21f7cabc
proper Pattern.match and corresponding Envir.subst_term, instead of Envir.norm_term of unify-family;
wenzelm
parents:
62074
diff
changeset
|
84 |
val thy = Proof_Context.theory_of ctxt; |
1add21f7cabc
proper Pattern.match and corresponding Envir.subst_term, instead of Envir.norm_term of unify-family;
wenzelm
parents:
62074
diff
changeset
|
85 |
val subst = fold (Pattern.match thy) (vars ~~ ts) (Vartab.empty, Vartab.empty); |
1add21f7cabc
proper Pattern.match and corresponding Envir.subst_term, instead of Envir.norm_term of unify-family;
wenzelm
parents:
62074
diff
changeset
|
86 |
val morphism = Morphism.term_morphism "method_instantiate" (Envir.subst_term subst); |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
87 |
val body' = (Method.map_source o map) (Token.transform morphism) body; |
63527 | 88 |
in Method.evaluate_runtime body' ctxt end; |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
89 |
|
62074 | 90 |
|
91 |
||
92 |
(** apply method closure **) |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
93 |
|
63186
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
94 |
fun recursive_method full_name vars body ts = |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
95 |
let val m = method_instantiate vars body |
63186
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
96 |
in put_recursive_method (full_name, m) #> m ts end; |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
97 |
|
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
98 |
fun apply_method ctxt method_name terms facts methods = |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
99 |
let |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
100 |
fun declare_facts (name :: names) (fact :: facts) = |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
101 |
fold (Context.proof_map o Named_Theorems.add_thm name) fact |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
102 |
#> declare_facts names facts |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
103 |
| declare_facts _ [] = I |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
104 |
| declare_facts [] (_ :: _) = error ("Excessive facts for method " ^ quote method_name); |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
105 |
val {vars, named_thms, methods = method_args, body} = get_closure ctxt method_name; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
106 |
in |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
107 |
declare_facts named_thms facts |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
108 |
#> fold update_dynamic_method (method_args ~~ methods) |
63186
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
109 |
#> recursive_method method_name vars body terms |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
110 |
end; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
111 |
|
61919 | 112 |
|
113 |
||
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
114 |
(** define method closure **) |
61919 | 115 |
|
116 |
local |
|
117 |
||
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
118 |
fun setup_local_method binding lthy = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
119 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
120 |
val full_name = Local_Theory.full_name lthy binding; |
62074 | 121 |
fun dynamic_method ctxt = lookup_dynamic_method ctxt full_name; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
122 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
123 |
lthy |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
124 |
|> update_dynamic_method (full_name, K Method.fail) |
62074 | 125 |
|> Method.local_setup binding (Scan.succeed dynamic_method) "(internal)" |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
126 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
127 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
128 |
fun check_named_thm ctxt binding = |
61919 | 129 |
let |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
130 |
val bname = Binding.name_of binding; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
131 |
val pos = Binding.pos_of binding; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
132 |
val full_name = Named_Theorems.check ctxt (bname, pos); |
61919 | 133 |
val parser: Method.modifier parser = |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
134 |
Args.$$$ bname -- Args.colon |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
135 |
>> K {init = I, attribute = Named_Theorems.add full_name, pos = pos}; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
136 |
in (full_name, parser) end; |
61919 | 137 |
|
61918 | 138 |
fun parse_term_args args = |
139 |
Args.context :|-- (fn ctxt => |
|
140 |
let |
|
141 |
val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt; |
|
142 |
||
143 |
fun parse T = |
|
144 |
(if T = propT then Syntax.parse_prop ctxt' else Syntax.parse_term ctxt') |
|
145 |
#> Type.constraint (Type_Infer.paramify_vars T); |
|
146 |
||
147 |
fun do_parse' T = |
|
148 |
Parse_Tools.name_term >> Parse_Tools.parse_val_cases (parse T); |
|
149 |
||
150 |
fun do_parse (Var (_, T)) = do_parse' T |
|
151 |
| do_parse (Free (_, T)) = do_parse' T |
|
152 |
| do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt' t); |
|
153 |
||
154 |
fun rep [] x = Scan.succeed [] x |
|
155 |
| rep (t :: ts) x = (do_parse t ::: rep ts) x; |
|
156 |
||
157 |
fun check ts = |
|
158 |
let |
|
159 |
val (ts, fs) = split_list ts; |
|
160 |
val ts' = Syntax.check_terms ctxt' ts |> Variable.polymorphic ctxt'; |
|
161 |
val _ = ListPair.app (fn (f, t) => f t) (fs, ts'); |
|
162 |
in ts' end; |
|
163 |
in Scan.lift (rep args) >> check end); |
|
164 |
||
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
165 |
fun parse_method_args method_args = |
61919 | 166 |
let |
167 |
fun bind_method (name, text) ctxt = |
|
168 |
let |
|
63527 | 169 |
val method = Method.evaluate_runtime text; |
61919 | 170 |
val inner_update = method o update_dynamic_method (name, K (method ctxt)); |
171 |
in update_dynamic_method (name, inner_update) ctxt end; |
|
172 |
||
173 |
fun rep [] x = Scan.succeed [] x |
|
63527 | 174 |
| rep (m :: ms) x = ((Method.text_closure >> pair m) ::: rep ms) x; |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
175 |
in rep method_args >> fold bind_method end; |
61919 | 176 |
|
61899 | 177 |
fun gen_method add_fixes name vars uses declares methods source lthy = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
178 |
let |
61898 | 179 |
val (uses_internal, lthy1) = lthy |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
180 |
|> Proof_Context.concealed |
72450 | 181 |
|> Local_Theory.begin_nested |
72436
d62d84634b06
direct exit to theory when ending nested target on theory target
haftmann
parents:
72433
diff
changeset
|
182 |
|-> Proof_Context.private_scope |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
183 |
|> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
184 |
|> Config.put Method.old_section_parser true |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
185 |
|> fold setup_local_method methods |
70182
ca9dfa7ee3bd
backed out experimental b67bab2b132c, which slipped in accidentally
haftmann
parents:
70177
diff
changeset
|
186 |
|> fold_map (fn b => Named_Theorems.declare b "") uses; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
187 |
|
60407 | 188 |
val (term_args, lthy2) = lthy1 |
60469 | 189 |
|> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
190 |
|
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
191 |
val (named_thms, modifiers) = map (check_named_thm lthy2) (declares @ uses) |> split_list; |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
192 |
|
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
193 |
val method_args = map (Local_Theory.full_name lthy2) methods; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
194 |
|
62073 | 195 |
fun parser args meth = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
196 |
apfst (Config.put_generic Method.old_section_parser true) #> |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
197 |
(parse_term_args args -- |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
198 |
parse_method_args method_args --| |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
199 |
(Scan.depend (fn context => |
61900 | 200 |
Scan.succeed (fold Named_Theorems.clear uses_internal context, ())) -- |
62073 | 201 |
Method.sections modifiers)) >> (fn (ts, decl) => meth ts o decl); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
202 |
|
63186
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
203 |
val full_name = Local_Theory.full_name lthy name; |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
204 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
205 |
val lthy3 = lthy2 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
206 |
|> Method.local_setup (Binding.make (Binding.name_of name, Position.none)) |
63186
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
207 |
(parser term_args (get_recursive_method full_name)) "(internal)" |
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
208 |
|> put_recursive_method (full_name, fn _ => fn _ => Method.fail); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
209 |
|
62078
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
62076
diff
changeset
|
210 |
val (text, src) = |
63527 | 211 |
Method.read_closure (Config.put Proof_Context.dynamic_facts_dummy true lthy3) source; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
212 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
213 |
val morphism = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
214 |
Variable.export_morphism lthy3 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
215 |
(lthy |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
216 |
|> Proof_Context.transfer (Proof_Context.theory_of lthy3) |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
217 |
|> fold Token.declare_maxidx src |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
218 |
|> Variable.declare_maxidx (Variable.maxidx_of lthy3)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
219 |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
220 |
val text' = (Method.map_source o map) (Token.transform morphism) text; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
221 |
val term_args' = map (Morphism.term morphism) term_args; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
222 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
223 |
lthy3 |
72450 | 224 |
|> Local_Theory.end_nested |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
225 |
|> Proof_Context.restore_naming lthy |
62070
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
226 |
|> put_closure name |
b13b98a4d5f8
more realistic Eisbach method invocation from ML;
wenzelm
parents:
62069
diff
changeset
|
227 |
{vars = term_args', named_thms = named_thms, methods = method_args, body = text'} |
63527 | 228 |
|> Method.local_setup name |
63185
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62795
diff
changeset
|
229 |
(Args.context :|-- (fn ctxt => |
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62795
diff
changeset
|
230 |
let val {body, vars, ...} = get_closure ctxt full_name in |
63186
dc221b8945f2
allow multiple recursive methods to co-exist in order to support mutual recursion;
matichuk <daniel.matichuk@nicta.com.au>
parents:
63185
diff
changeset
|
231 |
parser vars (recursive_method full_name vars body) end)) "" |
63185
08369e33c185
apply current morphism to method text before evaluating;
matichuk <daniel.matichuk@nicta.com.au>
parents:
62795
diff
changeset
|
232 |
|> pair full_name |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
233 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
234 |
|
61898 | 235 |
in |
236 |
||
61899 | 237 |
val method = gen_method Proof_Context.add_fixes; |
238 |
val method_cmd = gen_method Proof_Context.add_fixes_cmd; |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
239 |
|
61898 | 240 |
end; |
241 |
||
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
242 |
val _ = |
69593 | 243 |
Outer_Syntax.local_theory \<^command_keyword>\<open>method\<close> "Eisbach method definition" |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
244 |
(Parse.binding -- Parse.for_fixes -- |
69593 | 245 |
((Scan.optional (\<^keyword>\<open>methods\<close> |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) -- |
246 |
(Scan.optional (\<^keyword>\<open>uses\<close> |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) -- |
|
247 |
(Scan.optional (\<^keyword>\<open>declares\<close> |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) -- |
|
248 |
Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.args1 (K true)) >> |
|
61898 | 249 |
(fn ((((name, vars), (methods, uses)), declares), src) => |
61910 | 250 |
#2 o method_cmd name vars uses declares methods src)); |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
60553
diff
changeset
|
251 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
252 |
end; |