# HG changeset patch # User haftmann # Date 1237790467 -3600 # Node ID a400b06d03cbfc6546fc35d5340b7170b599844d # Parent 94b74365ceb92446e8cdc83613d878700073d06f# Parent 79e2d95649fe68a5e6a6bf06bdea0dc0557d6a92 merged diff -r 79e2d95649fe -r a400b06d03cb src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Sun Mar 22 20:47:49 2009 +0100 +++ b/src/Pure/General/antiquote.ML Mon Mar 23 07:41:07 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; diff -r 79e2d95649fe -r a400b06d03cb src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sun Mar 22 20:47:49 2009 +0100 +++ b/src/Pure/IsaMakefile Mon Mar 23 07:41:07 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 \ diff -r 79e2d95649fe -r a400b06d03cb src/Pure/ML-Systems/polyml-experimental.ML --- a/src/Pure/ML-Systems/polyml-experimental.ML Sun Mar 22 20:47:49 2009 +0100 +++ b/src/Pure/ML-Systems/polyml-experimental.ML Mon Mar 23 07:41:07 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) diff -r 79e2d95649fe -r a400b06d03cb src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Sun Mar 22 20:47:49 2009 +0100 +++ b/src/Pure/ML/ml_context.ML Mon Mar 23 07:41:07 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; diff -r 79e2d95649fe -r a400b06d03cb src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Sun Mar 22 20:47:49 2009 +0100 +++ b/src/Pure/ML/ml_lex.ML Mon Mar 23 07:41:07 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; diff -r 79e2d95649fe -r a400b06d03cb src/Pure/ML/ml_parse.ML --- a/src/Pure/ML/ml_parse.ML Sun Mar 22 20:47:49 2009 +0100 +++ b/src/Pure/ML/ml_parse.ML Mon Mar 23 07:41:07 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; diff -r 79e2d95649fe -r a400b06d03cb src/Pure/ML/ml_test.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_test.ML Mon Mar 23 07:41:07 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; + diff -r 79e2d95649fe -r a400b06d03cb src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sun Mar 22 20:47:49 2009 +0100 +++ b/src/Pure/ROOT.ML Mon Mar 23 07:41:07 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"; + diff -r 79e2d95649fe -r a400b06d03cb src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Sun Mar 22 20:47:49 2009 +0100 +++ b/src/Pure/Thy/latex.ML Mon Mar 23 07:41:07 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 diff -r 79e2d95649fe -r a400b06d03cb src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sun Mar 22 20:47:49 2009 +0100 +++ b/src/Pure/Thy/thy_output.ML Mon Mar 23 07:41:07 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;