[isabelle] Problems with the Code-Generator



Dear all,

I currently have the problem that the code-generator produces ambiguous function calls.

Consider the following theory:

theory Problem imports Rational Code_Char_chr
begin

fun f :: "rat ⇒ nat ⇒ bool"
where "f x z = ((x * x = x) ∧ (if z = 3 then z = z div z else z = 7))"

export_code f in Haskell file -



Then one obtains code which cannot be compiled due to the following reason:

module Nat where {

...

data Nat = Zero_nat | Suc Nat.Nat;

divmod :: Nat.Nat -> Nat.Nat -> (Nat.Nat, Nat.Nat);
divmod m n = ...

}

module Integer where {

import Nat;

...

divmod :: Integer -> Integer -> (Integer, Integer);
divmod k l = ...

mod_int :: Integer -> Integer -> Integer;
mod_int a b = snd (divmod a b);

div_int :: Integer -> Integer -> Integer;
div_int a b = fst (divmod a b);

}

Here, in the functions mod_int and div_int the call to divmod is ambiguous, it can refer to divmod within the Integer module or to divmod within the Nat module.

Is there any way how to avoid this situation?

Best regards,
Rene




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.