(module cvc-translator
        (main main))

(define (fold-left proc base lst)
  (let loop ((curr base)
             (lst lst))
    (if (null? lst)
      curr
      (loop (proc curr (car lst)) (cdr lst)))))

(define (combine-children children op)
  (fold-left (lambda (acc child)
               (if (and (list? child) (eq? (car child) op))
                 (append acc (cdr child))
                 (append acc (list child))))
             '()
             children))

(define (ac->n-ary ast)
  (let loop ((ast ast))
    (match-case ast
      ((AND . ?children)
       `(AND ,@(combine-children (map loop children) 'AND)))
      ((OR . ?children)
       `(OR ,@(combine-children (map loop children) 'OR)))
      ((ADD . ?children)
       `(ADD ,@(combine-children (map loop children) 'ADD)))
      ((?tag . ?children)
       `(,tag ,@(map loop children)))
      (?-
       ast))))


(define *cvc-keyword-list*
  '("REAL" "INTEGER" "BOOLEAN" "NOT" "OR" "AND" "XOR" "ASSERT" "IF" "THEN" "ELSE" "ENDIF" "QUERY" "TRUE" "FALSE" "TYPE"))

(define (cvc/init-lexer!)
  (for-each (lambda (word)
              (putprop! (string->symbol word) 'cvc-reserved #t))
            *cvc-keyword-list*))

(define *line* 1)

(define *cvc-lexer*
  (regular-grammar
   ((nonzero-digit (in ("19")))
    (id (: (or #\' #\_ alpha #\$) (* (or #\$ #\. #\' #\_ alpha digit))))
    (num (+ digit)))
   ((in #\newline #a012)
    (set! *line* (+ *line* 1))
    (ignore))
   ((+ (in #\space #\tab))
    (ignore))
   ;; comments
   ((: "%" (* (out #\newline)) #\newline)
    (set! *line* (+ *line* 1))
    (ignore))
   ;; parenthesis
   (#\(
    (cons 'LP *line*))
   (#\)
    (cons 'RP *line*))
   (#\[
    (cons 'LB *line*))
   (#\]
    (cons 'RB *line*))
   ("->"
    (cons 'ARROW *line*))
   (#\;
    (cons 'SEMI *line*))
   (#\,
    (cons 'COMMA *line*))
   (#\:
    (cons 'CLN *line*))
   ;; numbers
   (num
    (cons 'NUM (string->integer (the-string))))
   ((: #\- num)
    (cons 'NUM (string->integer (the-string))))
   ;; op
   (#\+
    (cons 'PLUS *line*))
   ("-"
    (cons 'MINUS *line*))
   ("*"
    (cons 'MUL *line*))
   ("<"
    (cons 'LT *line*))
   ("<="
    (cons 'LE *line*))
   ("<=>"
    (cons 'IFF *line*))
   (">"
    (cons 'GT *line*))
   (">="
    (cons 'GE *line*))
   (#\=
    (cons 'EQ *line*))
   ("=>"
    (cons 'IMPLIES *line*))
   ("/="
    (cons 'NEQ *line*))
   ("<=>"
    (cons 'IFF *line*))
   ;; identifiers
   (id
    (let* ((string   (the-string))
           (symbol   (string->symbol string))
           (upsymbol (string->symbol (string-upcase string))))
      (cond
       ((getprop symbol 'cvc-reserved)
        ;; (print "upsymbol" upsymbol)
        (cons upsymbol *line*))
       (else
        (cons 'ID symbol)))))
   ;; error
   (else
    (let ((c (the-failure)))
      (if (eof-object? c)
        c
        (list 'ERROR c *line*))))))

(define *real2int?* #f)

(define *cvc-parser* 
  (lalr-grammar
   ((left: MUL)
    (left: PLUS MINUS)
    (none: ID)
    (left: EQ NEQ LT GT LE GE)
    (none: NOT)
    (left: AND)
    (left: OR)
    (left: XOR)
    (right: IMPLIES)
    (left: IFF)
    LP RP LB RB NUM TRUE FALSE IF THEN ELSE ENDIF QUERY ASSERT SEMI CLN BOOLEAN REAL INTEGER ARROW COMMA TYPE)
   (start
    ((command-list) (reverse command-list)))
   (command-list
    (() '())
    ((command-list command) 
     (if command
       (cons command command-list)
       command-list)))
   (command
    ((ASSERT expr SEMI)
     `(ASSERT ,expr))
    ((QUERY expr SEMI)
     `(QUERY ,expr))
    ((ID CLN type SEMI)
     `(DECL ,ID ,type))
    ((ID CLN type EQ expr SEMI)
     `(DECL ,ID ,type ,expr))
    ((ID CLN TYPE SEMI)
     ;; ignore it
     #f))
   (type 
    ((BOOLEAN) 'BOOLEAN)
    ((INTEGER) 'INTEGER)
    ((REAL) (if *real2int?* 'INTEGER 'REAL))
    ((LB type@t1 ARROW type@t2 RB)
     `(FUNCTION-TYPE ,t1 ,t2))
    ((LB LB type+ RB ARROW type RB)
     `(FUNCTION-TYPE ,@(reverse type+) ,type)))
   (type+
    ((type)
     (list type))
    ((type+ COMMA type)
     (cons type type+)))
   (expr
    ((ID) ID)
    ((NUM) NUM)
    ((TRUE) 'TRUE)
    ((FALSE) 'FALSE)
    ((LP expr RP) expr)
    ((expr@e1 AND expr@e2) `(AND ,e1 ,e2))
    ((expr@e1 OR expr@e2) `(OR ,e1 ,e2))
    ((expr@e1 XOR expr@e2) `(XOR ,e1 ,e2))
    ((NOT expr) `(NOT ,expr))
    ((expr@e1 IMPLIES expr@e2) `(IMPLIES ,e1 ,e2))
    ((expr@e1 IFF expr@e2) `(IFF ,e1 ,e2))
    ((IF expr@e1 THEN expr@e2 ELSE expr@e3 ENDIF) `(ITE ,e1 ,e2 ,e3))
    ((expr@e1 PLUS expr@e2) `(ADD ,e1 ,e2))
    ((expr@e1 MINUS expr@e2) `(SUB ,e1 ,e2))
    ((MINUS expr) `(SUB 0 ,expr))
    ((expr@e1 MUL expr@e2) `(MUL ,e1 ,e2))
    ((expr@e1 LT expr@e2) `(LT ,e1 ,e2))
    ((expr@e1 LE expr@e2) `(LE ,e1 ,e2))
    ((expr@e1 GT expr@e2) `(GT ,e1 ,e2))
    ((expr@e1 GE expr@e2) `(GE ,e1 ,e2))
    ((expr@e1 EQ expr@e2) `(EQ ,e1 ,e2))
    ((expr@e1 NEQ expr@e2) `(NEQ ,e1 ,e2))
    ((ID LP expr+ RP) `(APP ,ID ,@(reverse expr+)))
    )
   (expr+
    ((expr)
     (list expr))
    ((expr+ COMMA expr)
     (cons expr expr+)))
    ))

(define (cvc/parse)
  (read/lalrp
   *cvc-parser*
   *cvc-lexer*
   (current-input-port)))

(define (cvc/parse-string astring)
  (with-input-from-string
      astring
    cvc/parse))

(define (cvc/parse-file filename)
  (with-input-from-file
      filename
    cvc/parse))

(define (display-infix-core op arg1 arg2 o-par c-par loop)
  (display o-par)
  (loop arg1)
  (display* " " op " ")
  (loop arg2)
  (display c-par))

(define (display-infix op arg1 arg2 loop)
  (display-infix-core op arg1 arg2 "(" ")" loop))

(define (display-infix-prop op arg1 arg2 loop)
  (display-infix-core op arg1 arg2 "[" "]" loop))

(define (make-queue . args)
  (let ((result (cons '() '())))
    (for-each (lambda (arg)
                (queue/insert! result arg))
              args)
    result))

(define (queue/reset! queue)
  (set-car! queue '())
  (set-cdr! queue '()))

(define (queue? obj)
  (and (pair? obj) (list? (car obj)) (list? (cdr obj))))

(define (queue/empty? q)
  (eq? (car q) '()))

(define (queue/front q)
  [assert (q) (and (queue? q) (not (queue/empty? q)))]
  (caar q))

(define (queue/rear q)
  [assert (q) (and (queue? q) (not (queue/empty? q)))]
  (cadr q))

(define (queue->list q)
  (car q))

(define (queue/length q)
  (length (car q)))

(define (queue/insert! q datum)
  (let ((new-pair (cons datum '())))
    (cond 
     ((eq? (car q) '())
      [assert (q) (eq? (cdr q) '())]
      (set-car! q new-pair)
      (set-cdr! q new-pair))
     (else
      (set-cdr! (cdr q) new-pair)
      (set-cdr! q new-pair))))
  q)

(define (cmds/ac->n-ary cmd-lst)
  (let ((r (make-queue)))
    (for-each (lambda (cmd)
                (queue/insert! r (ac->n-ary cmd)))
              cmd-lst)
    (queue->list r)))

(define (print-error . args)
  (with-output-to-port (current-error-port)
    (lambda ()
      (apply print args))))

(define (sign-error . args)
  (apply print-error args)
  (exit -1))

(define (make-var-kind-table cmd-lst)
  (let ((var-kind-table (make-hashtable)))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?id BOOLEAN . ?-)
                   (hashtable-put! var-kind-table id 'prop))
                  ((DECL ?id ?- . ?-)
                   (hashtable-put! var-kind-table id 'term))))
              cmd-lst)
    var-kind-table))
                  
(define (get-ast-kind ast var-kind-table)
  (cond
   ((list? ast)
    (case (car ast)
      ((ADD SUB APP) 'term)
      ((ITE)
       (get-ast-kind (caddr ast) var-kind-table))
      (else
       'prop)))
   ((memq ast '(TRUE FALSE))
    'prop)
   ((symbol? ast)
    (hashtable-get var-kind-table ast))
   ((number? ast)
    'term)
   (else
    (error 'get-ast-kind "unexpected ast" ast))))

(define (display-plain-symbol s prefix)
  (let ((first? #t))
    (for-each (lambda (c)
                (cond
                 ((and first? (eq? c #\_))
                  (display prefix))
                 ((or (char-alphabetic? c) (char-numeric? c) (eq? c #\_))
                  (display c))
                 (else
                  (display* prefix "_")
                  (display (char->integer c))
                  (display "__")))
                (set! first? #f))
              (string->list (symbol->string s)))))

(define (display-ics-symbol s)
  (display-plain-symbol s "ics_"))

(define (display-uclid-symbol s)
  (display-plain-symbol s "ucl_"))

(define (display-simplify-symbol s)
  (display-plain-symbol s "simp_"))

(define *ics-op-table* '((ADD . +) (SUB . -) (MUL . *) (LT . <) (LE . <=) (GT . >) (GE . >=) (EQ . =) (NEQ . <>)
                         (AND . "&") (OR . "|") (XOR . "#") (IFF . <=>) (IMPLIES . =>)))

;; the following function fixes a misuse of the operator = where a <=> is expected.
;; another problem with ICS is that it doesn't support predicates.
(define (fix-definitions-core cmd-list var-kind-table ics?)
  (let ((res-cmd-list (make-queue)))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((ASSERT (EQ ?id ?body))
                   (cond
                    ((and (symbol? id) (eq? (hashtable-get var-kind-table id) 'prop))
                     (let ((new-body (if (and ics? (eq? (get-ast-kind body var-kind-table) 'term))
                                       `(EQ ,body true)
                                       body)))
                       (queue/insert! res-cmd-list `(ASSERT (IFF ,id ,new-body)))))
                    (else
                     (queue/insert! res-cmd-list cmd))))
                  (else
                   (queue/insert! res-cmd-list cmd))))
              cmd-list)
    (queue->list res-cmd-list)))


(define (fix-ics-definitions cmd-list var-kind-table)
  (fix-definitions-core cmd-list var-kind-table #t))

(define (fix-uclid-definitions cmd-list var-kind-table) 
  (fix-definitions-core cmd-list var-kind-table #f))

(define (cvc->ics cmd-lst)
  (let* ((var-kind-table (make-var-kind-table cmd-lst))
         (cmd-lst (fix-ics-definitions cmd-lst var-kind-table))
         (assumptions (make-queue))
         (idx 0)
         (next-aux-id (lambda () 
                        (let ((result idx))
                          (set! idx (+ idx 1))
                          result)))
         (found-check-valid? #f)
         (pp-ast (lambda (ast)
                   (let loop ((ast ast))
                     (cond 
                      ((list? ast)
                       (let ((c (car ast)))
                         (cond
                          ((memq c '(ADD SUB MUL))
                           [assert (ast) (= (length ast) 3)]
                           (display-infix (cdr (assq c *ics-op-table*)) (cadr ast) (caddr ast) loop))
                          ((memq c '(OR AND IMPLIES IFF LT LE GT GE EQ NEQ))
                           [assert (ast) (= (length ast) 3)]
                           (display-infix-prop (cdr (assq c *ics-op-table*)) (cadr ast) (caddr ast) loop))
                          ((eq? c 'NOT)
                           [assert (ast) (= (length ast) 2)]
                           (display "[~ ")
                           (loop (cadr ast))
                           (display "]"))
                          ((eq? c 'APP)
                           (display-ics-symbol (cadr ast))
                           (display "(")
                           (let ((first #t))
                             (for-each (lambda (child)
                                         (unless first (display ", "))
                                         (loop child)
                                         (set! first #f))
                                       (cddr ast)))
                           (display ")"))
                          ((eq? c 'ITE)
                           [assert (ast) (= (length ast) 4)]
                           (let ((cond-expr (cadr ast))
                                 (then-expr (caddr ast))
                                 (else-expr (cadddr ast)))
                             (cond
                              ((eq? (get-ast-kind then-expr var-kind-table) 'prop)
                               (display "[if ") 
                               (loop cond-expr)
                               (display " then ")
                               (loop then-expr)
                               (display " else ")
                               (loop else-expr)
                               (display " end]")
                               )
                              (else
                               [assert (then-expr) (eq? (get-ast-kind then-expr var-kind-table) 'term)]
                               (let* ((aux-var (symbol-append 'icsaux (string->symbol (integer->string (next-aux-id)))))
                                      (top-ite `(ITE ,cond-expr
                                                     (EQ ,aux-var ,then-expr)
                                                     (EQ ,aux-var ,else-expr))))
                                 (queue/insert! assumptions top-ite)
                                 (hashtable-put! var-kind-table aux-var 'term)
                                 (display-ics-symbol aux-var))))))
                          (else
                           (error 'cvc->ics "unexpected ast" ast)))))
                      ((eq? ast 'TRUE)
                       (display 'tt))
                      ((eq? ast 'FALSE)
                       (display 'ff))
                      ((symbol? ast)
                       (display-ics-symbol ast))
                      (else
                       (display ast)))))))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?id BOOLEAN ?def)
                   (display "prop ")
                   (display-ics-symbol id)
                   (display " := ")
                   (pp-ast def)
                   (when (eq? (get-ast-kind def var-kind-table) 'term)
                     (display " = true"))
                   (print " ."))
                  ((DECL ?id ?- ?def)
                   (display "def ")
                   (display-ics-symbol id)
                   (display " := ")
                   (pp-ast def)
                   (print " ."))
                  ((ASSERT ?expr)
                   (queue/insert! assumptions expr))
                  ((QUERY ?expr)
                   (when found-check-valid?
                     (error 'cvc->ics "Only one QUERY is supported..." #unspecified))
                   (print "sat ")
                   (for-each (lambda (assumption)
                               (pp-ast assumption)
                               (print " & "))
                             (queue->list assumptions))
                   (display "~[ ")
                   (pp-ast expr)
                   (print " ]."))))
              cmd-lst)))

(define *simplify-op-table* '((ADD . +) (SUB . -) (MUL . *) (LT . <) (LE . <=) (GT . >) (GE . >=) (EQ . EQ) (NEQ . NEQ)
                              (AND . AND) (OR . OR) (IFF . IFF) (IMPLIES . IMPLIES) (NOT . NOT)))
;; XOR is not defined on Simplify

(define (cvc->simplify cmd-lst)
  (let* ((cmd-lst (cmds/ac->n-ary cmd-lst))
         (var-kind-table (make-var-kind-table cmd-lst))
         (assumptions (make-queue))
         (idx 0)
         (next-aux-id (lambda () 
                        (let ((result idx))
                          (set! idx (+ idx 1))
                          result)))
         (display-args (lambda (args loop)
                         (for-each (lambda (arg)
                                         (display " ")
                                         (loop arg))
                                   args)))
         (pp-ast (lambda (ast)
                   (let loop ((ast ast))
                     (cond 
                      ((list? ast)
                       (let ((c (car ast)))
                         (cond
                          ((assq c *simplify-op-table*) =>
                           (lambda (entry)
                             (display* "(" (cdr entry))
                             (display-args (cdr ast) loop)
                             (display ")")))
                          ((eq? c 'XOR)
                           (display "(NOT (IFF")
                           (display-args (cdr ast) loop)
                           (display "))"))
                          ((eq? c 'APP)
                           (display "(")
                           (display-simplify-symbol (cadr ast))
                           (display-args (cddr ast) loop)
                           (display ")"))
                          ((eq? c 'ITE)
                           [assert (ast) (= (length ast) 4)]
                           (let ((cond-expr (cadr ast))
                                 (then-expr (caddr ast))
                                 (else-expr (cadddr ast)))
                             (cond
                              ((eq? (get-ast-kind then-expr var-kind-table) 'prop)
                               (display "(OR (AND ")
                               (loop cond-expr)
                               (display " ")
                               (loop then-expr)
                               (display ") (AND (NOT ")
                               (loop cond-expr)
                               (display ") ")
                               (loop else-expr)
                               (display "))"))
                              (else
                               [assert (then-expr) (eq? (get-ast-kind then-expr var-kind-table) 'term)]
                               (let* ((aux-var (symbol-append 'saux (string->symbol (integer->string (next-aux-id)))))
                                      (top-ite `(ITE ,cond-expr
                                                     (EQ ,aux-var ,then-expr)
                                                     (EQ ,aux-var ,else-expr))))
                                 (queue/insert! assumptions top-ite)
                                 (hashtable-put! var-kind-table aux-var 'term)
                                 (display-simplify-symbol aux-var))))))
                          (else
                           (error 'cvc->simplify "unexpected ast" ast)))))
                      ((memq ast '(TRUE FALSE))
                       (display ast))
                      ((symbol? ast)
                       (display-simplify-symbol ast))
                      (else
                       (display ast)))))))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?id (FUNCTION-TYPE . ?types))
                   (let ((arity (- (length types) 1))
                         (range (car (reverse types))))
                     (when (eq? range 'BOOLEAN)
                       (display "(DEFPRED (")
                       (display-simplify-symbol id)
                       (display " ")
                       (let loop ((i 0))
                         (when (< i arity)
                           (display* " x" i)
                           (loop (+ i 1))))
                       (print "))"))))
                  ((DECL ?id BOOLEAN ?def)
                   (queue/insert! assumptions `(IFF ,id ,def)))
                  ((DECL ?id ?- ?def)
                   (queue/insert! assumptions `(EQ ,id ,def)))
                  ((ASSERT ?expr)
                   (queue/insert! assumptions expr))
                  ((QUERY ?expr)
                   (print "(OR ")
                   (cond
                    ((queue/empty? assumptions)
                     (print "FALSE"))
                    (else
                     (print "(NOT (AND ")
                     (let ((main-assumptions (queue->list assumptions)))
                       (set! assumptions (make-queue))
                       (for-each (lambda (assumption)
                                   (display "  ")
                                   (pp-ast assumption)
                                   (print ""))
                                 main-assumptions))
                     (print "))")))
                   (pp-ast expr)
                   (unless (queue/empty? assumptions)
                     (print "(NOT (AND ")
                     (for-each (lambda (ite-assumption)
                                 (display "  ")
                                 (pp-ast ite-assumption)
                                 (print ""))
                               (queue->list assumptions))
                     (print "))"))
                   (print ")"))))
              cmd-lst)))

(define *rel-op* '(LT LE GT GE EQ NEQ))

(define (rel-op? op)
  (memq op *rel-op*))

(define *uclid-op-table* '((LT . <) (LE . <=) (GT . >) (GE . >=) (EQ . =) (NEQ . !=)
                           (AND . "&") (OR . "|") (IFF . <=>) (IMPLIES . =>)))

; (define (num-aux-vars cmd-lst var-kind-table)
;   (let ((num-vars 0))
;     (for-each (lambda (cmd)
;                 (let loop ((expr cmd))
;                   (match-case expr
;                     ((ITE ?- ?then-expr ?-)
;                      (when (eq? (get-ast-kind then-expr var-kind-table) 'term)
;                        (set! num-vars (+ num-vars 1)))))
;                   (when (list? expr)
;                     (for-each loop (cdr expr)))))
;               cmd-lst)
;     num-vars))

(define (process-ite-for-uclid cmd-lst var-kind-table)
  (let* ((new-cmd-lst (make-queue))
         (idx 0)
         (next-aux-id (lambda () 
                        (let ((result idx))
                          (set! idx (+ idx 1))
                          result)))
         (gen-aux-name (lambda (idx)
                         (symbol-append 'uaux (string->symbol (integer->string idx)))))
         (ite->case (lambda (expr)
                      (let loop ((expr expr))
                        (match-case expr
                          ((ITE . ?children)
                           (let ((new-children (map loop children))
                                 (aux-var (gen-aux-name (next-aux-id)))
                                 (kind (get-ast-kind expr var-kind-table)))
                             (queue/insert! new-cmd-lst `(DECL ,aux-var ,(if (eq? kind 'prop) 'BOOLEAN 'INTEGER) (ITE ,@new-children)))
                             aux-var))
                          ((?tag . ?children)
                           `(,tag ,@(map loop children)))
                          (?-
                           expr))))))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?id ?type ?expr)
                   (queue/insert! new-cmd-lst `(DECL ,id ,type ,(ite->case expr))))
                  ((ASSERT ?expr)
                   (queue/insert! new-cmd-lst `(ASSERT ,(ite->case expr))))
                  ((QUERY ?expr)
                   (queue/insert! new-cmd-lst `(QUERY ,(ite->case expr))))
                  (?- 
                   (queue/insert! new-cmd-lst cmd))))
              cmd-lst)
    (queue->list new-cmd-lst)))

(define (sign-uclid-not-supported)
  (sign-error "Only separation logic is supported by the UCLID backend."))

(define (display-constant-prefix constant)
  (cond
   ((= constant 0)
    ;; do nothing
    #unspecified)
   ((= constant 1)
    (display "succ("))
   ((= constant -1)
    (display "pred("))
   ((> constant 1)
    (display* "succ^" constant "("))
   ((< constant -1)
    (display* "pred^" (- 0 constant) "("))
   (else
    (sign-uclid-not-supported))))

(define (display-constant-suffix constant)
  (unless (= constant 0)
    (display ")")))

(define (collect-data expr pos? add-entry-proc! inc-constant-proc!)
  (let loop ((expr expr)
             (pos? pos?))
    (match-case expr
      ((? number?)
       (inc-constant-proc! (if pos? expr (- 0 expr))))
      ((ADD ?arg1 ?arg2)
       (loop arg1 pos?)
       (loop arg2 pos?))
      ((SUB ?arg1 ?arg2)
       (loop arg1 pos?)
       (loop arg2 (not pos?)))
      ((MUL . ?-)
       (sign-uclid-not-supported))
      (?- 
       (add-entry-proc! expr pos?)))))

(define (display-rel-app rel-op arg1 arg2 pp-ast-proc)
  (let* ((new-arg1 #f)
         (new-arg2 #f)
         (constant 0)
         (add-entry-proc! 
          (lambda (expr pos?)
            (cond
             ((and pos? (not new-arg1))
              (set! new-arg1 expr))
             ((and (not pos?) (not new-arg2))
              (set! new-arg2 expr))
             (else
              (sign-uclid-not-supported)))))
         (inc-constant-proc!
          (lambda (inc)
            (set! constant (+ constant inc)))))
    (collect-data arg1 #t add-entry-proc! inc-constant-proc!)
    (collect-data arg2 #f add-entry-proc! inc-constant-proc!)
    (if new-arg1
      (pp-ast-proc new-arg1)
      (display "uclid_ZERO"))
    (display* " " rel-op " ")
    ;; moving the constant to the right-hand-side... this is a small hack to allow me to reuse this function to print definitions.
    (set! constant (- 0 constant)) 
    ;; display the right-hand-side
    (display-constant-prefix constant)
    (if new-arg2
      (pp-ast-proc new-arg2)
      (display "uclid_ZERO"))
    (display-constant-suffix constant)))

(define (cvc->uclid cmd-lst)
  (let* ((var-kind-table (make-var-kind-table cmd-lst))
         (cmd-lst1 (fix-uclid-definitions cmd-lst var-kind-table))
         (cmd-lst (process-ite-for-uclid cmd-lst1 var-kind-table))
         (assumptions (make-queue))
         (infix-op? (lambda (op)
                      (assq op *uclid-op-table*)))
         (found-check-valid? #f)
         (pp-ast (lambda (ast)
                   (let loop ((ast ast))
                     (match-case ast
                       (((? rel-op?) ?arg1 ?arg2)
                        (display-rel-app (cdr (assq (car ast) *uclid-op-table*)) arg1 arg2 loop))
                       ((ADD (? number?) ?expr)
                        (display-constant-prefix (cadr ast))
                        (loop expr)
                        (display-constant-suffix (cadr ast)))
                       ((ADD ?expr (? number?))
                        (display-constant-prefix (caddr ast))
                        (loop expr)
                        (display-constant-suffix (caddr ast)))
                       ((SUB ?expr (? number?))
                        (display-constant-prefix (- 0 (caddr ast)))
                        (loop expr)
                        (display-constant-suffix (- 0 (caddr ast))))
                       (((? infix-op?) ?arg1 ?arg2)
                        (display-infix (cdr (assq (car ast) *uclid-op-table*)) arg1 arg2 loop))
                       ((NOT ?expr)
                        (display "(~ ")
                        (loop expr)
                        (display ")"))
                       ((APP ?fun . ?args)
                        (display-uclid-symbol fun)
                        (display "(")
                        (let ((first #t))
                          (for-each (lambda (child)
                                      (unless first (display ", "))
                                      (loop child)
                                      (set! first #f))
                                    args))
                        (display ")"))
                       ((ITE ?cond-expr ?then-expr ?else-expr)
                        (display "case ")
                        (loop cond-expr)
                        (display " : ")
                        (loop then-expr)
                        (display " ; default : ")
                        (loop else-expr)
                        (display "; esac"))
                       (TRUE
                        (display "1"))
                       (FALSE
                        (display "0"))
                       ((? number?)
                        (display-constant-prefix ast)
                        (display "uclid_ZERO")
                        (display-constant-suffix ast))
                       ((? symbol?)
                        (display-uclid-symbol ast))
                       (?-
                        (error 'cvc->uclid "unexpected ast" ast)))))))
    (print "MODEL example")
    (print "CONTROL")
    (print "EXTVAR")
    (print "STOREVAR")
    (print "VAR")
    (print "CONST")
    (print "uclid_ZERO : TERM;")
    ;; declare auxiliary variables
;     (let loop ((idx (- (num-aux-vars cmd-lst var-kind-table) 1)))
;       (when (>= idx 0)
;         (print "  " (gen-aux-name idx) " : TERM;")
;         (loop (- idx 1))))
    ;; declare constants
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?id BOOLEAN)
                   (display "  ")
                   (display-uclid-symbol id)
                   (print " : TRUTH;"))
                  ((DECL ?id (or REAL INTEGER))
                   (display "  ")
                   (display-uclid-symbol id)
                   (print " : TERM;"))
                  ((DECL ?id (FUNCTION-TYPE . ?types))
                   (let ((arity (- (length types) 1))
                         (range (car (reverse types))))
                     (display "  ")
                     (display-uclid-symbol id)
                     (display " : ")
                     (if (eq? range 'BOOLEAN)
                       (print "PRED[" arity "];")
                       (print "FUNC[" arity "];"))))))
              cmd-lst)
    ;; definitions
    (print "DEFINE")
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?id ?- ?def)
                   (display "  ")
                   (display-uclid-symbol id)
                   (display " := ")
                   (pp-ast def)
                   (print ";"))))
              cmd-lst)
    ;; main
    (print "EXEC")
    (for-each (lambda (cmd)
                (match-case cmd
                  ((ASSERT ?expr)
                   (queue/insert! assumptions expr))
                  ((QUERY ?expr)
                   (when found-check-valid?
                     (error 'cvc->uclid "Only one QUERY is supported..." #unspecified))
                   (print "decide(")
                   (unless (queue/empty? assumptions)
                     (display "(")
                     (let ((first? #t))
                       (for-each (lambda (assumption)
                                   (unless first?
                                     (display "  & "))
                                   (set! first? #f)
                                   (pp-ast assumption)
                                   (print ""))
                                 (queue->list assumptions))
                       (print ") => ")))
                     (pp-ast expr)
                     (print ");"))))
              cmd-lst)))
    
(define (display-esolver-type type)
  (match-case type
    (INTEGER
     (display "int"))
    (REAL
     (display "real"))
    (BOOLEAN
     (display "bool"))
    ((FUNCTION-TYPE . ?types)
     (display "(->")
     (for-each (lambda (t)
                 (display " ")
                 (display-esolver-type t))
               types)
     (display ")"))))

(define *esolver-op-table* '((ADD . +) (SUB . -) (MUL . *) (LT . <) (LE . <=) (GT . >) (GE . >=) (EQ . =) (NEQ . /=)
                             (AND . and) (OR . or) (XOR . xor) (IFF . =) (IMPLIES . =>) (ITE . ite) (NOT . not)))

(define (display-esolver-expr expr)
  (cond
   ((and (list? expr) (assq (car expr) *esolver-op-table*)) =>
    (lambda (entry)
      (display* "(" (cdr entry))
      (for-each (lambda (arg)
                  (display " ")
                  (display-esolver-expr arg))
                (cdr expr))
      (display ")")))
   ((and (list? expr) (eq? (car expr) 'APP))
    (display* "(" (cadr expr))
      (for-each (lambda (arg)
                  (display " ")
                  (display-esolver-expr arg))
                (cddr expr))
      (display ")"))
   ((eq? expr 'TRUE)
    (display "true"))
   ((eq? expr 'FALSE)
    (display "false"))
   (else
    (display expr))))

(define (cvc->esolver cmd-lst)
  (let* ((cmd-lst (cmds/ac->n-ary cmd-lst))
         (th-idx 1)
         (assumptions (make-queue)))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?id ?type)
                   (display* "(define " id "::")
                   (display-esolver-type type)
                   (print ")"))))
              cmd-lst)
    (for-each (lambda (cmd)
                (match-case cmd
                  ((ASSERT ?expr)
                   (queue/insert! assumptions expr))
                  ((DECL ?id ?type ?def)
                   (display* "(define " id "::")
                   (display-esolver-type type)
                   (display " ")
                   (display-esolver-expr def)
                   (print ")"))
                  ((QUERY ?expr)
                   (print "(theorem th" th-idx " ")
                   (let ((assumption-list (queue->list assumptions)))
                     (cond 
                      ((null? assumption-list)
                       (display-esolver-expr expr))
                      ((null? (cdr assumption-list))
                       (display* "  (=> ")
                       (display-esolver-expr (car assumption-list))
                       (display " ")
                       (display-esolver-expr expr)
                       (display ")"))
                      (else
                       (print "  (=> (and")
                       (for-each (lambda (a)
                                   (display "         ")
                                   (display-esolver-expr a)
                                   (print ""))
                                 assumption-list)
                       (print "      )")
                       (display "      ")
                       (display-esolver-expr expr)
                       (display ")"))))
                   (set! th-idx (+ th-idx 1))
                   (print ")"))))
              cmd-lst)))


(define (display-svc-id s aliases)
  (when (hashtable-get aliases s)
    (display "$"))
  (display-plain-symbol s "s_"))

(define *svc-op-table* '((ADD . +) (MUL . *) (LT . <) (LE . <=) (GT . >) (GE . >=) (EQ . =) (NEQ . /=)
                         (AND . AND) (OR . OR) (XOR . XOR) (IFF . <=>) (IMPLIES . =>) (ITE . ITE) (NOT . NOT)))

(define (display-svc-expr expr aliases)
  (let loop ((expr expr))
    (cond
     ((and (list? expr) (assq (car expr) *svc-op-table*)) =>
      (lambda (entry)
        (display* "(" (cdr entry))
        (for-each (lambda (arg)
                    (display " ")
                    (loop arg))
                  (cdr expr))
        (display ")")))
     ((and (list? expr) (eq? (car expr) 'APP))
      (display* "(" (cadr expr))
      (for-each (lambda (arg)
                  (display " ")
                  (loop arg))
                (cddr expr))
      (display ")"))
     ((and (list? expr) (eq? (car expr) 'SUB))
      (display "(+ ")
      (loop (cadr expr))
      (for-each (lambda (arg) 
                  (display " ")
                  (display "(* -1 ")
                  (loop arg)
                  (display " )"))
                (cddr expr))
      (display ")"))
     ((eq? expr 'TRUE)
      (display "TRUE"))
     ((eq? expr 'FALSE)
      (display "FALSE"))
     ((symbol? expr)
      (display-svc-id expr aliases))
     (else
      (display expr)))))

(define (display-svc-root-expr expr aliases)
  (when (or (symbol? expr) (number? expr))
    (display "("))
  (display-svc-expr expr aliases)
  (when (or (symbol? expr) (number? expr))
    (display ")")))

(define (cvc->svc cmd-lst)
  (let ((cmd-lst (cmds/ac->n-ary cmd-lst))
        (aliases (make-hashtable)))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?id ?- ?def)
                   (hashtable-put! aliases id #t))))
              cmd-lst)
    (for-each (lambda (cmd)
                (match-case cmd
                  ((ASSERT ?expr)
                   (display "assert ")
                   (display-svc-root-expr expr aliases)
                   (print ""))
                  ((DECL ?id ?type ?def)
                   (display "set ")
                   (display-svc-id id aliases)
                   (display " ")
                   (display-svc-root-expr def aliases)
                   (print ""))
                  ((QUERY ?expr)
                   (display "check_valid ")
                   (display-svc-root-expr expr aliases)
                   (print ""))))
              cmd-lst)
    (print "quit")))

(define (display-cvc-type type)
  (match-case type
    (INTEGER
     (display "REAL"))
    (REAL
     (display "REAL"))
    (BOOLEAN
     (display "BOOLEAN"))
    ((FUNCTION-TYPE . ?types)
     (cond
      ((= (length types) 2)
       (display "[ ")
       (display-cvc-type (car types))
       (display " -> ")
       (display-cvc-type (cadr types))
       (display " ]"))
      (else
       (display "[ [ ")
       (display-cvc-type (car types))
       (let loop ((types (cdr types)))
         (cond
          ((null? (cdr types))
           (display " ] -> ")
           (display-cvc-type (car types)))
          (else
           (display " , ")
           (display-cvc-type (car types))
           (loop (cdr types)))))
       (display " ]"))))))

(define *cvc-op-table* '((ADD . +) (SUB . -) (MUL . *) (LT . <) (LE . <=) (GT . >) (GE . >=) (EQ . =) (NEQ . /=)
                         (AND . AND) (OR . OR) (XOR . XOR) (IFF . <=>) (IMPLIES . =>) ))

(define (display-cvc-expr expr)
  (cond
   ((and (list? expr) (assq (car expr) *cvc-op-table*)) =>
    (lambda (entry)
      [assert (expr) (= (length expr) 3)]
      (display-infix (cdr entry) (cadr expr) (caddr expr) display-cvc-expr)))
   ((and (list? expr) (eq? (car expr) 'NOT))
    (display "(NOT ")
    (display-cvc-expr (cadr expr))
    (display ")"))
   ((and (list? expr) (eq? (car expr) 'ITE))
    (display "IF ")
    (display-cvc-expr (cadr expr))
    (display " THEN ")
    (display-cvc-expr (caddr expr))
    (display " ELSE ")
    (display-cvc-expr (cadddr expr))
    (display " ENDIF"))
   ((and (list? expr) (eq? (car expr) 'APP))
    (display* (cadr expr) "(" (caddr expr))
    (for-each (lambda (arg)
                (display " ,")
                (display-cvc-expr arg))
              (cdddr expr))
    (display ")"))
   ((eq? expr 'TRUE)
    (display "true"))
   ((eq? expr 'FALSE)
    (display "false"))
   (else
    (display expr))))


(define (cvc->cvc cmd-lst)
  (for-each (lambda (cmd)
              (match-case cmd
                ((DECL ?id ?type)
                 (display* id " : ")
                 (display-cvc-type type)
                 (print " ;"))))
            cmd-lst)
  (for-each (lambda (cmd)
              (match-case cmd
                ((ASSERT ?expr)
                 (display "ASSERT ")
                 (display-cvc-expr expr)
                 (print " ;"))
                ((DECL ?id ?type ?def)
                 (display* id " : ")
                 (display-cvc-type type)
                 (display " = ")
                 (display-cvc-expr def)
                 (print " ;"))
                ((QUERY ?expr)
                 (display "QUERY ")
                 (display-cvc-expr expr)
                 (print " ;"))))
            cmd-lst))

(define (cvc-info input-file ast)
  (let ((num-non-bool-vars 0)
        (num-bool-vars 0))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?- BOOLEAN)
                   (set! num-bool-vars (+ num-bool-vars 1)))
                  ((DECL ?- ?-)
                   (set! num-non-bool-vars (+ num-non-bool-vars 1)))))
              ast)
    (print (+ num-bool-vars num-non-bool-vars) " " (prefix input-file) " " num-bool-vars " " num-non-bool-vars)))

(define (collect-vars! expr already-found-vars)
  (let loop ((expr expr))
    (cond
     ((list? expr)
      (for-each loop (cdr expr)))
     ((symbol? expr)
      (hashtable-put! already-found-vars expr #t)))))
     
(define (contains-var? expr var)
  (bind-exit (exit)
    (let loop ((expr expr))
      (cond
       ((list? expr)
        (for-each loop (cdr expr)))
       ((symbol? expr)
        (when (eq? expr var)
          (exit #t)))))
    #f))

;; the following function fixes a misuse of the operator = where a <=> is expected.
(define (fix-cvc-definitions cmd-list)
  (let ((bool-vars (make-hashtable))
        (res-cmd-list (make-queue)))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?id BOOLEAN)
                   (hashtable-put! bool-vars id #t)
                   (queue/insert! res-cmd-list cmd))
                  ((ASSERT (EQ ?id ?body))
                   (cond
                    ((and (symbol? id) (hashtable-get bool-vars id))
                     (queue/insert! res-cmd-list `(ASSERT (IFF ,id ,body))))
                    (else
                     (queue/insert! res-cmd-list cmd))))
                  (else
                   (queue/insert! res-cmd-list cmd))))
              cmd-list)
    (queue->list res-cmd-list)))
                                         
(define (extract-definitions cmd-list)
  (let ((already-found-vars (make-hashtable))
        (definitions (make-hashtable))
        (tmp-cmd-list (make-queue)))
    (for-each (lambda (cmd)
                (let ((cmd-kind (car cmd)))
                  (case cmd-kind
                    ((ASSERT)
                     (let ((expr (cadr cmd)))
                       (match-case expr
                         ((EQ ?var ?body)
                          (if (and (symbol? var)
                                   (not (hashtable-get already-found-vars var))
                                   (not (contains-var? body var)))
                            (hashtable-put! definitions var body)
                            (queue/insert! tmp-cmd-list cmd)))
                         (?- 
                          (queue/insert! tmp-cmd-list cmd)))
                       (collect-vars! expr already-found-vars)))
                    (else
                     (queue/insert! tmp-cmd-list cmd)))))
              cmd-list)
    (let ((res-cmd-list (make-queue)))
      (for-each (lambda (cmd)
                  (match-case cmd
                    ((DECL ?id ?type)
                     (cond  
                      ((hashtable-get definitions id) =>
                       (lambda (def)
                         (queue/insert! res-cmd-list `(DECL ,id ,type ,def))))
                      (else
                       (queue/insert! res-cmd-list cmd))))
                    (else
                     (queue/insert! res-cmd-list cmd))))
                (queue->list tmp-cmd-list))
      (queue->list res-cmd-list))))

(define (extract-duplicate-decls cmd-list)
  (let ((res-cmd-list (make-queue))
        (already-declared (make-hashtable)))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((DECL ?id ?type)
                   (unless (hashtable-get already-declared id)
                     (hashtable-put! already-declared id #t)
                     (queue/insert! res-cmd-list cmd)))
                  (?-
                   (queue/insert! res-cmd-list cmd))))
              cmd-list)
    (queue->list res-cmd-list)))

(define *version* 1.0)

(define (main argv)
  (cvc/init-lexer!)
  (let ((output-file #f)
        (mode 'esolver)
        (input-file #f)
        (def-detection? #t))
    (args-parse (cdr argv)
      (section "Help")
      (("?")
       (args-parse-usage #f)
       (exit 0))
      ((("-h" "--help") (help "?,-h,--help" "This help message"))
       (args-parse-usage #f)
       (exit 0))
      (section "Misc")
      ((("-v" "--version") (help "Version number"))
       (print *version*)
       (exit 0))
      (("--ics" (help "Produce an ICS formula."))
       (set! mode 'ics))
      (("--uclid" (help "Produce an UCLID formula."))
       (set! mode 'uclid))
      (("--cvc" (help "Produce a CVC formula."))
       (set! mode 'cvc))
      (("--esolver" (help "Produce an esolver formula."))
       (set! mode 'esolver))
      (("--simplify" (help "Produce a Simplify formula."))
       (set! mode 'simplify))
      (("--svc" (help "Produce a SVC formula."))
       (set! mode 'svc))
      (("--real2int" (help "Convert real variables to integer variables."))
       (set! *real2int?* #t))
      (("--no-def-detection" (help "Disable definition detection."))
       (set! def-detection? #f))
      (("--info" (help "Produces information about the formula."))
       (set! mode 'info))
      (("-o" ?file (help "The output file"))
       (set! output-file file))
      (else
       (when input-file
         (print-error "Illegal argument `" else "'. Usage:")
         (args-parse-usage #f)
         (exit -1))
       (set! input-file else)))
    (unless input-file
      (sign-error "Usage: cvc-translator [options] cvc-file-name\nTry `cvc-translator --help' for more information.")) 
    (let* ((tmp-ast1 (try
                      (cvc/parse-file input-file)
                      (lambda (escape proc msg obj)
                        (sign-error "Error at line " *line*))))
           (tmp-ast2 (extract-duplicate-decls tmp-ast1))
           (ast (if def-detection? (extract-definitions tmp-ast2) tmp-ast2)))
      (with-output-to-port (if output-file
                             (open-output-file output-file)
                             (current-output-port))
        (lambda ()
          (case mode
            ((ics)
             (cvc->ics ast))
            ((uclid)
             (cvc->uclid ast))
            ((cvc)
             (cvc->cvc (fix-cvc-definitions ast)))
            ((svc)
             (cvc->svc (fix-cvc-definitions ast)))
            ((simplify)
             (cvc->simplify ast))
            ((info)
             (cvc-info input-file ast))
            (else
             (cvc->esolver ast))))))))