[Why3-club] Problem with module translation to Coq

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Tue Mar 4 16:44:12 CET 2014


Dear Julien,

This is indeed a bug; thanks for reporting it.
It can be simplified even further, for instance into the following:

module B
  function orb int int : int
  function op bool bool : bool
  axiom ax: op True True = False
end

module C
  use import bool.Bool
  clone B with function op = orb
  goal g: false
end

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
symbol "orb".

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".

--
Jean-Christophe



On 04/03/2014 14:45, Julien Thierry wrote:
> Hi,
> 
> 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.
> 
> Regards,
> 
> 
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
> 



More information about the Why3-club mailing list