# HG changeset patch # User wenzelm # Date 1243891686 -7200 # Node ID fcd010617e6cfe5790e334f5135a6a77c864abe0 # Parent 9639a6d4d714a0750791282ded8bbb9f645fdbde added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test); diff -r 9639a6d4d714 -r fcd010617e6c src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Jun 01 23:28:05 2009 +0200 +++ b/src/Pure/IsaMakefile Mon Jun 01 23:28:06 2009 +0200 @@ -65,9 +65,10 @@ 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_env.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/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 9639a6d4d714 -r fcd010617e6c src/Pure/ML/ml_compiler.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_compiler.ML Mon Jun 01 23:28:06 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 9639a6d4d714 -r fcd010617e6c 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 Mon Jun 01 23:28:06 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 9639a6d4d714 -r fcd010617e6c src/Pure/ML/ml_test.ML --- a/src/Pure/ML/ml_test.ML Mon Jun 01 23:28:05 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,172 +0,0 @@ -(* Title: Pure/ML/ml_test.ML - Author: Makarius - -Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 762). -*) - -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 *) - -fun position_of ctxt - ({file, startLine = line, startPosition = i, endPosition = j, ...}: PolyML.location) = - (case pairself (ML_Env.token_position 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.>>> (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.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_Env.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.>> (ML_Env.inherit 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 (ML_Env.inherit 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 9639a6d4d714 -r fcd010617e6c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Jun 01 23:28:05 2009 +0200 +++ b/src/Pure/ROOT.ML Mon Jun 01 23:28:06 2009 +0200 @@ -56,6 +56,10 @@ use "General/secure.ML"; use "General/file.ML"; +if ml_system = "polyml-experimental" +then use "ML/ml_compiler_polyml-5.3.ML" +else use "ML/ml_compiler.ML"; + (*core of tactical proof system*) use "net.ML"; use "item_net.ML"; @@ -106,6 +110,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";