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



Not sure why it appears (indeed, I don't really need this defn at all). The
.thy file is attached. I am on Isabelle2015.



On 3 November 2016 at 10:26, Andreas Lochbihler <
andreas.lochbihler at inf.ethz.ch> wrote:

> 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
>
>
>
>
> 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",
>>               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
>>
>>

Attachment: Util.thy
Description: Binary data



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