[Why3-club] Problem with module translation to Coq
Jean-Christophe.Filliatre at lri.fr
Tue Mar 4 16:44:12 CET 2014
This is indeed a bug; thanks for reporting it.
It can be simplified even further, for instance into the following:
function orb int int : int
function op bool bool : bool
axiom ax: op True True = False
use import bool.Bool
clone B with function op = orb
goal g: false
The problem comes from Coq's driver, that prints "orb" for Why3's symbol
bool.Bool.orb in any circumstance, but it is now shadowed by your own
A simple workaround is to add names such as "orb" appearing in Coq's
driver to the black list at begginning of file src/printer/coq.ml. Then
your "orb" is renamed into "orb1".
On 04/03/2014 14:45, Julien Thierry wrote:
> When cloning a module and instantiating it's functions with two
> functions having the same name but from different modules, in the code
> generated by the Coq driver the names of the Why3 modules are lost and
> only one of the definitions is kept.
> I'm joining a file where this problem causes a typing error in the
> axiom Array_Generic_Op_Axiom.op_def due to the different signatures
> of Array.orb and Array_Generic_Op_Axiom.orb. In the end, only Array.orb
> is defined in the Coq code.
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
More information about the Why3-club