Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle 2016-RC2: warnings in generated code ...

Email Gateway (Aug 22 2022 at 12:20):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,

I just noticed, that there are overlapping patterns in the generated code for LCM and GCD, if one loads Code_Target_Int.
It seems that the original code-equations have not been deactivated. So, one gets warnings when compiling the generated
Haskell-code.

Best regards,
René

theory Scratch
imports
"~~/src/HOL/Library/Code_Target_Int"
begin

definition "f (x :: int) = gcd 5 (lcm x 7)"

export_code f in Haskell

(*
gcd_int :: Arith.Int -> Arith.Int -> Arith.Int;
gcd_int (Arith.Int_of_integer x) (Arith.Int_of_integer y) = Arith.Int_of_integer (Prelude.gcd x y);
gcd_int k l = Arith.abs_int
(if Arith.equal_int l Arith.zero_int then k
else gcd_int l (Arith.mod_int (Arith.abs_int k) (Arith.abs_int l)));

lcm_int :: Arith.Int -> Arith.Int -> Arith.Int;
lcm_int (Arith.Int_of_integer x) (Arith.Int_of_integer y) =
Arith.Int_of_integer (lcm_integer x y);
lcm_int a b =
Arith.divide_int (Arith.times_int (Arith.abs_int a) (Arith.abs_int b))
(gcd_int a b);

*)

Last updated: Apr 26 2024 at 08:19 UTC