[opentheory-users] interpretation in separate file

[Joe Leslie-Hurd]

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
>