(module base-env mzscheme
  
  (require-for-template (only (lib "list.ss") foldl)
                        mzscheme
                        "extra-procs.ss"
                        #%paramz
                        (lib "match-error.ss" "mzlib" "private" "match"))

  
  (require
   "types.ss"
   (only (lib "list.ss") foldl)
   "types-aux.ss"
   #%paramz
   (lib "match-error.ss" "mzlib" "private" "match"))

     
  (provide initial-env)
  
  (define-syntax (make-env stx)
    (syntax-case stx ()
      [(_ (nm ty) ...)
       #`(list (list #'nm ty) ...)]))
  
  (define -Pathlike (Un -Path -String))
  (define -Pathlike* (Un (-val 'up) (-val 'same) -Path -String))
  
  (define initial-env
    (let ([make-lst make-Listof]
          [make-lst/elements -pair])
      (make-env
       
       (car (make-poly (list 'a 'b) (cl-> [((make-lst (make-tvar 'a))) (make-tvar 'a)]
                                          [((make-pair-ty (make-tvar 'a) (make-tvar 'b))) (make-tvar 'a)])))
       (cadr (make-poly (list 'a) (-> (make-lst (make-tvar 'a)) (make-tvar 'a))))
       (caddr (-poly (a) (-> (-lst a) a)))
       (cadddr (-poly (a) (-> (-lst a) a)))
       (cdr (make-poly (list 'a 'b) (cl-> [((make-lst (make-tvar 'a))) (make-lst (make-tvar 'a))]
                                          [((make-pair-ty (make-tvar 'a) (make-tvar 'b))) (make-tvar 'b)])))
       (cddr (make-poly (list 'a) (-> (make-lst (make-tvar 'a)) (make-lst (make-tvar 'a)))))
       (cons (-poly (a b) 
                    (cl-> [(a (-lst a)) (-lst a)]
                          [(a b) (-pair a b)])))
       
       (null? (make-pred-ty (make-value null)))
       [null (make-value null)]
       (atom? (make-pred-ty A))
       (number? (make-pred-ty N))
       (boolean? (make-pred-ty B))
       (add1 (-> N N))
       (sub1 (-> N N))
       (eq? (-> Univ Univ B))
       (eqv? (-> Univ Univ B))
       (equal? (-> Univ Univ B))
       (even? (-> N B))
       [gensym (cl-> [(Sym) Sym]
                     [() Sym])]
       [string-append (->* null -String -String)]
       [open-input-string (-> -String -Port)]
       [read (cl-> 
              [(-Port) -Sexp]
              [() -Sexp])]
       [ormap (-poly (a) ((-> a Univ) (-lst a) . -> . (Un (-val #f) a)))]
       [andmap (-poly (a) ((-> a Univ) (-lst a) . -> . (Un (-val #f) a)))]
       [newline (-> -Void)]
       [not (-> B B)]
       [cons? (make-pred-ty (-pair Univ Univ))]
       [pair? (make-pred-ty (-pair Univ Univ))]
       [empty? (make-pred-ty (make-value null))]
       [empty (make-value null)]
       [string? (make-pred-ty -String)]
       [symbol? (make-pred-ty Sym)]
       [list? (make-pred-ty (-lst Univ))]
       [list (-poly (a) (->* '() a (-lst a)))]
       [procedure? (make-pred-ty (->* '() (Un) Univ))]
       [map 
        (-poly (a b c)
               (cl-> [((-> a b) (-lst a)) (-lst b)]
                     [((-> a b c) (-lst a) (-lst b)) (-lst c)]))]
       [for-each 
        (-poly (a b c)
               (cl-> [((-> a b) (-lst a)) -Void]
                     [((-> a b c) (-lst a) (-lst b)) -Void]))]
       [foldl (make-poly '(a b) 
                         (-> (-> (make-tvar 'a) (make-tvar 'b) (make-tvar 'b)) (make-tvar 'b) (make-lst (make-tvar 'a)) (make-tvar 'b)))]
       
       [call-with-values (-poly (a b) (-> (-> a) (-> a b) b))]
       
       (error 
        (make-funty (list 
                     (make-arr null Dyn)
                     (make-arr (list Sym -String) Dyn Univ)
                     (make-arr (list -String) Dyn Univ)
                     (make-arr (list Sym) Dyn))))
       
       [integer? (Univ . -> . B)]
       [namespace-variable-value 
        (cl-> 
         [(Sym) Univ]
         [(Sym B -Namespace (-> Univ)) Univ])]
        
       (match:error (Dyn . -> . Dyn))
       (display (Univ . -> . -Void))
       [void (->* '() Univ -Void)]
       [void? (make-pred-ty -Void)]
       [printf (->* (list -String) Univ -Void)]
       [format (->* (list -String) Univ -String)]   
       (fst (make-poly (list 'a 'b) (-> (make-lst/elements (make-tvar 'a) (make-tvar 'b)) (make-tvar 'a))))
       (snd (make-poly (list 'a 'b) (-> (make-lst/elements (make-tvar 'a) (make-tvar 'b)) (make-tvar 'b))))
       
       (= (->* (list N N) N B))
       (>= (->* (list N N) N B))
       (< (->* (list N N) N B))
       (<= (->* (list N N) N B))
       [> (->* (list N) N B)]
       (zero? (N . -> . B))
       (* (->* '() N N))
       (/ (->* (list N) N N))
       (+ (->* '() N N))
       (- (->* (list N) N N))
       (max (->* (list N) N N))
       (min (->* (list N) N N))
       [values  (make-poly '(a) (-> (make-tvar 'a) (make-tvar 'a)))]
       [vector-ref 
        (make-poly (list 'a) ((make-vec (make-tvar 'a)) N . -> . (make-tvar 'a)))]
       [build-vector (make-poly (list 'a) (N (N . -> . (make-tvar 'a)) . -> . (make-vec (make-tvar 'a))))]
       [reverse (make-poly '(a) (-> (make-lst (make-tvar 'a)) (make-lst (make-tvar 'a))))]
       [append (-poly (a) (->* (list) (-lst a) (-lst a)))]
       [length (make-poly '(a) (-> (make-lst (make-tvar 'a)) N))]
       [memq (make-poly (list 'a) (-> (make-tvar 'a) (make-lst (make-tvar 'a)) (Un (make-value #f) (make-lst (make-tvar 'a)))))]
       [memv (make-poly (list 'a) (-> (make-tvar 'a) (make-lst (make-tvar 'a)) (Un (make-value #f) (make-lst (make-tvar 'a)))))]
       [member (make-poly (list 'a) (-> (make-tvar 'a) (make-lst (make-tvar 'a)) (Un (make-value #f) (make-lst (make-tvar 'a)))))]
       
       [string<? (->* (list -String -String) -String B)]
       [string>? (->* (list -String -String) -String B)]
       [string=? (->* (list -String -String) -String B)]
       [string<=? (->* (list -String -String) -String B)]
       [string>=? (->* (list -String -String) -String B)]

       [string-ci<? (->* (list -String -String) -String B)]
       [string-ci>? (->* (list -String -String) -String B)]
       [string-ci=? (->* (list -String -String) -String B)]
       [string-ci<=? (->* (list -String -String) -String B)]
       [string-ci>=? (->* (list -String -String) -String B)]
       
       [string-upcase (-> -String -String)]
       [string-downcase (-> -String -String)]
       [string-titlecase (-> -String -String)]
       [string-foldcase (-> -String -String)]
       
       [string-normalize-nfd (-> -String -String)]
       [string-normalize-nfkd (-> -String -String)]
       [string-normalize-nfc (-> -String -String)]
       [string-normalize-nfkc (-> -String -String)]
       
       [assq (-poly (a) (-> Univ (-lst (-pair Univ a)) a))]

       [build-path ((list -Pathlike*) -Pathlike* . ->* . -Path)]
       [string->number (-> -String N)]
       [with-input-from-file (-poly (a) (-Pathlike (-> a) . -> . a))]
       
       [random (cl->
                [(N) N]
                [() N])]
       
       [list-ref (-poly (a) ((-lst a) N . -> . a))]
       [positive? (-> N B)]
       [negative? (-> N B)]
       [odd? (-> N B)]
       [even? (-> N B)]
       
       [apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
       
       [call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
       [call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
       
       [quotient (N N . -> . N)]
       [remainder (N N . -> . N)]
       [quotient/remainder (N N . -> . (-values (list N N)))]
       
       ;; parameter stuff
       
       [parameterization-key Sym]
       [extend-parameterization (-poly (a b) (-> Univ (-Param a b) a Univ))]
       [continuation-mark-set-first (-> (Un (-val #f) -Cont-Mark-Set) Univ Univ)]
       [make-parameter (-poly (a b) (cl-> [(a) (-Param a a)]
                                         [(b (a . -> . b)) (-Param a b)]))]
       [current-directory (-Param -Pathlike -Path)]
       [current-namespace (-Param -Namespace -Namespace)]
       
       ;; regexp stuff
       [regexp-match (-> -String -String (Un (-val #f) (-lst (Un (-val #f) -String))))]
       
       [number->string (N . -> . -String)]
       
       [current-milliseconds (-> N)]
       [modulo (N N . -> . N)]
       
       ;; errors
       
       [raise-type-error
        (cl->
         [(Sym -String Univ) (Un)]
         [(Sym -String N (-lst Univ)) (Un)])]
       
       ;; this is a hack
       
       [match:error ((list) Univ . ->* . (Un))]
       
       [vector-set! (-poly (a) (-> (make-vec a) N a -Void))]
       
       [vector->list (-poly (a) (-> (make-vec a) (-lst a)))]
       [list->vector (-poly (a) (-> (-lst a) (make-vec a)))]
       [exact? (N . -> . B)]
       [expt (N N . -> . N)]
       [vector (-poly (a) (->* (list) a (make-vec a)))]
       [real? (Univ . -> . B)]
       [exact->inexact (N . -> . N)]
       [inexact->exact (N . -> . N)]
       [make-string
        (cl->
         [(N) -String]
         [(N -Char) -String])]
       [string-set! (-String N -Char . -> . -Void)]
       [make-vector
        (-poly (a)
               (cl->
                [(N) (make-vec N)]
                [(N a) (make-vec a)]))]
       
       
       
       )))

  )