top

(in-package "PRETTYGOALS")

(include-book "doc")

(include-book "std/util/bstar" :dir :system)

(include-book "std/strings/defs-program" :dir :system)

(include-book "defsort/defsort" :dir :system)

(include-book "defsort/duplicated-members" :dir :system)

(include-book "misc/total-order" :dir :system)

(include-book "std/util/define" :dir :system)

(include-book "std/util/defines" :dir :system)

(include-book "tools/include-raw" :dir :system)

(program)

(defines collect-simple-accessor-calls
  (define collect-simple-accessor-calls
    (x)
    (cond ((or (atom x) (eq (car x) 'quote)) nil)
      ((symbolp (first x)) (if (and (consp (cdr x))
            (not (cddr x))
            (substrp "->" (symbol-name (first x)))
            (legal-variablep (second x)))
          (list x)
          (collect-simple-accessor-calls-list (cdr x))))
      (t nil)))
  (define collect-simple-accessor-calls-list
    (x)
    (if (atom x)
      nil
      (append (collect-simple-accessor-calls (car x))
        (collect-simple-accessor-calls-list (cdr x))))))

(defines apply-simple-accessors-subst
  (define apply-simple-accessors-subst
    (x (subst alistp))
    (cond ((or (atom x) (eq (car x) 'quote)) x)
      ((symbolp (first x)) (if (and (consp (cdr x))
            (not (cddr x))
            (substrp "->" (symbol-name (first x)))
            (legal-variablep (second x)))
          (b* ((replacement (cdr (assoc-equal x subst))))
            (or replacement
              (raise "No replacement for ~x0?"
                x)))
          (cons (car x)
            (apply-simple-accessors-subst-list (cdr x)
              subst))))
      (t x)))
  (define apply-simple-accessors-subst-list
    (x (subst alistp))
    (if (atom x)
      x
      (cons (apply-simple-accessors-subst (car x)
          subst)
        (apply-simple-accessors-subst-list (cdr x)
          subst)))))

(define deconstruct-simple-accessor-calls
  (calls)
  (b* (((when (atom calls)) (mv nil nil)) ((mv binders-alist
         replace-alist) (deconstruct-simple-accessor-calls (cdr calls)))
      ((list foo->bar var) (car calls))
      (str (symbol-name foo->bar))
      (idx (strpos "->" str))
      (foo (intern-in-package-of-symbol (subseq str 0 idx)
          foo->bar))
      (var.bar (intern-in-package-of-symbol (cat (symbol-name var)
            "."
            (subseq str (+ 2 idx) nil))
          foo->bar))
      (bind1 (cons var
          (list foo var)))
      (repl1 (cons (car calls) var.bar)))
    (mv (cons bind1 binders-alist)
      (cons repl1 replace-alist))))

(define my-count-fncalls
  (x)
  (cond ((or (atom x) (eq (car x) 'quote)) 0)
    ((eq (car x) 'not) (my-count-fncalls (cdr x)))
    ((symbolp (car x)) (+ 1 (my-count-fncalls (cdr x))))
    (t (+ (my-count-fncalls (car x))
        (my-count-fncalls (cdr x))))))

(define my-count-vars
  (x)
  (cond ((atom x) 1)
    ((eq (car x) 'quote) 0)
    ((symbolp (car x)) (my-count-vars (cdr x)))
    (t (+ (my-count-vars (car x))
        (my-count-vars (cdr x))))))

(define my-term<
  (x y)
  (b* (((when (atom x)) (if (atom y)
         (<< x y)
         t)) ((when (atom y)) nil)
      ((when (eq (car x) 'quote)) (if (eq (car y) 'quote)
          (<< x y)
          t))
      ((when (eq (car y) 'quote)) nil)
      (xcalls (my-count-fncalls x))
      (ycalls (my-count-fncalls y))
      ((when (< xcalls ycalls)) t)
      ((when (< ycalls xcalls)) nil)
      (xvars (my-count-vars x))
      (yvars (my-count-vars y))
      ((when (< xvars yvars)) t)
      ((when (< yvars xvars)) t))
    (<< x y)))

(defsort my-term-sort
  :compare< my-term<)

(define reorder-toplevel-hyps
  (x)
  (if (and (consp x)
      (eq (first x) 'implies)
      (consp (cdr x))
      (consp (cddr x))
      (not (cdddr x))
      (consp (second x))
      (equal (car (second x)) 'and))
    (list 'implies
      (cons 'and
        (my-term-sort (cdr (second x))))
      (third x))
    x))

(define keep-from-alist
  (keys alist)
  (cond ((atom alist) nil)
    ((member (caar alist) keys) (cons (car alist)
        (keep-from-alist keys
          (cdr alist))))
    (t (keep-from-alist keys
        (cdr alist)))))

(define type-check-messages
  (binders-alist)
  (b* ((vars (strip-cars binders-alist)) (dupes (duplicated-members vars))
      ((unless dupes) nil))
    (list (cat "-----------------------------------------------------------------
     WARNING: type confusion -- look above at "
        (join (symbol-list-names dupes) ", ")
        "!  Typo in theorem?
  -----------------------------------------------------------------"))))

(define b*ify-simple-accessors
  (x)
  (b* ((calls (collect-simple-accessor-calls x)) ((unless calls) (reorder-toplevel-hyps x))
      (calls (remove-duplicates-equal calls))
      ((mv binders-alist
         replace-alist) (deconstruct-simple-accessor-calls calls))
      (binders-alist (remove-duplicates-equal binders-alist))
      (rewritten-x (apply-simple-accessors-subst x
          replace-alist)))
    `(b* ,(PRETTYGOALS::PAIRLIS$ (PRETTYGOALS::STRIP-CDRS PRETTYGOALS::BINDERS-ALIST)
  NIL)
      ,@(PRETTYGOALS::TYPE-CHECK-MESSAGES PRETTYGOALS::BINDERS-ALIST)
      ,(PRETTYGOALS::REORDER-TOPLEVEL-HYPS PRETTYGOALS::REWRITTEN-X))))

(defstub post-untranslate-hook
  (x)
  t)

(defttag :prettygoals)

(include-raw "prettygoals-raw.lsp")

(defmacro set-pretty-goals
  (enabled-p)
  (if enabled-p
    `(progn (defttag :prettygoals)
      (defattach (post-untranslate-hook b*ify-simple-accessors)
        :skip-checks t))
    `(defattach post-untranslate-hook identity)))

(set-pretty-goals t)