22 val exec: (unit -> unit) -> Context.generic -> Context.generic |
22 val exec: (unit -> unit) -> Context.generic -> Context.generic |
23 val stored_thms: thm list ref |
23 val stored_thms: thm list ref |
24 val ml_store_thm: string * thm -> unit |
24 val ml_store_thm: string * thm -> unit |
25 val ml_store_thms: string * thm list -> unit |
25 val ml_store_thms: string * thm list -> unit |
26 val add_keywords: string list -> unit |
26 val add_keywords: string list -> unit |
27 val inline_antiq: string -> |
27 type antiq = |
28 (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit |
28 {struct_name: string, background: Proof.context} -> |
29 val value_antiq: string -> |
29 (Proof.context -> string * string) * Proof.context |
30 (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit |
30 val add_antiq: string -> |
31 val proj_value_antiq: string -> (Context.generic * Args.T list -> |
31 (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) -> unit |
32 (string * string * string) * (Context.generic * Args.T list)) -> unit |
|
33 val trace: bool ref |
32 val trace: bool ref |
34 val eval: bool -> Position.T -> string -> unit |
33 val eval: bool -> Position.T -> string -> unit |
35 val eval_file: Path.T -> unit |
34 val eval_file: Path.T -> unit |
36 val eval_in: Context.generic option -> bool -> Position.T -> string -> unit |
35 val eval_in: Context.generic option -> bool -> Position.T -> string -> unit |
37 val evaluate: (string -> unit) * (string -> 'b) -> bool -> |
36 val evaluate: (string -> unit) * (string -> 'b) -> bool -> |
74 fun ml_store_thm (name, th) = ml_store "hd" (name, [th]); |
73 fun ml_store_thm (name, th) = ml_store "hd" (name, [th]); |
75 |
74 |
76 fun bind_thm (name, thm) = ml_store_thm (name, Drule.standard thm); |
75 fun bind_thm (name, thm) = ml_store_thm (name, Drule.standard thm); |
77 fun bind_thms (name, thms) = ml_store_thms (name, map Drule.standard thms); |
76 fun bind_thms (name, thms) = ml_store_thms (name, map Drule.standard thms); |
78 |
77 |
|
78 fun thm name = ProofContext.get_thm (the_local_context ()) name; |
|
79 fun thms name = ProofContext.get_thms (the_local_context ()) name; |
|
80 |
79 |
81 |
80 |
82 |
81 (** ML antiquotations **) |
83 (** ML antiquotations **) |
82 |
84 |
83 (* maintain keywords *) |
85 (* antiquotation keywords *) |
|
86 |
|
87 local |
84 |
88 |
85 val global_lexicon = ref Scan.empty_lexicon; |
89 val global_lexicon = ref Scan.empty_lexicon; |
|
90 |
|
91 in |
86 |
92 |
87 fun add_keywords keywords = CRITICAL (fn () => |
93 fun add_keywords keywords = CRITICAL (fn () => |
88 change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords))); |
94 change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords))); |
89 |
95 |
90 |
96 fun get_lexicon () = ! global_lexicon; |
91 (* maintain commands *) |
97 |
92 |
98 end; |
93 datatype antiq = Inline of string | ProjValue of string * string * string; |
99 |
|
100 |
|
101 (* antiquotation commands *) |
|
102 |
|
103 type antiq = |
|
104 {struct_name: string, background: Proof.context} -> |
|
105 (Proof.context -> string * string) * Proof.context; |
|
106 |
|
107 local |
|
108 |
94 val global_parsers = ref (Symtab.empty: |
109 val global_parsers = ref (Symtab.empty: |
95 (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table); |
110 (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table); |
96 |
111 |
97 local |
112 in |
98 |
113 |
99 fun add_item kind name scan = CRITICAL (fn () => |
114 fun add_antiq name scan = CRITICAL (fn () => |
100 change global_parsers (fn tab => |
115 change global_parsers (fn tab => |
101 (if not (Symtab.defined tab name) then () |
116 (if not (Symtab.defined tab name) then () |
102 else warning ("Redefined ML antiquotation: " ^ quote name); |
117 else warning ("Redefined ML antiquotation: " ^ quote name); |
103 Symtab.update (name, scan >> kind) tab))); |
118 Symtab.update (name, scan) tab))); |
104 |
119 |
105 in |
120 fun antiquotation src ctxt = |
106 |
|
107 val inline_antiq = add_item Inline; |
|
108 val proj_value_antiq = add_item ProjValue; |
|
109 fun value_antiq name scan = proj_value_antiq name (scan >> (fn (a, s) => (a, s, ""))); |
|
110 |
|
111 end; |
|
112 |
|
113 |
|
114 (* command syntax *) |
|
115 |
|
116 fun syntax scan src = |
|
117 #1 (Args.context_syntax "ML antiquotation" scan src (the_local_context ())); |
|
118 |
|
119 fun command src = |
|
120 let val ((name, _), pos) = Args.dest_src src in |
121 let val ((name, _), pos) = Args.dest_src src in |
121 (case Symtab.lookup (! global_parsers) name of |
122 (case Symtab.lookup (! global_parsers) name of |
122 NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) |
123 NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) |
123 | SOME scan => syntax scan src) |
124 | SOME scan => Args.context_syntax "ML antiquotation" scan src ctxt) |
124 end; |
125 end; |
125 |
126 |
126 |
127 end; |
127 (* outer syntax *) |
128 |
128 |
129 |
129 structure T = OuterLex; |
130 (* parsing and evaluation *) |
|
131 |
|
132 local |
|
133 |
130 structure P = OuterParse; |
134 structure P = OuterParse; |
131 |
135 |
132 val antiq = |
136 val antiq = |
133 P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof) |
137 P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof) |
134 >> (fn ((x, pos), y) => Args.src ((x, y), pos)); |
138 >> (fn ((x, pos), y) => Args.src ((x, y), pos)); |
135 |
139 |
136 |
140 fun eval_antiquotes struct_name (txt, pos) opt_ctxt = |
137 (* input/output wrappers *) |
141 let |
138 |
142 val ants = Antiquote.scan_antiquotes (txt, pos); |
139 local |
143 val ((ml_env, ml_body), opt_ctxt') = |
140 |
144 if not (exists Antiquote.is_antiq ants) then (("", Symbol.escape txt), opt_ctxt) |
141 fun eval_antiquotes struct_name txt_pos = |
145 else |
142 let |
146 let |
143 val lex = ! global_lexicon; |
147 val ctxt = |
144 val ants = Antiquote.scan_antiquotes txt_pos; |
148 (case opt_ctxt of |
145 |
149 NONE => error ("Unknown context -- cannot expand ML antiquotations" ^ |
146 fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) |
150 Position.str_of pos) |
147 | expand (Antiquote.Antiq x) names = |
151 | SOME context => Context.proof_of context); |
148 (case command (Antiquote.scan_arguments lex antiq x) of |
152 |
149 Inline s => (("", s), names) |
153 val lex = get_lexicon (); |
150 | ProjValue (a, s, f) => |
154 fun no_decl _ = ("", ""); |
151 let |
155 |
152 val a' = if ML_Syntax.is_identifier a then a else "val"; |
156 fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state) |
153 val ([b], names') = Name.variants [a'] names; |
157 | expand (Antiquote.Antiq x) (scope, background) = |
154 val binding = "val " ^ b ^ " = " ^ s ^ ";\n"; |
158 let |
155 val value = |
159 val context = Stack.top scope; |
156 if f = "" then struct_name ^ "." ^ b |
160 val (f, context') = antiquotation (Antiquote.scan_arguments lex antiq x) context; |
157 else "(" ^ f ^ " " ^ struct_name ^ "." ^ b ^ ")"; |
161 val (decl, background') = f {background = background, struct_name = struct_name}; |
158 in ((binding, value), names') end); |
162 in (decl, (Stack.map_top (K context') scope, background')) end |
159 |
163 | expand (Antiquote.Open _) (scope, background) = |
160 val (decls, body) = |
164 (no_decl, (Stack.push scope, background)) |
161 fold_map expand ants ML_Syntax.reserved |
165 | expand (Antiquote.Close _) (scope, background) = |
162 |> #1 |> split_list |> pairself implode; |
166 (no_decl, (Stack.pop scope, background)); |
163 in ("structure " ^ struct_name ^ " =\nstruct\n" ^ decls ^ "end;", body) end; |
167 |
|
168 val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt); |
|
169 val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself implode; |
|
170 in (ml, SOME (Context.Proof ctxt')) end; |
|
171 in (("structure " ^ struct_name ^ " =\nstruct\n" ^ ml_env ^ "end;", ml_body), opt_ctxt') end; |
164 |
172 |
165 in |
173 in |
166 |
174 |
167 val trace = ref false; |
175 val trace = ref false; |
168 |
176 |
169 fun eval_wrapper pr verbose pos txt = |
177 fun eval_wrapper pr verbose pos txt = |
170 let |
178 let |
171 val struct_name = |
179 val struct_name = |
172 if Multithreading.available then "Isabelle" ^ serial_string () |
180 if Multithreading.available then "Isabelle" ^ serial_string () |
173 else "Isabelle"; |
181 else "Isabelle"; |
174 val (txt1, txt2) = eval_antiquotes struct_name (txt, pos); |
182 val ((env, body), env_ctxt) = eval_antiquotes struct_name (txt, pos) (Context.thread_data ()); |
175 val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else (); |
183 val _ = if ! trace then tracing (cat_lines [env, body]) else (); |
176 fun eval p = |
184 fun eval_raw p = |
177 use_text (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr; |
185 use_text (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr; |
178 in |
186 in |
179 eval Position.none false txt1; |
187 Context.setmp_thread_data env_ctxt (fn () => eval_raw Position.none false env) (); |
180 NAMED_CRITICAL "ML" (fn () => eval pos verbose txt2); (* FIXME non-critical with local ML env *) |
188 NAMED_CRITICAL "ML" (fn () => eval_raw pos verbose body); (* FIXME non-critical with local ML env *) |
181 forget_structure struct_name |
189 forget_structure struct_name |
182 end; |
190 end; |
183 |
191 |
184 end; |
192 end; |
185 |
193 |
202 fun expression pos bind body txt = |
210 fun expression pos bind body txt = |
203 exec (fn () => eval false pos |
211 exec (fn () => eval false pos |
204 ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^ |
212 ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^ |
205 " end (ML_Context.the_generic_context ())));")); |
213 " end (ML_Context.the_generic_context ())));")); |
206 |
214 |
207 |
|
208 (* basic antiquotations *) |
|
209 |
|
210 fun context x = (Scan.state >> Context.proof_of) x; |
|
211 |
|
212 local |
|
213 |
|
214 val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()")); |
|
215 |
|
216 val _ = inline_antiq "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) => |
|
217 ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))); |
|
218 |
|
219 val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); |
|
220 val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
221 val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
222 |
|
223 val _ = value_antiq "ctyp" (Args.typ >> (fn T => |
|
224 ("ctyp", |
|
225 "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)))); |
|
226 |
|
227 val _ = value_antiq "cterm" (Args.term >> (fn t => |
|
228 ("cterm", |
|
229 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
|
230 |
|
231 val _ = value_antiq "cprop" (Args.prop >> (fn t => |
|
232 ("cprop", |
|
233 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
|
234 |
|
235 fun type_ syn = (context -- Scan.lift Args.name >> (fn (ctxt, c) => |
|
236 #1 (Term.dest_Type (ProofContext.read_tyname ctxt c)) |
|
237 |> syn ? Sign.base_name |
|
238 |> ML_Syntax.print_string)); |
|
239 |
|
240 val _ = inline_antiq "type_name" (type_ false); |
|
241 val _ = inline_antiq "type_syntax" (type_ true); |
|
242 |
|
243 fun const syn = context -- Scan.lift Args.name >> (fn (ctxt, c) => |
|
244 #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c)) |
|
245 |> syn ? ProofContext.const_syntax_name ctxt |
|
246 |> ML_Syntax.print_string); |
|
247 |
|
248 val _ = inline_antiq "const_name" (const false); |
|
249 val _ = inline_antiq "const_syntax" (const true); |
|
250 |
|
251 val _ = inline_antiq "const" |
|
252 (context -- Scan.lift Args.name -- |
|
253 Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
|
254 >> (fn ((ctxt, c), Ts) => |
|
255 let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c) |
|
256 in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end)); |
|
257 |
|
258 in val _ = () end; |
|
259 |
|
260 |
|
261 |
|
262 (** fact references **) |
|
263 |
|
264 fun thm name = ProofContext.get_thm (the_local_context ()) name; |
|
265 fun thms name = ProofContext.get_thms (the_local_context ()) name; |
|
266 |
|
267 |
|
268 local |
|
269 |
|
270 fun print_interval (Facts.FromTo arg) = |
|
271 "Facts.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg |
|
272 | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i |
|
273 | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i; |
|
274 |
|
275 fun thm_antiq kind get get_name = value_antiq kind |
|
276 (context -- Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel) |
|
277 >> (fn (ctxt, ((name, pos), sel)) => |
|
278 let |
|
279 val _ = get ctxt (Facts.Named ((name, pos), sel)); |
|
280 val txt = |
|
281 "(Facts.Named ((" ^ ML_Syntax.print_string name ^ ", Position.none), " ^ |
|
282 ML_Syntax.print_option (ML_Syntax.print_list print_interval) sel ^ "))"; |
|
283 in (name, get_name ^ " (ML_Context.the_local_context ()) " ^ txt) end)); |
|
284 |
|
285 in |
|
286 |
|
287 val _ = add_keywords ["(", ")", "-", ","]; |
|
288 val _ = thm_antiq "thm" ProofContext.get_fact_single "ProofContext.get_fact_single"; |
|
289 val _ = thm_antiq "thms" ProofContext.get_fact "ProofContext.get_fact"; |
|
290 |
|
291 end; |
|
292 |
|
293 val _ = proj_value_antiq "cpat" (Scan.lift Args.name >> |
|
294 (fn name => ("cpat", |
|
295 "Thm.cterm_of (ML_Context.the_global_context ()) (Syntax.read_term \ |
|
296 \(ProofContext.set_mode ProofContext.mode_pattern (ML_Context.the_local_context ()))" |
|
297 ^ ML_Syntax.print_string name ^ ")", ""))); |
|
298 |
|
299 end; |
215 end; |
300 |
216 |
301 structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; |
217 structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; |
302 open Basic_ML_Context; |
218 open Basic_ML_Context; |