author | wenzelm |
Thu, 27 Mar 2008 14:41:20 +0100 | |
changeset 26432 | 095e448b95a0 |
parent 26416 | a66f86ef7bb9 |
child 26455 | 1757a6e049f4 |
permissions | -rw-r--r-- |
24581 | 1 |
(* Title: Pure/ML/ml_context.ML |
24574 | 2 |
ID: $Id$ |
3 |
Author: Makarius |
|
4 |
||
5 |
ML context and antiquotations. |
|
6 |
*) |
|
7 |
||
8 |
signature BASIC_ML_CONTEXT = |
|
9 |
sig |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
10 |
val store_thm: string * thm -> thm |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
11 |
val store_thms: string * thm list -> thm list |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
12 |
val bind_thm: string * thm -> unit |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
13 |
val bind_thms: string * thm list -> unit |
24574 | 14 |
val thm: xstring -> thm |
15 |
val thms: xstring -> thm list |
|
25204 | 16 |
end |
24574 | 17 |
|
18 |
signature ML_CONTEXT = |
|
19 |
sig |
|
20 |
include BASIC_ML_CONTEXT |
|
21 |
val the_generic_context: unit -> Context.generic |
|
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
22 |
val the_global_context: unit -> theory |
24574 | 23 |
val the_local_context: unit -> Proof.context |
24 |
val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
25 |
val stored_thms: thm list ref |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
26 |
val ml_store_thm: string * thm -> unit |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
27 |
val ml_store_thms: string * thm list -> unit |
24574 | 28 |
val add_keywords: string list -> unit |
29 |
val inline_antiq: string -> |
|
30 |
(Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit |
|
31 |
val value_antiq: string -> |
|
32 |
(Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit |
|
33 |
val proj_value_antiq: string -> (Context.generic * Args.T list -> |
|
34 |
(string * string * string) * (Context.generic * Args.T list)) -> unit |
|
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
35 |
val eval_antiquotes_fn: (string * Position.T -> string * string) ref (* FIXME tmp *) |
24574 | 36 |
val trace: bool ref |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
37 |
val use_mltext: bool -> Position.T -> string -> Context.generic option -> unit |
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
38 |
val use_mltext_update: bool -> Position.T -> string -> Context.generic -> Context.generic |
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
39 |
val use_let: Position.T -> string -> string -> string -> Context.generic -> Context.generic |
24574 | 40 |
val use: Path.T -> unit |
25204 | 41 |
val evaluate: (string -> unit) * (string -> 'b) -> bool -> |
42 |
string * (unit -> 'a) option ref -> string -> 'a |
|
43 |
end |
|
24574 | 44 |
|
45 |
structure ML_Context: ML_CONTEXT = |
|
46 |
struct |
|
47 |
||
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
48 |
(** implicit ML context **) |
24574 | 49 |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
50 |
val the_generic_context = Context.the_thread_data; |
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
51 |
val the_global_context = Context.theory_of o the_generic_context; |
24574 | 52 |
val the_local_context = Context.proof_of o the_generic_context; |
53 |
||
54 |
fun pass_context context f x = |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
55 |
(case Context.setmp_thread_data (SOME context) (fn () => (f x, Context.thread_data ())) () of |
24574 | 56 |
(y, SOME context') => (y, context') |
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
57 |
| (_, NONE) => error "Lost context after evaluation"); |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
58 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
59 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
60 |
(* theorem bindings *) |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
61 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
62 |
val store_thms = PureThy.smart_store_thms; |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
63 |
fun store_thm (name, th) = the_single (store_thms (name, [th])); |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
64 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
65 |
val stored_thms: thm list ref = ref []; |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
66 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
67 |
fun no_ml name = |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
68 |
if name = "" then true |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
69 |
else if ML_Syntax.is_identifier name then false |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
70 |
else error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
71 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
72 |
val use_text_verbose = use_text (0, "") Output.ml_output true; |
24574 | 73 |
|
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
74 |
fun ml_store_thm (name, th) = |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
75 |
let val th' = store_thm (name, th) in |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
76 |
if no_ml name then () |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
77 |
else setmp stored_thms [th'] |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
78 |
(fn () => use_text_verbose ("val " ^ name ^ " = hd (! ML_Context.stored_thms);")) () |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
79 |
end; |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
80 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
81 |
fun ml_store_thms (name, ths) = |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
82 |
let val ths' = store_thms (name, ths) in |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
83 |
if no_ml name then () |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
84 |
else setmp stored_thms ths' |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
85 |
(fn () => use_text_verbose ("val " ^ name ^ " = ! ML_Context.stored_thms;")) () |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
86 |
end; |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
87 |
|
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
88 |
fun bind_thm (name, thm) = ml_store_thm (name, Drule.standard thm); |
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
89 |
fun bind_thms (name, thms) = ml_store_thms (name, map Drule.standard thms); |
24574 | 90 |
|
91 |
||
92 |
||
93 |
(** ML antiquotations **) |
|
94 |
||
95 |
(* maintain keywords *) |
|
96 |
||
97 |
val global_lexicon = ref Scan.empty_lexicon; |
|
98 |
||
99 |
fun add_keywords keywords = CRITICAL (fn () => |
|
100 |
change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords))); |
|
101 |
||
102 |
||
103 |
(* maintain commands *) |
|
104 |
||
105 |
datatype antiq = Inline of string | ProjValue of string * string * string; |
|
106 |
val global_parsers = ref (Symtab.empty: |
|
107 |
(Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table); |
|
108 |
||
109 |
local |
|
110 |
||
111 |
fun add_item kind name scan = CRITICAL (fn () => |
|
112 |
change global_parsers (fn tab => |
|
113 |
(if not (Symtab.defined tab name) then () |
|
114 |
else warning ("Redefined ML antiquotation: " ^ quote name); |
|
115 |
Symtab.update (name, scan >> kind) tab))); |
|
116 |
||
117 |
in |
|
118 |
||
119 |
val inline_antiq = add_item Inline; |
|
120 |
val proj_value_antiq = add_item ProjValue; |
|
121 |
fun value_antiq name scan = proj_value_antiq name (scan >> (fn (a, s) => (a, s, ""))); |
|
122 |
||
123 |
end; |
|
124 |
||
125 |
||
126 |
(* command syntax *) |
|
127 |
||
128 |
fun syntax scan src = |
|
129 |
#1 (Args.context_syntax "ML antiquotation" scan src (the_local_context ())); |
|
130 |
||
131 |
fun command src = |
|
132 |
let val ((name, _), pos) = Args.dest_src src in |
|
133 |
(case Symtab.lookup (! global_parsers) name of |
|
134 |
NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) |
|
135 |
| SOME scan => syntax scan src) |
|
136 |
end; |
|
137 |
||
138 |
||
139 |
(* outer syntax *) |
|
140 |
||
141 |
structure T = OuterLex; |
|
142 |
structure P = OuterParse; |
|
143 |
||
144 |
val antiq = |
|
145 |
P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof) |
|
146 |
>> (fn ((x, pos), y) => Args.src ((x, y), pos)); |
|
147 |
||
148 |
||
149 |
(* input/output wrappers *) |
|
150 |
||
151 |
local |
|
152 |
||
153 |
val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;"; |
|
154 |
val isabelle_struct0 = isabelle_struct ""; |
|
155 |
||
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
156 |
fun eval_antiquotes txt_pos = |
24574 | 157 |
let |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
158 |
val ants = Antiquote.scan_antiquotes txt_pos; |
24574 | 159 |
|
160 |
fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) |
|
161 |
| expand (Antiquote.Antiq x) names = |
|
162 |
(case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of |
|
163 |
Inline s => (("", s), names) |
|
164 |
| ProjValue (a, s, f) => |
|
165 |
let |
|
166 |
val a' = if ML_Syntax.is_identifier a then a else "val"; |
|
167 |
val ([b], names') = Name.variants [a'] names; |
|
168 |
val binding = "val " ^ b ^ " = " ^ s ^ ";\n"; |
|
169 |
val value = |
|
170 |
if f = "" then "Isabelle." ^ b |
|
171 |
else "(" ^ f ^ " Isabelle." ^ b ^ ")"; |
|
172 |
in ((binding, value), names') end); |
|
173 |
||
174 |
val (decls, body) = |
|
25700 | 175 |
NAMED_CRITICAL "ML" (fn () => fold_map expand ants ML_Syntax.reserved) |
24574 | 176 |
|> #1 |> split_list |> pairself implode; |
25700 | 177 |
in (isabelle_struct decls, body) end; |
24574 | 178 |
|
179 |
in |
|
180 |
||
181 |
val eval_antiquotes_fn = ref eval_antiquotes; |
|
182 |
||
183 |
val trace = ref false; |
|
184 |
||
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
185 |
fun eval_wrapper pr verbose pos txt = |
24574 | 186 |
let |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
187 |
val (txt1, txt2) = ! eval_antiquotes_fn (txt, pos); (* FIXME tmp hook *) |
24574 | 188 |
val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else (); |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
189 |
fun eval p = |
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
190 |
use_text (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr; |
25755 | 191 |
in |
192 |
NAMED_CRITICAL "ML" (fn () => |
|
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
193 |
(eval Position.none false txt1; |
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
194 |
eval pos verbose txt2; |
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
195 |
eval Position.none false isabelle_struct0)) |
25755 | 196 |
end; |
24574 | 197 |
|
198 |
end; |
|
199 |
||
200 |
||
201 |
(* ML evaluation *) |
|
202 |
||
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
203 |
fun use_mltext verbose pos txt opt_context = |
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
204 |
Context.setmp_thread_data opt_context (fn () => eval_wrapper Output.ml_output verbose pos txt) (); |
24574 | 205 |
|
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
206 |
fun use_mltext_update verbose pos txt context = |
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
207 |
#2 (pass_context context (fn () => eval_wrapper Output.ml_output verbose pos txt) ()); |
24574 | 208 |
|
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
209 |
fun use_let pos bind body txt = |
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
210 |
use_mltext_update false pos |
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
211 |
("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^ |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
212 |
" end (ML_Context.the_generic_context ())));"); |
24574 | 213 |
|
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
214 |
fun use path = eval_wrapper Output.ml_output true (Position.path path) (File.read path); |
25204 | 215 |
|
25700 | 216 |
fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () => |
25204 | 217 |
let |
218 |
val _ = r := NONE; |
|
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
219 |
val _ = eval_wrapper pr verbose Position.none |
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
220 |
("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"); |
25204 | 221 |
in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) (); |
24574 | 222 |
|
223 |
||
224 |
(* basic antiquotations *) |
|
225 |
||
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
226 |
fun context x = (Scan.state >> Context.proof_of) x; |
25142 | 227 |
|
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
228 |
local |
25142 | 229 |
|
24574 | 230 |
val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()")); |
231 |
||
25142 | 232 |
val _ = inline_antiq "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) => |
233 |
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))); |
|
234 |
||
24574 | 235 |
val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); |
236 |
val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
237 |
val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
238 |
||
239 |
val _ = value_antiq "ctyp" (Args.typ >> (fn T => |
|
240 |
("ctyp", |
|
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
241 |
"Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)))); |
24574 | 242 |
|
243 |
val _ = value_antiq "cterm" (Args.term >> (fn t => |
|
244 |
("cterm", |
|
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
245 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
24574 | 246 |
|
247 |
val _ = value_antiq "cprop" (Args.prop >> (fn t => |
|
248 |
("cprop", |
|
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
249 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
24574 | 250 |
|
25142 | 251 |
fun type_ syn = (context -- Scan.lift Args.name >> (fn (ctxt, c) => |
24695 | 252 |
#1 (Term.dest_Type (ProofContext.read_tyname ctxt c)) |
25142 | 253 |
|> syn ? Sign.base_name |
24695 | 254 |
|> ML_Syntax.print_string)); |
24574 | 255 |
|
25142 | 256 |
val _ = inline_antiq "type_name" (type_ false); |
257 |
val _ = inline_antiq "type_syntax" (type_ true); |
|
258 |
||
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
259 |
fun const syn = context -- Scan.lift Args.name >> (fn (ctxt, c) => |
25346
7f2e3292e3dd
renamed ProofContext.read_const' to ProofContext.read_const_proper;
wenzelm
parents:
25334
diff
changeset
|
260 |
#1 (Term.dest_Const (ProofContext.read_const_proper ctxt c)) |
24574 | 261 |
|> syn ? ProofContext.const_syntax_name ctxt |
262 |
|> ML_Syntax.print_string); |
|
263 |
||
264 |
val _ = inline_antiq "const_name" (const false); |
|
265 |
val _ = inline_antiq "const_syntax" (const true); |
|
266 |
||
26188 | 267 |
val _ = inline_antiq "const" |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
268 |
(context -- Scan.lift Args.name -- |
26188 | 269 |
Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
270 |
>> (fn ((ctxt, c), Ts) => |
|
271 |
let |
|
272 |
val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c); |
|
26268 | 273 |
in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end)); |
26188 | 274 |
|
25142 | 275 |
in val _ = () end; |
24574 | 276 |
|
277 |
||
26416
a66f86ef7bb9
added store_thms etc. (formerly in Thy/thm_database.ML);
wenzelm
parents:
26405
diff
changeset
|
278 |
|
24574 | 279 |
(** fact references **) |
280 |
||
26346
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
281 |
fun thm name = ProofContext.get_thm (the_local_context ()) name; |
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
282 |
fun thms name = ProofContext.get_thms (the_local_context ()) name; |
24574 | 283 |
|
284 |
||
285 |
local |
|
286 |
||
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26268
diff
changeset
|
287 |
fun print_interval (Facts.FromTo arg) = |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26268
diff
changeset
|
288 |
"Facts.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26268
diff
changeset
|
289 |
| print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26268
diff
changeset
|
290 |
| print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i; |
24574 | 291 |
|
26368
3e74b09ce466
thm_antiq: produce error at runtime, not compile time;
wenzelm
parents:
26361
diff
changeset
|
292 |
fun thm_antiq kind get get_name = value_antiq kind |
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26374
diff
changeset
|
293 |
(context -- Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel) |
26374 | 294 |
>> (fn (ctxt, ((name, pos), sel)) => |
26368
3e74b09ce466
thm_antiq: produce error at runtime, not compile time;
wenzelm
parents:
26361
diff
changeset
|
295 |
let |
26374 | 296 |
val _ = get ctxt (Facts.Named ((name, pos), sel)); |
297 |
val txt = |
|
298 |
"(Facts.Named ((" ^ ML_Syntax.print_string name ^ ", Position.none), " ^ |
|
299 |
ML_Syntax.print_option (ML_Syntax.print_list print_interval) sel ^ "))"; |
|
300 |
in (name, get_name ^ " (ML_Context.the_local_context ()) " ^ txt) end)); |
|
24574 | 301 |
|
302 |
in |
|
303 |
||
304 |
val _ = add_keywords ["(", ")", "-", ","]; |
|
26368
3e74b09ce466
thm_antiq: produce error at runtime, not compile time;
wenzelm
parents:
26361
diff
changeset
|
305 |
val _ = thm_antiq "thm" ProofContext.get_fact_single "ProofContext.get_fact_single"; |
3e74b09ce466
thm_antiq: produce error at runtime, not compile time;
wenzelm
parents:
26361
diff
changeset
|
306 |
val _ = thm_antiq "thms" ProofContext.get_fact "ProofContext.get_fact"; |
24574 | 307 |
|
308 |
end; |
|
309 |
||
24685 | 310 |
val _ = proj_value_antiq "cpat" (Scan.lift Args.name >> |
311 |
(fn name => ("cpat", |
|
26432
095e448b95a0
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26416
diff
changeset
|
312 |
"Thm.cterm_of (ML_Context.the_global_context ()) (Syntax.read_term \ |
24685 | 313 |
\(ProofContext.set_mode ProofContext.mode_pattern (ML_Context.the_local_context ()))" |
314 |
^ ML_Syntax.print_string name ^ ")", ""))); |
|
24574 | 315 |
|
316 |
end; |
|
317 |
||
318 |
structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; |
|
319 |
open Basic_ML_Context; |