clarified signature: more explicit type Path.binding;
authorwenzelm
Sat, 30 Mar 2019 20:54:47 +0100
changeset 70197 c8e08d8ffb93
parent 70196 7a9c559bc518
child 70198 a8142ac5e4b6
clarified signature: more explicit type Path.binding; tuned;
etc/symbols
lib/texinputs/isabellesym.sty
src/HOL/SPARK/Tools/spark_vcs.ML
src/Pure/General/path.ML
src/Pure/ML/ml_syntax.ML
src/Pure/PIDE/resources.ML
src/Pure/Thy/export.ML
src/Pure/Thy/export_theory.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/generated_files.ML
src/Tools/Code/code_target.ML
--- a/etc/symbols	Sat Mar 30 12:07:31 2019 +0100
+++ b/etc/symbols	Sat Mar 30 20:54:47 2019 +0100
@@ -408,6 +408,7 @@
 \<^named_theorems>      argument: cartouche
 \<^nonterminal>         argument: cartouche
 \<^path>                argument: cartouche
+\<^path_binding>        argument: cartouche
 \<^plugin>              argument: cartouche
 \<^print>
 \<^prop>                argument: cartouche
--- a/lib/texinputs/isabellesym.sty	Sat Mar 30 12:07:31 2019 +0100
+++ b/lib/texinputs/isabellesym.sty	Sat Mar 30 20:54:47 2019 +0100
@@ -394,6 +394,7 @@
 \newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}}
 \newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}}
 \newcommand{\isactrlpath}{\isakeywordcontrol{path}}
+\newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}}
 \newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}
 \newcommand{\isactrlprint}{\isakeywordcontrol{print}}
 \newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Mar 30 12:07:31 2019 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Mar 30 20:54:47 2019 +0100
@@ -973,7 +973,7 @@
              \because their proofs contain oracles:" proved'));
           val prv_path = Path.ext "prv" path;
           val _ =
-            Export.export thy prv_path
+            Export.export thy (Path.binding (prv_path, Position.none))
               [implode (map (fn (s, _) => snd (strip_number s) ^
                 " -- proved by " ^ Distribution.version ^ "\n") proved'')];
         in {pfuns = pfuns, type_map = type_map, env = NONE} end))
--- a/src/Pure/General/path.ML	Sat Mar 30 12:07:31 2019 +0100
+++ b/src/Pure/General/path.ML	Sat Mar 30 20:54:47 2019 +0100
@@ -19,12 +19,12 @@
   val has_parent: T -> bool
   val is_absolute: T -> bool
   val is_basic: T -> bool
-  val all_basic: T -> bool
   val starts_basic: T -> bool
   val append: T -> T -> T
   val appends: T list -> T
   val implode: T -> string
   val explode: string -> T
+  val explode_pos: string * Position.T -> T * Position.T
   val decode: T XML.Decode.T
   val split: string -> T list
   val pretty: T -> Pretty.T
@@ -38,6 +38,14 @@
   val file_name: T -> string
   val smart_implode: T -> string
   val position: T -> Position.T
+  eqtype binding
+  val binding: T * Position.T -> binding
+  val binding0: T -> binding
+  val binding_map: (T -> T) -> binding -> binding
+  val dest_binding: binding -> T * Position.T
+  val implode_binding: binding -> string
+  val explode_binding: string * Position.T -> binding
+  val explode_binding0: string -> binding
 end;
 
 structure Path: PATH =
@@ -169,6 +177,9 @@
 
   in Path (norm (rev elems @ roots)) end;
 
+fun explode_pos (s, pos) =
+  (explode_path s handle ERROR msg => error (msg ^ Position.here pos), pos);
+
 fun split str =
   space_explode ":" str
   |> map_filter (fn s => if s = "" then NONE else SOME (explode_path s));
@@ -243,6 +254,26 @@
 
 val position = Position.file o smart_implode;
 
