[isabelle] OCaml code generation producing invalid code



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




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