1 (* Title: Pure/ML/ml_antiquote.ML
5 Common ML antiquotations.
8 signature ML_ANTIQUOTE =
11 (Context.generic * Args.T list -> Proof.context * (Context.generic * Args.T list)) -> unit
12 val variant: string -> Proof.context -> string * Proof.context
14 (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
15 val declaration: string -> string ->
16 (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
18 (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
21 structure ML_Antiquote: ML_ANTIQUOTE =
28 structure NamesData = ProofDataFun
30 type T = Name.context;
31 fun init _ = ML_Syntax.reserved;
36 val names = NamesData.get ctxt;
37 val ([b], names') = Name.variants [a] names;
38 val ctxt' = NamesData.put names' ctxt;
42 (* specific antiquotations *)
44 fun macro name scan = ML_Context.add_antiq name
45 (scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
46 (Context.Proof ctxt, fn {background, ...} => (K ("", ""), background)))));
48 fun inline name scan = ML_Context.add_antiq name
49 (scan >> (fn s => fn {struct_name, background} => (K ("", s), background)));
51 fun declaration kind name scan = ML_Context.add_antiq name
52 (scan >> (fn s => fn {struct_name, background} =>
54 val (a, background') = variant name background;
55 val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
56 val body = struct_name ^ "." ^ a;
57 in (K (env, body), background') end));
59 val value = declaration "val";
63 (** concrete antiquotations **)
65 structure P = OuterParse;
70 val _ = value "theory"
71 (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
72 || Scan.succeed "ML_Context.the_global_context ()");
74 val _ = value "theory_ref"
75 (Scan.lift Args.name >> (fn name =>
76 "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")
77 || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
79 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
81 val _ = inline "sort" (Args.context -- Scan.lift Args.name >> (fn (ctxt, s) =>
82 ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
84 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
85 val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
86 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
88 val _ = macro "let" (Args.context --
89 Scan.lift (P.and_list1 (P.and_list1 Args.name -- (Args.$$$ "=" |-- Args.name)))
90 >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
92 val _ = macro "note" (Args.context :|-- (fn ctxt =>
93 P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
94 ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
95 >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
97 val _ = value "ctyp" (Args.typ >> (fn T =>
98 "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
100 val _ = value "cterm" (Args.term >> (fn t =>
101 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
103 val _ = value "cprop" (Args.prop >> (fn t =>
104 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
107 (Args.context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
108 "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
111 fun type_ syn = (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
112 #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
113 |> syn ? Sign.base_name
114 |> ML_Syntax.print_string));
116 val _ = inline "type_name" (type_ false);
117 val _ = inline "type_syntax" (type_ true);
120 fun const syn = Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
121 #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
122 |> syn ? ProofContext.const_syntax_name ctxt
123 |> ML_Syntax.print_string);
125 val _ = inline "const_name" (const false);
126 val _ = inline "const_syntax" (const true);
128 val _ = inline "const"
129 (Args.context -- Scan.lift Args.name -- Scan.optional
130 (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
131 >> (fn ((ctxt, c), Ts) =>
132 let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
133 in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));