1(*  Title:      Pure/ML/ml_context.ML
2    Author:     Makarius
3
4ML context and antiquotations.
5*)
6
7signature ML_CONTEXT =
8sig
9  val check_antiquotation: Proof.context -> xstring * Position.T -> string
10  val struct_name: Proof.context -> string
11  val variant: string -> Proof.context -> string * Proof.context
12  type decl = Proof.context -> string * string
13  val value_decl: string -> string -> Proof.context -> decl * Proof.context
14  val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
15    theory -> theory
16  val print_antiquotations: bool -> Proof.context -> unit
17  val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
18  val eval_file: ML_Compiler.flags -> Path.T -> unit
19  val eval_source: ML_Compiler.flags -> Input.source -> unit
20  val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
21    ML_Lex.token Antiquote.antiquote list -> unit
22  val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
23  val exec: (unit -> unit) -> Context.generic -> Context.generic
24  val expression: Position.range -> string -> string -> string ->
25    ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
26end
27
28structure ML_Context: ML_CONTEXT =
29struct
30
31(** ML antiquotations **)
32
33(* names for generated environment *)
34
35structure Names = Proof_Data
36(
37  type T = string * Name.context;
38  val init_names = ML_Syntax.reserved |> Name.declare "ML_context";
39  fun init _ = ("Isabelle0", init_names);
40);
41
42fun struct_name ctxt = #1 (Names.get ctxt);
43val struct_begin = (Names.map o apfst) (fn _ => "Isabelle" ^ serial_string ());
44
45fun variant a ctxt =
46  let
47    val names = #2 (Names.get ctxt);
48    val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names;
49    val ctxt' = (Names.map o apsnd) (K names') ctxt;
50  in (b, ctxt') end;
51
52
53(* decl *)
54
55type decl = Proof.context -> string * string;  (*final context -> ML env, ML body*)
56
57fun value_decl a s ctxt =
58  let
59    val (b, ctxt') = variant a ctxt;
60    val env = "val " ^ b ^ " = " ^ s ^ ";\n";
61    val body = struct_name ctxt ^ "." ^ b;
62    fun decl (_: Proof.context) = (env, body);
63  in (decl, ctxt') end;
64
65
66(* theory data *)
67
68structure Antiquotations = Theory_Data
69(
70  type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table;
71  val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
72  val extend = I;
73  fun merge data : T = Name_Space.merge_tables data;
74);
75
76val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
77
78fun check_antiquotation ctxt =
79  #1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt);
80
81fun add_antiquotation name f thy = thy
82  |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
83
84fun print_antiquotations verbose ctxt =
85  Pretty.big_list "ML antiquotations:"
86    (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt)))
87  |> Pretty.writeln;
88
89fun apply_antiquotation src ctxt =
90  let val (src', f) = Token.check_src ctxt get_antiquotations src
91  in f src' ctxt end;
92
93
94(* parsing and evaluation *)
95
96local
97
98val antiq =
99  Parse.!!! ((Parse.token Parse.liberal_name ::: Parse.args) --| Scan.ahead Parse.eof);
100
101fun make_env name visible =
102  (ML_Lex.tokenize
103    ("structure " ^ name ^ " =\nstruct\n\
104     \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
105     " (Context.the_local_context ());\n"),
106   ML_Lex.tokenize "end;");
107
108fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");
109
110fun eval_antiquotes (ants, pos) opt_context =
111  let
112    val visible =
113      (case opt_context of
114        SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt
115      | _ => true);
116    val opt_ctxt = Option.map Context.proof_of opt_context;
117
118    val ((ml_env, ml_body), opt_ctxt') =
119      if forall (fn Antiquote.Text _ => true | _ => false) ants
120      then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
121      else
122        let
123          fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
124
125          fun expand_src range src ctxt =
126            let val (decl, ctxt') = apply_antiquotation src ctxt
127            in (decl #> tokenize range, ctxt') end;
128
129          fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
130            | expand (Antiquote.Control {name, range, body}) ctxt =
131                expand_src range
132                  (Token.make_src name (if null body then [] else [Token.read_cartouche body])) ctxt
133            | expand (Antiquote.Antiq {range, body, ...}) ctxt =
134                expand_src range
135                  (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt;
136
137          val ctxt =
138            (case opt_ctxt of
139              NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos)
140            | SOME ctxt => struct_begin ctxt);
141
142          val (begin_env, end_env) = make_env (struct_name ctxt) visible;
143          val (decls, ctxt') = fold_map expand ants ctxt;
144          val (ml_env, ml_body) =
145            decls |> map (fn decl => decl ctxt') |> split_list |> apply2 flat;
146        in ((begin_env @ ml_env @ end_env, ml_body), SOME ctxt') end;
147  in ((ml_env, ml_body), opt_ctxt') end;
148
149in
150
151fun eval flags pos ants =
152  let
153    val non_verbose = ML_Compiler.verbose false flags;
154
155    (*prepare source text*)
156    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.get_generic_context ());
157    val _ =
158      (case env_ctxt of
159        SOME ctxt =>
160          if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt
161          then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
162          else ()
163      | NONE => ());
164
165    (*prepare environment*)
166    val _ =
167      Context.setmp_generic_context
168        (Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt)
169        (fn () =>
170          (ML_Compiler.eval non_verbose Position.none env; Context.get_generic_context ())) ()
171      |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
172
173    (*eval body*)
174    val _ = ML_Compiler.eval flags pos body;
175
176    (*clear environment*)
177    val _ =
178      (case (env_ctxt, is_some (Context.get_generic_context ())) of
179        (SOME ctxt, true) =>
180          let
181            val name = struct_name ctxt;
182            val _ = ML_Compiler.eval non_verbose Position.none (reset_env name);
183            val _ = Context.>> (ML_Env.forget_structure name);
184          in () end
185      | _ => ());
186  in () end;
187
188end;
189
190
191(* derived versions *)
192
193fun eval_file flags path =
194  let val pos = Path.position path
195  in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
196
197fun eval_source flags source =
198  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
199
200fun eval_in ctxt flags pos ants =
201  Context.setmp_generic_context (Option.map Context.Proof ctxt)
202    (fn () => eval flags pos ants) ();
203
204fun eval_source_in ctxt flags source =
205  Context.setmp_generic_context (Option.map Context.Proof ctxt)
206    (fn () => eval_source flags source) ();
207
208fun exec (e: unit -> unit) context =
209  (case Context.setmp_generic_context (SOME context)
210      (fn () => (e (); Context.get_generic_context ())) () of
211    SOME context' => context'
212  | NONE => error "Missing context after execution");
213
214fun expression range name constraint body ants =
215  exec (fn () =>
216    eval ML_Compiler.flags (#1 range)
217     (ML_Lex.read "Context.put_generic_context (SOME (let val " @ ML_Lex.read_set_range range name @
218      ML_Lex.read (": " ^ constraint ^ " =") @ ants @
219      ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
220
221end;
222
223val ML = ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags);
224