# HG changeset patch # User clasohm # Date 816961837 -3600 # Node ID 71124bd19b40f64f74527fb56d0bc4e80b344f8c # Parent 0b63af4a2627310845fd4348aef932111a8c662e added functions for storing and retrieving information about datatypes diff -r 0b63af4a2627 -r 71124bd19b40 src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Tue Nov 21 13:47:06 1995 +0100 +++ b/src/Pure/Thy/thy_read.ML Tue Nov 21 14:50:37 1995 +0100 @@ -15,7 +15,8 @@ thy_time: string option, ml_time: string option, theory: theory option, thms: thm Symtab.table, thy_ss: Simplifier.simpset option, - simpset: Simplifier.simpset option}; + simpset: Simplifier.simpset option, + datatypes: (string * string list) list}; (*meaning of special values: thy_time, ml_time = None theory file has not been read yet = Some "" theory was read but has either been marked @@ -32,6 +33,8 @@ origin of the simpsets: thy_ss: snapshot of !Simpset.simpset after .thy file was read simpset: snapshot of !Simpset.simpset after .ML file was read + datatypes: list of constructors for each datatype that has been + defined in this theory *) signature READTHY = @@ -67,8 +70,12 @@ val get_thm : theory -> string -> thm val thms_of : theory -> (string * thm) list val simpset_of : string -> Simplifier.simpset + val print_theory : theory -> unit + val store_datatype : string * string list -> unit + val datatypes_of : theory -> (string * string list) list + val base_path : string ref val gif_path : string ref val index_path : string ref @@ -93,20 +100,20 @@ children = ["Pure", "CPure"], parents = [], thy_time = Some "", ml_time = Some "", theory = Some proto_pure_thy, thms = Symtab.null, - thy_ss = None, simpset = None}), + thy_ss = None, simpset = None, datatypes = []}), ("Pure", ThyInfo {path = "", children = [], parents = ["ProtoPure"], thy_time = Some "", ml_time = Some "", theory = Some pure_thy, thms = Symtab.null, - thy_ss = None, simpset = None}), + thy_ss = None, simpset = None, datatypes = []}), ("CPure", ThyInfo {path = "", children = [], parents = ["ProtoPure"], thy_time = Some "", ml_time = Some "", theory = Some cpure_thy, thms = Symtab.null, - thy_ss = None, simpset = None}) + thy_ss = None, simpset = None, datatypes = []}) ]); val loadpath = ref ["."]; (*default search path for theory files*) @@ -149,7 +156,7 @@ val cur_has_title = ref false; (*Name of theory currently being read*) -val cur_name = ref ""; +val cur_thyname = ref ""; @@ -294,10 +301,11 @@ (*Remove theory from all child lists in loaded_thys *) fun unlink_thy tname = let fun remove (ThyInfo {path, children, parents, thy_time, ml_time, - theory, thms, thy_ss, simpset}) = + theory, thms, thy_ss, simpset, datatypes}) = ThyInfo {path = path, children = children \ tname, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, - thms = thms, thy_ss = thy_ss, simpset = simpset} + thms = thms, thy_ss = thy_ss, simpset = simpset, + datatypes = datatypes} in loaded_thys := Symtab.map remove (!loaded_thys) end; (*Remove a theory from loaded_thys *) @@ -309,14 +317,13 @@ fun set_info tname thy_time ml_time = let val tinfo = case Symtab.lookup (!loaded_thys, tname) of Some (ThyInfo {path, children, parents, theory, thms, - thy_ss, simpset,...}) => + thy_ss, simpset, datatypes, ...}) => ThyInfo {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, - thy_ss = thy_ss, simpset = simpset} + thy_ss = thy_ss, simpset = simpset, datatypes = datatypes} | None => error ("set_info: theory " ^ tname ^ " not found"); - in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) - end; + in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; (*Mark theory as changed since last read if it has been completly read *) fun mark_outdated tname = @@ -503,7 +510,6 @@ else (); cur_htmlfile := Some (open_out (tack_on tpath ("." ^ tname ^ ".html"))); cur_has_title := false; - cur_name := tname; output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy")); mk_charthead sup_out tname "Ancestors" true gif_path rel_index_path @@ -544,14 +550,15 @@ (*Set absolute path for loaded theory *) fun set_path () = let val ThyInfo {children, parents, thy_time, ml_time, theory, thms, - thy_ss, simpset, ...} = + thy_ss, simpset, datatypes, ...} = the (Symtab.lookup (!loaded_thys, tname)); in loaded_thys := Symtab.update ((tname, ThyInfo {path = abs_path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, - thy_ss = thy_ss, simpset = simpset}), + thy_ss = thy_ss, simpset = simpset, + datatypes = datatypes}), !loaded_thys) end; @@ -568,20 +575,21 @@ seq mark_outdated present end; - (*Remove theorems associated with a theory*) + (*Remove theorems and datatypes associated with a theory*) fun delete_thms () = let val tinfo = case get_thyinfo tname of Some (ThyInfo {path, children, parents, thy_time, ml_time, theory, - thy_ss, simpset, ...}) => + thy_ss, simpset, datatypes, ...}) => ThyInfo {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = Symtab.null, - thy_ss = thy_ss, simpset = simpset} + thy_ss = thy_ss, simpset = simpset, + datatypes = []} | None => ThyInfo {path = "", children = [], parents = [], thy_time = None, ml_time = None, theory = None, thms = Symtab.null, - thy_ss = None, simpset = None}; + thy_ss = None, simpset = None, datatypes = []}; val ThyInfo {theory, ...} = tinfo; in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); @@ -592,27 +600,30 @@ fun save_thy_ss () = let val ThyInfo {path, children, parents, thy_time, ml_time, - theory, thms, simpset, ...} = the (get_thyinfo tname); + theory, thms, simpset, datatypes, ...} = + the (get_thyinfo tname); in loaded_thys := Symtab.update ((tname, ThyInfo {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, thy_ss = Some (!Simplifier.simpset), - simpset = simpset}), + simpset = simpset, datatypes = datatypes}), !loaded_thys) end; fun save_simpset () = let val ThyInfo {path, children, parents, thy_time, ml_time, - theory, thms, thy_ss, ...} = the (get_thyinfo tname); + theory, thms, thy_ss, datatypes, ...} = + the (get_thyinfo tname); in loaded_thys := Symtab.update ((tname, ThyInfo {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, thy_ss = thy_ss, - simpset = Some (!Simplifier.simpset)}), + simpset = Some (!Simplifier.simpset), + datatypes = datatypes}), !loaded_thys) end; @@ -653,7 +664,8 @@ end in if thy_uptodate andalso ml_uptodate then () else - (if thy_file = "" then () + (cur_thyname := tname; + if thy_file = "" then () else if thy_uptodate then simpset := let val ThyInfo {thy_ss, ...} = the (get_thyinfo tname); in the thy_ss end @@ -799,16 +811,18 @@ let val tinfo = case Symtab.lookup (!loaded_thys, base) of Some (ThyInfo {path, children, parents, thy_time, ml_time, - theory, thms, thy_ss, simpset}) => + theory, thms, thy_ss, simpset, datatypes}) => ThyInfo {path = path, children = child ins children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, - thy_ss = thy_ss, simpset = simpset} + thy_ss = thy_ss, simpset = simpset, + datatypes = datatypes} | None => ThyInfo {path = "", children = [child], parents = [], thy_time = None, ml_time = None, theory = None, thms = Symtab.null, - thy_ss = None, simpset = None}; + thy_ss = None, simpset = None, + datatypes = []}; in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; (*Load a base theory if not already done @@ -850,12 +864,13 @@ val dummy = let val tinfo = case Symtab.lookup (!loaded_thys, child) of Some (ThyInfo {path, children, thy_time, ml_time, theory, thms, - thy_ss, simpset, ...}) => + thy_ss, simpset, datatypes, ...}) => ThyInfo {path = path, children = children, parents = mergelist, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, - thy_ss = thy_ss, simpset = simpset} + thy_ss = thy_ss, simpset = simpset, + datatypes = datatypes} | None => error ("set_parents: theory " ^ child ^ " not found"); in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end; @@ -869,17 +884,18 @@ fun store_theory (thy, tname) = let val tinfo = case Symtab.lookup (!loaded_thys, tname) of Some (ThyInfo {path, children, parents, thy_time, ml_time, thms, - thy_ss, simpset, ...}) => + thy_ss, simpset, datatypes, ...}) => ThyInfo {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = Some thy, thms = thms, - thy_ss = thy_ss, simpset = simpset} + thy_ss = thy_ss, simpset = simpset, + datatypes = datatypes} | None => error ("store_theory: theory " ^ tname ^ " not found"); in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; -(** store and retrieve theorems **) +(*** Store and retrieve theorems ***) (*Guess to which theory a signature belongs and return it's thy_info*) fun thyinfo_of_sign sg = @@ -911,14 +927,14 @@ val theory_of_thm = theory_of_sign o #sign o rep_thm; -(* Store theorems *) +(** Store theorems **) (*Store a theorem in the thy_info of its theory, and in the theory's HTML file*) fun store_thm (name, thm) = let val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time, - theory, thms, thy_ss, simpset}) = + theory, thms, thy_ss, simpset, datatypes}) = thyinfo_of_sign (#sign (rep_thm thm)); val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false) @@ -941,7 +957,7 @@ (if not (!cur_has_title) then (cur_has_title := true; output (out, "

