Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] OCaml code generator problem: Big_int

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

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi,
the Ocaml code generator generates the following lines of (invalid)
OCaml-Code. Note that I'm using Efficient_Nat:

module Integer =
struct

let rec suc n = Big_int.add_big_int n 1;;

OCaml complains:

File "generated/Ta.ml", line 31, characters 38-39:
Error: This expression has type int but an expression was expected of type
Big_int.big_int

I do not know much about OCaml, but I suspect there is some missing
type-coercion.

Is there any fix to get correct generated code?

Many thanks in advance and regards,
Peter lammich

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

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

the Ocaml code generator generates the following lines of (invalid)
OCaml-Code. Note that I'm using Efficient_Nat:

this deficiency did not come to surface before the release of Isabelle
2009. A solution is to replace src/HOL/Library/Efficient_Nat.thy by
http://www4.in.tum.de/~haftmann/resources/Efficient_Nat.thy.

Hope this helps
Florian
signature.asc

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

From: Peter Lammich <peter.lammich@uni-muenster.de>
Florian Haftmann wrote:
Thank you very much, this helped!
The generated Ocaml code now compiles.

Regards
Peter

Last updated: Apr 25 2024 at 04:18 UTC