author | wenzelm |
Thu, 11 Feb 2010 22:55:16 +0100 | |
changeset 35114 | b1fd1d756e20 |
parent 35111 | 18cd034922ba |
child 35139 | e1a226a191b6 |
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 |
||
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27868
diff
changeset
|
76 |
val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) => |
27340 | 77 |
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))); |
78 |
||
79 |
val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); |
|
80 |
val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
81 |
val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
82 |
||
27379 | 83 |
val _ = macro "let" (Args.context -- |
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27868
diff
changeset
|
84 |
Scan.lift (P.and_list1 (P.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source))) |
27379 | 85 |
>> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt))); |
86 |
||
87 |
val _ = macro "note" (Args.context :|-- (fn ctxt => |
|
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27390
diff
changeset
|
88 |
P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) => |
27379 | 89 |
((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
|
90 |
>> (fn args => #2 (ProofContext.note_thmss "" args ctxt)))); |
27379 | 91 |
|
27340 | 92 |
val _ = value "ctyp" (Args.typ >> (fn T => |
93 |
"Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))); |
|
94 |
||
95 |
val _ = value "cterm" (Args.term >> (fn t => |
|
96 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); |
|
97 |
||
98 |
val _ = value "cprop" (Args.prop >> (fn t => |
|
99 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); |
|
100 |
||
101 |
val _ = value "cpat" |
|
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27868
diff
changeset
|
102 |
(Args.context -- Scan.lift Args.name_source >> uncurry ProofContext.read_term_pattern >> (fn t => |
27340 | 103 |
"Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); |
104 |
||
105 |
||
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27868
diff
changeset
|
106 |
fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => |
27340 | 107 |
#1 (Term.dest_Type (ProofContext.read_tyname ctxt c)) |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
108 |
|> syn ? Long_Name.base_name |
27340 | 109 |
|> ML_Syntax.print_string)); |
110 |
||
111 |
val _ = inline "type_name" (type_ false); |
|
112 |
val _ = inline "type_syntax" (type_ true); |
|
113 |
||
114 |
||
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27868
diff
changeset
|
115 |
fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => |
27340 | 116 |
#1 (Term.dest_Const (ProofContext.read_const_proper ctxt c)) |
117 |
|> syn ? ProofContext.const_syntax_name ctxt |
|
118 |
|> ML_Syntax.print_string); |
|
119 |
||
120 |
val _ = inline "const_name" (const false); |
|
121 |
val _ = inline "const_syntax" (const true); |
|
122 |
||
123 |
val _ = inline "const" |
|
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27868
diff
changeset
|
124 |
(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
|
125 |
(Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] |
27340 | 126 |
>> (fn ((ctxt, c), Ts) => |
127 |
let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c) |
|
128 |
in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end)); |
|
129 |
||
35111 | 130 |
val _ = inline "syntax_const" |
131 |
(Args.context -- Scan.lift Args.name >> (fn (ctxt, c) => |
|
132 |
if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c |
|
133 |
else error ("Unknown syntax const: " ^ quote c))); |
|
134 |
||
27340 | 135 |
end; |
136 |