Re: [isabelle] export_code to ml, big_int, pattern matching, Error: Syntax error: operator expected.
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:
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), ) ->
("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;
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:
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