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

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.