src/Pure/Thy/read.ML
author wenzelm
Sun Jul 23 12:10:11 2000 +0200 (2000-07-23)
changeset 9416 9144976964e7
parent 397 48cb3fa4bc59
permissions -rw-r--r--
removed all_sessions.graph;
improved graph 'directories';
tuned;
     1 (*  Title:      Pure/Thy/read
     2     ID:         $Id$
     3     Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson
     4     Copyright   1993  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 datatype thy_info = ThyInfo of {name: string, path: string,
    14                                 children: string list,
    15                                 thy_info: string option, ml_info: string option,
    16                                 theory: Thm.theory option};
    17 
    18 signature READTHY =
    19 sig
    20   datatype basetype = Thy  of string
    21                     | File of string
    22 
    23   val loaded_thys    : thy_info list ref
    24   val loadpath       : string list ref
    25   val delete_tmpfiles: bool ref
    26 
    27   val use_thy        : string -> unit
    28   val update         : unit -> unit
    29   val time_use_thy   : string -> unit
    30   val unlink_thy     : string -> unit
    31   val base_on        : basetype list -> string -> Thm.theory
    32   val store_theory   : string -> Thm.theory -> unit
    33 end;
    34 
    35 
    36 functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY =
    37 struct
    38 
    39 datatype basetype = Thy  of string
    40                   | File of string;
    41 
    42 val loaded_thys = ref [ThyInfo {name = "Pure", path = "", children = [], 
    43                                 thy_info = Some "", ml_info = Some "", 
    44                                 theory = Some Thm.pure_thy}];
    45 
    46 val loadpath = ref ["."];           (*default search path for theory files *)
    47 
    48 val delete_tmpfiles = ref true;         (*remove temporary files after use *)
    49 
    50 (*Make name of the output ML file for a theory *)
    51 fun out_name thy = "." ^ thy ^ ".thy.ML";
    52 
    53 (*Read a file specified by thy_file containing theory thy *)
    54 fun read_thy thy thy_file =
    55     let val instream  = open_in thy_file;
    56         val outstream = open_out (out_name thy)
    57     in  output (outstream, ThySyn.read (explode(input(instream, 999999))));
    58         close_out outstream;
    59         close_in instream
    60     end;
    61 
    62 fun file_exists file =
    63   let val instream = open_in file in close_in instream; true end
    64     handle Io _ => false;
    65 
    66 (*Get thy_info for a loaded theory *)
    67 fun get_thyinfo thy =
    68   let fun do_search (t :: loaded : thy_info list) =
    69             let val ThyInfo {name, ...} = t
    70             in if name = thy then Some t else do_search loaded end
    71         | do_search [] = None
    72   in do_search (!loaded_thys) end;
    73 
    74 (*Replace an item by the result of make_change *)
    75 fun change_thyinfo make_change =
    76   let fun search (t :: loaded) =
    77             let val ThyInfo {name, path, children, thy_info, ml_info,
    78                              theory} = t
    79                 val (new_t, continue) = make_change name path children thy_info
    80                                                     ml_info theory
    81             in if continue then            
    82                  new_t :: (search loaded)
    83                else
    84                  new_t :: loaded
    85             end
    86         | search [] = []
    87   in loaded_thys := search (!loaded_thys) end;
    88 
    89 (*Check if a theory was already loaded *)
    90 fun already_loaded thy =
    91   let val t = get_thyinfo thy
    92   in if is_none t then false
    93      else let val ThyInfo {thy_info, ml_info, ...} = the t
    94           in if is_none thy_info orelse is_none ml_info then false 
    95              else true end
    96   end;
    97 
    98 (*Check if a theory file has changed since its last use.
    99   Return a pair of boolean values for .thy and for .ML *)
   100 fun thy_unchanged thy thy_file ml_file = 
   101   let val t = get_thyinfo thy
   102   in if is_some t then
   103        let val ThyInfo {thy_info, ml_info, ...} = the t
   104            val tn = is_none thy_info;
   105            val mn = is_none ml_info
   106        in if not tn andalso not mn then
   107               ((file_info thy_file = the thy_info), 
   108                (file_info ml_file = the ml_info))
   109           else if not tn andalso mn then (true, false)
   110           else (false, false)
   111        end
   112      else (false, false)
   113   end;
   114 
   115 exception FILE_NOT_FOUND;   (*raised by find_file *)
   116 
   117 (*Find a file using a list of paths if no absolute or relative path is
   118   specified.*)
   119 fun find_file "" name =
   120       let fun find_it (curr :: paths) =
   121                 if file_exists (tack_on curr name) then
   122                     tack_on curr name
   123                 else 
   124                     find_it paths
   125            | find_it [] = ""
   126       in find_it (!loadpath) end
   127   | find_file path name =
   128       if file_exists (tack_on path name) then tack_on path name
   129                                          else "";
   130 
   131 (*Get absolute pathnames for a new or already loaded theory *)
   132 fun get_filenames path name =
   133   let fun make_absolute file =
   134         if file = "" then "" else 
   135             if hd (explode file) = "/" then file else tack_on (pwd ()) file;
   136 
   137       fun new_filename () =
   138         let val found = find_file path (name ^ ".thy")
   139                         handle FILE_NOT_FOUND => "";
   140             val thy_file = make_absolute found;
   141             val (thy_path, _) = split_filename thy_file;
   142             val found = find_file path (name ^ ".ML");
   143             val ml_file = if thy_file = "" then make_absolute found
   144                           else if file_exists (tack_on thy_path (name ^ ".ML"))
   145                           then tack_on thy_path (name ^ ".ML")
   146                           else "";
   147             val searched_dirs = if path = "" then (!loadpath) else [path]
   148         in if thy_file = "" andalso ml_file = "" then
   149              error ("Could not find file \"" ^ name ^ ".thy\" or \""
   150                     ^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n"
   151                     ^ "in the following directories: \"" ^
   152                     (space_implode "\", \"" searched_dirs) ^ "\"")
   153            else ();
   154            (thy_file, ml_file) 
   155         end;
   156 
   157       val thy = get_thyinfo name
   158   in if is_some thy andalso path = "" then
   159        let val ThyInfo {path = abs_path, ...} = the thy;
   160            val (thy_file, ml_file) = if abs_path = "" then new_filename ()
   161                                      else (find_file abs_path (name ^ ".thy"),
   162                                            find_file abs_path (name ^ ".ML"))
   163        in if thy_file = "" andalso ml_file = "" then
   164             (writeln ("Warning: File \"" ^ (tack_on path name)
   165                       ^ ".thy\"\ncontaining theory \"" ^ name
   166                       ^ "\" no longer exists.");
   167              new_filename ()
   168             )
   169           else (thy_file, ml_file)
   170        end
   171      else new_filename ()
   172   end;
   173 
   174 (*Remove theory from all child lists in loaded_thys *)
   175 fun unlink_thy thy =
   176   let fun remove name path children thy_info ml_info theory =
   177             (ThyInfo {name = name, path = path, children = children \ thy, 
   178                       thy_info = thy_info, ml_info = ml_info,
   179                       theory = theory}, true)
   180   in change_thyinfo remove end;
   181 
   182 (*Remove a theory from loaded_thys *)
   183 fun remove_thy thy =
   184   let fun remove (t :: ts) =
   185             let val ThyInfo {name, ...} = t
   186             in if name = thy then ts
   187                              else t :: (remove ts)
   188             end
   189         | remove [] = []
   190   in loaded_thys := remove (!loaded_thys) end;
   191 
   192 (*Change thy_info and ml_info for an existent item *)
   193 fun set_info thy_new ml_new thy =
   194   let fun change name path children thy_info ml_info theory =
   195         if name = thy then
   196             (ThyInfo {name = name, path = path, children = children,
   197                       thy_info = Some thy_new, ml_info = Some ml_new,
   198                       theory = theory}, false)
   199         else
   200             (ThyInfo {name = name, path = path, children = children,
   201                       thy_info = thy_info, ml_info = ml_info,
   202                       theory = theory}, true)
   203   in change_thyinfo change end;
   204 
   205 (*Mark theory as changed since last read if it has been completly read *)
   206 fun mark_outdated thy =
   207   if already_loaded thy then set_info "" "" thy
   208                         else ();
   209 
   210 (*Read .thy and .ML files that haven't been read yet or have changed since 
   211   they were last read;
   212   loaded_thys is a thy_info list ref containing all theories that have 
   213   completly been read by this and preceeding use_thy calls.
   214   If a theory changed since its last use its children are marked as changed *)
   215 fun use_thy name =
   216     let val (path, thy_name) = split_filename name;
   217         val (thy_file, ml_file) = get_filenames path thy_name;
   218         val (abs_path, _) = if thy_file = "" then split_filename ml_file
   219                             else split_filename thy_file;
   220         val (thy_uptodate, ml_uptodate) = thy_unchanged thy_name 
   221                                                         thy_file ml_file;
   222 
   223          (*Set absolute path for loaded theory *)
   224          fun set_path () =
   225            let fun change name path children thy_info ml_info theory =
   226                  if name = thy_name then            
   227                    (ThyInfo {name = name, path = abs_path, children = children,
   228                              thy_info = thy_info, ml_info = ml_info,
   229                              theory = theory}, false)
   230                  else
   231                    (ThyInfo {name = name, path = path, children = children,
   232                              thy_info = thy_info, ml_info = ml_info,
   233                              theory = theory}, true)
   234            in change_thyinfo change end;
   235 
   236          (*Mark all direct descendants of a theory as changed *)
   237          fun mark_children thy =
   238            let val ThyInfo {children, ...} = the (get_thyinfo thy)
   239                val loaded = filter already_loaded children
   240            in if loaded <> [] then
   241                   (writeln ("The following children of theory " ^ (quote thy)
   242                             ^ " are now out-of-date: "
   243                             ^ (quote (space_implode "\",\"" loaded)));
   244                    seq mark_outdated loaded
   245                   )
   246               else ()
   247            end
   248 
   249     in if thy_uptodate andalso ml_uptodate then ()
   250        else
   251        (
   252          if thy_uptodate orelse thy_file = "" then ()
   253          else (writeln ("Reading \"" ^ name ^ ".thy\"");
   254                read_thy thy_name thy_file;
   255                use (out_name thy_name)
   256               );
   257 
   258          if ml_file = "" then () 
   259          else (writeln ("Reading \"" ^ name ^ ".ML\"");
   260                use ml_file);
   261 
   262          use_string ["store_theory " ^ quote thy_name ^ " " ^ thy_name 
   263                      ^ ".thy;"];
   264 
   265          (*Now set the correct info*)
   266          set_info (file_info thy_file) (file_info ml_file) thy_name;
   267          set_path ();
   268 
   269          (*Mark theories that have to be reloaded*)
   270          mark_children thy_name;
   271 
   272          (*Remove temporary files*)
   273          if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate 
   274            then ()
   275          else delete_file (out_name thy_name)
   276         )
   277     end;
   278 
   279 fun time_use_thy tname = timeit(fn()=>
   280    (writeln("\n**** Starting Theory " ^ tname ^ " ****");  
   281     use_thy tname;
   282     writeln("\n**** Finished Theory " ^ tname ^ " ****"))
   283    );
   284 
   285 (*Load all thy or ML files that have been changed and also
   286   all theories that depend on them *)
   287 fun update () =
   288   let (*List theories in the order they have to be loaded *)
   289       fun load_order [] result = result
   290         | load_order thys result =
   291             let fun next_level (t :: ts) =
   292                       let val thy = get_thyinfo t
   293                       in if is_some thy then
   294                              let val ThyInfo {children, ...} = the thy
   295                              in children union (next_level ts)
   296                              end
   297                          else next_level ts
   298                       end
   299                   | next_level [] = [];
   300                   
   301                 val children = next_level thys
   302             in load_order children ((result \\ children) @ children) end;
   303 
   304       fun reload_changed (t :: ts) =
   305             let val thy = get_thyinfo t;
   306 
   307                 fun abspath () =
   308                   if is_some thy then
   309                     let val ThyInfo {path, ...} = the thy in path end
   310                   else "";
   311 
   312                 val (thy_file, ml_file) = get_filenames (abspath ()) t;
   313                 val (thy_uptodate, ml_uptodate) =
   314                         thy_unchanged t thy_file ml_file;
   315             in if thy_uptodate andalso ml_uptodate then ()
   316                                                    else use_thy t;
   317                reload_changed ts
   318             end
   319         | reload_changed [] = ();
   320 
   321      (*Remove all theories that are no descendants of Pure.
   322        If there are still children in the deleted theory's list
   323        schedule them for reloading *)
   324      fun collect_garbage not_garbage =
   325        let fun collect (t :: ts) =
   326                  let val ThyInfo {name, children, ...} = t
   327                  in if name mem not_garbage then collect ts
   328                     else (writeln("Theory \"" ^ name 
   329                            ^ "\" is no longer linked with Pure - removing it.");
   330                           remove_thy name;
   331                           seq mark_outdated children
   332                          )
   333                  end
   334              | collect [] = ()
   335 
   336        in collect (!loaded_thys) end
   337 
   338   in collect_garbage ("Pure" :: (load_order ["Pure"] []));
   339      reload_changed (load_order ["Pure"] [])
   340   end;
   341 
   342 (*Merge theories to build a base for a new theory.
   343   Base members are only loaded if they are missing. *)
   344 fun base_on bases child =
   345       let (*List all descendants of a theory list *)
   346           fun list_descendants (t :: ts) =
   347                 let val tinfo = get_thyinfo t
   348                 in if is_some tinfo then
   349                      let val ThyInfo {children, ...} = the tinfo
   350                      in children union (list_descendants (ts union children))
   351                      end
   352                    else []
   353                 end
   354             | list_descendants [] = [];
   355 
   356           (*Show the cycle that would be created by add_child *)
   357           fun show_cycle base =
   358             let fun find_it result curr =
   359                   let val tinfo = get_thyinfo curr
   360                   in if base = curr then 
   361                        error ("Cyclic dependency of theories: "
   362                               ^ child ^ "->" ^ base ^ result)
   363                      else if is_some tinfo then
   364                        let val ThyInfo {children, ...} = the tinfo
   365                        in seq (find_it ("->" ^ curr ^ result)) children
   366                        end
   367                      else ()
   368                   end
   369             in find_it "" child end;
   370         
   371           (*Check if a cycle will be created by add_child *)
   372           fun find_cycle base =
   373             if base mem (list_descendants [child]) then show_cycle base
   374             else ();
   375                    
   376           (*Add child to child list of base *)
   377           fun add_child base =
   378             let fun add (t :: loaded) =
   379                       let val ThyInfo {name, path, children,
   380                                        thy_info, ml_info, theory} = t
   381                       in if name = base then
   382                            ThyInfo {name = name, path = path,
   383                                     children = child ins children,
   384                                     thy_info = thy_info, ml_info = ml_info,
   385                                     theory = theory} :: loaded
   386                          else
   387                            t :: (add loaded)
   388                       end
   389                   | add [] =
   390                       [ThyInfo {name = base, path = "", children = [child], 
   391                                 thy_info = None, ml_info = None, theory = None}]
   392             in loaded_thys := add (!loaded_thys) end;       
   393 
   394           (*Load a base theory if not already done
   395             and no cycle would be created *)
   396           fun load base =
   397               let val thy_present = already_loaded base
   398                                             (*test this before child is added *)
   399               in
   400                 if child = base then
   401                     error ("Cyclic dependency of theories: " ^ child
   402                            ^ "->" ^ child)
   403                 else 
   404                   (find_cycle base;
   405                    add_child base;
   406                    if thy_present then ()
   407                    else (writeln ("Autoloading theory " ^ (quote base)
   408                                   ^ " (used by " ^ (quote child) ^ ")");
   409                          use_thy base)
   410                   )
   411               end; 
   412 
   413           (*Load all needed files and make a list of all real theories *)
   414           fun load_base (Thy b :: bs) =
   415                (load b;
   416                 b :: (load_base bs))
   417             | load_base (File b :: bs) =
   418                (load b;
   419                 load_base bs)    (*don't add it to merge_theories' parameter *)
   420             | load_base [] = [];
   421 
   422           (*Get theory object for a loaded theory *)
   423           fun get_theory name =
   424             let val ThyInfo {theory, ...} = the (get_thyinfo name)
   425             in the theory end;
   426 
   427           val mergelist = (unlink_thy child;
   428                            load_base bases);
   429           val (t :: ts) = if mergelist = [] then ["Pure"] else mergelist
   430                                                (*we have to return something *)
   431      in writeln ("Loading theory " ^ (quote child));
   432         foldl Thm.merge_theories (get_theory t, map get_theory ts) end;
   433 
   434 (*Change theory object for an existent item of loaded_thys 
   435   or create a new item *)
   436 fun store_theory thy_name thy =
   437   let fun make_change (t :: loaded) =
   438             let val ThyInfo {name, path, children, thy_info, ml_info, ...} = t
   439             in if name = thy_name then            
   440                     ThyInfo {name = name, path = path, children = children,
   441                              thy_info = thy_info, ml_info = ml_info,
   442                              theory = Some thy} :: loaded
   443                else
   444                     t :: (make_change loaded)
   445             end
   446         | make_change [] =
   447             [ThyInfo {name = thy_name, path = "", children = [],
   448                       thy_info = Some "", ml_info = Some "",
   449                       theory = Some thy}]
   450   in loaded_thys := make_change (!loaded_thys) end;
   451 
   452 end;