(module svc-translator
        (main main))

(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 *svc-keyword-list*
  '("and" "or" "not" "ite" "xor" "set" "quit" "check_valid" "TRUE" "FALSE"))

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

(define *line* 1)

(define *svc-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))
   ;; parenthesis
   (#\(
    (cons 'PAR-OPEN *line*))
   (#\)
    (cons 'PAR-CLO *line*))
   ;; numbers
   (num
    (cons 'CONSTANT (string->integer (the-string))))
   ((: #\- num)
    (cons 'CONSTANT (string->integer (the-string))))
   ;; op
   ((or "<=" ">=" "=>" "<=>" "/=")
    (cons (the-symbol) *line*))
   ((in #\* #\+ #\- #\/ #\% #\= #\< #\> #\~ #\:)
    (cons (the-symbol) *line*))
   ;; abv
   ((: #\$ (or id num))
    (cons 'ABV (the-symbol)))
   ;; identifiers
   (id
    (let* ((string   (the-string))
           (symbol   (string->symbol string))
           (upsymbol (string->symbol (string-upcase string))))
      (cond
       ((getprop symbol 'svc-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 *svc-parser* 
  (lalr-grammar
   (CONSTANT XOR OR AND NOT ITE + - = /= ABV PAR-OPEN PAR-CLO 
    < <= > >= => <=> SET ID QUIT CHECK_VALID TRUE FALSE)
   (start
    ((command-list) (reverse command-list)))
   (command-list
    (() '())
    ((command-list command) (cons command command-list)))
   (command
    ((SET ABV formula)
     `(SET ,ABV ,formula))
    ((QUIT) 'quit)
    ((CHECK_VALID formula) `(CHECK ,formula)))
   (formula
    ((ID) ID)
    ((CONSTANT) CONSTANT)
    ((ABV) ABV)
    ((TRUE) 'true)
    ((FALSE) 'false)
    ((PAR-OPEN formula PAR-CLO) formula)
    ((PAR-OPEN AND formula@f1 formula@f2 PAR-CLO) `(AND ,f1 ,f2))
    ((PAR-OPEN OR formula@f1 formula@f2 PAR-CLO) `(OR ,f1 ,f2))
    ((PAR-OPEN NOT formula PAR-CLO) `(NOT ,formula))
    ((PAR-OPEN => formula@f1 formula@f2 PAR-CLO) `(IMPLIES ,f1 ,f2))
    ((PAR-OPEN <=> formula@f1 formula@f2 PAR-CLO) `(IFF ,f1 ,f2))
    ((PAR-OPEN ITE formula@f1 formula@f2 formula@f3 PAR-CLO) `(ITE ,f1 ,f2 ,f3))
    ((PAR-OPEN + formula@f1 formula@f2 PAR-CLO) `(ADD ,f1 ,f2))
    ((PAR-OPEN - formula@f1 formula@f2 PAR-CLO) `(SUB ,f1 ,f2))
    ((PAR-OPEN < formula@f1 formula@f2 PAR-CLO) `(LT ,f1 ,f2))
    ((PAR-OPEN <= formula@f1 formula@f2 PAR-CLO) `(LE ,f1 ,f2))
    ((PAR-OPEN > formula@f1 formula@f2 PAR-CLO) `(GT ,f1 ,f2))
    ((PAR-OPEN >= formula@f1 formula@f2 PAR-CLO) `(GE ,f1 ,f2))
    ((PAR-OPEN = formula@f1 formula@f2 PAR-CLO) `(EQ ,f1 ,f2))
    ((PAR-OPEN /= formula@f1 formula@f2 PAR-CLO) `(NEQ ,f1 ,f2))
    ((PAR-OPEN ID formula-list PAR-CLO) (cons* 'UF ID (reverse formula-list)))
    )
   (formula-list
    ((formula) (list formula))
    ((formula-list formula) (cons formula formula-list)))
    ))

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

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

(define (svc/parse-file filename)
  (with-input-from-file
      filename
    svc/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 (collect-var-fun-kind cmd-lst)
  (let* ((var-table (make-hashtable))
         (abv-table (make-hashtable))
         (fun-table (make-hashtable))
         (process (lambda (ast expected-kind)
                    (let loop ((ast ast)
                               (expected-kind expected-kind))
                      (cond
                       ((list? ast)
                        (let ((c (car ast)))
                          (cond
                           ((memq c '(AND OR IMPLIES IFF NOT XOR))
                            (for-each (lambda (child)
                                        (loop child 'prop))
                                      (cdr ast)))
                           ((eq? c 'ITE)
                            [assert (ast) (= (length ast) 4)]
                            (loop (cadr ast) 'prop)
                            (loop (caddr ast) expected-kind)
                            (loop (cadddr ast) expected-kind))
                           ((eq? c 'UF)
                            (let ((fun (cadr ast))
                                  (args (cddr ast)))
                              (when expected-kind
                                (hashtable-put! fun-table fun (cons expected-kind (length args))))
                              (for-each (lambda (child)
                                          (loop child 'term))
                                        args)))
                           (else
                            (for-each (lambda (child)
                                        (loop child 'term))
                                      (cdr ast))))))
                       ((symbol? ast)
                        (let ((abv-body (hashtable-get abv-table ast)))
                          (when (and (not (hashtable-get var-table ast)) abv-body expected-kind)
                            (loop abv-body expected-kind))
                          (when expected-kind
                            (hashtable-put! var-table ast expected-kind)))))))))
    (for-each (lambda (cmd)
                (when (list? cmd)
                  (case (car cmd)
                    ((SET)
                     (hashtable-put! abv-table (cadr cmd) (caddr cmd))
                     (process (caddr cmd) #f))
                    ((CHECK)
                     (process (cadr cmd) 'prop)))))
              cmd-lst)
    (values var-table fun-table)))

(define (get-ast-kind ast var-kind-table)
  (cond
   ((list? ast)
    (case (car ast)
      ((ADD SUB UF) '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-bench-symbol s)
  (display "B")
  (let ((first? #t))
    (for-each (lambda (c)
                (cond
                 ((and first? (eq? c #\_))
                  (display "B_"))
                 ((or (char-alphabetic? c) (char-numeric? c) (eq? c #\_))
                  (display c))
                 (else
                  (display "B_")
                  (display (char->integer c))
                  (display "_")))
                (set! first? #f))
              (string->list (symbol->string s)))))

(define (svc->ics cmd-lst var-kind-table)
  (let* ((top-level-ite-list '())
         (idx 0)
         (next-aux-id (lambda () 
                        (let ((result idx))
                          (set! idx (+ idx 1))
                          result)))
         (ics-op-table '((ADD . +) (SUB . -) (LT . <) (LE . <=) (GT . >) (GE . >=) (EQ . =) (NEQ . <>)
                         (AND . "&") (OR . "|") (IFF . <=>) (IMPLIES . =>)))
         (found-check-valid? #f)
         (pp-ast (lambda (ast)
                   (let loop ((ast ast))
                     (cond 
                      ((list? ast)
                       (let ((c (car ast)))
                         (cond
                          ((memq c '(ADD SUB))
                           [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 'UF)
                           (display-bench-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))))
                                 (set! top-level-ite-list (cons top-ite top-level-ite-list))
                                 (hashtable-put! var-kind-table aux-var 'term)
                                 (display-bench-symbol aux-var))))))
                          (else
                           (error 'svc->ics "unexpected ast" ast)))))
                      ((eq? ast 'true)
                       (display 'tt))
                      ((eq? ast 'false)
                       (display 'ff))
                      ((symbol? ast)
                       (display-bench-symbol ast))
                      (else
                       (display ast)))))))
    (for-each (lambda (cmd)
                (when (list? cmd)
                  (case (car cmd)
                    ((SET)
                     (let* ((kind-var (hashtable-get var-kind-table (cadr cmd)))
                            (body (caddr cmd))
                            (kind-body (get-ast-kind body var-kind-table)))
                       (cond
                        ((eq? kind-var 'term)
                         (display "def ")
                         (display-bench-symbol (cadr cmd))
                         (display " := ")
                         (pp-ast body)
                         (print "."))
                        ((and (eq? kind-var 'prop) (eq? kind-body 'term))
                         (display "prop ")
                         (display-bench-symbol (cadr cmd))
                         (display " := [(")
                         (pp-ast body)
                         (print ") = true]."))
                        (else
                         (display "prop ")
                         (display-bench-symbol (cadr cmd))
                         (display " := ")
                         (pp-ast body)
                         (print ".")))))
                    ((CHECK)
                     (when found-check-valid?
                       (error 'svc->ics "Only one check_valid is supported..." #unspecified))
                     (set! found-check-valid? #t)
                     (print "sat ~[")
                     (pp-ast (cadr cmd))
                     (print "]")
                     (let loop ((top-ite-list top-level-ite-list))
                       (unless (null? top-ite-list)
                         (set! top-level-ite-list '())
                         (for-each (lambda (ite)
                                     (display " & ")
                                     (pp-ast ite))
                                   top-ite-list)
                         (loop top-level-ite-list)))
                     (print ".")
                     ))))
              cmd-lst)))

(define (collect-aliases cmd-list)
  (let ((alias-table (make-hashtable)))
    (for-each (lambda (cmd)
                (when (list? cmd)
                  (case (car cmd)
                    ((SET)
                     (hashtable-put! alias-table (cadr cmd) #t)))))
              cmd-list)
    alias-table))

(define (declare-esolver-unintepreted-consts var-kind-table alias-table)
  (hashtable-for-each var-kind-table
                      (lambda (var kind)
                        (unless (hashtable-get alias-table var)
                          (print "(define " var "::" (if (eq? kind 'prop) "bool" "int") ")")))))
                     
(define (declare-esolver-unintepreted-functions fun-kind-table)
  (hashtable-for-each fun-kind-table
                      (lambda (fun kind-arity)
                        (let ((kind (car kind-arity))
                              (arity (cdr kind-arity)))
                          (display* "(define " fun "::(-> ")
                          (let loop ((i 0))
                            (when (< i arity)
                              (display "int ")
                              (loop (+ i 1))))
                          (print (if (eq? kind 'prop) "bool" "int") "))")))))

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

(define (display-esolver-ast ast)
  (cond 
   ((list? ast)
    (let ((c (car ast)))
      (cond
       ((eq? c 'UF)
        (let ((fun (cadr ast))
              (args (cddr ast)))
          (display* "(" fun)
          (for-each (lambda (arg)
                      (display " ")
                      (display-esolver-ast arg))
                    args)
          (display ")")))
       (else
        [assert (c *esolver-op-table*) (assq c *esolver-op-table*)]
        (display* "(" (cdr (assq c *esolver-op-table*)))
        (for-each (lambda (arg)
                    (display " ")
                    (display-esolver-ast arg))
                  (cdr ast))
        (display ")")))))
   (else
    (display ast))))

(define (svc->esolver cmd-lst var-kind-table fun-kind-table)
  (let* ((alias-table (collect-aliases cmd-lst))
         (esolver-op-table '((ADD . +) (SUB . -) (LT . <) (LE . <=) (GT . >) (GE . >=) (EQ . =) (NEQ . <>)
                             (AND . "and") (OR . "or") (IFF . =) (IMPLIES . =>) (ITE . ite)))
         (thm-idx 1))
    (declare-esolver-unintepreted-consts var-kind-table alias-table)
    (declare-esolver-unintepreted-functions fun-kind-table)
    (for-each (lambda (cmd)
                (when (list? cmd)
                  (case (car cmd)
                    ((SET)
                     (let* ((var (cadr cmd))
                            (kind-var (hashtable-get var-kind-table var))
                            (body (caddr cmd)))
                       (display* "(define " var "::" (if (eq? kind-var 'prop) "bool" "int") " ")
                       (display-esolver-ast body)
                       (print ")")))
                    ((CHECK)
                     (display* "(theorem th" thm-idx " ")
                     (display-esolver-ast (cadr cmd))
                     (print ")")
                     (set! thm-idx (+ thm-idx 1))))))
              cmd-lst)))

(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) 'UF))
    (display-bench-symbol (cadr expr))
    (display "(")
    (display-cvc-expr (caddr expr))
    (for-each (lambda (arg)
                (display ", ")
                (display-cvc-expr arg))
              (cdddr 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"))
   ((symbol? expr)
    (display-bench-symbol expr))
   (else
    (display expr))))

(define (declare-cvc-unintepreted-consts var-kind-table alias-table)
  (hashtable-for-each var-kind-table
                      (lambda (var kind)
                        (unless (hashtable-get alias-table var)
                          (display-bench-symbol var)
                          (print " : " (if (eq? kind 'prop) "BOOLEAN" "REAL") ";")))))
                     
(define (declare-cvc-unintepreted-functions fun-kind-table)
  (hashtable-for-each fun-kind-table
                      (lambda (fun kind-arity)
                        (let ((kind (car kind-arity))
                              (arity (cdr kind-arity)))
                          (display-bench-symbol fun)
                          (display " : [ ")
                          (when (> arity 1)
                            (display "[ "))
                          (display "REAL")
                          (let loop ((i 0))
                            (when (< i (- arity 1))
                              (display ", REAL")
                              (loop (+ i 1))))
                          (when (> arity 1)
                            (display " ] "))
                          (display "-> ")
                          (print (if (eq? kind 'prop) "BOOLEAN" "REAL") " ];")))))


(define (svc->cvc cmd-lst var-kind-table fun-kind-table)
  (let ((alias-table (collect-aliases cmd-lst)))
    (declare-cvc-unintepreted-consts var-kind-table alias-table)
    (declare-cvc-unintepreted-functions fun-kind-table)
    (for-each (lambda (cmd)
                (when (list? cmd)
                  (case (car cmd)
                    ((SET)
                     (let* ((var (cadr cmd))
                            (kind-var (hashtable-get var-kind-table var))
                            (body (caddr cmd)))
                       (display-bench-symbol var)
                       (display* " : " (if (eq? kind-var 'prop) "BOOLEAN" "REAL") " = ")
                       (display-cvc-expr body)
                       (print ";")))
                    ((CHECK)
                     (display "QUERY ")
                     (display-cvc-expr (cadr cmd))
                     (print ";")))))
              cmd-lst)))

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

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

(define (uclid-infix-op? op)
  (assq op *uclid-op-table*))

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

(define (declare-uclid-unintepreted-consts var-kind-table alias-table)
  (hashtable-for-each var-kind-table
                      (lambda (var kind)
                        (unless (hashtable-get alias-table var)
                          (display-bench-symbol var)
                          (print " : " (if (eq? kind 'prop) "TRUTH" "TERM") ";")))))
                     
(define (declare-uclid-unintepreted-functions fun-kind-table)
  (hashtable-for-each fun-kind-table
                      (lambda (fun kind-arity)
                        (let ((kind (car kind-arity))
                              (arity (cdr kind-arity)))
                          (display-bench-symbol fun)
                          (print " : " (if (eq? kind 'prop) "PRED" "FUNC") "[" arity "];")))))

(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 `(SET ,aux-var (ITE ,@new-children)))
                             (hashtable-put! var-kind-table aux-var kind)
                             aux-var))
                          ((?tag . ?children)
                           `(,tag ,@(map loop children)))
                          (?-
                           expr))))))
    (for-each (lambda (cmd)
                (match-case cmd
                  ((SET ?id ?expr)
                   (queue/insert! new-cmd-lst `(SET ,id ,(ite->case expr))))
                  ((CHECK ?expr)
                   (queue/insert! new-cmd-lst `(CHECK ,(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 (display-uclid-expr 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))))
      (((? uclid-infix-op?) ?arg1 ?arg2)
       (display-infix (cdr (assq (car ast) *uclid-op-table*)) arg1 arg2 loop))
      ((NOT ?expr)
       (display "(~ ")
       (loop expr)
       (display ")"))
      ((UF ?fun . ?args)
       (display-bench-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-bench-symbol ast))
      (?-
       (error 'svc->uclid "unexpected ast" ast)))))

(define (svc->uclid cmd-lst var-kind-table fun-kind-table)
  (let* ((new-cmd-lst (process-ite-for-uclid cmd-lst var-kind-table))
         (alias-table (collect-aliases new-cmd-lst))
         (found-check-valid? #f))
    (print "MODEL example")
    (print "CONTROL")
    (print "EXTVAR")
    (print "STOREVAR")
    (print "VAR")
    (print "CONST")
    (print "uclid_ZERO : TERM;")
    (declare-uclid-unintepreted-consts var-kind-table alias-table)
    (declare-uclid-unintepreted-functions fun-kind-table)
    ;; definitions
    (print "DEFINE")
    (for-each (lambda (cmd)
                (match-case cmd
                  ((SET ?id ?def)
                   (display "  ")
                   (display-bench-symbol id)
                   (display " := ")
                   (display-uclid-expr def)
                   (print ";"))))
              new-cmd-lst)
    ;; main
    (print "EXEC")
    (for-each (lambda (cmd)
                (match-case cmd
                  ((CHECK ?expr)
                   (when found-check-valid?
                     (error 'svc->uclid "Only one CHECK is supported..." #unspecified))
                   (set! found-check-valid? #t)
                   (display "decide(")
                   (display-uclid-expr expr)
                   (print ");"))))
              new-cmd-lst)))

(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 *version* 2.0)

(define (main argv)
  (svc/init-lexer!)
  (let ((output-file #f)
        (mode 'ics)
        (input-file #f))
    (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))
      (("--cvc" (help "Produce a CVC formula."))
       (set! mode 'cvc))
      (("--uclid" (help "Produce an UCLID formula."))
       (set! mode 'uclid))
      (("--esolver" (help "Produce an esolver formula."))
       (set! mode 'esolver))
      (("-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: svc-translator [options] svc-file-name\nTry `svc-translator --help' for more information.")) 
    (let ((ast (try
                (svc/parse-file input-file)
                (lambda (escape proc msg obj)
                  (sign-error "Error at line " *line*)))))
      (multiple-value-bind
          (var-kind-table fun-kind-table)
          (collect-var-fun-kind ast)
        ;;(hashtable-for-each var-kind-table
        ;;                    (lambda (var kind)
        ;;                      (print var " -> " kind)))

        (with-output-to-port (if output-file
                               (open-output-file output-file)
                               (current-output-port))
          (lambda ()
            (case mode
              ((ics)
               (svc->ics ast var-kind-table))
              ((cvc)
               (svc->cvc ast var-kind-table fun-kind-table))
              ((uclid)
               (svc->uclid ast var-kind-table fun-kind-table))
              (else
               (svc->esolver ast var-kind-table fun-kind-table)))))))))