Hi Dmitriy, thanks for your answer.
Let me rephrase the matter as I perceive it:
Syntactic requirement: Print and parse singleton case clauses as let
bindings.
I agree that this can (and should) be done in a separate phase. Still
not sure whether check/uncheck is the right layer to accomplish this,
but this can still be elaborated.
But I see also that your suggestion would not need any special treatment
for simple let bindings (let x = y in t).
>> 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.
Well, in my original approach this would have been a necessity.
I'll try the check/uncheck approach.
Thanks a lot,
Florian
>> 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
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
