*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Interpretation problems of locales with datatype declarations*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Tue, 3 Nov 2015 11:39:16 +0100*Cc*: OndÅej KunÄar <kuncar at in.tum.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <563883D2.6060700@inf.ethz.ch>*References*: <563883D2.6060700@inf.ethz.ch>

Hi Andreas, in both cases plugins are to blame. The first example works if you add a (plugins del: code) annotation to foo. The code generator is inherently non-localized, thus Iâm not sure if this can be improved at all. The second example works if you add a (plugins del: lifting) annotation to bar. I believe Ondra can say what goes wrong in the lifting plugin. Dmitriy > On 03 Nov 2015, at 10:52, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote: > > Dear BNF experts, > > I have started to use datatype declarations inside locales, but this seems to cause problems at interpretations. Here is an example: > > locale l = fixes n :: nat begin > datatype 'a foo = Foo 'a > end > interpretation l 0 . > > The interpretation raises > > exception THM 0 raised (line 1216 of "thm.ML"): > Type not of sort term_of > term_of_class.term_of ?x â ?t > > > If the interpretation is inside a proof (rather than at the top-level), interpret works once, but I get a different error upon the second interpretation: > > locale l2 = fixes b :: bool begin > datatype 'b bar = Bar | Foobar 'b > lemma True > proof - > interpret t!: l2 True . > oops > end > > Here, interpret complains that > Monotocity rule for type "Scratch.l2.bar" is already_defined. > > Is this a fundamental problem of the BNF package and locales or just a limitation of the current implementation? Can I disable some plugins to make the examples work? > > Best, > Andreas

**Follow-Ups**:**Re: [isabelle] Interpretation problems of locales with datatype declarations***From:*Florian Haftmann

**References**:**[isabelle] Interpretation problems of locales with datatype declarations***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] datatype fails in unnamed contexts with assumptions
- Next by Date: Re: [isabelle] datatype fails in unnamed contexts with assumptions
- Previous by Thread: [isabelle] Interpretation problems of locales with datatype declarations
- Next by Thread: Re: [isabelle] Interpretation problems of locales with datatype declarations
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list