Incorrect order of variables in error message of transformation `apply`
The apply
transformation displays missing terms since #219 (closed), which is very useful.
However, the order of variables that are let
-bound within the rule seems incorrect. The let
-bound variables are displayed at the end of the list, whereas they have to be, in reversed order, provided first. (Should let
-bound variables be missing from apply
at all?)
Example
module Test
type a constant a0: a
type b constant b0: b
type c constant c0: c
function f unit : b
function g unit : c
predicate p a b c
axiom a : forall a.
let b = f () in
let c = g () in
p a b c ->
false
goal g : false
end
The transformation apply a
complaints on goal g
that
Error in transformation function: apply: there are 3 terms missing: a2 b1
c1
But the transformation apply with a0,b0,c0
fails with message
Error in transformation apply during unification of following two terms:
c1 : c
a0 : a1
Transformation failed:
apply a with a0,b0,c0
The transformation apply a with c0,b0,a0
actually works.