src/Pure/ML/ml_context.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 63671 eb4f59275c05
child 68816 5a53724fe247
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/ML/ml_context.ML
     2     Author:     Makarius
     3 
     4 ML context and antiquotations.
     5 *)
     6 
     7 signature ML_CONTEXT =
     8 sig
     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
    26 end
    27 
    28 structure ML_Context: ML_CONTEXT =
    29 struct
    30 
    31 (** ML antiquotations **)
    32 
    33 (* names for generated environment *)
    34 
    35 structure 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 
    42 fun struct_name ctxt = #1 (Names.get ctxt);
    43 val struct_begin = (Names.map o apfst) (fn _ => "Isabelle" ^ serial_string ());
    44 
    45 fun 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 
    55 type decl = Proof.context -> string * string;  (*final context -> ML env, ML body*)
    56 
    57 fun 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 
    68 structure 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 
    76 val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
    77 
    78 fun check_antiquotation ctxt =
    79   #1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt);
    80 
    81 fun add_antiquotation name f thy = thy
    82   |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
    83 
    84 fun 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 
    89 fun 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 
    96 local
    97 
    98 val antiq =
    99   Parse.!!! ((Parse.token Parse.liberal_name ::: Parse.args) --| Scan.ahead Parse.eof);
   100 
   101 fun 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 
   108 fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");
   109 
   110 fun 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 
   149 in
   150 
   151 fun 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 
   188 end;
   189 
   190 
   191 (* derived versions *)
   192 
   193 fun 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 
   197 fun eval_source flags source =
   198   eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
   199 
   200 fun eval_in ctxt flags pos ants =
   201   Context.setmp_generic_context (Option.map Context.Proof ctxt)
   202     (fn () => eval flags pos ants) ();
   203 
   204 fun eval_source_in ctxt flags source =
   205   Context.setmp_generic_context (Option.map Context.Proof ctxt)
   206     (fn () => eval_source flags source) ();
   207 
   208 fun 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 
   214 fun 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 
   221 end;
   222 
   223 val ML = ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags);