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



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

On 03/11/16 12:39, Tom Ridge wrote:
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
<mailto: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






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