Refactor more theory-reading code

- The "raw" theory stuff now exists in src/portableML/rawtheory;
  none of this depends on the kernel and can be used to read .dat
  files independently
- The kernel-dependent use of that code remains in src/postkernel

src/postkernel/DB_dtype.sml

@@ -1,38 +1,49 @@
 structure DB_dtype =
 struct
 
- datatype class = Thm | Axm | Def
- datatype location = Local of string | Stored of KernelSig.kernelname
- datatype thm_src_location =
-          Located of {scriptpath: string, linenum : int, exact : bool}
-        | Unknown
- fun inexactify_locn (Located{scriptpath,linenum,exact}) =
-       Located{scriptpath=scriptpath,linenum=linenum,exact=false}
-   | inexactify_locn Unknown = Unknown
+open RawTheory_dtype
+(* two flavours of "location"; the first with exactly that name is the logical/signature
+   location of a theorem: it's either local to the current session/segment and is not
+   going to persist, or it's bound to a particular kernelname
+*)
+datatype location = Local of string | Stored of KernelSig.kernelname
+(* the second flavour is the location of the SML declaration and definition of the
+   theorem value *)
+datatype thm_src_location =
+         Located of {scriptpath: string, linenum : int, exact : bool}
+       | Unknown
+fun inexactify_locn (Located{scriptpath,linenum,exact}) =
+      Located{scriptpath=scriptpath,linenum=linenum,exact=false}
+  | inexactify_locn Unknown = Unknown
+fun mkloc(s,i,b) =
+    Located{
+      scriptpath = holpathdb.reverse_lookup{path=s},
+      linenum = i,
+      exact = b
+    }
 
- datatype theory =
-          THEORY of string *
-                {types       : (string * int) list,
-                 consts      : (string * Type.hol_type) list,
-                 parents     : string list,
-                 axioms      : (string * Thm.thm) list,
-                 definitions : (string * Thm.thm) list,
-                 theorems    : (string * Thm.thm) list}
+type thminfo = {private: bool, loc:thm_src_location,class:class}
+fun updsrcloc f {private,loc,class} =
+    {private = private,loc = f loc,class = class}
 
- datatype selector = SelTM of Term.term | SelNM of string | SelTHY of string
- type thminfo = {private: bool, loc:thm_src_location,class:class}
- type data_value = (Thm.thm * thminfo)
- type public_data_value = Thm.thm * class * thm_src_location
- fun dvdrop_private ((th,i) : data_value) : public_data_value =
-     (th,#class i,#loc i)
- type 'a named = (string * string) * 'a
- type data = data_value named
- type public_data = public_data_value named
- fun drop_private (nms, dv) = (nms, dvdrop_private dv)
+datatype theory =
+         THEORY of string *
+                   {types       : (string * int) list,
+                    consts      : (string * Type.hol_type) list,
+                    parents     : string list,
+                    axioms      : (string * Thm.thm) list,
+                    definitions : (string * Thm.thm) list,
+                    theorems    : (string * Thm.thm) list}
+
+datatype selector = SelTM of Term.term | SelNM of string | SelTHY of string
+type data_value = (Thm.thm * thminfo)
+type public_data_value = Thm.thm * class * thm_src_location
+fun dvdrop_private ((th,i) : data_value) : public_data_value =
+    (th,#class i,#loc i)
+type 'a named = (string * string) * 'a
+type data = data_value named
+type public_data = public_data_value named
+fun drop_private (nms, dv) = (nms, dvdrop_private dv)
 
- fun mkloc(s,i,b) = Located{scriptpath = holpathdb.reverse_lookup{path=s},
-                            linenum = i, exact = b}
- fun updsrcloc f {private,loc,class} =
-     {private = private,loc = f loc,class = class}
 
 end

src/postkernel/SharingTables.sig

@@ -5,14 +5,9 @@ sig
   exception SharingTables of string
 
   type id = {Thy : string, Other : string}
-  datatype shared_type = datatype TheoryReader_dtype.encoded_type
+  datatype raw_type = datatype RawTheory_dtype.raw_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 = datatype TheoryReader_dtype.encoded_term
-  val shared_term_decode : shared_term HOLsexp.decoder
-  val shared_term_encode : shared_term HOLsexp.encoder
+  datatype raw_term = datatype RawTheory_dtype.raw_term
 
   type stringtable =
        {size : int, map : (string,int) Map.dict, list : string list}
@@ -21,10 +16,10 @@ sig
                   idlist : (int * int) list}
   type typetable = {tysize : int,
                     tymap : (Type.hol_type, int)Map.dict,
-                    tylist : shared_type list}
+                    tylist : raw_type list}
   type termtable = {termsize : int,
                     termmap : (Term.term, int)Map.dict,
-                    termlist : shared_term list}
+                    termlist : raw_term list}
 
   val empty_strtable : stringtable
   val empty_idtable : idtable
