import Control.Monad
import MonadUtils
import Data.Maybe
+import Pair
\end{code}
Note [GHC Formalism]
= do { (k,s,t,r) <- lintCoercion co'
; checkRole co Nominal r
; return (k,s,t,Representational) }
+
+
+lintCoercion this@(AxiomRuleCo co ts cs)
+ = do _ks <- mapM lintType ts
+ eqs <- mapM lintCoercion cs
+
+ let tyNum = length ts
+
+ case compare (coaxrTypeArity co) tyNum of
+ EQ -> return ()
+ LT -> err "Too many type arguments"
+ [ txt "expected" <+> int (coaxrTypeArity co)
+ , txt "provided" <+> int tyNum ]
+ GT -> err "Not enough type arguments"
+ [ txt "expected" <+> int (coaxrTypeArity co)
+ , txt "provided" <+> int tyNum ]
+ checkRoles 0 (coaxrAsmpRoles co) eqs
+
+ case coaxrProves co ts [ Pair l r | (_,l,r,_) <- eqs ] of
+ Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
+ Just (Pair l r) ->
+ do kL <- lintType l
+ kR <- lintType r
+ unless (eqKind kL kR)
+ $ err "Kind error in CoAxiomRule"
+ [ppr kL <+> txt "/=" <+> ppr kR]
+ return (kL, l, r, coaxrRole co)
+ where
+ txt = ptext . sLit
+ err m xs = failWithL $
+ hang (txt m) 2 $ vcat (txt "Rule:" <+> ppr (coaxrName co) : xs)
+
+ checkRoles n (e : es) ((_,_,_,r) : rs)
+ | e == r = checkRoles (n+1) es rs
+ | otherwise = err "Argument roles mismatch"
+ [ txt "In argument:" <+> int (n+1)
+ , txt "Expected:" <+> ppr e
+ , txt "Found:" <+> ppr r ]
+ checkRoles _ [] [] = return ()
+ checkRoles n [] rs = err "Too many coercion arguments"
+ [ txt "Expected:" <+> int n
+ , txt "Provided:" <+> int (n + length rs) ]
+
+ checkRoles n es [] = err "Not enough coercion arguments"
+ [ txt "Expected:" <+> int (n + length es)
+ , txt "Provided:" <+> int n ]
+
\end{code}
%************************************************************************
make_co dflags (LRCo lr co) = C.LRCoercion (make_lr lr) (make_co dflags co)
make_co dflags (InstCo co ty) = C.InstCoercion (make_co dflags co) (make_ty dflags ty)
make_co dflags (SubCo co) = C.SubCoercion (make_co dflags co)
+make_co _ (AxiomRuleCo {}) = panic "make_co AxiomRuleCo: not yet implemented"
+
make_lr :: LeftOrRight -> C.LeftOrRight
make_lr CLeft = C.CLeft
CoercionMap,
MaybeMap,
ListMap,
- TrieMap(..)
+ TrieMap(..),
+ lookupTypeMapTyCon
) where
import CoreSyn
import Name
import Type
import TypeRep
+import TyCon(TyCon)
import Var
import UniqFM
import Unique( Unique )
import FastString(FastString)
+import CoAxiom(CoAxiomRule(coaxrName))
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
, km_left :: CoercionMap a
, km_right :: CoercionMap a
, km_inst :: CoercionMap (TypeMap a)
- , km_sub :: CoercionMap a }
+ , km_sub :: CoercionMap a
+ , km_axiom_rule :: Map.Map FastString
+ (ListMap TypeMap (ListMap CoercionMap a))
+ }
wrapEmptyKM :: CoercionMap a
wrapEmptyKM = KM { km_refl = emptyTM, km_tc_app = emptyTM
, km_var = emptyTM, km_axiom = emptyNameEnv
, km_univ = emptyTM, km_sym = emptyTM, km_trans = emptyTM
, km_nth = emptyTM, km_left = emptyTM, km_right = emptyTM
- , km_inst = emptyTM, km_sub = emptyTM }
+ , km_inst = emptyTM, km_sub = emptyTM
+ , km_axiom_rule = emptyTM }
instance TrieMap CoercionMap where
type Key CoercionMap = Coercion
, km_var = kvar, km_axiom = kax
, km_univ = kuniv , km_sym = ksym, km_trans = ktrans
, km_nth = knth, km_left = kml, km_right = kmr
- , km_inst = kinst, km_sub = ksub })
+ , km_inst = kinst, km_sub = ksub
+ , km_axiom_rule = kaxr })
= KM { km_refl = mapTM (mapTM f) krefl
, km_tc_app = mapTM (mapNameEnv (mapTM f)) ktc
, km_app = mapTM (mapTM f) kapp
, km_left = mapTM f kml
, km_right = mapTM f kmr
, km_inst = mapTM (mapTM f) kinst
- , km_sub = mapTM f ksub }
+ , km_sub = mapTM f ksub
+ , km_axiom_rule = mapTM (mapTM (mapTM f)) kaxr
+ }
lkC :: CmEnv -> Coercion -> CoercionMap a -> Maybe a
lkC env co m
go (LRCo CLeft c) = km_left >.> lkC env c
go (LRCo CRight c) = km_right >.> lkC env c
go (SubCo c) = km_sub >.> lkC env c
+ go (AxiomRuleCo co ts cs) = km_axiom_rule >.>
+ lookupTM (coaxrName co) >=>
+ lkList (lkT env) ts >=>
+ lkList (lkC env) cs
+
xtC :: CmEnv -> Coercion -> XT a -> CoercionMap a -> CoercionMap a
xtC env co f EmptyKM = xtC env co f wrapEmptyKM
xtC env (LRCo CLeft c) f m = m { km_left = km_left m |> xtC env c f }
xtC env (LRCo CRight c) f m = m { km_right = km_right m |> xtC env c f }
xtC env (SubCo c) f m = m { km_sub = km_sub m |> xtC env c f }
+xtC env (AxiomRuleCo co ts cs) f m = m { km_axiom_rule = km_axiom_rule m
+ |> alterTM (coaxrName co)
+ |>> xtList (xtT env) ts
+ |>> xtList (xtC env) cs f}
fdC :: (a -> b -> b) -> CoercionMap a -> b -> b
fdC _ EmptyKM = \z -> z
. foldTM k (km_right m)
. foldTM (foldTM k) (km_inst m)
. foldTM k (km_sub m)
+ . foldTM (foldTM (foldTM k)) (km_axiom_rule m)
\end{code}
lookupTypeMap :: TypeMap a -> Type -> Maybe a
lookupTypeMap cm t = lkT emptyCME t cm
+-- Returns the type map entries that have keys starting with the given tycon.
+-- This only considers saturated applications (i.e. TyConApp ones).
+lookupTypeMapTyCon :: TypeMap a -> TyCon -> [a]
+lookupTypeMapTyCon EmptyTM _ = []
+lookupTypeMapTyCon TM { tm_tc_app = cs } tc =
+ case lookupUFM cs tc of
+ Nothing -> []
+ Just xs -> foldTM (:) xs []
+
extendTypeMap :: TypeMap a -> Type -> a -> TypeMap a
extendTypeMap m t v = xtT emptyCME t (\_ -> Just v) m
go r (TcCastCo co1 co2) = maybeSubCo r $ mkCoCast (go Nominal co1)
(go Nominal co2)
go r (TcCoVarCo v) = maybeSubCo r $ ds_ev_id subst v
+ go _ (TcAxiomRuleCo co ts cs) = AxiomRuleCo co
+ (map (Coercion.substTy subst) ts)
+ (map (go Nominal) cs)
+
+
ds_co_binds :: TcEvBinds -> CvSubst
ds_co_binds (EvBinds bs) = foldl ds_scc subst (sccEvBinds bs)
TcInteract
TcCanonical
TcSMonad
+ TcTypeNats
Class
Coercion
FamInstEnv
# We therefore need to split some of the modules off into a separate
# DLL. This clump are the modules reachable from DynFlags:
compiler_stage2_dll0_START_MODULE = DynFlags
-compiler_stage2_dll0_MODULES = Annotations Avail Bag BasicTypes Binary Bitmap BlockId BreakArray BufWrite ByteCodeAsm ByteCodeInstr ByteCodeItbls ByteCodeLink CLabel Class CmdLineParser Cmm CmmCallConv CmmExpr CmmInfo CmmMachOp CmmNode CmmType CmmUtils CoAxiom CodeGen.Platform CodeGen.Platform.ARM CodeGen.Platform.NoRegs CodeGen.Platform.PPC CodeGen.Platform.PPC_Darwin CodeGen.Platform.SPARC CodeGen.Platform.X86 CodeGen.Platform.X86_64 Coercion Config Constants CoreArity CoreFVs CoreSubst CoreSyn CoreTidy CoreUnfold CoreUtils CostCentre DataCon Demand Digraph DriverPhases DynFlags Encoding ErrUtils Exception FamInstEnv FastBool FastFunctions FastMutInt FastString FastTypes Fingerprint FiniteMap ForeignCall Hoopl Hoopl.Dataflow HsBinds HsDecls HsDoc HsExpr HsImpExp HsLit HsPat HsSyn HsTypes HsUtils HscTypes Id IdInfo IfaceSyn IfaceType InstEnv InteractiveEvalTypes Kind ListSetOps Literal Maybes MkCore MkGraph MkId Module MonadUtils Name NameEnv NameSet ObjLink OccName OccurAnal OptCoercion OrdList Outputable PackageConfig Packages Pair Panic Platform PlatformConstants PprCmm PprCmmDecl PprCmmExpr PprCore PrelNames PrelRules Pretty PrimOp RdrName Reg RegClass Rules SMRep Serialized SrcLoc StaticFlags StgCmmArgRep StgCmmClosure StgCmmEnv StgCmmLayout StgCmmMonad StgCmmProf StgCmmTicky StgCmmUtils StgSyn Stream StringBuffer TcEvidence TcType TrieMap TyCon Type TypeRep TysPrim TysWiredIn Unify UniqFM UniqSet UniqSupply Unique Util Var VarEnv VarSet
+
+compiler_stage2_dll0_MODULES =Annotations Avail Bag BasicTypes BinIface Binary Bitmap BlockId BreakArray BufWrite BuildTyCl ByteCodeAsm ByteCodeInstr ByteCodeItbls ByteCodeLink CLabel Class CmdLineParser Cmm CmmCallConv CmmExpr CmmInfo CmmMachOp CmmNode CmmType CmmUtils CoAxiom CodeGen.Platform CodeGen.Platform.ARM CodeGen.Platform.NoRegs CodeGen.Platform.PPC CodeGen.Platform.PPC_Darwin CodeGen.Platform.SPARC CodeGen.Platform.X86 CodeGen.Platform.X86_64 Coercion Config Constants CoreArity CoreFVs CoreLint CoreSubst CoreSyn CoreTidy CoreUnfold CoreUtils CostCentre DataCon Demand Digraph DriverPhases DynFlags Encoding ErrUtils Exception FamInst FamInstEnv FastBool FastFunctions FastMutInt FastString FastTypes Finder Fingerprint FiniteMap ForeignCall Hoopl Hoopl.Dataflow HsBinds HsDecls HsDoc HsExpr HsImpExp HsLit HsPat HsSyn HsTypes HsUtils HscTypes IOEnv Id IdInfo IfaceEnv IfaceSyn IfaceType InstEnv InteractiveEvalTypes Kind ListSetOps Literal LoadIface Maybes MkCore MkGraph MkId Module MonadUtils Name NameEnv NameSet ObjLink OccName OccurAnal OptCoercion OrdList Outputable PackageConfig Packages Pair Panic Platform PlatformConstants PprCmm PprCmmDecl PprCmmExpr PprCore PrelInfo PrelNames PrelRules Pretty PrimOp RdrName Reg RegClass Rules SMRep Serialized SrcLoc StaticFlags StgCmmArgRep StgCmmClosure StgCmmEnv StgCmmLayout StgCmmMonad StgCmmProf StgCmmTicky StgCmmUtils StgSyn Stream StringBuffer TcEvidence TcIface TcMType TcRnMonad TcRnTypes TcType TcTypeNats TrieMap TyCon Type TypeRep TysPrim TysWiredIn Unify UniqFM UniqSet UniqSupply Unique Util Var VarEnv VarSet
compiler_stage2_dll0_HS_OBJS = \
$(patsubst %,compiler/stage2/build/%.$(dyn_osuf),$(subst .,/,$(compiler_stage2_dll0_MODULES)))
= freeNamesIfCoercion co &&& freeNamesIfType ty
freeNamesIfCoercion (IfaceSubCo co)
= freeNamesIfCoercion co
+freeNamesIfCoercion (IfaceAxiomRuleCo _ax tys cos)
+ -- the axiom is just a string, so we don't count it as a name.
+ = fnList freeNamesIfType tys &&&
+ fnList freeNamesIfCoercion cos
freeNamesIfTvBndrs :: [IfaceTvBndr] -> NameSet
freeNamesIfTvBndrs = fnList freeNamesIfTvBndr
| IfaceLRCo LeftOrRight IfaceCoercion
| IfaceInstCo IfaceCoercion IfaceType
| IfaceSubCo IfaceCoercion
+ | IfaceAxiomRuleCo IfLclName [IfaceType] [IfaceCoercion]
\end{code}
%************************************************************************
= maybeParen ctxt_prec tYCON_PREC $
ptext (sLit "Inst") <+> pprParendIfaceCoercion co <+> pprParendIfaceType ty
+ppr_co ctxt_prec (IfaceAxiomRuleCo tc tys cos)
+ = maybeParen ctxt_prec tYCON_PREC
+ (sep [ppr tc, nest 4 (sep (map pprParendIfaceType tys ++ map pprParendIfaceCoercion cos))])
+
ppr_co ctxt_prec co
= ppr_special_co ctxt_prec doc cos
where (doc, cos) = case co of
put_ bh (IfaceSubCo a) = do
putByte bh 14
put_ bh a
-
+ put_ bh (IfaceAxiomRuleCo a b c) = do
+ putByte bh 15
+ put_ bh a
+ put_ bh b
+ put_ bh c
+
get bh = do
tag <- getByte bh
case tag of
return $ IfaceInstCo a b
14-> do a <- get bh
return $ IfaceSubCo a
+ 15-> do a <- get bh
+ b <- get bh
+ c <- get bh
+ return $ IfaceAxiomRuleCo a b c
_ -> panic ("get IfaceCoercion " ++ show tag)
\end{code}
(toIfaceType ty)
toIfaceCoercion (SubCo co) = IfaceSubCo (toIfaceCoercion co)
+toIfaceCoercion (AxiomRuleCo co ts cs) = IfaceAxiomRuleCo
+ (coaxrName co)
+ (map toIfaceType ts)
+ (map toIfaceCoercion cs)
\end{code}
to_ifsyn_rhs (SynonymTyCon ty)
= IfaceSynonymTyCon (tidyToIfaceType env1 ty)
+ to_ifsyn_rhs (BuiltInSynFamTyCon {}) = pprPanic "toIfaceDecl: BuiltInFamTyCon" (ppr tycon)
+
+
ifaceConDecls (NewTyCon { data_con = con }) = IfNewTyCon (ifaceConDecl con)
ifaceConDecls (DataTyCon { data_cons = cons }) = IfDataTyCon (map ifaceConDecl cons)
ifaceConDecls (DataFamilyTyCon {}) = IfDataFamTyCon
#include "HsVersions.h"
+import TcTypeNats(typeNatCoAxiomRules)
import IfaceSyn
import LoadIface
import IfaceEnv
import FastString
import Control.Monad
+import qualified Data.Map as Map
\end{code}
This module takes
tcIfaceCo (IfaceNthCo d c) = NthCo d <$> tcIfaceCo c
tcIfaceCo (IfaceLRCo lr c) = LRCo lr <$> tcIfaceCo c
tcIfaceCo (IfaceSubCo c) = SubCo <$> tcIfaceCo c
+tcIfaceCo (IfaceAxiomRuleCo ax tys cos) = AxiomRuleCo
+ <$> tcIfaceCoAxiomRule ax
+ <*> mapM tcIfaceType tys
+ <*> mapM tcIfaceCo cos
tcIfaceCoVar :: FastString -> IfL CoVar
tcIfaceCoVar = tcIfaceLclId
+
+tcIfaceCoAxiomRule :: FastString -> IfL CoAxiomRule
+tcIfaceCoAxiomRule n =
+ case Map.lookup n typeNatCoAxiomRules of
+ Just ax -> return ax
+ _ -> pprPanic "tcIfaceCoAxiomRule" (ppr n)
\end{code}
AbstractClosedSynFamilyTyCon -> closed_family_header <+> ptext (sLit "..")
SynonymTyCon rhs_ty -> hang (pprTyConHdr pefas tyCon <+> equals)
2 (ppr rhs_ty) -- Don't suppress foralls on RHS type!
+ BuiltInSynFamTyCon {} -> pprTyConHdr pefas tyCon <+> dcolon <+>
+ pprTypeForUser pefas (GHC.synTyConResKind tyCon)
+
-- e.g. type T = forall a. a->a
| Just cls <- GHC.tyConClass_maybe tyCon
= pprClass pefas ss cls
import Class
import TyCon
import Util
+import {-# SOURCE #-} TcTypeNats ( typeNatTyCons )
import Data.Array
\end{code}
, map (AnId . primOpId) allThePrimOps
]
where
- tycon_things = map ATyCon ([funTyCon] ++ primTyCons ++ wiredInTyCons)
+ tycon_things = map ATyCon ([funTyCon] ++ primTyCons ++ wiredInTyCons
+ ++ typeNatTyCons)
\end{code}
We let a lot of "non-standard" values be visible, so that we can make
-- Type-level naturals
singIClassName,
- typeNatLeqClassName,
- typeNatAddTyFamName,
- typeNatMulTyFamName,
- typeNatExpTyFamName,
-- Implicit parameters
ipClassName,
isStringClassName = clsQual dATA_STRING (fsLit "IsString") isStringClassKey
-- Type-level naturals
-singIClassName, typeNatLeqClassName,
- typeNatAddTyFamName, typeNatMulTyFamName, typeNatExpTyFamName :: Name
+singIClassName :: Name
singIClassName = clsQual gHC_TYPELITS (fsLit "SingI") singIClassNameKey
-typeNatLeqClassName = clsQual gHC_TYPELITS (fsLit "<=") typeNatLeqClassNameKey
-typeNatAddTyFamName = tcQual gHC_TYPELITS (fsLit "+") typeNatAddTyFamNameKey
-typeNatMulTyFamName = tcQual gHC_TYPELITS (fsLit "*") typeNatMulTyFamNameKey
-typeNatExpTyFamName = tcQual gHC_TYPELITS (fsLit "^") typeNatExpTyFamNameKey
-- Implicit parameters
ipClassName :: Name
selectorClassKey = mkPreludeClassUnique 41
-- SingI: see Note [SingI and EvLit] in TcEvidence
-singIClassNameKey, typeNatLeqClassNameKey :: Unique
+singIClassNameKey :: Unique
singIClassNameKey = mkPreludeClassUnique 42
-typeNatLeqClassNameKey = mkPreludeClassUnique 43
ghciIoClassKey :: Unique
ghciIoClassKey = mkPreludeClassUnique 44
-- Type-level naturals
typeNatKindConNameKey, typeSymbolKindConNameKey,
- typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey
+ typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey,
+ typeNatLeqTyFamNameKey
:: Unique
typeNatKindConNameKey = mkPreludeTyConUnique 160
typeSymbolKindConNameKey = mkPreludeTyConUnique 161
typeNatAddTyFamNameKey = mkPreludeTyConUnique 162
typeNatMulTyFamNameKey = mkPreludeTyConUnique 163
typeNatExpTyFamNameKey = mkPreludeTyConUnique 164
+typeNatLeqTyFamNameKey = mkPreludeTyConUnique 165
-- SIMD vector types (Unique keys)
floatX4PrimTyConKey, doubleX2PrimTyConKey, int32X4PrimTyConKey,
boolTy, boolTyCon, boolTyCon_RDR, boolTyConName,
trueDataCon, trueDataConId, true_RDR,
falseDataCon, falseDataConId, false_RDR,
+ promotedBoolTyCon, promotedFalseDataCon, promotedTrueDataCon,
-- * Ordering
ltDataCon, ltDataConId,
-- * Equality predicates
eqTyCon_RDR, eqTyCon, eqTyConName, eqBoxDataCon,
+ mkWiredInTyConName -- This is used in TcTypeNats to define the
+ -- built-in functions for evaluation.
) where
#include "HsVersions.h"
isPArrFakeCon :: DataCon -> Bool
isPArrFakeCon dcon = dcon == parrFakeCon (dataConSourceArity dcon)
\end{code}
+
+Promoted Booleans
+
+\begin{code}
+promotedBoolTyCon, promotedFalseDataCon, promotedTrueDataCon :: TyCon
+promotedBoolTyCon = promoteTyCon boolTyCon
+promotedTrueDataCon = promoteDataCon trueDataCon
+promotedFalseDataCon = promoteDataCon falseDataCon
+\end{code}
+
+
+
checkFamInstConsistency, tcExtendLocalFamInstEnv,
tcLookupFamInst,
tcGetFamInstEnvs,
- newFamInst
+ newFamInst,
+ TcBuiltInSynFamily(..), trivialBuiltInFamily
) where
+import Pair(Pair)
import HscTypes
import FamInstEnv
import InstEnv( roughMatchTcs )
import Control.Monad
import Data.Map (Map)
import qualified Data.Map as Map
+import TcEvidence(TcCoercion)
#include "HsVersions.h"
\end{code}
= do { eps <- getEps; env <- getGblEnv
; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }
\end{code}
+
+
+Type checking of built-in families
+==================================
+
+\begin{code}
+data TcBuiltInSynFamily = TcBuiltInSynFamily
+ { sfMatchFam :: [Type] -> Maybe (TcCoercion, TcType)
+ , sfInteractTop :: [Type] -> Type -> [Pair TcType]
+ , sfInteractInert :: [Type] -> Type ->
+ [Type] -> Type -> [Pair TcType]
+ }
+
+-- Provides default implementations that do nothing.
+trivialBuiltInFamily :: TcBuiltInSynFamily
+trivialBuiltInFamily = TcBuiltInSynFamily
+ { sfMatchFam = \_ -> Nothing
+ , sfInteractTop = \_ _ -> []
+ , sfInteractInert = \_ _ _ _ -> []
+ }
+\end{code}
+
+
--- /dev/null
+\begin{code}
+module FamInst where
+
+data TcBuiltInSynFamily
+\end{code}
mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcInstCos,
+ mkTcAxiomRuleCo,
tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo,
isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
liftTcCoSubstWith
| TcCoVarCo EqVar -- variable always at role N
| TcAxiomInstCo (CoAxiom Branched) Int [TcType] -- Int specifies branch number
-- See [CoAxiom Index] in Coercion.lhs
+ -- This is number of types and coercions are expected to macth to CoAxiomRule
+ -- (i.e., the CoAxiomRules are always fully saturated)
+ | TcAxiomRuleCo CoAxiomRule [TcType] [TcCoercion]
| TcSymCo TcCoercion
| TcTransCo TcCoercion TcCoercion
| TcNthCo Int TcCoercion
arity = coAxiomArity ax ind
ax_br = toBranchedAxiom ax
+mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercion
+mkTcAxiomRuleCo = TcAxiomRuleCo
+
mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] -> TcCoercion
mkTcUnbranchedAxInstCo ax tys
= mkTcAxInstCo ax 0 tys
go (TcTransCo co1 co2) = Pair (pFst (go co1)) (pSnd (go co2))
go (TcNthCo d co) = tyConAppArgN d <$> go co
go (TcLRCo lr co) = (pickLR lr . tcSplitAppTy) <$> go co
+ go (TcAxiomRuleCo ax ts cs) =
+ case coaxrProves ax ts (map tcCoercionKind cs) of
+ Just res -> res
+ Nothing -> panic "tcCoercionKind: malformed TcAxiomRuleCo"
-- c.f. Coercion.coercionKind
go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)
`minusVarSet` get_bndrs bs
go (TcLetCo {}) = emptyVarSet -- Harumph. This does legitimately happen in the call
-- to evVarsOfTerm in the DEBUG check of setEvBind
+ go (TcAxiomRuleCo _ _ cos) = foldr (unionVarSet . go) emptyVarSet cos
+
-- We expect only coercion bindings, so use evTermCoercion
go_bind :: EvBind -> VarSet
ppr_co p (TcSymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
ppr_co p (TcNthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
ppr_co p (TcLRCo lr co) = pprPrefixApp p (ppr lr) [pprParendTcCo co]
+ppr_co p (TcAxiomRuleCo co ts ps) = maybeParen p TopPrec
+ $ ppr_tc_axiom_rule_co co ts ps
+
+ppr_tc_axiom_rule_co :: CoAxiomRule -> [TcType] -> [TcCoercion] -> SDoc
+ppr_tc_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
+ where
+ ppTs [] = Outputable.empty
+ ppTs [t] = ptext (sLit "@") <> ppr_type TopPrec t
+ ppTs ts = ptext (sLit "@") <>
+ parens (hsep $ punctuate comma $ map pprType ts)
+
+ ppPs [] = Outputable.empty
+ ppPs [p] = pprParendTcCo p
+ ppPs (p : ps) = ptext (sLit "(") <+> pprTcCo p $$
+ vcat [ ptext (sLit ",") <+> pprTcCo q | q <- ps ] $$
+ ptext (sLit ")")
+
+
+
ppr_fun_co :: Prec -> TcCoercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
go (TcForAllCo tv co) = ASSERT( isImmutableTyVar tv )
do { co' <- go co; return (mkTcForAllCo tv co') }
go (TcInstCo co ty) = do { co' <- go co; ty' <- zonkTcTypeToType env ty; return (TcInstCo co' ty') }
+ go (TcAxiomRuleCo co ts cs) = do { ts' <- zonkTcTypeToTypes env ts
+ ; cs' <- mapM go cs
+ ; return (TcAxiomRuleCo co ts' cs')
+ }
\end{code}
import Type
import Unify
import FamInstEnv
+import FamInst(TcBuiltInSynFamily(..))
import InstEnv( lookupInstEnv, instanceDFunId )
import Var
import Bag
import Control.Monad ( foldM )
+import Data.Maybe(catMaybes)
import VarEnv
import Control.Monad( when, unless )
-import Pair ()
+import Pair (Pair(..))
import Unique( hasKey )
import UniqFM
import FastString ( sLit )
= do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
; rels <- extractRelevantInerts wi
; traceTcS "relevant inerts are:" $ ppr rels
+ ; builtInInteractions
; foldlBagM interact_next (ContinueWith wi) rels }
where interact_next Stop atomic_inert
-> do { insertInertItemTcS atomic_inert
; return (ContinueWith wi) }
}
+
+ -- See if we can compute some new derived work for built-ins.
+ builtInInteractions
+ | CFunEqCan { cc_fun = tc, cc_tyargs = args, cc_rhs = xi } <- wi
+ , Just ops <- isBuiltInSynFamTyCon_maybe tc =
+ do is <- getInertsFunEqTyCon tc
+ traceTcS "builtInCandidates: " $ ppr is
+ let interact = sfInteractInert ops args xi
+ impMbs <- sequence
+ [ do mb <- newDerived (mkTcEqPred lhs rhs)
+ case mb of
+ Just x -> return $ Just $ mkNonCanonical d x
+ Nothing -> return Nothing
+ | CFunEqCan { cc_tyargs = iargs
+ , cc_rhs = ixi
+ , cc_loc = d } <- is
+ , Pair lhs rhs <- interact iargs ixi
+ ]
+ let imps = catMaybes impMbs
+ unless (null imps) $ updWorkListTcS (extendWorkListEqs imps)
+ | otherwise = return ()
+
+
+
+
\end{code}
\begin{code}
succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
_other ->
- -- Look up in top-level instances
+ -- Look up in top-level instances, or built-in axiom
do { match_res <- matchFam fun_tc args -- See Note [MATCHING-SYNONYMS]
; case match_res of {
- Nothing -> return NoTopInt ;
+ Nothing -> try_improve_and_return ;
Just (co, ty) ->
-- Found a top-level instance
where
fam_ty = mkTyConApp fun_tc args
+ try_improve_and_return =
+ do { case isBuiltInSynFamTyCon_maybe fun_tc of
+ Just ops ->
+ do { let eqns = sfInteractTop ops args xi
+ ; impsMb <- mapM (\(Pair x y) -> newDerived (mkTcEqPred x y))
+ eqns
+ ; let work = map (mkNonCanonical loc) (catMaybes impsMb)
+ ; unless (null work) (updWorkListTcS (extendWorkListEqs work))
+ }
+ _ -> return ()
+ ; return NoTopInt
+ }
+
succeed_with :: String -> TcCoercion -> TcType -> TcS TopInteractResult
succeed_with str co rhs_ty -- co :: fun_tc args ~ rhs_ty
= do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
= eqClosedFamilyAx ax1 ax2
eqSynRhs (SynonymTyCon t1) (SynonymTyCon t2)
= eqTypeX env t1 t2
+ eqSynRhs (BuiltInSynFamTyCon _) (BuiltInSynFamTyCon _) = tc1 == tc2
eqSynRhs _ _ = False
in
roles1 == roles2 &&
modifyInertTcS,
insertInertItemTcS, partitionCCanMap, partitionEqMap,
getRelevantCts, extractRelevantInerts,
+ getInertsFunEqTyCon,
CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
PredMap, FamHeadMap,
partCtFamHeadMap, lookupFamHead, lookupSolvedDict,
|| unsolved_dicts || unsolved_funeqs
|| not (isEmptyBag (inert_insols icans)))) }
+
+{- Get inert function equation constraints that have the given tycon
+in their head. Not that the constraints remain in the inert set.
+We use this to check for derived interactions with built-in type-function
+constructors. -}
+getInertsFunEqTyCon :: TyCon -> TcS [Ct]
+getInertsFunEqTyCon tc =
+ do is <- getTcSInerts
+ let mp = unFamHeadMap $ inert_funeqs $ inert_cans is
+ return $ lookupTypeMapTyCon mp tc
+
+
extractRelevantInerts :: Ct -> TcS Cts
-- Returns the constraints from the inert set that are 'relevant' to react with
-- this constraint. The monad is left with the 'thinner' inerts.
ty = pSnd (tcCoercionKind co)
in return $ Just (co, ty)
+ | Just ops <- isBuiltInSynFamTyCon_maybe tycon = return (sfMatchFam ops args)
+
| otherwise
= return Nothing
SynonymTyCon ty ->
do { check_roles
; checkValidType syn_ctxt ty }
+ BuiltInSynFamTyCon _ -> return ()
| otherwise
= do { unless (isFamilyTyCon tc) $ check_roles -- don't check data families!
orphNamesOfCo (LRCo _ co) = orphNamesOfCo co
orphNamesOfCo (InstCo co ty) = orphNamesOfCo co `unionNameSets` orphNamesOfType ty
orphNamesOfCo (SubCo co) = orphNamesOfCo co
+orphNamesOfCo (AxiomRuleCo _ ts cs) = orphNamesOfTypes ts `unionNameSets`
+ orphNamesOfCos cs
orphNamesOfCos :: [Coercion] -> NameSet
orphNamesOfCos = orphNamesOfThings orphNamesOfCo
--- /dev/null
+module TcTypeNats
+ ( typeNatTyCons
+ , typeNatCoAxiomRules
+ , TcBuiltInSynFamily(..)
+ ) where
+
+import Type
+import Pair
+import TcType ( TcType )
+import TyCon ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..) )
+import Coercion ( Role(..) )
+import TcRnTypes ( Xi )
+import TcEvidence ( mkTcAxiomRuleCo, TcCoercion )
+import CoAxiom ( CoAxiomRule(..) )
+import Name ( Name, BuiltInSyntax(..) )
+import TysWiredIn ( typeNatKind, mkWiredInTyConName
+ , promotedBoolTyCon
+ , promotedFalseDataCon, promotedTrueDataCon
+ )
+import TysPrim ( tyVarList, mkArrowKinds )
+import PrelNames ( gHC_TYPELITS
+ , typeNatAddTyFamNameKey
+ , typeNatMulTyFamNameKey
+ , typeNatExpTyFamNameKey
+ , typeNatLeqTyFamNameKey
+ )
+import FamInst ( TcBuiltInSynFamily(..) )
+import FastString ( FastString, fsLit )
+import qualified Data.Map as Map
+import Data.Maybe ( isJust )
+
+{-------------------------------------------------------------------------------
+Built-in type constructors for functions on type-lelve nats
+-}
+
+typeNatTyCons :: [TyCon]
+typeNatTyCons =
+ [ typeNatAddTyCon
+ , typeNatMulTyCon
+ , typeNatExpTyCon
+ , typeNatLeqTyCon
+ ]
+
+typeNatAddTyCon :: TyCon
+typeNatAddTyCon = mkTypeNatFunTyCon2 name
+ TcBuiltInSynFamily
+ { sfMatchFam = matchFamAdd
+ , sfInteractTop = interactTopAdd
+ , sfInteractInert = interactInertAdd
+ }
+ where
+ name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "+")
+ typeNatAddTyFamNameKey typeNatAddTyCon
+
+typeNatMulTyCon :: TyCon
+typeNatMulTyCon = mkTypeNatFunTyCon2 name
+ TcBuiltInSynFamily
+ { sfMatchFam = matchFamMul
+ , sfInteractTop = interactTopMul
+ , sfInteractInert = interactInertMul
+ }
+ where
+ name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "*")
+ typeNatMulTyFamNameKey typeNatMulTyCon
+
+typeNatExpTyCon :: TyCon
+typeNatExpTyCon = mkTypeNatFunTyCon2 name
+ TcBuiltInSynFamily
+ { sfMatchFam = matchFamExp
+ , sfInteractTop = interactTopExp
+ , sfInteractInert = interactInertExp
+ }
+ where
+ name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "^")
+ typeNatExpTyFamNameKey typeNatExpTyCon
+
+typeNatLeqTyCon :: TyCon
+typeNatLeqTyCon =
+ mkSynTyCon name
+ (mkArrowKinds [ typeNatKind, typeNatKind ] boolKind)
+ (take 2 $ tyVarList typeNatKind)
+ [Nominal,Nominal]
+ (BuiltInSynFamTyCon ops)
+ NoParentTyCon
+
+ where
+ name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?")
+ typeNatLeqTyFamNameKey typeNatLeqTyCon
+ ops = TcBuiltInSynFamily
+ { sfMatchFam = matchFamLeq
+ , sfInteractTop = interactTopLeq
+ , sfInteractInert = interactInertLeq
+ }
+
+
+-- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
+mkTypeNatFunTyCon2 :: Name -> TcBuiltInSynFamily -> TyCon
+mkTypeNatFunTyCon2 op tcb =
+ mkSynTyCon op
+ (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind)
+ (take 2 $ tyVarList typeNatKind)
+ [Nominal,Nominal]
+ (BuiltInSynFamTyCon tcb)
+ NoParentTyCon
+
+
+
+
+{-------------------------------------------------------------------------------
+Built-in rules axioms
+-------------------------------------------------------------------------------}
+
+-- If you add additional rules, please remember to add them to
+-- `typeNatCoAxiomRules` also.
+axAddDef
+ , axMulDef
+ , axExpDef
+ , axLeqDef
+ , axAdd0L
+ , axAdd0R
+ , axMul0L
+ , axMul0R
+ , axMul1L
+ , axMul1R
+ , axExp1L
+ , axExp0R
+ , axExp1R
+ , axLeqRefl
+ , axLeq0L
+ :: CoAxiomRule
+
+axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
+ \x y -> num (x + y)
+
+axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $
+ \x y -> num (x * y)
+
+axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $
+ \x y -> num (x ^ y)
+
+axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $
+ \x y -> bool (x <= y)
+
+axAdd0L = mkAxiom1 "Add0L" $ \t -> (num 0 .+. t) === t
+axAdd0R = mkAxiom1 "Add0R" $ \t -> (t .+. num 0) === t
+axMul0L = mkAxiom1 "Mul0L" $ \t -> (num 0 .*. t) === num 0
+axMul0R = mkAxiom1 "Mul0R" $ \t -> (t .*. num 0) === num 0
+axMul1L = mkAxiom1 "Mul1L" $ \t -> (num 1 .*. t) === t
+axMul1R = mkAxiom1 "Mul1R" $ \t -> (t .*. num 1) === t
+axExp1L = mkAxiom1 "Exp1L" $ \t -> (num 1 .^. t) === num 1
+axExp0R = mkAxiom1 "Exp0R" $ \t -> (t .^. num 0) === num 1
+axExp1R = mkAxiom1 "Exp1R" $ \t -> (t .^. num 1) === t
+axLeqRefl = mkAxiom1 "LeqRefl" $ \t -> (t <== t) === bool True
+axLeq0L = mkAxiom1 "Leq0L" $ \t -> (num 0 <== t) === bool True
+
+typeNatCoAxiomRules :: Map.Map FastString CoAxiomRule
+typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
+ [ axAddDef
+ , axMulDef
+ , axExpDef
+ , axLeqDef
+ , axAdd0L
+ , axAdd0R
+ , axMul0L
+ , axMul0R
+ , axMul1L
+ , axMul1R
+ , axExp1L
+ , axExp0R
+ , axExp1R
+ , axLeqRefl
+ , axLeq0L
+ ]
+
+
+
+{-------------------------------------------------------------------------------
+Various utilities for making axioms and types
+-------------------------------------------------------------------------------}
+
+(.+.) :: Type -> Type -> Type
+s .+. t = mkTyConApp typeNatAddTyCon [s,t]
+
+(.*.) :: Type -> Type -> Type
+s .*. t = mkTyConApp typeNatMulTyCon [s,t]
+
+(.^.) :: Type -> Type -> Type
+s .^. t = mkTyConApp typeNatExpTyCon [s,t]
+
+(<==) :: Type -> Type -> Type
+s <== t = mkTyConApp typeNatLeqTyCon [s,t]
+
+(===) :: Type -> Type -> Pair Type
+x === y = Pair x y
+
+num :: Integer -> Type
+num = mkNumLitTy
+
+boolKind :: Kind
+boolKind = mkTyConApp promotedBoolTyCon []
+
+bool :: Bool -> Type
+bool b = if b then mkTyConApp promotedTrueDataCon []
+ else mkTyConApp promotedFalseDataCon []
+
+isBoolLitTy :: Type -> Maybe Bool
+isBoolLitTy tc =
+ do (tc,[]) <- splitTyConApp_maybe tc
+ case () of
+ _ | tc == promotedFalseDataCon -> return False
+ | tc == promotedTrueDataCon -> return True
+ | otherwise -> Nothing
+
+known :: (Integer -> Bool) -> TcType -> Bool
+known p x = case isNumLitTy x of
+ Just a -> p a
+ Nothing -> False
+
+
+
+
+-- For the definitional axioms
+mkBinAxiom :: String -> TyCon ->
+ (Integer -> Integer -> Type) -> CoAxiomRule
+mkBinAxiom str tc f =
+ CoAxiomRule
+ { coaxrName = fsLit str
+ , coaxrTypeArity = 2
+ , coaxrAsmpRoles = []
+ , coaxrRole = Nominal
+ , coaxrProves = \ts cs ->
+ case (ts,cs) of
+ ([s,t],[]) -> do x <- isNumLitTy s
+ y <- isNumLitTy t
+ return (mkTyConApp tc [s,t] === f x y)
+ _ -> Nothing
+ }
+
+mkAxiom1 :: String -> (Type -> Pair Type) -> CoAxiomRule
+mkAxiom1 str f =
+ CoAxiomRule
+ { coaxrName = fsLit str
+ , coaxrTypeArity = 1
+ , coaxrAsmpRoles = []
+ , coaxrRole = Nominal
+ , coaxrProves = \ts cs ->
+ case (ts,cs) of
+ ([s],[]) -> return (f s)
+ _ -> Nothing
+ }
+
+
+{-------------------------------------------------------------------------------
+Evaluation
+-------------------------------------------------------------------------------}
+
+matchFamAdd :: [Type] -> Maybe (TcCoercion, TcType)
+matchFamAdd [s,t]
+ | Just 0 <- mbX = Just (mkTcAxiomRuleCo axAdd0L [t] [], t)
+ | Just 0 <- mbY = Just (mkTcAxiomRuleCo axAdd0R [s] [], s)
+ | Just x <- mbX, Just y <- mbY =
+ Just (mkTcAxiomRuleCo axAddDef [s,t] [], num (x + y))
+ where mbX = isNumLitTy s
+ mbY = isNumLitTy t
+matchFamAdd _ = Nothing
+
+matchFamMul :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamMul [s,t]
+ | Just 0 <- mbX = Just (mkTcAxiomRuleCo axMul0L [t] [], num 0)
+ | Just 0 <- mbY = Just (mkTcAxiomRuleCo axMul0R [s] [], num 0)
+ | Just 1 <- mbX = Just (mkTcAxiomRuleCo axMul1L [t] [], t)
+ | Just 1 <- mbY = Just (mkTcAxiomRuleCo axMul1R [s] [], s)
+ | Just x <- mbX, Just y <- mbY =
+ Just (mkTcAxiomRuleCo axMulDef [s,t] [], num (x * y))
+ where mbX = isNumLitTy s
+ mbY = isNumLitTy t
+matchFamMul _ = Nothing
+
+matchFamExp :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamExp [s,t]
+ | Just 0 <- mbY = Just (mkTcAxiomRuleCo axExp0R [s] [], num 1)
+ | Just 1 <- mbX = Just (mkTcAxiomRuleCo axExp1L [t] [], num 1)
+ | Just 1 <- mbY = Just (mkTcAxiomRuleCo axExp1R [s] [], s)
+ | Just x <- mbX, Just y <- mbY =
+ Just (mkTcAxiomRuleCo axExpDef [s,t] [], num (x ^ y))
+ where mbX = isNumLitTy s
+ mbY = isNumLitTy t
+matchFamExp _ = Nothing
+
+matchFamLeq :: [Xi] -> Maybe (TcCoercion, Xi)
+matchFamLeq [s,t]
+ | Just 0 <- mbX = Just (mkTcAxiomRuleCo axLeq0L [t] [], bool True)
+ | Just x <- mbX, Just y <- mbY =
+ Just (mkTcAxiomRuleCo axLeqDef [s,t] [], bool (x <= y))
+ | eqType s t = Just (mkTcAxiomRuleCo axLeqRefl [s] [], bool True)
+ where mbX = isNumLitTy s
+ mbY = isNumLitTy t
+matchFamLeq _ = Nothing
+
+{-------------------------------------------------------------------------------
+Interact with axioms
+-------------------------------------------------------------------------------}
+
+interactTopAdd :: [Xi] -> Xi -> [Pair Type]
+interactTopAdd [s,t] r
+ | Just 0 <- mbZ = [ s === num 0, t === num 0 ]
+ | Just x <- mbX, Just z <- mbZ, Just y <- minus z x = [t === num y]
+ | Just y <- mbY, Just z <- mbZ, Just x <- minus z y = [s === num x]
+ where
+ mbX = isNumLitTy s
+ mbY = isNumLitTy t
+ mbZ = isNumLitTy r
+interactTopAdd _ _ = []
+
+interactTopMul :: [Xi] -> Xi -> [Pair Type]
+interactTopMul [s,t] r
+ | Just 1 <- mbZ = [ s === num 1, t === num 1 ]
+ | Just x <- mbX, Just z <- mbZ, Just y <- divide z x = [t === num y]
+ | Just y <- mbY, Just z <- mbZ, Just x <- divide z y = [s === num x]
+ where
+ mbX = isNumLitTy s
+ mbY = isNumLitTy t
+ mbZ = isNumLitTy r
+interactTopMul _ _ = []
+
+interactTopExp :: [Xi] -> Xi -> [Pair Type]
+interactTopExp [s,t] r
+ | Just 0 <- mbZ = [ s === num 0 ]
+ | Just x <- mbX, Just z <- mbZ, Just y <- logExact z x = [t === num y]
+ | Just y <- mbY, Just z <- mbZ, Just x <- rootExact z y = [s === num x]
+ where
+ mbX = isNumLitTy s
+ mbY = isNumLitTy t
+ mbZ = isNumLitTy r
+interactTopExp _ _ = []
+
+interactTopLeq :: [Xi] -> Xi -> [Pair Type]
+interactTopLeq [s,t] r
+ | Just 0 <- mbY, Just True <- mbZ = [ s === num 0 ]
+ where
+ mbY = isNumLitTy t
+ mbZ = isBoolLitTy r
+interactTopLeq _ _ = []
+
+
+
+{-------------------------------------------------------------------------------
+Interacton with inerts
+-------------------------------------------------------------------------------}
+
+interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertAdd [x1,y1] z1 [x2,y2] z2
+ | sameZ && eqType x1 x2 = [ y1 === y2 ]
+ | sameZ && eqType y1 y2 = [ x1 === x2 ]
+ where sameZ = eqType z1 z2
+interactInertAdd _ _ _ _ = []
+
+interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertMul [x1,y1] z1 [x2,y2] z2
+ | sameZ && known (/= 0) x1 && eqType x1 x2 = [ y1 === y2 ]
+ | sameZ && known (/= 0) y1 && eqType y1 y2 = [ x1 === x2 ]
+ where sameZ = eqType z1 z2
+
+interactInertMul _ _ _ _ = []
+
+interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertExp [x1,y1] z1 [x2,y2] z2
+ | sameZ && known (> 1) x1 && eqType x1 x2 = [ y1 === y2 ]
+ | sameZ && known (> 0) y1 && eqType y1 y2 = [ x1 === x2 ]
+ where sameZ = eqType z1 z2
+
+interactInertExp _ _ _ _ = []
+
+
+interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertLeq [x1,y1] z1 [x2,y2] z2
+ | bothTrue && eqType x1 y2 && eqType y1 x2 = [ x1 === y1 ]
+ | bothTrue && eqType y1 x2 = [ (x1 <== y2) === bool True ]
+ | bothTrue && eqType y2 x1 = [ (x2 <== y1) === bool True ]
+ where bothTrue = isJust $ do True <- isBoolLitTy z1
+ True <- isBoolLitTy z2
+ return ()
+
+interactInertLeq _ _ _ _ = []
+
+
+
+
+{- -----------------------------------------------------------------------------
+These inverse functions are used for simplifying propositions using
+concrete natural numbers.
+----------------------------------------------------------------------------- -}
+
+-- | Subtract two natural numbers.
+minus :: Integer -> Integer -> Maybe Integer
+minus x y = if x >= y then Just (x - y) else Nothing
+
+-- | Compute the exact logarithm of a natural number.
+-- The logarithm base is the second argument.
+logExact :: Integer -> Integer -> Maybe Integer
+logExact x y = do (z,True) <- genLog x y
+ return z
+
+
+-- | Divide two natural numbers.
+divide :: Integer -> Integer -> Maybe Integer
+divide _ 0 = Nothing
+divide x y = case divMod x y of
+ (a,0) -> Just a
+ _ -> Nothing
+
+-- | Compute the exact root of a natural number.
+-- The second argument specifies which root we are computing.
+rootExact :: Integer -> Integer -> Maybe Integer
+rootExact x y = do (z,True) <- genRoot x y
+ return z
+
+
+
+{- | Compute the the n-th root of a natural number, rounded down to
+the closest natural number. The boolean indicates if the result
+is exact (i.e., True means no rounding was done, False means rounded down).
+The second argument specifies which root we are computing. -}
+genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
+genRoot _ 0 = Nothing
+genRoot x0 1 = Just (x0, True)
+genRoot x0 root = Just (search 0 (x0+1))
+ where
+ search from to = let x = from + div (to - from) 2
+ a = x ^ root
+ in case compare a x0 of
+ EQ -> (x, True)
+ LT | x /= from -> search x to
+ | otherwise -> (from, False)
+ GT | x /= to -> search from x
+ | otherwise -> (from, False)
+
+{- | Compute the logarithm of a number in the given base, rounded down to the
+closest integer. The boolean indicates if we the result is exact
+(i.e., True means no rounding happened, False means we rounded down).
+The logarithm base is the second argument. -}
+genLog :: Integer -> Integer -> Maybe (Integer, Bool)
+genLog x 0 = if x == 1 then Just (0, True) else Nothing
+genLog _ 1 = Nothing
+genLog 0 _ = Nothing
+genLog x base = Just (exactLoop 0 x)
+ where
+ exactLoop s i
+ | i == 1 = (s,True)
+ | i < base = (s,False)
+ | otherwise =
+ let s1 = s + 1
+ in s1 `seq` case divMod i base of
+ (j,r)
+ | r == 0 -> exactLoop s1 j
+ | otherwise -> (underLoop s1 j, False)
+
+ underLoop s i
+ | i < base = s
+ | otherwise = let s1 = s + 1 in s1 `seq` underLoop s1 (div i base)
+
+
+
+
+
+
+
--- /dev/null
+module TcTypeNats where
+
+import TyCon (TyCon)
+
+typeNatTyCons :: [TyCon]
coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
placeHolderIncomps,
- Role(..), pprFullRole
+ Role(..), pprFullRole,
+
+ CoAxiomRule(..), Eqn
) where
import {-# SOURCE #-} TypeRep ( Type )
import Var
import Util
import Binary
+import Pair
import BasicTypes
import Data.Typeable ( Typeable )
import SrcLoc
3 -> return Phantom
_ -> panic ("get Role " ++ show tag)
-\end{code}
\ No newline at end of file
+\end{code}
+
+
+Rules for building Evidence
+---------------------------
+
+Conditional axioms. The genral idea is that a `CoAxiomRule` looks like this:
+
+ forall as. (r1 ~ r2, s1 ~ s2) => t1 ~ t2
+
+My intension is to reuse these for both (~) and (~#).
+The short-term plan is to use this datatype to represent the type-nat axioms.
+In the longer run, it would probably be good to unify this and `CoAxiom`,
+as `CoAxiom` is the special case when there are no assumptions.
+
+\begin{code}
+-- | A more explicit representation for `t1 ~ t2`.
+type Eqn = Pair Type
+
+-- | For now, we work only with nominal equality.
+data CoAxiomRule = CoAxiomRule
+ { coaxrName :: FastString
+ , coaxrTypeArity :: Int -- number of type argumentInts
+ , coaxrAsmpRoles :: [Role] -- roles of parameter equations
+ , coaxrRole :: Role -- role of resulting equation
+ , coaxrProves :: [Type] -> [Eqn] -> Maybe Eqn
+ -- ^ This returns @Nothing@ when we don't like
+ -- the supplied arguments.
+ } deriving Typeable
+
+instance Data.Data CoAxiomRule where
+ -- don't traverse?
+ toConstr _ = abstractConstr "CoAxiomRule"
+ gunfold _ _ = error "gunfold"
+ dataTypeOf _ = mkNoRepType "CoAxiomRule"
+
+instance Uniquable CoAxiomRule where
+ getUnique = getUnique . coaxrName
+
+instance Eq CoAxiomRule where
+ x == y = coaxrName x == coaxrName y
+
+instance Ord CoAxiomRule where
+ compare x y = compare (coaxrName x) (coaxrName y)
+
+instance Outputable CoAxiomRule where
+ ppr = ppr . coaxrName
+\end{code}
+
mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
mkForAllCo, mkUnsafeCo, mkUnivCo, mkSubCo, mkPhantomCo,
mkNewTypeCo, maybeSubCo, maybeSubCo2,
+ mkAxiomRuleCo,
-- ** Decomposition
splitNewTypeRepCo_maybe, instNewTyCon_maybe,
| SymCo Coercion -- :: e -> e
| TransCo Coercion Coercion -- :: e -> e -> e
+ -- The number of types and coercions should match exactly the expectations
+ -- of the CoAxiomRule (i.e., the rule is fully saturated).
+ | AxiomRuleCo CoAxiomRule [Type] [Coercion]
+
-- These are destructors
| NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
tyCoVarsOfCo (LRCo _ co) = tyCoVarsOfCo co
tyCoVarsOfCo (InstCo co ty) = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
tyCoVarsOfCo (SubCo co) = tyCoVarsOfCo co
+tyCoVarsOfCo (AxiomRuleCo _ ts cs) = tyVarsOfTypes ts `unionVarSet` tyCoVarsOfCos cs
tyCoVarsOfCos :: [Coercion] -> VarSet
tyCoVarsOfCos cos = foldr (unionVarSet . tyCoVarsOfCo) emptyVarSet cos
coVarsOfCo (LRCo _ co) = coVarsOfCo co
coVarsOfCo (InstCo co _) = coVarsOfCo co
coVarsOfCo (SubCo co) = coVarsOfCo co
+coVarsOfCo (AxiomRuleCo _ _ cos) = coVarsOfCos cos
coVarsOfCos :: [Coercion] -> VarSet
coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos
coercionSize (LRCo _ co) = 1 + coercionSize co
coercionSize (InstCo co ty) = 1 + coercionSize co + typeSize ty
coercionSize (SubCo co) = 1 + coercionSize co
+coercionSize (AxiomRuleCo _ tys cos) = 1 + sum (map typeSize tys)
+ + sum (map coercionSize cos)
\end{code}
%************************************************************************
go (InstCo co ty) = (InstCo $! go co) $! tidyType env ty
go (SubCo co) = SubCo $! go co
+ go (AxiomRuleCo ax tys cos) = let tys1 = map (tidyType env) tys
+ cos1 = tidyCos env cos
+ in tys1 `seqList` cos1 `seqList`
+ AxiomRuleCo ax tys1 cos1
+
+
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env = map (tidyCo env)
\end{code}
ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
ppr_co p (LRCo sel co) = pprPrefixApp p (ppr sel) [pprParendCo co]
ppr_co p (SubCo co) = pprPrefixApp p (ptext (sLit "Sub")) [pprParendCo co]
+ppr_co p (AxiomRuleCo co ts cs) = maybeParen p TopPrec $
+ ppr_axiom_rule_co co ts cs
+
+ppr_axiom_rule_co :: CoAxiomRule -> [Type] -> [Coercion] -> SDoc
+ppr_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
+ where
+ ppTs [] = Outputable.empty
+ ppTs [t] = ptext (sLit "@") <> ppr_type TopPrec t
+ ppTs ts = ptext (sLit "@") <>
+ parens (hsep $ punctuate comma $ map pprType ts)
+
+ ppPs [] = Outputable.empty
+ ppPs [p] = pprParendCo p
+ ppPs (p : ps) = ptext (sLit "(") <+> pprCo p $$
+ vcat [ ptext (sLit ",") <+> pprCo q | q <- ps ] $$
+ ptext (sLit ")")
+
+
ppr_role :: Role -> SDoc
ppr_role r = underscore <> ppr r
| ty1 `eqType` ty2 = Refl role ty1
| otherwise = UnivCo role ty1 ty2
+mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
+mkAxiomRuleCo = AxiomRuleCo
+
-- input coercion is Nominal
mkSubCo :: Coercion -> Coercion
mkSubCo (Refl Nominal ty) = Refl Representational ty
mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co )
SubCo co
+
-- takes a Nominal coercion and possibly casts it into a Representational one
maybeSubCo :: Role -> Coercion -> Coercion
maybeSubCo Nominal = id
coreEqCoercion2 env (SubCo co1) (SubCo co2)
= coreEqCoercion2 env co1 co2
+coreEqCoercion2 env (AxiomRuleCo a1 ts1 cs1) (AxiomRuleCo a2 ts2 cs2)
+ = a1 == a2 && all2 (eqTypeX env) ts1 ts2 && all2 (coreEqCoercion2 env) cs1 cs2
+
coreEqCoercion2 _ _ _ = False
\end{code}
go (LRCo lr co) = mkLRCo lr (go co)
go (InstCo co ty) = mkInstCo (go co) $! go_ty ty
go (SubCo co) = mkSubCo (go co)
+ go (AxiomRuleCo co ts cs) = let ts1 = map go_ty ts
+ cs1 = map go cs
+ in ts1 `seqList` cs1 `seqList`
+ AxiomRuleCo co ts1 cs1
+
+
substCoVar :: CvSubst -> CoVar -> Coercion
substCoVar (CvSubst in_scope _ cenv) cv
seqCo (LRCo _ co) = seqCo co
seqCo (InstCo co ty) = seqCo co `seq` seqType ty
seqCo (SubCo co) = seqCo co
+seqCo (AxiomRuleCo _ ts cs) = seqTypes ts `seq` seqCos cs
seqCos :: [Coercion] -> ()
seqCos [] = ()
go (LRCo lr co) = (pickLR lr . splitAppTy) <$> go co
go (InstCo aco ty) = go_app aco [ty]
go (SubCo co) = go co
+ go (AxiomRuleCo ax tys cos) =
+ case coaxrProves ax tys (map coercionKind cos) of
+ Just res -> res
+ Nothing -> panic "coercionKind: Malformed coercion"
+
go_app :: Coercion -> [Type] -> Pair Type
-- Collect up all the arguments and apply all at once
go (LRCo _ _) = Nominal
go (InstCo co _) = go co
go (SubCo _) = Representational
+ go (AxiomRuleCo c _ _) = coaxrRole c
\end{code}
Note [Nested InstCos]
opt_co' env sym _ (SubCo co) = opt_co env sym (Just Representational) co
+-- XXX: We could add another field to CoAxiomRule that
+-- would allow us to do custom simplifications.
+opt_co' env sym mrole (AxiomRuleCo co ts cs) =
+ wrapRole mrole (coaxrRole co) $
+ wrapSym sym $
+ AxiomRuleCo co (map (substTy env) ts)
+ (zipWith (opt_co env False) (map Just (coaxrAsmpRoles co)) cs)
+
+
+
-------------
opt_univ :: CvSubst -> Role -> Type -> Type -> Coercion
opt_univ env role oty1 oty2
isFamilyTyCon, isOpenFamilyTyCon,
isSynFamilyTyCon, isDataFamilyTyCon,
isOpenSynFamilyTyCon, isClosedSynFamilyTyCon_maybe,
+ isBuiltInSynFamTyCon_maybe,
isUnLiftedTyCon,
isGadtSyntaxTyCon, isDistinctTyCon, isDistinctAlgRhs,
isTyConAssoc, tyConAssoc_maybe,
-- * Recursion breaking
RecTcChecker, initRecTc, checkRecTc
+
) where
#include "HsVersions.h"
import {-# SOURCE #-} TypeRep ( Kind, Type, PredType )
import {-# SOURCE #-} DataCon ( DataCon, isVanillaDataCon )
+import {-# SOURCE #-} FamInst ( TcBuiltInSynFamily )
import Var
import Class
-- | A closed type synonym family declared in an hs-boot file with
-- type family F a where ..
| AbstractClosedSynFamilyTyCon
+
+ | BuiltInSynFamTyCon TcBuiltInSynFamily
\end{code}
Note [Closed type families]
isFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon }) = True
isFamilyTyCon (SynTyCon {synTcRhs = ClosedSynFamilyTyCon {} }) = True
isFamilyTyCon (SynTyCon {synTcRhs = AbstractClosedSynFamilyTyCon {} }) = True
+isFamilyTyCon (SynTyCon {synTcRhs = BuiltInSynFamTyCon {} }) = True
isFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
isFamilyTyCon _ = False
isSynFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon {}}) = True
isSynFamilyTyCon (SynTyCon {synTcRhs = ClosedSynFamilyTyCon {}}) = True
isSynFamilyTyCon (SynTyCon {synTcRhs = AbstractClosedSynFamilyTyCon {}}) = True
+isSynFamilyTyCon (SynTyCon {synTcRhs = BuiltInSynFamTyCon {}}) = True
isSynFamilyTyCon _ = False
isOpenSynFamilyTyCon :: TyCon -> Bool
(SynTyCon {synTcRhs = ClosedSynFamilyTyCon ax}) = Just ax
isClosedSynFamilyTyCon_maybe _ = Nothing
+isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe TcBuiltInSynFamily
+isBuiltInSynFamTyCon_maybe
+ SynTyCon {synTcRhs = BuiltInSynFamTyCon ops } = Just ops
+isBuiltInSynFamTyCon_maybe _ = Nothing
+
-- | Is this a synonym 'TyCon' that can have may have further instances appear?
isDataFamilyTyCon :: TyCon -> Bool
isDataFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
git.haskell.org / ghc.git / commitdiff
