(define-module  (language prolog typecheck equationalize)
  #:use-module (srfi srfi-1                    )
  #:use-module (ice-9 pretty-print             )  
  #:use-module (ice-9 match                    )  
  #:use-module (ice-9 receive                  )
  #:export (equationalize check))

;; the main function is equationalize, which takes a format that should be derived from 
;; tree-il representation with suitable tags to be able to communicate to the compiler
;; about type-checking conclusions. For know it's just a toy translator. The idea is to 
;; translate this code to a set of equations that later on is fed into the typechecker and
;; is a good starting point to see the type structure
;;
;; (equationalize Bindings Equations Code Outer-type)
;; To get the equations of (if 1 1 1) you would write 
;; (recieve (Bind Eq) (equationalize '() '() '(if 1 1 1) 'T-outer) ...)
;;
;; the language have just a few functions implemented for illustration
;; (number? X),(integer? X), (symbol? X), (char? X), (string? X)., (boolean? X).
;; plain simple (if X Y Z) (let Var Val Code) (lambda (x ...) code) is available as 
;; well. functions application should be written as (apply symbol? X).
;; and or and not is supported as is because they are special
;; 
;; So currently not that exciting but it is very instructive to play with a few expressions
;; an look att the corresponding equations that results. esiest is to use the check function
;; like (check Code) e.g. (check `(if 1 1 1)) which produces the type equation,

;;(if 1 1 1)
;;((or ((= 1 boolean) (= integer Texp))
;;     ((not (= 1 boolean)) (= integer Texp))))

;;Have a play!

(define (pp X)       (begin (pretty-print X) X))
(define union  (lambda (x y) (lset-union eq? x y)))

;;**************************** PRELUDE TO TYPECHECKING ***********************  

                            
;;This is just to kill of receive nesting buitifies the code alot

(define-syntax rlet
  (syntax-rules ()
    ((_ (((a ...) c) . l) code ...)
     (receive (a ...) c 
              (rlet l code ...)))
    ((_ ((a c) . l) code ...)
     (let ((a c)) 
       (rlet l code ...)))
    ((_ () code ...) (begin code ...))))


(define (compute-type Const Code)  
  (define (type? X) (and (symbol? X) (char-upper-case? (car (string->list (symbol->string X))))))
  (define (gen-map Code Bind Lam)
    (match Code
           ([X . L]     (gen-map X Bind (lambda (Bind) (gen-map L Bind Lam))))
           ((? type? X) (if (member X Bind)
                            (Lam Bind)
                            (let ((T (Const)))
                              (Lam (cons (cons X T) Bind)))))
           (_           (Lam Bind))))

  (define (make-rep X Bind)
    (match X
           ([X . L]  (cons (make-rep X Bind) (make-rep L Bind)))
           ([]       '[])
           (X        (let ((R (assoc-ref Bind X)))
                       (if R R X)))))
           
  (make-rep Code (gen-map Code '() (lambda (x) x))))

;;typecheck will create a list of equation that defines the rules for the predicates, the rules are
;; [= A B]           A and B should unify
;; [and A B] [A B]   A holds and B holds
;; [or A B]          A holds or B holds
;; [not A]           A is not true
;; [arg A]           A is an argument variable
;; [res A]           A is the result of a function
;;  e                Accepts everything
(define (equationalize Bind Eq Expr Tp)
  ;;(pp Expr)
  (match Expr
         (['let X V Code]   (rlet (((Bind Eq) (equationalize Bind Eq V X)))
                                  (equationalize (cons X Bind) Eq Code Tp  )))

         (['lambda V Code]  (rlet (( Tlam              (gensym "Tlam"))
                                   ((Bind-lam Eq-lam)  (equationalize (append V Bind) '() Code Tlam)))
                              (values Bind (cons `(= (lambda ,V ,Tlam ,Eq-lam) ,Tp) Eq))))
                               
         (['if P X Y]       (rlet ((F           (equationalize-bool Bind '() P))
                                   ((Bind1 Eq1) (F #t))
                                   ((Bind0 Eq0) (F #f))
                                   ((Bind1 Eq1) (equationalize Bind1 Eq1 X Tp))
                                   ((Bind0 Eq0) (equationalize Bind0 Eq0 Y Tp)))
                                (values (union Bind0 Bind1) (append `((or ,(reverse Eq1) ,(reverse Eq0))) Eq))))

         (['apply F A]      (rlet ((Ta        (map (lambda x (gensym "Targ")) A))
                                   (Tr        (gensym "Tres"))
                                   ((Bind Eq) (equationalize Bind Eq F `[lambda ,Ta ,Tr]))
                                   ((Bind Eq) (equationalize-arg Bind Eq A Ta)))
                               (values Bind (cons `[= [res ,Tr] ,Tp] Eq))))
         
         (['begin A]        (equationalize Bind Eq A Tp))
         (['begin A . L]    (rlet (((Bind Eq)  (equationalize Bind Eq A 'e)))
                                  (equationalize Bind Eq (cons 'begin L) Tp)))

         ((? symbol? X)     (if (member X Bind)
                                (values Bind (cons `(= ,X ,Tp) Eq))
                                (let ((Ts (symbol-property X ':type)))
                                  (if Ts
                                      (values Bind (cons `(= ,(compute-type (lambda () (gensym "T")) Ts) ,Tp) Eq))
                                      (values Bind (cons `(=  e ,Tp) Eq))))))
         
         (('quote (? symbol?))  (values Bind (cons `(= symbol    ,Tp) Eq)))
         ((? integer?)          (values Bind (cons `(= integer   ,Tp) Eq)))
         ((? boolean?)          (values Bind (cons `(= boolean   ,Tp) Eq)))
         ((? number? )          (values Bind (cons `(= number    ,Tp) Eq)))
         ((? char?   )          (values Bind (cons `(= character ,Tp) Eq)))
         ((? string? )          (values Bind (cons `(= string    ,Tp) Eq)))))

(define (check X)
  (rlet ((A          X)
         ((Ba Ea)   (equationalize '() '() A 'Texp)))
        (pp A)
        (pp (reverse Ea)))
  #t)

(define typemap  '((+ (lambda (number number) number))
                   (id (lam (A) A))
                   (- (lambda (number number) number))))

(map (lambda (x) (match x ((Sym T)  (set-symbol-property! Sym ':type T))))
     typemap)


(define (equationalize-arg Bind Eq Xs Tps)
  (match `(,Xs ,Tps)
         (([X . Xs] [Tp . Tps])   (rlet (((Bind Eq)  (equationalize Bind Eq X (list 'arg Tp))))
                                      (equationalize-arg Bind Eq Xs Tps)))
         (([]       []        )   (values Bind Eq))))


(define *predtypes*
  '((string?  string  )
    (symbol?  symbol  )
    (integer? integer )
    (number?  number  )
    (boolean? boolean )
    (char?    char    )))
  

(define (equationalize-bool Bind Eq Expr)
  (define (pred? X)
    (define (f L)
      (if (pair? L)
          (if (eq? X (caar L))
              #t
              (f (cdr L)))
          #f))
    (f *predtypes*))

  (define (type-of-pred X)
    (define (f L)
      (if (pair? L)
          (if (eq? X (caar L))
              (cadar L)
              (f (cdr L)))
          #f))
    (f *predtypes*))

  ;;(pk Expr)
  (match Expr
         (['and X Y]   (let ((F1 (equationalize-bool Bind Eq X))
                             (F2 (equationalize-bool Bind Eq Y)))
                         (lambda (X) 
                           (if X 
                               (rlet (((Bind1 Eq1) (F1 #t))
                                      ((Bind2 Eq2) (F2 #t)))
                                  (values (union Bind1 Bind2) `(and ,Eq1 ,Eq2)))
                               (rlet (((Bind1 Eq1) (F1 #f))
                                      ((Bind2 Eq2) (F2 #f)))
                                  (values (union Bind1 Bind2) `(or  ,Eq1 ,Eq2)))))))

         (['or X Y]    (let ((F1 (equationalize-bool Bind Eq X))
                             (F2 (equationalize-bool Bind Eq Y)))
                         (lambda (X) 
                           (if X 
                               (rlet (((Bind1 Eq1) (F1 #t))
                                      ((Bind2 Eq2) (F2 #t)))
                                  (values (union Bind1 Bind2) `(or ,Eq1 ,Eq2)))
                               (rlet (((Bind1 Eq1) (F1 #f))
                                      ((Bind2 Eq2) (F2 #f)))
                                  (values (union Bind1 Bind2) `(and  ,Eq1 ,Eq2)))))))

         (['not  X ]   (let ((F (equationalize-bool Bind Eq X)))
                         (lambda (X)
                           (if X (F #f) (F #t)))))

         ([(? pred? String?) X] (lambda (P)
                                  (if P 
                                      (equationalize Bind Eq X `(validated ,(type-of-pred String?)))
                                      (equationalize Bind Eq X `(validated (not ,(type-of-pred String?)))))))
         (X                     (lambda (P)
                                  (if P
                                      (values Bind (cons `[= ,X boolean] Eq))
                                      (values Bind (cons `[not [= ,X boolean]] Eq)))))))