-- UUAGC 0.9.50.2 (build/103/lib-ehc/UHC/Light/Compiler/AnaDomain.ag)
module UHC.Light.Compiler.AnaDomain(QualAGItf (..), TyAGItf (..), CoeAGItf (..)
, AnaEval (..), AnaEvalL, RelevTy (..), RelevTyL, MbRelevTy, RelevQual (..), RelevQualL, RelevCoe (..), RelevCoeL
, RQuant (..)
, RelevQualS
, (<.>)
, relevtyAnaEval
, AnaLattice (..)
, freshStrict, freshLazy
, anaMkBotFun
, relevCoeUnCompose
, relevCoeToComposeList
, RVarMpInfo (..)
, rvmiMbEval
, RVarMp, emptyRVarMp
, rvarmpEvalUnit
, rvarmpKeysSet, rvarmpUnions
, AnaMatchState (..), AMS, emptyAnaMatchState
, AMSOut (..), emptyAMSOut, amsoMkOk
, amsLE, amsRunMb) where

import UHC.Light.Compiler.Base.HsName.Builtin
import UHC.Light.Compiler.Base.Common
import UHC.Light.Compiler.Opts.Base
import UHC.Light.Compiler.VarMp
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List
import Data.Maybe
import Control.Monad.State
import Control.Applicative
import UHC.Util.Utils
import UHC.Light.Compiler.Base.Debug
import UHC.Util.Pretty
import Control.Monad hiding (join)
import UHC.Util.Serialize
import UHC.Util.Control.Monad (liftM6)
import Data.Typeable (Typeable)
import Data.Generics (Data)





















-- | quantifier for RelevTy_Fun
data RQuant
  = RQuant_Forall		-- the usual universal instantiation
  | RQuant_Rec			-- quantified for mutual recursive use, instantiates differently
  | RQuant_None			-- not quantified
  deriving
    ( Eq, Ord, Enum
    , Typeable, Data
    )



instance Show RQuant where
  show RQuant_Forall 	= "A"
  show RQuant_Rec 		= "R"
  show RQuant_None    	= ""



type RelevQualS = Set.Set RelevQual



infixl 3 `RelevCoe_Comp`
infixl 3 <.>

-- | smart variant of RelevCoe_Comp
(<.>) :: RelevCoe -> RelevCoe -> RelevCoe
RelevCoe_Id           <.> r                   = r
l                     <.> RelevCoe_Id         = l
RelevCoe_Eval   ll lr <.> RelevCoe_Eval rl rr
  | lr == rl                                  = RelevCoe_Eval ll rr
RelevCoe_CastTy ll (RelevTy_Ana lr)
                      <.> RelevCoe_Eval rl rr
  | lr == rl                                  = RelevCoe_CastTy ll (RelevTy_Ana rr)
l                     <.> RelevCoe_Comp rl rr = (l <.> rl) `RelevCoe_Comp` rr
RelevCoe_Comp   ll lr <.> r                   = ll `RelevCoe_Comp` (lr <.> r)
l                     <.> r                   = RelevCoe_Comp l r



relevtyAnaEval (RelevTy_Ana e) = e
relevtyAnaEval _               = panic "AnaDomain.relevtyAnaEval"



class AnaLattice a where
  top   :: a
  bot   :: a

  isTop :: a -> Bool
  isBot :: a -> Bool
  isVar :: a -> Maybe UID

  fresh :: UID -> a

  meetl  :: a -> a -> AMS (Maybe a)
  joinl  :: a -> a -> AMS (Maybe a)

  -- base <= base
  leBB_l :: a -> a -> AMS (AMSOut a)
  leBB_r :: a -> a -> AMS (AMSOut a)
  leBB_l = leBB
  leBB_r = leBB

  -- base <= base
  leBB :: a -> a -> AMS (AMSOut a)
  leBB = leBB_l

  -- base <= fun, default compares to fun result
  leBF :: a -> [a] -> a -> AMS (AMSOut a)
  leBF b fa fr = leBB b fr



-- | wrap action inside var looking up
anaVar
  :: AnaLattice x
     => (UID -> AnaMatchState -> Maybe x)       -- lookup
     -> res                          			-- when vars are equal anyway
     -> (x -> AMS res)                          -- when var found
     -> (x -> x -> AMS res)                     -- when var is not found
     -> UID -> x -> x
     -> AMS res
