-- 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 , tyquEqModuloLev, 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 tyquEqModuloLev (TyQu_Forall {}) (TyQu_Forall {}) = True tyquEqModuloLev (TyQu_Exists {}) (TyQu_Exists {}) = True tyquEqModuloLev _ _ = 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 {qu_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 {ty_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 {tv_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)