+
+(* binding: strictly monotonic path with position *)
+
+datatype binding = Binding of T * Position.T;
+
+fun binding (path, pos) =
+  if not (is_current path) andalso all_basic path then Binding (path, pos)
+  else error ("Bad path binding: " ^ print path ^ Position.here pos);
+
+fun binding0 path = binding (path, Position.none);
+fun binding_map f (Binding (path, pos)) = binding (f path, pos);
+
+fun dest_binding (Binding args) = args;
+
+val implode_binding = dest_binding #> #1 #> implode_path;
+
+val explode_binding = binding o explode_pos;
+fun explode_binding0 s = explode_binding (s, Position.none);
+
+
 (*final declarations of this structure!*)
 val implode = implode_path;
 val explode = explode_path;
--- a/src/Pure/ML/ml_syntax.ML	Sat Mar 30 12:07:31 2019 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Sat Mar 30 20:54:47 2019 +0100
@@ -23,6 +23,7 @@
   val print_properties: Properties.T -> string
   val print_position: Position.T -> string
   val print_range: Position.range -> string
+  val print_path_binding: Path.binding -> string
   val make_binding: string * Position.T -> string
   val print_indexname: indexname -> string
   val print_class: class -> string
@@ -98,6 +99,9 @@
 fun print_range range =
   "Position.range_of_properties " ^ print_properties (Position.properties_of_range range);
 
+fun print_path_binding binding =
+  "Path.binding " ^ print_pair print_path print_position (Path.dest_binding binding);
+
 fun make_binding (name, pos) =
   "Binding.make " ^ print_pair print_string print_position (name, pos);
 
--- a/src/Pure/PIDE/resources.ML	Sat Mar 30 12:07:31 2019 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Mar 30 20:54:47 2019 +0100
@@ -290,6 +290,9 @@
   ML_Antiquotation.value_embedded \<^binding>\<open>path\<close> (ML_antiq check_path) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>file\<close> (ML_antiq check_file) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
+  ML_Antiquotation.value_embedded \<^binding>\<open>path_binding\<close>
+    (Scan.lift (Parse.position Parse.path) >>
+      (ML_Syntax.print_path_binding o Path.explode_binding)) #>
   ML_Antiquotation.value \<^binding>\<open>master_dir\<close>
     (Args.theory >> (ML_Syntax.print_path o master_directory)));
 
--- a/src/Pure/Thy/export.ML	Sat Mar 30 12:07:31 2019 +0100
+++ b/src/Pure/Thy/export.ML	Sat Mar 30 20:54:47 2019 +0100
@@ -6,13 +6,12 @@
 
 signature EXPORT =
 sig
-  val check_name: Path.T -> string
-  type params = {theory: theory, path: Path.T, executable: bool, compress: bool}
+  type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool}
   val export_params: params -> string list -> unit
-  val export: theory -> Path.T -> string list -> unit
-  val export_executable: theory -> Path.T -> string list -> unit
-  val export_file: theory -> Path.T -> Path.T -> unit
-  val export_executable_file: theory -> Path.T -> Path.T -> unit
+  val export: theory -> Path.binding -> string list -> unit
+  val export_executable: theory -> Path.binding -> string list -> unit
+  val export_file: theory -> Path.binding -> Path.T -> unit
+  val export_executable_file: theory -> Path.binding -> Path.T -> unit
   val markup: theory -> Path.T -> Markup.T
   val message: theory -> Path.T -> string
 end;
@@ -22,33 +21,25 @@
 
 (* export *)
 
-fun check_name path =
-  let
-    val name = Path.implode path;
-    val _ =
-      if not (Path.is_current path) andalso Path.all_basic path then ()
-      else error ("Bad export name: " ^ quote name);
-  in name end;
+type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool};
 
-type params = {theory: theory, path: Path.T, executable: bool, compress: bool};
-
-fun export_params ({theory, path, executable, compress}: params) blob =
+fun export_params ({theory, binding, executable, compress}: params) blob =
   (Output.try_protocol_message o Markup.export)
    {id = Position.get_id (Position.thread_data ()),
     serial = serial (),
     theory_name = Context.theory_long_name theory,
-    name = check_name path,
+    name = Path.implode_binding binding,
     executable = executable,
     compress = compress} blob;
 