anaVar lkupVar dflt found notfound v1 a1 a2
  = do { s <- get
       ; let isV2@(~(Just v2)) = isVar a2
       ; if isJust isV2 && v1 == v2
         then return dflt
         else case lkupVar v1 s of
                Just a1' -> found    a1'
                _        -> notfound a1 a2
       }

anaBind
  :: (UID -> x -> RVarMp)
     -> (x -> res)
     -> UID -> x
     -> AMS res
anaBind mkVM mkRes v1 a2
  = do { s <- get
       ; put (amsBind (mkVM v1) a2 s)
       ; return $ mkRes a2
       }



instance AnaLattice AnaEval where
  top   = AnaEval_Lazy
  bot   = AnaEval_WHNF

  isTop AnaEval_Lazy = True
  isTop _            = False

  isBot AnaEval_WHNF = True
  isBot _            = False

  isVar (AnaEval_Var v) = Just v
  isVar _               = Nothing

  fresh = AnaEval_Var

  meetl a1@(AnaEval_Var v1) a2              = anaVar amsLookupEval (Just a1) (meetl a2) anaEvalMeet v1 a1 a2
  meetl a1 a2@(AnaEval_Var v2)              = anaVar amsLookupEval (Just a1) (meetl a1) anaEvalMeet v2 a2 a1
  meetl a1 a2                               = anaEvalMeet a1 a2

  joinl a1@(AnaEval_Var v1) a2              = anaVar amsLookupEval (Just a1) (joinl a2) anaEvalJoin v1 a1 a2
  joinl a1 a2@(AnaEval_Var v2)              = anaVar amsLookupEval (Just a1) (joinl a1) anaEvalJoin v2 a2 a1
  joinl a1 a2                               = anaEvalJoin a1 a2

  leBB_l a1@(AnaEval_Var v1) a2             = anaVar amsLookupEval (amsoMkOk a1 a1 $ RelevCoe_Eval a1 a1) (flip leBB_l a2)       leBB_r     v1 a1 a2
  leBB_l a1 a2                              = leBB_r a1 a2
  leBB_r a1 a2@(AnaEval_Var v2)             = anaVar amsLookupEval (amsoMkOk a1 a1 $ RelevCoe_Eval a1 a1) (     leBB_r a1) (flip anaEvalLE) v2 a2 a1
  leBB_r a1 a2                              = anaEvalLE a1 a2




-- | meet or join for 2 element lattice (only bot+top), nothing in between
anaMeetOrJoin
  :: AnaLattice x
     => (UID -> x -> RVarMp)		-- make var mapping (subst)
     -> Bool						-- is meet (True) or join (False)
     -> x -> x
     -> AMS (Maybe x)
anaMeetOrJoin mkVM isM a1 a2
  = mt False a1 a2
  where mt flip a1 a2
          | isB && isM  = return $ Just a1
          | isB         = return $ Just a2
          | isT && isM  = return $ Just a2
          | isT         = return $ Just a1
          | not flip    = mt True a2 a1
          | isJust m1 && isJust m2
                        = do { s <- get
                             ; let bound = amsBoundS s
                             ;      if not (v1 `Set.member` bound) then bind v1 a2
                               else if not (v2 `Set.member` bound) then bind v2 a1
                               else return Nothing
                             }
          | otherwise   = return Nothing
                        where m1@(~(Just v1)) = isVar a1
                              m2@(~(Just v2)) = isVar a2
                              -- areV = isJust m1 && isJust m2
                              isB  = isBot a1
                              isT  = isTop a1
        bind = anaBind mkVM Just

-- | meet, join, specialized for AnaEval
anaEvalMeet, anaEvalJoin :: AnaEval -> AnaEval -> AMS (Maybe AnaEval)
anaEvalMeet = anaMeetOrJoin rvarmpEvalUnit True
anaEvalJoin = anaMeetOrJoin rvarmpEvalUnit False

