clarified modules;
authorwenzelm
Tue Mar 01 22:11:36 2016 +0100 (2016-03-01)
changeset 62494b90109b2487c
parent 62493 dd154240a53c
child 62495 83db706d7771
clarified modules;
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/ML/ml_env.ML
src/Pure/RAW/ROOT_polyml.ML
src/Pure/RAW/compiler_polyml.ML
src/Pure/RAW/ml_compiler0.ML
src/Pure/ROOT
src/Pure/ROOT.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	Tue Mar 01 21:10:29 2016 +0100
     1.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Tue Mar 01 22:11:36 2016 +0100
     1.3 @@ -184,7 +184,7 @@
     1.4  
     1.5      in
     1.6          compiled_rewriter := NONE;      
     1.7 -        use_text ML_Env.local_context
     1.8 +        ML_Compiler0.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")
     2.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Tue Mar 01 21:10:29 2016 +0100
     2.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Tue Mar 01 22:11:36 2016 +0100
     2.3 @@ -486,7 +486,8 @@
     2.4  fun writeTextFile name s = File.write (Path.explode name) s
     2.5  
     2.6  fun use_source src =
     2.7 -  use_text ML_Env.local_context {line = 1, file = "", verbose = false, debug = false} src
     2.8 +  ML_Compiler0.use_text ML_Env.local_context
     2.9 +    {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	Tue Mar 01 21:10:29 2016 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Mar 01 22:11:36 2016 +0100
     3.3 @@ -206,7 +206,7 @@
     3.4  
     3.5  fun exec verbose code =
     3.6    ML_Context.exec (fn () =>
     3.7 -    use_text ML_Env.local_context
     3.8 +    ML_Compiler0.use_text ML_Env.local_context
     3.9        {line = 0, file = "generated code", verbose = verbose, debug = false} code)
    3.10  
    3.11  fun with_overlord_dir name f =
     4.1 --- a/src/Pure/ML/ml_env.ML	Tue Mar 01 21:10:29 2016 +0100
     4.2 +++ b/src/Pure/ML/ml_env.ML	Tue Mar 01 22:11:36 2016 +0100
     4.3 @@ -14,7 +14,7 @@
     4.4    val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
     4.5    val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
     4.6    val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
     4.7 -  val local_context: use_context
     4.8 +  val local_context: ML_Compiler0.context
     4.9    val local_name_space: ML_Name_Space.T
    4.10    val check_functor: string -> unit
    4.11  end
    4.12 @@ -162,7 +162,7 @@
    4.13      allFunct     = all #6 #allFunct}
    4.14    end;
    4.15  
    4.16 -val local_context: use_context =
    4.17 +val local_context: ML_Compiler0.context =
    4.18   {name_space = name_space {SML = false, exchange = false},
    4.19    here = Position.here oo Position.line_file,
    4.20    print = writeln,
     5.1 --- a/src/Pure/RAW/ROOT_polyml.ML	Tue Mar 01 21:10:29 2016 +0100
     5.2 +++ b/src/Pure/RAW/ROOT_polyml.ML	Tue Mar 01 22:11:36 2016 +0100
     5.3 @@ -167,7 +167,7 @@
     5.4  then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
     5.5  
     5.6  use "RAW/ml_positions.ML";
     5.7 -use "RAW/compiler_polyml.ML";
     5.8 +use "RAW/ml_compiler0.ML";
     5.9  
    5.10  PolyML.Compiler.reportUnreferencedIds := true;
    5.11  PolyML.Compiler.printInAlphabeticalOrder := false;
     6.1 --- a/src/Pure/RAW/compiler_polyml.ML	Tue Mar 01 21:10:29 2016 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,84 +0,0 @@
     6.4 -(*  Title:      Pure/RAW/compiler_polyml.ML
     6.5 -
     6.6 -Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
     6.7 -*)
     6.8 -
     6.9 -type use_context =
    6.10 - {name_space: ML_Name_Space.T,
    6.11 -  here: int -> string -> string,
    6.12 -  print: string -> unit,
    6.13 -  error: string -> unit};
    6.14 -
    6.15 -local
    6.16 -
    6.17 -val boot_context: use_context =
    6.18 - {name_space = ML_Name_Space.global,
    6.19 -  here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
    6.20 -  print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
    6.21 -  error = fn s => error s};
    6.22 -
    6.23 -fun drop_newline s =
    6.24 -  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    6.25 -  else s;
    6.26 -
    6.27 -in
    6.28 -
    6.29 -fun use_text ({name_space, here, print, error, ...}: use_context)
    6.30 -    {line, file, verbose, debug} text =
    6.31 -  let
    6.32 -    val _ = Secure.deny_ml ();
    6.33 -
    6.34 -    val current_line = Unsynchronized.ref line;
    6.35 -    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
    6.36 -    val out_buffer = Unsynchronized.ref ([]: string list);
    6.37 -    fun output () = drop_newline (implode (rev (! out_buffer)));
    6.38 -
    6.39 -    fun get () =
    6.40 -      (case ! in_buffer of
    6.41 -        [] => NONE
    6.42 -      | c :: cs =>
    6.43 -          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    6.44 -    fun put s = out_buffer := s :: ! out_buffer;
    6.45 -    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
    6.46 -     (put (if hard then "Error: " else "Warning: ");
    6.47 -      PolyML.prettyPrint (put, 76) msg1;
    6.48 -      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
    6.49 -      put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
    6.50 -
    6.51 -    val parameters =
    6.52 -     [PolyML.Compiler.CPOutStream put,
    6.53 -      PolyML.Compiler.CPNameSpace name_space,
    6.54 -      PolyML.Compiler.CPErrorMessageProc put_message,
    6.55 -      PolyML.Compiler.CPLineNo (fn () => ! current_line),
    6.56 -      PolyML.Compiler.CPFileName file,
    6.57 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
    6.58 -      ML_Compiler_Parameters.debug debug;
    6.59 -    val _ =
    6.60 -      (while not (List.null (! in_buffer)) do
    6.61 -        PolyML.compiler (get, parameters) ())
    6.62 -      handle exn =>
    6.63 -        if Exn.is_interrupt exn then reraise exn
    6.64 -        else
    6.65 -         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    6.66 -          error (output ()); reraise exn);
    6.67 -  in if verbose then print (output ()) else () end;
    6.68 -
    6.69 -fun use_file context {verbose, debug} file =
    6.70 -  let
    6.71 -    val instream = TextIO.openIn file;
    6.72 -    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    6.73 -  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    6.74 -
    6.75 -
    6.76 -fun use_debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
    6.77 -  | use_debug_option (SOME debug) = debug;
    6.78 -
    6.79 -fun use_operations (use_ : bool option -> string -> unit) =
    6.80 -  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
    6.81 -
    6.82 -val {use, use_debug, use_no_debug} =
    6.83 -  use_operations (fn opt_debug => fn file =>
    6.84 -    use_file boot_context {verbose = true, debug = use_debug_option opt_debug} file
    6.85 -      handle ERROR msg => (#print boot_context msg; raise error "ML error"));
    6.86 -
    6.87 -end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/RAW/ml_compiler0.ML	Tue Mar 01 22:11:36 2016 +0100
     7.3 @@ -0,0 +1,100 @@
     7.4 +(*  Title:      Pure/RAW/ml_compiler0.ML
     7.5 +
     7.6 +Runtime compilation and evaluation (bootstrap version of
     7.7 +Pure/ML/ml_compiler.ML).
     7.8 +*)
     7.9 +
    7.10 +signature ML_COMPILER0 =
    7.11 +sig
    7.12 +  type context =
    7.13 +   {name_space: ML_Name_Space.T,
    7.14 +    here: int -> string -> string,
    7.15 +    print: string -> unit,
    7.16 +    error: string -> unit}
    7.17 +  val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
    7.18 +  val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
    7.19 +  val debug_option: bool option -> bool
    7.20 +  val use_operations: (bool option -> string -> unit) ->
    7.21 +    {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
    7.22 +end;
    7.23 +
    7.24 +structure ML_Compiler0: ML_COMPILER0 =
    7.25 +struct
    7.26 +
    7.27 +type context =
    7.28 + {name_space: ML_Name_Space.T,
    7.29 +  here: int -> string -> string,
    7.30 +  print: string -> unit,
    7.31 +  error: string -> unit};
    7.32 +
    7.33 +fun drop_newline s =
    7.34 +  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    7.35 +  else s;
    7.36 +
    7.37 +fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
    7.38 +  let
    7.39 +    val _ = Secure.deny_ml ();
    7.40 +
    7.41 +    val current_line = Unsynchronized.ref line;
    7.42 +    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
    7.43 +    val out_buffer = Unsynchronized.ref ([]: string list);
    7.44 +    fun output () = drop_newline (implode (rev (! out_buffer)));
    7.45 +
    7.46 +    fun get () =
    7.47 +      (case ! in_buffer of
    7.48 +        [] => NONE
    7.49 +      | c :: cs =>
    7.50 +          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    7.51 +    fun put s = out_buffer := s :: ! out_buffer;
    7.52 +    fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
    7.53 +     (put (if hard then "Error: " else "Warning: ");
    7.54 +      PolyML.prettyPrint (put, 76) msg1;
    7.55 +      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
    7.56 +      put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n"));
    7.57 +
    7.58 +    val parameters =
    7.59 +     [PolyML.Compiler.CPOutStream put,
    7.60 +      PolyML.Compiler.CPNameSpace name_space,
    7.61 +      PolyML.Compiler.CPErrorMessageProc put_message,
    7.62 +      PolyML.Compiler.CPLineNo (fn () => ! current_line),
    7.63 +      PolyML.Compiler.CPFileName file,
    7.64 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
    7.65 +      ML_Compiler_Parameters.debug debug;
    7.66 +    val _ =
    7.67 +      (while not (List.null (! in_buffer)) do
    7.68 +        PolyML.compiler (get, parameters) ())
    7.69 +      handle exn =>
    7.70 +        if Exn.is_interrupt exn then reraise exn
    7.71 +        else
    7.72 +         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    7.73 +          error (output ()); reraise exn);
    7.74 +  in if verbose then print (output ()) else () end;
    7.75 +
    7.76 +fun use_file context {verbose, debug} file =
    7.77 +  let
    7.78 +    val instream = TextIO.openIn file;
    7.79 +    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    7.80 +  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    7.81 +
    7.82 +
    7.83 +fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
    7.84 +  | debug_option (SOME debug) = debug;
    7.85 +
    7.86 +fun use_operations (use_ : bool option -> string -> unit) =
    7.87 +  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
    7.88 +
    7.89 +end;
    7.90 +
    7.91 +val {use, use_debug, use_no_debug} =
    7.92 +  let
    7.93 +    val context: ML_Compiler0.context =
    7.94 +     {name_space = ML_Name_Space.global,
    7.95 +      here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
    7.96 +      print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
    7.97 +      error = fn s => error s};
    7.98 +  in
    7.99 +    ML_Compiler0.use_operations (fn opt_debug => fn file =>
   7.100 +      ML_Compiler0.use_file context
   7.101 +        {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
   7.102 +      handle ERROR msg => (#print context msg; raise error "ML error"))
   7.103 +  end;
     8.1 --- a/src/Pure/ROOT	Tue Mar 01 21:10:29 2016 +0100
     8.2 +++ b/src/Pure/ROOT	Tue Mar 01 22:11:36 2016 +0100
     8.3 @@ -5,11 +5,11 @@
     8.4    files
     8.5      "RAW/ROOT_polyml-5.6.ML"
     8.6      "RAW/ROOT_polyml.ML"
     8.7 -    "RAW/compiler_polyml.ML"
     8.8      "RAW/exn.ML"
     8.9      "RAW/exn_trace.ML"
    8.10      "RAW/exn_trace_raw.ML"
    8.11      "RAW/fixed_int_dummy.ML"
    8.12 +    "RAW/ml_compiler0.ML"
    8.13      "RAW/ml_compiler_parameters.ML"
    8.14      "RAW/ml_compiler_parameters_polyml-5.6.ML"
    8.15      "RAW/ml_debugger.ML"
    8.16 @@ -37,11 +37,11 @@
    8.17    files
    8.18      "RAW/ROOT_polyml-5.6.ML"
    8.19      "RAW/ROOT_polyml.ML"
    8.20 -    "RAW/compiler_polyml.ML"
    8.21      "RAW/exn.ML"
    8.22      "RAW/exn_trace.ML"
    8.23      "RAW/exn_trace_raw.ML"
    8.24      "RAW/fixed_int_dummy.ML"
    8.25 +    "RAW/ml_compiler0.ML"
    8.26      "RAW/ml_compiler_parameters.ML"
    8.27      "RAW/ml_compiler_parameters_polyml-5.6.ML"
    8.28      "RAW/ml_debugger.ML"
     9.1 --- a/src/Pure/ROOT.ML	Tue Mar 01 21:10:29 2016 +0100
     9.2 +++ b/src/Pure/ROOT.ML	Tue Mar 01 22:11:36 2016 +0100
     9.3 @@ -36,17 +36,18 @@
     9.4  
     9.5  val {use, use_debug, use_no_debug} =
     9.6    let
     9.7 -    val global_context: use_context =
     9.8 +    val context: ML_Compiler0.context =
     9.9       {name_space = ML_Name_Space.global,
    9.10        here = Position.here oo Position.line_file,
    9.11        print = writeln,
    9.12 -      error = error}
    9.13 +      error = error};
    9.14    in
    9.15 -    use_operations (fn opt_debug => fn file =>
    9.16 +    ML_Compiler0.use_operations (fn opt_debug => fn file =>
    9.17        Position.setmp_thread_data (Position.file_only file)
    9.18          (fn () =>
    9.19 -          use_file global_context {verbose = true, debug = use_debug_option opt_debug} file
    9.20 -            handle ERROR msg => (writeln msg; error "ML error")) ())
    9.21 +          ML_Compiler0.use_file context
    9.22 +            {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
    9.23 +          handle ERROR msg => (writeln msg; error "ML error")) ())
    9.24    end;
    9.25  
    9.26  
    9.27 @@ -228,7 +229,7 @@
    9.28  use "ML/ml_antiquotation.ML";
    9.29  
    9.30  val {use, use_debug, use_no_debug} =
    9.31 -  use_operations (fn opt_debug => fn file =>
    9.32 +  ML_Compiler0.use_operations (fn opt_debug => fn file =>
    9.33      let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
    9.34        ML_Context.eval_file flags (Path.explode file)
    9.35          handle ERROR msg => (writeln msg; error "ML error")
    10.1 --- a/src/Tools/Code/code_runtime.ML	Tue Mar 01 21:10:29 2016 +0100
    10.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Mar 01 22:11:36 2016 +0100
    10.3 @@ -82,7 +82,7 @@
    10.4  fun exec ctxt verbose code =
    10.5   (if Config.get ctxt trace then tracing code else ();
    10.6    ML_Context.exec (fn () =>
    10.7 -    use_text ML_Env.local_context
    10.8 +    ML_Compiler0.use_text ML_Env.local_context
    10.9        {line = 0, file = "generated code", verbose = verbose, debug = false} code));
   10.10  
   10.11  fun value ctxt (get, put, put_ml) (prelude, value) =
   10.12 @@ -509,7 +509,7 @@
   10.13  
   10.14  fun abort _ = error "Only value bindings allowed.";
   10.15  
   10.16 -val notifying_context : use_context =
   10.17 +val notifying_context : ML_Compiler0.context =
   10.18   {name_space =
   10.19     {lookupVal    = #lookupVal ML_Env.local_name_space,
   10.20      lookupType   = #lookupType ML_Env.local_name_space,
   10.21 @@ -540,7 +540,7 @@
   10.22      val thy' = Loaded_Values.put [] thy;
   10.23      val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
   10.24      val _ =
   10.25 -      use_text notifying_context
   10.26 +      ML_Compiler0.use_text notifying_context
   10.27          {line = 0, file = Path.implode filepath, verbose = false, debug = false}
   10.28          (File.read filepath);
   10.29      val thy'' = Context.the_theory (Context.the_thread_data ());
    11.1 --- a/src/Tools/Spec_Check/spec_check.ML	Tue Mar 01 21:10:29 2016 +0100
    11.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Tue Mar 01 22:11:36 2016 +0100
    11.3 @@ -127,7 +127,7 @@
    11.4  fun determine_type ctxt s =
    11.5    let
    11.6      val return = Unsynchronized.ref "return"
    11.7 -    val use_context : use_context =
    11.8 +    val context : ML_Compiler0.context =
    11.9       {name_space = #name_space ML_Env.local_context,
   11.10        here = #here ML_Env.local_context,
   11.11        print = fn r => return := r,
   11.12 @@ -135,7 +135,7 @@
   11.13      val _ =
   11.14        Context.setmp_thread_data (SOME (Context.Proof ctxt))
   11.15          (fn () =>
   11.16 -          use_text use_context
   11.17 +          ML_Compiler0.use_text context
   11.18              {line = 0, file = "generated code", verbose = true, debug = false} s) ()
   11.19    in
   11.20      Gen_Construction.parse_pred (! return)
   11.21 @@ -145,7 +145,7 @@
   11.22  fun run_test ctxt s =
   11.23    Context.setmp_thread_data (SOME (Context.Proof ctxt))
   11.24      (fn () =>
   11.25 -      use_text ML_Env.local_context
   11.26 +      ML_Compiler0.use_text ML_Env.local_context
   11.27          {line = 0, file = "generated code", verbose = false, debug = false} s) ();
   11.28  
   11.29  (*split input into tokens*)