definductor - ACL2 Book

other

(in-package "ACL2")

other

(program)

car/cdr-nestpfunction

(defun car/cdr-nestp
  (cdr-only-flg term mvars)
  (cond ((variablep term) (if (member-eq term mvars)
        term
        nil))
    ((fquotep term) nil)
    ((or (and (not cdr-only-flg) (eq (ffn-symb term) 'car))
       (eq (ffn-symb term) 'cdr)) (car/cdr-nestp cdr-only-flg (fargn term 1) mvars))
    (t nil)))

glue-termsfunction

(defun glue-terms
  (terms term)
  (cond ((endp terms) term)
    ((or (member-equal (car terms) (cdr terms))
       (equal (car terms) term)) (glue-terms (cdr terms) term))
    (t `(return-last 'progn
        ,(MARK-LOOP$-RECURSION-NUGGET (CAR TERMS))
        ,(GLUE-TERMS (CDR TERMS) TERM)))))

nugget-fn-call-actuals1function

(defun nugget-fn-call-actuals1
  (op targets)
  (cond ((endp targets) nil)
    (t (cons (cons (car (all-vars (car targets)))
          (if op
            (list op (car targets))
            (car targets)))
        (nugget-fn-call-actuals1 op (cdr targets))))))

nugget-fn-call-actualsfunction

(defun nugget-fn-call-actuals
  (formals op targets)
  (sublis-var-lst (nugget-fn-call-actuals1 op targets)
    formals))

car-cdr-cons-rewritermutual-recursion

(mutual-recursion (defun car-cdr-cons-rewriter
    (term)
    (cond ((variablep term) term)
      ((fquotep term) term)
      ((eq (ffn-symb term) 'car) (let ((arg (car-cdr-cons-rewriter (fargn term 1))))
          (cond ((variablep arg) term)
            ((fquotep arg) (let ((evg (unquote arg)))
                (cond ((atom evg) *nil*) (t (kwote (car evg))))))
            ((eq (ffn-symb arg) 'cons) (fargn arg 1))
            (t term))))
      ((eq (ffn-symb term) 'cdr) (let ((arg (car-cdr-cons-rewriter (fargn term 1))))
          (cond ((variablep arg) term)
            ((fquotep arg) (let ((evg (unquote arg)))
                (cond ((atom evg) *nil*) (t (kwote (cdr evg))))))
            ((eq (ffn-symb arg) 'cons) (fargn arg 2))
            (t term))))
      (t (fcons-term (ffn-symb term)
          (car-cdr-cons-rewriter-list (fargs term))))))
  (defun car-cdr-cons-rewriter-list
    (terms)
    (cond ((endp terms) nil)
      (t (cons (car-cdr-cons-rewriter (car terms))
          (car-cdr-cons-rewriter-list (cdr terms)))))))

car/cdr-nestspfunction

(defun car/cdr-nestsp
  (cdr-only-flg terms mvars)
  (cond ((endp terms) t)
    (t (and (car/cdr-nestp cdr-only-flg (car terms) mvars)
        (car/cdr-nestsp cdr-only-flg (cdr terms) mvars)))))

leftmost-innermostfunction

(defun leftmost-innermost
  (term)
  (cond ((variablep term) term)
    ((or (fquotep term) (null (fargs term))) term)
    (t (leftmost-innermost (fargn term 1)))))

leftmost-innermost-lstfunction

(defun leftmost-innermost-lst
  (terms)
  (cond ((endp terms) nil)
    (t (cons (leftmost-innermost (car terms))
        (leftmost-innermost-lst (cdr terms))))))

variablespfunction

(defun variablesp
  (lst)
  (cond ((endp lst) t)
    (t (and (variablep (car lst)) (variablesp (cdr lst))))))

true-cons-nestpfunction

(defun true-cons-nestp
  (term)
  (cond ((variablep term) nil)
    ((fquotep term) (equal term *nil*))
    (t (and (eq (ffn-symb term) 'cons)
        (true-cons-nestp (fargn term 2))))))

strip-true-cons-nestfunction

(defun strip-true-cons-nest
  (term)
  (cond ((variablep term) nil)
    ((fquotep term) nil)
    (t (cons (fargn term 1) (strip-true-cons-nest (fargn term 2))))))

conjoined-conspsfunction

(defun conjoined-consps
  (terms)
  (cond ((endp terms) *t*)
    (t `(if (consp ,(CAR TERMS))
        ,(CONJOINED-CONSPS (CDR TERMS))
        'nil))))

consed-carsfunction

(defun consed-cars
  (terms)
  (cond ((endp terms) *nil*)
    (t `(cons (car ,(CAR TERMS)) ,(CONSED-CARS (CDR TERMS))))))

variablep-lstfunction

(defun variablep-lst
  (lst)
  (cond ((endp lst) t)
    (t (and (variablep (car lst)) (variablep-lst (cdr lst))))))

nuggetfunction

(defun nugget
  (fn formals mvars alist term)
  (let ((style (loop$-scion-style (ffn-symb term))))
    (cond ((eq style :plain) (case-match term
          ((& ('quote ('lambda (e) body)) target) (cond ((not (loop$-recursion-ffnnamep fn body)) (mv nil nil))
              (t (let ((resolved-target (sublis-var alist target)))
                  (cond ((car/cdr-nestp t target mvars) (let* ((resolved-var (leftmost-innermost resolved-target)))
                        (mv nil
                          `(if (consp ,RESOLVED-VAR)
                            ,(GLUE-TERMS
  `(,(IF (FFNNAMEP FN BODY)
         (CAR-CDR-CONS-REWRITER
          (EXPAND-ALL-LAMBDAS `((LAMBDA (,E) ,BODY) (CAR ,RESOLVED-VAR))))
         `(,FN ,@(NUGGET-FN-CALL-ACTUALS FORMALS 'CAR (LIST RESOLVED-VAR))))
    ,@(IF (VARIABLEP RESOLVED-TARGET)
          NIL
          `((,FN
             ,@(NUGGET-FN-CALL-ACTUALS FORMALS NIL (LIST RESOLVED-TARGET))))))
  `(,FN ,@(NUGGET-FN-CALL-ACTUALS FORMALS 'CDR (LIST RESOLVED-VAR))))
                            'nil))))
                    (t (mv (msg "it contains a loop$ over the non-inductible target ~
                           ~x0."
                          target)
                        nil)))))))
          (& (mv nil nil))))
      ((eq style :fancy) (case-match term
          ((scion ('quote ('lambda (gvars ivars) body))
             gactuals
             target) (cond ((not (loop$-recursion-ffnnamep fn body)) (mv nil nil))
              ((not (and (nvariablep target)
                   (not (fquotep target))
                   (eq (ffn-symb target) 'loop$-as)
                   (true-cons-nestp (fargn target 1)))) (mv (msg "it uses the fancy loop$ scion ~x0 to map over a target, ~
                     ~x1, that we cannot destructure.  We expect the target ~
                     to be (LOOP$-AS (LIST t1 ... tn))."
                    scion
                    target)
                  nil))
              (t (let* ((targets (strip-true-cons-nest (fargn target 1))) (resolved-targets (sublis-var-lst alist targets)))
                  (cond ((car/cdr-nestsp t targets mvars) (let* ((resolved-vars (leftmost-innermost-lst resolved-targets)))
                        (cond ((not (no-duplicatesp resolved-vars)) (mv (msg "it calls the fancy loop$ scion ~x0 on a list of ~
                             targets that share measured formals ~x1."
                                scion
                                target)
                              nil))
                          (t (mv nil
                              `(if ,(CONJOINED-CONSPS RESOLVED-VARS)
                                ,(GLUE-TERMS
  `(,(IF (FFNNAMEP FN BODY)
         (CAR-CDR-CONS-REWRITER
          (EXPAND-ALL-LAMBDAS
           `((LAMBDA (,GVARS ,IVARS) ,BODY) ,GACTUALS
             ,(CONSED-CARS RESOLVED-VARS))))
         `(,FN ,@(NUGGET-FN-CALL-ACTUALS FORMALS 'CAR RESOLVED-VARS)))
    ,@(IF (VARIABLEP-LST RESOLVED-TARGETS)
          NIL
          `((,FN ,@(NUGGET-FN-CALL-ACTUALS FORMALS NIL RESOLVED-TARGETS)))))
  `(,FN ,@(NUGGET-FN-CALL-ACTUALS FORMALS 'CDR RESOLVED-VARS)))
                                'nil))))))
                    (t (mv (msg "it contains a loop$ over the non-inductible target ~
                           ~x0."
                          target)
                        nil)))))))
          (& (mv nil nil))))
      (t (mv nil nil)))))

generate-loop$-scion-nuggetsmutual-recursion

(mutual-recursion (defun generate-loop$-scion-nuggets
    (fn formals mvars alist term)
    (cond ((variablep term) (mv nil nil))
      ((fquotep term) (mv nil nil))
      ((lambda-applicationp term) (generate-loop$-scion-nuggets fn
          formals
          mvars
          alist
          (sublis-var (pairlis$ (lambda-formals (ffn-symb term)) (fargs term))
            (lambda-body (ffn-symb term)))))
      (t (mv-let (erp nugget)
          (nugget fn formals mvars alist term)
          (cond (erp (mv erp nil))
            (nugget (let* ((obj (unquote (fargn term 1))) (target (fargn term 2))
                  (ivar (car (lambda-object-formals obj)))
                  (mvars1 (add-to-set-eq ivar mvars))
                  (alist1 (cons (cons ivar `(car ,(SUBLIS-VAR ALIST TARGET))) alist))
                  (body (lambda-object-body obj)))
                (mv-let (erp nuggets-from-body)
                  (generate-loop$-scion-nuggets fn formals mvars1 alist1 body)
                  (cond (erp (mv erp nil))
                    (t (mv-let (erp nuggets-from-target)
                        (generate-loop$-scion-nuggets fn formals mvars alist target)
                        (cond (erp (mv erp nil))
                          (t (mv nil
                              (add-to-set-equal nugget
                                (union-equal nuggets-from-body nuggets-from-target)))))))))))
            (t (generate-loop$-scion-nuggets-list fn
                formals
                mvars
                alist
                (fargs term))))))))
  (defun generate-loop$-scion-nuggets-list
    (fn formals mvars alist terms)
    (cond ((endp terms) (mv nil nil))
      (t (mv-let (erp nuggets1)
          (generate-loop$-scion-nuggets fn
            formals
            mvars
            alist
            (car terms))
          (cond (erp (mv erp nil))
            (t (mv-let (erp nuggets2)
                (generate-loop$-scion-nuggets-list fn
                  formals
                  mvars
                  alist
                  (cdr terms))
                (cond (erp (mv erp nil))
                  (t (mv nil (union-equal nuggets1 nuggets2))))))))))))

