author | wenzelm |
Sat, 27 Feb 2010 13:32:38 +0100 | |
changeset 35396 | 041bb8d18916 |
parent 35361 | 4c7c849b70aa |
child 35401 | bfcbab8592ba |
permissions | -rw-r--r-- |
27340 | 1 |
(* Title: Pure/ML/ml_antiquote.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Common ML antiquotations. |
|
5 |
*) |
|
6 |
||
7 |
signature ML_ANTIQUOTE = |
|
8 |
sig |
|
30513 | 9 |
val macro: string -> Proof.context context_parser -> unit |
27340 | 10 |
val variant: string -> Proof.context -> string * Proof.context |
30513 | 11 |
val inline: string -> string context_parser -> unit |
12 |
val declaration: string -> string -> string context_parser -> unit |
|
13 |
val value: string -> string context_parser -> unit |
|
27340 | 14 |
end; |
15 |
||
16 |
structure ML_Antiquote: ML_ANTIQUOTE = |
|
17 |
struct |
|
18 |
||
19 |
(** generic tools **) |
|
20 |
||
21 |
(* ML names *) |
|
22 |
||
33519 | 23 |
structure NamesData = Proof_Data |
27340 | 24 |
( |
25 |
type T = Name.context; |
|
26 |
fun init _ = ML_Syntax.reserved; |
|
27 |
); |
|
28 |
||
29 |
fun variant a ctxt = |
|
30 |
let |
|
31 |
val names = NamesData.get ctxt; |
|
32 |
val ([b], names') = Name.variants [a] names; |
|
33 |
val ctxt' = NamesData.put names' ctxt; |
|
34 |
in (b, ctxt') end; |
|
35 |
||
36 |
||
37 |
(* specific antiquotations *) |
|
38 |
||
27379 | 39 |
fun macro name scan = ML_Context.add_antiq name |
27868 | 40 |
(fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed |
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33519
diff
changeset
|
41 |
(Context.Proof ctxt, fn background => (K ("", ""), background))))); |
27379 | 42 |
|
27340 | 43 |
fun inline name scan = ML_Context.add_antiq name |
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33519
diff
changeset
|
44 |
(fn _ => scan >> (fn s => fn background => (K ("", s), background))); |
27340 | 45 |
|
46 |
fun declaration kind name scan = ML_Context.add_antiq name |
|
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33519
diff
changeset
|
47 |
(fn _ => scan >> (fn s => fn background => |
27340 | 48 |
let |
49 |
val (a, background') = variant name background; |
|
50 |
val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n"; |
|
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33519
diff
changeset
|
51 |
val body = "Isabelle." ^ a; |
27340 | 52 |
in (K (env, body), background') end)); |
53 |
||
54 |
val value = declaration "val"; |
|
55 |
||
56 |
||
57 |
||
30231 | 58 |
(** misc antiquotations **) |
27340 | 59 |
|
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27390
diff
changeset
|
60 |
structure P = OuterParse; |
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27390
diff
changeset
|
61 |
|
30721
0579dec9f8ba
@{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;
wenzelm
parents:
30524
diff
changeset
|
62 |
val _ = value "binding" |
30524 | 63 |
(Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))); |
27340 | 64 |
|
65 |
val _ = value "theory" |
|
66 |
(Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name) |
|
67 |
|| Scan.succeed "ML_Context.the_global_context ()"); |
|
68 |
||
69 |
val _ = value "theory_ref" |
|
70 |
(Scan.lift Args.name >> (fn name => |
|
71 |
"Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")") |
|
72 |
|| Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())"); |
|
73 |
||
74 |
val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()"); |
|
75 |
||
76 |
val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); |
|
77 |
val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
78 |
val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
79 |
||
27379 | 80 |
val _ = macro "let" (Args.context -- |
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27868
diff
changeset
|
81 |
Scan.lift (P.and_list1 (P.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source))) |
27379 | 82 |
>> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt))); |
83 |
||
84 |
val _ = macro "note" (Args.context :|-- (fn ctxt => |
|
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27390
diff
changeset
|
85 |
P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) => |
27379 | 86 |
((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])]))) |
30761
ac7570d80c3d
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
wenzelm
parents:
30721
diff
changeset
|
87 |
>> (fn args => #2 (ProofContext.note_thmss "" args ctxt)))); |
27379 | 88 |
|
27340 | 89 |
val _ = value "ctyp" (Args.typ >> (fn T => |
90 |
"Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))); |
|
91 |
||
92 |
val _ = value "cterm" (Args.term >> (fn t => |
|
93 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); |
|
94 |
||
95 |
val _ = value "cprop" (Args.prop >> (fn t => |
|
96 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); |
|
97 |
||
98 |
val _ = value "cpat" |
|
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27868
diff
changeset
|
99 |
(Args.context -- Scan.lift Args.name_source >> uncurry ProofContext.read_term_pattern >> (fn t => |
27340 | 100 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); |
101 |
||
102 |
||
35396 | 103 |
(* type classes *) |
104 |
||
105 |
fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) => |
|
106 |
Sign.read_class thy s |
|
107 |
|> syn ? Long_Name.base_name (* FIXME authentic syntax *) |
|
108 |
|> ML_Syntax.print_string); |
|
109 |
||
110 |
val _ = inline "class" (class false); |
|
111 |
val _ = inline "class_syntax" (class true); |
|
112 |
||
113 |
val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => |
|
114 |
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))); |
|
115 |
||
116 |
||
35361
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
117 |
(* type constructors *) |
27340 | 118 |
|
35361
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
119 |
fun type_const kind check = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
120 |
let |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
121 |
val d = #1 (Term.dest_Type (ProofContext.read_type_name ctxt false c)); |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
122 |
val decl = Sign.the_type_decl (ProofContext.theory_of ctxt) d; |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
123 |
val s = |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
124 |
(case try check (d, decl) of |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
125 |
SOME s => s |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
126 |
| NONE => error ("Not a " ^ kind ^ ": " ^ quote d)); |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
127 |
in ML_Syntax.print_string s end); |
27340 | 128 |
|
35361
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
129 |
val _ = inline "type_name" (type_const "logical type" (fn (d, Type.LogicalType _) => d)); |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
130 |
val _ = inline "type_abbrev" (type_const "type abbreviation" (fn (d, Type.Abbreviation _) => d)); |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
131 |
val _ = inline "nonterminal" (type_const "nonterminal" (fn (d, Type.Nonterminal) => d)); |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
132 |
val _ = inline "type_syntax" (type_const "type" (fn (d, _) => Long_Name.base_name d)); (* FIXME authentic syntax *) |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
133 |
|
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
134 |
|
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35262
diff
changeset
|
135 |
(* constants *) |
27340 | 136 |
|
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27868
diff
changeset
|
137 |
fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => |
27340 | 138 |
#1 (Term.dest_Const (ProofContext.read_const_proper ctxt c)) |
35262
9ea4445d2ccf
slightly more abstract syntax mark/unmark operations;
wenzelm
parents:
35255
diff
changeset
|
139 |
|> syn ? Syntax.mark_const |
27340 | 140 |
|> ML_Syntax.print_string); |
141 |
||
142 |
val _ = inline "const_name" (const false); |
|
143 |
val _ = inline "const_syntax" (const true); |
|
144 |
||
145 |
val _ = inline "const" |
|
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27868
diff
changeset
|
146 |
(Args.context -- Scan.lift Args.name_source -- Scan.optional |
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27390
diff
changeset
|
147 |
(Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
35139 | 148 |
>> (fn ((ctxt, raw_c), Ts) => |
149 |
let |
|
150 |
val Const (c, _) = ProofContext.read_const_proper ctxt raw_c; |
|
151 |
val const = Const (c, Consts.instance (ProofContext.consts_of ctxt) (c, Ts)); |
|
152 |
in ML_Syntax.atomic (ML_Syntax.print_term const) end)); |
|
27340 | 153 |
|
35111 | 154 |
val _ = inline "syntax_const" |
155 |
(Args.context -- Scan.lift Args.name >> (fn (ctxt, c) => |
|
156 |
if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c |
|
157 |
else error ("Unknown syntax const: " ^ quote c))); |
|
158 |
||
27340 | 159 |
end; |
160 |