Email Gateway (Aug 22 2022 at 14:30): Email Gateway (Aug 22 2022 at 14:30):From: Tom Ridge via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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",
Typerep
("Util.rresult", [typerep _A.typerep_partial_term_of Type]))
| ty, Narrowing_constructor (Big_int.zero_big_int, [a]) ->
App (Const ("Util.rresult.Ok",
Typerep
("fun",
[typerep _A.typerep_partial_term_of Type;
Typerep
("Util.rresult",
[typerep _A.typerep_partial_term_of
Type])])),
partial_term_of _A Type a)
| ty, Narrowing_variable (p, tt) ->
Free ("_", Typerep
("Util.rresult",
[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?
Thanks
Email Gateway (Aug 22 2022 at 14:31):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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?
Andreas
Email Gateway (Aug 22 2022 at 14:31):From: Tom Ridge via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Not sure why it appears (indeed, I don't really need this defn at all). The
.thy file is attached. I am on Isabelle2015.
Util.thy
Email Gateway (Aug 22 2022 at 14:31):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Tom,
Your export_code command says that you want to export all constants defined in Util.thy.
Since the partial_term_of instance for rresult happens at the datatype declaration,
"Util._" also selects the definitions for the type class instance. So, if you select only
the functions you are interested in (say by explicitly listing them), you should not get
such monster definitions.
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 14:31):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Tom,
Your export_code command says that you want to export all constants defined in Util.thy.
Since the partial_term_of instance for rresult happens at the datatype declaration,
"Util._" also selects the definitions for the type class instance. So, if you select only
the functions you are interested in (say by explicitly listing them), you should not get
such monster definitions.
Hope this helps,
Andreas
Last updated: Apr 26 2024 at 12:28 UTC