[isabelle] Issue with `Simpl` user guide `Fac` example



Hi,

I wanted to have a look at Simpl. I built it from a local AFP copy. In the documentation, there is a section titled “User Guide” (I jumped there nearly immediately). In this section, at “34.3.4 Recursion”, there is a sample `Fac` imperative function.

If I type exactly what's exemplified there, I get an error about a type unification failure. I have to change `CALL` into `PROC` in order to make it work:

    theory Test_Simpl
    imports "$AFP/Simpl/Simpl"
    begin

      primrec fac :: "nat ⇒ nat"
        where "fac 0 = 1"
            | "fac (Suc n) = (Suc n) * (fac n)";

      procedures Fac (N :: nat | R :: nat)
        "IF ´N = 0 THEN ´R :== 1
         ELSE ´R :== PROC Fac(´N - 1);; ´R :== ´N * ´R
         FI";

    end

If I write `CALL` instead of `PROC` (the user guide really says `CALL`), I get this:

    Type unification failed: Clash of types "⦇A_' :: nat,
                      B_' :: nat, C_' :: nat,
                      I_' :: nat, M_' :: nat,
                      N_' :: nat, R_' :: nat,
                      S_' :: nat, Arr_' :: nat list,
                      Abr_' :: char list,
                      … ::
                        _⦈" and "⦇locals :: _ ⇒ _,
          … :: _⦈"

    Type error in application: incompatible operand type

    Operator:  locals ::
      (??'a, ??'b, ??'c, ??'d) stateSP_scheme
      ⇒ ??'b ⇒ ??'c
    Operand:   s :: (??'a, ??'e) XVcgEx.vars_scheme


I feel disturbed. First the documentation seems wrong, and then, the documentation which was generated by a fresh build, should have failed if there is an error somewhere. Or am I wrong? Do I have to report this as a bug to the author?


Also, a question aside: is it mandatory to import `$AFP/Simpl/Simpl`? It takes long to load for me, near to ten minutes. Is there an alternative sufficient subset?


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





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