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:
>
>         http://isabelle.in.tum.de/repos/testboard/rev/110a787dc7c9
>
> Cheers,
>         Florian
>
> Am 26.07.2017 um 17:59 schrieb Dominic Mulligan via Cl-isabelle-users:
>> 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
>>
>
> --
>
> PGP available:
> http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.