instance - ACL2 Book

other

(in-package "INSTANCE")

other

(program)

instance-variablepfunction

(defun instance-variablep
  (x)
  (and (symbolp x)
    (equal (car (explode-atom x 10)) #\?)))

other

(mutual-recursion (defun instance-unify-term
    (pattern term sublist)
    (if (atom pattern)
      (if (instance-variablep pattern)
        (let ((value (assoc pattern sublist)))
          (if (consp value)
            (if (equal term (cdr value))
              (mv t sublist)
              (mv nil nil))
            (mv t
              (acons pattern term sublist))))
        (if (equal term pattern)
          (mv t sublist)
          (mv nil nil)))
      (if (or (atom term)
          (not (eq (car term) (car pattern))))
        (mv nil nil)
        (if (or (eq (car term) 'quote)
            (eq (car pattern) 'quote))
          (if (equal term pattern)
            (mv t sublist)
            (mv nil nil))
          (instance-unify-list (cdr pattern)
            (cdr term)
            sublist)))))
  (defun instance-unify-list
    (pattern-list term-list
      sublist)
    (if (or (atom term-list)
        (atom pattern-list))
      (if (and (atom term-list)
          (atom pattern-list))
        (mv t sublist)
        (mv nil nil))
      (mv-let (successp new-sublist)
        (instance-unify-term (car pattern-list)
          (car term-list)
          sublist)
        (if successp
          (instance-unify-list (cdr pattern-list)
            (cdr term-list)
            new-sublist)
          (mv nil nil))))))

instance-substitutefunction

(defun instance-substitute
  (sublist term)
  (if (endp sublist)
    term
    (let* ((old (car (car sublist))) (new (cdr (car sublist)))
        (result (subst new old term)))
      (instance-substitute (cdr sublist)
        result))))

other

(mutual-recursion (defun instance-rewrite1
    (pat repl term)
    (mv-let (successful sublist)
      (instance-unify-term pat
        term
        nil)
      (if successful
        (instance-substitute sublist
          repl)
        (if (atom term)
          term
          (cons (instance-rewrite1 pat
              repl
              (car term))
            (instance-rewrite-lst1 pat
              repl
              (cdr term)))))))
  (defun instance-rewrite-lst1
    (pat repl lst)
    (if (endp lst)
      nil
      (cons (instance-rewrite1 pat
          repl
          (car lst))
        (instance-rewrite-lst1 pat
          repl
          (cdr lst))))))

instance-rewritefunction

(defun instance-rewrite
  (term subs)
  (if (endp subs)
    term
    (let ((first-sub (car subs)))
      (instance-rewrite (instance-rewrite1 (first first-sub)
          (second first-sub)
          term)
        (cdr subs)))))

instance-declsfunction

(defun instance-decls
  (decls subs)
  (if (endp decls)
    nil
    (if (pseudo-termp (car decls))
      (cons (instance-rewrite (car decls)
          subs)
        (instance-decls (cdr decls)
          subs))
      (cons (car decls)
        (instance-decls (cdr decls)
          subs)))))

instance-defunfunction

(defun instance-defun
  (defun subs)
  (let* ((defun-symbol (first defun)) (defun-name (second defun))
      (defun-args (third defun))
      (defun-decls (butlast (cdddr defun) 1))
      (defun-body (car (last defun)))
      (name/args (cons defun-name defun-args))
      (new-body (instance-rewrite defun-body
          subs))
      (new-name/args (instance-rewrite name/args
          subs))
      (new-decls (instance-decls defun-decls
          subs))
      (new-name (car new-name/args))
      (new-args (cdr new-name/args)))
    `(,INSTANCE::DEFUN-SYMBOL ,INSTANCE::NEW-NAME
      ,INSTANCE::NEW-ARGS
      ,@INSTANCE::NEW-DECLS
      ,INSTANCE::NEW-BODY)))

instance-defunsfunction

(defun instance-defuns
  (defun-list subs)
  (if (endp defun-list)
    nil
    (cons (instance-defun (car defun-list)
        subs)
      (instance-defuns (cdr defun-list)
        subs))))

defthm-namesfunction

(defun defthm-names
  (event-list)
  (if (endp event-list)
    nil
    (let* ((first-event (car event-list)) (event-type (first first-event)))
      (cond ((or (eq event-type 'defthm)
           (eq event-type 'defthmd)) (cons (second first-event)
            (defthm-names (cdr event-list))))
        ((eq event-type 'encapsulate) (append (defthm-names (cddr first-event))
            (defthm-names (cdr event-list))))
        (t (defthm-names (cdr event-list)))))))

create-new-namesfunction

(defun create-new-names
  (name-list suffix)
  (if (endp name-list)
    nil
    (acons (car name-list)
      (intern-in-package-of-symbol (string-append (symbol-name (car name-list))
          (symbol-name suffix))
        suffix)
      (create-new-names (cdr name-list)
        suffix))))

rename-defthmsfunction

(defun rename-defthms
  (event-list suffix)
  (sublis (create-new-names (defthm-names event-list)
      suffix)
    event-list))

sub-to-lambdafunction

(defun sub-to-lambda
  (sub)
  (let ((term (first sub)) (repl (second sub)))
    (let ((function-symbol (car term)) (lambda-args (cdr term)))
      `(,INSTANCE::FUNCTION-SYMBOL (lambda ,INSTANCE::LAMBDA-ARGS ,INSTANCE::REPL)))))

subs-to-lambdasfunction

(defun subs-to-lambdas
  (subs)
  (if (endp subs)
    nil
    (cons (sub-to-lambda (car subs))
      (subs-to-lambdas (cdr subs)))))

other

(mutual-recursion (defun term-functions
    (term)
    (if (atom term)
      nil
      (cons (car term)
        (term-list-functions (cdr term)))))
  (defun term-list-functions
    (list)
    (if (endp list)
      nil
      (append (term-functions (car list))
        (term-list-functions (cdr list))))))

subs-repl-functionsfunction

(defun subs-repl-functions
  (subs)
  (if (endp subs)
    nil
    (let* ((sub1 (car subs)) (repl (second sub1)))
      (append (term-functions repl)
        (subs-repl-functions (cdr subs))))))

function-list-to-definitionsfunction

(defun function-list-to-definitions
  (funcs)
  (if (endp funcs)
    nil
    (cons `(:d ,(CAR INSTANCE::FUNCS))
      (function-list-to-definitions (cdr funcs)))))

subs-to-defsfunction

(defun subs-to-defs
  (subs generics)
  (let* ((all-fns (subs-repl-functions subs)) (real-fns (set-difference-eq all-fns
          generics)))
    (function-list-to-definitions real-fns)))

other

(defconst *default-parse-values*
  '((nil) (nil) (nil) (nil) (nil)))

parse-defthm-optionfunction

(defun parse-defthm-option
  (option return-value)
  (cond ((equal (first option) :rule-classes) (update-nth 0
        (list t (second option))
        return-value))
    ((equal (first option) :instructions) (update-nth 1
        (list t (second option))
        return-value))
    ((equal (first option) :hints) (update-nth 2
        (list t (second option))
        return-value))
    ((equal (first option) :otf-flg) (update-nth 3
        (list t (second option))
        return-value))
    ((equal (first option) :doc) (update-nth 4
        (list t (second option))
        return-value))
    (t (er hard
        "Unknown flag in defthm options ~x0."
        (first option)))))

parse-defthm-optionsfunction

(defun parse-defthm-options
  (options return-value)
  (if (endp options)
    return-value
    (parse-defthm-options (cddr options)
      (parse-defthm-option options
        return-value))))

instance-defthmfunction

(defun instance-defthm
  (event new-name
    subs
    generics
    extra-defs)
  (let* ((defthm-symbol (first event)) (defthm-name (second event))
      (defthm-body (third event))
      (new-body (instance-rewrite defthm-body
          subs))
      (options (parse-defthm-options (cdddr event)
          *default-parse-values*))
      (rc-opt (first options)))
    `(,INSTANCE::DEFTHM-SYMBOL ,INSTANCE::NEW-NAME
      ,INSTANCE::NEW-BODY
      :hints (("Goal" :use (:functional-instance ,INSTANCE::DEFTHM-NAME
           ,@(INSTANCE::SUBS-TO-LAMBDAS INSTANCE::SUBS))
         :in-theory (union-theories (theory 'minimal-theory)
           (union-theories ',INSTANCE::EXTRA-DEFS
             ',(INSTANCE::SUBS-TO-DEFS INSTANCE::SUBS INSTANCE::GENERICS)))))
      ,@(IF (CAR INSTANCE::RC-OPT)
      `(:RULE-CLASSES ,(CDR INSTANCE::RC-OPT))
      NIL))))

instance-signaturefunction

(defun instance-signature
  (signature subs)
  (let ((name (first signature)) (rest (rest signature)))
    (cons (instance-rewrite subs name)
      rest)))

instance-signaturesfunction

(defun instance-signatures
  (signatures subs)
  (if (endp signatures)
    nil
    (cons (instance-signature (car signatures)
        subs)
      (instance-signatures (cdr signatures)
        subs))))

other

(mutual-recursion (defun instance-event
    (event subs
      suffix
      generics
      mode
      extra-defs)
    (if (null suffix)
      event
      (cond ((or (eq (car event) 'defun)
           (eq (car event) 'defund)) (instance-defun event subs))
        ((or (eq (car event) 'defthm)
           (eq (car event) 'defthmd)) (let* ((name (second event)) (new-name (intern-in-package-of-symbol (string-upcase (concatenate 'string
                      (symbol-name name)
                      (symbol-name suffix)))
                  suffix)))
            (instance-defthm event
              new-name
              subs
              generics
              extra-defs)))
        ((equal (car event) 'local) (if (eq mode 'constrained)
            (instance-event (second event)
              subs
              suffix
              generics
              mode
              extra-defs)
            nil))
        ((equal (car event) 'encapsulate) (instance-encapsulate event
            subs
            suffix
            generics
            mode
            extra-defs))
        (t (er hard
            "Don't know how to handle ~x0"
            (car event))))))
  (defun instance-event-list
    (events subs
      suffix
      generics
      mode
      extra-defs)
    (if (endp events)
      nil
      (let ((first (instance-event (car events)
             subs
             suffix
             generics
             mode
             extra-defs)) (rest (instance-event-list (cdr events)
              subs
              suffix
              generics
              mode
              extra-defs)))
        (if first
          (cons first rest)
          rest))))
  (defun instance-encapsulate
    (event subs
      suffix
      generics
      mode
      extra-defs)
    (declare (ignore mode))
    (let* ((signatures (second event)) (new-sigs (if signatures
            (instance-signatures subs
              signatures)
            nil))
        (new-events (instance-event-list (cddr event)
            subs
            suffix
            generics
            (if signatures
              'constrained
              nil)
            extra-defs)))
      `(encapsulate ,INSTANCE::NEW-SIGS
        ,@INSTANCE::NEW-EVENTS))))

instancemacro

(defmacro instance
  (theory)
  (let ((macro-name (intern-in-package-of-symbol (string-upcase (concatenate 'string "instance-" (string theory)))
         theory)))
    `(defmacro ,INSTANCE::MACRO-NAME
      (&key subs
        suffix
        generics
        extra-defs)
      (list* 'encapsulate
        nil
        (instance-event-list ,INSTANCE::THEORY
          subs
          suffix
          generics
          nil
          extra-defs)))))