@@ -36,23 +31,22 @@ sig
   val enc_tytable  : typetable HOLsexp.encoder
   val enc_tmtable  : termtable HOLsexp.encoder
 
-  val dec_strings  : string Vector.vector HOLsexp.decoder
   val dec_ids      : string Vector.vector -> id Vector.vector HOLsexp.decoder
 
-  val make_shared_type : Type.hol_type -> stringtable -> idtable -> typetable ->
+  val make_raw_type : Type.hol_type -> stringtable -> idtable -> typetable ->
                          (int * stringtable * idtable * typetable)
 
-  val make_shared_term : Term.term ->
+  val make_raw_term : Term.term ->
                          (stringtable * idtable * typetable * termtable) ->
                          int * (stringtable * idtable * typetable * termtable)
 
   val build_id_vector   : string Vector.vector -> (int * int) list ->
                           id Vector.vector
-  val build_type_vector : id Vector.vector -> shared_type list ->
+  val build_type_vector : id Vector.vector -> raw_type list ->
                           Type.hol_type Vector.vector
 
   val build_term_vector : id Vector.vector -> Type.hol_type Vector.vector ->
-                          shared_term list -> Term.term Vector.vector
+                          raw_term list -> Term.term Vector.vector
 
   type sharing_data_in
   type sharing_data_out
@@ -73,8 +67,8 @@ sig
   val dec_sdata :
       {before_types: unit -> unit,
        before_terms: Type.hol_type Vector.vector -> unit,
-       tables : TheoryReader_dtype.sharing_tables,
-       exports : TheoryReader_dtype.raw_exports} ->
+       tables : RawTheory_dtype.sharing_tables,
+       exports : RawTheory_dtype.raw_exports} ->
       sharing_data_out
   val export_from_sharing_data : sharing_data_out -> extract_data
   val read_term : sharing_data_out -> string -> Term.term

src/postkernel/SharingTables.sml

@@ -1,7 +1,7 @@
 structure SharingTables :> SharingTables =
 struct
 
-open Term Type DB_dtype
+open Term Type DB_dtype RawTheoryReader
 infix |>
 fun x |> f = f x
 
