Refactor theory-reading API

Hopefully it's a bit clearer for future readers. I also hope to make
it easier to reuse this code for non-theory loading and installation
purposes.

src/postkernel/SharingTables.sig

@@ -5,16 +5,12 @@ sig
   exception SharingTables of string
 
   type id = {Thy : string, Other : string}
-  datatype shared_type = TYV of string
-                       | TYOP of int list
+  datatype shared_type = datatype TheoryReader_dtype.encoded_type
   type thminfo = DB_dtype.thminfo
   val shared_type_decode : shared_type HOLsexp.decoder
   val shared_type_encode : shared_type HOLsexp.encoder
 
-  datatype shared_term = TMV of string * int
-                       | TMC of int * int
-                       | TMAp of int * int
-                       | TMAbs of int * int
+  datatype shared_term = datatype TheoryReader_dtype.encoded_term
   val shared_term_decode : shared_term HOLsexp.decoder
   val shared_term_encode : shared_term HOLsexp.encoder
 
@@ -75,9 +71,8 @@ sig
   val enc_sdata : sharing_data_in HOLsexp.encoder
 
   val dec_sdata :
-      {with_strings: (int -> string) -> unit,
-       with_stridty:
-         (int -> string) * (int -> id) * Type.hol_type Vector.vector -> unit} ->
+      {before_types: unit -> unit,
+       before_terms: Type.hol_type Vector.vector -> unit} ->
       sharing_data_out HOLsexp.decoder
   val export_from_sharing_data : sharing_data_out -> extract_data
   val read_term : sharing_data_out -> string -> Term.term

src/postkernel/SharingTables.sml

@@ -92,8 +92,8 @@ fun build_id_vector strings intpairs =
     Types
    ---------------------------------------------------------------------- *)
 
-datatype shared_type = TYV of string
-                     | TYOP of int list
+open TheoryReader_dtype
+datatype shared_type = datatype encoded_type
 
 type typetable = {tysize : int,
                   tymap : (hol_type, int)Map.dict,
@@ -103,12 +103,15 @@ local
   open HOLsexp
 in
 fun shared_type_encode (TYV s) = String s
-  | shared_type_encode (TYOP is) = List(map Integer is)
+  | shared_type_encode (TYOP {opn,args}) = List(map Integer (opn::args))
 
 fun shared_type_decode s =
     case string_decode s of
         SOME str => SOME (TYV str)
-      | _ => Option.map TYOP (list_decode int_decode s)
+      | _ => case list_decode int_decode s of
+                 NONE => NONE
+               | SOME [] => NONE
+               | SOME (opn::args) => SOME (TYOP {opn=opn, args = args})
 
 val enc_tytable : typetable encoder =
     tagged_encode "type-table" (list_encode shared_type_encode) o List.rev o
@@ -146,7 +149,7 @@ fun make_shared_type ty strtable idtable table =
             (tysize, strtable', idtable',
              {tysize = tysize + 1,
               tymap = Map.insert(tymap, ty, tysize),
-              tylist = TYOP (id :: newargs) :: tylist})
+              tylist = TYOP {opn = id, args = newargs} :: tylist})
           end
       end
 
@@ -157,18 +160,17 @@ fun build_type_vector idv shtylist = let
   fun build1 (shty, (n, tymap)) =
       case shty of
         TYV s => (n + 1, Map.insert(tymap, n, Type.mk_vartype s))
-      | TYOP idargs => let
-          val (id, Args) = valOf (List.getItem idargs)
+      | TYOP {opn,args} => let
           fun mapthis i =
               Map.find(tymap, i)
               handle Map.NotFound =>
                      raise SharingTables ("build_type_vector: (" ^
                                           String.concatWith " "
-                                                (map Int.toString Args) ^
+                                                (map Int.toString args) ^
                                           "), " ^ Int.toString i ^
                                           " not found")
-          val args = map mapthis Args
-          val {Thy,Other} = Vector.sub(idv, id)
+          val args = map mapthis args
+          val {Thy,Other} = Vector.sub(idv, opn)
         in
           (n + 1,
            Map.insert(tymap, n,
@@ -184,11 +186,7 @@ end
     Terms
    ---------------------------------------------------------------------- *)
 
-datatype shared_term = TMV of string * int
-                     | TMC of int * int
-                     | TMAp of int * int
-                     | TMAbs of int * int
-
+datatype shared_term = datatype encoded_term
 type termtable = {termsize : int,
                   termmap : (term, int)Map.dict,
                   termlist : shared_term list}
@@ -585,7 +583,7 @@ fun force s dec t =
         NONE => raise SharingTables ("Couldn't decode \""^s^"\": "^prsexp t)
       | SOME t => t
 
-fun dec_sdata {with_strings,with_stridty} t =
+fun dec_sdata {before_types,before_terms} t =
     let
       open HOLsexp
       val decoder =
@@ -622,10 +620,10 @@ fun dec_sdata {with_strings,with_stridty} t =
                 ((raw_untys, raw_nmtys), (raw_untms, raw_nmtms), rawthms)) =>
           let
             fun sub v i = Vector.sub(v,i)
