All Specware functions are unary. Multiple argument functions are modeled using either functions with product domains, or curried functions. For efficiency we wish to exploit Common Lisp's support of n-ary functions. Arity normalization aims to minimize unpacking and packing of products when passing arguments to functions with product domains, and currying normalization aims to minimize closure creation when calling curried functions. The saving is particularly important for recursive functions where there is saving at each recursive call, and in addition, currying normalization may permit the Common Lisp compiler to do tail recursion optimization. The naming scheme does not require knowledge of the definition of a function when generating calls to the function.
For each function whose argument is a product, two entry points are created: a unary function whose name is derived from the op as described above, and an n-ary function whose name has "-n" appended. Fir example, for
op min : Integer * Integer -> Integer |
there are two Lisp functions, #'MIN-2 and #'|!min|. A call with an explicit product is translated to the n-ary version, otherwise the unary version is used. For example, min(1,2) translates to (MIN-2 1 2), and foldr min inf l translates to (FOLDR-1-1-1 #'|!min| INF L). When generating Lisp for a definition, the form is examined to see whether the definition is naturally n-ary. If it is, then the primary definition is n-ary and the unary function is defined in terms of the n-ary function, otherwise the situation is reversed. For example, given the definition
def min(x,y) = if x <= y then x else y |
we get the two Common Lisp definitions:
(DEFUN MIN-2 (X Y) (if (<= x y) x y)) (DEFIN |!min| (X) (MIN-2 (CAR X) (CDR X))) |
and given the definition
def multFG(x: Nat * Nat) = (F x) * (G x) |
we get the two Common Lisp definitions:
(DEFUN MULTFG-2 (X Y) (MULTFG (CONS X Y))) (DEFUN MULTFG (X) (* (F X) (G X))) |
For each curried function (i.e. for each function whose codomain is a function) there is an additional uncurried version of the function with "-1" added n times to the name where n is the number of curried arguments. For example, for
op foldr: fa(key,a,b) (a * b -> b) -> b -> map(key,a) -> b |
there are two Lisp functions, #'FOLDR and #'FOLDR-1-1-1.
As with arity normalization, the definition of a curried function is examined to see whether it should be used to generate the curried or the uncurried version, with the other being defined in terms of this primary version.
As well as producing more efficient code, the currying normalization makes code easier to debug using the Common Lisp trace facility. For example if a function has a call of the form foldr x y z, this call is implemented as (FOLDR-1-1-1 x y z), so you can trace FOLDR-1-1-1 to find out how it is being called and what it is returning.