tau-characterization

(defun max-list
  (x)
  (if (atom x)
    -1
    (max (car x) (max-list (cdr x)))))

(defun find-x-terms-=-depth
  (terms x depth)
  "find terms having x at given depth"
  (if (endp terms)
    'nil
    (let ((d (depth-var x (car terms))))
      (if (and (natp d)
          (= depth d))
        (cons (car terms)
          (find-x-terms-=-depth (cdr terms)
            x
            depth))
        (find-x-terms-=-depth (cdr terms)
          x
          depth)))))

(defun find-x-terms->=-depth
  (terms x depth)
  "find terms having x at greater than or equal to given depth"
  (if (endp terms)
    'nil
    (let ((d (depth-var x (car terms))))
      (if (and (natp d)
          (<= depth d))
        (cons (car terms)
          (find-x-terms->=-depth (cdr terms)
            x
            depth))
        (find-x-terms->=-depth (cdr terms)
          x
          depth)))))

(defun union-lst
  (lsts)
  (declare (xargs :mode :logic :guard (true-list-listp lsts)))
  (if (endp lsts)
    nil
    (union-equal (car lsts)
      (union-lst (cdr lsts)))))

(defun recognizer-call-with-var
  (call var c)
  (case-match call
    ((p x) (and (equal x var)
        (get-conx-name p c)
        call))
    (& nil)))

