src/Pure/ML/ml_context.ML
author wenzelm
Thu Mar 19 15:44:14 2009 +0100 (2009-03-19)
changeset 30589 cbe27c4ef417
parent 30588 05f81bbb2614
child 30590 1d9c9fcf8513
permissions -rw-r--r--
Antiquote.Text: keep full position information;
     1 (*  Title:      Pure/ML/ml_context.ML
     2     Author:     Makarius
     3 
     4 ML context and antiquotations.
     5 *)
     6 
     7 signature BASIC_ML_CONTEXT =
     8 sig
     9   val bind_thm: string * thm -> unit
    10   val bind_thms: string * thm list -> unit
    11   val thm: xstring -> thm
    12   val thms: xstring -> thm list
    13 end
    14 
    15 signature ML_CONTEXT =
    16 sig
    17   include BASIC_ML_CONTEXT
    18   val the_generic_context: unit -> Context.generic
    19   val the_global_context: unit -> theory
    20   val the_local_context: unit -> Proof.context
    21   val exec: (unit -> unit) -> Context.generic -> Context.generic
    22   val inherit_env: Context.generic -> Context.generic -> Context.generic
    23   val name_space: ML_NameSpace.nameSpace
    24   val stored_thms: thm list ref
    25   val ml_store_thm: string * thm -> unit
    26   val ml_store_thms: string * thm list -> unit
    27   type antiq =
    28     {struct_name: string, background: Proof.context} ->
    29       (Proof.context -> string * string) * Proof.context
    30   val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
    31   val trace: bool ref
    32   val eval_wrapper: (string -> unit) * (string -> 'a) -> bool ->
    33     Position.T -> Symbol_Pos.text -> unit
    34   val eval: bool -> Position.T -> Symbol_Pos.text -> unit
    35   val eval_file: Path.T -> unit
    36   val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
    37   val evaluate: Proof.context -> (string -> unit) * (string -> 'b) -> bool ->
    38     string * (unit -> 'a) option ref -> string -> 'a
    39   val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
    40 end
    41 
    42 structure ML_Context: ML_CONTEXT =
    43 struct
    44 
    45 (** implicit ML context **)
    46 
    47 val the_generic_context = Context.the_thread_data;
    48 val the_global_context = Context.theory_of o the_generic_context;
    49 val the_local_context = Context.proof_of o the_generic_context;
    50 
    51 fun exec (e: unit -> unit) context =
    52   (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
    53     SOME context' => context'
    54   | NONE => error "Missing context after execution");
    55 
    56 
    57 (* ML name space *)
    58 
    59 structure ML_Env = GenericDataFun
    60 (
    61   type T =
    62     ML_NameSpace.valueVal Symtab.table *
    63     ML_NameSpace.typeVal Symtab.table *
    64     ML_NameSpace.fixityVal Symtab.table *
    65     ML_NameSpace.structureVal Symtab.table *
    66     ML_NameSpace.signatureVal Symtab.table *
    67     ML_NameSpace.functorVal Symtab.table;
    68   val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
    69   val extend = I;
    70   fun merge _
    71    ((val1, type1, fixity1, structure1, signature1, functor1),
    72     (val2, type2, fixity2, structure2, signature2, functor2)) : T =
    73    (Symtab.merge (K true) (val1, val2),
    74     Symtab.merge (K true) (type1, type2),
    75     Symtab.merge (K true) (fixity1, fixity2),
    76     Symtab.merge (K true) (structure1, structure2),
    77     Symtab.merge (K true) (signature1, signature2),
    78     Symtab.merge (K true) (functor1, functor2));
    79 );
    80 
    81 val inherit_env = ML_Env.put o ML_Env.get;
    82 
    83 val name_space: ML_NameSpace.nameSpace =
    84   let
    85     fun lookup sel1 sel2 name =
    86       Context.thread_data ()
    87       |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (ML_Env.get context)) name)
    88       |> (fn NONE => sel2 ML_NameSpace.global name | some => some);
    89 
    90     fun all sel1 sel2 () =
    91       Context.thread_data ()
    92       |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (ML_Env.get context)))
    93       |> append (sel2 ML_NameSpace.global ())
    94       |> sort_distinct (string_ord o pairself #1);
    95 
    96     fun enter ap1 sel2 entry =
    97       if is_some (Context.thread_data ()) then
    98         Context.>> (ML_Env.map (ap1 (Symtab.update entry)))
    99       else sel2 ML_NameSpace.global entry;
   100   in
   101    {lookupVal    = lookup #1 #lookupVal,
   102     lookupType   = lookup #2 #lookupType,
   103     lookupFix    = lookup #3 #lookupFix,
   104     lookupStruct = lookup #4 #lookupStruct,
   105     lookupSig    = lookup #5 #lookupSig,
   106     lookupFunct  = lookup #6 #lookupFunct,
   107     enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
   108     enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
   109     enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
   110     enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
   111     enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
   112     enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
   113     allVal       = all #1 #allVal,
   114     allType      = all #2 #allType,
   115     allFix       = all #3 #allFix,
   116     allStruct    = all #4 #allStruct,
   117     allSig       = all #5 #allSig,
   118     allFunct     = all #6 #allFunct}
   119   end;
   120 
   121 
   122 (* theorem bindings *)
   123 
   124 val stored_thms: thm list ref = ref [];
   125 
   126 fun ml_store sel (name, ths) =
   127   let
   128     val ths' = Context.>>> (Context.map_theory_result
   129       (PureThy.store_thms (Binding.name name, ths)));
   130     val _ =
   131       if name = "" then ()
   132       else if not (ML_Syntax.is_identifier name) then
   133         error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
   134       else setmp stored_thms ths' (fn () =>
   135         use_text name_space (0, "") Output.ml_output true
   136           ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) ();
   137   in () end;
   138 
   139 val ml_store_thms = ml_store "";
   140 fun ml_store_thm (name, th) = ml_store "hd" (name, [th]);
   141 
   142 fun bind_thm (name, thm) = ml_store_thm (name, Drule.standard thm);
   143 fun bind_thms (name, thms) = ml_store_thms (name, map Drule.standard thms);
   144 
   145 fun thm name = ProofContext.get_thm (the_local_context ()) name;
   146 fun thms name = ProofContext.get_thms (the_local_context ()) name;
   147 
   148 
   149 
   150 (** ML antiquotations **)
   151 
   152 (* antiquotation commands *)
   153 
   154 type antiq =
   155   {struct_name: string, background: Proof.context} ->
   156     (Proof.context -> string * string) * Proof.context;
   157 
   158 local
   159 
   160 val global_parsers = ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
   161 
   162 in
   163 
   164 fun add_antiq name scan = CRITICAL (fn () =>
   165   change global_parsers (fn tab =>
   166    (if not (Symtab.defined tab name) then ()
   167     else warning ("Redefined ML antiquotation: " ^ quote name);
   168     Symtab.update (name, scan) tab)));
   169 
   170 fun antiquotation src ctxt =
   171   let val ((name, _), pos) = Args.dest_src src in
   172     (case Symtab.lookup (! global_parsers) name of
   173       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
   174     | SOME scan => (Position.report (Markup.ML_antiq name) pos;
   175         Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
   176   end;
   177 
   178 end;
   179 
   180 
   181 (* parsing and evaluation *)
   182 
   183 local
   184 
   185 structure P = OuterParse;
   186 structure T = OuterLex;
   187 
   188 val antiq =
   189   P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
   190   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
   191 
   192 val struct_name = "Isabelle";
   193 
   194 fun eval_antiquotes (txt, pos) opt_context =
   195   let
   196     val syms = Symbol_Pos.explode (txt, pos);
   197     val ants = Antiquote.read (syms, pos);
   198     val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
   199     val ((ml_env, ml_body), opt_ctxt') =
   200       if not (exists Antiquote.is_antiq ants)
   201       then (("", Symbol.escape (Symbol_Pos.content syms)), opt_ctxt)
   202       else
   203         let
   204           val ctxt =
   205             (case opt_ctxt of
   206               NONE => error ("Unknown context -- cannot expand ML antiquotations" ^
   207                 Position.str_of pos)
   208             | SOME ctxt => Context.proof_of ctxt);
   209 
   210           val lex = #1 (OuterKeyword.get_lexicons ());
   211           fun no_decl _ = ("", "");
   212 
   213           fun expand (Antiquote.Text ss) state =
   214                 (K ("", Symbol.escape (Symbol_Pos.content ss)), state)
   215             | expand (Antiquote.Antiq x) (scope, background) =
   216                 let
   217                   val context = Stack.top scope;
   218                   val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
   219                   val (decl, background') = f {background = background, struct_name = struct_name};
   220                 in (decl, (Stack.map_top (K context') scope, background')) end
   221             | expand (Antiquote.Open _) (scope, background) =
   222                 (no_decl, (Stack.push scope, background))
   223             | expand (Antiquote.Close _) (scope, background) =
   224                 (no_decl, (Stack.pop scope, background));
   225 
   226           val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
   227           val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself implode;
   228         in (ml, SOME (Context.Proof ctxt')) end;
   229   in (("structure " ^ struct_name ^ " =\nstruct\n" ^ ml_env ^ "end;", ml_body), opt_ctxt') end;
   230 
   231 in
   232 
   233 val trace = ref false;
   234 
   235 fun eval_wrapper pr verbose pos txt =
   236   let
   237     fun eval_raw p = use_text name_space
   238       (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr;
   239 
   240     (*prepare source text*)
   241     val _ = Position.report Markup.ML_source pos;
   242     val ((env, body), env_ctxt) = eval_antiquotes (txt, pos) (Context.thread_data ());
   243     val _ = if ! trace then tracing (cat_lines [env, body]) else ();
   244 
   245     (*prepare static ML environment*)
   246     val _ = Context.setmp_thread_data env_ctxt
   247         (fn () => (eval_raw Position.none false env; Context.thread_data ())) ()
   248       |> (fn NONE => () | SOME context' => Context.>> (ML_Env.put (ML_Env.get context')));
   249 
   250     (*eval ML*)
   251     val _ = eval_raw pos verbose body;
   252 
   253     (*reset static ML environment*)
   254     val _ = eval_raw Position.none false "structure Isabelle = struct end";
   255   in () end;
   256 
   257 end;
   258 
   259 
   260 (* ML evaluation *)
   261 
   262 val eval = eval_wrapper Output.ml_output;
   263 fun eval_file path = eval true (Path.position path) (File.read path);
   264 
   265 fun eval_in ctxt verbose pos txt =
   266   Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos txt) ();
   267 
   268 fun evaluate ctxt pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
   269   let
   270     val _ = r := NONE;
   271     val _ = Context.setmp_thread_data (SOME (Context.Proof ctxt)) (fn () =>
   272       eval_wrapper pr verbose Position.none
   273         ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))")) ();
   274   in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
   275 
   276 fun expression pos bind body txt =
   277   exec (fn () => eval false pos
   278     ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
   279       " end (ML_Context.the_generic_context ())));"));
   280 
   281 end;
   282 
   283 structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
   284 open Basic_ML_Context;