(module dec-translator
        (main main))

(define *dec-keyword-list*
  '("if" "then" "else" "end" "true" "false"))

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

(define *line* 1)

(define *int-vars?* #f)

(define *dec-lexer*
  (regular-grammar
   ((nonzero-digit (in ("19"))))
   ((in #\newline #a012)
    (set! *line* (+ *line* 1))
    (ignore))
   ((+ (in #\space #\tab))
    (ignore))
   ;; OR
   (#\|
    (cons 'OR *line*))
   ;; AND
   (#\&
    (cons 'AND *line*))
   ;; parenthesis
   (#\(
    (cons 'PAR-OPEN *line*))
   (#\)
    (cons 'PAR-CLO *line*))
   ;; integer constant
   ((+ digit)
    (cons 'CONSTANT (string->integer (the-string))))
   ((or "<=" ">=" "->" "<->" "<>")
    (cons (the-symbol) *line*))
   ;; operators
   ((in #\* #\+ #\- #\/ #\% #\= #\< #\> #\~ #\:)
    (cons (the-symbol) *line*))
   ((: (or #\' #\_ alpha) (* (or #\' #\_ alpha digit)))
    (let* ((string   (the-string))
           (symbol   (string->symbol string))
           (upsymbol (string->symbol (string-upcase string))))
      (cond
       ((getprop symbol 'dec-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 *dec-parser* 
  (lalr-grammar
   ;;tokens
   ((left: * / %)
    (left: + -)
    (left: = <> >= <= > <)
    (none: ~)
    (left: AND)
    (left: OR)
    (right: ->)
    (left: <->)
    CONSTANT PAR-OPEN PAR-CLO ID CONST IF THEN ELSE END TRUE FALSE)
   (start 
    ((expr) expr))
   (expr
    ((TRUE) 'true)
    ((FALSE) 'false)
    ((PAR-OPEN expr PAR-CLO) expr)
    ((expr@e1 AND expr@e2) `(AND ,e1 ,e2))
    ((expr@e1 OR expr@e2) `(OR ,e1 ,e2))
    ((expr@e1 -> expr@e2) `(IMPLIES ,e1 ,e2))
    ((expr@e1 <-> expr@e2) `(IFF ,e1 ,e2))
    ((expr@e1 + expr@e2) `(ADD ,e1 ,e2))
    ((expr@e1 - expr@e2) `(SUB ,e1 ,e2))
    ((- expr) `(SUB 0 ,expr))
    ((IF expr@e1 THEN expr@e2 ELSE expr@e3 END) `(ITE ,e1 ,e2 ,e3))
    ((~ expr) `(NOT ,expr))
    ((expr@e1 = expr@e2) `(EQ ,e1 ,e2))
    ((expr@e1 <> expr@e2) `(NEQ ,e1 ,e2))
    ((expr@e1 > expr@e2) `(GT ,e1 ,e2))
    ((expr@e1 >= expr@e2) `(GE ,e1 ,e2))
    ((expr@e1 < expr@e2) `(LT ,e1 ,e2))
    ((expr@e1 <= expr@e2) `(LE ,e1 ,e2))
    ((ID) ID)
    ((CONSTANT) CONSTANT))))

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

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

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

(define (collect-var-types ast)
  (let ((table (make-hashtable)))
    (let loop ((ast ast)
               (expected-type 'bool))
      (cond
       ((list? ast)
        (let ((c (car ast)))
          (cond
           ((memq c '(ADD SUB GT GE LT LE EQ NEQ))
            (for-each (lambda (child) (loop child 'real))
                      (cdr ast)))
           ((eq? c 'ITE)
            [assert (ast) (= (length ast) 4)]
            (loop (cadr ast) 'bool)
            (loop (caddr ast) expected-type)
            (loop (cadddr ast) expected-type))
           (else
            (for-each (lambda (child) (loop child 'bool))
                      (cdr ast))))))
       ((symbol? ast)
        (unless (memq ast '(true false))
          (hashtable-put! table ast expected-type)))))
    table))

(define (ast-type ast var-type-table)
  (cond
   ((list? ast)
    (let ((c (car ast)))
      (cond
       ((memq c '(ADD SUB))
        'real)
       ((eq? c 'ITE)
        [assert (ast) (= (length ast) 4)]
        (ast-type (caddr ast) var-type-table))
       (else
        'bool))))
   ((memq ast '(true false))
    'bool)
   ((symbol? ast)
    (let ((type (hashtable-get var-type-table ast)))
      [assert (type) type]
      type))
   ((number? ast)
    'real)
   (else
    (error 'ast-type "unexpected ast" ast))))

(define (display-infix-core op arg-list o-par c-par loop)
  (display o-par)
  (loop (car arg-list))
  (for-each (lambda (arg)
              (display* " " op " ")
              (loop arg))
            (cdr arg-list))
  (display c-par))

(define (display-infix op arg-list loop)
  (display-infix-core op arg-list "(" ")" loop))

(define (display-infix-prop op arg-list loop)
  (display-infix-core op arg-list "[" "]" loop))

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

(define (dec->ics ast var-type-table)
  (print "sat ")
  (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 . =>)))
         (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)) (cdr 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)) (cdr ast) loop))
                          ((eq? c 'NOT)
                           [assert (ast) (= (length ast) 2)]
                           (display "[~ ")
                           (loop (cadr 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? (ast-type then-expr var-type-table) 'bool)
                               (display "[if ") 
                               (loop cond-expr)
                               (display " then ")
                               (loop then-expr)
                               (display " else ")
                               (loop else-expr)
                               (display " end]"))
                              (else
                               [assert (then-expr) (eq? (ast-type then-expr var-type-table) 'real)]
                               (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-type-table aux-var 'real)
                                 (display aux-var))))))
                          (else
                           (error 'dec->ics "unexpected ast" ast)))))
                      ((eq? ast 'true)
                       (display 'tt))
                      ((eq? ast 'false)
                       (display 'ff))
                      ((symbol? ast)
                       (display-ics-symbol ast))
                      (else
                       (display ast)))))))
    (pp-ast ast)
    (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 " .")
    ))

(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 *cvc-op-table* '((ADD . +) (SUB . -) (LT . <) (LE . <=) (GT . >) (GE . >=) (EQ . =) (NEQ . /=)
                         (AND . AND) (OR . OR) (XOR . XOR) (IFF . <=>) (IMPLIES . =>) ))

(define (dec->cvc ast var-type-table)
  (hashtable-for-each var-type-table
                      (lambda (var type)
                        (print "CVC_" var " : " (cond
                                                 ((eq? type 'bool) 
                                                  "BOOLEAN")
                                                 (else "REAL"))
                               ";")))
  (print "QUERY NOT(")
  (let loop ((ast ast))
    (cond 
     ((list? ast)
      (let ((c (car ast)))
        (cond
         ((memq c '(ADD SUB OR AND IMPLIES IFF LT LE GT GE EQ NEQ))
          (display-infix (cdr (assq c *cvc-op-table*)) (cdr ast) loop))
         ((eq? c 'NOT)
          [assert (ast) (= (length ast) 2)]
          (display "(NOT ")
          (loop (cadr ast))
          (display ")"))
         ((eq? c 'ITE)
          [assert (ast) (= (length ast) 4)]
          (let ((cond-expr (cadr ast))
                (then-expr (caddr ast))
                (else-expr (cadddr ast)))
            (display "IF ") 
            (loop cond-expr)
            (display " THEN ")
            (loop then-expr)
            (display " ELSE ")
            (loop else-expr)
            (display " ENDIF")))
         (else
          (error 'mathsat->cvc "unexpected ast" ast)))))
     ((eq? ast 'true)
      (display "TRUE"))
     ((eq? ast 'false)
      (display "FALSE"))
     ((symbol? ast)
      (display* "CVC_" ast))
     (else
      (display ast))))
  (print " );"))

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

(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 (dec->esolver ast var-type-table)
  (let ((ast (ac->n-ary ast)))
    (hashtable-for-each var-type-table
                        (lambda (var type)
                          (print "(define " var "::" (cond
                                                      ((eq? type 'bool) 
                                                       "bool")
                                                      (*int-vars?* "int")
                                                      (else "real"))
                                 ")")))
    (print "(theorem th1 (not ")
    (let loop ((ast ast))
      (cond
       ((list? ast)
        (display* "(" (cdr (assq (car ast) *esolver-op-table*)))
        (for-each (lambda (arg)
                    (display " ")
                    (loop arg))
                  (cdr ast))
        (display ")"))
       (else
        (display ast))))
    (print "))")))

(define (dec->uclid ast var-type-table)
  (sign-error "Feature not implemented."))

(define *version* 1.0)

(define (main argv)
  (dec/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))
      (("--int" (help "Use integer variables."))
       (set! *int-vars?* #t))
      (("--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: dec-translator [options] dec-file-name\nTry `dec-translator --help' for more information.")) 
    (let* ((ast (try
                 (dec/parse-file input-file)
                 (lambda (escape proc msg obj)
                   (sign-error "Error at line " *line*))))
           (var-type-table (collect-var-types ast)))
      (with-output-to-port (if output-file
                             (open-output-file output-file)
                             (current-output-port))
        (lambda ()
          (case mode
            ((ics)
             (dec->ics ast var-type-table))
            ((uclid)
             (dec->uclid ast var-type-table))
            ((cvc)
             (dec->cvc ast var-type-table))
            (else
             (dec->esolver ast var-type-table))))))))