Re: [isabelle] Interpretation problems of locales with datatype declarations
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.
> 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
> 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 .
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and