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
