[patch] teach Array.append to Pinterp
I'm going through the why3 tutorial in the manual, now at the MaxAndSum problem ( http://why3.lri.fr/doc/whyml.html#sec17 ). The manual does not give an example of how to actually test the program! I wrote some test code
let test () =
let one x = Array.make 1 x in
let (++) a b = Array.append a b in
max_sum (one 1 ++ one 3 ++ one 2)
and I found some documentation in how to actually run the test in section 7.1 ( http://why3.lri.fr/doc/exec.html#sec101 ). But running my test code (which is different from the one in 7.1) exhibits the following behavior:
File "../buffer/max_and_sum.mlw", line 3, characters 2-20:
warning: the keyword `import' is redundant here and can be omitted
File "../buffer/max_and_sum.mlw", line 4, characters 2-20:
warning: the keyword `import' is redundant here and can be omitted
File "../buffer/max_and_sum.mlw", line 5, characters 2-24:
warning: the keyword `import' is redundant here and can be omitted
Execution of MaxAndSum.test ():
type: (int, int)
anomaly: Why3.Pinterp.CannotCompute
After scratching my head, I figured out that the problem is with the Array.append function, which is defined as a built-in in the standard library. The following patch (suitable for git am
application)
0001-teach-Array.append-to-Pinterp.patch
lets pinterp.ml know about Array.append, and now my code above successfully computes the expected result.
Question
There is also a mlinterp.ml
file which looks very similar and also lacks an Array.append
primitive. What is this file used for? Should I also add the primitive there?