-fun export thy path blob =
-  export_params {theory = thy, path = path, executable = false, compress = true} blob;
+fun export thy binding blob =
+  export_params {theory = thy, binding = binding, executable = false, compress = true} blob;
 
-fun export_executable thy path blob =
-  export_params {theory = thy, path = path, executable = true, compress = true} blob;
+fun export_executable thy binding blob =
+  export_params {theory = thy, binding = binding, executable = true, compress = true} blob;
 
-fun export_file thy path file = export thy path [File.read file];
-fun export_executable_file thy path file = export_executable thy path [File.read file];
+fun export_file thy binding file = export thy binding [File.read file];
+fun export_executable_file thy binding file = export_executable thy binding [File.read file];
 
 
 (* information message *)
--- a/src/Pure/Thy/export_theory.ML	Sat Mar 30 12:07:31 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Sat Mar 30 20:54:47 2019 +0100
@@ -172,7 +172,7 @@
     if Options.bool (#options context) "export_theory" then f context thy else ()));
 
 fun export_body thy name body =
-  Export.export thy (Path.make ["theory", name])
+  Export.export thy (Path.binding0 (Path.make ["theory", name]))
     (Buffer.chunks (YXML.buffer_body body Buffer.empty));
 
 
--- a/src/Pure/Thy/thy_info.ML	Sat Mar 30 12:07:31 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Mar 30 20:54:47 2019 +0100
@@ -66,7 +66,7 @@
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
             val _ =
               if Options.bool options "export_document"
-              then Export.export thy (Path.explode "document.tex") output else ();
+              then Export.export thy (Path.explode_binding0 "document.tex") output else ();
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () end
       end));
--- a/src/Pure/Tools/generated_files.ML	Sat Mar 30 12:07:31 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML	Sat Mar 30 20:54:47 2019 +0100
@@ -6,7 +6,7 @@
 
 signature GENERATED_FILES =
 sig
-  val add_files: (Path.T * Position.T) * string -> theory -> theory
+  val add_files: Path.binding * string -> theory -> theory
   val get_files: theory -> {path: Path.T, pos: Position.T, content: string} list
   val write_files: theory -> Path.T -> (Path.T * Position.T) list
   val export_files: theory -> theory list -> (Path.T * Position.T) list
@@ -53,18 +53,12 @@
 
 (* files *)
 
