Extraction to OCaml does not properly handle syntactic shortcuts
The OCaml driver allows to not write %1
, %2
, etc, when an OCaml function has the same arguments as the corresponding WhyML function. For example,
module stack.Stack
syntax val pop "Stack.pop"
syntax val top "Stack.top"
Unfortunately, the OCaml printer does not handle these shortcuts properly. For example,
use stack.Stack
let f t raises { Empty } = pop t
gets extracted to
let f : type xi . (xi Stack.t) -> xi = fun t -> Stack.pop