anaEvalLE :: AnaEval -> AnaEval -> AMS (AMSOut AnaEval)
anaEvalLE a1 a2
  = le a1 a2
  where le a1@(AnaEval_Var v1) a2@(AnaEval_WHNF  )   = bind  v1 a2                        -- can't get lower than bot
        le a1@(AnaEval_Var v1) a2                    = delay a1 a2                        -- rest is delayed
        le a1@(AnaEval_Lazy  ) a2@(AnaEval_Var v2)   = bind  v2 a1                        -- can't get higher than top
        le a1                  a2@(AnaEval_Var v2)   = delay a1 a2                        -- rest is delayed
        le a1@(AnaEval_WHNF  ) a2@(AnaEval_WHNF  )   = return $ amsoMkOk a1 a2 (RelevCoe_Eval a1 a2)
        le a1@(AnaEval_WHNF  ) a2@(AnaEval_Lazy  )   = coe   a1 a2                        -- forget that it is alreay evaluated
        le a1@(AnaEval_Lazy  ) a2@(AnaEval_Lazy  )   = return $ amsoMkOk a1 a2 (RelevCoe_Eval a1 a2)
        le a1@(AnaEval_Lazy  ) a2@(AnaEval_WHNF  )   = coe' RelevCoe_Cast a1 a2           -- permitted, but not without marking as casting required, according to lattice
        le a1                  a2                    = return $ amsoMkFail -- Ok a1 a2 (RelevCoe_Err "anaEvalLE")

        bind = anaBind rvarmpEvalUnit (\a2 -> amsoMkOk a2 a2 $ RelevCoe_Eval a2 a2)

        -- | coerce
        coe' wrap l h = return $ amsoMkOk l h (RelevCoe_Eval l h)
        coe = coe' id

        -- | postpone by generating a qualification, to be solved later, or to end up in a signature
        delay l h
          = do { s <- get
               ; put (amsQual (RelevQual_SubEval l h) s)
               ; return $ amsoMkOk l h (RelevCoe_Eval l h)
               }



-- | Only valid for RelevTy_Ana as aggregrate of domains
instance AnaLattice RelevTy where
  top       = RelevTy_Ana top
  bot       = RelevTy_Ana bot

  isTop (RelevTy_Ana a1) = isTop a1
  isBot (RelevTy_Ana a1) = isBot a1
  isVar _                = Nothing
  -- isVar (RelevTy_Ana a1) = do { v1 <- isVar a1 ; return v1 }

  fresh u   = RelevTy_Ana (fresh u1)
            where (_,u1) = mkNewLevUID u

  meetl  (RelevTy_Ana a11) (RelevTy_Ana a21) = liftM (fmap RelevTy_Ana) (meetl  a11 a21)
  meetl  _                 _                 = return Nothing

  joinl  (RelevTy_Ana a11) (RelevTy_Ana a21) = liftM (fmap RelevTy_Ana) (joinl  a11 a21)
  joinl  _                 _                 = return Nothing

  leBB  (RelevTy_Ana a11) (RelevTy_Ana a21) = do { AMSOut l h c True <- leBB a11 a21
                                                 ; return $ amsoMkOk (RelevTy_Ana l) (RelevTy_Ana h) c
                                                 }
  leBB  (RelevTy_Fun _ _ _ a1 r1) (RelevTy_Fun _ _ _ a2 r2)
                                            = do { r_amso <- leBB r1 r2
                                                 ; a_amso <- mapM (uncurry leBB) (zip a2 a1)
                                                 ; return $ amsoMk (RelevTy_Fun  RQuant_None [] [] (map amsoHi  a_amso) (amsoLo  r_amso))
                                                                   (RelevTy_Fun  RQuant_None [] [] (map amsoLo  a_amso) (amsoHi  r_amso))
                                                                   (RelevCoe_Fun                   (map amsoCoe a_amso) (amsoCoe r_amso))
                                                                   (and $ amsoIsOk r_amso : map amsoIsOk a_amso)
                                                 }
  -- others lead to a constraint between t1 and function result, with a coercion between t1 and whole function t2
  -- Note: this has to be delegated to actual AnaDomain...
  {-
  leBB  t1 t2@(RelevTy_Fun _ _ a2 r2)
                                            = do { f_amso <- leBF t1 a2 r2
                                                 ; let t1' = anaMkBotFun (length a2)
                                                 ; return $ AMSOut (RelevTy_Fun  [] [] (map amsoHi  a_amso) (amsoLo  r_amso))
                                                                   (RelevTy_Fun  [] [] (map amsoLo  a_amso) (amsoHi  r_amso))
                                                                   (RelevCoe_Fun       (map amsoCoe a_amso) (amsoCoe r_amso))
                                                 }
  -}
  leBB  _                 _                 = return $ amsoMkFail -- Ok (RelevTy_Err "leBB.lo") (RelevTy_Err "leBB.hi") (RelevCoe_Err "leBB")

  {-
  leBB  (RelevTy_Ana a11) (RelevTy_Ana a21) = do { AMSOut l h c <- leBB a11 a21
                                                 ; return $ AMSOut (RelevTy_Ana l) (RelevTy_Ana h) c
                                                 }
  leBB  _                 _                 = return $ AMSOut (RelevTy_Err "leBB.lo") (RelevTy_Err "leBB.hi") (RelevCoe_Err "leBB")
  -}



