Re: [isabelle] export_code to ml, big_int, pattern matching, Error: Syntax error: operator expected.

Hi Tom,

The problem is that partial_term_of has code equations which pattern-match on Code_Integer.integer literals (namely 0 or 1) and there is a code_printing setup for this type. The simplest approach is probably to change the code equations such that they do if-tests rather than pattern matching. But before you do that: Why does the export_code command generate a definition for partial_term_of at all? This is supposed to be a constant that is used only internally by quickcheck with narrowing and therefore should only ever be exported to Haskell.

Can you find out why partial_term_of shows up in the generated code at all?


On 03/11/16 10:06, Tom Ridge via Cl-isabelle-users wrote:
Dear All,

I am extracting some isabelle code to ocaml.

The generated code contains monster definitions like:

let rec partial_term_of_rresult _A
  ty x1 = match ty, x1 with
    ty, Narrowing_constructor ((Big_int.big_int_of_int 1), []) ->
      Const ("Util.rresult.Error",
                ("Util.rresult", [typerep _A.typerep_partial_term_of Type]))
    | ty, Narrowing_constructor (Big_int.zero_big_int, [a]) ->
        App (Const ("Util.rresult.Ok",
                         [typerep _A.typerep_partial_term_of Type;
                               [typerep _A.typerep_partial_term_of
              partial_term_of _A Type a)
    | ty, Narrowing_variable (p, tt) ->
        Free ("_", Typerep
                       [typerep _A.typerep_partial_term_of Type]));;

Unfortunately this won't compile: ocamlc gives "Error: Syntax error:
operator expected."

The problem is that the expression (Big_int.big_int_of_int 1) is used as a
pattern, but it is a function application.

A quick fix is to manually replace occurrences with a variable "x" and add
a "when" clause to the pattern. But obviously manually editing generated
code is a no-no.

What am I doing wrong?


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