--- a/src/Pure/General/antiquote.ML Sun Mar 22 19:43:21 2009 +0100
+++ b/src/Pure/General/antiquote.ML Sun Mar 22 21:48:14 2009 +0100
@@ -11,11 +11,12 @@
Antiq of Symbol_Pos.T list * Position.T |
Open of Position.T |
Close of Position.T
- val is_antiq: 'a antiquote -> bool
+ val is_text: 'a antiquote -> bool
+ val report: ('a -> unit) -> 'a antiquote -> unit
+ val check_nesting: 'a antiquote list -> unit
val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
- val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
- Symbol_Pos.T list * Position.T -> 'a antiquote list
+ val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
end;
structure Antiquote: ANTIQUOTE =
@@ -29,8 +30,18 @@
Open of Position.T |
Close of Position.T;
-fun is_antiq (Text _) = false
- | is_antiq _ = true;
+fun is_text (Text _) = true
+ | is_text _ = false;
+
+
+(* report *)
+
+val report_antiq = Position.report Markup.antiq;
+
+fun report report_text (Text x) = report_text x
+ | report _ (Antiq (_, pos)) = report_antiq pos
+ | report _ (Open pos) = report_antiq pos
+ | report _ (Close pos) = report_antiq pos;
(* check_nesting *)
@@ -83,12 +94,9 @@
(* read *)
-fun read _ _ ([], _) = []
- | read report scanner (syms, pos) =
- (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
- SOME xs =>
- (List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos | Text x => report x) xs;
- check_nesting xs; xs)
- | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
+fun read (syms, pos) =
+ (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
+ SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
+ | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
end;
--- a/src/Pure/IsaMakefile Sun Mar 22 19:43:21 2009 +0100
+++ b/src/Pure/IsaMakefile Sun Mar 22 21:48:14 2009 +0100
@@ -69,7 +69,7 @@
Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \
Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
- ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
+ ML/ml_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
ML-Systems/install_pp_polyml-experimental.ML Proof/extraction.ML \
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \
--- a/src/Pure/ML-Systems/polyml-experimental.ML Sun Mar 22 19:43:21 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML Sun Mar 22 21:48:14 2009 +0100
@@ -72,6 +72,10 @@
(* toplevel pretty printing *)
+fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind)
+ | pretty_ml (PrettyString s) = ML_Pretty.String (s, size s)
+ | pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+
fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
| ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
| ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
--- a/src/Pure/ML/ml_context.ML Sun Mar 22 19:43:21 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Sun Mar 22 21:48:14 2009 +0100
@@ -29,6 +29,8 @@
(Proof.context -> string * string) * Proof.context
val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
val trace: bool ref
+ val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
+ Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
val eval_wrapper: (string -> unit) * (string -> 'a) -> bool ->
Position.T -> Symbol_Pos.text -> unit
val eval: bool -> Position.T -> Symbol_Pos.text -> unit
@@ -190,45 +192,44 @@
>> (fn ((x, pos), y) => Args.src ((x, y), pos));
val struct_name = "Isabelle";
+val begin_env = ML_Lex.tokenize ("structure " ^ struct_name ^ " =\nstruct\n");
+val end_env = ML_Lex.tokenize "end;";
-fun eval_antiquotes (txt, pos) opt_context =
+in
+
+fun eval_antiquotes (ants, pos) opt_context =
let
- val syms = Symbol_Pos.explode (txt, pos);
- val ants = Antiquote.read ML_Lex.report_token ML_Lex.scan_antiq (syms, pos);
val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
val ((ml_env, ml_body), opt_ctxt') =
- if not (exists Antiquote.is_antiq ants)
- then (("", Symbol.escape (Symbol_Pos.content syms)), opt_ctxt)
+ if forall Antiquote.is_text ants
+ then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
else
let
val ctxt =
(case opt_ctxt of
- NONE => error ("Unknown context -- cannot expand ML antiquotations" ^
- Position.str_of pos)
+ NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.str_of pos)
| SOME ctxt => Context.proof_of ctxt);
val lex = #1 (OuterKeyword.get_lexicons ());
- fun no_decl _ = ("", "");
+ fun no_decl _ = ([], []);
- fun expand (Antiquote.Text tok) state =
- (K ("", Symbol.escape (ML_Lex.content_of tok)), state)
+ fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
| expand (Antiquote.Antiq x) (scope, background) =
let
val context = Stack.top scope;
val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
val (decl, background') = f {background = background, struct_name = struct_name};
- in (decl, (Stack.map_top (K context') scope, background')) end
+ val decl' = pairself ML_Lex.tokenize o decl;
+ in (decl', (Stack.map_top (K context') scope, background')) end
| expand (Antiquote.Open _) (scope, background) =
(no_decl, (Stack.push scope, background))
| expand (Antiquote.Close _) (scope, background) =
(no_decl, (Stack.pop scope, background));
val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
- val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself implode;
+ val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
in (ml, SOME (Context.Proof ctxt')) end;
- in (("structure " ^ struct_name ^ " =\nstruct\n" ^ ml_env ^ "end;", ml_body), opt_ctxt') end;
-
-in
+ in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
val trace = ref false;
@@ -239,13 +240,15 @@
(*prepare source text*)
val _ = Position.report Markup.ML_source pos;
- val ((env, body), env_ctxt) = eval_antiquotes (txt, pos) (Context.thread_data ());
+ val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
+ val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ())
+ |>> pairself (implode o map ML_Lex.text_of);
val _ = if ! trace then tracing (cat_lines [env, body]) else ();
(*prepare static ML environment*)
val _ = Context.setmp_thread_data env_ctxt
(fn () => (eval_raw Position.none false env; Context.thread_data ())) ()
- |> (fn NONE => () | SOME context' => Context.>> (ML_Env.put (ML_Env.get context')));
+ |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
(*eval ML*)
val _ = eval_raw pos verbose body;
--- a/src/Pure/ML/ml_lex.ML Sun Mar 22 19:43:21 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML Sun Mar 22 21:48:14 2009 +0100
@@ -13,17 +13,17 @@
val stopper: token Scan.stopper
val is_regular: token -> bool
val is_improper: token -> bool
- val pos_of: token -> string
+ val pos_of: token -> Position.T
val kind_of: token -> token_kind
val content_of: token -> string
- val markup_of: token -> Markup.T
+ val text_of: token -> string
val report_token: token -> unit
val keywords: string list
- val scan_antiq: Symbol_Pos.T list -> token Antiquote.antiquote * Symbol_Pos.T list
val source: (Symbol.symbol, 'a) Source.source ->
(token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
Source.source) Source.source
val tokenize: string -> token list
+ val read_antiq: Symbol_Pos.T list * Position.T -> token Antiquote.antiquote list
end;
structure ML_Lex: ML_LEX =
@@ -42,10 +42,8 @@
(* position *)
-fun position_of (Token ((pos, _), _)) = pos;
-fun end_position_of (Token ((_, pos), _)) = pos;
-
-val pos_of = Position.str_of o position_of;
+fun pos_of (Token ((pos, _), _)) = pos;
+fun end_pos_of (Token ((_, pos), _)) = pos;
(* control tokens *)
@@ -57,7 +55,7 @@
| is_eof _ = false;
val stopper =
- Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+ Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
(* token content *)
@@ -67,6 +65,11 @@
fun kind_of (Token (_, (k, _))) = k;
+fun text_of tok =
+ (case kind_of tok of
+ Error msg => error msg
+ | _ => Symbol.escape (content_of tok));
+
fun is_regular (Token (_, (Error _, _))) = false
| is_regular (Token (_, (EOF, _))) = false
| is_regular _ = true;
@@ -78,22 +81,23 @@
(* markup *)
-val markup_of = kind_of #>
- (fn Keyword => Markup.ML_keyword
- | Ident => Markup.ML_ident
- | LongIdent => Markup.ML_ident
- | TypeVar => Markup.ML_tvar
- | Word => Markup.ML_numeral
- | Int => Markup.ML_numeral
- | Real => Markup.ML_numeral
- | Char => Markup.ML_char
- | String => Markup.ML_string
- | Space => Markup.none
- | Comment => Markup.ML_comment
- | Error _ => Markup.ML_malformed
- | EOF => Markup.none);
+val token_kind_markup =
+ fn Keyword => Markup.ML_keyword
+ | Ident => Markup.ML_ident
+ | LongIdent => Markup.ML_ident
+ | TypeVar => Markup.ML_tvar
+ | Word => Markup.ML_numeral
+ | Int => Markup.ML_numeral
+ | Real => Markup.ML_numeral
+ | Char => Markup.ML_char
+ | String => Markup.ML_string
+ | Space => Markup.none
+ | Comment => Markup.ML_comment
+ | Error _ => Markup.ML_malformed
+ | EOF => Markup.none;
-fun report_token tok = Position.report (markup_of tok) (position_of tok);
+fun report_token (Token ((pos, _), (kind, _))) =
+ Position.report (token_kind_markup kind) pos;
@@ -204,7 +208,7 @@
end;
-(* token source *)
+(* scan tokens *)
local
@@ -224,20 +228,31 @@
scan_ident >> token Ident ||
scan_typevar >> token TypeVar));
+val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
+
fun recover msg =
Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o symbol)
>> (fn cs => [token (Error msg) cs]);
in
-val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
-
fun source src =
Symbol_Pos.source (Position.line 1) src
|> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
val tokenize = Source.of_string #> source #> Source.exhaust;
+fun read_antiq (syms, pos) =
+ (Source.of_list syms
+ |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
+ (SOME (false, fn msg => recover msg >> map Antiquote.Text))
+ |> Source.exhaust
+ |> tap (List.app (Antiquote.report report_token))
+ |> tap Antiquote.check_nesting
+ |> tap (List.app (fn Antiquote.Text tok => ignore (text_of tok) | _ => ())))
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
+
end;
end;
--- a/src/Pure/ML/ml_parse.ML Sun Mar 22 19:43:21 2009 +0100
+++ b/src/Pure/ML/ml_parse.ML Sun Mar 22 21:48:14 2009 +0100
@@ -20,7 +20,7 @@
fun !!! scan =
let
fun get_pos [] = " (past end-of-file!)"
- | get_pos (tok :: _) = T.pos_of tok;
+ | get_pos (tok :: _) = Position.str_of (T.pos_of tok);
fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
| err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_test.ML Sun Mar 22 21:48:14 2009 +0100
@@ -0,0 +1,119 @@
+(* Title: Pure/ML/ml_test.ML
+ Author: Makarius
+
+Test of advanced ML compiler invocation in Poly/ML 5.3.
+*)
+
+signature ML_TEST =
+sig
+ val get_result: Proof.context -> PolyML.parseTree option
+ val eval: bool -> bool -> Position.T -> ML_Lex.token list -> unit
+end
+
+structure ML_Test: ML_TEST =
+struct
+
+(* eval ML source tokens *)
+
+structure Result = GenericDataFun
+(
+ type T = PolyML.parseTree option;
+ val empty = NONE;
+ fun extend _ = NONE;
+ fun merge _ _ = NONE;
+);
+
+val get_result = Result.get o Context.Proof;
+
+fun eval do_run verbose pos toks =
+ let
+ val (print, err) = Output.ml_output;
+
+ val input = toks |> map (fn tok =>
+ (serial (), (String.explode (ML_Lex.text_of tok), ML_Lex.pos_of tok)));
+ val index_pos = Inttab.lookup (Inttab.make (map (apsnd snd) input));
+
+ fun pos_of ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) =
+ (case (index_pos i, index_pos j) of
+ (SOME p, SOME q) => Position.encode_range (p, q)
+ | (SOME p, NONE) => p
+ | _ => Position.line_file line file);
+
+ val in_buffer = ref (map (apsnd fst) input);
+ val current_line = ref (the_default 1 (Position.line_of pos));
+ fun get () =
+ (case ! in_buffer of
+ [] => NONE
+ | (_, []) :: rest => (in_buffer := rest; get ())
+ | (i, c :: cs) :: rest =>
+ (in_buffer := (i, cs) :: rest;
+ if c = #"\n" then current_line := ! current_line + 1 else ();
+ SOME c));
+ fun get_index () = (case ! in_buffer of [] => 0 | (i, _) :: _ => i);
+
+ val out_buffer = ref ([]: string list);
+ fun put s = out_buffer := s :: ! out_buffer;
+ fun output () = implode (rev (! out_buffer));
+
+ fun put_message {message, hard, location, context = _} =
+ (put (if hard then "Error: " else "Warning: ");
+ put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
+ put (Position.str_of (pos_of location) ^ "\n"));
+
+ fun result_fun (parse_tree, code) () =
+ (Context.>> (Result.put parse_tree); (if is_none code then warning "Static Errors" else ()));
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream put,
+ PolyML.Compiler.CPNameSpace ML_Context.name_space,
+ PolyML.Compiler.CPErrorMessageProc put_message,
+ PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPLineOffset get_index,
+ PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
+ (if do_run then [] else [PolyML.Compiler.CPCompilerResultFun result_fun]);
+ val _ =
+ (while not (List.null (! in_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ err (output ()); raise exn);
+ in if verbose then print (output ()) else () end;
+
+
+(* ML test command *)
+
+fun ML_test do_run (txt, pos) =
+ let
+ val _ = Position.report Markup.ML_source pos;
+ val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
+ val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ());
+
+ val _ = Context.setmp_thread_data env_ctxt
+ (fn () => (eval true false Position.none env; Context.thread_data ())) ()
+ |> (fn NONE => () | SOME context' => Context.>> (ML_Context.inherit_env context'));
+ val _ = eval do_run true pos body;
+ val _ = eval true false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
+ in () end;
+
+
+local structure P = OuterParse and K = OuterKeyword in
+
+fun inherit_env (context as Context.Proof lthy) =
+ Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
+ | inherit_env context = context;
+
+val _ =
+ OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
+ (P.ML_source >> (fn src =>
+ Toplevel.generic_theory (ML_Context.exec (fn () => ML_test true src) #> inherit_env)));
+
+val _ =
+ OuterSyntax.command "ML_parse" "advanced ML compiler test (parse only)" (K.tag_ml K.thy_decl)
+ (P.ML_source >> (fn src =>
+ Toplevel.generic_theory (ML_Context.exec (fn () => ML_test false src) #> inherit_env)));
+
+end;
+
+end;
+
--- a/src/Pure/ROOT.ML Sun Mar 22 19:43:21 2009 +0100
+++ b/src/Pure/ROOT.ML Sun Mar 22 21:48:14 2009 +0100
@@ -101,4 +101,6 @@
(*configuration for Proof General*)
cd "ProofGeneral"; use "ROOT.ML"; cd "..";
+if ml_system = "polyml-experimental" then use "ML/ml_test.ML" else ();
use "pure_setup.ML";
+
--- a/src/Pure/Thy/latex.ML Sun Mar 22 19:43:21 2009 +0100
+++ b/src/Pure/Thy/latex.ML Sun Mar 22 21:48:14 2009 +0100
@@ -117,7 +117,7 @@
else if T.is_kind T.Verbatim tok then
let
val (txt, pos) = T.source_position_of tok;
- val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
+ val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
else output_syms s
--- a/src/Pure/Thy/thy_output.ML Sun Mar 22 19:43:21 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Mar 22 21:48:14 2009 +0100
@@ -156,9 +156,9 @@
end
| expand (Antiquote.Open _) = ""
| expand (Antiquote.Close _) = "";
- val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
+ val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
in
- if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
+ if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
else implode (map expand ants)
end;