1 (* Title: Pure/ML/ml_antiquote.ML
4 Common ML antiquotations.
7 signature ML_ANTIQUOTE =
9 val macro: string -> Proof.context context_parser -> unit
10 val variant: string -> Proof.context -> string * Proof.context
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
16 structure ML_Antiquote: ML_ANTIQUOTE =
23 structure Names = Proof_Data
25 type T = Name.context;
26 fun init _ = ML_Syntax.reserved;
31 val names = Names.get ctxt;
32 val ([b], names') = Name.variants [a] names;
33 val ctxt' = Names.put names' ctxt;
37 (* specific antiquotations *)
39 fun macro name scan = ML_Context.add_antiq name
40 (fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
41 (Context.Proof ctxt, fn background => (K ("", ""), background)))));
43 fun inline name scan = ML_Context.add_antiq name
44 (fn _ => scan >> (fn s => fn background => (K ("", s), background)));
46 fun declaration kind name scan = ML_Context.add_antiq name
47 (fn _ => scan >> (fn s => fn background =>
49 val (a, background') = variant name background;
50 val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
51 val body = "Isabelle." ^ a;
52 in (K (env, body), background') end));
54 val value = declaration "val";
58 (** misc antiquotations **)
60 val _ = inline "make_string" (Scan.succeed ml_make_string);
62 val _ = value "binding"
63 (Scan.lift (Parse.position Args.name)
64 >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
66 val _ = value "theory"
67 (Scan.lift Args.name >> (fn name => "Thy_Info.get_theory " ^ ML_Syntax.print_string name)
68 || Scan.succeed "ML_Context.the_global_context ()");
70 val _ = value "theory_ref"
71 (Scan.lift Args.name >> (fn name =>
72 "Theory.check_thy (Thy_Info.theory " ^ ML_Syntax.print_string name ^ ")")
73 || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
75 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
77 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
78 val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
79 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
81 val _ = macro "let" (Args.context --
83 (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
84 >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
86 val _ = macro "note" (Args.context :|-- (fn ctxt =>
87 Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
88 ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
89 >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
91 val _ = value "ctyp" (Args.typ >> (fn T =>
92 "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
94 val _ = value "cterm" (Args.term >> (fn t =>
95 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
97 val _ = value "cprop" (Args.prop >> (fn t =>
98 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
101 (Args.context -- Scan.lift Args.name_source >> uncurry ProofContext.read_term_pattern >> (fn t =>
102 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
107 fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
108 ProofContext.read_class ctxt s
109 |> syn ? Syntax.mark_class
110 |> ML_Syntax.print_string);
112 val _ = inline "class" (class false);
113 val _ = inline "class_syntax" (class true);
115 val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
116 ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
119 (* type constructors *)
121 fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
122 >> (fn (ctxt, (s, pos)) =>
124 val Type (c, _) = ProofContext.read_type_name_proper ctxt false s;
125 val decl = Type.the_decl (ProofContext.tsig_of ctxt) c;
127 (case try check (c, decl) of
129 | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos));
130 in ML_Syntax.print_string res end);
132 val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
133 val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
134 val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
135 val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c));
140 fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
141 >> (fn (ctxt, (s, pos)) =>
143 val Const (c, _) = ProofContext.read_const_proper ctxt false s;
144 val res = check (ProofContext.consts_of ctxt, c)
145 handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
146 in ML_Syntax.print_string res end);
148 val _ = inline "const_name" (const_name (fn (consts, c) => (Consts.the_type consts c; c)));
149 val _ = inline "const_abbrev" (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c)));
150 val _ = inline "const_syntax" (const_name (fn (_, c) => Syntax.mark_const c));
153 val _ = inline "syntax_const"
154 (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
155 if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
156 else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
158 val _ = inline "const"
159 (Args.context -- Scan.lift Args.name_source -- Scan.optional
160 (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
161 >> (fn ((ctxt, raw_c), Ts) =>
163 val Const (c, _) = ProofContext.read_const_proper ctxt true raw_c;
164 val const = Const (c, Consts.instance (ProofContext.consts_of ctxt) (c, Ts));
165 in ML_Syntax.atomic (ML_Syntax.print_term const) end));