;; Example of typechecking

;;if this is #t a trace of the type deduction is shown
(set! *type-trace* #f)



#|
Type system symbols
|#
(set! *type-symbols* 
      '(lambda arg 
         or and not
         cons tree1 tree2 list list2 nil 
         rec up down void
         string symbol char boolean
         number integer))

#|
this is used as such in
Assume X : (or string symbol)

for:
(if (string? X) A B) 

X will be forced to be of type string in A
|#

(set! *predtypes*
     `((string?  ,(lambda () 'string  ))
       (symbol?  ,(lambda () 'symbol  ))
       (integer? ,(lambda () 'integer ))
       (number?  ,(lambda () 'number  ))
       (boolean? ,(lambda () 'boolean ))
       (pair?    ,(lambda () `(cons ,(gensym "A")  ,(gensym "B"))))
       (char?    ,(lambda () 'char    ))))


;;declaring type signatures for some common lambdas
(declare +     : (lambda (number number) number))
(declare -     : (lambda (number number) number))
(declare <     : (lambda (number number) boolean))

(declare cons  : (lambda (A B) (cons A B)))
(declare car   : (lambda ((cons A B)) A))
(declare cdr   : (lambda ((cons A B)) B))
(declare pair? : (lambda (A) boolean))

;;subtype declaration
(subtype integer  is-a  number)

;;tree recursive types
(define-recursive-type (tree1 A)    
  (or (and A (not (cons B C)))  
      (cons (tree1 A) (tree1 A))))

;; An alternative because A => (cons (tree A) (tree A)) 
;; we can use the alternative 
(define-recursive-type (tree2 A)    
  (or (cons (tree2 A) (tree2 A))
      A))

;; list like types follows similarly
(define-recursive-type (list A)    
  (or nil (cons A (list A))))

(define-recursive-type (list2 A B) 
  (or (cons A (list2 A B))
      B))
           


#|
subtype example
|#

#|
(define (twice X) (+ X X))
|#
(tdefine (twice X)
    (type (lambda (integer) number)
        (+ X X)))

#|
recursive tree examples
|#

(tdefine (rec1 X)
    (type (lambda ((tree1 char))  (tree1 char))
        (if (pair? X)
            (let ((Car (car X)))
              (if (pair? Car)
                  (car Car)
                  Car))
            X)))

(tdefine (rec2 X)
    (type (lambda ((tree1 A)) (tree1 A))
        (if (pair? X)
            (let ((Car (car X)))
              (if (pair? Car)
                  (car Car)
                  Car))
            X)))

(tdefine (rec2 X)
    (type (lambda ((tree2 A)) (tree2 A))
        (if (pair? X)
            (let ((Car (car X)))
              (if (pair? Car)
                  (car Car)
                  Car))
            X)))

(tdefine (rec3 X)
    (type (lambda ((tree2 A)) (tree2 A))
        (if (pair? X)
            (let ((Car (car X)))
              (if (pair? Car)
                  (rec2 (car Car))
                  (rec2 Car)))
            (rec2 X))))

;; Trying to compare infinite sequence types
(define-recursive-type (up A B)
  (or (cons A (up A B))
      (cons B (up A B))))

(define-recursive-type (down A B)
  (cons A (cons A (down B A))))
           

;; this will typecheck without a diving into an infinite loop


;; e.g. X : (down char number)  unified with (up char number)
(tdefine (down/up1 X)
  (type (lambda ((down char number)) (up char number))
    X))
;; similarly
(tdefine (down/up2 X)
  (type (lambda ((down A B)) (up A B))
    X))

;; look this does not typecheck wich shows that it works if
;; a type error is signaled
;; note X produces (down A B) which is more general production then allowed
;; by the func spec (up A A)
(catch 
 #t 
 (lambda ()  
   (tdefine (down/up3 X)
     (type (lambda ((down A B)) (up A A))
       X)))
 (lambda x 
   (format #t "OK, if this is a type error~%")))

;; A case lambda example
(tdefine  a-car
  (case-lambda
    ((A)   (type (lambda ((list number)) number) 
             (if (pair? A)
                 (car A)
                 0)))
    ((A B) (type (lambda ((list number) number) number)
             (if (pair? A)
                 (car A)
                 B)))))

(tdefine (car10 X)
  (type (lambda ((list number)) number)
    (a-car X 10)))

;; A letrec example
(tdefine (my-map F L)
  (type (lambda ((lambda (arg A) B) (list A)) (list B))
    (letrec ((H (lambda (L)
                  (type (lambda ((list A)) (list B))
                    (if (pair? L)
                        (cons (F (car L)) (H (cdr L)))
                        '())))))
      (H L))))

(tdefine (double-it L)
  (type (lambda ((list number)) (list number))
    (my-map (lambda (X)
              (type (lambda (number) number)
                (+ X X)))
            L)))

;; A little more complex letrec example
(tdefine (oddeven N)
  (type (lambda (number) number)
    (letrec ((Odd   (lambda (N M) 
                      (type (lambda (number number) number)
                        (Even (- N 1) M))))
             (Even  (lambda (N M) 
                      (type (lambda (number number) number)
                        (if (< N 0) 
                            M
                            (Odd (- N 1) (+ M 1)))))))
      (Even N 0))))


;buggy and by design set! sematics are weak but it's possible
;to use multiple types although it's a fragile construction so 
;try to avoid using this and keep a single type for a variable
(tdefine (myset X Y)
  (type (lambda (number symbol) symbol)
    (let ((A (type (or number symbol)
               1)))
      (set! A (+ X 1))
      (set! A Y)
      'ok)))