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