-- | bottom only for AnaEval lattice, otherwise fresh
freshStrict :: UID -> RelevTy
freshStrict u
  = case fresh u of
      RelevTy_Ana _ -> RelevTy_Ana bot

-- | top only for AnaEval lattice, otherwise fresh
freshLazy :: UID -> RelevTy
freshLazy u
  = case fresh u of
      RelevTy_Ana _ -> RelevTy_Ana top



-- | construct 'worst case' assuming function signature, where we assume function assumes nothing and we cannot assume anything about result, except for the result being bottom (i.e. strict)
anaMkBotFun :: Int -> RelevTy
anaMkBotFun arity = RelevTy_Fun RQuant_None [] [] (replicate arity top) bot



-- | decompose RelevCoe composition in top and below
relevCoeUnCompose :: RelevCoe -> (RelevCoe,[RelevCoe])
relevCoeUnCompose (RelevCoe_Comp l r)
  = (l, u r)
  where u (RelevCoe_Comp l r) = l : u r
        u c                   = [c]
relevCoeUnCompose c = (c, [])



-- | decompose RelevCoe composition in list of subsequently applied coe's
relevCoeToComposeList :: RelevCoe -> [RelevCoe]
relevCoeToComposeList c
  = u [] c
  where u a (RelevCoe_Comp l r) = let a' = u a r in u a' l
        u a c                   = [c] ++ a



data RVarMpInfo             -- for all types of Var alternatives an alternative here
  = RVMIEval    AnaEval



rvmiMbEval :: RVarMpInfo -> Maybe AnaEval
rvmiMbEval (RVMIEval x) = Just x
-- for now, until more alternatives are in it
-- rvmiMbEval _            = Nothing



type RVarMp  = VarMpStk' UID RVarMpInfo

emptyRVarMp :: RVarMp
emptyRVarMp = emptyVarMpStk



rvarmpEvalUnit :: UID -> AnaEval -> RVarMp
-- poor mens occurcheck...
-- rvarmpEvalUnit v (AnaEval_Var v2) | v == v2  = emptyRVarMp
rvarmpEvalUnit v i                           = varmpstkUnit v (RVMIEval i)  -- [mkVarMp (Map.fromList [(v,RVMIEval i)])]



-- | renaming
rvarmpKeysSet :: RVarMp -> Set.Set UID
rvarmpKeysSet = varmpstkKeysSet

rvarmpUnions :: [RVarMp] -> RVarMp
rvarmpUnions = varmpstkUnions



-- | state maintained during matching
data AnaMatchState
  = AnaMatchState
      { amsBoundS           :: !UIDS        -- vars which are already bound
      , amsOuterVarMp       :: !RVarMp      -- as known from outside matching
      , amsLocalVarMp       :: !RVarMp      -- as gathered during a match (1 invocation of runState)
      , amsGathQual         :: !RelevQualS  -- gathered constraints
      }

type AMS    a = State AnaMatchState a

emptyAnaMatchState :: AnaMatchState
emptyAnaMatchState = AnaMatchState Set.empty emptyRVarMp emptyRVarMp Set.empty

instance Show AnaMatchState where
  show x = "AMS " ++ s (amsOuterVarMp x) ++ s (amsLocalVarMp x)
    where s m = show (assocLMapElt rvmiMbEval $ varmpstkToAssocL m)



-- | direct (non state) output of matching
data AMSOut a
  = AMSOut
      { amsoLo      :: a
      , amsoHi      :: a
      , amsoCoe     :: RelevCoe
      , amsoIsOk	:: Bool
      }

