{-# LANGUAGE LambdaCase #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} -- See calls to mkTemplateTyVars module GHC.Builtin.Types.Literals ( tryInteractInertFam, tryInteractTopFam, tryMatchFam , typeNatTyCons , typeNatCoAxiomRules , BuiltInSynFamily(..) -- If you define a new built-in type family, make sure to export its TyCon -- from here as well. -- See Note [Adding built-in type families] , typeNatAddTyCon , typeNatMulTyCon , typeNatExpTyCon , typeNatSubTyCon , typeNatDivTyCon , typeNatModTyCon , typeNatLogTyCon , typeNatCmpTyCon , typeSymbolCmpTyCon , typeSymbolAppendTyCon , typeCharCmpTyCon , typeConsSymbolTyCon , typeUnconsSymbolTyCon , typeCharToNatTyCon , typeNatToCharTyCon ) where import GHC.Prelude import GHC.Core.Type import GHC.Core.Unify ( tcMatchTys ) import GHC.Data.Pair import GHC.Core.TyCon ( TyCon, FamTyConFlav(..), mkFamilyTyCon, tyConArity , Injectivity(..), isBuiltInSynFamTyCon_maybe ) import GHC.Core.Coercion.Axiom import GHC.Core.TyCo.Compare ( tcEqType ) import GHC.Types.Name ( Name, BuiltInSyntax(..) ) import GHC.Types.Unique.FM import GHC.Builtin.Types import GHC.Builtin.Types.Prim ( mkTemplateAnonTyConBinders, mkTemplateTyVars ) import GHC.Builtin.Names ( gHC_INTERNAL_TYPELITS , gHC_INTERNAL_TYPELITS_INTERNAL , gHC_INTERNAL_TYPENATS , gHC_INTERNAL_TYPENATS_INTERNAL , typeNatAddTyFamNameKey , typeNatMulTyFamNameKey , typeNatExpTyFamNameKey , typeNatSubTyFamNameKey , typeNatDivTyFamNameKey , typeNatModTyFamNameKey , typeNatLogTyFamNameKey , typeNatCmpTyFamNameKey , typeSymbolCmpTyFamNameKey , typeSymbolAppendFamNameKey , typeCharCmpTyFamNameKey , typeConsSymbolTyFamNameKey , typeUnconsSymbolTyFamNameKey , typeCharToNatTyFamNameKey , typeNatToCharTyFamNameKey ) import GHC.Data.FastString import GHC.Utils.Panic import GHC.Utils.Outputable import Control.Monad ( guard ) import Data.List ( isPrefixOf, isSuffixOf ) import Data.Maybe ( listToMaybe ) import qualified Data.Char as Char {- Note [Type-level literals] ~~~~~~~~~~~~~~~~~~~~~~~~~~ There are currently three forms of type-level literals: natural numbers, symbols, and characters. Type-level literals are supported by CoAxiomRules (conditional axioms), which power the built-in type families (see Note [Adding built-in type families]). Currently, all built-in type families are for the express purpose of supporting type-level literals. See also the Wiki page: https://gitlab.haskell.org/ghc/ghc/wikis/type-nats Note [Adding built-in type families] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ There are a few steps to adding a built-in type family: * Adding a unique for the type family TyCon These go in GHC.Builtin.Names. It will likely be of the form @myTyFamNameKey = mkPreludeTyConUnique xyz@, where @xyz@ is a number that has not been chosen before in GHC.Builtin.Names. There are several examples already in GHC.Builtin.Names—see, for instance, typeNatAddTyFamNameKey. * Adding the type family TyCon itself This goes in GHC.Builtin.Types.Literals. There are plenty of examples of how to define these -- see, for instance, typeNatAddTyCon. Once your TyCon has been defined, be sure to: - Export it from GHC.Builtin.Types.Literals. (Not doing so caused #14632.) - Include it in the typeNatTyCons list, defined in GHC.Builtin.Types.Literals. * Define the type family somewhere Finally, you will need to define the type family somewhere, likely in @base@. Currently, all of the built-in type families are defined in GHC.TypeLits or GHC.TypeNats, so those are likely candidates. Since the behavior of your built-in type family is specified in GHC.Builtin.Types.Literals, you should give an open type family definition with no instances, like so: type family MyTypeFam (m :: Nat) (n :: Nat) :: Nat Changing the argument and result kinds as appropriate. * Update the relevant test cases The GHC test suite will likely need to be updated after you add your built-in type family. For instance: - The T9181 test prints the :browse contents of GHC.TypeLits, so if you added a test there, the expected output of T9181 will need to change. - The TcTypeNatSimple and TcTypeSymbolSimple tests have compile-time unit tests, as well as TcTypeNatSimpleRun and TcTypeSymbolSimpleRun, which have runtime unit tests. Consider adding further unit tests to those if your built-in type family deals with Nats or Symbols, respectively. Note [Inlining axiom constructors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We have a number of constructor functions with types like mkUnaryConstFoldAxiom :: TyCon -> String -> (Type -> Maybe a) -> (a -> Maybe Type) -> BuiltInFamRewrite For very type-family-heavy code, these higher order argument are inefficient; e.g. the fourth argument might always return (Just ty) in the above. Inlining them is a bit brutal, but not bad, makes a few-percent difference in, say perf test T13386. These functions aren't exported, so the effect is very local. -} ------------------------------------------------------------------------------- -- Key utility functions ------------------------------------------------------------------------------- tryInteractTopFam :: BuiltInSynFamily -> TyCon -> [Type] -> Type -> [(CoAxiomRule, TypeEqn)] -- The returned CoAxiomRule is always unary tryInteractTopFam fam fam_tc tys r = [(bifinj_axr bif, eqn_out) | bif <- sfInteract fam , Just eqn_out <- [bifinj_proves bif eqn_in] ] where eqn_in :: TypeEqn eqn_in = Pair (mkTyConApp fam_tc tys) r tryInteractInertFam :: BuiltInSynFamily -> TyCon -> [Type] -> [Type] -- F tys1 ~ F tys2 -> [(CoAxiomRule, TypeEqn)] tryInteractInertFam builtin_fam fam_tc tys1 tys2 = [(bifinj_axr bif, eqn_out) | bif <- sfInteract builtin_fam , Just eqn_out <- [bifinj_proves bif eqn_in] ] where eqn_in = Pair (mkTyConApp fam_tc tys1) (mkTyConApp fam_tc tys2) tryMatchFam :: BuiltInSynFamily -> [Type] -> Maybe (CoAxiomRule, [Type], Type) -- Does this reduce on the given arguments? -- If it does, returns (CoAxiomRule, types to instantiate the rule at, rhs type) -- That is: mkAxiomCo (BuiltInFamRew ax) (map mkNomReflCo ts) -- :: F tys ~r rhs, tryMatchFam builtin_fam arg_tys = listToMaybe $ -- Pick first rule to match [ (bifrw_axr rw_ax, inst_tys, res_ty) | rw_ax <- sfMatchFam builtin_fam , Just (inst_tys,res_ty) <- [bifrw_match rw_ax arg_tys] ] ------------------------------------------------------------------------------- -- Constructing BuiltInFamInjectivity, BuiltInFamRewrite ------------------------------------------------------------------------------- mkUnaryConstFoldAxiom :: TyCon -> String -> (Type -> Maybe a) -> (a -> Maybe Type) -> BuiltInFamRewrite -- For the definitional axioms, like (3+4 --> 7) {-# INLINE mkUnaryConstFoldAxiom #-} -- See Note [Inlining axiom constructors] mkUnaryConstFoldAxiom fam_tc str isReqTy f = bif where bif = BIF_Rewrite { bifrw_name = fsLit str , bifrw_axr = BuiltInFamRew bif , bifrw_fam_tc = fam_tc , bifrw_arity = 1 , bifrw_match = \ts -> do { [t1] <- return ts ; t1' <- isReqTy t1 ; res <- f t1' ; return ([t1], res) } , bifrw_proves = \cs -> do { [Pair s1 s2] <- return cs ; s2' <- isReqTy s2 ; z <- f s2' ; return (mkTyConApp fam_tc [s1] === z) } } mkBinConstFoldAxiom :: TyCon -> String -> (Type -> Maybe a) -> (Type -> Maybe b) -> (a -> b -> Maybe Type) -> BuiltInFamRewrite -- For the definitional axioms, like (3+4 --> 7) {-# INLINE mkBinConstFoldAxiom #-} -- See Note [Inlining axiom constructors] mkBinConstFoldAxiom fam_tc str isReqTy1 isReqTy2 f = bif where bif = BIF_Rewrite { bifrw_name = fsLit str , bifrw_axr = BuiltInFamRew bif , bifrw_fam_tc = fam_tc , bifrw_arity = 2 , bifrw_match = \ts -> do { [t1,t2] <- return ts ; t1' <- isReqTy1 t1 ; t2' <- isReqTy2 t2 ; res <- f t1' t2' ; return ([t1,t2], res) } , bifrw_proves = \cs -> do { [Pair s1 s2, Pair t1 t2] <- return cs ; s2' <- isReqTy1 s2 ; t2' <- isReqTy2 t2 ; z <- f s2' t2' ; return (mkTyConApp fam_tc [s1,t1] === z) } } mkRewriteAxiom :: TyCon -> String -> [TyVar] -> [Type] -- LHS of axiom -> Type -- RHS of axiom -> BuiltInFamRewrite -- Not higher order, no benefit in inlining -- See Note [Inlining axiom constructors] mkRewriteAxiom fam_tc str tpl_tvs lhs_tys rhs_ty = assertPpr (tyConArity fam_tc == length lhs_tys) (text str <+> ppr lhs_tys) $ bif where bif = BIF_Rewrite { bifrw_name = fsLit str , bifrw_axr = BuiltInFamRew bif , bifrw_fam_tc = fam_tc , bifrw_arity = bif_arity , bifrw_match = match_fn , bifrw_proves = inst_fn } bif_arity = length tpl_tvs match_fn :: [Type] -> Maybe ([Type],Type) match_fn arg_tys = assertPpr (tyConArity fam_tc == length arg_tys) (text str <+> ppr arg_tys) $ case tcMatchTys lhs_tys arg_tys of Nothing -> Nothing Just subst -> Just (substTyVars subst tpl_tvs, substTy subst rhs_ty) inst_fn :: [TypeEqn] -> Maybe TypeEqn inst_fn inst_eqns = assertPpr (length inst_eqns == bif_arity) (text str $$ ppr inst_eqns) $ Just (mkTyConApp fam_tc (substTys (zipTCvSubst tpl_tvs tys1) lhs_tys) === substTy (zipTCvSubst tpl_tvs tys2) rhs_ty) where (tys1, tys2) = unzipPairs inst_eqns mkTopUnaryFamDeduction :: String -> TyCon -> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity -- Deduction from (F s ~ r) where `F` is a unary type function {-# INLINE mkTopUnaryFamDeduction #-} -- See Note [Inlining axiom constructors] mkTopUnaryFamDeduction str fam_tc f = bif where bif = BIF_Interact { bifinj_name = fsLit str , bifinj_axr = BuiltInFamInj bif , bifinj_proves = \(Pair lhs rhs) -> do { (tc, [a]) <- splitTyConApp_maybe lhs ; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc) ; f a rhs } } mkTopBinFamDeduction :: String -> TyCon -> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity -- Deduction from (F s t ~ r) where `F` is a binary type function {-# INLINE mkTopBinFamDeduction #-} -- See Note [Inlining axiom constructors] mkTopBinFamDeduction str fam_tc f = bif where bif = BIF_Interact { bifinj_name = fsLit str , bifinj_axr = BuiltInFamInj bif , bifinj_proves = \(Pair lhs rhs) -> do { (tc, [a,b]) <- splitTyConApp_maybe lhs ; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc) ; f a b rhs } } mkUnaryBIF :: String -> TyCon -> BuiltInFamInjectivity -- Not higher order, no benefit in inlining -- See Note [Inlining axiom constructors] mkUnaryBIF str fam_tc = bif where bif = BIF_Interact { bifinj_name = fsLit str , bifinj_axr = BuiltInFamInj bif , bifinj_proves = proves } proves (Pair lhs rhs) = do { (tc2, [x2]) <- splitTyConApp_maybe rhs ; guard (tc2 == fam_tc) ; (tc1, [x1]) <- splitTyConApp_maybe lhs ; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc) ; return (Pair x1 x2) } mkBinBIF :: String -> TyCon -> WhichArg -> WhichArg -> (Type -> Bool) -- The guard on the equal args, if any -> BuiltInFamInjectivity {-# INLINE mkBinBIF #-} -- See Note [Inlining axiom constructors] mkBinBIF str fam_tc eq1 eq2 check_me = bif where bif = BIF_Interact { bifinj_name = fsLit str , bifinj_axr = BuiltInFamInj bif , bifinj_proves = proves } proves (Pair lhs rhs) = do { (tc2, [x2,y2]) <- splitTyConApp_maybe rhs ; guard (tc2 == fam_tc) ; (tc1, [x1,y1]) <- splitTyConApp_maybe lhs ; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc) ; case (eq1, eq2) of (ArgX,ArgX) -> do_it x1 x2 y1 y2 (ArgX,ArgY) -> do_it x1 y2 x2 y1 (ArgY,ArgX) -> do_it y1 x2 y2 x1 (ArgY,ArgY) -> do_it y1 y2 x1 x2 } do_it a1 a2 b1 b2 = do { same a1 a2; guard (check_me a1); return (Pair b1 b2) } noGuard :: Type -> Bool noGuard _ = True numGuard :: (Integer -> Bool) -> Type -> Bool numGuard pred ty = case isNumLitTy ty of Just n -> pred n Nothing -> False data WhichArg = ArgX | ArgY ------------------------------------------------------------------------------- -- Built-in type constructors for functions on type-level nats ------------------------------------------------------------------------------- -- The list of built-in type family TyCons that GHC uses. -- If you define a built-in type family, make sure to add it to this list. -- See Note [Adding built-in type families] typeNatTyCons :: [TyCon] typeNatTyCons = [ typeNatAddTyCon , typeNatMulTyCon , typeNatExpTyCon , typeNatSubTyCon , typeNatDivTyCon , typeNatModTyCon , typeNatLogTyCon , typeNatCmpTyCon , typeSymbolCmpTyCon , typeSymbolAppendTyCon , typeCharCmpTyCon , typeConsSymbolTyCon , typeUnconsSymbolTyCon , typeCharToNatTyCon , typeNatToCharTyCon ] -- The list of built-in type family axioms that GHC uses. -- If you define new axioms, make sure to include them in this list. -- See Note [Adding built-in type families] typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule typeNatCoAxiomRules = listToUFM $ [ pr | tc <- typeNatTyCons , Just ops <- [isBuiltInSynFamTyCon_maybe tc] , pr <- [ (bifinj_name bif, bifinj_axr bif) | bif <- sfInteract ops ] ++ [ (bifrw_name bif, bifrw_axr bif) | bif <- sfMatchFam ops ] ] ------------------------------------------------------------------------------- -- Addition (+) ------------------------------------------------------------------------------- typeNatAddTyCon :: TyCon typeNatAddTyCon = mkTypeNatFunTyCon2 name BuiltInSynFamily { sfMatchFam = axAddRewrites , sfInteract = axAddInjectivity } where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "+") typeNatAddTyFamNameKey typeNatAddTyCon sn,tn :: TyVar -- Of kind Natural (sn: tn: _) = mkTemplateTyVars (repeat typeSymbolKind) axAddRewrites :: [BuiltInFamRewrite] axAddRewrites = [ mkRewriteAxiom tc "Add0L" [tn] [num 0, var tn] (var tn) -- 0 + t --> t , mkRewriteAxiom tc "Add0R" [sn] [var sn, num 0] (var sn) -- s + 0 --> s , mkBinConstFoldAxiom tc "AddDef" isNumLitTy isNumLitTy $ -- 3 + 4 --> 7 \x y -> Just $ num (x + y) ] where tc = typeNatAddTyCon axAddInjectivity :: [BuiltInFamInjectivity] axAddInjectivity = [ -- (s + t ~ 0) => (s ~ 0) mkTopBinFamDeduction "AddT-0L" tc $ \ a _b r -> do { _ <- known r (== 0); return (Pair a (num 0)) } , -- (s + t ~ 0) => (t ~ 0) mkTopBinFamDeduction "AddT-0R" tc $ \ _a b r -> do { _ <- known r (== 0); return (Pair b (num 0)) } , -- (5 + t ~ 8) => (t ~ 3) mkTopBinFamDeduction "AddT-KKL" tc $ \ a b r -> do { na <- isNumLitTy a; nr <- known r (>= na); return (Pair b (num (nr-na))) } , -- (s + 5 ~ 8) => (s ~ 3) mkTopBinFamDeduction "AddT-KKR" tc $ \ a b r -> do { nb <- isNumLitTy b; nr <- known r (>= nb); return (Pair a (num (nr-nb))) } , mkBinBIF "AddI-xx" tc ArgX ArgX noGuard -- x1+y1~x2+y2 {x1=x2}=> (y1 ~ y2) , mkBinBIF "AddI-xy" tc ArgX ArgY noGuard -- x1+y1~x2+y2 {x1=y2}=> (x2 ~ y1) , mkBinBIF "AddI-yx" tc ArgY ArgX noGuard -- x1+y1~x2+y2 {y1=x2}=> (x1 ~ y2) , mkBinBIF "AddI-yy" tc ArgY ArgY noGuard -- x1+y1~x2+y2 {y1=y2}=> (x1 ~ x2) ] where tc = typeNatAddTyCon ------------------------------------------------------------------------------- -- Subtraction (-) ------------------------------------------------------------------------------- typeNatSubTyCon :: TyCon typeNatSubTyCon = mkTypeNatFunTyCon2 name BuiltInSynFamily { sfMatchFam = axSubRewrites , sfInteract = axSubInjectivity } where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "-") typeNatSubTyFamNameKey typeNatSubTyCon axSubRewrites :: [BuiltInFamRewrite] axSubRewrites = [ mkRewriteAxiom tc "Sub0R" [sn] [var sn, num 0] (var sn) -- s - 0 --> s , mkBinConstFoldAxiom tc "SubDef" isNumLitTy isNumLitTy $ -- 4 - 3 --> 1 if x>=y \x y -> fmap num (minus x y) ] where tc = typeNatSubTyCon axSubInjectivity :: [BuiltInFamInjectivity] axSubInjectivity = [ -- (a - b ~ 5) => (5 + b ~ a) mkTopBinFamDeduction "SubT" tc $ \ a b r -> do { _ <- isNumLitTy r; return (Pair (r .+. b) a) } , mkBinBIF "SubI-xx" tc ArgX ArgX noGuard -- (x-y1 ~ x-y2) => (y1 ~ y2) , mkBinBIF "SubI-yy" tc ArgY ArgY noGuard -- (x1-y ~ x2-y) => (x1 ~ x2) ] where tc = typeNatSubTyCon {- Note [Weakened interaction rule for subtraction] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ A simpler interaction here might be: `s - t ~ r` --> `t + r ~ s` This would enable us to reuse all the code for addition. Unfortunately, this works a little too well at the moment. Consider the following example: 0 - 5 ~ r --> 5 + r ~ 0 --> (5 = 0, r = 0) This (correctly) spots that the constraint cannot be solved. However, this may be a problem if the constraint did not need to be solved in the first place! Consider the following example: f :: Proxy (If (5 <=? 0) (0 - 5) (5 - 0)) -> Proxy 5 f = id Currently, GHC is strict while evaluating functions, so this does not work, because even though the `If` should evaluate to `5 - 0`, we also evaluate the "then" branch which generates the constraint `0 - 5 ~ r`, which fails. So, for the time being, we only add an improvement when the RHS is a constant, which happens to work OK for the moment, although clearly we need to do something more general. -} ------------------------------------------------------------------------------- -- Multiplication (*) ------------------------------------------------------------------------------- typeNatMulTyCon :: TyCon typeNatMulTyCon = mkTypeNatFunTyCon2 name BuiltInSynFamily { sfMatchFam = axMulRewrites , sfInteract = axMulInjectivity } where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "*") typeNatMulTyFamNameKey typeNatMulTyCon axMulRewrites :: [BuiltInFamRewrite] axMulRewrites = [ mkRewriteAxiom tc "Mul0L" [tn] [num 0, var tn] (num 0) -- 0 * t --> 0 , mkRewriteAxiom tc "Mul0R" [sn] [var sn, num 0] (num 0) -- s * 0 --> 0 , mkRewriteAxiom tc "Mul1L" [tn] [num 1, var tn] (var tn) -- 1 * t --> t , mkRewriteAxiom tc "Mul1R" [sn] [var sn, num 1] (var sn) -- s * 1 --> s , mkBinConstFoldAxiom tc "MulDef" isNumLitTy isNumLitTy $ -- 3 + 4 --> 12 \x y -> Just $ num (x * y) ] where tc = typeNatMulTyCon axMulInjectivity :: [BuiltInFamInjectivity] axMulInjectivity = [ -- (s * t ~ 1) => (s ~ 1) mkTopBinFamDeduction "MulT1" tc $ \ s _t r -> do { _ <- known r (== 1); return (Pair s r) } , -- (s * t ~ 1) => (t ~ 1) mkTopBinFamDeduction "MulT2" tc $ \ _s t r -> do { _ <- known r (== 1); return (Pair t r) } , -- (3 * t ~ 15) => (t ~ 5) mkTopBinFamDeduction "MulT3" tc $ \ s t r -> do { ns <- isNumLitTy s; nr <- isNumLitTy r; y <- divide nr ns; return (Pair t (num y)) } , -- (s * 3 ~ 15) => (s ~ 5) mkTopBinFamDeduction "MulT4" tc $ \ s t r -> do { nt <- isNumLitTy t; nr <- isNumLitTy r; y <- divide nr nt; return (Pair s (num y)) } , mkBinBIF "MulI-xx" tc ArgX ArgX (numGuard (/= 0)) -- (x*y1 ~ x*y2) {x/=0}=> (y1 ~ y2) , mkBinBIF "MulI-yy" tc ArgY ArgY (numGuard (/= 0)) -- (x1*y ~ x2*y) {y/=0}=> (x1 ~ x2) ] where tc = typeNatMulTyCon ------------------------------------------------------------------------------- -- Division: Div and Mod ------------------------------------------------------------------------------- typeNatDivTyCon :: TyCon typeNatDivTyCon = mkTypeNatFunTyCon2 name BuiltInSynFamily { sfMatchFam = axDivRewrites , sfInteract = [] } where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "Div") typeNatDivTyFamNameKey typeNatDivTyCon typeNatModTyCon :: TyCon typeNatModTyCon = mkTypeNatFunTyCon2 name BuiltInSynFamily { sfMatchFam = axModRewrites , sfInteract = [] } where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "Mod") typeNatModTyFamNameKey typeNatModTyCon axDivRewrites :: [BuiltInFamRewrite] axDivRewrites = [ mkRewriteAxiom tc "Div1" [sn] [var sn, num 1] (var sn) -- s `div` 1 --> s , mkBinConstFoldAxiom tc "DivDef" isNumLitTy isNumLitTy $ -- 8 `div` 4 --> 2 \x y -> do { guard (y /= 0); return (num (div x y)) } ] where tc = typeNatDivTyCon axModRewrites :: [BuiltInFamRewrite] axModRewrites = [ mkRewriteAxiom tc "Mod1" [sn] [var sn, num 1] (num 0) -- s `mod` 1 --> 0 , mkBinConstFoldAxiom tc "ModDef" isNumLitTy isNumLitTy $ -- 8 `mod` 3 --> 2 \x y -> do { guard (y /= 0); return (num (mod x y)) } ] where tc = typeNatModTyCon ------------------------------------------------------------------------------- -- Exponentiation: Exp ------------------------------------------------------------------------------- typeNatExpTyCon :: TyCon -- Exponentiation typeNatExpTyCon = mkTypeNatFunTyCon2 name BuiltInSynFamily { sfMatchFam = axExpRewrites , sfInteract = axExpInjectivity } where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "^") typeNatExpTyFamNameKey typeNatExpTyCon axExpRewrites :: [BuiltInFamRewrite] axExpRewrites = [ mkRewriteAxiom tc "Exp0R" [sn] [var sn, num 0] (num 1) -- s ^ 0 --> 1 , mkRewriteAxiom tc "Exp1L" [tn] [num 1, var tn] (num 1) -- 1 ^ t --> 1 , mkRewriteAxiom tc "Exp1R" [sn] [var sn, num 1] (var sn) -- s ^ 1 --> s , mkBinConstFoldAxiom tc "ExpDef" isNumLitTy isNumLitTy $ -- 2 ^ 3 --> 8 \x y -> Just (num (x ^ y)) ] where tc = typeNatExpTyCon axExpInjectivity :: [BuiltInFamInjectivity] axExpInjectivity = [ -- (s ^ t ~ 0) => (s ~ 0) mkTopBinFamDeduction "ExpT1" tc $ \ s _t r -> do { 0 <- isNumLitTy r; return (Pair s r) } , -- (2 ^ t ~ 8) => (t ~ 3) mkTopBinFamDeduction "ExpT2" tc $ \ s t r -> do { ns <- isNumLitTy s; nr <- isNumLitTy r; y <- logExact nr ns; return (Pair t (num y)) } , -- (s ^ 2 ~ 9) => (s ~ 3) mkTopBinFamDeduction "ExpT3" tc $ \ s t r -> do { nt <- isNumLitTy t; nr <- isNumLitTy r; y <- rootExact nr nt; return (Pair s (num y)) } , mkBinBIF "ExpI-xx" tc ArgX ArgX (numGuard (> 1)) -- (x^y1 ~ x^y2) {x>1}=> (y1 ~ y2) , mkBinBIF "ExpI-yy" tc ArgY ArgY (numGuard (/= 0)) -- (x1*y ~ x2*y) {y/=0}=> (x1 ~ x2) ] where tc = typeNatExpTyCon ------------------------------------------------------------------------------- -- Logarithm: Log2 ------------------------------------------------------------------------------- typeNatLogTyCon :: TyCon typeNatLogTyCon = mkTypeNatFunTyCon1 name BuiltInSynFamily { sfMatchFam = axLogRewrites , sfInteract = [] } where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "Log2") typeNatLogTyFamNameKey typeNatLogTyCon axLogRewrites :: [BuiltInFamRewrite] axLogRewrites = [ mkUnaryConstFoldAxiom tc "LogDef" isNumLitTy $ -- log 8 --> 3 \x -> do { (a,_) <- genLog x 2; return (num a) } ] where tc = typeNatLogTyCon ------------------------------------------------------------------------------- -- Comparision of Nats: CmpNat ------------------------------------------------------------------------------- typeNatCmpTyCon :: TyCon typeNatCmpTyCon = mkFamilyTyCon name (mkTemplateAnonTyConBinders [ naturalTy, naturalTy ]) orderingKind Nothing (BuiltInSynFamTyCon ops) Nothing NotInjective where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS_INTERNAL (fsLit "CmpNat") typeNatCmpTyFamNameKey typeNatCmpTyCon ops = BuiltInSynFamily { sfMatchFam = axCmpNatRewrites , sfInteract = axCmpNatInjectivity } axCmpNatRewrites :: [BuiltInFamRewrite] axCmpNatRewrites = [ mkRewriteAxiom tc "CmpNatRefl" [sn] [var sn, var sn] (ordering EQ) -- s `cmp` s --> EQ , mkBinConstFoldAxiom tc "CmpNatDef" isNumLitTy isNumLitTy $ -- 2 `cmp` 3 --> LT \x y -> Just (ordering (compare x y)) ] where tc = typeNatCmpTyCon axCmpNatInjectivity :: [BuiltInFamInjectivity] axCmpNatInjectivity = [ -- s `cmp` t ~ EQ ==> s ~ t mkTopBinFamDeduction "CmpNatT3" typeNatCmpTyCon $ \ s t r -> do { EQ <- isOrderingLitTy r; return (Pair s t) } ] ------------------------------------------------------------------------------- -- Comparsion of Symbols: CmpSymbol ------------------------------------------------------------------------------- typeSymbolCmpTyCon :: TyCon typeSymbolCmpTyCon = mkFamilyTyCon name (mkTemplateAnonTyConBinders [typeSymbolKind, typeSymbolKind]) orderingKind Nothing (BuiltInSynFamTyCon ops) Nothing NotInjective where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS_INTERNAL (fsLit "CmpSymbol") typeSymbolCmpTyFamNameKey typeSymbolCmpTyCon ops = BuiltInSynFamily { sfMatchFam = axSymbolCmpRewrites , sfInteract = axSymbolCmpInjectivity } ss,ts :: TyVar -- Of kind Symbol (ss: ts: _) = mkTemplateTyVars (repeat typeSymbolKind) axSymbolCmpRewrites :: [BuiltInFamRewrite] axSymbolCmpRewrites = [ mkRewriteAxiom tc "CmpSymbolRefl" [ss] [var ss, var ss] (ordering EQ) -- s `cmp` s --> EQ , mkBinConstFoldAxiom tc "CmpSymbolDef" isStrLitTy isStrLitTy $ -- "a" `cmp` "b" --> LT \x y -> Just (ordering (lexicalCompareFS x y)) ] where tc = typeSymbolCmpTyCon axSymbolCmpInjectivity :: [BuiltInFamInjectivity] axSymbolCmpInjectivity = [ mkTopBinFamDeduction "CmpSymbolT" typeSymbolCmpTyCon $ \ s t r -> do { EQ <- isOrderingLitTy r; return (Pair s t) } ] ------------------------------------------------------------------------------- -- AppendSymbol ------------------------------------------------------------------------------- typeSymbolAppendTyCon :: TyCon typeSymbolAppendTyCon = mkTypeSymbolFunTyCon2 name BuiltInSynFamily { sfMatchFam = axAppendRewrites , sfInteract = axAppendInjectivity } where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "AppendSymbol") typeSymbolAppendFamNameKey typeSymbolAppendTyCon axAppendRewrites :: [BuiltInFamRewrite] axAppendRewrites = [ mkRewriteAxiom tc "Concat0R" [ts] [nullStrLitTy, var ts] (var ts) -- "" ++ t --> t , mkRewriteAxiom tc "Concat0L" [ss] [var ss, nullStrLitTy] (var ss) -- s ++ "" --> s , mkBinConstFoldAxiom tc "AppendSymbolDef" isStrLitTy isStrLitTy $ -- "a" ++ "b" --> "ab" \x y -> Just (mkStrLitTy (appendFS x y)) ] where tc = typeSymbolAppendTyCon axAppendInjectivity :: [BuiltInFamInjectivity] axAppendInjectivity = [ -- (AppendSymbol a b ~ "") => (a ~ "") mkTopBinFamDeduction "AppendSymbolT1" tc $ \ a _b r -> do { rs <- isStrLitTy r; guard (nullFS rs); return (Pair a nullStrLitTy) } , -- (AppendSymbol a b ~ "") => (b ~ "") mkTopBinFamDeduction "AppendSymbolT2" tc $ \ _a b r -> do { rs <- isStrLitTy r; guard (nullFS rs); return (Pair b nullStrLitTy) } , -- (AppendSymbol "foo" b ~ "foobar") => (b ~ "bar") mkTopBinFamDeduction "AppendSymbolT3" tc $ \ a b r -> do { as <- isStrLitTyS a; rs <- isStrLitTyS r; guard (as `isPrefixOf` rs) ; return (Pair b (mkStrLitTyS (drop (length as) rs))) } , -- (AppendSymbol f "bar" ~ "foobar") => (f ~ "foo") mkTopBinFamDeduction "AppendSymbolT3" tc $ \ a b r -> do { bs <- isStrLitTyS b; rs <- isStrLitTyS r; guard (bs `isSuffixOf` rs) ; return (Pair a (mkStrLitTyS (take (length rs - length bs) rs))) } , mkBinBIF "AppI-xx" tc ArgX ArgX noGuard -- (x++y1 ~ x++y2) => (y1 ~ y2) , mkBinBIF "AppI-yy" tc ArgY ArgY noGuard -- (x1++y ~ x2++y) => (x1 ~ x2) ] where tc = typeSymbolAppendTyCon ------------------------------------------------------------------------------- -- ConsSymbol ------------------------------------------------------------------------------- typeConsSymbolTyCon :: TyCon typeConsSymbolTyCon = mkFamilyTyCon name (mkTemplateAnonTyConBinders [ charTy, typeSymbolKind ]) typeSymbolKind Nothing (BuiltInSynFamTyCon ops) Nothing (Injective [True, True]) where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "ConsSymbol") typeConsSymbolTyFamNameKey typeConsSymbolTyCon ops = BuiltInSynFamily { sfMatchFam = axConsRewrites , sfInteract = axConsInjectivity } axConsRewrites :: [BuiltInFamRewrite] axConsRewrites = [ mkBinConstFoldAxiom tc "ConsSymbolDef" isCharLitTy isStrLitTy $ -- 'a' : "bc" --> "abc" \x y -> Just $ mkStrLitTy (consFS x y) ] where tc = typeConsSymbolTyCon axConsInjectivity :: [BuiltInFamInjectivity] axConsInjectivity = [ -- ConsSymbol a b ~ "blah" => (a ~ 'b') mkTopBinFamDeduction "ConsSymbolT1" tc $ \ a _b r -> do { rs <- isStrLitTy r; (x,_) <- unconsFS rs; return (Pair a (mkCharLitTy x)) } , -- ConsSymbol a b ~ "blah" => (b ~ "lah") mkTopBinFamDeduction "ConsSymbolT2" tc $ \ _a b r -> do { rs <- isStrLitTy r; (_,xs) <- unconsFS rs; return (Pair b (mkStrLitTy xs)) } , mkBinBIF "ConsI-xx" tc ArgX ArgX noGuard -- (x:y1 ~ x:y2) => (y1 ~ y2) , mkBinBIF "ConsI-yy" tc ArgY ArgY noGuard -- (x1:y ~ x2:y) => (x1 ~ x2) ] where tc = typeConsSymbolTyCon ------------------------------------------------------------------------------- -- UnconsSymbol ------------------------------------------------------------------------------- typeUnconsSymbolTyCon :: TyCon typeUnconsSymbolTyCon = mkFamilyTyCon name (mkTemplateAnonTyConBinders [ typeSymbolKind ]) (mkMaybeTy charSymbolPairKind) Nothing (BuiltInSynFamTyCon ops) Nothing (Injective [True]) where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "UnconsSymbol") typeUnconsSymbolTyFamNameKey typeUnconsSymbolTyCon ops = BuiltInSynFamily { sfMatchFam = axUnconsRewrites , sfInteract = axUnconsInjectivity } computeUncons :: FastString -> Type computeUncons str = mkPromotedMaybeTy charSymbolPairKind (fmap reify (unconsFS str)) where reify :: (Char, FastString) -> Type reify (c, s) = charSymbolPair (mkCharLitTy c) (mkStrLitTy s) axUnconsRewrites :: [BuiltInFamRewrite] axUnconsRewrites = [ mkUnaryConstFoldAxiom tc "ConsSymbolDef" isStrLitTy $ -- 'a' : "bc" --> "abc" \x -> Just $ computeUncons x ] where tc = typeUnconsSymbolTyCon axUnconsInjectivity :: [BuiltInFamInjectivity] axUnconsInjectivity = [ -- (UnconsSymbol b ~ Nothing) => (b ~ "") mkTopUnaryFamDeduction "UnconsSymbolT1" tc $ \b r -> do { Nothing <- isPromotedMaybeTy r; return (Pair b nullStrLitTy) } , -- (UnconsSymbol b ~ Just ('f',"oobar")) => (b ~ "foobar") mkTopUnaryFamDeduction "UnconsSymbolT2" tc $ \b r -> do { Just pr <- isPromotedMaybeTy r ; (c,s) <- isPromotedPairType pr ; chr <- isCharLitTy c ; str <- isStrLitTy s ; return (Pair b (mkStrLitTy (consFS chr str))) } , mkUnaryBIF "UnconsI1" tc -- (UnconsSymbol x1 ~ z, UnconsSymbol x2 ~ z) => (x1 ~ x2) ] where tc = typeUnconsSymbolTyCon ------------------------------------------------------------------------------- -- CharToNat ------------------------------------------------------------------------------- typeCharToNatTyCon :: TyCon typeCharToNatTyCon = mkFamilyTyCon name (mkTemplateAnonTyConBinders [ charTy ]) naturalTy Nothing (BuiltInSynFamTyCon ops) Nothing (Injective [True]) where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "CharToNat") typeCharToNatTyFamNameKey typeCharToNatTyCon ops = BuiltInSynFamily { sfMatchFam = axCharToNatRewrites , sfInteract = axCharToNatInjectivity } axCharToNatRewrites :: [BuiltInFamRewrite] axCharToNatRewrites = [ mkUnaryConstFoldAxiom tc "CharToNatDef" isCharLitTy $ -- CharToNat 'a' --> 97 \x -> Just $ num (charToInteger x) ] where tc = typeCharToNatTyCon axCharToNatInjectivity :: [BuiltInFamInjectivity] axCharToNatInjectivity = [ -- (CharToNat c ~ 122) => (c ~ 'z') mkTopUnaryFamDeduction "CharToNatT1" typeCharToNatTyCon $ \c r -> do { nr <- isNumLitTy r; chr <- integerToChar nr; return (Pair c (mkCharLitTy chr)) } ] ------------------------------------------------------------------------------- -- NatToChar ------------------------------------------------------------------------------- typeNatToCharTyCon :: TyCon typeNatToCharTyCon = mkFamilyTyCon name (mkTemplateAnonTyConBinders [ naturalTy ]) charTy Nothing (BuiltInSynFamTyCon ops) Nothing (Injective [True]) where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "NatToChar") typeNatToCharTyFamNameKey typeNatToCharTyCon ops = BuiltInSynFamily { sfMatchFam = axNatToCharRewrites , sfInteract = axNatToCharInjectivity } axNatToCharRewrites :: [BuiltInFamRewrite] axNatToCharRewrites = [ mkUnaryConstFoldAxiom tc "NatToCharDef" isNumLitTy $ -- NatToChar 97 --> 'a' \n -> fmap mkCharLitTy (integerToChar n) ] where tc = typeNatToCharTyCon axNatToCharInjectivity :: [BuiltInFamInjectivity] axNatToCharInjectivity = [ -- (NatToChar n ~ 'z') => (n ~ 122) mkTopUnaryFamDeduction "CharToNatT1" typeNatToCharTyCon $ \n r -> do { c <- isCharLitTy r; return (Pair n (mkNumLitTy (charToInteger c))) } ] ----------------------------------------------------------------------------- -- CmpChar ----------------------------------------------------------------------------- typeCharCmpTyCon :: TyCon typeCharCmpTyCon = mkFamilyTyCon name (mkTemplateAnonTyConBinders [ charTy, charTy ]) orderingKind Nothing (BuiltInSynFamTyCon ops) Nothing NotInjective where name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS_INTERNAL (fsLit "CmpChar") typeCharCmpTyFamNameKey typeCharCmpTyCon ops = BuiltInSynFamily { sfMatchFam = axCharCmpRewrites , sfInteract = axCharCmpInjectivity } sc :: TyVar -- Of kind Char (sc: _) = mkTemplateTyVars (repeat charTy) axCharCmpRewrites :: [BuiltInFamRewrite] axCharCmpRewrites = [ mkRewriteAxiom tc "CmpCharRefl" [sc] [var sc, var sc] (ordering EQ) -- s `cmp` s --> EQ , mkBinConstFoldAxiom tc "CmpCharDef" isCharLitTy isCharLitTy $ -- 'a' `cmp` 'b' --> LT \chr1 chr2 -> Just $ ordering $ compare chr1 chr2 ] where tc = typeCharCmpTyCon axCharCmpInjectivity :: [BuiltInFamInjectivity] axCharCmpInjectivity = [ -- (CmpChar s t ~ EQ) => s ~ t mkTopBinFamDeduction "CmpCharT" typeCharCmpTyCon $ \ s t r -> do { EQ <- isOrderingLitTy r; return (Pair s t) } ] {------------------------------------------------------------------------------- Various utilities for making axioms and types -------------------------------------------------------------------------------} (===) :: Type -> Type -> Pair Type x === y = Pair x y num :: Integer -> Type num = mkNumLitTy var :: TyVar -> Type var = mkTyVarTy (.+.) :: Type -> Type -> Type s .+. t = mkTyConApp typeNatAddTyCon [s,t] {- (.-.) :: Type -> Type -> Type s .-. t = mkTyConApp typeNatSubTyCon [s,t] (.*.) :: Type -> Type -> Type s .*. t = mkTyConApp typeNatMulTyCon [s,t] tDiv :: Type -> Type -> Type tDiv s t = mkTyConApp typeNatDivTyCon [s,t] tMod :: Type -> Type -> Type tMod s t = mkTyConApp typeNatModTyCon [s,t] (.^.) :: Type -> Type -> Type s .^. t = mkTyConApp typeNatExpTyCon [s,t] cmpNat :: Type -> Type -> Type cmpNat s t = mkTyConApp typeNatCmpTyCon [s,t] cmpSymbol :: Type -> Type -> Type cmpSymbol s t = mkTyConApp typeSymbolCmpTyCon [s,t] appendSymbol :: Type -> Type -> Type appendSymbol s t = mkTyConApp typeSymbolAppendTyCon [s, t] -} nullStrLitTy :: Type -- The type "" nullStrLitTy = mkStrLitTy nilFS isStrLitTyS :: Type -> Maybe String isStrLitTyS ty = do { fs <- isStrLitTy ty; return (unpackFS fs) } mkStrLitTyS :: String -> Type mkStrLitTyS s = mkStrLitTy (mkFastString s) charSymbolPair :: Type -> Type -> Type charSymbolPair = mkPromotedPairTy charTy typeSymbolKind charSymbolPairKind :: Kind charSymbolPairKind = mkTyConApp pairTyCon [charTy, typeSymbolKind] orderingKind :: Kind orderingKind = mkTyConApp orderingTyCon [] ordering :: Ordering -> Type ordering o = case o of LT -> mkTyConApp promotedLTDataCon [] EQ -> mkTyConApp promotedEQDataCon [] GT -> mkTyConApp promotedGTDataCon [] isOrderingLitTy :: Type -> Maybe Ordering isOrderingLitTy tc = do (tc1,[]) <- splitTyConApp_maybe tc case () of _ | tc1 == promotedLTDataCon -> return LT | tc1 == promotedEQDataCon -> return EQ | tc1 == promotedGTDataCon -> return GT | otherwise -> Nothing -- Make a unary built-in constructor of kind: Nat -> Nat mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon mkTypeNatFunTyCon1 op tcb = mkFamilyTyCon op (mkTemplateAnonTyConBinders [ naturalTy ]) naturalTy Nothing (BuiltInSynFamTyCon tcb) Nothing NotInjective -- Make a binary built-in constructor of kind: Nat -> Nat -> Nat mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon mkTypeNatFunTyCon2 op tcb = mkFamilyTyCon op (mkTemplateAnonTyConBinders [ naturalTy, naturalTy ]) naturalTy Nothing (BuiltInSynFamTyCon tcb) Nothing NotInjective -- Make a binary built-in constructor of kind: Symbol -> Symbol -> Symbol mkTypeSymbolFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon mkTypeSymbolFunTyCon2 op tcb = mkFamilyTyCon op (mkTemplateAnonTyConBinders [ typeSymbolKind, typeSymbolKind ]) typeSymbolKind Nothing (BuiltInSynFamTyCon tcb) Nothing NotInjective same :: Type -> Type -> Maybe () same ty1 ty2 = guard (ty1 `tcEqType` ty2) known :: Type -> (Integer -> Bool) -> Maybe Integer known x p = do { nx <- isNumLitTy x; guard (p nx); return nx } charToInteger :: Char -> Integer charToInteger c = fromIntegral (Char.ord c) integerToChar :: Integer -> Maybe Char integerToChar n | inBounds = Just (Char.chr (fromInteger n)) where inBounds = n >= charToInteger minBound && n <= charToInteger maxBound integerToChar _ = Nothing {- ----------------------------------------------------------------------------- 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 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)