explicit debug flag for ML compiler;
authorwenzelm
Mon Aug 17 16:27:12 2015 +0200 (2015-08-17)
changeset 6095610d463883dc2
parent 60955 65149ae760a0
child 60957 574254152856
explicit debug flag for ML compiler;
src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Pure/General/secure.ML
src/Pure/Isar/isar_syn.ML
src/Pure/ML-Systems/compiler_polyml.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ML/ml_file.ML
src/Pure/ROOT.ML
src/Pure/Tools/debugger.ML
src/Tools/Code/code_runtime.ML
src/Tools/Spec_Check/spec_check.ML
     1.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Mon Aug 17 15:29:30 2015 +0200
     1.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Mon Aug 17 16:27:12 2015 +0200
     1.3 @@ -184,7 +184,8 @@
     1.4  
     1.5      in
     1.6          compiled_rewriter := NONE;      
     1.7 -        use_text ML_Env.local_context (1, "") false (!buffer);
     1.8 +        use_text ML_Env.local_context
     1.9 +          {line = 1, file = "", verbose = false, debug = false} (!buffer);
    1.10          case !compiled_rewriter of 
    1.11              NONE => raise (Compile "cannot communicate with compiled function")
    1.12            | SOME r => (compiled_rewriter := NONE; r)
     2.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Mon Aug 17 15:29:30 2015 +0200
     2.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Mon Aug 17 16:27:12 2015 +0200
     2.3 @@ -485,7 +485,8 @@
     2.4  
     2.5  fun writeTextFile name s = File.write (Path.explode name) s
     2.6  
     2.7 -fun use_source src = use_text ML_Env.local_context (1, "") false src
     2.8 +fun use_source src =
     2.9 +  use_text ML_Env.local_context {line = 1, file = "", verbose = false, debug = false} src
    2.10      
    2.11  fun compile rules = 
    2.12      let
     3.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Aug 17 15:29:30 2015 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Aug 17 16:27:12 2015 +0200
     3.3 @@ -205,7 +205,9 @@
     3.4    File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
     3.5  
     3.6  fun exec verbose code =
     3.7 -  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
     3.8 +  ML_Context.exec (fn () =>
     3.9 +    Secure.use_text ML_Env.local_context
    3.10 +      {line = 0, file = "generated code", verbose = verbose, debug = false} code)
    3.11  
    3.12  fun with_overlord_dir name f =
    3.13    let
     4.1 --- a/src/Pure/General/secure.ML	Mon Aug 17 15:29:30 2015 +0200
     4.2 +++ b/src/Pure/General/secure.ML	Mon Aug 17 16:27:12 2015 +0200
     4.3 @@ -10,8 +10,9 @@
     4.4    val is_secure: unit -> bool
     4.5    val deny_secure: string -> unit
     4.6    val secure_mltext: unit -> unit
     4.7 -  val use_text: use_context -> int * string -> bool -> string -> unit
     4.8 -  val use_file: use_context -> bool -> string -> unit
     4.9 +  val use_text: use_context ->
    4.10 +    {line: int, file: string, verbose: bool, debug: bool} -> string -> unit
    4.11 +  val use_file: use_context -> {verbose: bool, debug: bool} -> string -> unit
    4.12    val toplevel_pp: string list -> string -> unit
    4.13  end;
    4.14  
    4.15 @@ -37,10 +38,9 @@
    4.16  val raw_use_file = use_file;
    4.17  val raw_toplevel_pp = toplevel_pp;
    4.18  
    4.19 -fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt);
    4.20 -fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name);
    4.21 +fun use_text context flags (text: string) = (secure_mltext (); raw_use_text context flags text);
    4.22 +fun use_file context flags (file: string) = (secure_mltext (); raw_use_file context flags file);
    4.23  
    4.24  fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
    4.25  
    4.26  end;
    4.27 -
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Aug 17 15:29:30 2015 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 17 16:27:12 2015 +0200
     5.3 @@ -209,9 +209,9 @@
     5.4          let
     5.5            val ([{lines, pos, ...}], thy') = files thy;
     5.6            val source = Input.source true (cat_lines lines) (pos, pos);
     5.7 -          val flags =
     5.8 +          val flags: ML_Compiler.flags =
     5.9              {SML = true, exchange = false, redirect = true, verbose = true,
    5.10 -              writeln = writeln, warning = warning};
    5.11 +              debug = NONE, writeln = writeln, warning = warning};
    5.12          in
    5.13            thy' |> Context.theory_map
    5.14              (ML_Context.exec (fn () => ML_Context.eval_source flags source))
    5.15 @@ -221,9 +221,9 @@
    5.16    Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
    5.17      (Parse.ML_source >> (fn source =>
    5.18        let
    5.19 -        val flags =
    5.20 +        val flags: ML_Compiler.flags =
    5.21            {SML = true, exchange = true, redirect = false, verbose = true,
    5.22 -            writeln = writeln, warning = warning};
    5.23 +            debug = NONE, writeln = writeln, warning = warning};
    5.24        in
    5.25          Toplevel.theory
    5.26            (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
    5.27 @@ -233,9 +233,9 @@
    5.28    Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment"
    5.29      (Parse.ML_source >> (fn source =>
    5.30        let
    5.31 -        val flags =
    5.32 +        val flags: ML_Compiler.flags =
    5.33            {SML = false, exchange = true, redirect = false, verbose = true,
    5.34 -            writeln = writeln, warning = warning};
    5.35 +            debug = NONE, writeln = writeln, warning = warning};
    5.36        in
    5.37          Toplevel.generic_theory
    5.38            (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
     6.1 --- a/src/Pure/ML-Systems/compiler_polyml.ML	Mon Aug 17 15:29:30 2015 +0200
     6.2 +++ b/src/Pure/ML-Systems/compiler_polyml.ML	Mon Aug 17 16:27:12 2015 +0200
     6.3 @@ -12,11 +12,11 @@
     6.4  in
     6.5  
     6.6  fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
     6.7 -    (line, file) verbose txt =
     6.8 +    {line, file, verbose, debug} text =
     6.9    let
    6.10      val current_line = Unsynchronized.ref line;
    6.11      val in_buffer =
    6.12 -      Unsynchronized.ref (String.explode (tune_source (ml_positions line file txt)));
    6.13 +      Unsynchronized.ref (String.explode (tune_source (ml_positions line file text)));
    6.14      val out_buffer = Unsynchronized.ref ([]: string list);
    6.15      fun output () = drop_newline (implode (rev (! out_buffer)));
    6.16  
    6.17 @@ -38,7 +38,8 @@
    6.18        PolyML.Compiler.CPErrorMessageProc put_message,
    6.19        PolyML.Compiler.CPLineNo (fn () => ! current_line),
    6.20        PolyML.Compiler.CPFileName file,
    6.21 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
    6.22 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
    6.23 +      ML_Compiler_Parameters.debug debug;
    6.24      val _ =
    6.25        (while not (List.null (! in_buffer)) do
    6.26          PolyML.compiler (get, parameters) ())
    6.27 @@ -49,10 +50,10 @@
    6.28            error (output ()); reraise exn);
    6.29    in if verbose then print (output ()) else () end;
    6.30  
    6.31 -fun use_file context verbose file =
    6.32 +fun use_file context {verbose, debug} file =
    6.33    let
    6.34      val instream = TextIO.openIn file;
    6.35 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    6.36 -  in use_text context (1, file) verbose txt end;
    6.37 +    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    6.38 +  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    6.39  
    6.40  end;
     7.1 --- a/src/Pure/ML-Systems/polyml.ML	Mon Aug 17 15:29:30 2015 +0200
     7.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Aug 17 16:27:12 2015 +0200
     7.3 @@ -177,6 +177,10 @@
     7.4    val display_val = pretty_ml o PolyML.NameSpace.displayVal;
     7.5  end;
     7.6  
     7.7 +use "ML-Systems/ml_compiler_parameters.ML";
     7.8 +if ML_System.name = "polyml-5.5.3"
     7.9 +then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
    7.10 +
    7.11  use "ML-Systems/use_context.ML";
    7.12  use "ML-Systems/ml_positions.ML";
    7.13  use "ML-Systems/compiler_polyml.ML";
    7.14 @@ -191,12 +195,8 @@
    7.15  if ML_System.name = "polyml-5.5.3"
    7.16  then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
    7.17  
    7.18 -use "ML-Systems/ml_compiler_parameters.ML";
    7.19 -if ML_System.name = "polyml-5.5.3"
    7.20 -then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
    7.21 -
    7.22  fun toplevel_pp context (_: string list) pp =
    7.23 -  use_text context (1, "pp") false
    7.24 +  use_text context {line = 1, file = "pp", verbose = false, debug = false}
    7.25      ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
    7.26  
    7.27  fun ml_make_string struct_name =
     8.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Aug 17 15:29:30 2015 +0200
     8.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Aug 17 16:27:12 2015 +0200
     8.3 @@ -82,7 +82,8 @@
     8.4  
     8.5  (* ML command execution *)
     8.6  
     8.7 -fun use_text ({tune_source, print, error, ...}: use_context) (line, file) verbose txt =
     8.8 +fun use_text ({tune_source, print, error, ...}: use_context)
     8.9 +    {line, file, verbose, debug = _: bool} text =
    8.10    let
    8.11      val ref out_orig = Control.Print.out;
    8.12  
    8.13 @@ -93,7 +94,7 @@
    8.14        in String.substring (str, 0, Int.max (0, size str - 1)) end;
    8.15    in
    8.16      Control.Print.out := out;
    8.17 -    Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file txt)))
    8.18 +    Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file text)))
    8.19        handle exn =>
    8.20          (Control.Print.out := out_orig;
    8.21            error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
    8.22 @@ -101,11 +102,11 @@
    8.23      if verbose then print (output ()) else ()
    8.24    end;
    8.25  
    8.26 -fun use_file context verbose file =
    8.27 +fun use_file context {verbose, debug} file =
    8.28    let
    8.29      val instream = TextIO.openIn file;
    8.30 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    8.31 -  in use_text context (1, file) verbose txt end;
    8.32 +    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    8.33 +  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    8.34  
    8.35  
    8.36  (* toplevel pretty printing *)
    8.37 @@ -123,7 +124,7 @@
    8.38    in pprint end;
    8.39  
    8.40  fun toplevel_pp context path pp =
    8.41 -  use_text context (1, "pp") false
    8.42 +  use_text context {line = 1, file = "pp", verbose = false, debug = false}
    8.43      ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
    8.44        "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
    8.45  
     9.1 --- a/src/Pure/ML/ml_compiler.ML	Mon Aug 17 15:29:30 2015 +0200
     9.2 +++ b/src/Pure/ML/ml_compiler.ML	Mon Aug 17 16:27:12 2015 +0200
     9.3 @@ -8,7 +8,7 @@
     9.4  sig
     9.5    type flags =
     9.6      {SML: bool, exchange: bool, redirect: bool, verbose: bool,
     9.7 -      writeln: string -> unit, warning: string -> unit}
     9.8 +      debug: bool option, writeln: string -> unit, warning: string -> unit}
     9.9    val flags: flags
    9.10    val verbose: bool -> flags -> flags
    9.11    val eval: flags -> Position.T -> ML_Lex.token list -> unit
    9.12 @@ -19,23 +19,26 @@
    9.13  
    9.14  type flags =
    9.15    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    9.16 -    writeln: string -> unit, warning: string -> unit};
    9.17 +    debug: bool option, writeln: string -> unit, warning: string -> unit};
    9.18  
    9.19  val flags: flags =
    9.20    {SML = false, exchange = false, redirect = false, verbose = false,
    9.21 -    writeln = writeln, warning = warning};
    9.22 +    debug = NONE, writeln = writeln, warning = warning};
    9.23  
    9.24  fun verbose b (flags: flags) =
    9.25 -  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b,
    9.26 -    writeln = #writeln flags, warning = #warning flags};
    9.27 +  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
    9.28 +    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
    9.29  
    9.30  fun eval (flags: flags) pos toks =
    9.31    let
    9.32      val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
    9.33      val line = the_default 1 (Position.line_of pos);
    9.34      val file = the_default "ML" (Position.file_of pos);
    9.35 +    val debug = the_default false (#debug flags);
    9.36      val text = ML_Lex.flatten toks;
    9.37 -  in Secure.use_text ML_Env.local_context (line, file) (#verbose flags) text end;
    9.38 +  in
    9.39 +    Secure.use_text ML_Env.local_context
    9.40 +      {line = line, file = file, verbose = #verbose flags, debug = debug} text
    9.41 +  end;
    9.42  
    9.43  end;
    9.44 -
    10.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Aug 17 15:29:30 2015 +0200
    10.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Aug 17 16:27:12 2015 +0200
    10.3 @@ -225,6 +225,11 @@
    10.4  
    10.5      (* compiler invocation *)
    10.6  
    10.7 +    val debug =
    10.8 +      (case #debug flags of
    10.9 +        SOME debug => debug
   10.10 +      | NONE => ML_Options.debugger_enabled opt_context);
   10.11 +
   10.12      val parameters =
   10.13       [PolyML.Compiler.CPOutStream write,
   10.14        PolyML.Compiler.CPNameSpace space,
   10.15 @@ -235,7 +240,8 @@
   10.16        PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
   10.17        PolyML.Compiler.CPCompilerResultFun result_fun,
   10.18        PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
   10.19 -     ML_Compiler_Parameters.debug (ML_Options.debugger_enabled opt_context);
   10.20 +     ML_Compiler_Parameters.debug debug;
   10.21 +
   10.22      val _ =
   10.23        (while not (List.null (! input_buffer)) do
   10.24          PolyML.compiler (get, parameters) ())
   10.25 @@ -257,4 +263,3 @@
   10.26    end;
   10.27  
   10.28  end;
   10.29 -
    11.1 --- a/src/Pure/ML/ml_file.ML	Mon Aug 17 15:29:30 2015 +0200
    11.2 +++ b/src/Pure/ML/ml_file.ML	Mon Aug 17 16:27:12 2015 +0200
    11.3 @@ -14,9 +14,9 @@
    11.4            val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
    11.5            val provide = Resources.provide (src_path, digest);
    11.6            val source = Input.source true (cat_lines lines) (pos, pos);
    11.7 -          val flags =
    11.8 +          val flags: ML_Compiler.flags =
    11.9              {SML = false, exchange = false, redirect = true, verbose = true,
   11.10 -              writeln = writeln, warning = warning};
   11.11 +              debug = NONE, writeln = writeln, warning = warning};
   11.12          in
   11.13            gthy
   11.14            |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    12.1 --- a/src/Pure/ROOT.ML	Mon Aug 17 15:29:30 2015 +0200
    12.2 +++ b/src/Pure/ROOT.ML	Mon Aug 17 16:27:12 2015 +0200
    12.3 @@ -41,10 +41,10 @@
    12.4  val use_text = Secure.use_text;
    12.5  val use_file = Secure.use_file;
    12.6  
    12.7 -fun use s =
    12.8 -  Position.setmp_thread_data (Position.file_only s)
    12.9 +fun use file =
   12.10 +  Position.setmp_thread_data (Position.file_only file)
   12.11      (fn () =>
   12.12 -      Secure.use_file ML_Parse.global_context true s
   12.13 +      Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
   12.14          handle ERROR msg => (writeln msg; error "ML error")) ();
   12.15  
   12.16  val toplevel_pp = Secure.toplevel_pp;
    13.1 --- a/src/Pure/Tools/debugger.ML	Mon Aug 17 15:29:30 2015 +0200
    13.2 +++ b/src/Pure/Tools/debugger.ML	Mon Aug 17 16:27:12 2015 +0200
    13.3 @@ -144,13 +144,12 @@
    13.4  fun evaluate {SML, verbose} =
    13.5    ML_Context.eval
    13.6      {SML = SML, exchange = false, redirect = false, verbose = verbose,
    13.7 -      writeln = writeln_message, warning = warning_message}
    13.8 +      debug = SOME false, writeln = writeln_message, warning = warning_message}
    13.9      Position.none;
   13.10  
   13.11  fun eval_setup thread_name index SML context =
   13.12    context
   13.13    |> Context_Position.set_visible_generic false
   13.14 -  |> Config.put_generic ML_Options.debugger false
   13.15    |> ML_Env.add_name_space {SML = SML}
   13.16        (ML_Debugger.debug_name_space (the_debug_state thread_name index));
   13.17  
    14.1 --- a/src/Tools/Code/code_runtime.ML	Mon Aug 17 15:29:30 2015 +0200
    14.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Aug 17 16:27:12 2015 +0200
    14.3 @@ -80,8 +80,10 @@
    14.4  val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
    14.5  
    14.6  fun exec ctxt verbose code =
    14.7 -  (if Config.get ctxt trace then tracing code else ();
    14.8 -  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));
    14.9 + (if Config.get ctxt trace then tracing code else ();
   14.10 +  ML_Context.exec (fn () =>
   14.11 +    Secure.use_text ML_Env.local_context
   14.12 +      {line = 0, file = "generated code", verbose = verbose, debug = false} code));
   14.13  
   14.14  fun value ctxt (get, put, put_ml) (prelude, value) =
   14.15    let
   14.16 @@ -538,8 +540,10 @@
   14.17    let
   14.18      val thy' = Loaded_Values.put [] thy;
   14.19      val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
   14.20 -    val _ = Secure.use_text notifying_context
   14.21 -      (0, Path.implode filepath) false (File.read filepath);
   14.22 +    val _ =
   14.23 +      Secure.use_text notifying_context
   14.24 +        {line = 0, file = Path.implode filepath, verbose = false, debug = false}
   14.25 +        (File.read filepath);
   14.26      val thy'' = Context.the_theory (Context.the_thread_data ());
   14.27      val names = Loaded_Values.get thy'';
   14.28    in (names, thy'') end;
    15.1 --- a/src/Tools/Spec_Check/spec_check.ML	Mon Aug 17 15:29:30 2015 +0200
    15.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Mon Aug 17 16:27:12 2015 +0200
    15.3 @@ -135,7 +135,9 @@
    15.4        error = #error ML_Env.local_context}
    15.5      val _ =
    15.6        Context.setmp_thread_data (SOME (Context.Proof ctxt))
    15.7 -        (fn () => Secure.use_text use_context (0, "generated code") true s) ()
    15.8 +        (fn () =>
    15.9 +          Secure.use_text use_context
   15.10 +            {line = 0, file = "generated code", verbose = true, debug = false} s) ()
   15.11    in
   15.12      Gen_Construction.parse_pred (! return)
   15.13    end;
   15.14 @@ -143,7 +145,9 @@
   15.15  (*call the compiler and run the test*)
   15.16  fun run_test ctxt s =
   15.17    Context.setmp_thread_data (SOME (Context.Proof ctxt))
   15.18 -    (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false s) ();
   15.19 +    (fn () =>
   15.20 +      Secure.use_text ML_Env.local_context
   15.21 +        {line = 0, file = "generated code", verbose = false, debug = false} s) ();
   15.22  
   15.23  (*split input into tokens*)
   15.24  fun input_split s =