From 41e0bdc6b31b9bc98a3b6562caa6f69a27140ffa Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Thu, 23 Jan 2025 10:49:33 +1100 Subject: [PATCH] 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 | 71 +++++---- src/postkernel/SharingTables.sig | 26 ++-- src/postkernel/SharingTables.sml | 69 +++------ src/postkernel/TheoryReader.sig | 6 +- src/postkernel/TheoryReader.sml | 207 +------------------------- src/postkernel/TheoryReader_dtype.sml | 63 -------- tools/sequences/kernel | 1 + 7 files changed, 73 insertions(+), 370 deletions(-) delete mode 100644 src/postkernel/TheoryReader_dtype.sml diff --git a/src/postkernel/DB_dtype.sml b/src/postkernel/DB_dtype.sml index 0d9004a65e..e756834112 100644 --- a/src/postkernel/DB_dtype.sml +++ b/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 diff --git a/src/postkernel/SharingTables.sig b/src/postkernel/SharingTables.sig index 8f4e987ec5..59cca76845 100644 --- a/src/postkernel/SharingTables.sig +++ b/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 diff --git a/src/postkernel/SharingTables.sml b/src/postkernel/SharingTables.sml index 1a61b7ff20..8218a0cddd 100644 --- a/src/postkernel/SharingTables.sml +++ b/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,43 +171,23 @@ 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 @@ -230,7 +195,7 @@ fun make_shared_term tm (tables as (strtable,idtable,tytable,tmtable)) = 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 diff --git a/src/postkernel/TheoryReader.sig b/src/postkernel/TheoryReader.sig index 54e94b7ffa..5e97d60014 100644 --- a/src/postkernel/TheoryReader.sig +++ b/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 diff --git a/src/postkernel/TheoryReader.sml b/src/postkernel/TheoryReader.sml index bf4d670e3b..5d0768dfad 100644 --- a/src/postkernel/TheoryReader.sml +++ b/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 TheoryReader_dtype +open HolKernel SharingTables RawTheory_dtype RawTheoryReader fun temp_encoded_update sdata thyname {data,ty} = Theory.LoadableThyData.temp_encoded_update { @@ -23,211 +23,6 @@ fun temp_encoded_update sdata thyname {data,ty} = data = data } -exception TheoryReader of string -val prsexp = HOLPP.pp_to_string 70 HOLsexp.printer - - -fun dtag s t = - case HOLsexp.dest_tagged s t of - NONE => raise TheoryReader ("Expecting tag "^s) - | SOME t => t - -fun dtaglist tags t = - let open HOLsexp - in - case strip_list t of - (_, SOME last) => raise TheoryReader - ("Extraneous at end of list: " ^prsexp t) - | (els, NONE) => - let - fun recurse tags els A = - case (tags,els) of - ([],[]) => List.rev A - | ([], e::_) => raise TheoryReader ("Extra list element: "^ - prsexp e) - | (t::_, []) => raise TheoryReader ("No data for tag " ^ t) - | (t::ts, e::es) => - let val e = dtag t e - in - recurse ts es (e::A) - end - in - recurse tags els [] - end - end - -fun force s dec t = - case dec t of - NONE => raise TheoryReader ("Couldn't decode \""^s^"\": "^prsexp t) - | SOME t => t - -fun string_to_class "A" = SOME DB.Axm - | string_to_class "T" = SOME DB.Thm - | string_to_class "D" = SOME DB.Def - | string_to_class _ = NONE - -val dec_thyname : raw_name HOLsexp.decoder = - let open HOLsexp - in - HOLsexp.map_decode - (fn (s,n1,n2) => {thy = s, tstamp1 = n1, tstamp2 = n2}) $ - pair3_decode (string_decode, - Option.map Arbnum.fromString o string_decode, - Option.map Arbnum.fromString o string_decode) - end - - -(* ---------------------------------------------------------------------- - decoding raw theorems - ---------------------------------------------------------------------- *) - -fun decclass 0 = DB_dtype.Axm - | decclass 1 = DB_dtype.Def - | decclass 2 = DB_dtype.Thm - | decclass i = raise SharingTables ("Bad theorem class: "^Int.toString i) - -val dep_decode : int raw_dep HOLsexp.decoder = let - open HOLsexp - fun depmunge dilist = - case dilist of - [] => NONE - | (n,[i]) :: rest => SOME{me = (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 loc_decode ilist = - case ilist of - [] => SOME rlUnknown - | exactp :: lnum :: path => - SOME (rlLocated {path = path, linenum = lnum, exact = exactp <> 0}) - | _ => NONE - -val info_decode = let - open HOLsexp - fun bind ilist = - case ilist of - ctag :: privtag :: rest => - Option.map (fn rl => - {class = decclass ctag, - private = privtag <> 0, - loc = rl}) - (loc_decode rest) - | _ => NONE -in - bind_decode (list_decode int_decode) bind -end - -val thm_decode : raw_thm HOLsexp.decoder = - let - open HOLsexp - fun thmmunge(i,(di,tags),{class,private,loc},tms) = - case tms of - [] => NONE - | c::hyps => - SOME { - name = i, deps = di, tags = tags, concl = c, - hyps = hyps,class=class,private=private,loc=loc - } - in - Option.mapPartial thmmunge o - pair4_decode (int_decode, deptag_decode, info_decode, - list_decode string_decode) - end - - -val core_decode = - let open HOLsexp - in - map_decode - (fn ((strt,idt,tyt,tmt), ((utys,ntys), (utms,ntms), thms)) => - {tables = {stringt = strt, idt = idt, typet = tyt, termt = tmt}, - exports = { - unnamed_types = utys, - named_types = ntys, - unnamed_terms = utms, - named_terms = - map (fn (n,t) => {name = n, encoded_term = t}) ntms, - thms = thms - } - }) - (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 - ) - ) - ) - ) - ) - end - -fun load_raw_thydata {thyname, path} : raw_theory = - let - open HOLsexp - val raw_data = fromFile path - val raw_data = dtag "theory" raw_data - val (thyparentage, rest) = - case raw_data of - Cons(t1,t2) => (t1,t2) - | _ => raise TheoryReader "No thy-parentage prefix" - val (thy_data, parents_data) = - case thyparentage of - Cons p => p - | _ => raise TheoryReader "thyparentage not a pair" - val fullthy as {thy,...} = force "thyname" dec_thyname thy_data - val parents = force "parents" (list_decode dec_thyname) parents_data - val ({tables,exports}, incorporate_data, thydata_data) = - force "toplevel_decode" ( - pair3_decode ( - core_decode, - tagged_decode "incorporate" SOME, - tagged_decode "loadable-thydata" SOME - ) - ) rest - val (new_types, new_consts) = - force "incorporate_decode" ( - pair_decode( - tagged_decode "incorporate-types" ( - list_decode (pair_decode (string_decode, int_decode)) - ), - tagged_decode "incorporate-consts" ( - list_decode (pair_decode (string_decode, int_decode)) - ) - ) - ) incorporate_data - in - { name = fullthy, parents = parents, - tables = tables, - exports = exports, - newsig = {types = new_types, consts = new_consts}, - thydata = thydata_data - } - end fun load_thydata (r as {thyname,path}) = let diff --git a/src/postkernel/TheoryReader_dtype.sml b/src/postkernel/TheoryReader_dtype.sml deleted file mode 100644 index 6c7348f8df..0000000000 --- a/src/postkernel/TheoryReader_dtype.sml +++ /dev/null @@ -1,63 +0,0 @@ -structure TheoryReader_dtype = -struct - - -type raw_name = {thy : string, tstamp1 : Arbnum.num, tstamp2 : Arbnum.num} -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 Vector.vector, - idt : (int * int) list, - typet : encoded_type list, - termt : encoded_term list} - -type 'thy raw_dep = { - me : 'thy * int, (* thy, thm-number *) - deps : ('thy * int list) list (* per theory thm numbers *) -} - -datatype raw_loc = - rlUnknown | rlLocated of {path:int list, linenum : int, exact:bool} - -type raw_thm = { - name : int, (* reference to string table *) - deps : int raw_dep, - tags : string list, - class : DB_dtype.class (* Thm | Axm | Def *), - private : bool, - loc : raw_loc, - concl : string, - hyps : string list -} - -type raw_exports = { - (* for types, ints are references into accompanying type-vector *) - unnamed_types : int list, - named_types : (string * int) list, - (* for terms, strings are encoded with write_raw *) - unnamed_terms : string list, - named_terms : {name:string, encoded_term: string} list, - thms : raw_thm list -} - -type raw_core = {tables : sharing_tables, exports : raw_exports} - -type raw_theory = { - name : raw_name, - parents : raw_name list, - tables : sharing_tables, - newsig : { - types : (string * int) list, (* names and arities *) - consts : (string * int) list (* names and (encoded) types *) - }, - exports : raw_exports, - thydata : HOLsexp.t -} - - -end (* struct *) diff --git a/tools/sequences/kernel b/tools/sequences/kernel index f1db7ad4b8..c014a1bfd3 100644 --- a/tools/sequences/kernel +++ b/tools/sequences/kernel @@ -12,6 +12,7 @@ tools/mlyacc/mlyacclib [poly]src/portableML/poly src/portableML src/portableML/monads +src/portableML/rawtheory [poly]src/portableML/json [poly]src/portableML/poly/concurrent [mosml]src/portableML/mosml/concurrent