get-loop$-scion-default-quoted-lambda-objectfunction

(defun get-loop$-scion-default-quoted-lambda-object
  (scion alist)
  (cond ((endp alist) *nil*)
    ((eq scion (cadr (car alist))) (case (car (car alist))
        (sum ''(lambda (e) (declare (ignore e)) '0))
        (always ''(lambda (e) (declare (ignore e)) 't))
        (thereis ''(lambda (e) (declare (ignore e)) 'nil))
        (collect ''(lambda (e) (declare (ignore e)) 'nil))
        (append ''(lambda (e) (declare (ignore e)) 'nil))
        (otherwise ''(lambda (e) (declare (ignore e)) 'nil))))
    ((eq scion (caddr (car alist))) (case (car (car alist))
        (sum ''(lambda (loop$-gvars loop$-ivars)
            (declare (ignore loop$-gvars loop$-ivars))
            '0))
        (always ''(lambda (loop$-gvars loop$-ivars)
            (declare (ignore loop$-gvars loop$-ivars))
            't))
        (thereis ''(lambda (loop$-gvars loop$-ivars)
            (declare (ignore loop$-gvars loop$-ivars))
            'nil))
        (collect ''(lambda (loop$-gvars loop$-ivars)
            (declare (ignore loop$-gvars loop$-ivars))
            'nil))
        (append ''(lambda (loop$-gvars loop$-ivars)
            (declare (ignore loop$-gvars loop$-ivars))
            'nil))
        (otherwise ''(lambda (loop$-gvars loop$-ivars)
            (declare (ignore loop$-gvars loop$-ivars))
            'nil))))
    (t (get-loop$-scion-default-quoted-lambda-object scion
        (cdr alist)))))

rename-fn-and-replace-for-loop$-lambda-objsmutual-recursion

(mutual-recursion (defun rename-fn-and-replace-for-loop$-lambda-objs
    (new-fn old-fn term)
    (cond ((variablep term) term)
      ((fquotep term) term)
      ((lambda-applicationp term) (cons-term (make-lambda (lambda-formals (ffn-symb term))
            (rename-fn-and-replace-for-loop$-lambda-objs new-fn
              old-fn
              (lambda-body (ffn-symb term))))
          (rename-fn-and-replace-for-loop$-lambda-objs-list new-fn
            old-fn
            (fargs term))))
      ((eq (ffn-symb term) old-fn) (cons-term new-fn
          (rename-fn-and-replace-for-loop$-lambda-objs-list new-fn
            old-fn
            (fargs term))))
      ((and (member-eq (loop$-scion-style (ffn-symb term))
           '(:plain :fancy))
         (quotep (fargn term 1))
         (consp (unquote (fargn term 1)))
         (eq (car (unquote (fargn term 1))) 'lambda)) (cons-term (ffn-symb term)
          (cons (get-loop$-scion-default-quoted-lambda-object (ffn-symb term)
              *for-loop$-keyword-info*)
            (rename-fn-and-replace-for-loop$-lambda-objs-list new-fn
              old-fn
              (cdr (fargs term))))))
      (t (cons-term (ffn-symb term)
          (rename-fn-and-replace-for-loop$-lambda-objs-list new-fn
            old-fn
            (fargs term))))))
  (defun rename-fn-and-replace-for-loop$-lambda-objs-list
    (new-fn old-fn terms)
    (cond ((endp terms) nil)
      (t (cons (rename-fn-and-replace-for-loop$-lambda-objs new-fn
            old-fn
            (car terms))
          (rename-fn-and-replace-for-loop$-lambda-objs-list new-fn
            old-fn
            (cdr terms)))))))

make-inductor-defun-and-rulefunction

(defun make-inductor-defun-and-rule
  (fn inductor-fn measure rel ruler-extenders hints wrld)
  (let* ((inductor-fn1 (or inductor-fn (packn (list fn '-inductor)))) (formals (formals fn wrld))
      (body (possibly-clean-up-dirty-lambda-objects :all (remove-guard-holders (body fn nil wrld) wrld)
          wrld
          (remove-guard-holders-lamp)))
      (jst (getpropc fn 'justification nil wrld))
      (measure1 (or measure (access justification jst :measure)))
      (rel1 (or rel (access justification jst :rel)))
      (ruler-extenders1 (or ruler-extenders
          (access justification jst :ruler-extenders)))
      (mvars (all-vars measure1)))
    (mv-let (erp nuggets)
      (generate-loop$-scion-nuggets fn formals mvars nil body)
      (cond (erp (mv erp nil))
        (t (let* ((body1 (if nuggets
                 (rename-fn-and-replace-for-loop$-lambda-objs-list inductor-fn1
                   fn
                   (glue-terms nuggets body))
                 *nil*)) (ignores (set-difference-eq formals (all-vars body1)))
              (rule-name (packn (list fn '-induction-rule))))
            (cond (nuggets (mv nil
                  `(encapsulate nil
                    (defun$ ,INDUCTOR-FN1
                      ,FORMALS
                      (declare (xargs :mode :logic :measure ,MEASURE1
                          :well-founded-relation ,REL1
                          :ruler-extenders ,RULER-EXTENDERS1
                          ,@(IF HINTS
      `(:HINTS ,HINTS)
      NIL))
                        ,@(IF IGNORES
      `(IGNORE ,@IGNORES)
      NIL))
                      ,BODY1)
                    (defthm ,RULE-NAME
                      t
                      :rule-classes ((:induction :pattern (,FN ,@FORMALS)
                         :scheme (,INDUCTOR-FN1 ,@FORMALS)))))))
              (t (mv (msg "there are no recursive loop$s in it.") nil)))))))))

other

(set-state-ok t)

definductor-fn1function

(defun definductor-fn1
  (fn inductor-fn
    measure
    well-founded-relation
    ruler-extenders
    hints
    state)
  (let ((wrld (w state)))
    (cond ((or (not (symbolp fn))
         (not (getpropc fn 'loop$-recursion nil wrld))) (er soft
          'definductor
          "The first argument to definductor must be the name of a previously ~
         defined loop$-recursive function and ~x0 is not."
          fn))
      ((not (symbolp inductor-fn)) (er soft
          'definductor
          "The second argument to definductor must be nil or the name you ~
         choose to give to the inductor function generated for ~x0 but ~x1 is ~
         not a symbol."
          fn
          inductor-fn))
      (t (er-let* ((measures (if measure
               (translate-measures (list measure)
                 t
                 'definductor
                 wrld
                 state)
               (value '(nil)))))
          (let* ((tmeasure (car measures)))
            (mv-let (erp encap)
              (make-inductor-defun-and-rule fn
                inductor-fn
                tmeasure
                well-founded-relation
                ruler-extenders
                hints
                wrld)
              (cond (erp (er soft
                    'definductor
                    "We cannot construct an inductor for ~x0 because ~@1"
                    fn
                    erp))
                (t (value encap))))))))))

definductor-fnfunction

(defun definductor-fn
  (fn inductor-fn
    measure
    well-founded-relation
    ruler-extenders
    hints)
  (declare (xargs :mode :logic :guard t))
  `(definductor-fn1 ',FN
    ',INDUCTOR-FN
    ',MEASURE
    ',WELL-FOUNDED-RELATION
    ',RULER-EXTENDERS
    ',HINTS
    state))

definductormacro

(defmacro definductor
  (fn &key
    inductor-fn
    measure
    well-founded-relation
    ruler-extenders
    hints)
  `(with-output :off (warning warning!
      observation
      prove
      proof-builder
      event
      history
      summary
      proof-tree)
    :stack :push :gag-mode nil
    (make-event (with-output :stack :pop ,(DEFINDUCTOR-FN FN INDUCTOR-FN MEASURE WELL-FOUNDED-RELATION RULER-EXTENDERS
  HINTS))
      :on-behalf-of :quiet! :check-expansion t)))