Michael: I like the private_db idea.
Jeremy: I believe many of the theorems and definitions created by the
ind_type machinery are simply _deleted_ before the theory is exported, so
they cannot be recovered afterwards. As long as deleted constants are not
mentioned in exported theorems (but only in their proofs, which aren't
stored anyway) the system remains sound, so HOL allows such deletion and
omission.
On 17 January 2018 at 00:07, Jeremy Dawson <jeremy.daw...@anu.edu.au> wrote:
> A related question: some time back I was looking at how datatypes are
> constructed, and found stuff in theory ind_type, and theorems like
> list_TY_DEF (which one finds by doing find "ty_def")
>
> But it seems that there are also theorems created which define the
> constructors of the list datatype in terms of ind_type$CONSTR,
> ind_type$BOTTOM, ind_type$FCONS, etc, but that these theorems are very well
> hidden. I intended to investigate more to find how these theorems are
> hidden, and where if possible to find them, but never got back to it.
>
> Can anyone help me on that question? And is it relevant to this current
> discussion?
>
> Cheers,
>
> Jeremy
>
>
>
> On 01/17/2018 10:28 AM, michael.norr...@data61.csiro.au wrote:
>
>> If people wanting to store these “uninteresting” theorems are happy to
>> wrap and unwrap the OMITs, this would be one approach.
>>
>> I had been thinking of adding a
>>
>> save_private_thm(name, privatedbname, thm)
>>
>> entrypoint to Theory.sml. You’d want multiple possible “private dbs”, so
>> there would be an entry-point along the lines of
>>
>> get_private_db : string -> (string,thm) Binarymap.dict
>>
>> Every time a theory was loaded, this private_db would change, so in many
>> applications it might not be appropriate to store the result of
>>
>> get_private_db “cakeml/translator”
>>
>> but to instead write
>>
>> val th = Binarymap.peek(get_private_db “cakeml/translator”,
>> “theorem-name”)
>>
>> Michael
>>
>> On 16/1/18, 18:35, "Magnus Myreen" <myr...@chalmers.se> wrote:
>>
>> 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.Norrish@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
>>
>>
> ------------------------------------------------------------
> ------------------
> 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
