translate-type

(in-package "SMT")

(include-book "centaur/fty/top" :dir :system)

(include-book "xdoc/top" :dir :system)

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

(include-book "../../verified/hint-interface")

(include-book "../../verified/basics")

(include-book "./datatypes")

(defsection smt-translate-fty
  :parents (z3-py)
  :short "Translating FTY declarations"
  (local (in-theory (enable string-or-symbol-p)))
  (define translate-bool
    ((b booleanp) (nil-type symbolp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    (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"))))
  (define translate-symbol
    ((sym symbolp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    (downcase-string (lisp-to-python-names sym)))
  (define translate-symbol-lst
    ((formals symbol-listp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable translate-symbol
           paragraphp
           wordp))))
    :measure (len formals)
    (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
        `(#\, #\  ,@(SMT::TRANSLATE-SYMBOL-LST REST)))))
  (define translate-type
    ((type symbolp) (int-to-rat booleanp)
      (flag symbolp))
    :returns (translated stringp)
    (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))))
  (define translate-fty-field-lst
    ((fields fty-field-alist-p) (int-to-rat booleanp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable translate-type
           translate-symbol
           paragraphp
           wordp))))
    :measure (len fields)
    :hints (("Goal" :in-theory (e/d (fty-field-alist-fix) nil)))
    (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 `(", ('" ,SMT::NAME "', " ,TYPE ")")))
      (cons translated-field
        (translate-fty-field-lst rest int-to-rat))))
  (define translate-fty-prod
    ((name symbolp) (fields fty-field-alist-p)
      (int-to-rat booleanp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    (b* ((name (symbol-fix name)) (name (translate-symbol name))
        (datatype-line `(,SMT::NAME "= z3.Datatype"
            #\(
            #\'
            ,SMT::NAME
            #\'
            #\)
            #\
))
        (translated-fields (translate-fty-field-lst fields int-to-rat))
        (fields-line `(,SMT::NAME ".declare('"
            ,SMT::NAME
            "'"
            ,@SMT::TRANSLATED-FIELDS
            ")"
            #\
))
        (create-line `(,SMT::NAME " = " ,SMT::NAME ".create()" #\
)))
      `(,SMT::DATATYPE-LINE ,SMT::FIELDS-LINE ,SMT::CREATE-LINE)))
  (define translate-fty-option
    ((name symbolp) (some-type symbolp)
      (int-to-rat booleanp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    (b* ((name (symbol-fix name)) (name (translate-symbol name))
        (datatype-line `(,SMT::NAME "= z3.Datatype"
            #\(
            #\'
            ,SMT::NAME
            #\'
            #\)
            #\
))
        (translated-type (translate-type some-type int-to-rat nil))
        (declare-line1 `(,SMT::NAME ".declare('some', ('val', "
            ,SMT::TRANSLATED-TYPE
            "))"
            #\
))
        (declare-line2 `(,SMT::NAME ".declare('nil')" #\
))
        (create-line `(,SMT::NAME " = " ,SMT::NAME ".create()" #\
)))
      `(,SMT::DATATYPE-LINE ,SMT::DECLARE-LINE1
        ,SMT::DECLARE-LINE2
        ,SMT::CREATE-LINE)))
  (define translate-fty-list
    ((name symbolp) (elt-type symbolp)
      (int-to-rat booleanp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    (b* ((name (symbol-fix name)) (name (translate-symbol name))
        (datatype-line `(,SMT::NAME "= z3.Datatype"
            #\(
            #\'
            ,SMT::NAME
            #\'
            #\)
            #\
))
        (translated-elt-type (translate-type elt-type int-to-rat nil))
        (declare-line1 `(,SMT::NAME ".declare('cons', ('car', "
            ,SMT::TRANSLATED-ELT-TYPE
            "), "
            "('cdr', "
            ,SMT::NAME
            "))"
            #\
))
        (declare-line2 `(,SMT::NAME ".declare('nil')" #\
))
        (consp-fn `("def " ,SMT::NAME
            "_consp(l): return Not(l == "
            ,SMT::NAME
            ".nil)"
            #\
))
        (create-line `(,SMT::NAME " = " ,SMT::NAME ".create()" #\
)))
      `(,SMT::DATATYPE-LINE ,SMT::DECLARE-LINE1
        ,SMT::DECLARE-LINE2
        ,SMT::CREATE-LINE
        ,SMT::CONSP-FN)))
  (define translate-fty-alist-assoc-return
    ((key-type symbolp) (val-type symbolp)
      (assoc-return paragraphp)
      (int-to-rat booleanp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    (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 `(,SMT::ASSOC-RETURN "= z3.Datatype('"
            ,SMT::ASSOC-RETURN
            "')"
            #\
))
        (declare-line1 `(,SMT::ASSOC-RETURN ".declare('cons', ('car', "
            ,SMT::KEY-TYPE
            "), ('cdr', "
            ,SMT::VAL-TYPE
            "))"
            #\
))
        (declare-line2 `(,SMT::ASSOC-RETURN ".declare('nil')" #\
))
        (consp-fn `("def " ,SMT::ASSOC-RETURN
            "_consp(l): return Not(l == "
            ,SMT::ASSOC-RETURN
            ".nil)"
            #\
))
        (create-line `(,SMT::ASSOC-RETURN " = "
            ,SMT::ASSOC-RETURN
            ".create()"
            #\
)))
      `(,@SMT::DATATYPE-LINE ,@SMT::DECLARE-LINE1
        ,@SMT::DECLARE-LINE2
        ,SMT::CREATE-LINE
        ,@SMT::CONSP-FN)))
  (define translate-fty-alist-acons
    ((name symbolp) (maybe-val symbolp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    (b* ((name (symbol-fix name)) (maybe-val (symbol-fix maybe-val))
        (maybe-val (translate-symbol maybe-val))
        (name (translate-symbol name))
        (fn-name `(,SMT::NAME "_acons")))
      `("def " ,SMT::FN-NAME
        "(key, value, alist): return Store(alist, key, "
        ,SMT::MAYBE-VAL
        ".some(value))"
        #\
)))
  (define translate-fty-alist-assoc
    ((name symbolp) (maybe-val symbolp)
      (assoc-return paragraphp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    :guard-debug t
    (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 `(,SMT::NAME "_" ,(SMT::TRANSLATE-SYMBOL 'SMT::ASSOC-EQUAL))))
      `("def " ,SMT::FN-NAME
        "(key, alist): return If(Select(alist, key) == "
        ,SMT::MAYBE-VAL
        ".nil, "
        ,SMT::ASSOC-RETURN
        ".nil, "
        ,SMT::ASSOC-RETURN
        ".cons(key, "
        ,SMT::MAYBE-VAL
        ".val(Select(alist, key))))"
        #\
)))
  (define make-pair-type
    ((key-type symbolp) (val-type symbolp))
    :returns (pair-type stringp)
    (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))))
  (define translate-fty-alist-type
    ((name symbolp) (key-type symbolp)
      (maybe-val symbolp)
      (int-to-rat booleanp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    (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)))
      `(,SMT::NAME " = ArraySort("
        ,SMT::KEY-TYPE
        ", "
        ,SMT::MAYBE-VAL
        ")"
        #\
)))
  (define translate-fty-alist
    ((name symbolp) (key-type symbolp)
      (val-type symbolp)
      (int-to-rat booleanp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    :guard-hints (("Goal" :in-theory (e/d (paragraphp wordp) nil)))
    (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 `(,SMT::MAYBE-VAL-TYPE ,SMT::ALIST-EQUALITY
          ,SMT::ASSOC-RETURN-TYPE)
        `(,SMT::ACONS-FN ,SMT::ASSOC-FN))))
  (define translate-one-fty-type
    ((name symbolp) (body fty-type-p)
      (int-to-rat booleanp))
    :returns (translated paragraphp
      :hints (("Goal" :in-theory (enable paragraphp wordp))))
    (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))))
  (define translate-fty-types-recur
    ((fty-types fty-types-p) (int-to-rat booleanp))
    :returns (translated paragraphp)
    :measure (len fty-types)
    :hints (("Goal" :in-theory (e/d (fty-types-fix) nil)))
    (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))
  (define translate-fty-types
    ((fty-types fty-types-p) (int-to-rat booleanp))
    :returns (translated paragraphp)
    (translate-fty-types-recur fty-types
      int-to-rat)))

(defsection smt-translate-abstract-sort
  :parents (z3-py)
  :short "Translating abstract sorts."
  (define translate-abstract-types
    ((abs symbol-listp))
    :returns (translated paragraphp)
    :measure (len (symbol-list-fix abs))
    (b* ((abs (symbol-list-fix abs)) ((unless (consp abs)) nil)
        ((cons abs-hd abs-tl) abs)
        (name (translate-symbol abs-hd))
        (first-abs `(,SMT::NAME " = z3.DeclareSort('" ,SMT::NAME "')" #\
)))
      `(,SMT::FIRST-ABS ,@(SMT::TRANSLATE-ABSTRACT-TYPES SMT::ABS-TL)))))