enumerators-gen

(in-package "DEFDATA")

(include-book "defdata-util")

(include-book "data-structures/utilities" :dir :system)

(defun forbidden-names-enum
  nil
  (declare (xargs :guard t))
  '(_seed _v _i _choice))

(verify-guards forbidden-names-enum)

(defattach forbidden-names
  forbidden-names-enum)

(defmacro split
  (k i)
  "another name for defdata::split-nat"
  `(split-nat ,DEFDATA::K ,DEFDATA::I))

(defmacro switch
  (k i)
  `(weighted-switch-nat ',(CONS 1 (MAKE-LIST (1- DEFDATA::K) :INITIAL-ELEMENT 5))
    ,DEFDATA::I))

(defmacro make-enum-i...
  (s x)
  `(make-enum-i ,DEFDATA::S
    ,DEFDATA::X
    kwd-alist
    m
    c
    b
    wrld))

(defmacro make-enum-is...
  (ss xs)
  `(make-enum-is ,DEFDATA::SS
    ,DEFDATA::XS
    kwd-alist
    m
    c
    b
    wrld))

(program)

(mutual-recursion (defun make-enum-i
    (s i
      kwd-alist
      m
      c
      b
      wrld)
    "Make enumerator interpretation for core defdata exp s.
 where
 i is the name of the current indicial argument (dont confuse with an integer)
 kwd-alist gives some defaults.
 M is type metadata table + some basic info for the clique of types being defined.
 C is the constructor table + some basic info for new constructors.
 B is the builtin combinator table."
    (cond ((possible-constant-value-p s) (if (quotep s)
          s
          (list 'quote s)))
      ((proper-symbolp s) (if (assoc-eq s m)
          `(,(DEFDATA::GET2 DEFDATA::S :ENUMERATOR DEFDATA::M) ,DEFDATA::I)
          s))
      ((not (true-listp s)) (make-enum-i (cdr s)
          i
          kwd-alist
          m
          c
          b
          wrld))
      ((assoc-eq (car s) b) (b* ((enum-i-fn (get2 (car s) :enum-i b)) (k (len (cdr s))))
          (if enum-i-fn
            (funcall-w enum-i-fn
              (list i s)
              'make-enum-i
              wrld)
            (if (eq (car s) 'or)
              `(mv-let (_choice ,DEFDATA::I)
                (switch-nat ,DEFDATA::K ,DEFDATA::I)
                (declare (ignorable ,DEFDATA::I))
                (case _choice . ,(DEFDATA::LIST-UP-LISTS (DEFDATA::MAKE-NUMLIST-FROM 0 DEFDATA::K)
  (DEFDATA::MAKE-ENUM-IS... (CDR DEFDATA::S)
   (MAKE-LIST DEFDATA::K :INITIAL-ELEMENT DEFDATA::I)))))
              nil))))
      ((assoc-eq (car s) c) (b* ((k (len (cdr s))) (pkg (get1 :current-package kwd-alist))
            (vari (fix-intern$ "I" pkg))
            (i1--ik (numbered-vars vari k))
            (enum-arg-exprs (make-enum-is... (remove-names-lst (cdr s))
                i1--ik))
            (binding (bind-names-vals (cdr s)
                enum-arg-exprs))
            (?satisfies-exprs (get-all :satisfies kwd-alist))
            (rst (make-enum-is... (keep-names-lst (cdr s))
                i1--ik)))
          `(b* (((list . ,DEFDATA::I1--IK) (split-nat ,DEFDATA::K ,DEFDATA::I)))
            ,(IF DEFDATA::BINDING
     `(DEFDATA::B* ,DEFDATA::BINDING (,(CAR DEFDATA::S) . ,DEFDATA::RST))
     `(,(CAR DEFDATA::S) . ,DEFDATA::RST)))))
      (t `(,(CAR DEFDATA::S) . ,(DEFDATA::MAKE-ENUM-IS... (CDR DEFDATA::S)
  (MAKE-LIST (DEFDATA::LEN (CDR DEFDATA::S)) :INITIAL-ELEMENT DEFDATA::I))))))
  (defun make-enum-is
    (texps is
      kwd-alist
      m
      c
      b
      wrld)
    (declare (ignorable kwd-alist))
    (if (endp texps)
      'nil
      (b* ((car-enum-i (make-enum-i... (car texps)
             (car is))))
        (and car-enum-i
          (cons car-enum-i
            (make-enum-is... (cdr texps)
              (cdr is))))))))

(defun make-enum-declare-forms
  (ivar kwd-alist)
  (b* ((guard-lambda (get1 :enum-guard kwd-alist)) (actuals (list ivar))
      (?term-method (get1 :termination-method kwd-alist))
      (measure-decl-forms nil)
      (guard-decl-forms (and guard-lambda
          `((declare (xargs :mode :program :guard ,(DEFDATA::EXPAND-LAMBDA (CONS DEFDATA::GUARD-LAMBDA DEFDATA::ACTUALS))))))))
    (append measure-decl-forms
      guard-decl-forms)))

(defun enum-event
  (p top-kwd-alist wrld)
  "make a enumerator defun event."
  (b* (((cons name a) p) ((assocs ndef
         n
         new-constructors
         new-types
         kwd-alist) a)
      (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)))
      (i (fix-intern$ "I" pkg))
      (ivar (if (member-eq i avoid-lst)
          i
          (generate-variable i
            avoid-lst
            nil
            nil
            wrld)))
      (enum-body (make-enum-i ndef
          ivar
          kwd-alist
          m
          c
          b
          wrld))
      (enum-decls (make-enum-declare-forms ivar
          kwd-alist)))
    `(defun ,(DEFDATA::ENUMERATOR-NAME DEFDATA::NAME DEFDATA::A DEFDATA::M)
      (,DEFDATA::IVAR)
      ,@DEFDATA::ENUM-DECLS
      ,DEFDATA::ENUM-BODY)))

(defloop enum-events
  (ps kwd-alist wrld)
  (for ((p in ps))
    (collect (enum-event p
        kwd-alist
        wrld))))

(defun enumerator-events
  (d kwd-alist wrld)
  (b* ((enum-events (enum-events d
         kwd-alist
         wrld)) (p? (get1 :print-commentary kwd-alist)))
    (if (consp (cdr d))
      `((commentary ,DEFDATA::P?
         "~| Enumerator events...~%") (mutual-recursion ,@DEFDATA::ENUM-EVENTS))
      (cons `(commentary ,DEFDATA::P?
          "~| Enumerator events...~%")
        enum-events))))

(defun mv2-let-seq
  (bs vals body)
  (if (endp bs)
    body
    (list 'mv-let
      (car bs)
      (car vals)
      (mv2-let-seq (cdr bs)
        (cdr vals)
        body))))

(defloop bind-mv2-names-enum/acc-calls
  (texps vals
    temp-names
    acc-exp)
  "b* mv binding for each name decl texp -> corresponding val, albeit when not named, take a temp name"
  (for ((texp in texps) (val in vals)
      (nm in temp-names))
    (collect (if (named-defdata-exp-p texp)
        (list (list 'mv (car texp) acc-exp)
          val)
        (list (list 'mv nm acc-exp)
          val)))))

(mutual-recursion (defun recursive-refs
    (texp new-names)
    (cond ((possible-constant-value-p texp) 0)
      ((proper-symbolp texp) (if (member-eq texp new-names)
          1
          0))
      ((not (true-listp texp)) (if (member-equal (cdr texp)
            new-names)
          1
          0))
      (t (recursive-refs-lst (cdr texp)
          new-names))))
  (defun recursive-refs-lst
    (texps new-names)
    (if (endp texps)
      0
      (+ (recursive-refs (car texps)
          new-names)
        (recursive-refs-lst (cdr texps)
          new-names)))))

(defun has-recursive-reference-p
  (texp new-names)
  (> (recursive-refs texp new-names)
    0))

(defloop collect-base-cases
  (texps new-names)
  (for ((texp in texps))
    (append (and (not (has-recursive-reference-p texp
            new-names))
        (list texp)))))

(defloop collect-rec-cases
  (texps new-names)
  (for ((texp in texps))
    (append (and (has-recursive-reference-p texp
          new-names)
        (list texp)))))

(defun bound-seeds-to-recursive-calls
  (i i1--ik
    texps
    new-names)
  (if (endp texps)
    'nil
    (b* ((i_current (car i1--ik)) (texp (car texps)))
      (cons (if (has-recursive-reference-p texp
            new-names)
          `(if (or (zp ,DEFDATA::I_CURRENT)
              (< ,DEFDATA::I_CURRENT ,DEFDATA::I))
            ,DEFDATA::I_CURRENT
            (1- ,DEFDATA::I_CURRENT))
          i_current)
        (bound-seeds-to-recursive-calls i
          (cdr i1--ik)
          (cdr texps)
          new-names)))))

(defloop recursive-p-marked-lst
  (texps new-names)
  (for ((texp in texps))
    (collect (has-recursive-reference-p texp
        new-names))))

(defun uniformly-partition-size-binding-aux
  (svar comp-svars
    k
    rec-p-lst
    texps
    m)
  (if (endp rec-p-lst)
    'nil
    (if (car rec-p-lst)
      (cons (if (> k 1)
          `((mv ,(CAR DEFDATA::COMP-SVARS)
             (the (unsigned-byte 63) _seed)) (genrandom-seed (1+ (nfix ,DEFDATA::SVAR))
              _seed))
          `((mv ,(CAR DEFDATA::COMP-SVARS)
             (the (unsigned-byte 63) _seed)) (mv ,DEFDATA::SVAR _seed)))
        (uniformly-partition-size-binding-aux `(- ,DEFDATA::SVAR ,(CAR DEFDATA::COMP-SVARS))
          (cdr comp-svars)
          (1- k)
          (cdr rec-p-lst)
          (cdr texps)
          m))
      (cons `((mv ,(CAR DEFDATA::COMP-SVARS)
           (the (unsigned-byte 63) _seed)) ,(IF (AND (DEFDATA::PROPER-SYMBOLP (CAR DEFDATA::TEXPS))
          (DEFDATA::ASSOC-EQ (CAR DEFDATA::TEXPS) DEFDATA::M))
     `(DEFDATA::CHOOSE-SIZE
       ,(DEFDATA::GET2 (CAR DEFDATA::TEXPS) :MIN-REC-DEPTH DEFDATA::M)
       ,(DEFDATA::GET2 (CAR DEFDATA::TEXPS) :MAX-REC-DEPTH DEFDATA::M)
       DEFDATA::_SEED)
     `(DEFDATA::MV ,DEFDATA::SVAR DEFDATA::_SEED)))
        (uniformly-partition-size-binding-aux svar
          (cdr comp-svars)
          k
          (cdr rec-p-lst)
          (cdr texps)
          m)))))

(defun uniformly-partition-size-binding
  (svar comp-svars
    texps
    new-names
    m)
  (b* ((rec-p-lst (recursive-p-marked-lst texps
         new-names)) (k (len (collect-rec-cases texps
            new-names))))
    (uniformly-partition-size-binding-aux svar
      comp-svars
      k
      rec-p-lst
      texps
      m)))

(defmacro make-enum/acc-i...
  (s x)
  `(make-enum/acc-i ,DEFDATA::S
    ,DEFDATA::X
    kwd-alist
    new-names
    m
    c
    b
    wrld))

(defmacro make-enum/acc-is...
  (ss xs)
  `(make-enum/acc-is ,DEFDATA::SS
    ,DEFDATA::XS
    kwd-alist
    new-names
    m
    c
    b
    wrld))

(defabbrev make-choice-expr-for-enum/acc
  (ss i)
  (let ((k (len ss)))
    (if (= k 1)
      (car (make-enum/acc-is... ss (list i)))
      `(b* (((mv _choice _seed) (random-index-seed ,DEFDATA::K _seed)))
        (case _choice
          ,@(DEFDATA::LIST-UP-LISTS (DEFDATA::MAKE-NUMLIST-FROM 0 DEFDATA::K)
   (DEFDATA::MAKE-ENUM/ACC-IS... DEFDATA::SS
    (MAKE-LIST DEFDATA::K :INITIAL-ELEMENT DEFDATA::I)))
          (otherwise (mv nil _seed)))))))

(mutual-recursion (defun make-enum/acc-i
    (s i
      kwd-alist
      new-names
      m
      c
      b
      wrld)
    (declare (ignorable new-names))
    "enumerator/acc interpretation for core defdata exp s.
i is the name of the current indicial argument (dont confuse with an integer) that is used as recursion measure.
kwd-alist gives some defaults.
new-names is self-explanatory (imp to find recursive references)
M is type metadata table + some basic info for the clique of types being defined.
C is the constructor table + some basic info for new constructors.
B is the builtin combinator table."
    (cond ((possible-constant-value-p s) `(mv ,(IF (DEFDATA::QUOTEP DEFDATA::S)
     DEFDATA::S
     (LIST 'QUOTE DEFDATA::S))
          _seed))
      ((proper-symbolp s) (if (assoc-eq s m)
          `(,(DEFDATA::GET2 DEFDATA::S :ENUM/ACC DEFDATA::M) ,DEFDATA::I
            _seed)
          `(mv ,DEFDATA::S _seed)))
      ((not (true-listp s)) (make-enum/acc-i (cdr s)
          i
          kwd-alist
          new-names
          m
          c
          b
          wrld))
      ((assoc-eq (car s) b) (b* ((enum/acc-i-fn (get2 (car s) :enum/acc-i b)) ((when enum/acc-i-fn) (funcall-w enum/acc-i-fn
                (list i s)
                'make-enum/acc-i
                wrld))
            ((unless (eq (car s) 'or)) (er hard
                'make-enum/acc-i
                "~| Unsupported combinator ~x0.~%"
                (car s))))
          (b* ((base-texps (collect-base-cases (cdr s)
                 new-names)) (rec-texps (collect-rec-cases (cdr s)
                  new-names)))
            (if (null rec-texps)
              (make-choice-expr-for-enum/acc base-texps
                i)
              `(if (zp ,DEFDATA::I)
                ,(DEFDATA::MAKE-CHOICE-EXPR-FOR-ENUM/ACC DEFDATA::BASE-TEXPS DEFDATA::I)
                ,(DEFDATA::MAKE-CHOICE-EXPR-FOR-ENUM/ACC DEFDATA::REC-TEXPS DEFDATA::I))))))
      ((assoc-eq (car s) c) (b* ((k (len (cdr s))) (i1--ik (numbered-vars i k))
            (enum/acc-exprs (make-enum/acc-is... (remove-names-lst (cdr s))
                i1--ik))
            (pkg (get1 :current-package kwd-alist))
            (_v (fix-intern$ "_V" pkg))
            (_v1--_vk (numbered-vars _v k))
            (binding (bind-mv2-names-enum/acc-calls (cdr s)
                enum/acc-exprs
                _v1--_vk
                '_seed))
            (names (replace-calls-with-names _v1--_vk
                (cdr s))))
          `(b* (,@(DEFDATA::UNIFORMLY-PARTITION-SIZE-BINDING `(1- ,DEFDATA::I) DEFDATA::I1--IK
   (DEFDATA::REMOVE-NAMES-LST (CDR DEFDATA::S)) DEFDATA::NEW-NAMES DEFDATA::M) ,@DEFDATA::BINDING)
            (mv (,(CAR DEFDATA::S) . ,DEFDATA::NAMES)
              _seed))))
      (t `(,(CAR DEFDATA::S) . ,(DEFDATA::MAKE-ENUM/ACC-IS... (CDR DEFDATA::S)
  (MAKE-LIST (DEFDATA::LEN (CDR DEFDATA::S)) :INITIAL-ELEMENT DEFDATA::I))))))
  (defun make-enum/acc-is
    (texps is
      kwd-alist
      new-names
      m
      c
      b
      wrld)
    (declare (ignorable kwd-alist))
    (if (endp texps)
      'nil
      (b* ((car-enum-i (make-enum/acc-i... (car texps)
             (car is))))
        (and car-enum-i
          (cons car-enum-i
            (make-enum/acc-is... (cdr texps)
              (cdr is))))))))

(defun make-enum/acc-declare-forms
  (ivar kwd-alist)
  (b* ((guard-lambda (get1 :enum/acc-guard kwd-alist)) (actuals (list ivar '_seed))
      (ign-decls `((declare (ignorable ,DEFDATA::IVAR)))))
    (if guard-lambda
      (append ign-decls
        `((declare (xargs :mode :program :guard ,(DEFDATA::EXPAND-LAMBDA (CONS DEFDATA::GUARD-LAMBDA DEFDATA::ACTUALS))))))
      ign-decls)))

(program)

(defun enum/acc-event
  (p top-kwd-alist wrld)
  "make a enumerator/acc defun event."
  (b* (((cons name a) p) ((assocs ndef
         ndecl
         new-constructors
         new-types
         kwd-alist) a)
      (c (append new-constructors
          (table-alist 'data-constructor-table
            wrld)))
      (m (append new-types
          (table-alist 'type-metadata-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 ndecl)))
      (size (fix-intern$ "SIZE" pkg))
      (sizevar (if (member-eq size avoid-lst)
          size
          (generate-variable size
            avoid-lst
            nil
            nil
            wrld)))
      (enum/acc-body (make-enum/acc-i ndef
          sizevar
          kwd-alist
          (strip-cars new-types)
          m
          c
          b
          wrld))
      (enum/acc-decls (make-enum/acc-declare-forms sizevar
          kwd-alist)))
    `(defun ,(DEFDATA::GET2 DEFDATA::NAME :ENUM/ACC DEFDATA::M)
      (,DEFDATA::SIZEVAR _seed)
      ,@DEFDATA::ENUM/ACC-DECLS
      ,DEFDATA::ENUM/ACC-BODY)))

(defloop enum/acc-events
  (ps kwd-alist wrld)
  (for ((p in ps))
    (collect (enum/acc-event p
        kwd-alist
        wrld))))

(defun enumerator/acc-events
  (d kwd-alist wrld)
  (b* ((enum/acc-events (enum/acc-events d
         kwd-alist
         wrld)))
    (if (consp (cdr d))
      `((mutual-recursion ,@DEFDATA::ENUM/ACC-EVENTS))
      enum/acc-events)))

(add-pre-post-hook defdata-defaults-table
  :cgen-hook-fns '(enumerator-events enumerator/acc-events))