Re: [Hol-info] Share list of terms with later theories

[Jeremy Dawson]

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"  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,   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"  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  
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,   
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" 

Re: [Hol-info] Share list of terms with later theories

[Michael.Norrish]

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"  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,   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"  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  
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,   
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"  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
> >>  

Re: [Hol-info] Share list of terms with later theories

[Magnus Myreen]

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,   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"  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  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,   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"  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 

Re: [Hol-info] Share list of terms with later theories

[Michael.Norrish]

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"  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  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,   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"  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 

Re: [Hol-info] Share list of terms with later theories

[Konrad Slind]

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  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,   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"  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"  wrote:
>> >
>> > Hello everyone,
>> >
>> > suppose I have a custom tactic that depends on 

Re: [Hol-info] Share list of terms with later theories

[Magnus Myreen]

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,   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"  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"  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
> >
>  

Re: [Hol-info] Share list of terms with later theories

[Michael.Norrish]

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"  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"  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 

[Hol-info] Share list of terms with later theories

[Magnus Myreen]

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"  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

Re: [Hol-info] Share list of terms with later theories

[Michael.Norrish]

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"  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

[Hol-info] Share list of terms with later theories

[Heiko Becker]

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