-fun add_files ((path0, pos), content) =
-  let
-    val path = Path.expand path0;
-    fun err msg ps = error (msg ^ ": " ^ Path.print path ^ Position.here_list ps);
-    val _ =
-      if Path.is_absolute path then err "Illegal absolute path" [pos]
-      else if Path.has_parent path then err "Illegal parent path" [pos]
-      else ();
-  in
+fun add_files (binding, content) =
+  let val (path, pos) = Path.dest_binding binding in
     (Data.map o @{apply 3(1)}) (fn files =>
       (case AList.lookup (op =) files path of
-        SOME (pos', _) => err "Duplicate generated file" [pos, pos']
+        SOME (pos', _) =>
+          error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos'])
       | NONE => (path, (pos, content)) :: files))
   end;
 
@@ -83,7 +77,7 @@
 fun export_files thy other_thys =
   other_thys |> maps (fn other_thy =>
     get_files other_thy |> map (fn {path, pos, content} =>
-      (Export.export thy path [content]; (path, pos))));
+      (Export.export thy (Path.binding (path, pos)) [content]; (path, pos))));
 
 fun the_file_content thy path =
   (case find_first (fn file => #path file = path) (get_files thy) of
@@ -175,13 +169,14 @@
     val thy = Proof_Context.theory_of lthy;
 
     val path = Path.explode file;
+    val binding = Path.binding (path, pos);
     val file_type =
       the_file_type thy (#2 (Path.split_ext path))
         handle ERROR msg => error (msg ^ Position.here pos);
 
     val header = #make_comment file_type " generated by Isabelle ";
     val content = header ^ "\n" ^ read_source lthy file_type source;
-  in lthy |> (Local_Theory.background_theory o add_files) ((path, pos), content) end;
+  in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end;
 
  
 
--- a/src/Tools/Code/code_target.ML	Sat Mar 30 12:07:31 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Sat Mar 30 20:54:47 2019 +0100
@@ -11,8 +11,9 @@
 
   datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
 
-  val export_code_for: ({physical: bool} * Path.T) option -> string -> string -> int option -> Token.T list
-    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory
+  val export_code_for: ({physical: bool} * (Path.T * Position.T)) option -> string -> string
+    -> int option -> Token.T list  -> Code_Thingol.program -> bool -> Code_Symbol.T list
+    -> local_theory -> local_theory
   val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list
   val present_code_for: Proof.context -> string -> string -> int option -> Token.T list
@@ -21,7 +22,7 @@
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory
 
   val export_code: bool -> string list
-    -> (((string * string) * ({physical: bool} * Path.T) option) * Token.T list) list
+    -> (((string * string) * ({physical: bool} * (Path.T * Position.T)) option) * Token.T list) list
     -> local_theory -> local_theory
   val export_code_cmd: bool -> string list
     -> (((string * string) * ({physical: bool} * (string * Position.T)) option) * Token.T list) list
@@ -273,13 +274,14 @@
 
 local
 
-fun export_logical file_prefix format pretty_modules =
+fun export_logical (file_prefix, file_pos) format pretty_modules =
   let
     val prefix = Path.append (Path.basic codeN) file_prefix;
     fun export path content thy =
       let
-        val thy' = thy |> Generated_Files.add_files ((path, Position.none), content);
-        val _ = Export.export thy' path [content];
+        val binding = Path.binding (path, file_pos);
+        val thy' = thy |> Generated_Files.add_files (binding, content);
+        val _ = Export.export thy' binding [content];
       in thy' end;
   in
     (case pretty_modules of
@@ -303,10 +305,10 @@
   (case some_file of
     NONE =>
       let val (file_prefix, thy') = next_export thy;
-      in export_logical (Path.basic file_prefix) format pretty_code thy' end
+      in export_logical (Path.basic file_prefix, Position.none) format pretty_code thy' end
   | SOME ({physical = false}, file_prefix) =>
       export_logical file_prefix format pretty_code thy
-  | SOME ({physical = true}, file) =>
+  | SOME ({physical = true}, (file, _)) =>
       let
         val root = File.full_path (Resources.master_directory thy) file;
         val _ = File.check_dir (Path.dir root);
@@ -448,7 +450,7 @@
         val destination = make_destination p;
         val lthy' = lthy
           |> Local_Theory.background_theory
-            (export_result (SOME ({physical = true}, destination)) format
+            (export_result (SOME ({physical = true}, (destination, Position.none))) format
               (invoke_serializer lthy target_name generatedN args program all_public syms));
         val cmd = make_command generatedN;
         val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1";
@@ -503,11 +505,8 @@
 (* code generation *)
 
 fun prep_destination (location, (s, pos)) =
-  if location = {physical = false} then
-    let
-      val path = (Path.explode s |> tap Export.check_name)
-        handle ERROR msg => error (msg ^ Position.here pos)
-    in (location, path) end
+  if location = {physical = false}
+  then (location, Path.explode_pos (s, pos))
   else
     let
       val _ =
@@ -519,9 +518,9 @@
           (Markup.markup Markup.keyword1 "export_code" ^ " with " ^
             Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos);
       val _ = Position.report pos Markup.language_path;
-      val path = Path.explode s;
+      val path = #1 (Path.explode_pos (s, pos));
       val _ = Position.report pos (Markup.path (Path.smart_implode path));
-    in (location, path) end;
+    in (location, (path, pos)) end;
 
 fun export_code all_public cs seris lthy =
   let