Continue to refactor TheoryReader code

Want to next ensure that .dat files can be read by code that does not
use or depend on kernel code.

src/1/DiskThms.sml

@@ -32,12 +32,21 @@ struct
                 handle Interrupt => raise Interrupt
                      | _ => raise Fail "Couldn't parse sexp from file"
       in
-        case dec_sdata {with_strings = fn _ => (), with_stridty = fn _ => ()} t
-         of
+        case TheoryReader.core_decode t of
             NONE => raise Fail "Couldn't decode sexp"
-          | SOME sdi =>
-            map (fn (n,th,i) => (n,th))
-                (#theorems (export_from_sharing_data sdi))
+          | SOME {tables,exports} =>
+            let
+              val sdo = SharingTables.dec_sdata {
+                    tables = tables,
+                    exports = exports,
+                    before_types = fn () => (),
+                    before_terms = fn _ => ()
+                  }
+            in
+              map
+                (fn (n,th,i) => (n,th))
+                (#theorems (export_from_sharing_data sdo))
+            end
       end
 
   fun read_file fname =

src/AI/aiLib.sml

@@ -821,10 +821,18 @@ fun export_goal file (goal as (asl,w)) =
 fun import_terml file =
   let
     val t = HOLsexp.fromFile file
-    val sdo = valOf (dec_sdata {with_strings = fn _ => (),
-                                with_stridty = fn _ => ()} t)
   in
-    #unnamed_terms (export_from_sharing_data sdo)
+    case TheoryReader.core_decode t of
+        NONE => raise Option
+      | SOME {exports,tables} =>
+        let
+          val sdo = dec_sdata {before_types = fn _ => (),
+                               before_terms = fn _ => (),
+                               tables = tables,
+                               exports = exports}
+        in
+          #unnamed_terms (export_from_sharing_data sdo)
+        end
   end
 
 fun import_goal file = let val l = import_terml file in (tl l, hd l) end
@@ -859,9 +867,9 @@ fun enc_tmdata (encf,tmlf) tmdata =
 
 fun dec_tmdata decf t =
   let
-    val a = {with_strings = fn _ => (), with_stridty = fn _ => ()}
-    val (sdo, tmdata) =
-      valOf (pair_decode (dec_sdata a, SOME) t)
+    val ({exports,tables}, tmdata) = valOf (pair_decode (TheoryReader.core_decode, SOME) t)
+    val sdo = dec_sdata {exports = exports, tables = tables,
+                         before_types = fn _ => (), before_terms = fn _ => ()}
     val dec_tm = Option.map (read_term sdo) o string_decode
   in
     decf dec_tm tmdata

src/postkernel/SharingTables.sig

@@ -72,8 +72,10 @@ sig
 
   val dec_sdata :
       {before_types: unit -> unit,
-       before_terms: Type.hol_type Vector.vector -> unit} ->
-      sharing_data_out HOLsexp.decoder
+       before_terms: Type.hol_type Vector.vector -> unit,
+       tables : TheoryReader_dtype.sharing_tables,
+       exports : TheoryReader_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
   val read_string : sharing_data_out -> int -> string

src/postkernel/SharingTables.sml

@@ -498,9 +498,8 @@ type sharing_data_out =
       Term.term Vector.vector * extract_data)
 
 
-type 'a depinfo = {head : 'a * int, deps : ('a * int list) list}
-fun mapdepinfo f ({head = (a,i),deps}:'a depinfo) : 'b depinfo =
-    {head = (f a, i), deps = map (fn (a,l) => (f a, l)) deps}
+fun mapdepinfo f ({me = (a,i),deps}:'a raw_dep) : 'b raw_dep =
+    {me = (f a, i), deps = map (fn (a,l) => (f a, l)) deps}
 
 fun translatepath slist =
     let
@@ -513,129 +512,61 @@ fun translatepath slist =
           [] => OS.Path.toString {arcs = [], isAbs = true, vol = ""}
         | v::arcs => OS.Path.toString {arcs = arcs, isAbs = isAbs, vol = v}
     end
-fun decclass 0 = Axm
-  | decclass 1 = Def
-  | decclass 2 = Thm
-  | decclass i = raise SharingTables ("Bad theorem class: "^Int.toString i)
-
-fun translate_info f ilist =
-    case ilist of
-        [classtag,privtag] =>
-          {loc = Unknown, private = privtag <> 0, class = decclass classtag}
-      | classtag::privatep::exactp::lnum::rest =>
-          {loc = Located{scriptpath = translatepath (map f rest),
-                         linenum = lnum, exact = (exactp <> 0)},
-           private = privatep <> 0, class = decclass classtag}
-      | _ => raise SharingTables "Bad theorem information"
-
-fun read_thm strv tmvector thmrec =
-    let
-      val {name,depinfo:int depinfo,tagnames,encoded_hypscon,encodedloc} = thmrec
-      val getstr = (fn i => Vector.sub(strv,i))
-      val depinfo = mapdepinfo getstr depinfo
-      val thminfo = translate_info getstr encodedloc
-      val dd = (#head depinfo, #deps depinfo)
-      val terms = map (Term.read_raw tmvector) encoded_hypscon
-    in
-      (Vector.sub(strv, name), Thm.disk_thm((dd,tagnames), terms), thminfo)
-    end
 
-val dep_decode = let
-  open HOLsexp
-  fun depmunge dilist =
-      case dilist of
-          [] => NONE
-        | (n,[i]) :: rest => SOME{head = (n,i), deps = rest}
-        | _ => NONE
-in
-  Option.mapPartial depmunge o
-  list_decode (pair_decode(int_decode, list_decode int_decode))
-end
-val deptag_decode = let open HOLsexp in
-                      pair_decode(dep_decode, list_decode string_decode)
-                    end
+fun translate_loc f rloc =
+    case rloc of
+        rlUnknown => Unknown
+      | rlLocated {path,linenum,exact} =>
+        Located {
+          scriptpath=translatepath (map f path), linenum = linenum,
+          exact = exact
+        }
 
-(* really just maps to list of ints that need interpreting once string table
-   is available *)
-fun loc_decode s =
-    let open HOLsexp
-    in
-      case s of
-          Symbol "unknown_loc" => SOME []
-        | _ => list_decode int_decode s
-    end
-
-val thm_decode =
+fun read_thm strv tmvector (thmrec:raw_thm) =
     let
-      open HOLsexp
-      fun thmmunge(i,(di,tags),loc,tms) =
-          {name = i, depinfo = di, tagnames = tags, encoded_hypscon = tms,
-           encodedloc=loc}
+      val {name,deps,tags,class,private,loc,concl,hyps} = thmrec
+      val getstr = (fn i => Vector.sub(strv,i))
+      val depinfo = mapdepinfo getstr deps
+      val loc' = translate_loc getstr loc
+      val dd = (#me depinfo, #deps depinfo)
+      val terms = map (Term.read_raw tmvector) (concl::hyps)
+      val thminfo = {private=private,loc=loc',class=class}
     in
-      Option.map thmmunge o
-      pair4_decode (int_decode, deptag_decode, loc_decode,
-                    list_decode string_decode)
+      (Vector.sub(strv, name), Thm.disk_thm((dd,tags), terms), thminfo)
     end
 
+
 val prsexp = HOLPP.pp_to_string 70 HOLsexp.printer
 fun force s dec t =
     case dec t of
         NONE => raise SharingTables ("Couldn't decode \""^s^"\": "^prsexp t)
       | SOME t => t
 
-fun dec_sdata {before_types,before_terms} t =
+fun dec_sdata {before_types,before_terms,tables,exports} =
     let
-      open HOLsexp
-      val decoder =
-            tagged_decode "core-data" (
-              pair_decode(
-                tagged_decode "tables" (
-                  pair4_decode(
-                    dec_strings,
-                    tagged_decode "id-table"
-                       (list_decode (pair_decode(int_decode, int_decode))),
-                    tagged_decode "type-table" (list_decode shared_type_decode),
-                    tagged_decode "term-table" (list_decode shared_term_decode)
-                  )
-                ),
-                tagged_decode "exports" (
-                  pair3_decode(
-                    pair_decode( (* types *)
-                      list_decode int_decode,
-                      list_decode (pair_decode(string_decode, int_decode))
-                    ),
-                    pair_decode( (* terms *)
-                      list_decode string_decode,
-                      list_decode (pair_decode(string_decode, string_decode))
-                    ),
-                    (* theorems *) list_decode thm_decode
-                  )
-                )
-              )
-            )
+      val {stringt = strv, idt = intplist, typet = shtylist,
+           termt = shtmlist} = tables
+      val {unnamed_types = raw_untys, named_types = raw_nmtys,
+           unnamed_terms = raw_untms, named_terms = raw_nmtms,
+           thms = rawthms} = exports
+      fun sub v i = Vector.sub(v,i)
+      val _ = before_types ()
+      val idv = build_id_vector strv intplist
+      val tyv = build_type_vector idv shtylist
+      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
+      val untms = map (Term.read_raw tmv) raw_untms
+      val nmtms = map (fn {name,encoded_term} =>
+                          (name, Term.read_raw tmv encoded_term))
+                      raw_nmtms
+      val thms = map (read_thm strv tmv) rawthms
     in
-      case decoder t of
-          NONE => NONE
-        | SOME ((strv,intplist,shtylist,shtmlist),
-                ((raw_untys, raw_nmtys), (raw_untms, raw_nmtms), rawthms)) =>
-          let
-            fun sub v i = Vector.sub(v,i)
-            val _ = before_types ()
-            val idv = build_id_vector strv intplist
-            val tyv = build_type_vector idv shtylist
-            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
-            val untms = map (Term.read_raw tmv) raw_untms
-            val nmtms = map (fn (nm,s) => (nm, Term.read_raw tmv s)) raw_nmtms
-            val thms = map (read_thm strv tmv) rawthms
-          in
-            SOME (strv,idv,tyv,tmv,
-                  {named_types = nmtys, unnamed_types = untys,
-                   named_terms = nmtms, unnamed_terms = untms,
-                   theorems = thms})
-          end
+      (strv,idv,tyv,tmv,
+       {named_types = nmtys, unnamed_types = untys,
+        named_terms = nmtms, unnamed_terms = untms,
+        theorems = thms})
     end
 
 fun export_from_sharing_data (_, _, _, _, exp) = exp

src/postkernel/TheoryPP.sml

@@ -311,9 +311,18 @@ fun pp_struct (info_record : struct_info_record) = let
               add_string "structure TDB = struct" >> add_break(1,2) >>
               add_string "val thydata = " >> add_break(1,4) >>
               block INCONSISTENT 0 (
-                add_string "TheoryReader.load_thydata" >> add_break (1,2) >>
-                add_string (mlquote name) >> add_break (1,2) >>
-                add_string ("(holpathdb.subst_pathvars "^datfile^")")
+                add_string "TheoryReader.load_thydata {" >> add_break (1,2) >>
+                block CONSISTENT 0 (
+                  block INCONSISTENT 2 (
+                    add_string "thyname =" >> add_break(1,2) >>
+                    add_string (mlquote name ^ ",")
+                  ) >> add_break (1,0) >>
+                  block INCONSISTENT 2 (
+                    add_string "path =" >> add_break(1,2) >>
+                    add_string ("holpathdb.subst_pathvars "^datfile)
+                  ) >>
+                  add_break(1,~2) >> add_string "}"
+                )
               ) >> add_break(1,2) >>
               add_string ("fun find s = #1 (valOf (Symtab.lookup thydata s))") >>
               add_break(1,0) >> add_string "end"

src/postkernel/TheoryReader.sig

@@ -2,10 +2,16 @@ signature TheoryReader =
 sig
 
   exception TheoryReader of string
-  val load_thydata : string -> string ->
+  type raw_theory = TheoryReader_dtype.raw_theory
+  type sharing_tables = TheoryReader_dtype.sharing_tables
+  type raw_exports = TheoryReader_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
+  val core_decode : raw_core HOLsexp.decoder
+
+  val load_raw_thydata : {thyname:string,path:string} -> raw_theory
 
-  type raw = TheoryReader_dtype.raw
 
 end