support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
authorwenzelm
Tue Apr 05 18:20:25 2016 +0200 (2016-04-05)
changeset 628732f9c8a18f832
parent 62872 bf1b4d3440a3
child 62874 b0194643e64c
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
src/Pure/Isar/isar_syn.ML
src/Pure/ML/ML_Root.thy
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_file.ML
src/Pure/Pure.thy
src/Pure/Tools/debugger.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Apr 05 18:18:36 2016 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 05 18:20:25 2016 +0200
     1.3 @@ -197,8 +197,8 @@
     1.4      val provide = Resources.provide (src_path, digest);
     1.5      val source = Input.source true (cat_lines lines) (pos, pos);
     1.6      val flags: ML_Compiler.flags =
     1.7 -      {SML = false, exchange = false, redirect = true, verbose = true,
     1.8 -        debug = debug, writeln = writeln, warning = warning};
     1.9 +      {SML_syntax = false, SML_env = false, exchange = false, redirect = true,
    1.10 +        verbose = true, debug = debug, writeln = writeln, warning = warning};
    1.11    in
    1.12      gthy
    1.13      |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    1.14 @@ -211,8 +211,8 @@
    1.15      val ([{lines, pos, ...}: Token.file], thy') = files thy;
    1.16      val source = Input.source true (cat_lines lines) (pos, pos);
    1.17      val flags: ML_Compiler.flags =
    1.18 -      {SML = true, exchange = false, redirect = true, verbose = true,
    1.19 -        debug = debug, writeln = writeln, warning = warning};
    1.20 +      {SML_syntax = true, SML_env = true, exchange = false, redirect = true,
    1.21 +        verbose = true, debug = debug, writeln = writeln, warning = warning};
    1.22    in
    1.23      thy' |> Context.theory_map
    1.24        (ML_Context.exec (fn () => ML_Context.eval_source flags source))
    1.25 @@ -255,8 +255,8 @@
    1.26      (Parse.ML_source >> (fn source =>
    1.27        let
    1.28          val flags: ML_Compiler.flags =
    1.29 -          {SML = true, exchange = true, redirect = false, verbose = true,
    1.30 -            debug = NONE, writeln = writeln, warning = warning};
    1.31 +          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
    1.32 +            verbose = true, debug = NONE, writeln = writeln, warning = warning};
    1.33        in
    1.34          Toplevel.theory
    1.35            (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
    1.36 @@ -267,8 +267,8 @@
    1.37      (Parse.ML_source >> (fn source =>
    1.38        let
    1.39          val flags: ML_Compiler.flags =
    1.40 -          {SML = false, exchange = true, redirect = false, verbose = true,
    1.41 -            debug = NONE, writeln = writeln, warning = warning};
    1.42 +          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
    1.43 +            verbose = true, debug = NONE, writeln = writeln, warning = warning};
    1.44        in
    1.45          Toplevel.generic_theory
    1.46            (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
     2.1 --- a/src/Pure/ML/ML_Root.thy	Tue Apr 05 18:18:36 2016 +0200
     2.2 +++ b/src/Pure/ML/ML_Root.thy	Tue Apr 05 18:20:25 2016 +0200
     2.3 @@ -10,6 +10,8 @@
     2.4    and "use_thy" :: thy_load
     2.5  begin
     2.6  
     2.7 +setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
     2.8 +
     2.9  ML \<open>
    2.10  local
    2.11  
     3.1 --- a/src/Pure/ML/ml_compiler.ML	Tue Apr 05 18:18:36 2016 +0200
     3.2 +++ b/src/Pure/ML/ml_compiler.ML	Tue Apr 05 18:20:25 2016 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  signature ML_COMPILER =
     3.5  sig
     3.6    type flags =
     3.7 -    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
     3.8 +    {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
     3.9        debug: bool option, writeln: string -> unit, warning: string -> unit}
    3.10    val debug_flags: bool option -> flags
    3.11    val flags: flags
    3.12 @@ -21,18 +21,19 @@
    3.13  (* flags *)
    3.14  
    3.15  type flags =
    3.16 -  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    3.17 +  {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
    3.18      debug: bool option, writeln: string -> unit, warning: string -> unit};
    3.19  
    3.20  fun debug_flags opt_debug : flags =
    3.21 -  {SML = false, exchange = false, redirect = false, verbose = false,
    3.22 +  {SML_syntax = false, SML_env = false, exchange = false, redirect = false, verbose = false,
    3.23      debug = opt_debug, writeln = writeln, warning = warning};
    3.24  
    3.25  val flags = debug_flags NONE;
    3.26  
    3.27  fun verbose b (flags: flags) =
    3.28 -  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
    3.29 -    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
    3.30 +  {SML_syntax = #SML_syntax flags, SML_env = #SML_env flags, exchange = #exchange flags,
    3.31 +    redirect = #redirect flags, verbose = b, debug = #debug flags,
    3.32 +    writeln = #writeln flags, warning = #warning flags};
    3.33  
    3.34  
    3.35  (* parse trees *)
    3.36 @@ -144,7 +145,7 @@
    3.37  
    3.38  fun eval (flags: flags) pos toks =
    3.39    let
    3.40 -    val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
    3.41 +    val space = ML_Env.make_name_space {SML = #SML_env flags, exchange = #exchange flags};
    3.42      val opt_context = Context.thread_data ();
    3.43  
    3.44  
    3.45 @@ -153,7 +154,7 @@
    3.46      val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
    3.47  
    3.48      val input_explode =
    3.49 -      if #SML flags then String.explode
    3.50 +      if #SML_syntax flags then String.explode
    3.51        else maps (String.explode o Symbol.esc) o Symbol.explode;
    3.52  
    3.53      val input_buffer =
     4.1 --- a/src/Pure/ML/ml_context.ML	Tue Apr 05 18:18:36 2016 +0200
     4.2 +++ b/src/Pure/ML/ml_context.ML	Tue Apr 05 18:20:25 2016 +0200
     4.3 @@ -218,7 +218,7 @@
     4.4    in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
     4.5  
     4.6  fun eval_source flags source =
     4.7 -  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
     4.8 +  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML_syntax flags) source);
     4.9  
    4.10  fun eval_in ctxt flags pos ants =
    4.11    Context.setmp_thread_data (Option.map Context.Proof ctxt)
     5.1 --- a/src/Pure/ML/ml_env.ML	Tue Apr 05 18:18:36 2016 +0200
     5.2 +++ b/src/Pure/ML/ml_env.ML	Tue Apr 05 18:20:25 2016 +0200
     5.3 @@ -12,6 +12,7 @@
     5.4    val add_breakpoint: serial * (bool Unsynchronized.ref * Position.T) ->
     5.5      Context.generic -> Context.generic
     5.6    val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
     5.7 +  val init_bootstrap: Context.generic -> Context.generic
     5.8    val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
     5.9    val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
    5.10    val context: ML_Compiler0.context
    5.11 @@ -92,6 +93,23 @@
    5.12  
    5.13  (* name space *)
    5.14  
    5.15 +val init_bootstrap =
    5.16 +  Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    5.17 +    let
    5.18 +      val sml_tables' =
    5.19 +        sml_tables |> (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
    5.20 +            let
    5.21 +              val val2 =
    5.22 +                fold (fn (x, y) =>
    5.23 +                  member (op =) ML_Name_Space.excluded_values x ? Symtab.update (x, y))
    5.24 +                (#allVal ML_Name_Space.global ()) val1;
    5.25 +              val structure2 =
    5.26 +                fold (fn (x, y) =>
    5.27 +                  member (op =) ML_Name_Space.excluded_structures x ? Symtab.update (x, y))
    5.28 +                (#allStruct ML_Name_Space.global ()) structure1;
    5.29 +            in (val2, type1, fixity1, structure2, signature1, functor1) end);
    5.30 +    in make_data (bootstrap, tables, sml_tables', breakpoints) end);
    5.31 +
    5.32  fun add_name_space {SML} (space: ML_Name_Space.T) =
    5.33    Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    5.34      let
     6.1 --- a/src/Pure/ML/ml_file.ML	Tue Apr 05 18:18:36 2016 +0200
     6.2 +++ b/src/Pure/ML/ml_file.ML	Tue Apr 05 18:20:25 2016 +0200
     6.3 @@ -19,9 +19,10 @@
     6.4      val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
     6.5      val provide = Resources.provide (src_path, digest);
     6.6      val source = Input.source true (cat_lines lines) (pos, pos);
     6.7 +    val (SML_syntax, SML_env) = SML src_path;
     6.8      val flags =
     6.9 -      {SML = SML src_path, exchange = false, redirect = true, verbose = true,
    6.10 -        debug = debug, writeln = writeln, warning = warning};
    6.11 +      {SML_syntax = SML_syntax, SML_env = SML_env, exchange = false, redirect = true,
    6.12 +        verbose = true, debug = debug, writeln = writeln, warning = warning};
    6.13    in
    6.14      gthy
    6.15      |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    6.16 @@ -29,15 +30,15 @@
    6.17      |> Context.mapping provide (Local_Theory.background_theory provide)
    6.18    end);
    6.19  
    6.20 -val ML = command (K false);
    6.21 -val SML = command (K true);
    6.22 +val ML = command (K (false, false));
    6.23 +val SML = command (K (true, true));
    6.24  
    6.25  val use =
    6.26    command (fn path =>
    6.27      (case try (#2 o Path.split_ext) path of
    6.28 -      SOME "ML" => false
    6.29 -    | SOME "sml" => true
    6.30 -    | SOME "sig" => true
    6.31 +      SOME "ML" => (false, true)
    6.32 +    | SOME "sml" => (true, true)
    6.33 +    | SOME "sig" => (true, true)
    6.34      | _ =>
    6.35          error ("Bad file name " ^ Path.print path ^
    6.36            "\nExpected .ML for Isabelle/ML or .sml/.sig for Standard ML")));
     7.1 --- a/src/Pure/Pure.thy	Tue Apr 05 18:18:36 2016 +0200
     7.2 +++ b/src/Pure/Pure.thy	Tue Apr 05 18:20:25 2016 +0200
     7.3 @@ -133,8 +133,8 @@
     7.4      (Parse.ML_source >> (fn source =>
     7.5        let
     7.6          val flags: ML_Compiler.flags =
     7.7 -          {SML = true, exchange = true, redirect = false, verbose = true,
     7.8 -            debug = NONE, writeln = writeln, warning = warning};
     7.9 +          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
    7.10 +            verbose = true, debug = NONE, writeln = writeln, warning = warning};
    7.11        in
    7.12          Toplevel.theory
    7.13            (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
    7.14 @@ -145,8 +145,8 @@
    7.15      (Parse.ML_source >> (fn source =>
    7.16        let
    7.17          val flags: ML_Compiler.flags =
    7.18 -          {SML = false, exchange = true, redirect = false, verbose = true,
    7.19 -            debug = NONE, writeln = writeln, warning = warning};
    7.20 +          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
    7.21 +            verbose = true, debug = NONE, writeln = writeln, warning = warning};
    7.22        in
    7.23          Toplevel.generic_theory
    7.24            (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
     8.1 --- a/src/Pure/Tools/debugger.ML	Tue Apr 05 18:18:36 2016 +0200
     8.2 +++ b/src/Pure/Tools/debugger.ML	Tue Apr 05 18:20:25 2016 +0200
     8.3 @@ -143,7 +143,7 @@
     8.4  
     8.5  fun evaluate {SML, verbose} =
     8.6    ML_Context.eval
     8.7 -    {SML = SML, exchange = false, redirect = false, verbose = verbose,
     8.8 +    {SML_syntax = SML, SML_env = SML, exchange = false, redirect = false, verbose = verbose,
     8.9        debug = SOME false, writeln = writeln_message, warning = warning_message}
    8.10      Position.none;
    8.11