From 77c1bc81966bc7cb1da01b07b06772fd031f2c25 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Thu, 23 Jan 2025 11:02:08 +1100 Subject: [PATCH] Include files that should have appeared in previous commit --- src/portableML/rawtheory/Holmakefile | 1 + src/portableML/rawtheory/RawTheoryReader.sig | 28 +++ src/portableML/rawtheory/RawTheoryReader.sml | 245 +++++++++++++++++++ src/portableML/rawtheory/RawTheory_dtype.sml | 67 +++++ 4 files changed, 341 insertions(+) create mode 100644 src/portableML/rawtheory/Holmakefile create mode 100644 src/portableML/rawtheory/RawTheoryReader.sig create mode 100644 src/portableML/rawtheory/RawTheoryReader.sml create mode 100644 src/portableML/rawtheory/RawTheory_dtype.sml diff --git a/src/portableML/rawtheory/Holmakefile b/src/portableML/rawtheory/Holmakefile new file mode 100644 index 0000000000..0392dadd51 --- /dev/null +++ b/src/portableML/rawtheory/Holmakefile @@ -0,0 +1 @@ +CLINE_OPTIONS = --no_overlay diff --git a/src/portableML/rawtheory/RawTheoryReader.sig b/src/portableML/rawtheory/RawTheoryReader.sig new file mode 100644 index 0000000000..e3ea207ad7 --- /dev/null +++ b/src/portableML/rawtheory/RawTheoryReader.sig @@ -0,0 +1,28 @@ +signature RawTheoryReader = +sig + + exception TheoryReader of string + type 'a decoder = 'a HOLsexp.decoder + type 'a encoder = 'a HOLsexp.encoder + 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} + datatype raw_type = datatype RawTheory_dtype.raw_type + datatype raw_term = datatype RawTheory_dtype.raw_term + type raw_thm = RawTheory_dtype.raw_thm + + val decode : raw_theory decoder + + (* auxiliaries that are possibly of independent interest *) + val force : string -> 'a decoder -> HOLsexp.t -> 'a (* EXN: TheoryReader *) + val raw_type_decode : raw_type decoder + val raw_type_encode : raw_type encoder + val raw_term_decode : raw_term decoder + val raw_term_encode : raw_term encoder + + val thm_decode : raw_thm decoder + val core_decode : raw_core decoder + val load_raw_thydata : {thyname:string,path:string} -> raw_theory + +end diff --git a/src/portableML/rawtheory/RawTheoryReader.sml b/src/portableML/rawtheory/RawTheoryReader.sml new file mode 100644 index 0000000000..49ca314581 --- /dev/null +++ b/src/portableML/rawtheory/RawTheoryReader.sml @@ -0,0 +1,245 @@ +structure RawTheoryReader :> RawTheoryReader = +struct + +open RawTheory_dtype + +open HOLsexp +infixr 1 $ +fun f $ x = f x +exception TheoryReader of string +val prsexp = HOLPP.pp_to_string 70 HOLsexp.printer + +fun dtag s t = + case dest_tagged s t of + NONE => raise TheoryReader ("Expecting tag "^s) + | SOME t => t + +fun dtaglist tags t = + 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 + +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 Axm + | string_to_class "T" = SOME Thm + | string_to_class "D" = SOME Def + | string_to_class _ = NONE + +val dec_thyname : raw_name decoder = + 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) + +(* ---------------------------------------------------------------------- + raw types and terms + ---------------------------------------------------------------------- *) + +fun raw_type_encode (TYV s) = String s + | raw_type_encode (TYOP {opn,args}) = List(map Integer (opn::args)) + +fun raw_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}) + + +fun raw_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 raw_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 + + + +(* ---------------------------------------------------------------------- + decoding raw theorems + ---------------------------------------------------------------------- *) + +fun decclass 0 = DB_dtype.Axm + | decclass 1 = DB_dtype.Def + | decclass 2 = DB_dtype.Thm + | decclass i = raise TheoryReader ("Bad theorem class: "^Int.toString i) + +val dep_decode : int raw_dep decoder = let + 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 = pair_decode(dep_decode, list_decode string_decode) + +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 + 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 decoder = + let + 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 dec_strings = + map_decode Vector.fromList $ + tagged_decode "string-table" (list_decode string_decode) + +val core_decode = + 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 = map (munge_thm_strings strt) 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 raw_type_decode), + tagged_decode "term-table" (list_decode raw_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 + ) + ) + ) + ) + ) + +fun decode s = + let + val raw_data = dtag "theory" s + 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 + SOME { + name = fullthy, parents = parents, + tables = tables, + exports = exports, + newsig = {types = new_types, consts = new_consts}, + thydata = thydata_data + } + end + +fun load_raw_thydata {thyname, path} : raw_theory = + case decode (fromFile path) of + NONE => raise TheoryReader ("Invalid file at "^path) + | SOME v => v + + +end diff --git a/src/portableML/rawtheory/RawTheory_dtype.sml b/src/portableML/rawtheory/RawTheory_dtype.sml new file mode 100644 index 0000000000..357afa15e9 --- /dev/null +++ b/src/portableML/rawtheory/RawTheory_dtype.sml @@ -0,0 +1,67 @@ +structure RawTheory_dtype = +struct + +datatype class = Thm | Axm | Def + + +type raw_name = {thy : string, tstamp1 : Arbnum.num, tstamp2 : Arbnum.num} +datatype raw_type = TYV of string + | TYOP of {opn : int (* ref to idtable *), + args : int list (* refs to earlier types *)} + +(* TMAp and TMAbs constructors unused by SharingTables infrastructure *) +datatype raw_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 : raw_type list, + termt : raw_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 : string, (* reference to string table *) + deps : string raw_dep, + tags : string list, + class : class (* Thm | Axm | Def *), + private : bool, + loc : raw_loc, + concl : string, (* encoded term, decode with Term.read_raw *) + hyps : string list (* encoded terms, as above *) +} + +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