1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/ml_context.ML	Fri Jan 19 22:08:13 2007 +0100
     1.3 @@ -0,0 +1,195 @@
     1.4 +(*  Title:      Pure/Thy/ml_context.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +ML context and antiquotations.
     1.9 +*)
    1.10 +
    1.11 +signature BASIC_ML_CONTEXT =
    1.12 +sig
    1.13 +  val the_context: unit -> theory
    1.14 +  val thm: xstring -> thm
    1.15 +  val thms: xstring -> thm list
    1.16 +end;
    1.17 +
    1.18 +signature ML_CONTEXT =
    1.19 +sig
    1.20 +  include BASIC_ML_CONTEXT
    1.21 +  val get_context: unit -> Context.generic option
    1.22 +  val set_context: Context.generic option -> unit
    1.23 +  val setmp: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    1.24 +  val the_generic_context: unit -> Context.generic
    1.25 +  val the_local_context: unit -> Proof.context
    1.26 +  val pass: Context.generic option -> ('a -> 'b) -> 'a -> 'b * Context.generic option
    1.27 +  val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic
    1.28 +  val save: ('a -> 'b) -> 'a -> 'b
    1.29 +  val >> : (theory -> theory) -> unit
    1.30 +  val add_keywords: string list -> unit
    1.31 +  val inline_antiq: string -> (Args.T list -> string * Args.T list) -> unit
    1.32 +  val value_antiq: string -> (Args.T list -> (string * string) * Args.T list) -> unit
    1.33 +  val use_mltext: string -> bool -> Context.generic option -> unit
    1.34 +  val use_mltext_update: string -> bool -> Context.generic -> Context.generic
    1.35 +  val use_let: string -> string -> string -> Context.generic -> Context.generic
    1.36 +end;
    1.37 +
    1.38 +structure ML_Context: ML_CONTEXT =
    1.39 +struct
    1.40 +
    1.41 +(** Implicit ML context **)
    1.42 +
    1.43 +local
    1.44 +  val current_context = ref (NONE: Context.generic option);
    1.45 +in
    1.46 +  fun get_context () = ! current_context;
    1.47 +  fun set_context opt_context = current_context := opt_context;
    1.48 +  fun setmp opt_context f x = Library.setmp current_context opt_context f x;
    1.49 +end;
    1.50 +
    1.51 +fun the_generic_context () =
    1.52 +  (case get_context () of
    1.53 +    SOME context => context
    1.54 +  | _ => error "Unknown context");
    1.55 +
    1.56 +val the_context = Context.theory_of o the_generic_context;
    1.57 +val the_local_context = Context.proof_of o the_generic_context;
    1.58 +
    1.59 +fun pass opt_context f x =
    1.60 +  setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x;
    1.61 +
    1.62 +fun pass_context context f x =
    1.63 +  (case pass (SOME context) f x of
    1.64 +    (y, SOME context') => (y, context')
    1.65 +  | (_, NONE) => error "Lost context in ML");
    1.66 +
    1.67 +fun save f x = setmp (get_context ()) f x;
    1.68 +
    1.69 +fun change_theory f =
    1.70 +  set_context (SOME (Context.map_theory f (the_generic_context ())));
    1.71 +
    1.72 +
    1.73 +
    1.74 +(** ML antiquotations **)
    1.75 +
    1.76 +(* maintain keywords *)
    1.77 +
    1.78 +val global_lexicon = ref Scan.empty_lexicon;
    1.79 +
    1.80 +fun add_keywords keywords =
    1.81 +  change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords));
    1.82 +
    1.83 +
    1.84 +(* maintain commands *)
    1.85 +
    1.86 +datatype antiq = Inline of string | Value of string * string;
    1.87 +val global_parsers = ref (Symtab.empty: (Args.T list -> antiq * Args.T list) Symtab.table);
    1.88 +
    1.89 +local
    1.90 +
    1.91 +fun add_item kind name scan = change global_parsers (fn tab =>
    1.92 + (if not (Symtab.defined tab name) then ()
    1.93 +  else warning ("Redefined ML antiquotation: " ^ quote name);
    1.94 +  Symtab.update (name, scan >> kind) tab));
    1.95 +
    1.96 +in
    1.97 +
    1.98 +val inline_antiq = add_item Inline;
    1.99 +val value_antiq = add_item Value;
   1.100 +
   1.101 +end;
   1.102 +
   1.103 +
   1.104 +(* command syntax *)
   1.105 +
   1.106 +fun syntax scan src =
   1.107 +  #1 (Args.context_syntax "ML antiquotation" (Scan.lift scan) src (the_local_context ()));
   1.108 +
   1.109 +fun command src =
   1.110 +  let val ((name, _), pos) = Args.dest_src src in
   1.111 +    (case Symtab.lookup (! global_parsers) name of
   1.112 +      NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
   1.113 +    | SOME scan => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos))
   1.114 +        (fn () => syntax scan src) ())
   1.115 +  end;
   1.116 +
   1.117 +
   1.118 +(* outer syntax *)
   1.119 +
   1.120 +structure T = OuterLex;
   1.121 +structure P = OuterParse;
   1.122 +
   1.123 +val antiq =
   1.124 +  P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof)
   1.125 +  >> (fn ((x, pos), y) => Args.src ((x, y), pos));
   1.126 +
   1.127 +
   1.128 +(* input/output wrappers *)
   1.129 +
   1.130 +local
   1.131 +
   1.132 +val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;";
   1.133 +val isabelle_struct0 = isabelle_struct "";
   1.134 +
   1.135 +fun eval_antiquotes txt =
   1.136 +  let
   1.137 +    val ants = Antiquote.scan_antiquotes (txt, Position.line 1);
   1.138 +
   1.139 +    fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names)
   1.140 +      | expand (Antiquote.Antiq x) names =
   1.141 +          (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of
   1.142 +            Inline s => (("", s), names)
   1.143 +          | Value (a, s) =>
   1.144 +              let
   1.145 +                val a' = if ML_Syntax.is_identifier a then a else "val";
   1.146 +                val ([b], names') = Name.variants [a'] names;
   1.147 +              in (("val " ^ b ^ " = " ^ s ^ ";\n", "Isabelle." ^ b), names') end);
   1.148 +
   1.149 +    val (decls, body) =
   1.150 +      fold_map expand ants ML_Syntax.reserved
   1.151 +      |> #1 |> split_list |> pairself implode;
   1.152 +  in (isabelle_struct decls, body) end;
   1.153 +
   1.154 +fun eval verbose txt =
   1.155 +  Output.ML_errors (use_text Output.ml_output verbose) txt;
   1.156 +
   1.157 +in
   1.158 +
   1.159 +fun eval_wrapper verbose txt =
   1.160 +  let val (txt1, txt2) = eval_antiquotes txt
   1.161 +  in eval false txt1; eval verbose txt2; eval false isabelle_struct0 end;
   1.162 +
   1.163 +end;
   1.164 +
   1.165 +
   1.166 +
   1.167 +(** ML evaluation **)
   1.168 +
   1.169 +fun use_mltext txt verbose opt_context = setmp opt_context (fn () => eval_wrapper verbose txt) ();
   1.170 +fun use_mltext_update txt verbose context = #2 (pass_context context (eval_wrapper verbose) txt);
   1.171 +
   1.172 +fun use_context txt = use_mltext_update
   1.173 +  ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false;
   1.174 +
   1.175 +fun use_let bind body txt =
   1.176 +  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   1.177 +
   1.178 +
   1.179 +
   1.180 +(** implicit fact references **)
   1.181 +
   1.182 +fun thm name = ProofContext.get_thm (the_local_context ()) (Name name);
   1.183 +fun thms name = ProofContext.get_thms (the_local_context ()) (Name name);
   1.184 +
   1.185 +val _ = value_antiq "thm"
   1.186 +  (Args.name >> (fn s => (s, "ML_Context.thm " ^ ML_Syntax.print_string s)));
   1.187 +val _ = value_antiq "thms"
   1.188 +  (Args.name >> (fn s => (s, "ML_Context.thms " ^ ML_Syntax.print_string s)));
   1.189 +
   1.190 +
   1.191 +(*final declarations of this structure!*)
   1.192 +nonfix >>;
   1.193 +fun >> f = change_theory f;
   1.194 +
   1.195 +end;
   1.196 +
   1.197 +structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
   1.198 +open Basic_ML_Context;