Email Gateway (Aug 22 2022 at 14:58): Email Gateway (Aug 22 2022 at 14:58):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I have an ML function of type "term -> term" (that is, a function
transforming a Pure term). That function (call it "embed") assumes that
the input term is fully checked. In particular, there must not be any
remaining meta-syntactic stuff (like "_constrain"). The input may have
any type, though.
I now want to define a parse translation that applies that function.
syntax "_embed" :: "'a ⇒ term" ("⟨_⟩")
I've tried various incantations but the problem is that
a) either stuff like "_constrain" remains or
b) when I strip constraints, in "⟨map f xs⟩", "map" is considered a free
variable (but it's a constant)
How would I implement such a parse translation?
(NB: this is to improve the readability of several things in my
formalization – I can always apply the "embed" function "by hand" but
that makes it notationally cumbersome)
Cheers
Lars
Email Gateway (Aug 22 2022 at 14:58):From: Peter Lammich <lammich@in.tum.de>
Hi lars,
There is a stack of processing that is done to the term after parsing, the
check phase. It uses simple numeric values to order the different steps in the
check phase. Looks like you want your translation bwen executed last, matching
on some special constant for embed, which is set up such that thebother check
phase s can handle it, eg a plain const embed :: prop => prop
Peter
Email Gateway (Aug 22 2022 at 14:59):From: Lars Hupel <hupel@in.tum.de>
Hi Peter,
yes, that works. From what I can tell, this approach has two downsides:
1) I need to manually traverse the term to find the constant
2) there's no error if I somehow screw up; the useless constant will
just remain in the parsed term
On the other hand, markup works out of the box.
Cheers
Lars
Last updated: Apr 25 2024 at 16:19 UTC