emptyAMSOut :: AnaLattice a => AMSOut a
emptyAMSOut = AMSOut bot top RelevCoe_Id True

amsoMk :: a -> a -> RelevCoe -> Bool -> AMSOut a
amsoMk l h c ok = AMSOut l h c ok

amsoMkOk :: a -> a -> RelevCoe -> AMSOut a
amsoMkOk l h c = amsoMk l h c True

amsoMkFail :: AnaLattice a => AMSOut a
amsoMkFail = emptyAMSOut {amsoIsOk = False}

instance Show a => Show (AMSOut a) where
  show x = "AMSOut (" ++ show (amsoLo x) ++ " <= " ++ show (amsoHi x) ++ ")"



amsBind :: (x -> RVarMp) -> x -> AnaMatchState -> AnaMatchState
amsBind b a s = s {amsLocalVarMp = b a |+> amsLocalVarMp s}

amsQual :: RelevQual -> AnaMatchState -> AnaMatchState
amsQual q s = s {amsGathQual = Set.insert q (amsGathQual s)}



-- | run leBB
amsLE :: AnaLattice x => RVarMp -> x -> x -> (AMSOut x,AnaMatchState)
amsLE m x1 x2 = runState (leBB x1 x2) (emptyAnaMatchState {amsOuterVarMp = m})

-- | run a Maybe returning AMS
amsRunMb :: AnaMatchState -> AMS (Maybe x) -> Maybe (x,AnaMatchState)
amsRunMb s ams
  = case runState ams s of
      (Just x, s) -> Just (x,s)
      _           -> Nothing



-- | Lookup in VarMp's of AnaMatchState
amsLookup :: UID -> AnaMatchState -> Maybe RVarMpInfo
amsLookup i s = varmpLookup i (amsOuterVarMp s) <|> varmpLookup i (amsLocalVarMp s)

amsLookupEval :: UID -> AnaMatchState -> Maybe AnaEval
amsLookupEval i s = do { i <- amsLookup i s ; rvmiMbEval i }



instance Serialize RQuant where
  sput = sputEnum8
  sget = sgetEnum8

instance Serialize RelevQual where
  sput (RelevQual_SubEval a b        ) = sputWord8 0 >> sput a >> sput b
  -- sput (RelevQual_Alt     a b c d e f) = sputWord8 1 >> sput a >> sput b >> sput c >> sput d >> sput e >> sput f
  sget
    = do t <- sgetWord8
         case t of
            0 -> liftM2 RelevQual_SubEval         sget sget
            -- 1 -> liftM6 RelevQual_Alt             sget sget sget sget sget sget

instance Serialize RelevTy where
  sput (RelevTy_Ana   a        ) = sputWord8 0 >> sput a
  sput (RelevTy_Fun   a b c d e) = sputWord8 1 >> sput a >> sput b >> sput c >> sput d >> sput e
  sput (RelevTy_None           ) = sputWord8 2
  sput (RelevTy_Err   a        ) = sputWord8 3 >> sput a
  sget
    = do t <- sgetWord8
         case t of
            0 -> liftM  RelevTy_Ana         sget
            1 -> liftM5 RelevTy_Fun         sget sget sget sget sget
            2 -> return RelevTy_None
            3 -> liftM  RelevTy_Err         sget

instance Serialize RelevCoe where
  sput (RelevCoe_Id             ) = sputWord8 0
  sput (RelevCoe_Err     a      ) = sputWord8 1 >> sput a
  sput (RelevCoe_Comp    a b    ) = sputWord8 2 >> sput a >> sput b
  sput (RelevCoe_Fun     a b    ) = sputWord8 3 >> sput a >> sput b
  sput (RelevCoe_Cast    a      ) = sputWord8 4 >> sput a
  sput (RelevCoe_Eval    a b    ) = sputWord8 5 >> sput a >> sput b
  sput (RelevCoe_CastTy  a b    ) = sputWord8 6 >> sput a >> sput b
  sget
    = do t <- sgetWord8
         case t of
            0 -> return RelevCoe_Id
            1 -> liftM  RelevCoe_Err         sget
            2 -> liftM2 RelevCoe_Comp        sget sget
            3 -> liftM2 RelevCoe_Fun         sget sget
            4 -> liftM  RelevCoe_Cast        sget
            5 -> liftM2 RelevCoe_Eval        sget sget
            6 -> liftM2 RelevCoe_CastTy      sget sget

