56205
|
1 |
(* Title: Pure/ML/ml_antiquotations.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Miscellaneous ML antiquotations.
|
|
5 |
*)
|
|
6 |
|
|
7 |
structure ML_Antiquotations: sig end =
|
|
8 |
struct
|
|
9 |
|
|
10 |
val _ = Theory.setup
|
|
11 |
(ML_Antiquotation.inline @{binding assert}
|
|
12 |
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
|
|
13 |
|
|
14 |
ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
|
|
15 |
|
|
16 |
ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
|
|
17 |
(Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
|
|
18 |
ML_Syntax.print_string name))) #>
|
|
19 |
|
|
20 |
ML_Antiquotation.value @{binding theory}
|
|
21 |
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
|
|
22 |
(Context_Position.report ctxt pos
|
|
23 |
(Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
|
|
24 |
"Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
|
|
25 |
|| Scan.succeed "Proof_Context.theory_of ML_context") #>
|
|
26 |
|
|
27 |
ML_Antiquotation.value @{binding theory_context}
|
|
28 |
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
|
|
29 |
(Context_Position.report ctxt pos
|
|
30 |
(Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
|
|
31 |
"Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
|
|
32 |
ML_Syntax.print_string name))) #>
|
|
33 |
|
|
34 |
ML_Antiquotation.inline @{binding context} (Scan.succeed "Isabelle.ML_context") #>
|
|
35 |
|
|
36 |
ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
|
|
37 |
ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
|
|
38 |
ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
|
|
39 |
|
|
40 |
ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T =>
|
|
41 |
"Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
|
|
42 |
ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
|
|
43 |
|
|
44 |
ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t =>
|
|
45 |
"Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
|
|
46 |
ML_Syntax.atomic (ML_Syntax.print_term t))) #>
|
|
47 |
|
|
48 |
ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
|
|
49 |
"Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
|
|
50 |
ML_Syntax.atomic (ML_Syntax.print_term t))) #>
|
|
51 |
|
|
52 |
ML_Antiquotation.value @{binding cpat}
|
|
53 |
(Args.context --
|
|
54 |
Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
|
|
55 |
"Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
|
|
56 |
ML_Syntax.atomic (ML_Syntax.print_term t))));
|
|
57 |
|
|
58 |
|
|
59 |
(* type classes *)
|
|
60 |
|
|
61 |
fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
|
|
62 |
Proof_Context.read_class ctxt s
|
|
63 |
|> syn ? Lexicon.mark_class
|
|
64 |
|> ML_Syntax.print_string);
|
|
65 |
|
|
66 |
val _ = Theory.setup
|
|
67 |
(ML_Antiquotation.inline @{binding class} (class false) #>
|
|
68 |
ML_Antiquotation.inline @{binding class_syntax} (class true) #>
|
|
69 |
|
|
70 |
ML_Antiquotation.inline @{binding sort}
|
|
71 |
(Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
|
|
72 |
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
|
|
73 |
|
|
74 |
|
|
75 |
(* type constructors *)
|
|
76 |
|
|
77 |
fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
|
|
78 |
>> (fn (ctxt, (s, pos)) =>
|
|
79 |
let
|
|
80 |
val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
|
|
81 |
val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
|
|
82 |
val res =
|
|
83 |
(case try check (c, decl) of
|
|
84 |
SOME res => res
|
|
85 |
| NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
|
|
86 |
in ML_Syntax.print_string res end);
|
|
87 |
|
|
88 |
val _ = Theory.setup
|
|
89 |
(ML_Antiquotation.inline @{binding type_name}
|
|
90 |
(type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
|
|
91 |
ML_Antiquotation.inline @{binding type_abbrev}
|
|
92 |
(type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
|
|
93 |
ML_Antiquotation.inline @{binding nonterminal}
|
|
94 |
(type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
|
|
95 |
ML_Antiquotation.inline @{binding type_syntax}
|
|
96 |
(type_name "type" (fn (c, _) => Lexicon.mark_type c)));
|
|
97 |
|
|
98 |
|
|
99 |
(* constants *)
|
|
100 |
|
|
101 |
fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
|
|
102 |
>> (fn (ctxt, (s, pos)) =>
|
|
103 |
let
|
|
104 |
val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
|
|
105 |
val res = check (Proof_Context.consts_of ctxt, c)
|
|
106 |
handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
|
|
107 |
in ML_Syntax.print_string res end);
|
|
108 |
|
|
109 |
val _ = Theory.setup
|
|
110 |
(ML_Antiquotation.inline @{binding const_name}
|
|
111 |
(const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
|
|
112 |
ML_Antiquotation.inline @{binding const_abbrev}
|
|
113 |
(const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
|
|
114 |
ML_Antiquotation.inline @{binding const_syntax}
|
|
115 |
(const_name (fn (_, c) => Lexicon.mark_const c)) #>
|
|
116 |
|
|
117 |
ML_Antiquotation.inline @{binding syntax_const}
|
|
118 |
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
|
|
119 |
if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
|
|
120 |
then ML_Syntax.print_string c
|
|
121 |
else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
|
|
122 |
|
|
123 |
ML_Antiquotation.inline @{binding const}
|
|
124 |
(Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
|
|
125 |
(Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
|
|
126 |
>> (fn ((ctxt, raw_c), Ts) =>
|
|
127 |
let
|
|
128 |
val Const (c, _) =
|
|
129 |
Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
|
|
130 |
val consts = Proof_Context.consts_of ctxt;
|
|
131 |
val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
|
|
132 |
val _ = length Ts <> n andalso
|
|
133 |
error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
|
|
134 |
quote c ^ enclose "(" ")" (commas (replicate n "_")));
|
|
135 |
val const = Const (c, Consts.instance consts (c, Ts));
|
|
136 |
in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
|
|
137 |
|
|
138 |
|
|
139 |
(* outer syntax *)
|
|
140 |
|
|
141 |
fun with_keyword f =
|
|
142 |
Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
|
|
143 |
(f ((name, Thy_Header.the_keyword thy name), pos)
|
|
144 |
handle ERROR msg => error (msg ^ Position.here pos)));
|
|
145 |
|
|
146 |
val _ = Theory.setup
|
|
147 |
(ML_Antiquotation.value @{binding keyword}
|
|
148 |
(with_keyword
|
|
149 |
(fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
|
|
150 |
| ((name, SOME _), pos) =>
|
|
151 |
error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
|
|
152 |
ML_Antiquotation.value @{binding command_spec}
|
|
153 |
(with_keyword
|
|
154 |
(fn ((name, SOME kind), pos) =>
|
|
155 |
"Keyword.command_spec " ^ ML_Syntax.atomic
|
|
156 |
((ML_Syntax.print_pair
|
|
157 |
(ML_Syntax.print_pair ML_Syntax.print_string
|
|
158 |
(ML_Syntax.print_pair
|
|
159 |
(ML_Syntax.print_pair ML_Syntax.print_string
|
|
160 |
(ML_Syntax.print_list ML_Syntax.print_string))
|
|
161 |
(ML_Syntax.print_list ML_Syntax.print_string)))
|
|
162 |
ML_Syntax.print_position) ((name, kind), pos))
|
|
163 |
| ((name, NONE), pos) =>
|
|
164 |
error ("Expected command keyword " ^ quote name ^ Position.here pos))));
|
|
165 |
|
|
166 |
end;
|
|
167 |
|