Hi Florian,
On 27.08.2015 10:03, Florian Haftmann wrote:
Hi Dmitriy,
In short, I have come to the conclusion that
let (a, b) = p in t
case p of (a, b) => t
at the moment being logically distinct, should be one and the same. In
other words, I suggest that any case expression on tuples should be
printed using »let« rather than »case«. The constant »Let« would turn
into a degenerate case combinator with no actual pattern match.
I tried to change this in the expectation that tuning the syntax rules
for Let would be sufficient, but found out that's not the case: if case
is to be interwoven with let, the syntax machinery for let must act on
the same syntactic layer to behave consistently (the usual observation
when dealing with syntax).
Hence, to go forward here, it is inevitable to extend the case syntax
code itself, roughly as follows:
a) Map »case x of y ⇒ f y« to »Let x f« and vice versa.
b) Map singleton case clauses to let clauses and vice versa.
c) Collapse/expand consecutive let clauses (let x = y in let z = w in …
<--> let x = y; z = w in …)
Since I suppose you know that code best, how feasible does this agenda
look for you? I guess a) has to be implemented in Isabelle/ML anyway,
but maybe then b) and c) are simple enough to be achieved using »syntax«
productions.
I am slightly confused by "and vice versa". Clearly you want the mapping
to go in one direction. There are two questions: (1) what is the logical
representation (2) what is printed.
If I understand you correctly you want the answer for both to be Let
expressions (for case combinators of single-constructor (co)datatypes).
Then I would say, the way to go is to implement a syntax phase for
translating the affected case combinators into Let expressions and
install it *after* the case syntax translation phase. Something along
the following lines (generalized beyond the product type).
ML ‹
fun Let_of_case ctxt ts =
let
fun substT T =
let
val ((U1, (U2, U3)), (U4, U5)) = T |> dest_funT |>> (dest_funT
##> dest_funT) ||> dest_funT;
in
U4 --> (HOLogic.mk_prodT (U1, U2) --> U3) --> U5
end;
fun subst (Const (@{const_name case_prod}, T) $ rhs $ t) =
Const (@{const_name Let}, substT T) $ (subst t) $
(HOLogic.mk_split (subst rhs))
| subst (t $ u) = subst t $ subst u
| subst t = t
in
map subst ts
end;
val _ = Context.>> (Syntax_Phases.term_check 2 "case → Let" Let_of_case)
›
This, however, does not work with (a), since today "case x of y ⇒ f y"
is translated to "f x". But the question is anyway whether this is not
what you want.
In contrast, if you would like to have the case combinators as the
logical representation, the translation of Let into case probably should
happen before the case syntax translation phase (and would be more
complicated). Printing then would work roughly as in the code above
(replace "check 2" with "uncheck 0").
In any case I would prefer not to extend the case syntax translation
itself, since it is quite complicated already.
Hope that helps,
Dmitriy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
