Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems with the Code-Generator

Email Gateway (Aug 18 2022 at 14:21):

From: René Thiemann <rene.thiemann@uibk.ac.at>
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

Email Gateway (Aug 18 2022 at 14:22):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,

this problem will disappear in the upcoming release.

For the moment, it is best to provide an explicit module name:

export_code f in Haskell module_name <insert module name here> file -

Hope this helps,
Florian
signature.asc

Last updated: Apr 19 2024 at 16:20 UTC