Repository : ssh://[email protected]/ghc On branch : type-nats-simple Link : http://ghc.haskell.org/trac/ghc/changeset/e742f24c5c0ec19639a7dde10fad3e1cd25535b8/ghc
>--------------------------------------------------------------- commit e742f24c5c0ec19639a7dde10fad3e1cd25535b8 Author: Iavor S. Diatchki <[email protected]> Date: Wed Sep 4 07:41:17 2013 -0700 Move declarations for type-nat TyCons to TcTypeNat >--------------------------------------------------------------- e742f24c5c0ec19639a7dde10fad3e1cd25535b8 compiler/prelude/PrelInfo.lhs | 4 ++ compiler/prelude/TysWiredIn.lhs | 36 ------------------ compiler/typecheck/TcTypeNats.hs | 67 +++++++++++++++++++++++++++++++-- compiler/typecheck/TcTypeNats.hs-boot | 5 +++ 4 files changed, 72 insertions(+), 40 deletions(-) diff --git a/compiler/prelude/PrelInfo.lhs b/compiler/prelude/PrelInfo.lhs index bb3e54a..542525c 100644 --- a/compiler/prelude/PrelInfo.lhs +++ b/compiler/prelude/PrelInfo.lhs @@ -42,6 +42,7 @@ import HscTypes import Class import TyCon import Util +import {-# SOURCE #-} TcTypeNats ( typeNatTyThings ) import Data.Array \end{code} @@ -87,6 +88,9 @@ wiredInThings -- PrimOps , map (AnId . primOpId) allThePrimOps + + -- TyCons and axioms for type-nats + , typeNatTyThings ] where tycon_things = map ATyCon ([funTyCon] ++ primTyCons ++ wiredInTyCons) diff --git a/compiler/prelude/TysWiredIn.lhs b/compiler/prelude/TysWiredIn.lhs index e996617..5ec290a 100644 --- a/compiler/prelude/TysWiredIn.lhs +++ b/compiler/prelude/TysWiredIn.lhs @@ -68,9 +68,6 @@ module TysWiredIn ( -- * Equality predicates eqTyCon_RDR, eqTyCon, eqTyConName, eqBoxDataCon, - -- * Type-level naturals - typeNatAddTyCon, typeNatMulTyCon, typeNatExpTyCon - ) where #include "HsVersions.h" @@ -788,36 +785,3 @@ isPArrFakeCon dcon = dcon == parrFakeCon (dataConSourceArity dcon) - -%******************************************************************* -%* -\subsection[TysWiredIn-TypeNat]{Type-level Numbers} -%* -%******************************************************************* - - -Type functions related to type-nats. - -\begin{code} - --- Make a binary built-in constructor of kind: Nat -> Nat -> Nat -mkTypeNatFunTyCon2 :: Name -> TyCon -mkTypeNatFunTyCon2 op = - mkSynTyCon op - (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind) - (take 2 $ tyVarList typeNatKind) - [Nominal,Nominal] - OpenSynFamilyTyCon -- XXX: BuiltIn - NoParentTyCon - -typeNatAddTyCon :: TyCon -typeNatAddTyCon = mkTypeNatFunTyCon2 typeNatAddTyFamName - -typeNatMulTyCon :: TyCon -typeNatMulTyCon = mkTypeNatFunTyCon2 typeNatMulTyFamName - -typeNatExpTyCon :: TyCon -typeNatExpTyCon = mkTypeNatFunTyCon2 typeNatExpTyFamName - -\end{code} - diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs index e5880b4..a8138f5 100644 --- a/compiler/typecheck/TcTypeNats.hs +++ b/compiler/typecheck/TcTypeNats.hs @@ -1,16 +1,57 @@ -module TcTypeNats (tnMatchFam, tnInteractTop) where +module TcTypeNats (tnMatchFam, tnInteractTop, typeNatTyThings) where import Type import Pair -import TyCon ( TyCon ) +import TyCon ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..) ) +import Coercion ( Role(..) ) import TcRnTypes ( Xi ) import TcEvidence ( mkTcAxiomRuleCo, TcCoercion ) import CoAxiom ( CoAxiomRule(..) ) import Name ( Name, mkWiredInName, BuiltInSyntax(..) ) import OccName ( mkOccName, tcName ) import Unique ( mkAxiomRuleUnique ) -import PrelNames ( gHC_PRIM ) -import TysWiredIn ( typeNatAddTyCon, typeNatMulTyCon, typeNatExpTyCon ) +import TysWiredIn ( typeNatKind ) +import TysPrim ( tyVarList, mkArrowKinds ) +import PrelNames ( gHC_PRIM + , typeNatAddTyFamName + , typeNatMulTyFamName + , typeNatExpTyFamName + ) + +typeNatTyThings :: [TyThing] +typeNatTyThings = typeNatTyCons ++ typeNatAxioms + + +{------------------------------------------------------------------------------- +Built-in type constructors for functions on type-lelve nats +-} + +typeNatTyCons :: [TyThing] +typeNatTyCons = map ATyCon + [ typeNatAddTyCon + , typeNatMulTyCon + , typeNatExpTyCon + ] + +typeNatAddTyCon :: TyCon +typeNatAddTyCon = mkTypeNatFunTyCon2 typeNatAddTyFamName + +typeNatMulTyCon :: TyCon +typeNatMulTyCon = mkTypeNatFunTyCon2 typeNatMulTyFamName + +typeNatExpTyCon :: TyCon +typeNatExpTyCon = mkTypeNatFunTyCon2 typeNatExpTyFamName + +-- Make a binary built-in constructor of kind: Nat -> Nat -> Nat +mkTypeNatFunTyCon2 :: Name -> TyCon +mkTypeNatFunTyCon2 op = + mkSynTyCon op + (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind) + (take 2 $ tyVarList typeNatKind) + [Nominal,Nominal] + OpenSynFamilyTyCon -- XXX: BuiltIn + NoParentTyCon + @@ -73,6 +114,24 @@ axExp1L = mkAxiom1 axExp1LKey "Exp1L" $ \t -> (num 1 .^. t) === num 1 axExp0R = mkAxiom1 axExp0RKey "Exp0R" $ \t -> (t .^. num 0) === num 1 axExp1R = mkAxiom1 axExp1RKey "Exp1R" $ \t -> (t .^. num 1) === t +typeNatAxioms :: [TyThing] +typeNatAxioms = map ACoAxiomRule + [ axAddDef + , axMulDef + , axExpDef + , axAdd0L + , axAdd0R + , axMul0L + , axMul0R + , axMul1L + , axMul1R + , axExp1L + , axExp0R + , axExp1R + ] + + + {------------------------------------------------------------------------------- Various utilities for making axioms and types diff --git a/compiler/typecheck/TcTypeNats.hs-boot b/compiler/typecheck/TcTypeNats.hs-boot new file mode 100644 index 0000000..7bb324b --- /dev/null +++ b/compiler/typecheck/TcTypeNats.hs-boot @@ -0,0 +1,5 @@ +module TcTypeNats where + +import TypeRep(TyThing) + +typeNatTyThings :: [TyThing] _______________________________________________ ghc-commits mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-commits
