[opentheory-users] interpretation in separate file

[Joe Leslie-Hurd]

Hi Ramana,

Following your suggestion I've written documentation for the
interpretation files:

http://www.gilith.com/research/opentheory/interpretation.html

I've also converted all of my theories on the Gilith repo to use
interpretation files rather than interpret: lines, because it's easier
to read and keep in sync with my HOL Light source theories.

Cheers,

Joe

On Mon, Apr 25, 2016 at 11:54 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> Yes, the documentation could definitely be improved by describing
> interpretation files. Your reverse engineering is quite correct, plus
> comments are also allowed. For an example take a look at the
> interpretation file used by the latest version of the byte-def theory:
>
> http://opentheory.gilith.com/opentheory/packages/byte-def-1.98/word.int
>
> Cheers,
>
> Joe
>
>
>
> On Mon, Apr 25, 2016 at 11:30 PM, Ramana Kumar <ramana at member.fsf.org> wrote:
>> Hi Joe,
>>
>> Thanks for implementing this!
>>
>> I think the documentation isn't very clear about what interpretation files
>> should contain. However, I think I figured it out to some extent: They
>> should have lines like the "interpret:" lines except without the leading
>> "interpret:", and blank lines are allowed.
>>
>> I'm trying it out more now, and will let you know if I run into anything.
>>
>> Cheers,
>> Ramana
>>
>> On 24 April 2016 at 16:58, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>>
>>> Hi Ramana,
>>>
>>> The latest version of the opentheory tool (release 20160423) now
>>> includes support for
>>>
>>> interpretation: "file.int"
>>>
>>> lines in theory files, as documented here:
>>>
>>> http://www.gilith.com/research/opentheory/theory.html
>>>
>>> It's lightly tested, so please let me know if you discover anything
>>> odd with the new feature.
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> On Wed, Apr 20, 2016 at 9:37 PM, Ramana Kumar <ramana at member.fsf.org>
>>> wrote:
>>> > Cool. Thanks!
>>> >
>>> > On 21 April 2016 at 02:40, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>> >>
>>> >> By the way, I am working on adding this feature, but for various
>>> >> technical reasons of how the code is structured it's turning out to be
>>> >> non-trivial. I'll let you know when the feature is added.
>>> >>
>>> >> Cheers,
>>> >>
>>> >> Joe
>>> >>
>>> >> On Sun, Apr 3, 2016 at 10:16 PM, Joe Leslie-Hurd <joe at gilith.com>
>>> >> wrote:
>>> >> > Sure thing, I'll work on adding this feature.
>>> >> >
>>> >> > Cheers,
>>> >> >
>>> >> > Joe
>>> >> >
>>> >> > On Fri, Apr 1, 2016 at 3:41 PM, Ramana Kumar <ramana at member.fsf.org>
>>> >> > wrote:
>>> >> >> Hi Joe,
>>> >> >>
>>> >> >> I would like to reopen this request. It seems like I'm going to be
>>> >> >> copying
>>> >> >> interpretations around a lot again.
>>> >> >>
>>> >> >> Cheers,
>>> >> >> Ramana
>>> >> >>
>>> >> >> On 4 March 2016 at 12:14, Ramana Kumar <ramana at member.fsf.org>
>>> >> >> wrote:
>>> >> >>>
>>> >> >>> Hi Joe,
>>> >> >>>
>>> >> >>> It turns out this is not so urgent for me since Michael and I came
>>> >> >>> up
>>> >> >>> with
>>> >> >>> another method:
>>> >> >>> Put all the article-combination stuff into one file
>>> >> >>> uninterpreted.thy
>>> >> >>> (main block is a union), then turn that into uninterpreted.art, and
>>> >> >>> finally
>>> >> >>> do the interpretation all at once (so it only appears in one file)
>>> >> >>> in
>>> >> >>> interpreted.thy, whose main block is an article block for
>>> >> >>> "uninterpreted.art".
>>> >> >>>
>>> >> >>> However, interpretations from files would probably still be good
>>> >> >>> for
>>> >> >>> other
>>> >> >>> scenarios. I would tweak your suggested syntax to use
>>> >> >>> "interpretation"
>>> >> >>> rather than "interpret-file", to match "article" (which also takes
>>> >> >>> a
>>> >> >>> filename).
>>> >> >>>
>>> >> >>> Cheers,
>>> >> >>> Ramana
>>> >> >>>
>>> >> >>> On 5 March 2016 at 05:51, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>> >> >>>>
>>> >> >>>> Hi Ramana,
>>> >> >>>>
>>> >> >>>> I agree with you that it would be good for theory files to support
>>> >> >>>> pulling in interpretations from files. How about the following
>>> >> >>>> syntax:
>>> >> >>>>
>>> >> >>>> interpret-file: "file.int"
>>> >> >>>>
>>> >> >>>> inside a theory block? It probably makes sense to allow multiple
>>> >> >>>> of
>>> >> >>>> these, just like multiple
>>> >> >>>>
>>> >> >>>> interpret: type/const "X" as "Y"
>>> >> >>>>
>>> >> >>>> lines are allowed, but raise an error if the same symbol is
>>> >> >>>> interpreted in multiple ways.
>>> >> >>>>
>>> >> >>>> Cheers,
>>> >> >>>>
>>> >> >>>> Joe
>>> >> >>>>
>>> >> >>>> On Thu, Mar 3, 2016 at 4:21 PM, Ramana Kumar
>>> >> >>>> <ramana at member.fsf.org>
>>> >> >>>> wrote:
>>> >> >>>> > Is it possible to include an interpretation in a theory file,
>>> >> >>>> > rather
>>> >> >>>> > than
>>> >> >>>> > having to write it out inline? Since I sometimes want to include
>>> >> >>>> > a
>>> >> >>>> > rather
>>> >> >>>> > large interpretation within multiple blocks within the same
>>> >> >>>> > theory
>>> >> >>>> > file, I
>>> >> >>>> > end up having to write a template file and then generate the
>>> >> >>>> > real
>>> >> >>>> > .thy
>>> >> >>>> > file
>>> >> >>>> > from that, to avoid lots of copy-pasting. Is mine the
>>> >> >>>> > recommended
>>> >> >>>> > approach,
>>> >> >>>> > or is there a better way?
>>> >> >>>> >
>>> >> >>>> > _______________________________________________
>>> >> >>>> > opentheory-users mailing list
>>> >> >>>> > opentheory-users at gilith.com
>>> >> >>>> > http://www.gilith.com/opentheory/mailing-list
>>> >> >>>> >
>>> >> >>>>
>>> >> >>>> _______________________________________________
>>> >> >>>> opentheory-users mailing list
>>> >> >>>> opentheory-users at gilith.com
>>> >> >>>> http://www.gilith.com/opentheory/mailing-list
>>> >> >>>
>>> >> >>>
>>> >> >>
>>> >> >>
>>> >> >> _______________________________________________
>>> >> >> opentheory-users mailing list
>>> >> >> opentheory-users at gilith.com
>>> >> >> http://www.gilith.com/opentheory/mailing-list
>>> >> >>
>>> >>
>>> >> _______________________________________________
>>> >> opentheory-users mailing list
>>> >> opentheory-users at gilith.com
>>> >> http://www.gilith.com/opentheory/mailing-list
>>> >
>>> >
>>> >
>>> > _______________________________________________
>>> > opentheory-users mailing list
>>> > opentheory-users at gilith.com
>>> > http://www.gilith.com/opentheory/mailing-list
>>> >
>>>
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>
>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>