[Why3-club] record simplifications

Guillaume Melquiond guillaume.melquiond at inria.fr
Fri Nov 16 18:19:01 CET 2012


Le vendredi 16 novembre 2012 à 17:50 +0100, Johannes Kanig a écrit :
> Hello Why3 team,
> 
> I have the following little module/theory:
> 
>   module Test
>     use import int.Int
> 
>     type r = { a : int ; b : int }
> 
>     function f "inline" (x : r) : int = x.a + 1
> 
>     goal g:
>       f { a = 2; b = 3} = 3 /\ ({ a = 2; b = 3}).a = 2
> 
> end
> 
> and the following questions:
> 
> 1) I would like to eliminate the trivial build/select of the record on
> the right hand side of the "/\". Which built-in transformation, if any,
> allows me to do that? I thought that "eliminate_algebraic" does
> something like that (besides eliminating algebraic types), but I had no
> luck. Or do I need to roll my own transformation?
> 
> 2) Same question for the left hand side of the "/\", but here we need to
> inline "f" first. Suppose I have a transformation that inlines "f" (e.g.
> by inlining all functions that are marked with the "inline" tag). I
> suppose I can then chain that with the hypothetical transformation of (1)?

If I am not mistaken, that is precisely what src/transform/eval_match.ml
does. Except that it is only called by the WP, which would explain why
it fails for you. (But I am no expert.)

Best regards,

Guillaume




More information about the Why3-club mailing list