[Why3-club] record simplifications

Johannes Kanig kanig at adacore.com
Fri Nov 16 17:50:24 CET 2012

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


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)?

Thanks in advance,


Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list