;;; The `prune' function removes instantiated type variables at the
;;; top level of a type.

;;; It returns an uninstantiated type variable or a type constructor.

(define-integrable (prune ntype)
  (if (ntyvar? ntype)
      (if (instantiated? ntype)
	  (prune-1 (ntyvar-value ntype))
	  ntype)
      ntype))

;;; This is because lucid can't hack inlining recursive fns.

(define (prune-1 x) (prune x))

(define-integrable (instantiated? ntyvar)
  (ntyvar-value ntyvar))
;  (not (eq? (ntyvar-value ntyvar) '#f)))  ;*** Lucid compiler bug?

(define (prune/l l)
  (map (function prune) l))


;;; These functions convert between AST types and gtypes.  Care is taken to
;;; ensure that the gtyvars are in the same order that they appear in the
;;; context.  This is needed to make dictionary conversion work right.

(define (ast->gtype context type)
  (mlet (((gcontext env) (context->gcontext context '() '()))
	 ((type env1) (type->gtype type env))
	 (gcontext-classes (arrange-gtype-classes env1 gcontext)))
    (**gtype gcontext-classes type)))

;;; This is similar except that the ordering of the tyvars is as defined in
;;; the data type.  This is used only for instance declarations and allows
;;; for simple context implication checks.  It also used by the signature
;;; of the dictionary variable.

(define (ast->gtype/inst context type)
  (mlet (((type env) (type->gtype type '()))
	 ((gcontext env1) (context->gcontext context '() env))
	 (gcontext-classes (arrange-gtype-classes env1 gcontext)))
    (**gtype gcontext-classes type)))

;;; This converts a context into gtype form [[class]]: a list of classes
;;; for each gtyvar.  This returns the context and the gtyvar environment.

(define (context->gcontext context gcontext env)
  (if (null? context)
      (values gcontext env)
      (mlet ((sym (context-tyvar (car context)))
	     (class (class-ref-class (context-class (car context))))
	     ((n new-env) (ast->gtyvar sym env))
	     (old-context (get-gtyvar-context n gcontext))
	     (new-context (merge-single-class class old-context))
	     (new-gcontext (cons (tuple n new-context) gcontext)))
	(context->gcontext (cdr context) new-gcontext new-env))))

;;; This assigns a gtyvar number to a tyvar name.

(define (ast->gtyvar sym env)
  (let ((res (assq sym env)))
    (if (eq? res '#f)
	(let ((n (length env)))
	  (values n (cons (tuple sym n) env)))
	(values (tuple-2-2 res) env))))

(define (get-gtyvar-context n gcontext)
  (cond ((null? gcontext)
	 '())
	((eqv? n (tuple-2-1 (car gcontext)))
	 (tuple-2-2 (car gcontext)))
	(else (get-gtyvar-context n (cdr gcontext)))))

(define (type->gtype type env)
  (if (tyvar? type)
      (mlet (((n env1) (ast->gtyvar (tyvar-name type) env)))
	(values (**gtyvar n) env1))
      (mlet (((types env1) (type->gtype/l (tycon-args type) env)))
	(values (**ntycon (tycon-def type) types) env1))))

(define (type->gtype/l types env)
  (if (null? types)
      (values '() env)
      (mlet (((type env1) (type->gtype (car types) env))
	     ((other-types env2) (type->gtype/l (cdr types) env1)))
	 (values (cons type other-types) env2))))

(define (arrange-gtype-classes env gcontext)
  (arrange-gtype-classes-1 0 (length env) env gcontext))

(define (arrange-gtype-classes-1 m n env gcontext)
  (if (equal? m n)
      '()
      (cons (get-gtyvar-context m gcontext)
	    (arrange-gtype-classes-1 (1+ m) n env gcontext))))

;;; These routines convert gtypes back to ordinary types.

(define (instantiate-gtype g)
 (mlet (((gtype _) (instantiate-gtype/newvars g)))
    gtype))

(define (instantiate-gtype/newvars g)
  (if (null? (gtype-context g))
      (values (gtype-type g) '())
      (let ((new-tyvars (create-new-tyvars (gtype-context g))))
	(values (copy-gtype (gtype-type g) new-tyvars) new-tyvars))))

(define (create-new-tyvars ctxts)
  (if (null? ctxts)
      '()
      (let ((tyvar (**ntyvar)))
	(setf (ntyvar-context tyvar) (car ctxts))
	(cons tyvar (create-new-tyvars (cdr ctxts))))))

(define (copy-gtype g env)
  (cond ((ntycon? g)
	 (**ntycon (ntycon-tycon g)
		   (map (lambda (g1) (copy-gtype g1 env))
			(ntycon-args g))))
	((ntyvar? g)
	 g)
	((gtyvar? g)
	 (list-ref env (gtyvar-varnum g)))
	((const-type? g)
	 (const-type-type g))))

;;; ntypes may contain synonyms.  These are expanded here.  Only the
;;; top level synonym is expanded.

(define (expand-ntype-synonym type)
  (if (and (ntycon? type)
	   (synonym? (ntycon-tycon type)))
      (let ((syn (ntycon-tycon type)))
	(expand-ntype-synonym
  	  (expand-ntype-synonym-1 (synonym-body syn)
				  (map (lambda (var val)
					 (tuple var val))
				       (synonym-args syn)
				       (ntycon-args type)))))
      type))

(define (expand-ntype-synonym-1 type env)
  (if (tyvar? type)
      (tuple-2-2 (assq (tyvar-name type) env))
      (**ntycon (tycon-def type)
		(map (lambda (ty) (expand-ntype-synonym-1 ty env))
		     (tycon-args type)))))

;;; This is used in generalization.  Note that ntyvars will remain when
;;; non-generic tyvars are encountered.

(define (ntype->gtype ntype)
  (mlet (((res _) (ntype->gtype/env ntype '())))
    res))

(define (ntype->gtype/env ntype required-vars)
  (mlet (((gtype env) (ntype->gtype-1 ntype required-vars)))
   (values 
    (make gtype (type gtype) (context (map (lambda (x) (ntyvar-context x))
					  env)))
    env)))

(define (ntype->gtype-1 ntype env)
 (let ((ntype (prune ntype)))
  (cond ((ntycon? ntype)
	 (mlet (((args env1) (ntype->gtype/l (ntycon-args ntype) env)))
	   (values (**ntycon (ntycon-tycon ntype) args) env1)))
	(else
	 (ntyvar->gtyvar ntype env)))))

(define (ntype->gtype/l types env)
  (if (null? types)
      (values '() env)
      (mlet (((type env1) (ntype->gtype-1 (car types) env))
	     ((types2 env2) (ntype->gtype/l (cdr types) env1)))
	(values (cons type types2) env2))))

(define (ntyvar->gtyvar ntyvar env)
  (if (non-generic? ntyvar)
      (values ntyvar env)
      (let ((l (list-pos ntyvar env)))
	(if (eq? l '#f)
	    (values (**gtyvar (length env)) (append env (list ntyvar)))
	    (values (**gtyvar l) env)))))
     
(define (list-pos x l)
  (list-pos-1 x l 0))

(define (list-pos-1 x l n)
  (cond ((null? l)
	 '#f)
	((eq? x (car l))
	 n)
	(else
	 (list-pos-1 x (cdr l) (1+ n)))))


;;; These utils are used in dictionary conversion.

(define (**dsel/method class method dict-code)
  (let ((pos (locate-in-list method (class-method-vars class) 0)))
    (**tuple-sel (class-dict-size class) pos dict-code)))

(define (**dsel/dict class dict-class dict-code)
  (let ((pos (locate-in-list
	      dict-class (class-super* class) (class-n-methods class))))
    (**tuple-sel (class-dict-size class) pos dict-code)))
  
(define (locate-in-list var l pos)
  (if (null? l)
      (error "Locate in list failed")
      (if (eq? var (car l))
	  pos
	  (locate-in-list var (cdr l) (1+ pos)))))

;;; These routines deal with contexts.  A context is a list classes.

;;; A context is normalized whenever class is a superclass of another.

(define (merge-contexts ctxt1 ctxt2)
  (if (null? ctxt1)
      ctxt2
      (merge-single-class (car ctxt1) (merge-contexts (cdr ctxt1) ctxt2))))

;;; This could perhaps avoid some consing but I don't imagine it would
;;; make much difference.

(define (merge-single-class class ctxt)
  (cond ((null? ctxt)
	 (list class))
	((eq? class (car ctxt))
	 ctxt)
	((memq class (class-super* (car ctxt)))
	 ctxt)
	((memq (car ctxt) (class-super* class))
	 (merge-single-class class (cdr ctxt)))
	(else
	 (cons (car ctxt) (merge-single-class class (cdr ctxt))))))

;;; This determines if ctxt2 is contained in ctxt1.

(define (context-implies? ctxt1 ctxt2)
  (or (null? ctxt2)
      (and (single-class-implies? ctxt1 (car ctxt2))
	   (context-implies? ctxt1 (cdr ctxt2)))))

(define (single-class-implies? ctxt class)
  (and (not (null? ctxt))
       (or (memq class ctxt)
	   (super-class-implies? ctxt class))))

(define (super-class-implies? ctxt class)
  (and (not (null? ctxt))
       (or (memq class (class-super* (car ctxt)))
	   (super-class-implies? (cdr ctxt) class))))

;;; This looks at the context of a full signature.

(define (full-context-implies? ctxt1 ctxt2)
  (or (null? ctxt1)
      (and (context-implies? (car ctxt1) (car ctxt2))
	   (full-context-implies? (cdr ctxt1) (cdr ctxt2)))))

;;; This is used to avoid type circularity on unification.

(define (occurs-in-type tyvar type) ; Cardelli algorithm
  (let ((type (prune type)))
    (if (ntyvar? type)
	(eq? type tyvar)
	(occurs-in-type/l tyvar (ntycon-args type)))))

; Does a tyvar occur in a list of types?
(define (occurs-in-type/l tyvar types)
  (if (null? types)
      '#f
      (or (occurs-in-type tyvar (car types))
	  (occurs-in-type/l tyvar (cdr types)))))

(define-integrable (non-generic? tyvar)
  (occurs-in-type/l tyvar (dynamic *non-generic-tyvars*)))

(define (collect-tyvars ntype)
  (collect-tyvars-1 ntype '()))

(define (collect-tyvars-1 ntype vars)
 (let ((ntype (prune ntype)))
  (if (ntyvar? ntype)
      (if (or (memq ntype vars) (non-generic? ntype))
	  vars
	  (cons ntype vars))
      (collect-tyvars/l-1 (ntycon-args ntype) vars))))

(define (collect-tyvars/l types)
  (collect-tyvars/l-1 types '()))

(define (collect-tyvars/l-1 types vars)
  (if (null? types)
      vars
      (collect-tyvars/l-1 (cdr types) (collect-tyvars-1 (car types) vars))))

;;; Random utilities

(define (decl-var decl)
  (var-ref-var (var-pat-var (valdef-lhs decl))))