definec - ACL2 Book

other

(in-package "ACL2S")

other

(include-book "defunc" :ttags :all)

map-predsfunction

(defun map-preds
  (types tbl atbl)
  (declare (xargs :guard (and (symbol-listp types)
        (sym-aalistp tbl)
        (sym-aalistp atbl))))
  (if (endp types)
    nil
    (cons (pred-of-type (car types)
        tbl
        atbl)
      (map-preds (rest types)
        tbl
        atbl))))

map-intern-typefunction

(defun map-intern-type
  (type pkg)
  (declare (xargs :guard (and (symbolp type) (pkgp pkg))))
  (if (keywordp type)
    (fix-intern$ (symbol-name type) pkg)
    type))

map-intern-typesfunction

(defun map-intern-types
  (types pkg)
  (declare (xargs :guard (and (symbol-listp types)
        (pkgp pkg))))
  (if (endp types)
    nil
    (cons (map-intern-type (car types) pkg)
      (map-intern-types (rest types) pkg))))

make-input-contract-auxfunction

(defun make-input-contract-aux
  (args types)
  (declare (xargs :guard (and (symbol-listp args)
        (symbol-listp types))))
  (cond ((endp args) nil)
    ((equal (car types) 'allp) (make-input-contract-aux (rest args)
        (rest types)))
    (t (cons `(,(CAR ACL2S::TYPES) ,(CAR ACL2S::ARGS))
        (make-input-contract-aux (rest args)
          (rest types))))))

make-input-contractfunction

(defun make-input-contract
  (args types)
  (declare (xargs :guard (and (symbol-listp args)
        (symbol-listp types))))
  (let ((res (make-input-contract-aux args types)))
    (cond ((endp res) t)
      ((equal (len res) 1) (first res))
      (t (cons 'and res)))))

find-bad-d-arg-typesfunction

(defun find-bad-d-arg-types
  (d-arg-types d-arg-preds)
  (cond ((endp d-arg-preds) nil)
    ((null (car d-arg-preds)) (car d-arg-types))
    (t (find-bad-d-arg-types (cdr d-arg-types)
        (cdr d-arg-preds)))))

find-next-typefunction

(defun find-next-type
  (var l acc)
  (cond ((endp l) acc)
    ((keywordp (car l)) (find-next-type var
        (cdr l)
        (cons (car l) (cons var acc))))
    ((endp acc) (find-next-type var (cdr l) acc))
    (t acc)))

process-typed-args-auxfunction

(defun process-typed-args-aux
  (l acc)
  (cond ((endp l) (rev acc))
    ((keywordp (car l)) (process-typed-args-aux (cdr l) acc))
    (t (process-typed-args-aux (cdr l)
        (append (find-next-type (car l) (cdr l) nil)
          acc)))))

process-typed-argsfunction

(defun process-typed-args
  (l)
  (process-typed-args-aux l nil))

skip-keywordsfunction

(defun skip-keywords
  (l)
  (cond ((endp l) l)
    ((keywordp (car l)) (skip-keywords (cdr l)))
    (t l)))

proper-argspfunction

(defun proper-argsp
  (l)
  (or (endp l)
    (and (consp (cdr l))
      (legal-variablep (first l))
      (if (keywordp (second l))
        (proper-argsp (skip-keywords (cddr l)))
        (proper-argsp (cdr l))))))

definec-coremacro

(defmacro definec-core
  (name d? &rest args)
  `(with-output :stack :push :off :all :on (error comment)
    (make-event (b* ((tbl (table-alist 'type-metadata-table
             (w state))) (atbl (table-alist 'type-alias-table
              (w state)))
          (pkg (current-package state))
          (name ',ACL2S::NAME)
          (d? ',ACL2S::D?)
          (args ',ACL2S::ARGS)
          (f-args (car args))
          ((unless (proper-argsp f-args)) (er hard
              'definec
              "~%The arguments to ~x0 are not well formed.
See the documentation for example arguments: ~x1"
              name
              f-args))
          (f-argsp (process-typed-args f-args))
          (f-type (map-intern-type (second args) pkg))
          (d-args (evens f-argsp))
          (def-args (remove-duplicates d-args))
          (d-arg-types (odds f-argsp))
          (d-arg-types (map-intern-types d-arg-types pkg))
          (d-arg-preds (map-preds d-arg-types tbl atbl))
          (pred (pred-of-type f-type tbl atbl))
          (ic (make-input-contract d-args
              d-arg-preds))
          (oc (make-contract name
              def-args
              pred))
          (defunc `(defunc-core ,ACL2S::NAME
              ,ACL2S::D?
              ,ACL2S::DEF-ARGS
              :input-contract ,ACL2S::IC
              :output-contract ,ACL2S::OC
              ,@(CDDR ACL2S::ARGS)))
          (bad-type (find-bad-d-arg-types d-arg-types
              d-arg-preds))
          ((when bad-type) (er hard
              'definec
              "~%One of the argument types, ~x0, is not a type."
              bad-type))
          ((unless pred) (er hard
              'definec
              "~%The given return type, ~x0, is not a known type."
              f-type)))
        `(with-output :stack :pop ,ACL2S::DEFUNC)))))

definecmacro

(defmacro definec
  (name &rest args)
  `(definec-core ,ACL2S::NAME nil ,@ACL2S::ARGS))

definedcmacro

(defmacro definedc
  (name &rest args)
  `(definec-core ,ACL2S::NAME t ,@ACL2S::ARGS))

other

(include-book "xdoc/top" :dir :system)

other

(defxdoc definec
  :parents (acl2-sedan macro-libraries defunc)
  :short "Function definitions with contracts extending @(see defunc)."
  :long "
<h3>Examples</h3>

@({

  (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)
})

<h3>Purpose</h3>
<p>
The macro @(see definec) is an extension of @(see defunc)
that makes it more convient to specify simple contracts.
For example, the expansion of
</p>

@({

  (definec f (x y :nat) :nat
    (+ x y))
})

<p>
includes the following events.
</p>

@({

  (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)))))

})

<p> Notice that nat was turned into natp. We convert type names into
the corresponding predicates using @(see 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 @(see defdata) knows.  </p>

<p>
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.
</p>

<p>
As the examples above show, the parameter types and the return type
are used to generate @(see defunc) contracts and then the rest of
the arguments are passed to @(see defunc), so you can use all the
bells and whistles of @(see defunc).

</p>
")

definecdmacro

(defmacro definecd
  (name &rest args)
  `(with-output :off :all :on (error)
    :stack :push (encapsulate nil
      (with-output :stack :pop (definec ,ACL2S::NAME ,@ACL2S::ARGS))
      (make-event `(with-output :off :all :on (summary)
          :summary-off (:other-than form)
          (in-theory (disable ,(ACL2S::MAKE-SYMBL `(,',ACL2S::NAME ACL2S::-DEFINITION-RULE)
  (ACL2S::CURRENT-PACKAGE ACL2S::STATE)))))))))

definedcdmacro

(defmacro definedcd
  (name &rest args)
  `(with-output :off :all :on (error)
    :stack :push (encapsulate nil
      (with-output :stack :pop (definedc ,ACL2S::NAME ,@ACL2S::ARGS))
      (make-event `(with-output :off :all :on (summary)
          :summary-off (:other-than form)
          (in-theory (disable ,(ACL2S::MAKE-SYMBL `(,',ACL2S::NAME ACL2S::-DEFINITION-RULE)
  (ACL2S::CURRENT-PACKAGE ACL2S::STATE)))))))))

definec-no-testmacro

(defmacro definec-no-test
  (name &rest args)
  `(gen-acl2s-local testing-enabled
    nil
    ((definec ,ACL2S::NAME ,@ACL2S::ARGS))))

definecd-no-testmacro

(defmacro definecd-no-test
  (name &rest args)
  `(gen-acl2s-local testing-enabled
    nil
    ((definecd ,ACL2S::NAME ,@ACL2S::ARGS))))

definedc-no-testmacro

(defmacro definedc-no-test
  (name &rest args)
  `(gen-acl2s-local testing-enabled
    nil
    ((definedc ,ACL2S::NAME ,@ACL2S::ARGS))))

definedcd-no-testmacro

(defmacro definedcd-no-test
  (name &rest args)
  `(gen-acl2s-local testing-enabled
    nil
    ((definedcd ,ACL2S::NAME ,@ACL2S::ARGS))))