Re: [isabelle] OCaml code generation producing invalid code



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

Attachment: signature.asc
Description: OpenPGP digital signature



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