(defun dumber-negate-lit
  (term)
  (cond ((variablep term) (fcons-term* 'not term))
    ((fquotep term) (cond ((equal term nil) t) (t nil)))
    ((eq (ffn-symb term) 'not) (fargn term 1))
    (t (fcons-term* 'not term))))

(defun break-one-destructor-nest
  (es x c)
  (b* ((recog-call (governing-recognizer-call-with-var es
         x
         c)) ((unless recog-call) (mv nil nil es nil))
      (es (remove-equal recog-call es))
      (recog (ffn-symb recog-call))
      (conx (get-conx-name recog c))
      (dest-pred-alist (get2 conx :dest-pred-alist c))
      (k (len dest-pred-alist))
      (dex-calls (list-up-lists (strip-cars dest-pred-alist)
          (make-list k :initial-element x)))
      (x1--xk (numbered-vars x k))
      (cons-x (cons conx x1--xk))
      (sub-alist (pairlis$ dex-calls x1--xk))
      (es (sublis-expr-lst sub-alist es))
      (x-terms (find-x-terms->=-depth es x 0)))
    (mv cons-x
      x1--xk
      es
      x-terms)))

(defun tau-rule-and-terms=>px
  (es p x c)
  (b* ((fes (find-x-terms->=-depth es x 2)))
    (if (> (len fes) 1)
      (b* (((mv cons-x
            x1--xk
            dest-es
            remaining-x-es) (break-one-destructor-nest es
             x
             c)))
        (if cons-x
          (cond (remaining-x-es (prog2$ (cw? nil
                  "~| Presence of ~x0 precludes a tau characterization of ~x1~%"
                  remaining-x-es
                  p)
                "Multiple sig terms i.e. (P1 (f x1 ...)) OR (P2 (f x1 ...))
 not allowed in conclusion of signature rule."))
            ((nested-functional-terms-with-vars-p dest-es
               x1--xk) (prog2$ (cw? nil
                  "~| Nested destructors precludes a tau characterization of ~x0~%"
                  p)
                "Nesting i.e. (P (f ... (g x1 ...) ...) not allowed in conclusion of signature rule"))
            (t `(implies (and . ,DEFDATA::DEST-ES)
                (,DEFDATA::P ,DEFDATA::CONS-X))))
          (prog2$ (cw? nil
              "~| Non-dest-eliminable AND nest ~x0 precludes a tau characterization of ~x1~%"
              fes
              p)
            "Illegal tau rule")))
      (if fes
        (if (= (depth-var x (car fes)) 2)
          `(implies (and . ,(CONS (DEFDATA::DUMBER-NEGATE-LIT (LIST DEFDATA::P DEFDATA::X))
       (REMOVE (CAR DEFDATA::FES) DEFDATA::ES)))
            ,(DEFDATA::DUMBER-NEGATE-LIT (CAR DEFDATA::FES)))
          "Nesting i.e. (P (f ... (g x1 ...) ...) not allowed in conclusion of signature rule")
        `(implies (and . ,DEFDATA::ES)
          (,DEFDATA::P ,DEFDATA::X))))))

(defun tau-rules-form=>px
  (e px
    new-fns-and-args
    ctx
    c
    wrld)
  (b* (((mv erp te) (pseudo-translate e
         new-fns-and-args
         wrld)) ((when erp) (prog2$ (cw "~| ~x0: Error in translate: ~x1"
            ctx
            te)
          (list "Error in translate in tau-rules => direction")))
      (te (expand-lambda te))
      (conjunctive-clauses (cnf-dnf t te nil))
      (rules (tau-rules-dnf=>px conjunctive-clauses
          px
          c)))
    rules))

(defun tau-rules-px=>or-terms
  (terms p x)
  (if (consp terms)
    (b* ((fes2 (find-x-terms->=-depth terms x 2)))
      (cond ((null fes2) (cond ((endp (cdr terms)) `((implies (,DEFDATA::P ,DEFDATA::X)
                 ,(CAR DEFDATA::TERMS))))
            ((endp (cddr terms)) `((implies (and (,DEFDATA::P ,DEFDATA::X) (not ,(CAR DEFDATA::TERMS)))
                 ,(CADR DEFDATA::TERMS)) (implies (and (,DEFDATA::P ,DEFDATA::X) (not ,(CADR DEFDATA::TERMS)))
                  ,(CAR DEFDATA::TERMS))))
            ((endp (cdddr terms)) `((implies (and (,DEFDATA::P ,DEFDATA::X)
                   (not ,(FIRST DEFDATA::TERMS))
                   (not ,(SECOND DEFDATA::TERMS)))
                 ,(THIRD DEFDATA::TERMS)) (implies (and (,DEFDATA::P ,DEFDATA::X)
                    (not ,(FIRST DEFDATA::TERMS))
                    (not ,(THIRD DEFDATA::TERMS)))
                  ,(SECOND DEFDATA::TERMS))
                (implies (and (,DEFDATA::P ,DEFDATA::X)
                    (not ,(SECOND DEFDATA::TERMS))
                    (not ,(THIRD DEFDATA::TERMS)))
                  ,(FIRST DEFDATA::TERMS))))
            (t `((implies (and . ,(CONS (LIST DEFDATA::P DEFDATA::X)
       (DEFDATA::DUMBER-NEGATE-LIT-LST (CDR DEFDATA::TERMS))))
                 ,(CAR DEFDATA::TERMS))))))
        ((not (consp (cdr fes2))) (if (= (depth-var x (car fes2)) 2)
            `((implies (and . ,(CONS (LIST DEFDATA::P DEFDATA::X)
       (DEFDATA::DUMBER-NEGATE-LIT-LST
        (DEFDATA::SET-DIFFERENCE-EQUAL DEFDATA::TERMS DEFDATA::FES2))))
               ,(CAR DEFDATA::FES2)))
            (list "Nesting i.e. (P (f ... (g x1 ...) ...) not allowed in conclusion of signature rule")))
        (t (list "Multiple sig terms i.e. (P1 (f x1 ...)) OR (P2 (f x1 ...))
 not allowed in conclusion of signature rule"))))
    (list "Impossible: Empty clause")))

(defun get-eq-constant
  (term wrld)
  "if term is a equality-with-constant, then return (equal e evg)"
  (b* (((mv &
        recog
        e
        &) (tau-like-term term :same-var wrld)))
    (if (and (consp recog) (null (cdr recog)))
      `(equal ,DEFDATA::E ,(CAR DEFDATA::RECOG))
      nil)))

(defun get-eq-constant-dont-change
  (term wrld)
  "if term is a equality-with-constant, then return (equal e evg)"
  (b* (((mv &
        recog
        &
        &) (tau-like-term term :same-var wrld)))
    (if (and (consp recog) (null (cdr recog)))
      term
      nil)))

(defun tau-rule-px-recog=>prod
  (and-terms p
    x
    c
    wrld)
  (declare (ignorable p wrld))
  (b* ((recog-exp (governing-recognizer-call-with-var and-terms
         x
         c)) (recog-exp (and recog-exp
          (proper-symbolp (car recog-exp))
          (or (and (subtype-p (car recog-exp)
                'atom
                wrld)
              (list 'atom (cadr recog-exp)))
            recog-exp)))
      ((unless recog-exp) nil)
      (dterms (remove-equal recog-exp
          and-terms)))
    (if (find-x-terms->=-depth dterms
        x
        3)
      (list "Nesting i.e. (P (f ... (g x1 ...) ...) not allowed in conclusion of signature rule.")
      `((implies (and (,DEFDATA::P ,DEFDATA::X) ,DEFDATA::RECOG-EXP)
         (and . ,DEFDATA::DTERMS))))))

(defun tau-rule-px-=>eq-nil-hack
  (and-terms p x wrld)
  (b* ((eq-exp (get-first-eq-constant-dont-change and-terms
         wrld)) ((unless eq-exp) nil)
      (recog-exp (if (or (and (equal (second eq-exp) ''nil)
              (equal (third eq-exp) x))
            (and (equal (second eq-exp) 'nil)
              (equal (third eq-exp) x))
            (and (equal (second eq-exp) x)
              (equal (third eq-exp) ''nil))
            (and (equal (second eq-exp) x)
              (equal (third eq-exp) 'nil)))
          (list 'endp x)
          nil))
      ((unless recog-exp) nil))
    `((implies (and (,DEFDATA::P ,DEFDATA::X) ,DEFDATA::RECOG-EXP)
       ,DEFDATA::EQ-EXP))))

(defun recognizer-call
  (call c wrld)
  (declare (ignorable wrld))
  (case-match call
    ((p x) (and (proper-symbolp x)
        (or (get-conx-name p c))
        call))
    (& nil)))

(defun disjoint-clause2-p
  (cl1 cl2 c wrld)
  (b* ((p1x (governing-recognizer-call cl1
         c
         wrld)) (p2x (governing-recognizer-call cl2
          c
          wrld))
      (evg1-term (get-first-eq-constant cl1 wrld))
      (evg2-term (get-first-eq-constant cl2 wrld))
      (evg1 (and evg1-term (third evg1-term)))
      (evg2 (and evg2-term (third evg2-term))))
    (cond ((and evg1-term evg2-term) (not (equal evg1 evg2)))
      ((and evg2-term
         p1x
         (equal (second p1x) (second evg2-term))) (if (function-symbolp (car p1x) wrld)
          (b* (((mv erp res) (ev-fncall-w (car p1x)
                 (list evg2)
                 wrld
                 nil
                 nil
                 t
                 t
                 nil)))
            (and (not erp) (not res)))
          t))
      ((and evg1-term
         p2x
         (equal (second p2x) (second evg1-term))) (if (function-symbolp (car p2x) wrld)
          (b* (((mv erp res) (ev-fncall-w (car p2x)
                 (list evg1)
                 wrld
                 nil
                 nil
                 t
                 t
                 nil)))
            (and (not erp) (not res)))
          t))
      ((and p1x p2x) (if (and (function-symbolp (car p1x) wrld)
            (function-symbolp (car p2x) wrld))
          (disjoint-p (car p1x)
            (car p2x)
            wrld)
          t))
      (t nil))))

(defun mutually-disjoint-clauses-p
  (clauses c wrld)
  (if (or (endp clauses) (endp (cdr clauses)))
    t
    (and (clause-disjoint-with-clauses-p (car clauses)
        (cdr clauses)
        c
        wrld)
      (mutually-disjoint-clauses-p (cdr clauses)
        c
        wrld))))

(defun tau-rules-px=>def/conjunctive
  (clauses p
    x
    c
    wrld)
  (b* ((prod-clauses (filter-prods clauses
         c
         wrld)) (base-clauses (set-difference-equal clauses
          prod-clauses))
      (base-terms (strip-cars base-clauses))
      (prod-recogs (governing-recognizer-calls prod-clauses
          c
          wrld))
      (neg-prod-recogs (negate-terms prod-recogs)))
    (if (= (len base-terms) 1)
      `((implies (and (,DEFDATA::P ,DEFDATA::X) ,@DEFDATA::NEG-PROD-RECOGS)
         ,(CAR DEFDATA::BASE-TERMS)))
      `((implies (and (,DEFDATA::P ,DEFDATA::X) ,@DEFDATA::NEG-PROD-RECOGS)
         (or . ,DEFDATA::BASE-TERMS))))))

(defun shallow-prod-p
  (texp c)
  (and (consp texp)
    (assoc-equal (car texp) c)))

(defun shallow-union-of-prods-p
  (texp c)
  (and (consp texp)
    (eq (car texp) 'or)
    (b* ((targs (cdr texp)) (prods (filter-shallow-prods targs c))
        (rest (set-difference-equal targs
            prods)))
      (and (consp prods)
        (var-or-quoted-listp rest)))))

(defun tau-rules-px=>form
  (form px
    s
    new-fns-and-args
    ctx
    c
    wrld)
  (b* (((mv erp te) (pseudo-translate form
         new-fns-and-args
         wrld)) ((when erp) (prog2$ (cw "~| ~x0: Error in translate: ~x1"
            ctx
            te)
          (list "Error in translate in tau-rules => direction")))
      (te (expand-lambda te)))
    (if (shallow-union-of-prods-p s c)
      (b* ((conj-clauses (cnf-dnf t te nil)))
        (if (mutually-disjoint-clauses-p conj-clauses
            c
            wrld)
          (append (tau-rules-px=>eq-constants conj-clauses
              (car px)
              (cadr px)
              wrld)
            (tau-rules-px=>def/conjunctive conj-clauses
              (car px)
              (cadr px)
              c
              wrld)
            (tau-rules-px=>sop conj-clauses
              (car px)
              (cadr px)
              c
              wrld))
          (list "Unable to characterize (using tau rules) a non-disjoint union type")))
      (b* ((clauses (cnf-dnf t te t)))
        (tau-rules-px=>cnf clauses px)))))

(defun mv-messages-rule
  (rules)
  (b* ((msgs (filter-strings rules)) (rules (set-difference-equal rules msgs)))
    (cond ((and (consp rules) (consp (cdr rules))) (mv msgs (cons 'and rules)))
      ((consp rules) (mv msgs (car rules)))
      (t (mv msgs nil)))))

(defun all-1-arity-fns1
  (conx-al)
  (b* ((dest-pred-alist (get1 :dest-pred-alist conx-al)) (recog (get1 :recog conx-al)))
    (cons recog
      (strip-cars dest-pred-alist))))

(defun all-conx-fns-args1
  (cx x)
  (b* (((cons conx conx-al) cx) (arity (get1 :arity conx-al))
      (v1--vk (numbered-vars x arity)))
    (cons conx v1--vk)))

(defun extend-wrld-with-fn-args-list-with-tau-pair
  (fn-args-lst wrld)
  (cond ((endp fn-args-lst) wrld)
    (t (let ((fn (caar fn-args-lst)))
        (putprop fn
          'tau-pair
          (if (is-allp-alias fn wrld)
            (cons nil fn)
            (cons 0 fn))
          (extend-wrld-with-fn-args-list-with-tau-pair (cdr fn-args-lst)
            wrld))))))

(defun chk-acceptable-tau-rule
  (term fn-args-lst wrld)
  (let ((pairs (split-on-conjoined-disjunctions-in-hyps-of-pairs (strip-force-and-case-split-in-hyps-of-pairs (unprettyify term)))) (wrld1 (extend-wrld-with-fn-args-list-with-tau-pair fn-args-lst
          wrld)))
    (acceptable-tau-rulesp :all pairs wrld1)))

(defun tau-characterization-events1
  (pair top-kwd-alist
    ctx
    wrld)
  (b* (((cons name a) pair) ((assocs ndef
         n
         new-constructors
         new-types
         kwd-alist) a)
      (new-constructors (delete2-key :field-pred-alist new-constructors))
      (c (append new-constructors
          (table-alist 'data-constructor-table
            wrld)))
      (m (append new-types
          (table-alist 'type-metadata-table
            wrld)))
      (a (table-alist 'type-alias-table
          wrld))
      (b (table-alist 'builtin-combinator-table
          wrld))
      (kwd-alist (append kwd-alist top-kwd-alist))
      (pkg (get1 :current-package kwd-alist))
      (avoid-lst (append (forbidden-names)
          (strip-cars n)))
      (v (fix-intern$ "V" pkg))
      (x (fix-intern$ "X" pkg))
      (xvar (if (member-eq v avoid-lst)
          v
          (generate-variable v
            avoid-lst
            nil
            nil
            wrld)))
      (pred-body (make-pred-i ndef
          xvar
          kwd-alist
          a
          m
          c
          b
          wrld))
      (pred-name (predicate-name name
          a
          m))
      (px `(,DEFDATA::PRED-NAME ,DEFDATA::XVAR))
      (mon-fns (all-1-arity-fns new-constructors))
      (all-conx-fns-args (all-conx-fns-args new-constructors
          x))
      (current-preds (predicate-names (strip-cars new-types)
          a
          new-types))
      (new-fns-and-args (append (list-up-lists current-preds
            (make-list (len current-preds)
              :initial-element x))
          (and new-constructors all-conx-fns-args)
          (and new-constructors
            (list-up-lists mon-fns
              (make-list (len mon-fns)
                :initial-element x)))))
      ((mv msgs<= rule-=>-px) (mv-messages-rule (tau-rules-form=>px pred-body
            px
            new-fns-and-args
            ctx
            c
            wrld)))
      ((mv msgs=> rule-px-=>) (mv-messages-rule (tau-rules-px=>form pred-body
            px
            ndef
            new-fns-and-args
            ctx
            c
            wrld)))
      (without-names-ndef (remove-names ndef))
      (constituent-tnames (set-difference-eq (all-vars without-names-ndef)
          (strip-cars new-types)))
      (constituent-preds (predicate-names constituent-tnames))
      (disabled (runes-to-be-disabled constituent-preds
          wrld))
      ((mv erp term-=>-px) (pseudo-translate rule-=>-px
          new-fns-and-args
          wrld))
      ((when erp) (er hard?
          ctx
          "~| Bad translate ~x0.~%"
          rule-=>-px))
      ((mv erp term-px-=>) (pseudo-translate rule-px-=>
          new-fns-and-args
          wrld))
      ((when erp) (er hard?
          ctx
          "~| Bad translate ~x0.~%"
          rule-px-=>))
      (rule-=>-px-tau-acceptable-p (chk-acceptable-tau-rule term-=>-px
          new-fns-and-args
          wrld))
      (rule-px-=>-tau-acceptable-p (chk-acceptable-tau-rule term-px-=>
          new-fns-and-args
          wrld))
      (unacceptable-tau-rule-msg "The formula fails to fit any of the forms for acceptable :TAU-SYSTEM rules.")
      (msgs=> (remove-duplicates-equal (append (and (not rule-=>-px-tau-acceptable-p)
              (list unacceptable-tau-rule-msg))
            msgs=>)))
      (msgs<= (remove-duplicates-equal (append (and (not rule-px-=>-tau-acceptable-p)
              (list unacceptable-tau-rule-msg))
            msgs<=)))
      (?recp (get1 :recp kwd-alist))
      (yes (get1 :print-commentary kwd-alist)))
    (append (and msgs<=
        `((commentary ,DEFDATA::YES
           "~| ~x0 <= body -- not complete. ~|Reasons: ~x1 ~%"
           ',DEFDATA::PX
           ',DEFDATA::MSGS<=)))
      (and msgs=>
        `((commentary ,DEFDATA::YES
           "~| ~x0 => body -- not complete. ~|Reasons: ~x1 ~%"
           ',DEFDATA::PX
           ',DEFDATA::MSGS=>)))
      (and (not msgs=>)
        (not msgs<=)
        rule-px-=>-tau-acceptable-p
        rule-px-=>-tau-acceptable-p
        `((commentary ,DEFDATA::YES
           "~|Defdata/Note: ~x0 relatively complete for Tau.~%"
           ',(CAR DEFDATA::PX))))
      (and rule-=>-px
        `((defthm ,(SYMBOL-FNS::PREFIX 'DEFDATA::DEF 'DEFDATA::=> DEFDATA::NAME)
           ,DEFDATA::RULE-=>-PX
           :hints (("Goal" :in-theory (e/d (,(CAR DEFDATA::PX))
                (,@DEFDATA::DISABLED ,@(DEFDATA::STRIP-CARS DEFDATA::NEW-CONSTRUCTORS)))))
           :rule-classes (,@(AND DEFDATA::RULE-=>-PX-TAU-ACCEPTABLE-P (LIST :TAU-SYSTEM)) :rewrite))))
      (and rule-px-=>
        `((defthm ,(SYMBOL-FNS::SUFFIX DEFDATA::NAME 'DEFDATA::=> 'DEFDATA::DEF)
           ,DEFDATA::RULE-PX-=>
           :hints (("Goal" :in-theory (e/d (,(CAR DEFDATA::PX)) (,@DEFDATA::DISABLED))))
           :rule-classes (,@(AND DEFDATA::RULE-PX-=>-TAU-ACCEPTABLE-P '(:TAU-SYSTEM)) (:forward-chaining :trigger-terms (,DEFDATA::PX)))))))))

(defun tau-characterization-events
  (ps kwd-alist wrld)
  (cons `(commentary ,(DEFDATA::GET1 :PRINT-COMMENTARY DEFDATA::KWD-ALIST)
      "~| Tau characterization events...~%")
    (tau-characterization-events0 ps
      kwd-alist
      wrld)))