# HG changeset patch # User wenzelm # Date 1243946627 -7200 # Node ID 8991eb94fb0b054a70f221a348d5d8b4ab816327 # Parent 380188f5e75e1f0b91607a7521b56057adbc8af7# Parent 7f65653e3d48da6c1a9bff8018ff66b3b15de6c0 merged diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/General/ROOT.ML diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/General/secure.ML --- a/src/Pure/General/secure.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Pure/General/secure.ML Tue Jun 02 14:43:47 2009 +0200 @@ -9,6 +9,7 @@ val set_secure: unit -> unit val is_secure: unit -> bool val deny_secure: string -> unit + val secure_mltext: unit -> unit val use_text: use_context -> int * string -> bool -> string -> unit val use_file: use_context -> bool -> string -> unit val toplevel_pp: string list -> string -> unit diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Pure/IsaMakefile Tue Jun 02 14:43:47 2009 +0200 @@ -55,19 +55,20 @@ General/table.ML General/url.ML General/xml.ML General/yxml.ML \ Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \ Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \ - Isar/constdefs.ML Isar/context_rules.ML \ - Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \ - Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \ - Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \ - Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \ - Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ - Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \ - Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \ - Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML \ - 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_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \ + Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \ + Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \ + Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \ + Isar/local_theory.ML Isar/locale.ML Isar/method.ML \ + Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \ + Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \ + Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \ + Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \ + Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML \ + Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \ + Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML \ + ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \ + ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \ + ML-Systems/install_pp_polyml.ML \ ML-Systems/install_pp_polyml-experimental.ML \ ML-Systems/use_context.ML Proof/extraction.ML \ Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Pure/Isar/ROOT.ML Tue Jun 02 14:43:47 2009 +0200 @@ -24,6 +24,13 @@ use "outer_parse.ML"; use "value_parse.ML"; use "args.ML"; + +(*ML support*) +use "../ML/ml_syntax.ML"; +use "../ML/ml_env.ML"; +if ml_system = "polyml-experimental" +then use "../ML/ml_compiler_polyml-5.3.ML" +else use "../ML/ml_compiler.ML"; use "../ML/ml_context.ML"; (*theory sources*) diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Pure/Isar/attrib.ML Tue Jun 02 14:43:47 2009 +0200 @@ -240,8 +240,7 @@ (* rename_abs *) -val rename_abs : (Context.generic * thm -> Context.generic * thm) parser = - Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars'); +fun rename_abs x = (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')) x; (* unfold / fold definitions *) diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Jun 02 14:43:47 2009 +0200 @@ -296,11 +296,11 @@ (* use ML text *) fun propagate_env (context as Context.Proof lthy) = - Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy) + Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) | propagate_env context = context; fun propagate_env_prf prf = Proof.map_contexts - (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf; + (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf; val _ = OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl) diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/ML-Systems/compiler_polyml-5.0.ML --- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Jun 02 14:43:47 2009 +0200 @@ -1,6 +1,6 @@ (* Title: Pure/ML-Systems/compiler_polyml-5.0.ML -Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1. +Runtime compilation for Poly/ML 5.0 and 5.1. *) fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt = diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Pure/ML-Systems/polyml_common.ML Tue Jun 02 14:43:47 2009 +0200 @@ -17,6 +17,8 @@ val forget_structure = PolyML.Compiler.forgetStructure; +val _ = PolyML.Compiler.forgetValue "print"; + (* Compiler options *) diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/ML/ml_compiler.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_compiler.ML Tue Jun 02 14:43:47 2009 +0200 @@ -0,0 +1,23 @@ +(* Title: Pure/ML/ml_compiler.ML + Author: Makarius + +Runtime compilation -- generic version. +*) + +signature ML_COMPILER = +sig + val eval: bool -> Position.T -> ML_Lex.token list -> unit +end + +structure ML_Compiler: ML_COMPILER = +struct + +fun eval verbose pos toks = + let + val line = the_default 1 (Position.line_of pos); + val file = the_default "ML" (Position.file_of pos); + val text = ML_Lex.flatten toks; + in Secure.use_text ML_Env.local_context (line, file) verbose text end; + +end; + diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/ML/ml_compiler_polyml-5.3.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Jun 02 14:43:47 2009 +0200 @@ -0,0 +1,144 @@ +(* Title: Pure/ML/ml_compiler_polyml-5.3.ML + Author: Makarius + +Advanced runtime compilation for Poly/ML 5.3 (SVN 762). +*) + +signature ML_COMPILER = +sig + val eval: bool -> Position.T -> ML_Lex.token list -> unit +end + +structure ML_Compiler: ML_COMPILER = +struct + +(* original source positions *) + +fun position_of (SOME context) (loc: PolyML.location) = + (case pairself (ML_Env.token_position context) (#startPosition loc, #endPosition loc) of + (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2) + | (SOME pos, NONE) => pos + | _ => Position.line_file (#startLine loc) (#file loc)) + | position_of NONE (loc: PolyML.location) = Position.line_file (#startLine loc) (#file loc); + + +(* parse trees *) + +fun report_parse_tree context depth space = + let + val pos_of = position_of context; + fun report loc (PolyML.PTtype types) = + PolyML.NameSpace.displayTypeExpression (types, depth, space) + |> pretty_ml |> Pretty.from_ML |> Pretty.string_of + |> Position.report_text Markup.ML_typing (pos_of loc) + | report loc (PolyML.PTdeclaredAt decl) = + Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) "" + |> Position.report_text Markup.ML_ref (pos_of loc) + | report _ (PolyML.PTnextSibling tree) = report_tree (tree ()) + | report _ (PolyML.PTfirstChild tree) = report_tree (tree ()) + | report _ _ = () + and report_tree (loc, props) = List.app (report loc) props; + in report_tree end; + + +(* eval ML source tokens *) + +fun eval verbose pos toks = + let + val _ = Secure.secure_mltext (); + val {name_space = space, print, error = err, ...} = ML_Env.local_context; + + + (* input *) + + val input = + if is_none (Context.thread_data ()) then map (pair 0) toks + else Context.>>> (ML_Env.register_tokens toks); + val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input); + + val current_line = ref (the_default 1 (Position.line_of pos)); + + fun get_index () = + the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer)); + + fun get () = + (case ! input_buffer of + [] => NONE + | (_, []) :: rest => (input_buffer := rest; get ()) + | (i, c :: cs) :: rest => + (input_buffer := (i, cs) :: rest; + if c = #"\n" then current_line := ! current_line + 1 else (); + SOME c)); + + + (* output *) + + val output_buffer = ref Buffer.empty; + fun output () = Buffer.content (! output_buffer); + fun put s = change output_buffer (Buffer.add s); + + 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 (position_of (Context.thread_data ()) location) ^ "\n")); + + + (* results *) + + val depth = get_print_depth (); + + fun apply_result {fixes, types, signatures, structures, functors, values} = + let + fun display disp x = + if depth > 0 then + (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n") + else (); + + fun apply_fix (a, b) = + (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b)); + fun apply_type (a, b) = + (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b)); + fun apply_sig (a, b) = + (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b)); + fun apply_struct (a, b) = + (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b)); + fun apply_funct (a, b) = + (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b)); + fun apply_val (a, b) = + (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b)); + in + List.app apply_fix fixes; + List.app apply_type types; + List.app apply_sig signatures; + List.app apply_struct structures; + List.app apply_funct functors; + List.app apply_val values + end; + + fun result_fun (phase1, phase2) () = + (case phase1 of NONE => () + | SOME parse_tree => report_parse_tree (Context.thread_data ()) depth space parse_tree; + case phase2 of NONE => err "Static Errors" + | SOME code => apply_result (code ())); (* FIXME Toplevel.program *) + + + (* compiler invocation *) + + val parameters = + [PolyML.Compiler.CPOutStream put, + PolyML.Compiler.CPNameSpace space, + PolyML.Compiler.CPErrorMessageProc put_message, + PolyML.Compiler.CPLineNo (fn () => ! current_line), + PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)), + PolyML.Compiler.CPLineOffset get_index, + PolyML.Compiler.CPCompilerResultFun result_fun]; + val _ = + (while not (List.null (! input_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; + +end; + diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Pure/ML/ml_context.ML Tue Jun 02 14:43:47 2009 +0200 @@ -19,9 +19,6 @@ val the_global_context: unit -> theory val the_local_context: unit -> Proof.context val exec: (unit -> unit) -> Context.generic -> Context.generic - val inherit_env: Context.generic -> Context.generic -> Context.generic - val name_space: ML_Name_Space.T - val local_context: use_context val stored_thms: thm list ref val ml_store_thm: string * thm -> unit val ml_store_thms: string * thm list -> unit @@ -54,78 +51,6 @@ | NONE => error "Missing context after execution"); -(* ML name space *) - -structure ML_Env = GenericDataFun -( - type T = - ML_Name_Space.valueVal Symtab.table * - ML_Name_Space.typeVal Symtab.table * - ML_Name_Space.fixityVal Symtab.table * - ML_Name_Space.structureVal Symtab.table * - ML_Name_Space.signatureVal Symtab.table * - ML_Name_Space.functorVal Symtab.table; - val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty); - val extend = I; - fun merge _ - ((val1, type1, fixity1, structure1, signature1, functor1), - (val2, type2, fixity2, structure2, signature2, functor2)) : T = - (Symtab.merge (K true) (val1, val2), - Symtab.merge (K true) (type1, type2), - Symtab.merge (K true) (fixity1, fixity2), - Symtab.merge (K true) (structure1, structure2), - Symtab.merge (K true) (signature1, signature2), - Symtab.merge (K true) (functor1, functor2)); -); - -val inherit_env = ML_Env.put o ML_Env.get; - -val name_space: ML_Name_Space.T = - let - fun lookup sel1 sel2 name = - Context.thread_data () - |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (ML_Env.get context)) name) - |> (fn NONE => sel2 ML_Name_Space.global name | some => some); - - fun all sel1 sel2 () = - Context.thread_data () - |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (ML_Env.get context))) - |> append (sel2 ML_Name_Space.global ()) - |> sort_distinct (string_ord o pairself #1); - - fun enter ap1 sel2 entry = - if is_some (Context.thread_data ()) then - Context.>> (ML_Env.map (ap1 (Symtab.update entry))) - else sel2 ML_Name_Space.global entry; - in - {lookupVal = lookup #1 #lookupVal, - lookupType = lookup #2 #lookupType, - lookupFix = lookup #3 #lookupFix, - lookupStruct = lookup #4 #lookupStruct, - lookupSig = lookup #5 #lookupSig, - lookupFunct = lookup #6 #lookupFunct, - enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal, - enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType, - enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix, - enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct, - enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig, - enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct, - allVal = all #1 #allVal, - allType = all #2 #allType, - allFix = all #3 #allFix, - allStruct = all #4 #allStruct, - allSig = all #5 #allSig, - allFunct = all #6 #allFunct} - end; - -val local_context: use_context = - {tune_source = ML_Parse.fix_ints, - name_space = name_space, - str_of_pos = Position.str_of oo Position.line_file, - print = writeln, - error = error}; - - (* theorem bindings *) val stored_thms: thm list ref = ref []; @@ -139,8 +64,8 @@ else if not (ML_Syntax.is_identifier name) then error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") else setmp stored_thms ths' (fn () => - use_text local_context (0, "") true - ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) (); + ML_Compiler.eval true Position.none + (ML_Lex.tokenize ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);"))) (); in () end; val ml_store_thms = ml_store ""; @@ -199,6 +124,7 @@ val struct_name = "Isabelle"; val begin_env = ML_Lex.tokenize ("structure " ^ struct_name ^ " =\nstruct\n"); val end_env = ML_Lex.tokenize "end;"; +val reset_env = ML_Lex.tokenize "structure Isabelle = struct end"; in @@ -240,26 +166,21 @@ fun eval verbose pos txt = let - fun eval_raw p = use_text local_context - (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)); - (*prepare source text*) val _ = Position.report Markup.ML_source pos; 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 (); + val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ()); + val _ = + if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten 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.>> (inherit_env context')); + (fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) () + |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context')); - (*eval ML*) - val _ = eval_raw pos verbose body; - - (*reset static ML environment*) - val _ = eval_raw Position.none false "structure Isabelle = struct end"; + val _ = ML_Compiler.eval verbose pos body; + val _ = ML_Compiler.eval false Position.none reset_env; in () end; end; diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/ML/ml_env.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_env.ML Tue Jun 02 14:43:47 2009 +0200 @@ -0,0 +1,111 @@ +(* Title: Pure/ML/ml_env.ML + Author: Makarius + +Local environment of ML sources and results. +*) + +signature ML_ENV = +sig + val inherit: Context.generic -> Context.generic -> Context.generic + val register_tokens: ML_Lex.token list -> Context.generic -> + (serial * ML_Lex.token) list * Context.generic + val token_position: Context.generic -> serial -> Position.T option + val name_space: ML_Name_Space.T + val local_context: use_context +end + +structure ML_Env: ML_ENV = +struct + +(* context data *) + +structure Env = GenericDataFun +( + type T = + Position.T Inttab.table * + (ML_Name_Space.valueVal Symtab.table * + ML_Name_Space.typeVal Symtab.table * + ML_Name_Space.fixityVal Symtab.table * + ML_Name_Space.structureVal Symtab.table * + ML_Name_Space.signatureVal Symtab.table * + ML_Name_Space.functorVal Symtab.table); + val empty = + (Inttab.empty, + (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty)); + val extend = I; + fun merge _ + ((toks1, (val1, type1, fixity1, structure1, signature1, functor1)), + (toks2, (val2, type2, fixity2, structure2, signature2, functor2))) : T = + (Inttab.merge (K true) (toks1, toks2), + (Symtab.merge (K true) (val1, val2), + Symtab.merge (K true) (type1, type2), + Symtab.merge (K true) (fixity1, fixity2), + Symtab.merge (K true) (structure1, structure2), + Symtab.merge (K true) (signature1, signature2), + Symtab.merge (K true) (functor1, functor2))); +); + +val inherit = Env.put o Env.get; + + +(* source tokens *) + +fun register_tokens toks context = + let + val regs = map (fn tok => (serial (), tok)) toks; + val context' = context + |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs)); + in (regs, context') end; + +val token_position = Inttab.lookup o #1 o Env.get; + + +(* results *) + +val name_space: ML_Name_Space.T = + let + fun lookup sel1 sel2 name = + Context.thread_data () + |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name) + |> (fn NONE => sel2 ML_Name_Space.global name | some => some); + + fun all sel1 sel2 () = + Context.thread_data () + |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context)))) + |> append (sel2 ML_Name_Space.global ()) + |> sort_distinct (string_ord o pairself #1); + + fun enter ap1 sel2 entry = + if is_some (Context.thread_data ()) then + Context.>> (Env.map (apsnd (ap1 (Symtab.update entry)))) + else sel2 ML_Name_Space.global entry; + in + {lookupVal = lookup #1 #lookupVal, + lookupType = lookup #2 #lookupType, + lookupFix = lookup #3 #lookupFix, + lookupStruct = lookup #4 #lookupStruct, + lookupSig = lookup #5 #lookupSig, + lookupFunct = lookup #6 #lookupFunct, + enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal, + enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType, + enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix, + enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct, + enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig, + enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct, + allVal = all #1 #allVal, + allType = all #2 #allType, + allFix = all #3 #allFix, + allStruct = all #4 #allStruct, + allSig = all #5 #allSig, + allFunct = all #6 #allFunct} + end; + +val local_context: use_context = + {tune_source = ML_Parse.fix_ints, + name_space = name_space, + str_of_pos = Position.str_of oo Position.line_file, + print = writeln, + error = error}; + +end; + diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Pure/ML/ml_lex.ML Tue Jun 02 14:43:47 2009 +0200 @@ -18,6 +18,7 @@ val kind_of: token -> token_kind val content_of: token -> string val text_of: token -> string + val flatten: token list -> string val report_token: token -> unit val keywords: string list val source: (Symbol.symbol, 'a) Source.source -> @@ -73,6 +74,8 @@ Error msg => error msg | _ => Symbol.escape (content_of tok)); +val flatten = implode o map text_of; + fun is_regular (Token (_, (Error _, _))) = false | is_regular (Token (_, (EOF, _))) = false | is_regular _ = true; diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/ML/ml_test.ML --- a/src/Pure/ML/ml_test.ML Tue Jun 02 14:37:05 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,191 +0,0 @@ -(* Title: Pure/ML/ml_test.ML - Author: Makarius - -Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 744). -*) - -signature ML_TEST = -sig - val position_of: Proof.context -> PolyML.location -> Position.T - val eval: bool -> Position.T -> ML_Lex.token list -> unit -end - -structure ML_Test: ML_TEST = -struct - -(* extra ML environment *) - -structure Extra_Env = GenericDataFun -( - type T = Position.T Inttab.table; (*position of registered tokens*) - val empty = Inttab.empty; - val extend = I; - fun merge _ = Inttab.merge (K true); -); - -fun inherit_env context = - ML_Context.inherit_env context #> - Extra_Env.put (Extra_Env.get context); - -fun register_tokens toks context = - let - val regs = map (fn tok => (serial (), tok)) toks; - val context' = context - |> Extra_Env.map (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs); - in (regs, context') end; - -fun position_of ctxt - ({file, startLine = line, startPosition = i, endPosition = j, ...}: PolyML.location) = - (case pairself (Inttab.lookup (Extra_Env.get (Context.Proof ctxt))) (i, j) of - (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2) - | (SOME pos, NONE) => pos - | _ => Position.line_file line file); - - -(* parse trees *) - -fun report_parse_tree context depth space = - let - val pos_of = position_of (Context.proof_of context); - fun report loc (PolyML.PTtype types) = - PolyML.NameSpace.displayTypeExpression (types, depth, space) - |> pretty_ml |> Pretty.from_ML |> Pretty.string_of - |> Position.report_text Markup.ML_typing (pos_of loc) - | report loc (PolyML.PTdeclaredAt decl) = - Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) "" - |> Position.report_text Markup.ML_ref (pos_of loc) - | report _ (PolyML.PTnextSibling tree) = report_tree (tree ()) - | report _ (PolyML.PTfirstChild tree) = report_tree (tree ()) - | report _ _ = () - and report_tree (loc, props) = List.app (report loc) props; - in report_tree end; - - -(* eval ML source tokens *) - -fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks = - let - (* input *) - - val input = Context.>>> (register_tokens toks); - val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input); - - val current_line = ref (the_default 1 (Position.line_of pos)); - - fun get_index () = - the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer)); - - fun get () = - (case ! input_buffer of - [] => NONE - | (_, []) :: rest => (input_buffer := rest; get ()) - | (i, c :: cs) :: rest => - (input_buffer := (i, cs) :: rest; - if c = #"\n" then current_line := ! current_line + 1 else (); - SOME c)); - - - (* output *) - - val output_buffer = ref Buffer.empty; - fun output () = Buffer.content (! output_buffer); - fun put s = change output_buffer (Buffer.add s); - - 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 - (position_of (Context.proof_of (the (Context.thread_data ()))) location) ^ "\n")); - - - (* results *) - - val depth = get_print_depth (); - - fun apply_result {fixes, types, signatures, structures, functors, values} = - let - fun display disp x = - if depth > 0 then - (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n") - else (); - - fun apply_fix (a, b) = - (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b)); - fun apply_type (a, b) = - (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b)); - fun apply_sig (a, b) = - (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b)); - fun apply_struct (a, b) = - (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b)); - fun apply_funct (a, b) = - (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b)); - fun apply_val (a, b) = - (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b)); - in - List.app apply_fix fixes; - List.app apply_type types; - List.app apply_sig signatures; - List.app apply_struct structures; - List.app apply_funct functors; - List.app apply_val values - end; - - fun result_fun (phase1, phase2) () = - (case phase1 of NONE => () - | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) depth space parse_tree; - case phase2 of NONE => error "Static Errors" - | SOME code => apply_result (Toplevel.program code)); - - - (* compiler invocation *) - - val parameters = - [PolyML.Compiler.CPOutStream put, - PolyML.Compiler.CPNameSpace space, - PolyML.Compiler.CPErrorMessageProc put_message, - PolyML.Compiler.CPLineNo (fn () => ! current_line), - PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)), - PolyML.Compiler.CPLineOffset get_index, - PolyML.Compiler.CPCompilerResultFun result_fun]; - val _ = - (while not (List.null (! input_buffer)) do - PolyML.compiler (get, parameters) ()) - handle exn => - (put ("Exception- " ^ General.exnMessage exn ^ " raised"); - error (output ()); raise exn); - in if verbose then print (output ()) else () end; - -val eval = use_text ML_Context.local_context; - - -(* ML test command *) - -fun ML_test (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 false Position.none env; Context.thread_data ())) () - |> (fn NONE => () | SOME context' => Context.>> (inherit_env context')); - val _ = eval true pos body; - val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end"); - in () end; - - -local structure P = OuterParse and K = OuterKeyword in - -fun propagate_env (context as Context.Proof lthy) = - Context.Proof (LocalTheory.map_contexts (inherit_env context) lthy) - | propagate_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 src) #> propagate_env))); - -end; - -end; - diff -r 380188f5e75e -r 8991eb94fb0b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Pure/ROOT.ML Tue Jun 02 14:43:47 2009 +0200 @@ -46,7 +46,6 @@ use "Syntax/syntax.ML"; use "type_infer.ML"; -use "ML/ml_syntax.ML"; (*core of tactical proof system*) use "net.ML"; @@ -98,6 +97,5 @@ (*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 380188f5e75e -r 8991eb94fb0b src/Tools/Compute_Oracle/am_compiler.ML --- a/src/Tools/Compute_Oracle/am_compiler.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Tools/Compute_Oracle/am_compiler.ML Tue Jun 02 14:43:47 2009 +0200 @@ -185,7 +185,7 @@ in compiled_rewriter := NONE; - use_text ML_Context.local_context (1, "") false (!buffer); + use_text ML_Env.local_context (1, "") false (!buffer); case !compiled_rewriter of NONE => raise (Compile "cannot communicate with compiled function") | SOME r => (compiled_rewriter := NONE; r) diff -r 380188f5e75e -r 8991eb94fb0b src/Tools/Compute_Oracle/am_sml.ML --- a/src/Tools/Compute_Oracle/am_sml.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Tools/Compute_Oracle/am_sml.ML Tue Jun 02 14:43:47 2009 +0200 @@ -492,7 +492,7 @@ fun writeTextFile name s = File.write (Path.explode name) s -fun use_source src = use_text ML_Context.local_context (1, "") false src +fun use_source src = use_text ML_Env.local_context (1, "") false src fun compile cache_patterns const_arity eqs = let diff -r 380188f5e75e -r 8991eb94fb0b src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Tue Jun 02 14:37:05 2009 +0200 +++ b/src/Tools/code/code_ml.ML Tue Jun 02 14:43:47 2009 +0200 @@ -1081,7 +1081,7 @@ fun isar_seri_sml module_name = Code_Target.parse_args (Scan.succeed ()) #> (fn () => serialize_ml target_SML - (SOME (use_text ML_Context.local_context (1, "generated code") false)) + (SOME (use_text ML_Env.local_context (1, "generated code") false)) pr_sml_module pr_sml_stmt module_name); fun isar_seri_ocaml module_name =