Re: [isabelle] Interpretation problems of locales with datatype declarations



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.