|
|
|---|
|
|
|
|---|
Function definitions with contracts extending defunc.
(definec my-len (a :all) :nat (if (atom a) 0 (+ 1 (my-len (rest a))))) ; An alternate, but equivalent, definition of my-len (definec my-len (a :all) :nat (match a (:atom 0) ((& . r) (1+ (my-len r))))) ; Notice that both x and y are nats (definec f (x y :nat) :nat (+ x y)) ; Both x and y are true-lists (definec my-app (x y :tl) :tl (match x (nil y) ((f . r) (cons f (my-app r y))))) ; All is the universal type (definec my-atom (x :all) :bool (atom x)) ; Factorial (definec my-fact (x :nat) :pos (match x ((:or 0 1) 1) (& (* x (my-fact (1- x)))))) ; list-sum (definec list-sum (l :rational-list) :rational (match l (nil 0) ((f . r) (+ f (list-sum r))))) ; Average: notice that l is a both a rational-list and a cons (definec average (l :rational-list :cons) :rational (/ (list-sum l) (len l))) ; Square a list, with some extra keyword arguments (definec square-list (l :nat-list) :nat-list (match l (nil nil) ((f . r) (app (list (* f f)) (square-list r)))) :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 expansion of
(definec f (x y :nat) :nat (+ x y))
includes 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 must use keywords, 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.