src/Pure/ML/ml_context.ML
author wenzelm
Thu Mar 20 17:38:55 2008 +0100 (2008-03-20 ago)
changeset 26368 3e74b09ce466
parent 26361 7946f459c6c8
child 26374 be47e9a83b4f
permissions -rw-r--r--
thm_antiq: produce error at runtime, not compile time;
tuned;
     1 (*  Title:      Pure/ML/ml_context.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 ML context and antiquotations.
     6 *)
     7 
     8 signature BASIC_ML_CONTEXT =
     9 sig
    10   val the_context: unit -> theory
    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 get_context: unit -> Context.generic option
    19   val set_context: Context.generic option -> unit
    20   val setmp: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    21   val the_generic_context: unit -> Context.generic
    22   val the_local_context: unit -> Proof.context
    23   val pass: Context.generic option -> ('a -> 'b) -> 'a -> 'b * Context.generic option
    24   val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic
    25   val save: ('a -> 'b) -> 'a -> 'b
    26   val >> : (theory -> theory) -> unit
    27   val add_keywords: string list -> unit
    28   val inline_antiq: string ->
    29     (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
    30   val value_antiq: string ->
    31     (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit
    32   val proj_value_antiq: string -> (Context.generic * Args.T list ->
    33       (string * string * string) * (Context.generic * Args.T list)) -> unit
    34   val eval_antiquotes_fn: (string -> string * string) ref  (* FIXME tmp *)
    35   val trace: bool ref
    36   val use_mltext: string -> bool -> Context.generic option -> unit
    37   val use_mltext_update: string -> bool -> Context.generic -> Context.generic
    38   val use_let: string -> string -> string -> Context.generic -> Context.generic
    39   val use: Path.T -> unit
    40   val evaluate: (string -> unit) * (string -> 'b) -> bool ->
    41     string * (unit -> 'a) option ref -> string -> 'a
    42 end
    43 
    44 structure ML_Context: ML_CONTEXT =
    45 struct
    46 
    47 (** Implicit ML context **)
    48 
    49 local
    50   val current_context = ref (NONE: Context.generic option);
    51 in
    52   fun get_context () = ! current_context;
    53   fun set_context opt_context = current_context := opt_context;
    54   fun setmp opt_context f x = Library.setmp current_context opt_context f x;
    55 end;
    56 
    57 fun the_generic_context () =
    58   (case get_context () of
    59     SOME context => context
    60   | _ => error "Unknown context");
    61 
    62 val the_local_context = Context.proof_of o the_generic_context;
    63 
    64 val the_context = Context.theory_of o the_generic_context;
    65 
    66 fun pass opt_context f x =
    67   setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x;
    68 
    69 fun pass_context context f x =
    70   (case pass (SOME context) f x of
    71     (y, SOME context') => (y, context')
    72   | (_, NONE) => error "Lost context in ML");
    73 
    74 fun save f x = NAMED_CRITICAL "ML" (fn () => setmp (get_context ()) f x);
    75 
    76 fun change_theory f = NAMED_CRITICAL "ML" (fn () =>
    77   set_context (SOME (Context.map_theory f (the_generic_context ()))));
    78 
    79 
    80 
    81 (** ML antiquotations **)
    82 
    83 (* maintain keywords *)
    84 
    85 val global_lexicon = ref Scan.empty_lexicon;
    86 
    87 fun add_keywords keywords = CRITICAL (fn () =>
    88   change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords)));
    89 
    90 
    91 (* maintain commands *)
    92 
    93 datatype antiq = Inline of string | ProjValue of string * string * string;
    94 val global_parsers = ref (Symtab.empty:
    95   (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table);
    96 
    97 local
    98 
    99 fun add_item kind name scan = CRITICAL (fn () =>
   100   change global_parsers (fn tab =>
   101    (if not (Symtab.defined tab name) then ()
   102     else warning ("Redefined ML antiquotation: " ^ quote name);
   103     Symtab.update (name, scan >> kind) tab)));
   104 
   105 in
   106 
   107 val inline_antiq = add_item Inline;
   108 val proj_value_antiq = add_item ProjValue;
   109 fun value_antiq name scan = proj_value_antiq name (scan >> (fn (a, s) => (a, s, "")));
   110 
   111 end;
   112 
   113 
   114 (* command syntax *)
   115 
   116 fun syntax scan src =
   117   #1 (Args.context_syntax "ML antiquotation" scan src (the_local_context ()));
   118 
   119 fun command src =
   120   let val ((name, _), pos) = Args.dest_src src in
   121     (case Symtab.lookup (! global_parsers) name of
   122       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
   123     | SOME scan => syntax scan src)
   124   end;
   125 
   126 
   127 (* outer syntax *)
   128 
   129 structure T = OuterLex;
   130 structure P = OuterParse;
   131 
   132 val antiq =
   133   P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof)
   134   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
   135 
   136 
   137 (* input/output wrappers *)
   138 
   139 local
   140 
   141 val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;";
   142 val isabelle_struct0 = isabelle_struct "";
   143 
   144 fun eval_antiquotes txt =
   145   let
   146     val ants = Antiquote.scan_antiquotes (txt, Position.line 1);
   147 
   148     fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names)
   149       | expand (Antiquote.Antiq x) names =
   150           (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of
   151             Inline s => (("", s), names)
   152           | ProjValue (a, s, f) =>
   153               let
   154                 val a' = if ML_Syntax.is_identifier a then a else "val";
   155                 val ([b], names') = Name.variants [a'] names;
   156                 val binding = "val " ^ b ^ " = " ^ s ^ ";\n";
   157                 val value =
   158                   if f = "" then "Isabelle." ^ b
   159                   else "(" ^ f ^ " Isabelle." ^ b ^ ")";
   160               in ((binding, value), names') end);
   161 
   162     val (decls, body) =
   163       NAMED_CRITICAL "ML" (fn () => fold_map expand ants ML_Syntax.reserved)
   164       |> #1 |> split_list |> pairself implode;
   165   in (isabelle_struct decls, body) end;
   166 
   167 in
   168 
   169 val eval_antiquotes_fn = ref eval_antiquotes;
   170 
   171 val trace = ref false;
   172 
   173 fun eval_wrapper name pr verbose txt =
   174   let
   175     val (txt1, txt2) = ! eval_antiquotes_fn txt;  (* FIXME tmp hook *)
   176     val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else ();
   177     fun eval nm = use_text nm pr;
   178   in
   179     NAMED_CRITICAL "ML" (fn () =>
   180       (eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0))
   181   end;
   182 
   183 fun ML_wrapper pr = eval_wrapper "ML" pr;
   184 
   185 end;
   186 
   187 
   188 (* ML evaluation *)
   189 
   190 fun use_mltext txt verbose opt_context =
   191   setmp opt_context (fn () => ML_wrapper Output.ml_output verbose txt) ();
   192 
   193 fun use_mltext_update txt verbose context =
   194   #2 (pass_context context (fn () => ML_wrapper Output.ml_output verbose txt) ());
   195 
   196 fun use_context txt = use_mltext_update
   197   ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false;
   198 
   199 fun use_let bind body txt =
   200   use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   201 
   202 fun use path = eval_wrapper (Path.implode path) Output.ml_output true (File.read path);
   203 
   204 fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
   205   let
   206     val _ = r := NONE;
   207     val _ = ML_wrapper pr verbose ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
   208   in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
   209 
   210 
   211 (* basic antiquotations *)
   212 
   213 local
   214 
   215 fun context x = (Scan.state >> Context.proof_of) x;
   216 
   217 val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()"));
   218 
   219 val _ = inline_antiq "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) =>
   220   ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
   221 
   222 val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
   223 val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
   224 val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
   225 
   226 val _ = value_antiq "ctyp" (Args.typ >> (fn T =>
   227   ("ctyp",
   228     "Thm.ctyp_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))));
   229 
   230 val _ = value_antiq "cterm" (Args.term >> (fn t =>
   231   ("cterm",
   232     "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
   233 
   234 val _ = value_antiq "cprop" (Args.prop >> (fn t =>
   235   ("cprop",
   236     "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
   237 
   238 fun type_ syn = (context -- Scan.lift Args.name >> (fn (ctxt, c) =>
   239     #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
   240     |> syn ? Sign.base_name
   241     |> ML_Syntax.print_string));
   242 
   243 val _ = inline_antiq "type_name" (type_ false);
   244 val _ = inline_antiq "type_syntax" (type_ true);
   245 
   246 fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
   247   #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
   248   |> syn ? ProofContext.const_syntax_name ctxt
   249   |> ML_Syntax.print_string);
   250 
   251 val _ = inline_antiq "const_name" (const false);
   252 val _ = inline_antiq "const_syntax" (const true);
   253 
   254 val _ = inline_antiq "const"
   255   ((Scan.state >> Context.proof_of) -- Scan.lift Args.name --
   256     Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   257     >> (fn ((ctxt, c), Ts) =>
   258       let
   259         val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c);
   260       in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
   261 
   262 in val _ = () end;
   263 
   264 
   265 (** fact references **)
   266 
   267 fun thm name = ProofContext.get_thm (the_local_context ()) name;
   268 fun thms name = ProofContext.get_thms (the_local_context ()) name;
   269 
   270 
   271 local
   272 
   273 fun print_interval (Facts.FromTo arg) =
   274       "Facts.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg
   275   | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i
   276   | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
   277 
   278 fun print_named args =
   279   "Facts.Named " ^
   280     ML_Syntax.print_pair (ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position)
   281       (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) args;
   282 
   283 fun thm_antiq kind get get_name = value_antiq kind
   284   ((Scan.state >> Context.proof_of) --
   285     Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel)
   286   >> (fn (ctxt, thmspec as ((name, _), _)) =>
   287       let
   288         val _ = get ctxt (Facts.Named thmspec);
   289         val thmspec_txt = ML_Syntax.atomic (print_named thmspec);
   290       in (name, get_name ^ " (ML_Context.the_local_context ()) " ^ thmspec_txt) end));
   291 
   292 in
   293 
   294 val _ = add_keywords ["(", ")", "-", ","];
   295 val _ = thm_antiq "thm" ProofContext.get_fact_single "ProofContext.get_fact_single";
   296 val _ = thm_antiq "thms" ProofContext.get_fact "ProofContext.get_fact";
   297 
   298 end;
   299 
   300 val _ = proj_value_antiq "cpat" (Scan.lift Args.name >>
   301     (fn name => ("cpat",
   302       "Thm.cterm_of (ML_Context.the_context ()) (Syntax.read_term \
   303       \(ProofContext.set_mode ProofContext.mode_pattern (ML_Context.the_local_context ()))"
   304       ^ ML_Syntax.print_string name ^ ")", "")));
   305 
   306 (*final declarations of this structure!*)
   307 nonfix >>;
   308 fun >> f = change_theory f;
   309 
   310 end;
   311 
   312 structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
   313 open Basic_ML_Context;