more abstract Thy_Load.load_file/use_file for external theory resources;
authorwenzelm
Fri Jul 08 14:37:19 2011 +0200 (2011-07-08)
changeset 4370224fb44c1086a
parent 43701 f91c3c899911
child 43703 c37a1f29bbc0
more abstract Thy_Load.load_file/use_file for external theory resources;
prefer Boogie_Loader.parse_b2i on already loaded text, bypassing former File.fold_lines optimization;
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/Quickcheck_Narrowing.thy
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Jul 08 13:59:54 2011 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Jul 08 14:37:19 2011 +0200
     1.3 @@ -22,15 +22,14 @@
     1.4          "expected file ending " ^ quote ext)
     1.5  
     1.6      val base_path = Path.explode base_name |> tap check_ext
     1.7 -    val full_path = Thy_Load.check_file (Thy_Load.master_directory thy) base_path
     1.8 +    val (text, thy') = Thy_Load.use_file base_path thy
     1.9  
    1.10 -    val _ = Boogie_VCs.is_closed thy orelse
    1.11 +    val _ = Boogie_VCs.is_closed thy' orelse
    1.12        error ("Found the beginning of a new Boogie environment, " ^
    1.13          "but another Boogie environment is still open.")
    1.14    in
    1.15 -    thy
    1.16 -    |> Boogie_Loader.load_b2i (not quiet) offsets full_path
    1.17 -    |> Thy_Load.provide_file base_path
    1.18 +    thy'
    1.19 +    |> Boogie_Loader.parse_b2i (not quiet) offsets text
    1.20    end
    1.21  
    1.22  
     2.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Jul 08 13:59:54 2011 +0200
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Jul 08 14:37:19 2011 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  signature BOOGIE_LOADER =
     2.5  sig
     2.6    val load_b2i: bool -> (string * int) list -> Path.T -> theory -> theory
     2.7 +  val parse_b2i: bool -> (string * int) list -> string -> theory -> theory
     2.8  end
     2.9  
    2.10  structure Boogie_Loader: BOOGIE_LOADER =
    2.11 @@ -321,12 +322,12 @@
    2.12  
    2.13  datatype token = Token of string | Newline | EOF
    2.14  
    2.15 -fun tokenize path =
    2.16 +fun tokenize fold_lines input =
    2.17    let
    2.18      fun blank c = (c = #" " orelse c = #"\t" orelse c = #"\n" orelse c = #"\r")
    2.19      fun split line (i, tss) = (i + 1,
    2.20        map (pair i) (map Token (String.tokens blank line) @ [Newline]) :: tss)
    2.21 -  in apsnd (flat o rev) (File.fold_lines split path (1, [])) end
    2.22 +  in apsnd (flat o rev) (fold_lines split input (1, [])) end
    2.23  
    2.24  fun stopper i = Scan.stopper (K (i, EOF)) (fn (_, EOF) => true | _ => false)
    2.25  
    2.26 @@ -336,8 +337,8 @@
    2.27  
    2.28  fun scan_fail msg = Scan.fail_with (scan_err msg)
    2.29  
    2.30 -fun finite scan path =
    2.31 -  let val (i, ts) = tokenize path
    2.32 +fun finite scan fold_lines input =
    2.33 +  let val (i, ts) = tokenize fold_lines input
    2.34    in
    2.35      (case Scan.error (Scan.finite (stopper i) scan) ts of
    2.36        (x, []) => x
    2.37 @@ -591,6 +592,9 @@
    2.38    var_decls tds fds |--
    2.39    vcs verbose offsets tds fds)))
    2.40  
    2.41 -fun load_b2i verbose offsets path thy = finite (parse verbose offsets thy) path
    2.42 +fun load_b2i verbose offsets path thy = finite (parse verbose offsets thy) File.fold_lines path
    2.43 +
    2.44 +fun parse_b2i verbose offsets text thy =
    2.45 +  finite (parse verbose offsets thy) (fn f => fold f o String.tokens (fn c => c = #"\n")) text
    2.46  
    2.47  end
     3.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 08 13:59:54 2011 +0200
     3.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 08 14:37:19 2011 +0200
     3.3 @@ -5,9 +5,9 @@
     3.4  theory Quickcheck_Narrowing
     3.5  imports Quickcheck_Exhaustive
     3.6  uses
     3.7 -  ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
     3.8 -  ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
     3.9 -  ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
    3.10 +  ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
    3.11 +  ("Tools/Quickcheck/Narrowing_Engine.hs")
    3.12 +  ("Tools/Quickcheck/narrowing_generators.ML")
    3.13  begin
    3.14  
    3.15  subsection {* Counterexample generator *}
    3.16 @@ -352,9 +352,7 @@
    3.17  
    3.18  subsubsection {* Setting up the counterexample generator *}
    3.19  
    3.20 -setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")) *}
    3.21 -setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")) *}
    3.22 -use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
    3.23 +use "Tools/Quickcheck/narrowing_generators.ML"
    3.24  
    3.25  setup {* Narrowing_Generators.setup *}
    3.26  
     4.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Jul 08 13:59:54 2011 +0200
     4.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Jul 08 14:37:19 2011 +0200
     4.3 @@ -13,9 +13,10 @@
     4.4  structure SPARK_Commands: SPARK_COMMANDS =
     4.5  struct
     4.6  
     4.7 +(* FIXME proper Thy_Load.use_file, also for fdl_path and rls_path (!?) *)
     4.8  fun spark_open (vc_name, prfx) thy =
     4.9    let
    4.10 -    val vc_path = Thy_Load.check_file (Thy_Load.master_directory thy) (Path.explode vc_name);
    4.11 +    val ((vc_path, vc_id), vc_text) = Thy_Load.load_file thy (Path.explode vc_name);
    4.12      val (base, header) =
    4.13        (case Path.split_ext vc_path of
    4.14          (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
    4.15 @@ -27,7 +28,7 @@
    4.16      SPARK_VCs.set_vcs
    4.17        (snd (Fdl_Parser.parse_declarations (Path.position fdl_path) (File.read fdl_path)))
    4.18        (Fdl_Parser.parse_rules (Path.position rls_path) (File.read rls_path))
    4.19 -      (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path)))
    4.20 +      (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) vc_text))
    4.21        base prfx thy
    4.22    end;
    4.23  
     5.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 08 13:59:54 2011 +0200
     5.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 08 14:37:19 2011 +0200
     5.3 @@ -198,8 +198,13 @@
     5.4  
     5.5  (** invocation of Haskell interpreter **)
     5.6  
     5.7 -val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
     5.8 -val pnf_narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
     5.9 +val narrowing_engine =
    5.10 +  Context.>>> (Context.map_theory_result
    5.11 +    (Thy_Load.use_file (Path.explode "Tools/Quickcheck/Narrowing_Engine.hs")))
    5.12 +
    5.13 +val pnf_narrowing_engine =
    5.14 +  Context.>>> (Context.map_theory_result
    5.15 +    (Thy_Load.use_file (Path.explode "Tools/Quickcheck/PNF_Narrowing_Engine.hs")))
    5.16  
    5.17  fun exec verbose code =
    5.18    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
     6.1 --- a/src/Pure/Thy/thy_load.ML	Fri Jul 08 13:59:54 2011 +0200
     6.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Jul 08 14:37:19 2011 +0200
     6.3 @@ -12,9 +12,10 @@
     6.4    val check_file: Path.T -> Path.T -> Path.T
     6.5    val check_thy: Path.T -> string ->
     6.6      {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list}
     6.7 +  val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
     6.8 +  val use_file: Path.T -> theory -> string * theory
     6.9    val loaded_files: theory -> Path.T list
    6.10    val all_current: theory -> bool
    6.11 -  val provide_file: Path.T -> theory -> theory
    6.12    val use_ml: Path.T -> unit
    6.13    val exec_ml: Path.T -> generic_theory -> generic_theory
    6.14    val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory
    6.15 @@ -71,13 +72,6 @@
    6.16  
    6.17  fun check_file dir file = File.check_file (File.full_path dir file);
    6.18  
    6.19 -fun digest_file dir file =
    6.20 -  let
    6.21 -    val full_path = check_file dir file;
    6.22 -    val text = File.read full_path;
    6.23 -    val id = SHA1.digest text;
    6.24 -  in (text, (full_path, id)) end;
    6.25 -
    6.26  fun check_thy dir name =
    6.27    let
    6.28      val master_file = check_file dir (Thy_Header.thy_path name);
    6.29 @@ -89,7 +83,20 @@
    6.30    in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
    6.31  
    6.32  
    6.33 -(* loaded files *)
    6.34 +(* load files *)
    6.35 +
    6.36 +fun load_file thy src_path =
    6.37 +  let
    6.38 +    val full_path = check_file (master_directory thy) src_path;
    6.39 +    val text = File.read full_path;
    6.40 +    val id = SHA1.digest text;
    6.41 +  in ((full_path, id), text) end;
    6.42 +
    6.43 +fun use_file src_path thy =
    6.44 +  let
    6.45 +    val (path_id, text) = load_file thy src_path;
    6.46 +    val thy' = provide (src_path, path_id) thy;
    6.47 +  in (text, thy') end;
    6.48  
    6.49  val loaded_files = map (#1 o #2) o #provided o Files.get;
    6.50  
    6.51 @@ -109,11 +116,11 @@
    6.52  
    6.53  fun all_current thy =
    6.54    let
    6.55 -    val {master_dir, provided, ...} = Files.get thy;
    6.56 +    val {provided, ...} = Files.get thy;
    6.57      fun current (src_path, (_, id)) =
    6.58 -      (case try (digest_file master_dir) src_path of
    6.59 +      (case try (load_file thy) src_path of
    6.60          NONE => false
    6.61 -      | SOME (_, (_, id')) => id = id');
    6.62 +      | SOME ((_, id'), _) => id = id');
    6.63    in can check_loaded thy andalso forall current provided end;
    6.64  
    6.65  val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
    6.66 @@ -121,9 +128,6 @@
    6.67  
    6.68  (* provide files *)
    6.69  
    6.70 -fun provide_file src_path thy =
    6.71 -  provide (src_path, #2 (digest_file (master_directory thy) src_path)) thy;
    6.72 -
    6.73  fun eval_file path text = ML_Context.eval_text true (Path.position path) text;
    6.74  
    6.75  fun use_ml src_path =
    6.76 @@ -134,7 +138,7 @@
    6.77      let
    6.78        val thy = ML_Context.the_global_context ();
    6.79  
    6.80 -      val (text, (path, id)) = digest_file (master_directory thy) src_path;
    6.81 +      val ((path, id), text) = load_file thy src_path;
    6.82        val _ = eval_file path text;
    6.83        val _ = Context.>> Local_Theory.propagate_ml_env;
    6.84