-- | contains all rule systems
module Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeqAlg (algPolySeq) where

import Language.Haskell.FreeTheorems.Variations.PolySeq.M
import Language.Haskell.FreeTheorems.Variations.PolySeq.AlgCommon
import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax

-- * Typing algorithm

polySeqTyping :: Cont -> Term -> M (Constraint,Typ)
polySeqTyping gamma t =
    case t of
      Var v        -> do{ tau <- getTypVarInCont gamma v;
			  superType tau
			}
      Abs v tau t' -> do{ (c1,tau2) <- polySeqTyping (addTermVar gamma (v,tau)) t';
			  (c2,tau1) <- subType tau;
			  lab       <- makeLabel;
			  return (Conj c1 c2, TArrow lab tau1 tau2)
			}
      App t1 t2    -> do{ (c1,tau12) <- polySeqTyping gamma t1;
			  (tau1,tau2)<- getArrowComps tau12;
			  (c2,tau1') <- polySeqTyping gamma t2;
			  c3         <- makeEqual tau1 tau1';
			  return (Conj (Conj c1 c2) c3,tau2)
			}
      TAbs tv t'   -> do{ lv <- makeLabel;
			  (c,tau) <- polySeqTyping (addTypVar gamma (tv,lv)) t';
			  return (c,TAll lv tv tau)
			}
      TApp t' tau  -> do{ c1           <- seqable gamma tau;
			  (c2,atau)    <- polySeqTyping gamma t';
			  (lab,tv,tau1)<- getAllComps atau;
			  (c3,tau3)    <- superType (substTyp tau1 tau tv);
			  return (Conj (Conj c2 c3) (Impl (Eq lab (LVal Epsilon)) c1),tau3)
			}
      Nil tau      -> do{ (c,tau') <- superType tau;
			  return (c,TList tau')
			}
      Cons t1 t2   -> do{ (c1,tau) <- polySeqTyping gamma t1;
			  (c2,ltau)<- polySeqTyping gamma t2;
			  tau'     <- getElemType ltau;
			  c3       <- makeEqual tau tau';
			  return (Conj (Conj c1 c2) c3,TList tau)
			}
      LCase t1 t2 v1 v2 t3 ->
                      do{ (c1,ltau)<- polySeqTyping gamma t1;
			  tau1     <- getElemType ltau;
			  (c2,tau2)<- polySeqTyping gamma t2;
			  (c3,tau2')<- polySeqTyping (addTermVar (addTermVar gamma (v1,tau1)) (v2,ltau)) t3;
			  c4       <- makeEqual tau2 tau2';
			  return (Conj (Conj (Conj c1 c2) c3) c4,tau2)
			}
      Fix t'       -> do{ (c1,tau)   <- polySeqTyping gamma t';
			  (tau1,tau2)<- getArrowComps tau;
			  c2         <- makeEqual tau1 tau2;
			  return (Conj c1 c2,tau1)
			}
      LSeq v t1 t2 -> do{ (c1,tau1) <- polySeqTyping gamma t1;
			  c2        <- seqable gamma tau1;
			  (c3,tau2) <- polySeqTyping (addTermVar gamma (v,tau1)) t2;
			  return (Conj (Conj c1 c2) c3, tau2)
			}
      Let  v t1 t2 -> do{ (c1,tau1) <- polySeqTyping gamma t1;
			  (c2,tau2) <- polySeqTyping (addTermVar gamma (v,tau1)) t2;
			  return (Conj c1 c2, tau2)
			}
      Seq t1 t2    -> do{ (c1,tau1) <- polySeqTyping gamma t1;
			  c2        <- seqable gamma tau1;
			  (c3,tau2) <- polySeqTyping gamma t2;
			  return (Conj (Conj c1 c2) c3, tau2)
			}
      I _          -> return (Tru,TInt)
      Add t1 t2    -> do{ (c1,tau1) <- polySeqTyping gamma t1;
			  isInt tau1;
			  (c2,tau2) <- polySeqTyping gamma t2;
			  isInt tau2;
			  return (Conj c1 c2,TInt)
			}
      T            -> return (Tru,TBool)
      F            -> return (Tru,TBool)
      BCase t1 t2 t3 -> do{ (_,tau1) <- polySeqTyping gamma t1; --the constraint will always be Tru
			    isBool tau1;
			    (c2,tau2) <- polySeqTyping gamma t2;
			    (c3,tau3) <- polySeqTyping gamma t3;
			    c4        <- makeEqual tau2 tau3;
			    return (Conj (Conj c2 c3) c4,tau2)
			  }

-- * seqable check

seqable :: Cont -> Typ -> M Constraint
seqable gamma tau =
    case tau of
      TVar tv              -> do{ lab <- getLabTVar gamma tv;
				  return (Eq (lab) (LVal Epsilon))
				}
      TArrow lab _  _    -> return (Eq lab (LVal Epsilon))
      TAll   _   tv tau' -> seqable (addTypVar gamma (tv,LVal Epsilon)) tau'
      TList  _           -> return Tru
      TInt               -> return Tru
      TBool              -> return Tru

-- * typ comparison

superType :: Typ -> M (Constraint,Typ)
superType tau =
    case tau of
      TVar tv              -> return (Tru,tau)
      TArrow lab tau1 tau2 -> do{ (c1,tau) <- subType tau1;
				  (c2,tau')<- superType tau2;
				  lab'     <- makeLabel;
				  return (Conj (Conj c1 c2) (Leq lab' lab),TArrow lab' tau tau')
				}
      TAll lab tv tau      -> do{ (c,tau') <- superType tau;
				  lab'     <- makeLabel;
				  return (Conj c (Leq lab lab'), TAll lab' tv tau')
				}
      TList tau            -> do{ (c,tau') <- superType tau;
				  return (c,TList tau')
				}
      TInt                 -> return (Tru,TInt)
      TBool                -> return (Tru,TBool)

subType :: Typ -> M (Constraint,Typ)
subType tau =
    case tau of
      TVar tv              -> return (Tru,tau)
      TArrow lab tau1 tau2 -> do{ (c1,tau) <- superType tau1;
				  (c2,tau')<- subType tau2;
				  lab'     <- makeLabel;
				  return (Conj (Conj c1 c2) (Leq lab lab'),TArrow lab' tau tau')
				}
      TAll lab tv tau      -> do{ (c,tau') <- subType tau;
				  lab'     <- makeLabel;
				  return (Conj c (Leq lab' lab), TAll lab' tv tau')
				}
      TList tau            -> do{ (c,tau') <- subType tau;
				  return (c,TList tau')
				}
      TInt                 -> return (Tru,TInt)
      TBool                -> return (Tru,TBool)

makeEqual :: Typ -> Typ -> M Constraint
makeEqual tau tau' =
    case tau of
      TVar tv              -> if tau' == TVar tv then return Tru else abort
      TArrow lab tau1 tau2 -> case tau' of
                                TArrow lab' tau1' tau2' -> do{ c1 <- makeEqual tau1 tau1';
							       c2 <- makeEqual tau2 tau2';
							       return (Conj (Conj c1 c2) (Eq lab lab'))
							     }
                                _                       -> abort
      TAll lab tv tau1     -> case tau' of
                                TAll lab' tv' tau1' -> if tv == tv'
						       then
						         do{ c <- makeEqual tau1 tau1';
							     return (Conj c (Eq lab lab'))
							   }
						       else abort
				_                   -> abort
      TList tau1           -> case tau' of
                                TList tau1' -> makeEqual tau1 tau1'
				_           -> abort
      TInt                 -> if tau' == TInt  then return Tru else abort
      TBool                -> if tau' == TBool then return Tru else abort

-- * main function

algPolySeq :: Term -> M (Term,Constraint,Typ)
algPolySeq t = do{ t'      <- annotate t;
		   (c,tau) <- polySeqTyping emptyCont t';
		   return (t',c,tau)
		 }