[opentheory-users] interpretation in separate file

[Joe Leslie-Hurd]

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
>