instance Serialize AnaEval where
  sput (AnaEval_Var   a      ) = sputWord8 0 >> sput a
  sput (AnaEval_WHNF         ) = sputWord8 1
  sput (AnaEval_Lazy         ) = sputWord8 2
  sput (AnaEval_Meet  a      ) = sputWord8 3 >> sput a
  sput (AnaEval_Join  a      ) = sputWord8 4 >> sput a
  sget
    = do t <- sgetWord8
         case t of
            0 -> liftM  AnaEval_Var         sget
            1 -> return AnaEval_WHNF
            2 -> return AnaEval_Lazy
            3 -> liftM  AnaEval_Meet        sget
            4 -> liftM  AnaEval_Join        sget

-- AnaEval -----------------------------------------------------
data AnaEval = AnaEval_Var {av_AnaEval_Var :: !(UID)}
             | AnaEval_WHNF {}
             | AnaEval_Lazy {}
             | AnaEval_Meet {opnds_AnaEval_Meet :: !(AnaEvalL)}
             | AnaEval_Join {opnds_AnaEval_Join :: !(AnaEvalL)}
             deriving ( Data,Eq,Ord,Show,Typeable)
-- AnaEvalL ----------------------------------------------------
type AnaEvalL = [AnaEval]
-- CoeAGItf ----------------------------------------------------
data CoeAGItf = CoeAGItf_AGItf {relevCoe_CoeAGItf_AGItf :: !(RelevCoe)}
              deriving ( Data,Eq,Ord,Show,Typeable)
-- MbRelevTy ---------------------------------------------------
type MbRelevTy = Maybe (RelevTy)
-- QualAGItf ---------------------------------------------------
data QualAGItf = QualAGItf_AGItf {relevQual_QualAGItf_AGItf :: !(RelevQual)}
               deriving ( Data,Eq,Ord,Show,Typeable)
-- RelevCoe ----------------------------------------------------
data RelevCoe = RelevCoe_Id {}
              | RelevCoe_Err {str_RelevCoe_Err :: !(String)}
              | RelevCoe_Comp {l_RelevCoe_Comp :: !(RelevCoe),r_RelevCoe_Comp :: !(RelevCoe)}
              | RelevCoe_Fun {args_RelevCoe_Fun :: !(RelevCoeL),res_RelevCoe_Fun :: !(RelevCoe)}
              | RelevCoe_Cast {coe_RelevCoe_Cast :: !(RelevCoe)}
              | RelevCoe_CastTy {l_RelevCoe_CastTy :: !(RelevTy),r_RelevCoe_CastTy :: !(RelevTy)}
              | RelevCoe_Eval {from_RelevCoe_Eval :: !(AnaEval),to_RelevCoe_Eval :: !(AnaEval)}
              deriving ( Data,Eq,Ord,Show,Typeable)
-- RelevCoeL ---------------------------------------------------
type RelevCoeL = [RelevCoe]
-- RelevQual ---------------------------------------------------
data RelevQual = RelevQual_SubEval {l_RelevQual_SubEval :: !(AnaEval),r_RelevQual_SubEval :: !(AnaEval)}
               deriving ( Data,Eq,Ord,Show,Typeable)
-- RelevQualL --------------------------------------------------
type RelevQualL = [RelevQual]
-- RelevTy -----------------------------------------------------
data RelevTy = RelevTy_None {}
             | RelevTy_Err {str_RelevTy_Err :: !(String)}
             | RelevTy_Ana {eval_RelevTy_Ana :: !(AnaEval)}
             | RelevTy_Fun {quant_RelevTy_Fun :: !(RQuant),quants_RelevTy_Fun :: !(([UID])),quals_RelevTy_Fun :: !(RelevQualL),args_RelevTy_Fun :: !(RelevTyL),res_RelevTy_Fun :: !(RelevTy)}
             deriving ( Data,Eq,Ord,Show,Typeable)
-- RelevTyL ----------------------------------------------------
type RelevTyL = [RelevTy]
-- TyAGItf -----------------------------------------------------
data TyAGItf = TyAGItf_AGItf {relevTy_TyAGItf_AGItf :: !(RelevTy)}
             deriving ( Data,Eq,Ord,Show,Typeable)