|
|
|---|
|
|
|
|---|
Function definitions with contracts extending defunc.
(definec f (x :nat y :nat) :nat (+ x y)) (definec len (a :all) :nat (if (atom a) 0 (+ 1 (len (rest a))))) (definec app (x :tl y :tl) :tl (if (endp x) y (cons (car x) (app (cdr x) y)))) (definec square-list (l nat-list) nat-list (if (endp l) nil (app (list (* (car l) (car l))) (square-list (cdr l)))) :verbose t :skip-tests t)
The macro definec is an extension of defunc that makes it more convient to specify simple contracts. For example, the expansions of
(definec f (x :nat y :nat) :nat (+ x y))
and
(definec f (x nat y nat) nat (+ x y))
are equivalent and include the following events.
(defunc f (x y) :input-contract (and (natp x) (natp y)) :output-contract (natp (f x y)) (+ x y)) (defthm f-definec-fc-rule (implies (force (and (natp x) (natp y))) (natp (f x y))) :rule-classes ((:forward-chaining :trigger-terms ((f x y)))))
Notice that nat was turned into natp. We convert type names into the corresponding predicates using defdata and we support all (the type of the ACL2 universe), tl (the type of true-lists), int (the type of integers), bool (the type of booleans) and all other types defdata knows.
When specifying types one can use keywords or regular symbols, as shown above. It is important to put a space between the variable name and the type, e.g., x:nat will lead to errors.
As the examples above show, the paramater types and the return type are used to generate defunc contracts and then the rest of the arguments are passed to defunc, so you can use all the bells and whistles of defunc.