Theorems proved in " ^ (!cur_name) ^ + (!cur_thyname) ^ ".ML\">" ^ (!cur_thyname) ^ ".ML:

\n")) else (); output (out, "" ^ name ^ "\n
" ^
@@ -955,7 +971,8 @@
      ((thy_name, ThyInfo {path = path, children = children, parents = parents,
                           thy_time = thy_time, ml_time = ml_time,
                           theory = theory, thms = thms',
-                          thy_ss = thy_ss, simpset = simpset}),
+                          thy_ss = thy_ss, simpset = simpset,
+                          datatypes = datatypes}),
       !loaded_thys);
     thm_to_html ();
     if duplicate then thm else store_thm_db (name, thm)
@@ -986,7 +1003,7 @@
   use_string ["val " ^ name ^ " = !qed_thm;"]);
 
 
-(* Retrieve theorems *)
+(** Retrieve theorems **)
 
 (*Get all theorems belonging to a given theory*)
 fun thmtab_of_thy thy =
@@ -1014,29 +1031,10 @@
 (*Get stored theorems of a theory*)
 val thms_of = Symtab.dest o thmtab_of_thy;
 
-(*Get simpset of a theory*)
-fun simpset_of tname =
-  case get_thyinfo tname of
-      Some (ThyInfo {simpset, ...}) =>
-        if is_some simpset then the simpset
-        else error ("Simpset of theory " ^ tname ^ " has not been stored yet")
-    | None => error ("Theory " ^ tname ^ " not stored by loader");
-
-(* print theory *)
-
-fun print_thms thy =
-  let
-    val thms = thms_of thy;
-    fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
-      Pretty.quote (pretty_thm th)];
-  in
-    Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
-  end;
-
-fun print_theory thy = (Drule.print_theory thy; print_thms thy);
 
 
-(* Misc HTML functions *)
+
+(*** Misc HTML functions ***)
 
 (*Init HTML generator by setting paths and creating new files*)
 fun init_html () =