@@ -30,10 +30,6 @@ in
 fun enc_strtable (strtable : stringtable) =
     tagged_encode "string-table" (list_encode String)
                   (List.rev (#list strtable))
-val dec_strings =
-    Option.map Vector.fromList o
-    tagged_decode "string-table" (list_decode string_decode)
-
 fun enc_idtable (idtable : idtable) =
     tagged_encode "id-table" (list_encode (pair_encode(Integer,Integer)))
                   (List.rev (#idlist idtable))
@@ -92,34 +88,23 @@ fun build_id_vector strings intpairs =
     Types
    ---------------------------------------------------------------------- *)
 
-open TheoryReader_dtype
-datatype shared_type = datatype encoded_type
+open RawTheory_dtype
 
 type typetable = {tysize : int,
                   tymap : (hol_type, int)Map.dict,
-                  tylist : shared_type list}
+                  tylist : raw_type list}
 
 local
   open HOLsexp
 in
-fun shared_type_encode (TYV s) = String s
-  | 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)
-      | _ => 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
+    tagged_encode "type-table" (list_encode raw_type_encode) o List.rev o
     #tylist
 
 end (* local *)
 
-fun make_shared_type ty strtable idtable table =
+fun make_raw_type ty strtable idtable table =
     case Map.peek(#tymap table, ty) of
       SOME i => (i, strtable, idtable, table)
     | NONE => let
@@ -138,7 +123,7 @@ fun make_shared_type ty strtable idtable table =
                 make_shared_id {Thy = Thy, Other = Tyop} (strtable, idtable)
             fun foldthis (tyarg, (results, strtable, idtable, table)) = let
               val (result, strtable', idtable', table') =
-                  make_shared_type tyarg strtable idtable table
+                  make_raw_type tyarg strtable idtable table
             in
               (result::results, strtable', idtable', table')
             end
@@ -186,51 +171,31 @@ end
     Terms
    ---------------------------------------------------------------------- *)
 
-datatype shared_term = datatype encoded_term
 type termtable = {termsize : int,
                   termmap : (term, int)Map.dict,
-                  termlist : shared_term list}
+                  termlist : raw_term list}
 
 local
   open HOLsexp
 in
-fun shared_term_encode stm =
-    case stm of
-        TMV (s,i) => List[String s, Integer i]
-      | TMC (i,j) => List[Integer i, Integer j]
-      | TMAp(i,j) => List[Symbol "ap", Integer i, Integer j]
-      | TMAbs(i,j) => List[Symbol "ab", Integer i, Integer j]
-fun shared_term_decode s =
-    let
-      val (els, last) = strip_list s
-    in
-      if last <> NONE then NONE
-      else
-        case els of
-            [String s, Integer i] => SOME (TMV (s,i))
-          | [Integer i, Integer j] => SOME (TMC(i,j))
-          | [Symbol "ap", Integer i, Integer j] => SOME (TMAp(i,j))
-          | [Symbol "ab", Integer i, Integer j] => SOME (TMAbs(i,j))
-          | _ => NONE
-    end
 
 val enc_tmtable : termtable encoder =
-    tagged_encode "term-table" (list_encode shared_term_encode) o
+    tagged_encode "term-table" (list_encode raw_term_encode) o
     List.rev o #termlist
 end (* local *)
 
 val empty_termtable : termtable =
     {termsize = 0, termmap = Map.mkDict Term.compare, termlist = [] }
 
-fun make_shared_term tm (tables as (strtable,idtable,tytable,tmtable)) =
+fun make_raw_term tm (tables as (strtable,idtable,tytable,tmtable)) =
     case Map.peek(#termmap tmtable, tm) of
       SOME i => (i, tables)
     | NONE => let
       in
         if is_var tm then let
             val (s, ty) = dest_var tm
             val (ty_i, strtable, idtable, tytable) =
-                make_shared_type ty strtable idtable tytable
+                make_raw_type ty strtable idtable tytable
             val {termsize, termmap, termlist} = tmtable
           in
             (termsize,
@@ -244,7 +209,7 @@ fun make_shared_term tm (tables as (strtable,idtable,tytable,tmtable)) =
             val (id_i, strtable, idtable) =
                 make_shared_id {Thy = Thy, Other = Name} (strtable, idtable)
             val (ty_i, strtable, idtable, tytable) =
-                make_shared_type Ty strtable idtable tytable
+                make_raw_type Ty strtable idtable tytable
             val {termsize, termmap, termlist} = tmtable
           in
             (termsize,
@@ -255,8 +220,8 @@ fun make_shared_term tm (tables as (strtable,idtable,tytable,tmtable)) =
           end
         else if is_comb tm then let
             val (f, x) = dest_comb tm
-            val (f_i, tables) = make_shared_term f tables
-            val (x_i, tables) = make_shared_term x tables
+            val (f_i, tables) = make_raw_term f tables
+            val (x_i, tables) = make_raw_term x tables
             val (strtable, idtable, tytable, tmtable) = tables
             val {termsize, termmap, termlist} = tmtable
           in
@@ -268,8 +233,8 @@ fun make_shared_term tm (tables as (strtable,idtable,tytable,tmtable)) =
           end
         else  (* must be an abstraction *) let
             val (v, body) = dest_abs tm
-            val (v_i, tables) = make_shared_term v tables
-            val (body_i, tables) = make_shared_term body tables
+            val (v_i, tables) = make_raw_term v tables
+            val (body_i, tables) = make_raw_term body tables
             val (strtable, idtable, tytable, tmtable) = tables
             val {termsize, termmap, termlist} = tmtable
           in
@@ -339,7 +304,7 @@ fun add_types tys (SDI{strtable,idtable,tytable,tmtable,exp}) =
     let
       fun dotypes (ty, (strtable, idtable, tytable)) = let
         val (_, strtable, idtable, tytable) =
-            make_shared_type ty strtable idtable tytable
+            make_raw_type ty strtable idtable tytable
       in
         (strtable, idtable, tytable)
       end
@@ -354,7 +319,7 @@ fun add_terms tms (SDI{strtable,idtable,tytable,tmtable,exp}) =
     let
       val tms = Term.all_atomsl tms empty_tmset |> HOLset.listItems
       val (strtable,idtable,tytable,tmtable) =
-          List.foldl (fn (t,tables) => #2 (make_shared_term t tables))
+          List.foldl (fn (t,tables) => #2 (make_raw_term t tables))
                      (strtable,idtable,tytable,tmtable)
                      tms
     in

src/postkernel/TheoryReader.sig

@@ -2,9 +2,9 @@ signature TheoryReader =
 sig
 
   exception TheoryReader of string
-  type raw_theory = TheoryReader_dtype.raw_theory
-  type sharing_tables = TheoryReader_dtype.sharing_tables
-  type raw_exports = TheoryReader_dtype.raw_exports
+  type raw_theory = RawTheory_dtype.raw_theory
+  type sharing_tables = RawTheory_dtype.sharing_tables
+  type raw_exports = RawTheory_dtype.raw_exports
   type raw_core = {tables : sharing_tables, exports : raw_exports}
   val load_thydata : {thyname:string,path:string} ->
                      (Thm.thm * DB_dtype.thminfo) Symtab.table