Hi all, How about defining:
OMIT x = x in markerScript.sml and making it print as ... and adjust HOL so that a theorem with a top-level OMIT does not show up in DB searches. Cheers, Magnus On 12 January 2018 at 00:00, <michael.norr...@data61.csiro.au> wrote: > I was thinking along these lines, yeah. Such theorems could also be stopped > from appearing in the Theory.sig file. > > Michael > > On 12/1/18, 07:31, "Konrad Slind" <konrad.sl...@gmail.com> wrote: > > Theorems that need to persist between sessions are most easily stored by > name > in theories. Maybe some kind of PolyML database magic could also be > used, I don't > know. As far as DB searches, it wouldn't be hard to implement a > refined DB search > mechanism that first discarded all theorems that met some kind of > naming convention > (e.g., those starting with an underscore or something like that) and > then did the usual > search (which can be on name fragment or pattern). > > Konrad. > > > On Wed, Jan 10, 2018 at 7:09 PM, Magnus Myreen <myr...@chalmers.se> wrote: > > Ah, I didn't realise this existed. Thanks for the pointers! > > > > How does storing of theorems work in this setting? One can't construct > > a theorem from a string in a decode function. > > > > I guess the string could refer to a theorem name that's stored in the > > theory, but this is a bit inconvenient because some of the theorems in > > the translator's state are currently not stored in the theory (other > > than in the automatically produced theorem that is an encoding of the > > entire state). I guess an encode function could invent an unused name > > and store the theorem while it's producing the encoding. This can lead > > to some strange things turning up in DB searches (as is the case with > > the current approach). > > > > Cheers, > > Magnus > > > > > > On 11 January 2018 at 11:24, <michael.norr...@data61.csiro.au> wrote: > >> That level of generality is already possible, and has always been a > desideratum for the design. (The grammar update information stored is about > that complicated for example; consider the types that occur in a call to > add_rule.) > >> > >> The painful part is that you have to write functions to encode and > decode the types into and out of strings (because these strings are written > into the theory files). There are functions for doing basic SML types in > src/parse/Coding, and the handling of terms is handled by writing functions > that take functions for doing this as parameters. See the bottom of > src/parse/term_grammar for the encoding and decoding, and > src/parse/GrammarDeltas for the way this is put together for the grammar > example. > >> > >> You can see the fundamental building blocks at the LoadableThyData > structure in src/postkernel/Theory. > >> > >> Certainly, providing a method for going through a generic s-expression > type might be easiest for users to understand, so perhaps I can build that as > well as term lists. > >> > >> Michael > >> > >> On 11/1/18, 11:08, "Magnus Myreen" <myr...@chalmers.se> wrote: > >> > >> Hi Michael, > >> > >> I see that you are considering to add a TermSetData feature. Could > you > >> please add something more general? I'd appreciate a feature that > can > >> store the CakeML translator's state in theories. Currently, the > CakeML > >> translator stores its state in a single theorem so that the other > >> theories can load the state and continue from previous states. > >> > >> As far as I can tell, the ThmSetData machinery (and probably the > >> TermSetData equivalent) won't help with the translator. The reason > is > >> that the translator's state is a collection of lists of list of > tuples > >> of combinations of strings, type, terms and theorems. > >> > >> The current approach encodes all of these structures into a single > >> unreadable theorem. This works but it seems a bit ad hoc and causes > >> huge unreadable theorems to pop up in various DB searches. > >> > >> Suggestion: could we have a way to store a s-expression-like data > into > >> theories? If the s-expressions would allow strings, types, terms, > >> theorems and, of course, pairs/lists of s-expressions, then I think > >> the translator's state could very naturally be stored in theories. > >> > >> Cheers, > >> Magnus > >> > >> > There is generic machinery for adding values of various forms to > theories so > >> > that future theories and ML code can see them. The smoothest > instantiation > >> > is in ThmSetData (in src/1) which allows storage of sets of > theorems in a > >> > “2D matrix” indexed by theory-name and set-name. For example, > the automatic > >> > rewrites behind the “simp” attribute are implemented this way. > >> > > >> > The storage of grammar updates is handled with the same > technology. > >> > > >> > A hacky way to store terms would be to use theorems with > conclusions of the > >> > form > >> > > >> > K T (myterm) > >> > > >> > and to then use ThmSetData. > >> > > >> > A better way, which, now that I’ve been prodded, I may implement > soon, would > >> > be to write a TermSetData. > >> > > >> > I hope this helps. I’m happy to discuss the details of this > relatively > >> > undocumented feature further if you want more help. > >> > > >> > Best wishes, > >> > Michael > >> > > >> > On 11/1/18, 01:51, "Heiko Becker" <hbec...@mpi-sws.org> wrote: > >> > > >> > Hello everyone, > >> > > >> > suppose I have a custom tactic that depends on a list of > terms and I > >> > want to keep adding elements to the list throughout my > development. > >> > I tried to achieve this using a :term list ref on the ML > level. However, > >> > it is the case that if I add some term in theory A and > inspect the list > >> > in theory B, where A is in the theory graph before B, all > elements added > >> > in A are not in the list anymore. > >> > > >> > Can someone give me a hint on why this is the case or tell > me a better > >> > way to "share" a list of terms from a theory with theories > depending on > >> > it? > >> > > >> > Cheers, > >> > > >> > Heiko > >> > > >> > > >> > > ------------------------------------------------------------------------------ > >> > Check out the vibrant tech community on one of the world's > most > >> > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > >> > _______________________________________________ > >> > hol-info mailing list > >> > hol-info@lists.sourceforge.net > >> > https://lists.sourceforge.net/lists/listinfo/hol-info > >> > > >> > > >> > > ------------------------------------------------------------------------------ > >> > Check out the vibrant tech community on one of the world's most > >> > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > >> > _______________________________________________ > >> > hol-info mailing list > >> > hol-info@lists.sourceforge.net > >> > https://lists.sourceforge.net/lists/listinfo/hol-info > >> > > >> > >> > >> > ------------------------------------------------------------------------------ > >> Check out the vibrant tech community on one of the world's most > >> engaging tech sites, Slashdot.org! http://sdm.link/slashdot > >> _______________________________________________ > >> hol-info mailing list > >> hol-info@lists.sourceforge.net > >> https://lists.sourceforge.net/lists/listinfo/hol-info > > > > > ------------------------------------------------------------------------------ > > Check out the vibrant tech community on one of the world's most > > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > > _______________________________________________ > > hol-info mailing list > > hol-info@lists.sourceforge.net > > https://lists.sourceforge.net/lists/listinfo/hol-info > > ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
