[Why3-club] why3 execute: Cannot execute expression match

David MENTRE dmentre at linux-france.org
Fri Aug 19 18:27:12 CEST 2016


Hello Guillaume,

Le 19/08/2016 à 18:02, Guillaume Melquiond a écrit :
> You just moved the matching issue from f to bool_t_of_bool. You should
> have written the latter function as
> 
>  function bool_t_of_bool (b : bool) : bool_t
>  = if b then DTrue else DFalse

Oops, I was fooled by the error message (pointing on "match ((b1,
b2))"). Now it works!

For the record, here is the workaround:
"""
module Execute_test

 type bool_t = DTrue | DFalse (* work-around for execute bug in Why3
0.87.0 *)

 function bool_t_of_bool (b : bool) : bool_t
 = if b then DTrue else DFalse

 let f (cmd_previous cmd_current : bool) : bool
 = let b1, b2 = (bool_t_of_bool cmd_previous, bool_t_of_bool cmd_current) in
   match b1, b2 with
   | DFalse, DTrue -> True
   | _, _ -> False
   end

 let test ()
 = f False True

end
"""

Thanks!
david



More information about the Why3-club mailing list