• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
      • Z3-installation
      • Smt-hint
      • Tutorial
      • Status
      • Developer
        • Verified
        • Trusted
          • Translation-datatypes
          • Smt-run
          • Smt-prove
          • Smt-write
          • Smt-trusted-cp
          • Z3-py
            • Smt-translator
            • Smt-translate-fty
            • Smt-names
            • Smt-recover-types
            • Smt-pretty-print
            • Smt-header
            • Smt-translate-abstract-sort
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Bitcoin
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Z3-py

Smt-translate-fty

Translating FTY declarations

Definitions and Theorems

Function: translate-bool

(defun translate-bool (b nil-type)
 (declare (xargs :guard (and (booleanp b) (symbolp nil-type))))
 (let ((acl2::__function__ 'translate-bool))
  (declare (ignorable acl2::__function__))
  (cond
   ((and (equal b nil) (equal nil-type nil))
    (list "False"))
   ((equal b nil)
    (list
       (downcase-string (concatenate 'string
                                     (lisp-to-python-names nil-type)
                                     ".nil"))))
   (t (list "True")))))

Theorem: paragraphp-of-translate-bool

(defthm paragraphp-of-translate-bool
  (b* ((translated (translate-bool b nil-type)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-symbol

(defun translate-symbol (sym)
  (declare (xargs :guard (symbolp sym)))
  (let ((acl2::__function__ 'translate-symbol))
    (declare (ignorable acl2::__function__))
    (downcase-string (lisp-to-python-names sym))))

Theorem: paragraphp-of-translate-symbol

(defthm paragraphp-of-translate-symbol
  (b* ((translated (translate-symbol sym)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-symbol-lst

(defun translate-symbol-lst (formals)
  (declare (xargs :guard (symbol-listp formals)))
  (let ((acl2::__function__ 'translate-symbol-lst))
    (declare (ignorable acl2::__function__))
    (b* ((formals (symbol-list-fix formals))
         ((unless (consp formals)) nil)
         ((unless (consp (cdr formals)))
          (list (translate-symbol (car formals))))
         ((cons first rest) formals)
         (translated-name (translate-symbol first)))
      (cons translated-name
            (cons '#\,
                  (cons '#\Space
                        (translate-symbol-lst rest)))))))

Theorem: paragraphp-of-translate-symbol-lst

(defthm paragraphp-of-translate-symbol-lst
  (b* ((translated (translate-symbol-lst formals)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-type

(defun translate-type (type int-to-rat flag)
  (declare (xargs :guard (and (symbolp type)
                              (booleanp int-to-rat)
                              (symbolp flag))))
  (let ((acl2::__function__ 'translate-type))
    (declare (ignorable acl2::__function__))
    (b* ((type (symbol-fix type))
         (item (cond ((equal flag 'uninterpreted)
                      (assoc-equal type *smt-uninterpreted-types*))
                     ((and (equal type 'integerp) int-to-rat)
                      (assoc-equal 'rationalp *smt-types*))
                     (t (assoc-equal type *smt-types*))))
         ((unless (endp item)) (cdr item)))
      (downcase-string (lisp-to-python-names type)))))

Theorem: stringp-of-translate-type

(defthm stringp-of-translate-type
  (b* ((translated (translate-type type int-to-rat flag)))
    (stringp translated))
  :rule-classes :rewrite)

Function: translate-fty-field-lst

(defun translate-fty-field-lst (fields int-to-rat)
  (declare (xargs :guard (and (fty-field-alist-p fields)
                              (booleanp int-to-rat))))
  (let ((acl2::__function__ 'translate-fty-field-lst))
    (declare (ignorable acl2::__function__))
    (b* ((fields (fty-field-alist-fix fields))
         ((unless (consp fields)) nil)
         ((cons first rest) fields)
         (name (translate-symbol (car first)))
         (type (translate-type (cdr first)
                               int-to-rat nil))
         (translated-field
              (cons '", ('"
                    (cons name
                          (cons '"', " (cons type '(")")))))))
      (cons translated-field
            (translate-fty-field-lst rest int-to-rat)))))

Theorem: paragraphp-of-translate-fty-field-lst

(defthm paragraphp-of-translate-fty-field-lst
  (b* ((translated (translate-fty-field-lst fields int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-fty-prod

(defun translate-fty-prod (name fields int-to-rat)
 (declare (xargs :guard (and (symbolp name)
                             (fty-field-alist-p fields)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-fty-prod))
  (declare (ignorable acl2::__function__))
  (b*
   ((name (symbol-fix name))
    (name (translate-symbol name))
    (datatype-line
       (cons name
             (cons '"= z3.Datatype"
                   (cons '#\(
                         (cons '#\'
                               (cons name '(#\' #\) #\Newline)))))))
    (translated-fields (translate-fty-field-lst fields int-to-rat))
    (fields-line
     (cons
      name
      (cons
        '".declare('"
        (cons name
              (cons '"'"
                    (append translated-fields '(")" #\Newline)))))))
    (create-line
         (cons name
               (cons '" = "
                     (cons name '(".create()" #\Newline))))))
   (cons datatype-line
         (cons fields-line (cons create-line 'nil))))))

Theorem: paragraphp-of-translate-fty-prod

(defthm paragraphp-of-translate-fty-prod
  (b* ((translated (translate-fty-prod name fields int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-fty-option

(defun translate-fty-option (name some-type int-to-rat)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp some-type)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-fty-option))
  (declare (ignorable acl2::__function__))
  (b*
   ((name (symbol-fix name))
    (name (translate-symbol name))
    (datatype-line
       (cons name
             (cons '"= z3.Datatype"
                   (cons '#\(
                         (cons '#\'
                               (cons name '(#\' #\) #\Newline)))))))
    (translated-type (translate-type some-type int-to-rat nil))
    (declare-line1
         (cons name
               (cons '".declare('some', ('val', "
                     (cons translated-type '("))" #\Newline)))))
    (declare-line2 (cons name '(".declare('nil')" #\Newline)))
    (create-line
         (cons name
               (cons '" = "
                     (cons name '(".create()" #\Newline))))))
   (cons datatype-line
         (cons declare-line1
               (cons declare-line2
                     (cons create-line 'nil)))))))

Theorem: paragraphp-of-translate-fty-option

(defthm paragraphp-of-translate-fty-option
 (b* ((translated (translate-fty-option name some-type int-to-rat)))
   (paragraphp translated))
 :rule-classes :rewrite)

Function: translate-fty-list

(defun translate-fty-list (name elt-type int-to-rat)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp elt-type)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-fty-list))
  (declare (ignorable acl2::__function__))
  (b*
   ((name (symbol-fix name))
    (name (translate-symbol name))
    (datatype-line
       (cons name
             (cons '"= z3.Datatype"
                   (cons '#\(
                         (cons '#\'
                               (cons name '(#\' #\) #\Newline)))))))
    (translated-elt-type (translate-type elt-type int-to-rat nil))
    (declare-line1
     (cons
         name
         (cons '".declare('cons', ('car', "
               (cons translated-elt-type
                     (cons '"), "
                           (cons '"('cdr', "
                                 (cons name '("))" #\Newline))))))))
    (declare-line2 (cons name '(".declare('nil')" #\Newline)))
    (consp-fn (cons '"def "
                    (cons name
                          (cons '"_consp(l): return Not(l == "
                                (cons name '(".nil)" #\Newline))))))
    (create-line
         (cons name
               (cons '" = "
                     (cons name '(".create()" #\Newline))))))
   (cons datatype-line
         (cons declare-line1
               (cons declare-line2
                     (cons create-line (cons consp-fn 'nil))))))))

Theorem: paragraphp-of-translate-fty-list

(defthm paragraphp-of-translate-fty-list
  (b* ((translated (translate-fty-list name elt-type int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-fty-alist-assoc-return

(defun translate-fty-alist-assoc-return
       (key-type val-type assoc-return int-to-rat)
 (declare (xargs :guard (and (symbolp key-type)
                             (symbolp val-type)
                             (paragraphp assoc-return)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-fty-alist-assoc-return))
  (declare (ignorable acl2::__function__))
  (b*
   ((key-type (symbol-fix key-type))
    (key-type (translate-type key-type int-to-rat nil))
    (val-type (symbol-fix val-type))
    (val-type (translate-type val-type int-to-rat nil))
    (assoc-return (paragraph-fix assoc-return))
    (datatype-line
         (cons assoc-return
               (cons '"= z3.Datatype('"
                     (cons assoc-return '("')" #\Newline)))))
    (declare-line1
      (cons assoc-return
            (cons '".declare('cons', ('car', "
                  (cons key-type
                        (cons '"), ('cdr', "
                              (cons val-type '("))" #\Newline)))))))
    (declare-line2 (cons assoc-return
                         '(".declare('nil')" #\Newline)))
    (consp-fn
      (cons '"def "
            (cons assoc-return
                  (cons '"_consp(l): return Not(l == "
                        (cons assoc-return '(".nil)" #\Newline))))))
    (create-line (cons assoc-return
                       (cons '" = "
                             (cons assoc-return
                                   '(".create()" #\Newline))))))
   (append datatype-line
           (append declare-line1
                   (append declare-line2
                           (cons create-line consp-fn)))))))

Theorem: paragraphp-of-translate-fty-alist-assoc-return

(defthm paragraphp-of-translate-fty-alist-assoc-return
  (b* ((translated (translate-fty-alist-assoc-return
                        key-type
                        val-type assoc-return int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-fty-alist-acons

(defun translate-fty-alist-acons (name maybe-val)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp maybe-val))))
 (let ((acl2::__function__ 'translate-fty-alist-acons))
  (declare (ignorable acl2::__function__))
  (b* ((name (symbol-fix name))
       (maybe-val (symbol-fix maybe-val))
       (maybe-val (translate-symbol maybe-val))
       (name (translate-symbol name))
       (fn-name (cons name '("_acons"))))
   (cons
       '"def "
       (cons fn-name
             (cons '"(key, value, alist): return Store(alist, key, "
                   (cons maybe-val
                         '(".some(value))" #\Newline))))))))

Theorem: paragraphp-of-translate-fty-alist-acons

(defthm paragraphp-of-translate-fty-alist-acons
  (b* ((translated (translate-fty-alist-acons name maybe-val)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-fty-alist-assoc

(defun translate-fty-alist-assoc (name maybe-val assoc-return)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp maybe-val)
                             (paragraphp assoc-return))))
 (let ((acl2::__function__ 'translate-fty-alist-assoc))
  (declare (ignorable acl2::__function__))
  (b* ((name (symbol-fix name))
       (name (translate-symbol name))
       (maybe-val (symbol-fix maybe-val))
       (maybe-val (translate-symbol maybe-val))
       (assoc-return (paragraph-fix assoc-return))
       (fn-name (cons name
                      (cons '"_"
                            (cons (translate-symbol 'assoc-equal)
                                  'nil)))))
   (cons
    '"def "
    (cons
     fn-name
     (cons
      '"(key, alist): return If(Select(alist, key) == "
      (cons
       maybe-val
       (cons
        '".nil, "
        (cons
         assoc-return
         (cons
          '".nil, "
          (cons
           assoc-return
           (cons
            '".cons(key, "
            (cons
              maybe-val
              '(".val(Select(alist, key))))" #\Newline))))))))))))))

Theorem: paragraphp-of-translate-fty-alist-assoc

(defthm paragraphp-of-translate-fty-alist-assoc
 (b* ((translated
           (translate-fty-alist-assoc name maybe-val assoc-return)))
   (paragraphp translated))
 :rule-classes :rewrite)

Function: make-pair-type

(defun make-pair-type (key-type val-type)
  (declare (xargs :guard (and (symbolp key-type)
                              (symbolp val-type))))
  (let ((acl2::__function__ 'make-pair-type))
    (declare (ignorable acl2::__function__))
    (b* ((key-type (symbol-fix key-type))
         (val-type (symbol-fix val-type))
         (key-type-str (symbol-name key-type))
         (val-type-str (symbol-name val-type))
         (pair-type (concatenate 'string
                                 key-type-str "_" val-type-str)))
      (downcase-string (lisp-to-python-names pair-type)))))

Theorem: stringp-of-make-pair-type

(defthm stringp-of-make-pair-type
  (b* ((pair-type (make-pair-type key-type val-type)))
    (stringp pair-type))
  :rule-classes :rewrite)

Function: translate-fty-alist-type

(defun translate-fty-alist-type (name key-type maybe-val int-to-rat)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp key-type)
                             (symbolp maybe-val)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-fty-alist-type))
  (declare (ignorable acl2::__function__))
  (b* ((name (symbol-fix name))
       (name (translate-symbol name))
       (key-type (symbol-fix key-type))
       (key-type (translate-type key-type int-to-rat nil))
       (maybe-val (symbol-fix maybe-val))
       (maybe-val (translate-type maybe-val int-to-rat nil)))
    (cons name
          (cons '" = ArraySort("
                (cons key-type
                      (cons '", "
                            (cons maybe-val '(")" #\Newline)))))))))

Theorem: paragraphp-of-translate-fty-alist-type

(defthm paragraphp-of-translate-fty-alist-type
 (b*
  ((translated
     (translate-fty-alist-type name key-type maybe-val int-to-rat)))
  (paragraphp translated))
 :rule-classes :rewrite)

Function: translate-fty-alist

(defun translate-fty-alist (name key-type val-type int-to-rat)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp key-type)
                             (symbolp val-type)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-fty-alist))
  (declare (ignorable acl2::__function__))
  (b*
   ((name (symbol-fix name))
    (key-type (symbol-fix key-type))
    (val-type (symbol-fix val-type))
    (val-type-pkg (symbol-package-name val-type))
    (val-type-str (translate-type val-type int-to-rat nil))
    (maybe-val-str (concatenate 'string
                                "maybe_" val-type-str))
    (maybe-val (intern$ maybe-val-str val-type-pkg))
    (maybe-val-type
         (translate-fty-option maybe-val val-type int-to-rat))
    (assoc-return (make-pair-type key-type val-type))
    (assoc-return-type (translate-fty-alist-assoc-return
                            key-type
                            val-type assoc-return int-to-rat))
    (alist-equality
      (translate-fty-alist-type name key-type maybe-val int-to-rat))
    (acons-fn (translate-fty-alist-acons name maybe-val))
    (assoc-fn
         (translate-fty-alist-assoc name maybe-val assoc-return)))
   (append (cons maybe-val-type
                 (cons alist-equality
                       (cons assoc-return-type 'nil)))
           (cons acons-fn (cons assoc-fn 'nil))))))

Theorem: paragraphp-of-translate-fty-alist

(defthm paragraphp-of-translate-fty-alist
 (b* ((translated
           (translate-fty-alist name key-type val-type int-to-rat)))
   (paragraphp translated))
 :rule-classes :rewrite)

Function: translate-one-fty-type

(defun translate-one-fty-type (name body int-to-rat)
 (declare (xargs :guard (and (symbolp name)
                             (fty-type-p body)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-one-fty-type))
  (declare (ignorable acl2::__function__))
  (b* ((body (fty-type-fix body)))
   (cond
       ((equal (fty-type-kind body) :prod)
        (translate-fty-prod name (fty-type-prod->fields body)
                            int-to-rat))
       ((equal (fty-type-kind body) :option)
        (translate-fty-option name (fty-type-option->some-type body)
                              int-to-rat))
       ((equal (fty-type-kind body) :list)
        (translate-fty-list name (fty-type-list->elt-type body)
                            int-to-rat))
       ((equal (fty-type-kind body) :alist)
        (translate-fty-alist name (fty-type-alist->key-type body)
                             (fty-type-alist->val-type body)
                             int-to-rat))
       (t nil)))))

Theorem: paragraphp-of-translate-one-fty-type

(defthm paragraphp-of-translate-one-fty-type
  (b* ((translated (translate-one-fty-type name body int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-fty-types-recur

(defun translate-fty-types-recur (fty-types int-to-rat)
 (declare (xargs :guard (and (fty-types-p fty-types)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-fty-types-recur))
  (declare (ignorable acl2::__function__))
  (b*
   ((fty-types (fty-types-fix fty-types))
    ((unless (consp fty-types)) nil)
    ((cons first rest) fty-types)
    ((cons name body) first)
    (translated-first (translate-one-fty-type name body int-to-rat))
    (translated-rest (translate-fty-types-recur rest int-to-rat))
    (translated (cons translated-first translated-rest)))
   translated)))

Theorem: paragraphp-of-translate-fty-types-recur

(defthm paragraphp-of-translate-fty-types-recur
 (b* ((translated (translate-fty-types-recur fty-types int-to-rat)))
   (paragraphp translated))
 :rule-classes :rewrite)

Function: translate-fty-types

(defun translate-fty-types (fty-types int-to-rat)
  (declare (xargs :guard (and (fty-types-p fty-types)
                              (booleanp int-to-rat))))
  (let ((acl2::__function__ 'translate-fty-types))
    (declare (ignorable acl2::__function__))
    (translate-fty-types-recur fty-types int-to-rat)))

Theorem: paragraphp-of-translate-fty-types

(defthm paragraphp-of-translate-fty-types
  (b* ((translated (translate-fty-types fty-types int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)