Re: [isabelle] OCaml code generation producing invalid code
Great, thanks for that!
On 3 August 2017 at 14:01, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> Hi Dominic,
> thanks for reporting this.
> A possible solution is currently in testing:
> Am 26.07.2017 um 17:59 schrieb Dominic Mulligan via Cl-isabelle-users:
>> It seems that the OCaml serialisation for the code generator in
>> Isabelle2016-1 sometimes spits out invalid OCaml. The following small
>> theory Test imports Main begin
>> definition foo :: "bool" where
>> "foo â âc::char. c = CHR 0x1"
>> export_code foo in OCaml
>> file "test.ml"
>> 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
>> 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
> PGP available:
This archive was generated by a fusion of
Pipermail (Mailman edition) and