Email Gateway (Aug 22 2022 at 11:52): Email Gateway (Aug 22 2022 at 11:52):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
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.
I think so and I am working on it.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 11:53):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Changsets 4b53042d7a40 and 072012fb4a10 solve the issue by generalizing
matters appropriately. Their might still be a problem in the stack of
plugins, but at least it does not bite immediately. I will anyway have
a closer look at that.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 11:55):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 11:57):From: Dmitriy Traytel <traytel@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
Last updated: Nov 21 2024 at 12:39 UTC