[opentheory-users] interpretation in separate file

[Joe Leslie-Hurd]

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
>