uhc-light-1.1.9.4: src/UHC/Light/Compiler/Ty.hs
-- UUAGC 0.9.52.1 (build/103/lib-ehc/UHC/Light/Compiler/Ty.ag)
module UHC.Light.Compiler.Ty(TyAGItf (..), Ty (..), TyAnn (..), TyL, tyInt, tyChar
, tyLHdAndTl, tyProdArgs
, tyUnAnn
, tyCanonAnn
, TyVarId, mkTyVar, mkNewTyVar, mkNewUIDTyVarL, mkNewTyVarL, mkTyFreshProd, mkTyFreshProdFrom, tyEnsureNonAny
, TyVarIdL, TyVarIdS
, LookupTy
, TyVarWild (..), TyVarWildMp
, tvwmpNoQuantS
, mkTyQu, TyVarCateg (..)
, tyMbVar
, tyVar
, TyQu (..)
, tvCatIsPlain, tvCatIsFixed
, TvInfo (..)
, emptyTvInfo
, mkTvInfo, mkTvInfoTy
, TvCatMp, emptyTvCatMp
, tyQu_Forall, tyQu_Exists
, tyquIsExists, tyquIsForall
, tyquMetaLev
, tyquExists
, showTyQu
, tyAnnMono
, tyAnnDecomposeMk
, tyIsVar, tyIsCon
, tvIsPlain, tyIsVarPlain
, tyIsSimple
, tyMbCon, tyConNm
, Polarity
, polCovariant, polContravariant, polInvariant
, polIsCovariant, polIsContravariant, polIsInvariant
, polOpp
, FIMode (..)
, fimOpp
, fimSwapPol
, InstTo (..)
, instToSplitQu
, kiStar
, tyQu_KiForall, tyQu_KiExists
, tyAppFunArgsWithLkup
, TyKiKey (..)
, tyKiKeyMbName
, tyKiKeyIsName
, instToL1AssocL
, kiRow
, FldTyL
, tyRowUnAnn, tyRowExtsUnAnn
, tyMbConWithLkup
, tyAppFunMbConNm, tyAppFunConNm
, tyRowExtsWithLkup, tyRecExtrWithLkup, tyRecExtsWithLkup
, tyRowExtr, tyRecExtr, tyRecExts
, rowExtCmp
, tyRecOffset
, tyDataTyNm
, tyRecExts2
, tyRowOffsetOrder
, tyExtsOffset
, tyRecOffsetWithLkup
, Pred (..)
, Impls (..), ImplsVarId
, TyCtxt (..)
, tyEnsureNonAnyImpl
, LookupImpls
, tvCatIsMeta
, TvPurpose (..)
, tvpurposeIsTy
, mkTvInfoPlain
, PredScope (..), initPredScope
, pscpMbVar
, pscpEnter, pscpLeave
, pscpEnter', pscpLeave', pscpMk'
, pscpIsVisibleIn, pscpCommon
, pscpParents
, pscpCmp, pscpCmpByLen
, ImplsProveOcc (..), mkImplsProveOcc
, PredOcc (..), poId, mkPredOcc
, CHRPredOccCxt (..)
, CHRPredOcc' (..), CHRPredOcc, cpoScope, mkCHRPredOcc
, cpo2PredOcc
, mkTyMetaVar
, mkImplsTail, mkImplsVar, mkImplsNil
, mkTyImpls
, mkTyPr
, tyArrowArgResWithLkup
, tyArrowImplsResWithLkup, tyArrowImplsArgResWithLkup
, tyArrowImplsRes, tyArrowImplsArgRes
, tyQuant
, tyLImplsPreds
, tyPred, predNm, tyPredNm, tyPrArrowArgsRes
, tyPredMatchNmArgs, predMatchNmArgs
, tyPred2DataTy, pred2DataTy
, predTy
, predHasRuntimeEvidence
, implsPredsTailWithLkup, tyImplsWithLkup, implsPrIdLWithLkup
, tyImpls, implsPredsTail, implsPredsMbTail, implsIsTail, tyIsImplsTail, tyImplsPreds, implsPrIdPredL, implsPrIdL
, tyMb1ArrTailVar2VarWithLkup
, implsMbVar, implsTailVar
, implsIsEmpty
, tyIsPredicated, tyIsPredicatedWithLkup
, Label (..), LabelAGItf (..)
, LabelVarId
, LabelOffset (..)
, tyIsEmptyRow
, tyRowIsCanonOrdered
, labelMbVar
, tyLamArgsRes
, tyIsLam
, mkTyLam
, tyString
, tyAppFunArgsMk
, tyLamEtaRed
, tyDecomposeMk
, tyRecMap
, PredSeq (..)
, predSeqToList, predLFlatten
, mkPolNegate, mkPolVar
, tyAllConS
, tyInteger
, tyMbRecExts
, mkPredOccRng
, mkCHRPredOccRng
, tyIsA) where
import UHC.Util.Utils
import UHC.Light.Compiler.Base.Common
import UHC.Light.Compiler.Base.TermLike
import UHC.Light.Compiler.Base.HsName.Builtin
import UHC.Light.Compiler.Opts.Base
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.List
import qualified UHC.Util.RLList.LexScope as LexScope
import UHC.Util.Pretty
import UHC.Util.Utils
import Control.Monad
import UHC.Util.Binary
import UHC.Util.Serialize
{-|
There are some conventions/restrictions on the structure of types that are not enforced
by the abstract syntax:
Encoding of prove-constraints:
concrete syntax:
{! impls !} -> ty
abstract syntax:
Ty_App (Ty_App (Ty_Con "->") (Ty_Impls impls)) ty
Encoding of assume-constraints:
concrete syntax:
(ty, {! pred1 !}, ..., {! predn !})
abstract syntax:
Ty_Ext (... (Ty_Ext ty (prod m+1) (Ty_Pred pred_1) ) ...) (prod m+n) (Ty_Pred pred_n)
In other words: the predicates are at the outset of a product, pred_n "more outermost"
than pred_{n-1}.
-}
{-|
The basic alternatives encode the following:
- Con: data type constructors, including tuple constructors
- App: application to 1 argument, for example 'a -> b' is encoded as (App (App -> a) b)
- Any: representing Bot/Top depending on context: (1) unknown expected type, (2) error type
- Var: type variables, including a category: plain tyvars, fixed tyvars (aka skolems)
-}
{-|
The module UHC.Light.Compiler.Ty
contains the Haskell interface to the internal representation of types
used by EHC. The AST is described in Ty/AbsSyn.
-}
type TyL = [Ty]
type TyVarId = VarId
type TyVarIdL = [TyVarId]
type TyVarIdS = VarIdS
type FldTyL = AssocL (Maybe HsName) Ty
type ImplsVarId = VarId
type LabelVarId = VarId
type LookupTy = TyVarId -> Maybe Ty
type LookupImpls = ImplsVarId -> Maybe Impls
-- | tyvars may act as wildcard, that is, they act as placeholders inside partial type signatures, providing
-- some structure. Such wildcards come in flavors:
data TyVarWild
= TyVarWild_NoQuantTyExpr_YesQuantLetBinding -- quantify: not in TyExpr, yes in let binding
| TyVarWild_NoQuantTyExpr_NoQuantLetBinding -- quantify: not in TyExpr, not in let binding (enforce monomorphism)
deriving Eq
type TyVarWildMp = Map.Map TyVarId TyVarWild
tvwmpNoQuantS :: TyVarWildMp -> UIDS
tvwmpNoQuantS = Map.keysSet . Map.filter (== TyVarWild_NoQuantTyExpr_NoQuantLetBinding)
tvCatIsPlain :: TyVarCateg -> Bool
tvCatIsPlain TyVarCateg_Plain = True
tvCatIsPlain _ = False
tvCatIsFixed :: TyVarCateg -> Bool
tvCatIsFixed TyVarCateg_Fixed = True
tvCatIsFixed _ = False
tvCatIsMeta :: TyVarCateg -> Bool
tvCatIsMeta TyVarCateg_Meta = True
tvCatIsMeta _ = False
data TvPurpose
= TvPurpose_Ty TyVarCateg -- stands for unknown type, the known humble type variable
| TvPurpose_Impls -- possibly empty sequence of implicit parameters
| TvPurpose_Scope -- predicate scope
| TvPurpose_Pred -- predicate
| TvPurpose_AssNm -- assumed name, in CHR
| TvPurpose_Label -- label, in CHR, for ext records
| TvPurpose_Offset -- offset, in CHR, for ext records
| TvPurpose_PredSeq -- experimental still
deriving (Eq,Ord)
instance Show TvPurpose where
show (TvPurpose_Ty TyVarCateg_Fixed) = "c"
show (TvPurpose_Ty TyVarCateg_Meta ) = "m"
show (TvPurpose_Ty _ ) = "v"
show TvPurpose_Impls = "i"
show TvPurpose_Scope = "s"
show TvPurpose_Pred = "p"
show TvPurpose_AssNm = "a"
show TvPurpose_Label = "l"
show TvPurpose_Offset = "o"
show TvPurpose_PredSeq = "s"
tvpurposeIsTy (TvPurpose_Ty _) = True
tvpurposeIsTy _ = False
data TvInfo
= TvInfo
{ tvinfoCateg :: !TyVarCateg
, tvinfoPurpose :: !TvPurpose
}
emptyTvInfo
= TvInfo TyVarCateg_Plain
(TvPurpose_Ty TyVarCateg_Plain)
mkTvInfo = TvInfo
mkTvInfoTy :: TyVarCateg -> TvInfo
mkTvInfoTy c = mkTvInfo c (TvPurpose_Ty c)
instance Show TvInfo where
show i | pur == TvPurpose_Ty TyVarCateg_Fixed && cat == TyVarCateg_Fixed = "c"
| otherwise = show pur
where cat = tvinfoCateg i
pur = tvinfoPurpose i
mkTvInfoPlain :: TvPurpose -> TvInfo
mkTvInfoPlain p = mkTvInfo TyVarCateg_Plain p
type TvCatMp = Map.Map TyVarId TvInfo
emptyTvCatMp = Map.empty
data LabelOffset
= LabelOffset_Off !Int
| LabelOffset_Var !UID
deriving
( Eq, Ord
, Typeable
)
instance Show LabelOffset where
show (LabelOffset_Off o) = show o
show (LabelOffset_Var v) = "off_" ++ show v
data PredScope
= PredScope_Lev !LexScope.LexScope
| PredScope_Var !TyVarId
deriving (Eq,Ord)
initPredScope :: PredScope
initPredScope = PredScope_Lev LexScope.empty
deriving instance Typeable PredScope
pscpMbVar :: PredScope -> Maybe TyVarId
pscpMbVar (PredScope_Var v) = Just v
pscpMbVar _ = Nothing
instance Show PredScope where
show (PredScope_Lev l) = show l
show (PredScope_Var v) = "[sc_" ++ show v ++ "]"
pscpEnter :: Int -> PredScope -> (Int,PredScope)
pscpEnter x (PredScope_Lev s) = (x+1,PredScope_Lev (x `LexScope.enter` s))
pscpLeave :: PredScope -> PredScope
pscpLeave (PredScope_Lev s) = PredScope_Lev $ fromJust $ LexScope.leave s
-- enter yes/no scope, give back the threaded counter to outside the new scope and inside
-- use in conjunction with pscpLeave'
pscpEnter' :: Bool -> Int -> (Int,Int)
pscpEnter' yesEnter x
= if yesEnter
then (fst $ pscpEnter x initPredScope,0)
else (x,x)
-- leave scope, on previous entering yes/no scope, give back the threaded counter to outside the new scope and inside
-- use in conjunction with pscpEnter'
pscpLeave' :: Bool -> Int -> Int -> Int
pscpLeave' yesEnter newScopeCounter innerScopeCounter
= if yesEnter
then newScopeCounter
else innerScopeCounter
-- make scope, depending on yes/no entering
-- use in conjunction with pscpEnter'
pscpMk' :: Bool -> Int -> PredScope -> PredScope
pscpMk' yesEnter x s
= if yesEnter
then snd $ pscpEnter x s
else s
pscpIsVisibleIn :: PredScope -> PredScope -> Bool
pscpIsVisibleIn (PredScope_Lev sOuter) (PredScope_Lev sInner) = sOuter `LexScope.isVisibleIn` sInner
pscpIsVisibleIn _ _ = False
pscpCommon :: PredScope -> PredScope -> Maybe PredScope
pscpCommon (PredScope_Lev s1) (PredScope_Lev s2) = Just $ PredScope_Lev $ LexScope.common s1 s2
pscpCommon _ _ = Nothing
pscpParents :: PredScope -> [PredScope]
pscpParents (PredScope_Lev s) = map PredScope_Lev $ LexScope.parents s
pscpParents _ = []
pscpCmp :: PredScope -> PredScope -> Maybe Ordering
pscpCmp (PredScope_Lev s) (PredScope_Lev t) = Just $ s `compare` t
pscpCmp _ _ = Nothing
pscpCmpByLen :: PredScope -> PredScope -> Ordering
pscpCmpByLen (PredScope_Lev s) (PredScope_Lev t) = s `LexScope.compareByLength` t
data ImplsProveOcc
= ImplsProveOcc
{ ipoId :: !UID
, ipoScope :: !PredScope
}
deriving (Eq,Show,Ord)
mkImplsProveOcc :: UID -> PredScope -> ImplsProveOcc
mkImplsProveOcc = ImplsProveOcc
deriving instance Typeable ImplsProveOcc
data PredOcc
= PredOcc
{ poPr :: !Pred
, poPoi :: !PredOccId
, poScope :: !PredScope
, poRange :: !Range
}
deriving (Show,Eq,Ord)
poId :: PredOcc -> UID
poId = poiId . poPoi
mkPredOcc :: Pred -> PredOccId -> PredScope -> PredOcc
mkPredOcc p i sc = rngLift emptyRange mkPredOccRng p i sc
mkPredOccRng :: Range -> Pred -> PredOccId -> PredScope -> PredOcc
mkPredOccRng r p i sc = PredOcc p i sc r
data CHRPredOccCxt
= CHRPredOccCxt_Scope1
{ cpocxScope :: !PredScope -- default, only allowed value for occurring preds
-- -- others for solving and CHR's only
}
deriving (Show,Eq,Ord,Generic)
deriving instance Typeable CHRPredOccCxt
data CHRPredOcc' p
= CHRPredOcc
{ cpoPr :: !p
-- , cpoScope :: !PredScope
, cpoCxt :: !CHRPredOccCxt
, cpoRange :: !Range
}
deriving (Show,Eq,Ord,Generic)
type CHRPredOcc = CHRPredOcc' Pred
mkCHRPredOcc :: Pred -> PredScope -> CHRPredOcc
mkCHRPredOcc p sc = mkCHRPredOccRng emptyRange p sc
cpoScope :: CHRPredOcc -> PredScope
cpoScope = cpocxScope . cpoCxt
cpo2PredOcc :: PredOccId -> CHRPredOcc -> PredOcc
cpo2PredOcc i o
= mkPredOccRng
(cpoRange o)
(cpoPr o)
i
(cpoScope o)
-- #if __GLASGOW_HASKELL__ >= 708
deriving instance Typeable CHRPredOcc'
-- #else
-- deriving instance Typeable1 CHRPredOcc'
-- #endif
mkCHRPredOccRng :: Range -> Pred -> PredScope -> CHRPredOcc
mkCHRPredOccRng r p sc = CHRPredOcc p (CHRPredOccCxt_Scope1 sc) r
tyQu_Forall = TyQu_Forall metaLevVal
tyQu_Exists = TyQu_Exists metaLevVal
tyQu_KiForall = TyQu_Forall metaLevTy
tyQu_KiExists = TyQu_Exists metaLevTy
tyquIsExists, tyquIsForall :: TyQu -> Bool
tyquIsForall (TyQu_Forall _) = True
tyquIsForall _ = False
tyquIsExists (TyQu_Exists _) = True
tyquIsExists _ = False
tyquMetaLev (TyQu_Forall l) = l
tyquMetaLev (TyQu_Exists l) = l
tyquMetaLev (TyQu_Plain l) = l
tyquExists, tyquForall :: TyQu -> TyQu
tyquForall (TyQu_Exists l) = TyQu_Forall l
tyquForall q = q
tyquExists (TyQu_Forall l) = TyQu_Exists l
tyquExists q = q
showTyQu (TyQu_Forall 0) = "forall"
showTyQu (TyQu_Forall 1) = "forall" ++ [charKindStar]
showTyQu (TyQu_Forall l) = "forall" ++ [charKindStar] ++ show l
showTyQu (TyQu_Exists 0) = "exists"
showTyQu (TyQu_Exists 1) = "exists" ++ [charKindStar]
showTyQu (TyQu_Exists l) = "exists" ++ [charKindStar] ++ show l
showTyQu (TyQu_Plain 0) = ""
showTyQu (TyQu_Plain 1) = [charKindStar]
showTyQu (TyQu_Plain l) = [charKindStar] ++ show l
tyIsA :: Ty -> String
tyIsA (Ty_Con a ) = "CON"
tyIsA (Ty_App a b ) = "APP"
tyIsA (Ty_Ann a b ) = "ANN"
tyIsA (Ty_Var a b ) = "VAR"
tyIsA (Ty_Any ) = "ANY"
tyIsA (Ty_TBind a b c d) = "QUANT"
tyIsA (Ty_Ext a b c ) = "EXT"
tyIsA (Ty_Pred a ) = "PRED"
tyIsA (Ty_Lam a b ) = "LAM"
tyIsA (Ty_Impls a ) = "IMPLS"
-- | Remove TyAnn's
tyUnAnn :: Ty -> Ty
tyUnAnn = fst . appUnAnn
{-# INLINE tyUnAnn #-}
tyRowUnAnn :: AssocL HsName Ty -> AssocL HsName Ty
tyRowUnAnn = assocLMapElt tyUnAnn
tyRowExtsUnAnn :: (Ty,AssocL HsName Ty) -> (Ty,AssocL HsName Ty)
tyRowExtsUnAnn (x,y) = (tyUnAnn x,tyRowUnAnn y)
-- | Canonicalize TyAnn's
tyCanonAnn :: Ty -> Ty
tyCanonAnn t
= c [] t
where c seen t@(Ty_Ann a ta) | a `elem` seen = c seen ta
| otherwise = Ty_Ann a $ c (a:seen) ta
c _ t = t
-- | Add TyAnn
tyAnn :: TyAnn -> Ty -> Ty
tyAnn a t@(Ty_Ann a' _) | a == a' = t
tyAnn a t = Ty_Ann a t
-- | Add TyAnn_Mono
tyAnnMono :: Ty -> Ty
tyAnnMono = tyAnn TyAnn_Mono
-- | Decompose type for annotation into unannotated type + reconstruction
tyAnnDecomposeMk :: Ty -> (Ty, [TyAnn], Ty -> Ty)
tyAnnDecomposeMk t
= case t of
Ty_Ann a t' -> (ta,as,\ta' -> tyAnn a $ mk ta')
where (ta,as,mk) = tyAnnDecomposeMk t'
_ -> (t ,[],id)
tyIsVar :: Ty -> Bool
tyIsVar = isJust . tyMbVar
tyIsCon :: Ty -> Bool
tyIsCon = isJust . tyMbCon
tyIsQu :: Ty -> Bool
tyIsQu = isJust . tyMbQu
tyIsVarPlain :: Ty -> Bool
tyIsVarPlain = maybe False (tvCatIsPlain . snd) . tyMbVar'
tvIsPlain :: TvCatMp -> TyVarId -> Bool
tvIsPlain m v = maybe False (tvCatIsPlain . tvinfoCateg) $ Map.lookup v m
tyIsEmptyRow :: Ty -> Bool
tyIsEmptyRow = maybe False (== hsnRowEmpty) . tyMbCon
tyIsSimple :: Ty -> Bool
tyIsSimple t = tyIsVar t || tyIsCon t
tyIsLam :: Ty -> Bool
tyIsLam ty
= not (null as)
where (as,_) = tyLamArgsRes ty
instance {-# OVERLAPPING #-} AppLike Ty Ty {- TyAnn () -} where
-- AppLike
app1App = Ty_App
appTop = id
appCon = Ty_Con . mkHNm
appPar = id
appRngVar _ = panic "Ty.appRngVar"
appProdApp tyL = recRec (zip positionalFldNames tyL)
-- appDflt = Ty_Any
appDbg s = Ty_Dbg $ "*ERR: " ++ s ++ " :*"
appMbCon (Ty_Con n) = Just n
appMbCon _ = Nothing
appMbApp1 (Ty_App f a) = Just (f,a)
appMbApp1 _ = Nothing
appMbAnn1 (Ty_Ann a t) = Just (t, Ty_Ann a)
appMbAnn1 _ = Nothing
appMbCanon1 t = do (is,r) <- tyMbArrowImplsResWithLkup (const Nothing) t
if not (null is) && all (maybe False implsIsEmpty . tyMbImpls) is then return (r, appArr is) else Nothing
appMbDbg (Ty_Dbg s) = Just s
appMbDbg _ = Nothing
appMbBind1 (Ty_TBind q v k t) = Just (t, Ty_TBind q v k)
appMbBind1 _ = Nothing
instance BndLike Ty TyVarId {- TyAnn () -} where
-- BndLike
bndBndIn n l x = Ty_TBind (TyQu_Plain (l-1)) n x
instance {-# OVERLAPPING #-} RecLike Ty Ty {- TyAnn () -} where
-- RecLike
recRow r = foldl (\t (n,e) -> Ty_Ext t n e) r
recMbRecRow = tyMbRecRowWithLkup (const Nothing)
recUnRowExts = tyRowExtsWithLkup (const Nothing)
mkTyVar :: TyVarId -> Ty
mkTyVar tv = Ty_Var tv TyVarCateg_Plain
mkTyMetaVar :: TyVarId -> Ty
mkTyMetaVar tv = Ty_Var tv TyVarCateg_Meta
mkNewTyVar :: UID -> Ty
mkNewTyVar u = let (_,v) = mkNewUID u in mkTyVar v
mkNewUIDTyVarL :: Int -> UID -> ([UID],TyL)
mkNewUIDTyVarL sz u = let vs = mkNewUIDL sz u in (vs,map mkTyVar vs)
mkNewTyVarL :: Int -> UID -> TyL
mkNewTyVarL sz u = snd (mkNewUIDTyVarL sz u)
tyEnsureNonAny :: UID -> Ty -> Ty
tyEnsureNonAny u t = if t /= Ty_Any then t else mkNewTyVar u
tyEnsureNonAnyImpl :: UID -> Ty -> Ty
tyEnsureNonAnyImpl u t
= if t /= Ty_Any then t
else let [i,r] = mkNewUIDL 2 u
in [mkImplsVar i] `appArr` mkTyVar r
mkTyQu :: TyQu -> [(TyVarId,Ty)] -> Ty -> Ty
mkTyQu q tvL t = foldr (\(tv,k) t -> Ty_TBind q tv k t) t tvL
mkTyFreshProdFrom :: UID -> Int -> Ty
mkTyFreshProdFrom uid arity = appProdApp . map mkTyVar . mkNewUIDL arity $ uid
mkTyFreshProd :: Int -> Ty
mkTyFreshProd = mkTyFreshProdFrom uidStart
mkTyLam :: [TyVarId] -> Ty -> Ty
mkTyLam args body = foldr Ty_Lam body args
mkImplsTail :: ImplsVarId -> Impls
mkImplsTail v = Impls_Tail v []
mkImplsVar :: ImplsVarId -> Ty
mkImplsVar v = Ty_Impls (mkImplsTail v)
mkImplsNil :: Ty
mkImplsNil = Ty_Impls Impls_Nil
mkTyImpls :: [Pred] -> Ty -> Ty
mkTyImpls prL t = map mkTyPr prL `appArr` t
mkTyPr :: Pred -> Ty
mkTyPr p
= case p of
Pred_Pred t -> t
_ -> Ty_Pred p
tyInt :: Ty
tyInt = appCon hsnInt
tyChar :: Ty
tyChar = appCon hsnChar
kiStar :: Ty
kiStar = appCon hsnKindStar
kiRow :: Ty
kiRow = appCon hsnKindRow
-- tyRowEmpty = appCon hsnRowEmpty
tyInteger :: Ty
tyInteger = appCon hsnInteger
tyString :: EHCOpts -> Ty
tyString o = appCon (ehcOptBuiltin o ehbnPrelString)
-- tyArrowArgsRes :: Ty -> (TyL,Ty)
-- tyAppFunArgs :: Ty -> (Ty,TyL)
-- tyAppArgs :: Ty -> TyL
-- tyArrowArgs :: Ty -> TyL
-- tyArrowRes :: Ty -> Ty
-- tyArrowArg :: Ty -> Ty
tyArrowArgResWithLkup :: LookupTy -> Ty -> (Ty,Ty)
tyArrowArgResWithLkup lookup = tyVarChkVisitLift lookup appUn1Arr appUn1Arr
tyArrowImplsArgResWithLkup :: LookupTy -> Ty -> (TyL,Ty,Ty)
tyArrowImplsArgResWithLkup lookup t
= (i,a,r)
where (i,t') = tyArrowImplsResWithLkup lookup t
(a,r) = tyArrowArgResWithLkup lookup t'
tyMbArrowImplsResWithLkup :: LookupTy -> Ty -> Maybe (TyL,Ty)
tyMbArrowImplsResWithLkup lookup t
= extr t
where extr t = case appMb1Arr t of
Just (a,r)
| isImpls a'
-- -> let (as,r') = extr r in (a':as,r')
-> case extr r of
Just (as,r') -> Just (a':as,r')
_ -> Just ([a'],r)
where a' = tyUnAnn a
isImpls (Ty_Pred _) = True
isImpls (Ty_Impls _) = True
isImpls _ = False
_ -> tyVarLift lookup extr (const Nothing) t
tyArrowImplsResWithLkup :: LookupTy -> Ty -> (TyL,Ty)
tyArrowImplsResWithLkup lookup t = maybe ([],t) id $ tyMbArrowImplsResWithLkup lookup t
tyArrowImplsRes :: Ty -> (TyL,Ty)
tyArrowImplsRes = tyArrowImplsResWithLkup (const Nothing)
tyArrowImplsArgRes :: Ty -> (TyL,Ty,Ty)
tyArrowImplsArgRes = tyArrowImplsArgResWithLkup (const Nothing)
tyProdArgs :: Ty -> TyL
tyLHdAndTl :: [Ty] -> (Ty,TyL)
-- Substitution aware
tyAppFunArgsWithLkup :: LookupTy -> Ty -> (Ty,TyL)
tyAppFunArgsWithLkup lookup = tyVarChkVisitLift lookup appUnApp appUnApp
{-# INLINE tyAppFunArgsWithLkup #-}
tyAppFunArgsMk :: Ty -> (Ty, TyL, Ty -> TyL -> Ty)
tyAppFunArgsMk
= extr []
where extr as t
= case tyUnAnn t of
Ty_TBind q v k t -> (f,as,\f as -> Ty_TBind q v k $ mk f as)
where (f,as,mk) = tyAppFunArgsMk t
Ty_App f a -> extr (a:as) f
_ -> (t,as,\f as -> appTopApp (f:as))
tyLHdAndTl = hdAndTl' Ty_Any
{-# INLINE tyLHdAndTl #-}
tyMbCon :: Ty -> Maybe HsName
-- tyMbCon t = case tyUnAnn t of {Ty_Con nm -> Just nm ; _ -> Nothing}
tyMbCon = appMbCon -- . fst . appUnAnn
{-# INLINE tyMbCon #-}
tyConNm :: Ty -> HsName
tyConNm = maybe hsnUnknown id . tyMbCon
{-# INLINE tyConNm #-}
tyMbConWithLkup :: LookupTy -> Ty -> Maybe HsName
tyMbConWithLkup lookup = tyVarChkVisitLift lookup tyMbCon tyMbCon
{-# INLINE tyMbConWithLkup #-}
tyMbVar' :: Ty -> Maybe (TyVarId,TyVarCateg)
tyMbVar' t = case tyUnAnn t of {Ty_Var v c -> Just (v,c) ; _ -> Nothing}
tyMbVar :: Ty -> Maybe TyVarId
tyMbVar = fmap fst . tyMbVar'
{-# INLINE tyMbVar #-}
tyMbQu :: Ty -> Maybe TyQu
tyMbQu t
= case tyUnAnn t of
Ty_TBind q _ _ _
-> Just q
_ -> Nothing
tyVar :: Ty -> TyVarId
tyVar = maybe uidStart id . tyMbVar
{-# INLINE tyVar #-}
tyProdArgs ty = let (t,al) = tyRecExts ty in map snd al
tyAppFunMbConNm :: Ty -> Maybe HsName
tyAppFunMbConNm = tyMbCon . fst . appUnApp
{-# INLINE tyAppFunMbConNm #-}
tyAppFunConNm :: Ty -> HsName
tyAppFunConNm = tyConNm . fst . appUnApp
{-# INLINE tyAppFunConNm #-}
-- | The name of a data type extracted from a Ty
tyDataTyNm :: Ty -> HsName
tyDataTyNm = tyAppFunConNm . appUnArrRes
-- | All constructors occurring in a type
tyAllConS :: Ty -> Set.Set HsName
tyAllConS t
= Set.unions $ (maybe Set.empty Set.singleton $ tyMbCon f) : map tyAllConS a
where (f,a,_) = tyDecomposeMk t
tyQuant :: Ty -> Ty
tyQuant t
= case tyUnAnn t of
Ty_TBind _ _ _ t' -> tyQuant t'
_ -> t
tyLImplsPreds :: TyL -> ([Pred],Impls)
tyLImplsPreds = foldr (\t (ps,i) -> case tyUnAnn t of {Ty_Pred p -> (p:ps,i); Ty_Impls i -> (ps,i)}) ([],Impls_Nil)
tyLamArgsRes :: Ty -> ([TyVarId],Ty)
tyLamArgsRes
= extr
where extr t
= case tyUnAnn t of
Ty_Lam a r -> (a:as',r')
where (as',r') = extr r
_ -> ([],t)
-- Eta reduce when the full list of args can be eliminated thus, i.e. it matches with the tail of the args applied in the app (if any) of the body
tyLamEtaRed :: Ty -> Maybe Ty
tyLamEtaRed t
| llas > 0 && rlDiff >= 0 && map mkTyVar las == rTl = Just (appTopApp (f:rHd))
| otherwise = Nothing
where (las,r ) = tyLamArgsRes t
(f ,ras) = appUnApp r
llas = length las
rlas = length ras
rlDiff = rlas - llas
(rHd,rTl) = splitAt rlDiff ras
-- mkTyRow :: Ty -> AssocL HsName Ty -> Ty
-- mkTyRow r = foldl (\t (n,e) -> Ty_Ext t n e) r
{-
mkTyRec :: AssocL HsName Ty -> Ty
mkTyRec al = hsnRec `appConApp` [recRowEmp `recRow` al]
mkTyRecExt :: Ty -> AssocL HsName Ty -> Ty
mkTyRecExt recd al
= let (row,exts) = recUnRowExts (recUnRecRow recd)
in hsnRec `appConApp` [row `recRow` (exts ++ al)]
-}
-- mkTySum :: AssocL HsName Ty -> Ty
-- mkTySum al = hsnSum `appConApp` [recRowEmp `recRow` al]
tyVarChkVisitLift :: LookupTy -> (Ty -> x) -> (Ty -> x) -> Ty -> x
tyVarChkVisitLift
= withLkupChkVisitLift tyMbVar (noVisit . tyUnAnn)
where noVisit (Ty_TBind _ qv _ _) = Set.singleton qv
noVisit _ = Set.empty
tyVarLift :: LookupTy -> (Ty -> x) -> (Ty -> x) -> Ty -> x
tyVarLift = withLkupLift tyMbVar
{-# INLINE tyVarLift #-}
implsTailVarLiftCyc :: (TyVarId -> Maybe Impls) -> (TyVarIdS -> Impls -> x) -> (Impls -> x) -> TyVarIdS -> Impls -> x
implsTailVarLiftCyc = withLkupLiftCyc1 implsMbVar (const Set.empty)
{-# INLINE implsTailVarLiftCyc #-}
tyRowExtsWithLkup :: LookupTy -> Ty -> (Ty,AssocL HsName Ty)
tyRowExtsWithLkup lookup
= extr []
where extr as t
= case tyUnAnn t of
(Ty_Ext r l e) -> extr ((l,e):as) r
t' -> tyVarLift lookup (extr as) (flip (,) as) t'
tyRecExtsWithLkup :: LookupTy -> Ty -> (Ty,AssocL HsName Ty)
tyRecExtsWithLkup lookup t
= case tyRecRowWithLkup lookup t of
Ty_Any -> (Ty_Any,[])
row -> tyRowExtsWithLkup lookup row
tyRecRowWithLkup :: LookupTy -> Ty -> Ty
tyRecRowWithLkup lookup = maybe Ty_Any id . tyMbRecRowWithLkup lookup
tyRowExtrWithLkup :: LookupTy -> HsName -> Ty -> Maybe (Ty,Ty)
tyRowExtrWithLkup lookup lbl t
= extr t
where extr t
= case tyUnAnn t of
(Ty_Ext r l e) | lbl == l -> Just (r,e)
| otherwise -> maybe Nothing (\(r',e') -> Just (Ty_Ext r' l e,e')) (extr r)
t' -> tyVarLift lookup extr (const Nothing) t'
tyRecExtrWithLkup :: LookupTy -> HsName -> Ty -> Maybe (Ty,Ty)
tyRecExtrWithLkup lookup lbl t
= case tyRowExtrWithLkup lookup lbl (tyRecRowWithLkup lookup t) of
Nothing -> Nothing
Just (r,e) -> Just (hsnRec `appConApp` [r],e)
tyMbRecRowWithLkup :: LookupTy -> Ty -> Maybe Ty
tyMbRecRowWithLkup lookup t
= case tyAppFunArgsWithLkup lookup t of
(f,[row])
-> case tyMbConWithLkup lookup f of
Just n | hsnIsRec n || hsnIsSum n -> Just row
_ -> Nothing
_ -> Nothing
-- tyMbRecRow :: Ty -> Maybe Ty
-- tyMbRecRow = tyMbRecRowWithLkup (const Nothing)
-- {-# INLINE tyMbRecRow #-}
{-
= case tyAppFunArgs t of
(Ty_Con n,[row]) | hsnIsRec n || hsnIsSum n -> Just row
_ -> Nothing
-}
-- tyRecRow :: Ty -> Ty
-- tyRecRow = maybe Ty_Any id . recMbRecRow
-- {-# INLINE tyRecRow #-}
-- tyRowExts :: Ty -> (Ty,AssocL HsName Ty)
-- tyRowExts = tyRowExtsWithLkup (const Nothing)
-- {-# INLINE tyRowExts #-}
tyRecExts :: Ty -> (Ty,AssocL HsName Ty)
tyRecExts = tyRecExtsWithLkup (const Nothing)
{-# INLINE tyRecExts #-}
tyRowExtr :: HsName -> Ty -> Maybe (Ty,Ty)
tyRowExtr = tyRowExtrWithLkup (const Nothing)
{-# INLINE tyRowExtr #-}
tyRecExtr :: HsName -> Ty -> Maybe (Ty,Ty)
tyRecExtr = tyRecExtrWithLkup (const Nothing)
{-# INLINE tyRecExtr #-}
tyMbRecExts :: Ty -> Maybe (Ty,AssocL HsName Ty)
tyMbRecExts = fmap recUnRowExts . recMbRecRow
tyRecExts2 :: Ty -> AssocL HsName (AssocL HsName Ty)
tyRecExts2
= assocLMapElt (snd . tyRecExts) . snd . tyRecExts
tyDecomposeMk :: Ty -> (Ty, TyL, Ty -> TyL -> Ty)
tyDecomposeMk t
= case t of
Ty_TBind q v k t' -> (f,as,\f' as' -> Ty_TBind q v k $ mk f' as')
where (f,as,mk) = tyDecomposeMk t'
Ty_App _ _ -> (f,as,\f' as' -> appTopApp (f':as'))
where (f,as) = appUnApp t
Ty_Ext _ _ _ -> (r,assocLElts e,\r' e' -> recRow r' $ zip (assocLKeys e) e')
where (r,e) = recUnRowExts t
_ | not (null an) -> (t2,as,\f' as' -> mk1 $ mk2 f' as')
| otherwise -> (t,[],const)
where (t1,an,mk1) = tyAnnDecomposeMk t
(t2,as,mk2) = tyDecomposeMk t1
-- | Map 'f' over fields of record
tyRecMap :: (Ty -> Ty) -> Ty -> Ty
tyRecMap f r
= mk rem (map f fs)
where (rem,fs,mk) = tyDecomposeMk r
tyRowIsCanonOrdered :: AssocL HsName a -> Bool
tyRowIsCanonOrdered = isSortedByOn rowLabCmp fst
{-# INLINE tyRowIsCanonOrdered #-}
rowExtCmp :: (HsName,a) -> (HsName,a) -> Ordering
rowExtCmp (n1,_) (n2,_) = n1 `rowLabCmp` n2
{-# INLINE rowExtCmp #-}
-- tyRowCanonOrderBy :: (o -> o -> Ordering) -> AssocL o a -> AssocL o a
-- tyRowCanonOrderBy = rowCanonOrderBy
-- {-# INLINE tyRowCanonOrderBy #-}
-- tyRowCanonOrder :: AssocL HsName a -> AssocL HsName a
-- tyRowCanonOrder = tyRowCanonOrderBy rowLabCmp
-- {-# INLINE tyRowCanonOrder #-}
tyRowOffsetOrder :: (a -> Int) -> AssocL HsName a -> AssocL HsName a
tyRowOffsetOrder off = sortOnLazy (off . snd)
{-# INLINE tyRowOffsetOrder #-}
tyExtsOffset :: HsName -> AssocL HsName a -> ((Int,Presence),Maybe a)
tyExtsOffset lbl exts
= find 0 lbl exts
where find o l (e@(_,a):es) = case (l,panic "Ty.tyExtsOffset") `rowExtCmp` e of
GT -> find (o+1) l es
EQ -> ((o,Present),Just a)
LT -> ((o,Absent),Nothing)
find o _ [] = ((o,Absent),Nothing)
tyRecOffset :: HsName -> Ty -> Int
tyRecOffset lbl t
= fst $ fst $ tyExtsOffset lbl $ rowCanonOrder exts
where (_,exts) = tyRecExts t
tyRecOffsetWithLkup :: LookupTy -> HsName -> Ty -> Int
tyRecOffsetWithLkup lookup nm
= tyVarLift lookup o o
where o = tyRecOffset nm
tyPred :: Ty -> Pred
tyPred t
= case tyUnAnn t of
Ty_Pred pt -> pt
_ -> Pred_Pred t
predNm :: Pred -> HsName
predNm = tyAppFunConNm . predTy
{-# INLINE predNm #-}
tyPredNm :: Ty -> HsName
tyPredNm = predNm . tyPred
{-# INLINE tyPredNm #-}
tyPrArrowArgsRes :: Ty -> ([Pred],Pred)
tyPrArrowArgsRes tp = let (tl,t) = appUnArr tp in (map tyPred tl, tyPred t)
-- | extract class name and class args of predicate packages as Ty
tyPredMatchNmArgs :: Ty -> (HsName,[Ty])
tyPredMatchNmArgs = predMatchNmArgs . tyPred
{-# INLINE tyPredMatchNmArgs #-}
-- | extract class name and class args of predicate
predMatchNmArgs :: Pred -> (HsName,[Ty])
predMatchNmArgs p
= case p of
Pred_Class t -> (tyAppFunConNm t, appUnAppArgs t)
Pred_Pred t -> predMatchNmArgs $ snd $ tyPrArrowArgsRes t
Pred_Lacks _ (Label_Lab l) -> (hsnUniqify HsNameUniqifier_LacksLabel l, [])
Pred_Lacks _ _ -> (mkHNm "_LabVar_", []) -- necessary? only used by CHR's
Pred_Eq t1 t2 -> (hsnEqTilde,[t1,t2])
-- | construct for a predicate its corresponding data type
pred2DataTy :: Pred -> Ty
pred2DataTy p
= appConApp (hsnClass2Dict n) as
where (n,as) = predMatchNmArgs p
-- | construct for a predicate packaged as a Ty its corresponding data type
tyPred2DataTy :: Ty -> Ty
tyPred2DataTy = pred2DataTy . tyPred
{-# INLINE tyPred2DataTy #-}
predTy :: Pred -> Ty
predTy p
= case p of
Pred_Class t -> t
Pred_Pred t -> t
Pred_Lacks t _ -> t
Pred_Eq t _ -> t -- does it matter if we return the left or the right type?
predSeqToList :: PredSeq -> [Pred]
predSeqToList (PredSeq_Cons h t) = h : predSeqToList t
predSeqToList _ = []
predLFlatten :: [Pred] -> [Pred]
predLFlatten
= concatMap fl
where fl (Pred_Preds s) = predSeqToList s
fl p = [p]
-- | Is runtime evidence required for the predicate?
predHasRuntimeEvidence :: Pred -> Bool
predHasRuntimeEvidence p
= case p of
Pred_Eq _ _ -> False
_ -> True
implsPredsTailWithLkup' :: (TyVarId -> Maybe Impls) -> PredScope -> Impls -> ([(PredOcc,[ImplsProveOcc])],Impls)
implsPredsTailWithLkup' lookup sc i
= extr Set.empty i
where extr vsVisited i
= case i of
Impls_Cons _ p pv prange ipos t
-> ((mkPredOccRng prange p pv sc,ipos) : p',mi)
where (p',mi) = extr vsVisited t
_ -> implsTailVarLiftCyc lookup extr ((,) []) vsVisited i
implsPredsTailWithLkup :: (TyVarId -> Maybe Impls) -> PredScope -> Impls -> ([PredOcc],Impls)
implsPredsTailWithLkup lookup sc i
= (map fst is,t)
where (is,t) = implsPredsTailWithLkup' lookup sc i
tyImplsWithLkup :: LookupTy -> Ty -> Impls
tyImplsWithLkup lookup = tyVarLift lookup tyImpls tyImpls
{-# INLINE tyImplsWithLkup #-}
implsPrIdLWithLkup :: (TyVarId -> Maybe Impls) -> Impls -> [PredOccId]
implsPrIdLWithLkup lookup = map poPoi . fst . implsPredsTailWithLkup lookup initPredScope
{-# INLINE implsPrIdLWithLkup #-}
tyMbVarWithLkup :: LookupTy -> Ty -> Maybe TyVarId
tyMbVarWithLkup lookup = tyVarLift lookup tyMbVar tyMbVar
tyMbImpls :: Ty -> Maybe Impls
tyMbImpls
= extr . tyUnAnn
where extr (Ty_Impls i) = Just i
extr _ = Nothing
tyImpls :: Ty -> Impls
tyImpls = panicJust "tyImpls" . tyMbImpls
{-# INLINE tyImpls #-}
implsPredsTail' :: PredScope -> Impls -> ([(PredOcc,[ImplsProveOcc])],Impls)
implsPredsTail' = implsPredsTailWithLkup' (const Nothing)
{-# INLINE implsPredsTail' #-}
implsPredsTail :: PredScope -> Impls -> ([PredOcc],Impls)
implsPredsTail = implsPredsTailWithLkup (const Nothing)
{-# INLINE implsPredsTail #-}
implsPredsMbTail :: Impls -> ([(PredOcc,[ImplsProveOcc])],Maybe Impls)
implsPredsMbTail i = case implsPredsTail' initPredScope i of
(i',t@(Impls_Tail _ _)) -> (i',Just t)
(i', Impls_Nil ) -> (i',Nothing)
tyImplsPreds :: PredScope -> Ty -> [PredOcc]
tyImplsPreds sc = fst . implsPredsTail sc . tyImpls
{-# INLINE tyImplsPreds #-}
implsIsTail :: Impls -> Bool
implsIsTail = isJust . implsMbVar
{-# INLINE implsIsTail #-}
tyIsImplsTail :: Ty -> Bool
tyIsImplsTail = implsIsTail . tyImpls
{-# INLINE tyIsImplsTail #-}
implsPrIdPredL :: Impls -> [(PredOccId,Pred)]
implsPrIdPredL i = [ (poPoi po, poPr po) | po <- fst $ implsPredsTail initPredScope i ]
implsPrIdL :: Impls -> [PredOccId]
implsPrIdL = map fst . implsPrIdPredL
{-# INLINE implsPrIdL #-}
-- | Is an 'Impls' the tail (last empty element) of a sequence?
implsMbTailVarWithLkup :: LookupImpls -> Impls -> Maybe ImplsVarId
implsMbTailVarWithLkup lkup (Impls_Tail iv _) = maybe (Just iv) (const Nothing) (lkup iv)
implsMbTailVarWithLkup _ _ = Nothing
{-# INLINE implsMbTailVarWithLkup #-}
-- | Is a 'Ty' the tail of an Impls?
tyMbTailVarWithLkup :: LookupImpls -> Ty -> Maybe ImplsVarId
tyMbTailVarWithLkup lkup t = do { i <- tyMbImpls t ; implsMbTailVarWithLkup lkup i }
{-# INLINE tyMbTailVarWithLkup #-}
-- | Is 'Ty' a function type from an Impls tail to ...
tyMb1ArrTailVarWithLkup :: LookupImpls -> Ty -> Maybe (ImplsVarId,Ty)
tyMb1ArrTailVarWithLkup lkup t = do { (a,r) <- appMb1Arr t; i <- tyMbTailVarWithLkup lkup a; return (i,r) }
{-# INLINE tyMb1ArrTailVarWithLkup #-}
-- | Is 'Ty' a function type from an Impls tail to a ty var
tyMb1ArrTailVar2VarWithLkup :: LookupTy -> LookupImpls -> Ty -> Maybe (ImplsVarId,TyVarId)
tyMb1ArrTailVar2VarWithLkup lkupt lkupi t = do { (i,r) <- tyMb1ArrTailVarWithLkup lkupi t; v <- tyMbVarWithLkup lkupt r; return (i,v) }
implsMbVar :: Impls -> Maybe TyVarId
implsMbVar (Impls_Tail v _) = Just v
implsMbVar _ = Nothing
implsTailVar :: Impls -> ImplsVarId
implsTailVar = panicJust "implsTailVar" . implsMbVar
{-# INLINE implsTailVar #-}
implsIsEmpty :: Impls -> Bool
implsIsEmpty (Impls_Cons _ _ _ _ _ _) = False
implsIsEmpty _ = True
tyIsPredicated :: Ty -> Bool
tyIsPredicated (Ty_Impls i) = not $ implsIsEmpty i
tyIsPredicated t = isPr a
where a = map tyUnAnn $ appUnArrArgs t
isPr (Ty_Pred p:_) = True
isPr _ = False
tyIsPredicatedWithLkup :: LookupTy -> Ty -> Bool
tyIsPredicatedWithLkup lookup = tyVarLift lookup tyIsPredicated tyIsPredicated
{-# INLINE tyIsPredicatedWithLkup #-}
labelMbVar :: Label -> Maybe TyVarId
labelMbVar (Label_Var v) = Just v
labelMbVar _ = Nothing
data TyKiKey
= TyKiKey_Name !HsName
| TyKiKey_TyVar !TyVarId
deriving (Eq,Ord,Generic)
instance Show TyKiKey where
show (TyKiKey_Name n) = show n
show (TyKiKey_TyVar v) = show v
deriving instance Typeable TyKiKey
tyKiKeyMbName :: TyKiKey -> Maybe HsName
tyKiKeyMbName (TyKiKey_Name n) = Just n
tyKiKeyMbName _ = Nothing
tyKiKeyIsName :: TyKiKey -> Bool
tyKiKeyIsName = isJust . tyKiKeyMbName
{-# INLINE tyKiKeyIsName #-}
data TyCtxt = TyCtxt_Ty | TyCtxt_Pred | TyCtxt_Class deriving (Show,Eq)
type Polarity = Ty
polCovariant :: Polarity
polCovariant = appCon hsnCovariant
polContravariant :: Polarity
polContravariant = appCon hsnContravariant
polInvariant :: Polarity
polInvariant = appCon hsnInvariant
mkPolNegate :: Polarity -> Polarity
mkPolNegate = appCon1App hsnPolNegation
mkPolVar :: UID -> Polarity
mkPolVar = mkTyVar
polIs :: HsName -> Polarity -> Bool
polIs nm = maybe False (== nm) . tyMbCon
polIsCovariant, polIsContravariant, polIsInvariant :: Polarity -> Bool
polIsCovariant = polIs hsnCovariant
polIsContravariant = polIs hsnContravariant
polIsInvariant = polIs hsnInvariant
polOpp :: Polarity -> Polarity
polOpp pol | polIsCovariant pol = polContravariant
| polIsContravariant pol = polCovariant
| otherwise = polInvariant
data FIMode = FitSubLR
| FitSubRL
| FitUnify
deriving (Eq,Ord)
fimOpp :: FIMode -> FIMode
fimOpp m
= case m of
FitSubLR -> FitSubRL
FitSubRL -> FitSubLR
_ -> m
fimSwapPol :: Polarity -> FIMode -> FIMode
fimSwapPol pol m = if polIsContravariant pol then fimOpp m else m
instance Show FIMode where
show FitSubLR = "<="
show FitSubRL = ">="
show FitUnify = "=="
data InstTo
= InstTo_Plain -- a plain value
| InstTo_Qu -- the fresh type (tyvar) instantiated to
{ instoQu :: TyQu -- how tvar was quantified, also includes the meta level
, instoFrom :: TyVarId -- the tvar from which is instantiated
, instoTo :: TyVarId -- the new tvar to which is instantiated
, instoL1 :: Ty
}
{-
| InstTo_Lam -- a lambda
{ instoLam :: [InstTo]
}
-}
deriving Show
instToIsQu :: InstTo -> Bool
instToIsQu (InstTo_Qu _ _ _ _) = True
instToIsQu _ = False
-- split of initial quantifier instantiations, to be used for Sys F generation for type parameterization
instToSplitQu :: [InstTo] -> ([InstTo],[InstTo])
instToSplitQu = span instToIsQu
-- get tvar -> kind bindings of instantiation
instToL1AssocL :: [InstTo] -> AssocL TyVarId (MetaLev,Ty)
instToL1AssocL l = [ (v,(tyquMetaLev q,k)) | (InstTo_Qu q _ v k) <- l ]
instance Serialize TyKiKey
instance Binary ImplsProveOcc where
put (ImplsProveOcc a b) = put a >> put b
get = liftM2 ImplsProveOcc get get
instance Serialize ImplsProveOcc where
sput = sputPlain
sget = sgetPlain
instance Binary PredScope where
put (PredScope_Lev a ) = putWord8 0 >> put a
put (PredScope_Var a ) = putWord8 1 >> put a
get = do tag <- getWord8
case tag of
0 -> liftM PredScope_Lev get
1 -> liftM PredScope_Var get
instance Serialize PredScope where
sput = sputPlain
sget = sgetPlain
instance Binary CHRPredOccCxt where
put (CHRPredOccCxt_Scope1 a) = put a
get = liftM CHRPredOccCxt_Scope1 get
instance Serialize CHRPredOccCxt where
sput = sputPlain
sget = sgetPlain
instance Binary LabelOffset where
put (LabelOffset_Off a) = putWord8 0 >> put a
put (LabelOffset_Var a) = putWord8 1 >> put a
get = do t <- getWord8
case t of
0 -> liftM LabelOffset_Off get
1 -> liftM LabelOffset_Var get
instance Serialize LabelOffset where
sput = sputPlain
sget = sgetPlain
instance Binary TyQu where
put (TyQu_Forall a) = putWord8 0 >> put a
put (TyQu_Exists a) = putWord8 1 >> put a
put (TyQu_Plain a) = putWord8 1 >> put a
get = do tag <- getWord8
case tag of
0 -> liftM TyQu_Forall get
1 -> liftM TyQu_Exists get
2 -> liftM TyQu_Plain get
instance Serialize TyQu where
sput = sputPlain
sget = sgetPlain
instance Serialize Ty
instance Serialize TyAnn
instance Serialize Pred
instance Serialize Label
instance Serialize PredSeq
instance Serialize Impls
instance Serialize CHRPredOcc
instance Binary TyVarCateg where
put = putEnum8
get = getEnum8
instance Serialize TyVarCateg where
sput = sputPlain
sget = sgetPlain
-- Impls -------------------------------------------------------
data Impls = Impls_Tail {iv_Impls_Tail :: !(ImplsVarId),proveOccs_Impls_Tail :: !(([ImplsProveOcc]))}
| Impls_Cons {iv_Impls_Cons :: !(ImplsVarId),pr_Impls_Cons :: !(Pred),pv_Impls_Cons :: !(PredOccId),prange_Impls_Cons :: !(Range),proveOccs_Impls_Cons :: !(([ImplsProveOcc])),tl_Impls_Cons :: !(Impls)}
| Impls_Nil {}
deriving ( Eq,Generic,Ord,Show,Typeable)
-- Label -------------------------------------------------------
data Label = Label_Lab {nm_Label_Lab :: !(HsName)}
| Label_Var {lv_Label_Var :: !(LabelVarId)}
deriving ( Eq,Generic,Ord,Show,Typeable)
-- LabelAGItf --------------------------------------------------
data LabelAGItf = LabelAGItf_AGItf {lab_LabelAGItf_AGItf :: !(Label)}
deriving ( Eq,Generic,Ord,Show,Typeable)
-- Pred --------------------------------------------------------
data Pred = Pred_Class {ty_Pred_Class :: !(Ty)}
| Pred_Pred {ty_Pred_Pred :: !(Ty)}
| Pred_Lacks {ty_Pred_Lacks :: !(Ty),lab_Pred_Lacks :: !(Label)}
| Pred_Arrow {args_Pred_Arrow :: !(PredSeq),res_Pred_Arrow :: !(Pred)}
| Pred_Eq {tyL_Pred_Eq :: !(Ty),tyR_Pred_Eq :: !(Ty)}
| Pred_Var {pv_Pred_Var :: !(TyVarId)}
| Pred_Preds {seq_Pred_Preds :: !(PredSeq)}
deriving ( Eq,Generic,Ord,Show,Typeable)
-- PredSeq -----------------------------------------------------
data PredSeq = PredSeq_Cons {hd_PredSeq_Cons :: !(Pred),tl_PredSeq_Cons :: !(PredSeq)}
| PredSeq_Nil {}
| PredSeq_Var {av_PredSeq_Var :: !(TyVarId)}
deriving ( Eq,Generic,Ord,Show,Typeable)
-- Ty ----------------------------------------------------------
data Ty = Ty_Con {nm_Ty_Con :: !(HsName)}
| Ty_App {func_Ty_App :: !(Ty),arg_Ty_App :: !(Ty)}
| Ty_Ann {ann_Ty_Ann :: !(TyAnn),ty_Ty_Ann :: !(Ty)}
| Ty_Dbg {info_Ty_Dbg :: !(String)}
| Ty_Any {}
| Ty_Var {tv_Ty_Var :: !(TyVarId),categ_Ty_Var :: !(TyVarCateg)}
| Ty_TBind {qu_Ty_TBind :: !(TyQu),tv_Ty_TBind :: !(TyVarId),l1_Ty_TBind :: !(Ty),ty_Ty_TBind :: !(Ty)}
| Ty_Ext {ty_Ty_Ext :: !(Ty),nm_Ty_Ext :: !(HsName),extTy_Ty_Ext :: !(Ty)}
| Ty_Pred {pr_Ty_Pred :: !(Pred)}
| Ty_Lam {tv_Ty_Lam :: !(TyVarId),ty_Ty_Lam :: !(Ty)}
| Ty_Impls {impls_Ty_Impls :: !(Impls)}
deriving ( Eq,Generic,Ord,Show,Typeable)
-- TyAGItf -----------------------------------------------------
data TyAGItf = TyAGItf_AGItf {ty_TyAGItf_AGItf :: !(Ty)}
deriving ( Eq,Generic,Ord,Show,Typeable)
-- TyAnn -------------------------------------------------------
data TyAnn = TyAnn_Empty {}
| TyAnn_Strictness {s_TyAnn_Strictness :: !(Strictness)}
| TyAnn_Mono {}
deriving ( Eq,Generic,Ord,Show,Typeable)
-- TyQu --------------------------------------------------------
data TyQu = TyQu_Forall {mlev_TyQu_Forall :: !(MetaLev)}
| TyQu_Exists {mlev_TyQu_Exists :: !(MetaLev)}
| TyQu_Plain {mlev_TyQu_Plain :: !(MetaLev)}
deriving ( Eq,Generic,Ord,Show,Typeable)
-- TyVarCateg --------------------------------------------------
data TyVarCateg = TyVarCateg_Plain {}
| TyVarCateg_Fixed {}
| TyVarCateg_Meta {}
deriving ( Enum,Eq,Generic,Ord,Show,Typeable)