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

Oops, my apologies. The imports was wrong. From the `UserGuide.thy` source file, I changed it into the following, and it's OK with `CALL`:


Le Fri, 18 Apr 2014 03:22:35 +0200, Yannick Duchêne (Hibou57) <yannick_duchene at> a écrit:


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"

       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


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.