-            val _ = with_strings (fn i => Vector.sub(strv,i))
+            val _ = before_types ()
             val idv = build_id_vector strv intplist
             val tyv = build_type_vector idv shtylist
-            val _ = with_stridty (sub strv, sub idv, tyv)
+            val _ = before_terms tyv
             val tmv = build_term_vector idv tyv shtmlist
             val untys = map (fn i => Vector.sub(tyv,i)) raw_untys
             val nmtys = map (fn (s,i) => (s, Vector.sub(tyv,i))) raw_nmtys

src/postkernel/Theory.sig

@@ -133,17 +133,22 @@ sig
 
   val format_name_message : {pfx:string,name:string} -> string
 
-(* For internal use *)
+(* For internal use
+
+    incorporate_types and incorporate_consts are versions of new_type and new_constant
+    used in loaded theory files from disk.
+
+    Similarly, link_parents is used when a theory is declared so that
+    its ancestors are identified.
+
+ *)
 
-  val pp_thm                 : (thm -> HOLPP.pretty) ref
   val link_parents           : string*num*num -> (string*num*num) list -> unit
   val incorporate_types      : string -> (string*int) list -> unit
+  val incorporate_consts     : string -> (string*hol_type) list -> unit
+  val pp_thm                 : (thm -> HOLPP.pretty) ref
 
 
-  val store_definition       : string * thm -> thm
-  val gen_store_definition   : string * thm * thm_src_location -> thm
-  val incorporate_consts : string -> hol_type Vector.vector ->
-                           (string*int) list -> unit
   (* Theory files (which are just SML source code) call this function as
      the last thing done when they load.  This will in turn cause a
      TheoryDelta event to be sent to all registered listeners *)

src/postkernel/Theory.sml

@@ -662,10 +662,8 @@ fun incorporate_types thy tys =
   in List.app itype tys
   end;
 
-fun incorporate_consts thy tyvector consts =
-  let fun iconst(s,i) = (install_const(s,Vector.sub(tyvector,i),thy);())
-  in List.app iconst consts
-  end;
+fun incorporate_consts thy consts =
+    List.app (fn (s,ty) => ignore (install_const(s,ty,thy))) consts
 
 (* ----------------------------------------------------------------------
     Theory data functions

src/postkernel/TheoryReader.sig

@@ -5,6 +5,8 @@ sig
   val load_thydata : string -> string ->
                      (Thm.thm * DB_dtype.thminfo) Symtab.table
 
+  type raw = TheoryReader_dtype.raw
+
 end
 
 (* [load_thydata thyname fname] loads the filename and makes the appropriate

src/postkernel/TheoryReader.sml

@@ -13,7 +13,7 @@ type thm      = Thm.thm;
 type term     = Term.term
 type hol_type = Type.hol_type
 
-open HolKernel SharingTables
+open HolKernel SharingTables TheoryReader_dtype
 
 fun temp_encoded_update sdata thyname {data,ty} =
     Theory.LoadableThyData.temp_encoded_update {
@@ -146,11 +146,13 @@ fun load_thydata thyname path =
             )
           )
         ) incorporate_data
-    fun with_strings _ = Theory.incorporate_types thyname new_types
-    fun with_stridty (str,id,tyv) =
-        Theory.incorporate_consts thyname tyv new_consts
+    fun before_types () = Theory.incorporate_types thyname new_types
+    fun before_terms tyv =
+        Theory.incorporate_consts
+          thyname
+          (map (fn (n,i) => (n,Vector.sub(tyv,i))) new_consts)
     val share_data = force "decoding core-data" (
-          dec_sdata {with_strings = with_strings, with_stridty = with_stridty}
+          dec_sdata {before_types = before_types, before_terms = before_terms}
         ) core_data
     val {theorems = named_thms,...} = export_from_sharing_data share_data
 

src/postkernel/TheoryReader_dtype.sml

@@ -0,0 +1,25 @@
+structure TheoryReader_dtype =
+struct
+
+
+type raw_name = {thy : string, tstamp1 : string, tstamp2 : string}
+datatype encoded_type = TYV of string
+                      | TYOP of {opn : int (* ref to idtable *),
+                                 args : int list (* refs to earlier types *)}
+datatype encoded_term = TMV of string * int
+                      | TMC of int * int
+                      | TMAp of int * int
+                      | TMAbs of int * int
+
+type sharing_tables = {stringt : string list,
+                       idt : (int * int) list,
+                       typet : encoded_type list,
+                       termt : encoded_term list}
+type raw =
+     { name : raw_name,
+       ancestors : raw_name list,
+       tables : sharing_tables
+     }
+
+
+end (* struct *)