Movatterモバイル変換

{-# LANGUAGE Trustworthy #-}{-# LANGUAGE DataKinds #-}{-# LANGUAGE KindSignatures #-}{-# LANGUAGE TypeFamilies #-}{-# LANGUAGE TypeOperators #-}{-# LANGUAGE NoStarIsType #-}{-# LANGUAGE FlexibleInstances #-}{-# LANGUAGE FlexibleContexts #-}{-# LANGUAGE ScopedTypeVariables #-}{-# LANGUAGE ConstraintKinds #-}{-# LANGUAGE ExistentialQuantification #-}{-# LANGUAGE RankNTypes #-}{-# LANGUAGE NoImplicitPrelude #-}{-# LANGUAGE MagicHash #-}{-# LANGUAGE PolyKinds #-}{-| This module is an internal GHC module.  It declares the constants usedin the implementation of type-level natural numbers.  The programmer interfacefor working with type-level naturals should be defined in a separate library.@since 4.10.0.0-}moduleGHC.TypeNats(-- * Nat KindNat-- declared in GHC.Types in package ghc-prim-- * Linking type and value level,KnownNat,natVal,natVal',SomeNat(..),someNatVal,sameNat-- * Functions on type literals,type(<=),type(<=?),type(+),type(*),type(^),type(-),CmpNat,Div,Mod,Log2)whereimportGHC.Base(Eq(..),Ord(..),Bool(True),Ordering(..),otherwise)importGHC.Types(Nat)importGHC.Natural(Natural)importGHC.Show(Show(..))importGHC.Read(Read(..))importGHC.Prim(magicDict,Proxy#)importData.Maybe(Maybe(..))importData.Proxy(Proxy(..))importData.Type.Equality((:~:)(Refl))importUnsafe.Coerce(unsafeCoerce)---------------------------------------------------------------------------------- | This class gives the integer associated with a type-level natural.-- There are instances of the class for every concrete literal: 0, 1, 2, etc.---- @since 4.7.0.0classKnownNat(n::Nat)wherenatSing::SNatn-- | @since 4.10.0.0natVal::forallnproxy.KnownNatn=>proxyn->NaturalnatVal_=casenatSing::SNatnofSNatx->x-- | @since 4.10.0.0natVal'::foralln.KnownNatn=>Proxy#n->NaturalnatVal'_=casenatSing::SNatnofSNatx->x-- | This type represents unknown type-level natural numbers.---- @since 4.10.0.0dataSomeNat=foralln.KnownNatn=>SomeNat(Proxyn)-- | Convert an integer into an unknown type-level natural.---- @since 4.10.0.0someNatVal::Natural->SomeNatsomeNatValn=withSNatSomeNat(SNatn)Proxy-- | @since 4.7.0.0instanceEqSomeNatwhereSomeNatx==SomeNaty=natValx==natValy-- | @since 4.7.0.0instanceOrdSomeNatwherecompare(SomeNatx)(SomeNaty)=compare(natValx)(natValy)-- | @since 4.7.0.0instanceShowSomeNatwhereshowsPrecp(SomeNatx)=showsPrecp(natValx)-- | @since 4.7.0.0instanceReadSomeNatwherereadsPrecpxs=do(a,ys)<-readsPrecpxs[(someNatVala,ys)]--------------------------------------------------------------------------------infix4<=?,<=infixl6+,-infixl7*,`Div`,`Mod`infixr8^-- | Comparison of type-level naturals, as a constraint.---- @since 4.7.0.0typex<=y=(x<=?y)~'True-- | Comparison of type-level naturals, as a function.---- @since 4.7.0.0typefamilyCmpNat(m::Nat)(n::Nat)::Ordering{- | Comparison of type-level naturals, as a function.NOTE: The functionality for this function should be subsumedby 'CmpNat', so this might go away in the future.Please let us know, if you encounter discrepancies between the two. -}typefamily(m::Nat)<=?(n::Nat)::Bool-- | Addition of type-level naturals.---- @since 4.7.0.0typefamily(m::Nat)+(n::Nat)::Nat-- | Multiplication of type-level naturals.---- @since 4.7.0.0typefamily(m::Nat)*(n::Nat)::Nat-- | Exponentiation of type-level naturals.---- @since 4.7.0.0typefamily(m::Nat)^(n::Nat)::Nat-- | Subtraction of type-level naturals.---- @since 4.7.0.0typefamily(m::Nat)-(n::Nat)::Nat-- | Division (round down) of natural numbers.-- @Div x 0@ is undefined (i.e., it cannot be reduced).---- @since 4.11.0.0typefamilyDiv(m::Nat)(n::Nat)::Nat-- | Modulus of natural numbers.-- @Mod x 0@ is undefined (i.e., it cannot be reduced).---- @since 4.11.0.0typefamilyMod(m::Nat)(n::Nat)::Nat-- | Log base 2 (round down) of natural numbers.-- @Log 0@ is undefined (i.e., it cannot be reduced).---- @since 4.11.0.0typefamilyLog2(m::Nat)::Nat---------------------------------------------------------------------------------- | We either get evidence that this function was instantiated with the-- same type-level numbers, or 'Nothing'.---- @since 4.7.0.0sameNat::(KnownNata,KnownNatb)=>Proxya->Proxyb->Maybe(a:~:b)sameNatxy|natValx==natValy=Just(unsafeCoerceRefl)|otherwise=Nothing---------------------------------------------------------------------------------- PRIVATE:newtypeSNat(n::Nat)=SNatNaturaldataWrapNab=WrapN(KnownNata=>Proxya->b)-- See Note [magicDictId magic] in "basicType/MkId.hs"withSNat::(KnownNata=>Proxya->b)->SNata->Proxya->bwithSNatfxy=magicDict(WrapNf)xy