Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] OCaml code generation producing invalid code

view this post on Zulip Email Gateway (Aug 22 2022 at 15:48):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,

It seems that the OCaml serialisation for the code generator in
Isabelle2016-1 sometimes spits out invalid OCaml. The following small
theory

theory Test imports Main begin

definition foo :: "bool" where
"foo ≡ ∀c::char. c = CHR 0x1"

export_code foo in OCaml
file "test.ml"

end

will produce OCaml code in "test.ml" that is rejected by the OCaml
compiler (I am using 4.02.3, but the problem seems independent of any
particular version of OCaml). In particular, it seems that on line
1041 of the generated file the code generator is forgetting that
there's a signature imposed on the Finite_Set module, and at line 1041
the implementation type of the Finite_Set.finite type is therefore
abstract:

File "test.ml", line 1041, characters 19-21:
Error: This expression has type unit but an expression was expected of type
char Finite_Set.finite

Thanks,
Dominic

view this post on Zulip Email Gateway (Aug 22 2022 at 15:54):

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

thanks for reporting this.

A possible solution is currently in testing:

http://isabelle.in.tum.de/repos/testboard/rev/110a787dc7c9

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 15:55):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Great, thanks for that!

Last updated: Apr 23 2024 at 16:19 UTC