[opentheory-users] interpretation in separate file

[Ramana Kumar]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160421/8212476f/attachment.html>