44 (fn _ => scan >> (fn s => fn background => (K ("", s), background))); |
44 (fn _ => scan >> (fn s => fn background => (K ("", s), background))); |
45 |
45 |
46 fun declaration kind name scan = ML_Context.add_antiq name |
46 fun declaration kind name scan = ML_Context.add_antiq name |
47 (fn _ => scan >> (fn s => fn background => |
47 (fn _ => scan >> (fn s => fn background => |
48 let |
48 let |
49 val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background; |
49 val (a, background') = |
|
50 variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) background; |
50 val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n"; |
51 val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n"; |
51 val body = "Isabelle." ^ a; |
52 val body = "Isabelle." ^ a; |
52 in (K (env, body), background') end)); |
53 in (K (env, body), background') end)); |
53 |
54 |
54 val value = declaration "val"; |
55 val value = declaration "val"; |
55 |
56 |
56 |
57 |
57 |
58 |
58 (** misc antiquotations **) |
59 (** misc antiquotations **) |
59 |
60 |
60 val _ = inline "assert" |
61 val _ = Context.>> (Context.map_theory |
61 (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")"); |
|
62 |
62 |
63 val _ = inline "make_string" (Scan.succeed ml_make_string); |
63 (inline (Binding.name "assert") |
|
64 (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> |
64 |
65 |
65 val _ = value "binding" |
66 inline (Binding.name "make_string") (Scan.succeed ml_make_string) #> |
66 (Scan.lift (Parse.position Args.name) |
|
67 >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))); |
|
68 |
67 |
69 val _ = value "theory" |
68 value (Binding.name "binding") |
70 (Scan.lift Args.name >> (fn name => |
69 (Scan.lift (Parse.position Args.name) |
71 "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name) |
70 >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))) #> |
72 || Scan.succeed "ML_Context.the_global_context ()"); |
|
73 |
71 |
74 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()"); |
72 value (Binding.name "theory") |
|
73 (Scan.lift Args.name >> (fn name => |
|
74 "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name) |
|
75 || Scan.succeed "ML_Context.the_global_context ()") #> |
75 |
76 |
76 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); |
77 value (Binding.name "context") (Scan.succeed "ML_Context.the_local_context ()") #> |
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 |
78 |
80 val _ = macro "let" (Args.context -- |
79 inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> |
81 Scan.lift |
80 inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
82 (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source))) |
81 inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> |
83 >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))); |
|
84 |
82 |
85 val _ = macro "note" (Args.context :|-- (fn ctxt => |
83 macro (Binding.name "let") |
86 Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) => |
84 (Args.context -- |
87 ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])]))) |
85 Scan.lift |
88 >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))); |
86 (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source))) |
|
87 >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))) #> |
89 |
88 |
90 val _ = value "ctyp" (Args.typ >> (fn T => |
89 macro (Binding.name "note") |
91 "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))); |
90 (Args.context :|-- (fn ctxt => |
|
91 Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms |
|
92 >> (fn ((a, srcs), ths) => |
|
93 ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])]))) |
|
94 >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #> |
92 |
95 |
93 val _ = value "cterm" (Args.term >> (fn t => |
96 value (Binding.name "ctyp") (Args.typ >> (fn T => |
94 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); |
97 "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> |
95 |
98 |
96 val _ = value "cprop" (Args.prop >> (fn t => |
99 value (Binding.name "cterm") (Args.term >> (fn t => |
97 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); |
100 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
98 |
101 |
99 val _ = value "cpat" |
102 value (Binding.name "cprop") (Args.prop >> (fn t => |
100 (Args.context -- Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t => |
103 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> |
101 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); |
104 |
|
105 value (Binding.name "cpat") |
|
106 (Args.context -- |
|
107 Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t => |
|
108 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ |
|
109 ML_Syntax.atomic (ML_Syntax.print_term t))))); |
102 |
110 |
103 |
111 |
104 (* type classes *) |
112 (* type classes *) |
105 |
113 |
106 fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => |
114 fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => |
107 Proof_Context.read_class ctxt s |
115 Proof_Context.read_class ctxt s |
108 |> syn ? Lexicon.mark_class |
116 |> syn ? Lexicon.mark_class |
109 |> ML_Syntax.print_string); |
117 |> ML_Syntax.print_string); |
110 |
118 |
111 val _ = inline "class" (class false); |
119 val _ = Context.>> (Context.map_theory |
112 val _ = inline "class_syntax" (class true); |
120 (inline (Binding.name "class") (class false) #> |
|
121 inline (Binding.name "class_syntax") (class true) #> |
113 |
122 |
114 val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => |
123 inline (Binding.name "sort") |
115 ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))); |
124 (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => |
|
125 ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))))); |
116 |
126 |
117 |
127 |
118 (* type constructors *) |
128 (* type constructors *) |
119 |
129 |
120 fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source) |
130 fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source) |
126 (case try check (c, decl) of |
136 (case try check (c, decl) of |
127 SOME res => res |
137 SOME res => res |
128 | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos)); |
138 | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos)); |
129 in ML_Syntax.print_string res end); |
139 in ML_Syntax.print_string res end); |
130 |
140 |
131 val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c)); |
141 val _ = Context.>> (Context.map_theory |
132 val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)); |
142 (inline (Binding.name "type_name") |
133 val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)); |
143 (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> |
134 val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Lexicon.mark_type c)); |
144 inline (Binding.name "type_abbrev") |
|
145 (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> |
|
146 inline (Binding.name "nonterminal") |
|
147 (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> |
|
148 inline (Binding.name "type_syntax") |
|
149 (type_name "type" (fn (c, _) => Lexicon.mark_type c)))); |
135 |
150 |
136 |
151 |
137 (* constants *) |
152 (* constants *) |
138 |
153 |
139 fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source) |
154 fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source) |
142 val Const (c, _) = Proof_Context.read_const_proper ctxt false s; |
157 val Const (c, _) = Proof_Context.read_const_proper ctxt false s; |
143 val res = check (Proof_Context.consts_of ctxt, c) |
158 val res = check (Proof_Context.consts_of ctxt, c) |
144 handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos); |
159 handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos); |
145 in ML_Syntax.print_string res end); |
160 in ML_Syntax.print_string res end); |
146 |
161 |
147 val _ = inline "const_name" (const_name (fn (consts, c) => (Consts.the_type consts c; c))); |
162 val _ = Context.>> (Context.map_theory |
148 val _ = inline "const_abbrev" (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))); |
163 (inline (Binding.name "const_name") |
149 val _ = inline "const_syntax" (const_name (fn (_, c) => Lexicon.mark_const c)); |
164 (const_name (fn (consts, c) => (Consts.the_type consts c; c))) #> |
|
165 inline (Binding.name "const_abbrev") |
|
166 (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> |
|
167 inline (Binding.name "const_syntax") |
|
168 (const_name (fn (_, c) => Lexicon.mark_const c)) #> |
150 |
169 |
|
170 inline (Binding.name "syntax_const") |
|
171 (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) => |
|
172 if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) |
|
173 then ML_Syntax.print_string c |
|
174 else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))) #> |
151 |
175 |
152 val _ = inline "syntax_const" |
176 inline (Binding.name "const") |
153 (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) => |
177 (Args.context -- Scan.lift Args.name_source -- Scan.optional |
154 if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) |
178 (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
155 then ML_Syntax.print_string c |
179 >> (fn ((ctxt, raw_c), Ts) => |
156 else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))); |
180 let |
157 |
181 val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c; |
158 val _ = inline "const" |
182 val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts)); |
159 (Args.context -- Scan.lift Args.name_source -- Scan.optional |
183 in ML_Syntax.atomic (ML_Syntax.print_term const) end)))); |
160 (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
|
161 >> (fn ((ctxt, raw_c), Ts) => |
|
162 let |
|
163 val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c; |
|
164 val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts)); |
|
165 in ML_Syntax.atomic (ML_Syntax.print_term const) end)); |
|
166 |
184 |
167 end; |
185 end; |
168 |
186 |