src/Pure/Thy/read.ML
author clasohm
Fri Oct 22 13:42:51 1993 +0100 (1993-10-22)
changeset 74 208ab8773a73
parent 0 a5a9c433f639
child 78 e76a1edc2e49
permissions -rw-r--r--
changes in Readthy:
- reads needed base theories automatically
- keeps a time stamp for all read files
- update function
- checks for cycles
- path list that is searched for files
- reads theories that are created in .ML files
- etc.
     1 (*  Title:      Pure/Thy/read
     2     ID:         $Id$
     3     Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson
     4     Copyright   1992  TU Muenchen
     5 
     6 Reading and writing the theory definition files.
     7 
     8 For theory XXX, the  input file is called XXX.thy
     9                 the output file is called .XXX.thy.ML
    10                 and it then tries to read XXX.ML
    11 *)
    12 
    13 signature READTHY =
    14 sig
    15   type thy_info
    16 
    17   val use_thy        : string -> unit
    18   val update         : unit -> unit
    19   val time_use_thy   : string -> unit
    20   val base_on        : string list -> string -> Thm.theory
    21   val store_theory   : string -> Thm.theory -> unit
    22   val list_loaded    : unit -> thy_info list
    23   val set_loaded     : thy_info list -> unit
    24   val set_loadpath   : string list -> unit
    25   val relations      : string -> unit
    26 end;
    27 
    28 
    29 functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY =
    30 struct
    31 
    32 datatype thy_info = ThyInfo of {name: string, childs: string list, 
    33                                 thy_info: string, ml_info: string, 
    34                                 theory: Thm.theory};
    35 
    36 val loaded_thys = ref [ThyInfo {name = "pure", childs = [], thy_info = "",
    37                        ml_info = "", theory = Thm.pure_thy}];
    38 
    39 val loadpath = ref ["."];
    40 
    41 
    42 (*Make name of the output ML file for a theory *)
    43 fun out_name thy = "." ^ thy ^ ".thy.ML";
    44 
    45 (*Read a file specified by thy_file containing theory thy *)
    46 fun read_thy thy thy_file =
    47     let val instream  = open_in thy_file;
    48         val outstream = open_out (out_name thy)
    49     in  output (outstream, ThySyn.read (explode(input(instream, 999999))));
    50         close_out outstream;
    51         close_in instream
    52     end;
    53 
    54 fun file_exists file =
    55   let val instream = open_in file in close_in instream; true end
    56     handle Io _ => false;
    57 
    58 exception FILE_NOT_FOUND; (*raised by find_file *)
    59 
    60 (*Find a file using a list of paths if no absolute or relative path is
    61   specified.*)
    62 fun find_file "" name =
    63       let fun find_it (curr :: paths) =
    64                 if file_exists (tack_on curr name) then
    65                     tack_on curr name
    66                 else 
    67                     find_it paths
    68            | find_it [] = raise FILE_NOT_FOUND
    69       in find_it (!loadpath) end
    70   | find_file path name =
    71       if file_exists (tack_on path name) then tack_on path name
    72                                          else raise FILE_NOT_FOUND;
    73 
    74 (*Use the file if it exists *)
    75 fun try_use file = 
    76       if file_exists file then use file else ();
    77 
    78 (*Check if a theory was already loaded *)
    79 fun already_loaded thy =
    80   let fun do_search ((ThyInfo {name, ...}) :: loaded) =
    81               if name = thy then true else do_search loaded
    82         | do_search [] = false
    83   in do_search (!loaded_thys) end;
    84 
    85 (*Get thy_info for a loaded theory *)
    86 fun get_thyinfo thy =
    87   let fun do_search (t :: loaded : thy_info list) =
    88             let val ThyInfo {name, ...} = t
    89             in if name = thy then t else do_search loaded end
    90         | do_search [] = error ("Internal error (get_thyinfo): theory " 
    91                                 ^ thy ^ " not found.")
    92   in do_search (!loaded_thys) end;
    93 
    94 (*Check if a theory file has changed since its last use.
    95   Return a pair of boolean values for .thy and for .ML. *)
    96 fun thy_unchanged thy thy_file ml_file = 
    97       if already_loaded thy then 
    98         let val ThyInfo {thy_info, ml_info, ...} = get_thyinfo thy;
    99         in ((file_info (thy_file) = thy_info), (file_info (ml_file) = ml_info))
   100         end
   101       else (false, false);
   102 
   103 (*Get theory object for a loaded theory *)
   104 fun get_theory name =
   105   let val ThyInfo {theory, ...} = get_thyinfo name
   106   in theory end;
   107 
   108 (*Read .thy and .ML files that haven't been read yet or have changed since 
   109   they were last read;
   110   loaded_thys is a thy_info list ref containing all theories that have 
   111   completly been read by this and preceeding use_thy calls.
   112   If a theory changed since its last use its childs are marked as changed *)
   113 fun use_thy name =
   114     let val (path, thy_name) = split_filename name;
   115         val thy = to_lower thy_name;
   116         val thy_file = (find_file path (thy ^ ".thy")
   117                         handle FILE_NOT_FOUND => "");
   118         val (thy_path, _) = split_filename thy_file;
   119         val ml_file = if thy_file = ""
   120                       then (find_file path (thy ^ ".ML")
   121                             handle FILE_NOT_FOUND => 
   122                              error ("Could find no .thy or .ML file for theory "
   123                                     ^ name))
   124                       else if file_exists (thy_path ^ thy ^ ".ML")
   125                       then thy_path ^ thy ^ ".ML"
   126                       else ""
   127         val (thy_uptodate, ml_uptodate) = thy_unchanged thy thy_file ml_file;
   128 
   129         (*Remove theory from all child lists in loaded_thys.
   130           Afterwards add_child should be called for the (new) base theories *)
   131         fun remove_child thy =
   132           let fun do_remove (ThyInfo {name, childs, thy_info, ml_info, theory}
   133                             :: loaded) result =
   134                     do_remove loaded 
   135                       (ThyInfo {name = name, childs = childs \ thy, 
   136                                 thy_info = thy_info, ml_info = ml_info,
   137                                 theory = theory} :: result)
   138                 | do_remove [] result = result;
   139           in loaded_thys := do_remove (!loaded_thys) [] end;
   140           
   141          exception THY_NOT_FOUND;  (*Raised by set_info *)
   142 
   143          (*Change thy_info and ml_info for an existent item or create
   144            a new item with empty child list *)
   145          fun set_info thy_new ml_new thy =
   146                let fun make_change (t :: loaded) =
   147                          let val ThyInfo {name, childs, theory, ...} = t
   148                          in if name = thy then            
   149                               ThyInfo {name = name, childs = childs,
   150                                        thy_info = thy_new, ml_info = ml_new,
   151                                        theory = theory} :: loaded
   152                             else
   153                               t :: (make_change loaded)
   154                          end
   155                      | make_change [] = raise THY_NOT_FOUND
   156                in loaded_thys := make_change (!loaded_thys) end;
   157 
   158          (*Mark all direct and indirect descendants of a theory as changed *)
   159          fun mark_childs thy =
   160            let val ThyInfo {childs, ...} = get_thyinfo thy
   161            in writeln ("Marking childs of modified theory " ^ thy ^ " (" ^
   162                        (space_implode "," childs) ^ ")");
   163               seq (set_info "" "") childs
   164               handle THY_NOT_FOUND => ()
   165                         (*If this theory was automatically loaded by a child 
   166                           then the child cannot be found in loaded_thys *)
   167            end
   168 
   169     in if thy_uptodate andalso ml_uptodate then ()
   170        else
   171        (
   172          writeln ("Loading theory " ^ name);
   173          if thy_uptodate orelse (thy_file = "") then ()
   174          else
   175          (
   176              (*Allow dependency lists to be rebuild completely *)
   177              remove_child thy;
   178                 
   179              read_thy thy thy_file
   180          );
   181          
   182          (*Actually read files!*)
   183          if thy_uptodate orelse (thy_file = "") then ()
   184                          else use (out_name thy);
   185          if (thy_file = "") then          (*theory object created in .ML file*)
   186              (
   187                  use ml_file;
   188                  let val outstream = open_out (".tmp.ML") 
   189                  in
   190                     output (outstream, "store_theory " ^ quote name ^ " " ^ name
   191                                        ^ ".thy;\n");
   192                     close_out outstream 
   193                  end;
   194                  use ".tmp.ML";
   195                  delete_file ".tmp.ML"
   196              )
   197          else try_use ml_file;
   198 
   199          (*Now set the correct info.*)
   200          (set_info (file_info thy_file) (file_info ml_file) thy
   201           handle THY_NOT_FOUND => error ("Could not find theory \"" ^ name
   202                                          ^ "\" (wrong filename?)"));
   203 
   204          (*Mark theories that have to be reloaded.*)
   205          mark_childs thy;
   206 
   207          delete_file (out_name thy)
   208        )
   209     end;
   210 
   211 fun time_use_thy tname = timeit(fn()=>
   212    (writeln("\n**** Starting Theory " ^ tname ^ " ****");  
   213     use_thy tname;
   214     writeln("\n**** Finished Theory " ^ tname ^ " ****"))
   215    );
   216 
   217 (*Load all thy or ML files that have been changed and also
   218   all theories that depend on them *)
   219 fun update () =
   220   let (*List theories in the order they have to be loaded *)
   221       fun load_order [] result = result
   222         | load_order thys result =
   223             let fun next_level (t :: ts) =
   224                       let val ThyInfo {childs, ...} = get_thyinfo t
   225                       in childs union (next_level ts)
   226                       end
   227                   | next_level [] = [];
   228                   
   229                 val childs = next_level thys
   230             in load_order childs ((result \\ childs) @ childs) end;
   231 
   232       fun reload_changed (t :: ts) =
   233             let val curr = get_thyinfo t;
   234                 val thy_file = (find_file "" (t ^ ".thy")
   235                                 handle FILE_NOT_FOUND => "");
   236                 val (thy_path, _) = split_filename thy_file;
   237                 val ml_file = if thy_file = ""
   238                               then (find_file "" (t ^ ".ML")
   239                                     handle FILE_NOT_FOUND => 
   240                              error ("Could find no .thy or .ML file for theory "
   241                                     ^ t))
   242                               else if file_exists (thy_path ^ t ^ ".ML")
   243                               then thy_path ^ t ^ ".ML"
   244                               else ""
   245                 val (thy_uptodate, ml_uptodate) =
   246                       thy_unchanged t thy_file ml_file;
   247  
   248             in if thy_uptodate andalso ml_uptodate then ()
   249                                                    else use_thy t;
   250                reload_changed ts
   251             end
   252         | reload_changed [] = ()
   253   in reload_changed (load_order ["pure"] []) end;
   254 
   255 (*Merge theories to build a base for a new theory.
   256   Base members are only loaded if they are missing. *)
   257 fun base_on (t :: ts) child =
   258       let val childl = to_lower child;
   259 
   260           fun load_base base =
   261               let val basel = to_lower base;
   262 
   263                   (*List all descendants of a theory list *)
   264                   fun list_descendants (t :: ts) =
   265                         if already_loaded t then
   266                           let val ThyInfo {childs, ...} = get_thyinfo t
   267                           in childs union (list_descendants (ts union childs))
   268                           end
   269                         else []
   270                     | list_descendants [] = [];
   271  
   272                   (*Show the cycle that would be created by add_child *)
   273                   fun show_cycle () =
   274                     let fun find_it result curr =
   275                           if basel = curr then 
   276                               error ("Cyclic dependency of theories: "
   277                                      ^ childl ^ "->" ^ basel ^ result)
   278                           else if already_loaded curr then
   279                             let val ThyInfo {childs, ...} = get_thyinfo curr
   280                             in seq (find_it ("->" ^ curr ^ result)) childs
   281                             end
   282                           else ()
   283                     in find_it "" childl end;
   284 
   285                   (*Check if a cycle will be created by add_child *)
   286                   fun find_cycle () =
   287                     if basel mem (list_descendants [childl]) then show_cycle ()
   288                     else ();
   289                    
   290                   (*Add child to child list of base *)
   291                   fun add_child (t :: loaded) =
   292                         let val ThyInfo {name, childs, thy_info, ml_info, 
   293                                          theory} = t
   294                         in if name = basel then
   295                              ThyInfo {name = name, childs = childl ins childs,
   296                                       thy_info = thy_info, ml_info = ml_info,
   297                                       theory = theory} :: loaded
   298                            else
   299                              t :: (add_child loaded)
   300                         end
   301                    | add_child [] =
   302                        [ThyInfo {name = basel, childs = [childl], 
   303                                  thy_info = "", ml_info = "",
   304                                  theory = Thm.pure_thy}];
   305                                          (*Thm.pure_thy is used as a dummy *)
   306 
   307                   val thy_there = already_loaded basel
   308                                             (*test this before child is added *)
   309               in
   310                 if childl = basel then
   311                     error ("Cyclic dependency of theories: " ^ child
   312                            ^ "->" ^ child)
   313                 else find_cycle ();
   314                 loaded_thys := add_child (!loaded_thys);
   315                 if thy_there then ()
   316                 else (writeln ("Autoloading theory " ^ base
   317                                ^ " (used by " ^ child ^ ")");
   318                       use_thy base
   319                      )
   320               end;
   321               
   322           val (tl :: tls) = map to_lower (t :: ts)
   323      in seq load_base (t :: ts);
   324         foldl Thm.merge_theories (get_theory tl, map get_theory tls)
   325      end
   326   | base_on [] _ = raise Match;
   327 
   328 (*Change theory object for an existent item of loaded_thys 
   329   or create a new item *)
   330 fun store_theory thy_name thy =
   331   let fun make_change (t :: loaded) =
   332             let val ThyInfo {name, childs, thy_info, ml_info, ...} = t
   333             in if name = (to_lower thy_name) then            
   334                     ThyInfo {name = name, childs = childs,
   335                              thy_info = thy_info, ml_info = ml_info,
   336                              theory = thy} :: loaded
   337                else
   338                     t :: (make_change loaded)
   339             end
   340         | make_change [] =
   341             [ThyInfo {name = (to_lower thy_name), childs = [], thy_info = "", 
   342                       ml_info = "", theory = thy}]
   343   in loaded_thys := make_change (!loaded_thys) end;
   344 
   345 (*Create a list of all theories loaded by this structure *)
   346 fun list_loaded () = (!loaded_thys);
   347 
   348 (*Change the list of loaded theories *)
   349 fun set_loaded [] =
   350       loaded_thys := [ThyInfo {name = "pure", childs = [], thy_info = "",
   351                       ml_info = "", theory = Thm.pure_thy}]
   352   | set_loaded ts =
   353       loaded_thys := ts;
   354 
   355 (*Change the path list that is to be searched for .thy and .ML files *)
   356 fun set_loadpath new_path =
   357   loadpath := new_path;
   358 
   359 (*This function is for debugging purposes only *)
   360 fun relations thy =
   361   let val ThyInfo {childs, ...} = get_thyinfo thy
   362   in
   363      writeln (thy ^ ": " ^ (space_implode ", " childs));
   364      seq relations childs
   365   end
   366 
   367 end;
   368