@@ -1151,7 +1149,53 @@
      if level = 0 then () else link_directory ()
   end;
 
-(*CD to a directory and load its ROOT.ML file*)
+
+(*** Print theory ***)
+
+fun print_thms thy =
+  let
+    val thms = thms_of thy;
+    fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
+      Pretty.quote (pretty_thm th)];
+  in
+    Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
+  end;
+
+fun print_theory thy = (Drule.print_theory thy; print_thms thy);
+
+
+(*** Store and retrieve information about datatypes ***)
+fun store_datatype (name, cons) =
+  let val tinfo = case get_thyinfo (!cur_thyname) of
+        Some (ThyInfo {path, children, parents, thy_time, ml_time, theory,
+                       thms, thy_ss, simpset, datatypes}) =>
+          ThyInfo {path = path, children = children, parents = parents,
+                   thy_time = thy_time, ml_time = ml_time,
+                   theory = theory, thms = thms,
+                   thy_ss = thy_ss, simpset = simpset,
+                   datatypes = (name, cons) :: datatypes}
+      | None => error "store_datatype: theory not found";
+  in
+writeln ("*** Storing datatype " ^ name ^ " (" ^ commas cons ^ ") for theory " ^ (!cur_thyname));
+     loaded_thys := Symtab.update ((!cur_thyname, tinfo), !loaded_thys) end;
+
+fun datatypes_of thy =
+  let val (_, ThyInfo {datatypes, ...}) = thyinfo_of_sign (sign_of thy);
+  in datatypes end;
+
+
+(*** Misc functions ***)
+
+(*Get simpset of a theory*)
+fun simpset_of tname =
+  case get_thyinfo tname of
+      Some (ThyInfo {simpset, ...}) =>
+        if is_some simpset then the simpset
+        else error ("Simpset of theory " ^ tname ^ " has not been stored yet")
+    | None => error ("Theory " ^ tname ^ " not stored by loader");
+
+(*CD to a directory and load its ROOT.ML file;
+  also do some work for HTML generation*)
 fun use_dir dirname =
   (cd dirname;
    if !make_html then init_html() else ();