src/Pure/Thy/thy_read.ML
author lcp
Tue Jul 25 17:03:16 1995 +0200 (1995-07-25 ago)
changeset 1194 563ecd14c1d8
parent 1157 da78c293e8dc
child 1223 53e4b22aa1f2
permissions -rw-r--r--
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
     1 (*  Title:      Pure/Thy/thy_read.ML
     2     ID:         $Id$
     3     Author:     Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and
     4                 Tobias Nipkow and L C Paulson
     5     Copyright   1994 TU Muenchen
     6 
     7 Functions for reading theory files, and storing and retrieving theories
     8 and theorems.
     9 *)
    10 
    11 (*Type for theory storage*)
    12 datatype thy_info = ThyInfo of {path: string,
    13                                 children: string list,
    14                                 thy_time: string option,
    15                                 ml_time: string option,
    16                                 theory: theory option,
    17                                 thms: thm Symtab.table};
    18       (*meaning of special values:
    19         thy_time, ml_time = None     theory file has not been read yet
    20                           = Some ""  theory was read but has either been marked
    21                                      as outdated or there is no such file for
    22                                      this theory (see e.g. 'virtual' theories
    23                                      like Pure or theories without a ML file)
    24         theory = None  theory has not been read yet
    25        *)
    26 
    27 signature READTHY =
    28 sig
    29   datatype basetype = Thy  of string
    30                     | File of string
    31 
    32   val loaded_thys    : thy_info Symtab.table ref
    33   val loadpath       : string list ref
    34   val delete_tmpfiles: bool ref
    35 
    36   val use_thy        : string -> unit
    37   val update         : unit -> unit
    38   val time_use_thy   : string -> unit
    39   val unlink_thy     : string -> unit
    40   val mk_base        : basetype list -> string -> bool -> theory
    41   val store_theory   : theory * string -> unit
    42 
    43   val theory_of_sign: Sign.sg -> theory
    44   val theory_of_thm: thm -> theory
    45   val store_thm: string * thm -> thm
    46   val bind_thm: string * thm -> unit
    47   val qed: string -> unit
    48   val qed_thm: thm ref
    49   val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
    50   val qed_goalw: string -> theory->thm list->string->(thm list->tactic list)
    51                  -> unit
    52   val get_thm: theory -> string -> thm
    53   val thms_of: theory -> (string * thm) list
    54   val print_theory: theory -> unit
    55 end;
    56 
    57 
    58 functor ReadthyFUN(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY =
    59 struct
    60 local open ThmDB in
    61 
    62 datatype basetype = Thy  of string
    63                   | File of string;
    64 
    65 val loaded_thys = ref (Symtab.make [("ProtoPure",
    66                                      ThyInfo {path = "",
    67                                        children = ["Pure", "CPure"],
    68                                        thy_time = Some "", ml_time = Some "",
    69                                        theory = Some proto_pure_thy,
    70                                        thms = Symtab.null}),
    71                                     ("Pure", ThyInfo {path = "", children = [],
    72                                        thy_time = Some "", ml_time = Some "",
    73                                        theory = Some pure_thy,
    74                                        thms = Symtab.null}),
    75                                     ("CPure", ThyInfo {path = "",
    76                                        children = [],
    77                                        thy_time = Some "", ml_time = Some "",
    78                                        theory = Some cpure_thy,
    79                                        thms = Symtab.null})]);
    80 
    81 val loadpath = ref ["."];           (*default search path for theory files *)
    82 
    83 val delete_tmpfiles = ref true;         (*remove temporary files after use *)
    84 
    85 (*Make name of the output ML file for a theory *)
    86 fun out_name tname = "." ^ tname ^ ".thy.ML";
    87 
    88 (*Read a file specified by thy_file containing theory thy *)
    89 fun read_thy tname thy_file =
    90   let
    91     val instream  = open_in thy_file;
    92     val outstream = open_out (out_name tname);
    93   in
    94     output (outstream, ThySyn.parse tname (input (instream, 999999)));
    95     close_out outstream;
    96     close_in instream
    97   end;
    98 
    99 fun file_exists file =
   100   let val instream = open_in file in close_in instream; true end
   101     handle Io _ => false;
   102 
   103 (*Get thy_info for a loaded theory *)
   104 fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
   105 
   106 (*Check if a theory was completly loaded *)
   107 fun already_loaded thy =
   108   let val t = get_thyinfo thy
   109   in if is_none t then false
   110      else let val ThyInfo {thy_time, ml_time, ...} = the t
   111           in is_some thy_time andalso is_some ml_time end
   112   end;
   113 
   114 (*Check if a theory file has changed since its last use.
   115   Return a pair of boolean values for .thy and for .ML *)
   116 fun thy_unchanged thy thy_file ml_file =
   117   case get_thyinfo thy of
   118       Some (ThyInfo {thy_time, ml_time, ...}) =>
   119        let val tn = is_none thy_time;
   120            val mn = is_none ml_time
   121        in if not tn andalso not mn then
   122             ((file_info thy_file = the thy_time),
   123              (file_info ml_file = the ml_time))
   124           else if not tn andalso mn then
   125             (file_info thy_file = the thy_time, false)
   126           else
   127             (false, false)
   128        end
   129     | None => (false, false)
   130 
   131 exception FILE_NOT_FOUND;   (*raised by find_file *)
   132 
   133 (*Find a file using a list of paths if no absolute or relative path is
   134   specified.*)
   135 fun find_file "" name =
   136       let fun find_it (curr :: paths) =
   137                 if file_exists (tack_on curr name) then
   138                     tack_on curr name
   139                 else
   140                     find_it paths
   141            | find_it [] = ""
   142       in find_it (!loadpath) end
   143   | find_file path name =
   144       if file_exists (tack_on path name) then tack_on path name
   145                                          else "";
   146 
   147 (*Get absolute pathnames for a new or already loaded theory *)
   148 fun get_filenames path name =
   149   let fun make_absolute file =
   150         if file = "" then "" else
   151             if hd (explode file) = "/" then file else tack_on (pwd ()) file;
   152 
   153       fun new_filename () =
   154         let val found = find_file path (name ^ ".thy")
   155                         handle FILE_NOT_FOUND => "";
   156             val thy_file = make_absolute found;
   157             val (thy_path, _) = split_filename thy_file;
   158             val found = find_file path (name ^ ".ML");
   159             val ml_file = if thy_file = "" then make_absolute found
   160                           else if file_exists (tack_on thy_path (name ^ ".ML"))
   161                           then tack_on thy_path (name ^ ".ML")
   162                           else "";
   163             val searched_dirs = if path = "" then (!loadpath) else [path]
   164         in if thy_file = "" andalso ml_file = "" then
   165              error ("Could not find file \"" ^ name ^ ".thy\" or \""
   166                     ^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n"
   167                     ^ "in the following directories: \"" ^
   168                     (space_implode "\", \"" searched_dirs) ^ "\"")
   169            else ();
   170            (thy_file, ml_file)
   171         end;
   172 
   173       val tinfo = get_thyinfo name;
   174   in if is_some tinfo andalso path = "" then
   175        let val ThyInfo {path = abs_path, ...} = the tinfo;
   176            val (thy_file, ml_file) = if abs_path = "" then new_filename ()
   177                                      else (find_file abs_path (name ^ ".thy"),
   178                                            find_file abs_path (name ^ ".ML"))
   179        in if thy_file = "" andalso ml_file = "" then
   180             (writeln ("Warning: File \"" ^ (tack_on path name)
   181                       ^ ".thy\"\ncontaining theory \"" ^ name
   182                       ^ "\" no longer exists.");
   183              new_filename ()
   184             )
   185           else (thy_file, ml_file)
   186        end
   187      else new_filename ()
   188   end;
   189 
   190 (*Remove theory from all child lists in loaded_thys *)
   191 fun unlink_thy tname =
   192   let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms}) =
   193         ThyInfo {path = path, children = children \ tname,
   194                  thy_time = thy_time, ml_time = ml_time,
   195                  theory = theory, thms = thms}
   196   in loaded_thys := Symtab.map remove (!loaded_thys) end;
   197 
   198 (*Remove a theory from loaded_thys *)
   199 fun remove_thy tname =
   200   loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname)
   201                  (Symtab.dest (!loaded_thys)));
   202 
   203 (*Change thy_time and ml_time for an existent item *)
   204 fun set_info thy_time ml_time tname =
   205   let val ThyInfo {path, children, theory, thms, ...} =
   206         the (Symtab.lookup (!loaded_thys, tname));
   207   in loaded_thys := Symtab.update ((tname,
   208        ThyInfo {path = path, children = children,
   209                 thy_time = thy_time, ml_time = ml_time,
   210                 theory = theory, thms = thms}), !loaded_thys)
   211   end;
   212 
   213 (*Mark theory as changed since last read if it has been completly read *)
   214 fun mark_outdated tname =
   215   let val t = get_thyinfo tname;
   216   in if is_none t then ()
   217      else let val ThyInfo {thy_time, ml_time, ...} = the t
   218           in set_info (if is_none thy_time then None else Some "")
   219                       (if is_none ml_time then None else Some "")
   220                       tname
   221           end
   222   end;
   223 
   224 (*Read .thy and .ML files that haven't been read yet or have changed since
   225   they were last read;
   226   loaded_thys is a thy_info list ref containing all theories that have
   227   completly been read by this and preceeding use_thy calls.
   228   If a theory changed since its last use its children are marked as changed *)
   229 fun use_thy name =
   230     let val (path, tname) = split_filename name;
   231         val (thy_file, ml_file) = get_filenames path tname;
   232         val (abs_path, _) = if thy_file = "" then split_filename ml_file
   233                             else split_filename thy_file;
   234         val (thy_uptodate, ml_uptodate) = thy_unchanged tname
   235                                                         thy_file ml_file;
   236 
   237          (*Set absolute path for loaded theory *)
   238          fun set_path () =
   239            let val ThyInfo {children, thy_time, ml_time, theory, thms, ...} =
   240                  the (Symtab.lookup (!loaded_thys, tname));
   241            in loaded_thys := Symtab.update ((tname,
   242                                ThyInfo {path = abs_path, children = children,
   243                                         thy_time = thy_time, ml_time = ml_time,
   244                                         theory = theory, thms = thms}),
   245                                !loaded_thys)
   246            end;
   247 
   248          (*Mark all direct descendants of a theory as changed *)
   249          fun mark_children thy =
   250            let val ThyInfo {children, ...} = the (get_thyinfo thy);
   251                val present = filter (is_some o get_thyinfo) children;
   252                val loaded = filter already_loaded present;
   253            in if loaded <> [] then
   254                 writeln ("The following children of theory " ^ (quote thy)
   255                          ^ " are now out-of-date: "
   256                          ^ (quote (space_implode "\",\"" loaded)))
   257               else ();
   258               seq mark_outdated present
   259            end;
   260 
   261         (*Remove all theorems associated with a theory*)
   262         fun delete_thms () =
   263           let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
   264              Some (ThyInfo {path, children, thy_time, ml_time, theory, ...}) =>
   265                  ThyInfo {path = path, children = children,
   266                           thy_time = thy_time, ml_time = ml_time,
   267                           theory = theory, thms = Symtab.null}
   268            | None => ThyInfo {path = "", children = [],
   269                               thy_time = None, ml_time = None,
   270                               theory = None, thms = Symtab.null};
   271          in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
   272     in if thy_uptodate andalso ml_uptodate then ()
   273        else
   274        (
   275          delete_thms ();
   276 
   277          if thy_uptodate orelse thy_file = "" then ()
   278          else (writeln ("Reading \"" ^ name ^ ".thy\"");
   279                read_thy tname thy_file;
   280                use (out_name tname);
   281 
   282                if not (!delete_tmpfiles) then ()
   283                else delete_file (out_name tname)
   284               );
   285          set_info (Some (file_info thy_file)) None tname;
   286                                        (*mark thy_file as successfully loaded*)
   287 
   288          if ml_file = "" then ()
   289          else (writeln ("Reading \"" ^ name ^ ".ML\"");
   290                use ml_file);
   291 
   292          use_string
   293            ["val _ = (store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");\
   294             \map store_thm_db (axioms_of " ^ tname ^ ".thy));"];
   295                     (*Store theory again because it could have been redefined*)
   296 
   297          (*Now set the correct info*)
   298          set_info (Some (file_info thy_file)) (Some (file_info ml_file)) tname;
   299          set_path ();
   300 
   301          (*Mark theories that have to be reloaded*)
   302          mark_children tname
   303         )
   304     end;
   305 
   306 fun time_use_thy tname = timeit(fn()=>
   307    (writeln("\n**** Starting Theory " ^ tname ^ " ****");
   308     use_thy tname;
   309     writeln("\n**** Finished Theory " ^ tname ^ " ****"))
   310    );
   311 
   312 (*Load all thy or ML files that have been changed and also
   313   all theories that depend on them *)
   314 fun update () =
   315   let (*List theories in the order they have to be loaded *)
   316       fun load_order [] result = result
   317         | load_order thys result =
   318             let fun next_level (t :: ts) =
   319                       let val thy = get_thyinfo t
   320                       in if is_some thy then
   321                              let val ThyInfo {children, ...} = the thy
   322                              in children union (next_level ts) end
   323                          else next_level ts
   324                       end
   325                   | next_level [] = [];
   326 
   327                 val children = next_level thys;
   328             in load_order children ((result \\ children) @ children) end;
   329 
   330       fun reload_changed (t :: ts) =
   331             let val thy = get_thyinfo t;
   332 
   333                 fun abspath () =
   334                   if is_some thy then
   335                     let val ThyInfo {path, ...} = the thy in path end
   336                   else "";
   337 
   338                 val (thy_file, ml_file) = get_filenames (abspath ()) t;
   339                 val (thy_uptodate, ml_uptodate) =
   340                         thy_unchanged t thy_file ml_file;
   341             in if thy_uptodate andalso ml_uptodate then ()
   342                                                    else use_thy t;
   343                reload_changed ts
   344             end
   345         | reload_changed [] = ();
   346 
   347      (*Remove all theories that are no descendants of ProtoPure.
   348        If there are still children in the deleted theory's list
   349        schedule them for reloading *)
   350      fun collect_garbage not_garbage =
   351        let fun collect ((tname, ThyInfo {children, ...}) :: ts) =
   352                  if tname mem not_garbage then collect ts
   353                  else (writeln ("Theory \"" ^ tname ^
   354                        "\" is no longer linked with ProtoPure - removing it.");
   355                        remove_thy tname;
   356                        seq mark_outdated children)
   357              | collect [] = ()
   358 
   359        in collect (Symtab.dest (!loaded_thys)) end;
   360   in collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] []));
   361      reload_changed (load_order ["Pure", "CPure"] [])
   362   end;
   363 
   364 (*Merge theories to build a base for a new theory.
   365   Base members are only loaded if they are missing. *)
   366 fun mk_base bases child mk_draft =
   367       let (*List all descendants of a theory list *)
   368           fun list_descendants (t :: ts) =
   369                 let val tinfo = get_thyinfo t
   370                 in if is_some tinfo then
   371                      let val ThyInfo {children, ...} = the tinfo
   372                      in children union (list_descendants (ts union children))
   373                      end
   374                    else []
   375                 end
   376             | list_descendants [] = [];
   377 
   378           (*Show the cycle that would be created by add_child *)
   379           fun show_cycle base =
   380             let fun find_it result curr =
   381                   let val tinfo = get_thyinfo curr
   382                   in if base = curr then
   383                        error ("Cyclic dependency of theories: "
   384                               ^ child ^ "->" ^ base ^ result)
   385                      else if is_some tinfo then
   386                        let val ThyInfo {children, ...} = the tinfo
   387                        in seq (find_it ("->" ^ curr ^ result)) children
   388                        end
   389                      else ()
   390                   end
   391             in find_it "" child end;
   392 
   393           (*Check if a cycle would be created by add_child *)
   394           fun find_cycle base =
   395             if base mem (list_descendants [child]) then show_cycle base
   396             else ();
   397 
   398           (*Add child to child list of base *)
   399           fun add_child base =
   400             let val tinfo =
   401                   case Symtab.lookup (!loaded_thys, base) of
   402                       Some (ThyInfo {path, children, thy_time, ml_time,
   403                                      theory, thms}) =>
   404                         ThyInfo {path = path, children = child ins children,
   405                                  thy_time = thy_time, ml_time = ml_time,
   406                                  theory = theory, thms = thms}
   407                     | None => ThyInfo {path = "", children = [child],
   408                                        thy_time = None, ml_time = None,
   409                                        theory = None, thms = Symtab.null};
   410             in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
   411 
   412           (*Load a base theory if not already done
   413             and no cycle would be created *)
   414           fun load base =
   415               let val thy_loaded = already_loaded base
   416                                            (*test this before child is added *)
   417               in
   418                 if child = base then
   419                     error ("Cyclic dependency of theories: " ^ child
   420                            ^ "->" ^ child)
   421                 else
   422                   (find_cycle base;
   423                    add_child base;
   424                    if thy_loaded then ()
   425                    else (writeln ("Autoloading theory " ^ (quote base)
   426                                   ^ " (used by " ^ (quote child) ^ ")");
   427                          use_thy base)
   428                   )
   429               end;
   430 
   431           (*Load all needed files and make a list of all real theories *)
   432           fun load_base (Thy b :: bs) =
   433                (load b;
   434                 b :: (load_base bs))
   435             | load_base (File b :: bs) =
   436                (load b;
   437                 load_base bs)                    (*don't add it to mergelist *)
   438             | load_base [] = [];
   439 
   440           (*Get theory object for a loaded theory *)
   441           fun get_theory name =
   442             let val ThyInfo {theory, ...} = the (get_thyinfo name)
   443             in the theory end;
   444 
   445           val mergelist = (unlink_thy child;
   446                            load_base bases);
   447      in writeln ("Loading theory " ^ (quote child));
   448         merge_thy_list mk_draft (map get_theory mergelist) end;
   449 
   450 (*Change theory object for an existent item of loaded_thys
   451   or create a new item; also store axioms in Thm database*)
   452 fun store_theory (thy, tname) =
   453   let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
   454                Some (ThyInfo {path, children, thy_time, ml_time, thms, ...}) =>
   455                  ThyInfo {path = path, children = children,
   456                           thy_time = thy_time, ml_time = ml_time,
   457                           theory = Some thy, thms = thms}
   458              | None => ThyInfo {path = "", children = [],
   459                                 thy_time = None, ml_time = None,
   460                                 theory = Some thy, thms = Symtab.null};
   461   in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
   462   end;
   463 
   464 
   465 (** store and retrieve theorems **)
   466 
   467 (*Guess to which theory a signature belongs and return it's thy_info*)
   468 fun thyinfo_of_sign sg =
   469   let
   470     val ref xname = hd (#stamps (Sign.rep_sg sg));
   471     val opt_info = get_thyinfo xname;
   472 
   473     fun eq_sg (ThyInfo {theory = None, ...}) = false
   474       | eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy);
   475 
   476     val show_sg = Pretty.str_of o Sign.pretty_sg;
   477   in
   478     if is_some opt_info andalso eq_sg (the opt_info) then
   479       (xname, the opt_info)
   480     else
   481       (case Symtab.find_first (eq_sg o snd) (!loaded_thys) of
   482         Some name_info => name_info
   483       | None => error ("Theory " ^ show_sg sg ^ " not stored by loader"))
   484   end;
   485 
   486 
   487 (*Try to get the theory object corresponding to a given signature*)
   488 fun theory_of_sign sg =
   489   (case thyinfo_of_sign sg of
   490     (_, ThyInfo {theory = Some thy, ...}) => thy
   491   | _ => sys_error "theory_of_sign");
   492 
   493 (*Try to get the theory object corresponding to a given theorem*)
   494 val theory_of_thm = theory_of_sign o #sign o rep_thm;
   495 
   496 
   497 (* Store theorems *)
   498 
   499 (*Store a theorem in the thy_info of its theory*)
   500 fun store_thm (name, thm) =
   501   let
   502     val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms}) =
   503       thyinfo_of_sign (#sign (rep_thm thm));
   504     val thms' = Symtab.update_new ((name, thm), thms)
   505       handle Symtab.DUPLICATE s => 
   506         (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
   507            (writeln ("Warning: Theorem database already contains copy of\
   508                      \ theorem " ^ quote name);
   509             thms)
   510          else error ("Duplicate theorem name " ^ quote s));
   511   in
   512     loaded_thys := Symtab.update
   513      ((thy_name, ThyInfo {path = path, children = children,
   514        thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms'}),
   515       ! loaded_thys);
   516     store_thm_db (name, thm)
   517   end;
   518 
   519 (*Store result of proof in loaded_thys and as ML value*)
   520 
   521 val qed_thm = ref flexpair_def(*dummy*);
   522 
   523 fun bind_thm (name, thm) =
   524   (qed_thm := thm;
   525    use_string ["val " ^ name ^ " = standard (store_thm (" ^ quote name ^
   526                ", !qed_thm));"]);
   527 
   528 fun qed name =
   529   use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^ ", result ());"];
   530 
   531 fun qed_goal name thy agoal tacsf =
   532   (qed_thm := prove_goal thy agoal tacsf;
   533    use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^", !qed_thm);"]);
   534 
   535 fun qed_goalw name thy rths agoal tacsf =
   536   (qed_thm := prove_goalw thy rths agoal tacsf;
   537    use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^", !qed_thm);"]);
   538 
   539 
   540 (* Retrieve theorems *)
   541 
   542 (*Get all direct ancestors of a theory*)
   543 fun get_parents child =
   544   let fun has_child (tname, ThyInfo {children, theory, ...}) = 
   545         if child mem children then Some tname else None;
   546   in mapfilter has_child (Symtab.dest (!loaded_thys)) end;
   547 
   548 (*Get all theorems belonging to a given theory*)
   549 fun thmtab_ofthy thy =
   550   let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy);
   551   in thms end;
   552 
   553 fun thmtab_ofname name =
   554   let val ThyInfo {thms, ...} = the (get_thyinfo name);
   555   in thms end;
   556 
   557 (*Get a stored theorem specified by theory and name*)
   558 fun get_thm thy name =
   559   let fun get [] [] searched =
   560            raise THEORY ("get_thm: no theorem " ^ quote name, [thy])
   561         | get [] ng searched =
   562             get (ng \\ searched) [] searched
   563         | get (t::ts) ng searched =
   564             (case Symtab.lookup (thmtab_ofname t, name) of
   565                  Some thm => thm
   566                | None => get ts (ng union (get_parents t)) (t::searched));
   567 
   568       val (tname, _) = thyinfo_of_sign (sign_of thy);
   569   in get [tname] [] [] end;
   570 
   571 (*Get stored theorems of a theory*)
   572 val thms_of = Symtab.dest o thmtab_ofthy;
   573 
   574 
   575 (* print theory *)
   576 
   577 fun print_thms thy =
   578   let
   579     val thms = thms_of thy;
   580     fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
   581       Pretty.quote (pretty_thm th)];
   582   in
   583     Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
   584   end;
   585 
   586 fun print_theory thy = (Drule.print_theory thy; print_thms thy);
   587 
   588 end
   589 end;