{-# Language Safe, DeriveGeneric, DeriveAnyClass, RecordWildCards #-}
{-# Language FlexibleInstances, FlexibleContexts #-}
{-# Language PatternGuards #-}
{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.Type
( module Cryptol.TypeCheck.Type
, module Cryptol.TypeCheck.TCon
) where
import GHC.Generics (Generic)
import Control.DeepSeq
import Data.Map(Map)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
import Cryptol.Parser.Selector
import Cryptol.Parser.Position(Located,thing,Range,emptyRange)
import Cryptol.Parser.AST(ImpName(..))
import Cryptol.ModuleSystem.Name
import Cryptol.Utils.Ident (Ident, isInfixIdent, exprModName, ogModule, ModName)
import Cryptol.TypeCheck.TCon
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Solver.InfNat
import Cryptol.Utils.Fixity
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.RecordMap
import Prelude
infix 4 =#=, >==
infixr 5 `tFun`
type FunctorParams = Map Ident ModParam
allParamNames :: FunctorParams -> ModParamNames
allParamNames :: FunctorParams -> ModParamNames
allParamNames FunctorParams
mps =
ModParamNames
{ mpnTypes :: Map Name ModTParam
mpnTypes = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions (forall a b. (a -> b) -> [a] -> [b]
map ModParamNames -> Map Name ModTParam
mpnTypes [ModParamNames]
ps)
, mpnConstraints :: [Located Type]
mpnConstraints = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ModParamNames -> [Located Type]
mpnConstraints [ModParamNames]
ps
, mpnFuns :: Map Name ModVParam
mpnFuns = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions (forall a b. (a -> b) -> [a] -> [b]
map ModParamNames -> Map Name ModVParam
mpnFuns [ModParamNames]
ps)
, mpnTySyn :: Map Name TySyn
mpnTySyn = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions (forall a b. (a -> b) -> [a] -> [b]
map ModParamNames -> Map Name TySyn
mpnTySyn [ModParamNames]
ps)
, mpnDoc :: Maybe Text
mpnDoc = forall a. Maybe a
Nothing
}
where
ps :: [ModParamNames]
ps = forall a b. (a -> b) -> [a] -> [b]
map ModParam -> ModParamNames
mpParameters (forall k a. Map k a -> [a]
Map.elems FunctorParams
mps)
data ModParam = ModParam
{ ModParam -> Ident
mpName :: Ident
, ModParam -> Maybe ModName
mpQual :: !(Maybe ModName)
, ModParam -> ImpName Name
mpIface :: ImpName Name
, ModParam -> ModParamNames
mpParameters :: ModParamNames
} deriving (Int -> ModParam -> ShowS
[ModParam] -> ShowS
ModParam -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ModParam] -> ShowS
$cshowList :: [ModParam] -> ShowS
show :: ModParam -> [Char]
$cshow :: ModParam -> [Char]
showsPrec :: Int -> ModParam -> ShowS
$cshowsPrec :: Int -> ModParam -> ShowS
Show, forall x. Rep ModParam x -> ModParam
forall x. ModParam -> Rep ModParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModParam x -> ModParam
$cfrom :: forall x. ModParam -> Rep ModParam x
Generic, ModParam -> ()
forall a. (a -> ()) -> NFData a
rnf :: ModParam -> ()
$crnf :: ModParam -> ()
NFData)
data ModParamNames = ModParamNames
{ ModParamNames -> Map Name ModTParam
mpnTypes :: Map Name ModTParam
, ModParamNames -> Map Name TySyn
mpnTySyn :: !(Map Name TySyn)
, ModParamNames -> [Located Type]
mpnConstraints :: [Located Prop]
, ModParamNames -> Map Name ModVParam
mpnFuns :: Map.Map Name ModVParam
, ModParamNames -> Maybe Text
mpnDoc :: !(Maybe Text)
} deriving (Int -> ModParamNames -> ShowS
[ModParamNames] -> ShowS
ModParamNames -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ModParamNames] -> ShowS
$cshowList :: [ModParamNames] -> ShowS
show :: ModParamNames -> [Char]
$cshow :: ModParamNames -> [Char]
showsPrec :: Int -> ModParamNames -> ShowS
$cshowsPrec :: Int -> ModParamNames -> ShowS
Show, forall x. Rep ModParamNames x -> ModParamNames
forall x. ModParamNames -> Rep ModParamNames x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModParamNames x -> ModParamNames
$cfrom :: forall x. ModParamNames -> Rep ModParamNames x
Generic, ModParamNames -> ()
forall a. (a -> ()) -> NFData a
rnf :: ModParamNames -> ()
$crnf :: ModParamNames -> ()
NFData)
data ModTParam = ModTParam
{ ModTParam -> Name
mtpName :: Name
, ModTParam -> Kind
mtpKind :: Kind
, ModTParam -> Maybe Text
mtpDoc :: Maybe Text
} deriving (Int -> ModTParam -> ShowS
[ModTParam] -> ShowS
ModTParam -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ModTParam] -> ShowS
$cshowList :: [ModTParam] -> ShowS
show :: ModTParam -> [Char]
$cshow :: ModTParam -> [Char]
showsPrec :: Int -> ModTParam -> ShowS
$cshowsPrec :: Int -> ModTParam -> ShowS
Show,forall x. Rep ModTParam x -> ModTParam
forall x. ModTParam -> Rep ModTParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModTParam x -> ModTParam
$cfrom :: forall x. ModTParam -> Rep ModTParam x
Generic,ModTParam -> ()
forall a. (a -> ()) -> NFData a
rnf :: ModTParam -> ()
$crnf :: ModTParam -> ()
NFData)
mtpParam :: ModTParam -> TParam
mtpParam :: ModTParam -> TParam
mtpParam ModTParam
mtp = TParam { tpUnique :: Int
tpUnique = Name -> Int
nameUnique (ModTParam -> Name
mtpName ModTParam
mtp)
, tpKind :: Kind
tpKind = ModTParam -> Kind
mtpKind ModTParam
mtp
, tpFlav :: TPFlavor
tpFlav = Name -> TPFlavor
TPModParam (ModTParam -> Name
mtpName ModTParam
mtp)
, tpInfo :: TVarInfo
tpInfo = TVarInfo
desc
}
where desc :: TVarInfo
desc = TVarInfo { tvarDesc :: TypeSource
tvarDesc = Name -> TypeSource
TVFromModParam (ModTParam -> Name
mtpName ModTParam
mtp)
, tvarSource :: Range
tvarSource = Name -> Range
nameLoc (ModTParam -> Name
mtpName ModTParam
mtp)
}
data ModVParam = ModVParam
{ ModVParam -> Name
mvpName :: Name
, ModVParam -> Schema
mvpType :: Schema
, ModVParam -> Maybe Text
mvpDoc :: Maybe Text
, ModVParam -> Maybe Fixity
mvpFixity :: Maybe Fixity
} deriving (Int -> ModVParam -> ShowS
[ModVParam] -> ShowS
ModVParam -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ModVParam] -> ShowS
$cshowList :: [ModVParam] -> ShowS
show :: ModVParam -> [Char]
$cshow :: ModVParam -> [Char]
showsPrec :: Int -> ModVParam -> ShowS
$cshowsPrec :: Int -> ModVParam -> ShowS
Show,forall x. Rep ModVParam x -> ModVParam
forall x. ModVParam -> Rep ModVParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModVParam x -> ModVParam
$cfrom :: forall x. ModVParam -> Rep ModVParam x
Generic,ModVParam -> ()
forall a. (a -> ()) -> NFData a
rnf :: ModVParam -> ()
$crnf :: ModVParam -> ()
NFData)
data Schema = Forall { Schema -> [TParam]
sVars :: [TParam], Schema -> [Type]
sProps :: [Prop], Schema -> Type
sType :: Type }
deriving (Schema -> Schema -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Schema -> Schema -> Bool
$c/= :: Schema -> Schema -> Bool
== :: Schema -> Schema -> Bool
$c== :: Schema -> Schema -> Bool
Eq, Int -> Schema -> ShowS
[Schema] -> ShowS
Schema -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Schema] -> ShowS
$cshowList :: [Schema] -> ShowS
show :: Schema -> [Char]
$cshow :: Schema -> [Char]
showsPrec :: Int -> Schema -> ShowS
$cshowsPrec :: Int -> Schema -> ShowS
Show, forall x. Rep Schema x -> Schema
forall x. Schema -> Rep Schema x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Schema x -> Schema
$cfrom :: forall x. Schema -> Rep Schema x
Generic, Schema -> ()
forall a. (a -> ()) -> NFData a
rnf :: Schema -> ()
$crnf :: Schema -> ()
NFData)
data TParam = TParam { TParam -> Int
tpUnique :: !Int
, TParam -> Kind
tpKind :: Kind
, TParam -> TPFlavor
tpFlav :: TPFlavor
, TParam -> TVarInfo
tpInfo :: !TVarInfo
}
deriving (forall x. Rep TParam x -> TParam
forall x. TParam -> Rep TParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TParam x -> TParam
$cfrom :: forall x. TParam -> Rep TParam x
Generic, TParam -> ()
forall a. (a -> ()) -> NFData a
rnf :: TParam -> ()
$crnf :: TParam -> ()
NFData, Int -> TParam -> ShowS
[TParam] -> ShowS
TParam -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TParam] -> ShowS
$cshowList :: [TParam] -> ShowS
show :: TParam -> [Char]
$cshow :: TParam -> [Char]
showsPrec :: Int -> TParam -> ShowS
$cshowsPrec :: Int -> TParam -> ShowS
Show)
data TPFlavor = TPModParam Name
| TPUnifyVar
| TPSchemaParam Name
| TPTySynParam Name
| TPPropSynParam Name
| TPNewtypeParam Name
| TPPrimParam Name
deriving (forall x. Rep TPFlavor x -> TPFlavor
forall x. TPFlavor -> Rep TPFlavor x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TPFlavor x -> TPFlavor
$cfrom :: forall x. TPFlavor -> Rep TPFlavor x
Generic, TPFlavor -> ()
forall a. (a -> ()) -> NFData a
rnf :: TPFlavor -> ()
$crnf :: TPFlavor -> ()
NFData, Int -> TPFlavor -> ShowS
[TPFlavor] -> ShowS
TPFlavor -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TPFlavor] -> ShowS
$cshowList :: [TPFlavor] -> ShowS
show :: TPFlavor -> [Char]
$cshow :: TPFlavor -> [Char]
showsPrec :: Int -> TPFlavor -> ShowS
$cshowsPrec :: Int -> TPFlavor -> ShowS
Show)
tMono :: Type -> Schema
tMono :: Type -> Schema
tMono = [TParam] -> [Type] -> Type -> Schema
Forall [] []
isMono :: Schema -> Maybe Type
isMono :: Schema -> Maybe Type
isMono Schema
s =
case Schema
s of
Forall [] [] Type
t -> forall a. a -> Maybe a
Just Type
t
Schema
_ -> forall a. Maybe a
Nothing
schemaParam :: Name -> TPFlavor
schemaParam :: Name -> TPFlavor
schemaParam = Name -> TPFlavor
TPSchemaParam
tySynParam :: Name -> TPFlavor
tySynParam :: Name -> TPFlavor
tySynParam = Name -> TPFlavor
TPTySynParam
propSynParam :: Name -> TPFlavor
propSynParam :: Name -> TPFlavor
propSynParam = Name -> TPFlavor
TPPropSynParam
newtypeParam :: Name -> TPFlavor
newtypeParam :: Name -> TPFlavor
newtypeParam = Name -> TPFlavor
TPNewtypeParam
modTyParam :: Name -> TPFlavor
modTyParam :: Name -> TPFlavor
modTyParam = Name -> TPFlavor
TPModParam
tpfName :: TPFlavor -> Maybe Name
tpfName :: TPFlavor -> Maybe Name
tpfName TPFlavor
f =
case TPFlavor
f of
TPFlavor
TPUnifyVar -> forall a. Maybe a
Nothing
TPModParam Name
x -> forall a. a -> Maybe a
Just Name
x
TPSchemaParam Name
x -> forall a. a -> Maybe a
Just Name
x
TPTySynParam Name
x -> forall a. a -> Maybe a
Just Name
x
TPPropSynParam Name
x -> forall a. a -> Maybe a
Just Name
x
TPNewtypeParam Name
x -> forall a. a -> Maybe a
Just Name
x
TPPrimParam Name
x -> forall a. a -> Maybe a
Just Name
x
tpName :: TParam -> Maybe Name
tpName :: TParam -> Maybe Name
tpName = TPFlavor -> Maybe Name
tpfName forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TPFlavor
tpFlav
data Type = TCon !TCon ![Type]
| TVar TVar
| TUser !Name ![Type] !Type
| TRec !(RecordMap Ident Type)
| TNewtype !Newtype ![Type]
deriving (Int -> Type -> ShowS
[Type] -> ShowS
Type -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> [Char]
$cshow :: Type -> [Char]
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show, forall x. Rep Type x -> Type
forall x. Type -> Rep Type x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Type x -> Type
$cfrom :: forall x. Type -> Rep Type x
Generic, Type -> ()
forall a. (a -> ()) -> NFData a
rnf :: Type -> ()
$crnf :: Type -> ()
NFData)
data TVar = TVFree !Int Kind (Set TParam) TVarInfo
| TVBound {-# UNPACK #-} !TParam
deriving (Int -> TVar -> ShowS
[TVar] -> ShowS
TVar -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TVar] -> ShowS
$cshowList :: [TVar] -> ShowS
show :: TVar -> [Char]
$cshow :: TVar -> [Char]
showsPrec :: Int -> TVar -> ShowS
$cshowsPrec :: Int -> TVar -> ShowS
Show, forall x. Rep TVar x -> TVar
forall x. TVar -> Rep TVar x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TVar x -> TVar
$cfrom :: forall x. TVar -> Rep TVar x
Generic, TVar -> ()
forall a. (a -> ()) -> NFData a
rnf :: TVar -> ()
$crnf :: TVar -> ()
NFData)
tvInfo :: TVar -> TVarInfo
tvInfo :: TVar -> TVarInfo
tvInfo TVar
tv =
case TVar
tv of
TVFree Int
_ Kind
_ Set TParam
_ TVarInfo
d -> TVarInfo
d
TVBound TParam
tp -> TParam -> TVarInfo
tpInfo TParam
tp
tvUnique :: TVar -> Int
tvUnique :: TVar -> Int
tvUnique (TVFree Int
u Kind
_ Set TParam
_ TVarInfo
_) = Int
u
tvUnique (TVBound TParam { tpUnique :: TParam -> Int
tpUnique = Int
u }) = Int
u
data TVarInfo = TVarInfo { TVarInfo -> Range
tvarSource :: !Range
, TVarInfo -> TypeSource
tvarDesc :: !TypeSource
}
deriving (Int -> TVarInfo -> ShowS
[TVarInfo] -> ShowS
TVarInfo -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TVarInfo] -> ShowS
$cshowList :: [TVarInfo] -> ShowS
show :: TVarInfo -> [Char]
$cshow :: TVarInfo -> [Char]
showsPrec :: Int -> TVarInfo -> ShowS
$cshowsPrec :: Int -> TVarInfo -> ShowS
Show, forall x. Rep TVarInfo x -> TVarInfo
forall x. TVarInfo -> Rep TVarInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TVarInfo x -> TVarInfo
$cfrom :: forall x. TVarInfo -> Rep TVarInfo x
Generic, TVarInfo -> ()
forall a. (a -> ()) -> NFData a
rnf :: TVarInfo -> ()
$crnf :: TVarInfo -> ()
NFData)
data TypeSource = TVFromModParam Name
| TVFromSignature Name
| TypeWildCard
| TypeOfRecordField Ident
| TypeOfTupleField Int
| TypeOfSeqElement
| LenOfSeq
| TypeParamInstNamed Name Ident
| TypeParamInstPos Name Int
| DefinitionOf Name
| LenOfCompGen
| TypeOfArg ArgDescr
| TypeOfRes
| FunApp
| TypeOfIfCondExpr
| TypeFromUserAnnotation
| GeneratorOfListComp
| TypeErrorPlaceHolder
deriving (Int -> TypeSource -> ShowS
[TypeSource] -> ShowS
TypeSource -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TypeSource] -> ShowS
$cshowList :: [TypeSource] -> ShowS
show :: TypeSource -> [Char]
$cshow :: TypeSource -> [Char]
showsPrec :: Int -> TypeSource -> ShowS
$cshowsPrec :: Int -> TypeSource -> ShowS
Show, forall x. Rep TypeSource x -> TypeSource
forall x. TypeSource -> Rep TypeSource x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TypeSource x -> TypeSource
$cfrom :: forall x. TypeSource -> Rep TypeSource x
Generic, TypeSource -> ()
forall a. (a -> ()) -> NFData a
rnf :: TypeSource -> ()
$crnf :: TypeSource -> ()
NFData)
data ArgDescr = ArgDescr
{ ArgDescr -> Maybe Name
argDescrFun :: Maybe Name
, ArgDescr -> Maybe Int
argDescrNumber :: Maybe Int
}
deriving (Int -> ArgDescr -> ShowS
[ArgDescr] -> ShowS
ArgDescr -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ArgDescr] -> ShowS
$cshowList :: [ArgDescr] -> ShowS
show :: ArgDescr -> [Char]
$cshow :: ArgDescr -> [Char]
showsPrec :: Int -> ArgDescr -> ShowS
$cshowsPrec :: Int -> ArgDescr -> ShowS
Show,forall x. Rep ArgDescr x -> ArgDescr
forall x. ArgDescr -> Rep ArgDescr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ArgDescr x -> ArgDescr
$cfrom :: forall x. ArgDescr -> Rep ArgDescr x
Generic,ArgDescr -> ()
forall a. (a -> ()) -> NFData a
rnf :: ArgDescr -> ()
$crnf :: ArgDescr -> ()
NFData)
noArgDescr :: ArgDescr
noArgDescr :: ArgDescr
noArgDescr = ArgDescr { argDescrFun :: Maybe Name
argDescrFun = forall a. Maybe a
Nothing, argDescrNumber :: Maybe Int
argDescrNumber = forall a. Maybe a
Nothing }
tvSourceName :: TypeSource -> Maybe Name
tvSourceName :: TypeSource -> Maybe Name
tvSourceName TypeSource
tvs =
case TypeSource
tvs of
TVFromModParam Name
x -> forall a. a -> Maybe a
Just Name
x
TVFromSignature Name
x -> forall a. a -> Maybe a
Just Name
x
TypeParamInstNamed Name
x Ident
_ -> forall a. a -> Maybe a
Just Name
x
TypeParamInstPos Name
x Int
_ -> forall a. a -> Maybe a
Just Name
x
DefinitionOf Name
x -> forall a. a -> Maybe a
Just Name
x
TypeOfArg ArgDescr
x -> ArgDescr -> Maybe Name
argDescrFun ArgDescr
x
TypeSource
_ -> forall a. Maybe a
Nothing
data TypeWithSource = WithSource
{ TypeWithSource -> Type
twsType :: Type
, TypeWithSource -> TypeSource
twsSource :: TypeSource
, TypeWithSource -> Maybe Range
twsRange :: !(Maybe Range)
}
type Prop = Type
data TySyn = TySyn { TySyn -> Name
tsName :: Name
, TySyn -> [TParam]
tsParams :: [TParam]
, TySyn -> [Type]
tsConstraints :: [Prop]
, TySyn -> Type
tsDef :: Type
, TySyn -> Maybe Text
tsDoc :: !(Maybe Text)
}
deriving (Int -> TySyn -> ShowS
[TySyn] -> ShowS
TySyn -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TySyn] -> ShowS
$cshowList :: [TySyn] -> ShowS
show :: TySyn -> [Char]
$cshow :: TySyn -> [Char]
showsPrec :: Int -> TySyn -> ShowS
$cshowsPrec :: Int -> TySyn -> ShowS
Show, forall x. Rep TySyn x -> TySyn
forall x. TySyn -> Rep TySyn x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TySyn x -> TySyn
$cfrom :: forall x. TySyn -> Rep TySyn x
Generic, TySyn -> ()
forall a. (a -> ()) -> NFData a
rnf :: TySyn -> ()
$crnf :: TySyn -> ()
NFData)
data Newtype = Newtype { Newtype -> Name
ntName :: Name
, Newtype -> [TParam]
ntParams :: [TParam]
, Newtype -> [Type]
ntConstraints :: [Prop]
, Newtype -> Name
ntConName :: !Name
, Newtype -> RecordMap Ident Type
ntFields :: RecordMap Ident Type
, Newtype -> Maybe Text
ntDoc :: Maybe Text
} deriving (Int -> Newtype -> ShowS
[Newtype] -> ShowS
Newtype -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Newtype] -> ShowS
$cshowList :: [Newtype] -> ShowS
show :: Newtype -> [Char]
$cshow :: Newtype -> [Char]
showsPrec :: Int -> Newtype -> ShowS
$cshowsPrec :: Int -> Newtype -> ShowS
Show, forall x. Rep Newtype x -> Newtype
forall x. Newtype -> Rep Newtype x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Newtype x -> Newtype
$cfrom :: forall x. Newtype -> Rep Newtype x
Generic, Newtype -> ()
forall a. (a -> ()) -> NFData a
rnf :: Newtype -> ()
$crnf :: Newtype -> ()
NFData)
instance Eq Newtype where
Newtype
x == :: Newtype -> Newtype -> Bool
== Newtype
y = Newtype -> Name
ntName Newtype
x forall a. Eq a => a -> a -> Bool
== Newtype -> Name
ntName Newtype
y
instance Ord Newtype where
compare :: Newtype -> Newtype -> Ordering
compare Newtype
x Newtype
y = forall a. Ord a => a -> a -> Ordering
compare (Newtype -> Name
ntName Newtype
x) (Newtype -> Name
ntName Newtype
y)
data AbstractType = AbstractType
{ AbstractType -> Name
atName :: Name
, AbstractType -> Kind
atKind :: Kind
, AbstractType -> ([TParam], [Type])
atCtrs :: ([TParam], [Prop])
, AbstractType -> Maybe Fixity
atFixitiy :: Maybe Fixity
, AbstractType -> Maybe Text
atDoc :: Maybe Text
} deriving (Int -> AbstractType -> ShowS
[AbstractType] -> ShowS
AbstractType -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [AbstractType] -> ShowS
$cshowList :: [AbstractType] -> ShowS
show :: AbstractType -> [Char]
$cshow :: AbstractType -> [Char]
showsPrec :: Int -> AbstractType -> ShowS
$cshowsPrec :: Int -> AbstractType -> ShowS
Show, forall x. Rep AbstractType x -> AbstractType
forall x. AbstractType -> Rep AbstractType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep AbstractType x -> AbstractType
$cfrom :: forall x. AbstractType -> Rep AbstractType x
Generic, AbstractType -> ()
forall a. (a -> ()) -> NFData a
rnf :: AbstractType -> ()
$crnf :: AbstractType -> ()
NFData)
instance HasKind AbstractType where
kindOf :: AbstractType -> Kind
kindOf AbstractType
at = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) (AbstractType -> Kind
atKind AbstractType
at) (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasKind t => t -> Kind
kindOf (forall a b. (a, b) -> a
fst (AbstractType -> ([TParam], [Type])
atCtrs AbstractType
at)))
instance HasKind TVar where
kindOf :: TVar -> Kind
kindOf (TVFree Int
_ Kind
k Set TParam
_ TVarInfo
_) = Kind
k
kindOf (TVBound TParam
tp) = forall t. HasKind t => t -> Kind
kindOf TParam
tp
instance HasKind Type where
kindOf :: Type -> Kind
kindOf Type
ty =
case Type
ty of
TVar TVar
a -> forall t. HasKind t => t -> Kind
kindOf TVar
a
TCon TCon
c [Type]
ts -> forall a. Kind -> [a] -> Kind
quickApply (forall t. HasKind t => t -> Kind
kindOf TCon
c) [Type]
ts
TUser Name
_ [Type]
_ Type
t -> forall t. HasKind t => t -> Kind
kindOf Type
t
TRec {} -> Kind
KType
TNewtype{} -> Kind
KType
instance HasKind TySyn where
kindOf :: TySyn -> Kind
kindOf TySyn
ts = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) (forall t. HasKind t => t -> Kind
kindOf (TySyn -> Type
tsDef TySyn
ts)) (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasKind t => t -> Kind
kindOf (TySyn -> [TParam]
tsParams TySyn
ts))
instance HasKind Newtype where
kindOf :: Newtype -> Kind
kindOf Newtype
nt = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) Kind
KType (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasKind t => t -> Kind
kindOf (Newtype -> [TParam]
ntParams Newtype
nt))
instance HasKind TParam where
kindOf :: TParam -> Kind
kindOf TParam
p = TParam -> Kind
tpKind TParam
p
quickApply :: Kind -> [a] -> Kind
quickApply :: forall a. Kind -> [a] -> Kind
quickApply Kind
k [] = Kind
k
quickApply (Kind
_ :-> Kind
k) (a
_ : [a]
ts) = forall a. Kind -> [a] -> Kind
quickApply Kind
k [a]
ts
quickApply Kind
k [a]
_ = forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"Cryptol.TypeCheck.AST.quickApply"
[ [Char]
"Applying a non-function kind:", forall a. Show a => a -> [Char]
show Kind
k ]
kindResult :: Kind -> Kind
kindResult :: Kind -> Kind
kindResult (Kind
_ :-> Kind
k) = Kind -> Kind
kindResult Kind
k
kindResult Kind
k = Kind
k
instance Eq Type where
TUser Name
_ [Type]
_ Type
x == :: Type -> Type -> Bool
== Type
y = Type
x forall a. Eq a => a -> a -> Bool
== Type
y
Type
x == TUser Name
_ [Type]
_ Type
y = Type
y forall a. Eq a => a -> a -> Bool
== Type
x
TCon TCon
x [Type]
xs == TCon TCon
y [Type]
ys = TCon
x forall a. Eq a => a -> a -> Bool
== TCon
y Bool -> Bool -> Bool
&& [Type]
xs forall a. Eq a => a -> a -> Bool
== [Type]
ys
TVar TVar
x == TVar TVar
y = TVar
x forall a. Eq a => a -> a -> Bool
== TVar
y
TRec RecordMap Ident Type
xs == TRec RecordMap Ident Type
ys = RecordMap Ident Type
xs forall a. Eq a => a -> a -> Bool
== RecordMap Ident Type
ys
TNewtype Newtype
ntx [Type]
xs == TNewtype Newtype
nty [Type]
ys = Newtype
ntx forall a. Eq a => a -> a -> Bool
== Newtype
nty Bool -> Bool -> Bool
&& [Type]
xs forall a. Eq a => a -> a -> Bool
== [Type]
ys
Type
_ == Type
_ = Bool
False
instance Ord Type where
compare :: Type -> Type -> Ordering
compare Type
x0 Type
y0 =
case (Type
x0,Type
y0) of
(TUser Name
_ [Type]
_ Type
t, Type
_) -> forall a. Ord a => a -> a -> Ordering
compare Type
t Type
y0
(Type
_, TUser Name
_ [Type]
_ Type
t) -> forall a. Ord a => a -> a -> Ordering
compare Type
x0 Type
t
(TVar TVar
x, TVar TVar
y) -> forall a. Ord a => a -> a -> Ordering
compare TVar
x TVar
y
(TVar {}, Type
_) -> Ordering
LT
(Type
_, TVar {}) -> Ordering
GT
(TCon TCon
x [Type]
xs, TCon TCon
y [Type]
ys) -> forall a. Ord a => a -> a -> Ordering
compare (TCon
x,[Type]
xs) (TCon
y,[Type]
ys)
(TCon {}, Type
_) -> Ordering
LT
(Type
_,TCon {}) -> Ordering
GT
(TRec RecordMap Ident Type
xs, TRec RecordMap Ident Type
ys) -> forall a. Ord a => a -> a -> Ordering
compare RecordMap Ident Type
xs RecordMap Ident Type
ys
(TRec{}, Type
_) -> Ordering
LT
(Type
_, TRec{}) -> Ordering
GT
(TNewtype Newtype
x [Type]
xs, TNewtype Newtype
y [Type]
ys) -> forall a. Ord a => a -> a -> Ordering
compare (Newtype
x,[Type]
xs) (Newtype
y,[Type]
ys)
instance Eq TParam where
TParam
x == :: TParam -> TParam -> Bool
== TParam
y = TParam -> Int
tpUnique TParam
x forall a. Eq a => a -> a -> Bool
== TParam -> Int
tpUnique TParam
y
instance Ord TParam where
compare :: TParam -> TParam -> Ordering
compare TParam
x TParam
y = forall a. Ord a => a -> a -> Ordering
compare (TParam -> Int
tpUnique TParam
x) (TParam -> Int
tpUnique TParam
y)
tpVar :: TParam -> TVar
tpVar :: TParam -> TVar
tpVar TParam
p = TParam -> TVar
TVBound TParam
p
type SType = Type
superclassSet :: Prop -> Set Prop
superclassSet :: Type -> Set Type
superclassSet (TCon (PC PC
PPrime) [Type
n]) =
forall a. Ord a => [a] -> Set a
Set.fromList [ Type -> Type
pFin Type
n, Type
n Type -> Type -> Type
>== Type
tTwo ]
superclassSet (TCon (PC PC
p0) [Type
t]) = PC -> Set Type
go PC
p0
where
super :: PC -> Set Type
super PC
p = forall a. Ord a => a -> Set a -> Set a
Set.insert (TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
p) [Type
t]) (PC -> Set Type
go PC
p)
go :: PC -> Set Type
go PC
PRing = PC -> Set Type
super PC
PZero
go PC
PLogic = PC -> Set Type
super PC
PZero
go PC
PField = PC -> Set Type
super PC
PRing
go PC
PIntegral = PC -> Set Type
super PC
PRing
go PC
PRound = PC -> Set Type
super PC
PField forall a. Semigroup a => a -> a -> a
<> PC -> Set Type
super PC
PCmp
go PC
PCmp = PC -> Set Type
super PC
PEq
go PC
PSignedCmp = PC -> Set Type
super PC
PEq
go PC
_ = forall a. Monoid a => a
mempty
superclassSet Type
_ = forall a. Monoid a => a
mempty
newtypeConType :: Newtype -> Schema
newtypeConType :: Newtype -> Schema
newtypeConType Newtype
nt =
[TParam] -> [Type] -> Type -> Schema
Forall [TParam]
as (Newtype -> [Type]
ntConstraints Newtype
nt)
forall a b. (a -> b) -> a -> b
$ RecordMap Ident Type -> Type
TRec (Newtype -> RecordMap Ident Type
ntFields Newtype
nt) Type -> Type -> Type
`tFun` Newtype -> [Type] -> Type
TNewtype Newtype
nt (forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Type
TVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
tpVar) [TParam]
as)
where
as :: [TParam]
as = Newtype -> [TParam]
ntParams Newtype
nt
abstractTypeTC :: AbstractType -> TCon
abstractTypeTC :: AbstractType -> TCon
abstractTypeTC AbstractType
at =
case Name -> Maybe TCon
builtInType (AbstractType -> Name
atName AbstractType
at) of
Just TCon
tcon
| forall t. HasKind t => t -> Kind
kindOf TCon
tcon forall a. Eq a => a -> a -> Bool
== AbstractType -> Kind
atKind AbstractType
at -> TCon
tcon
| Bool
otherwise ->
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"abstractTypeTC"
[ [Char]
"Mismatch between built-in and declared type."
, [Char]
"Name: " forall a. [a] -> [a] -> [a]
++ forall a. PP a => a -> [Char]
pretty (AbstractType -> Name
atName AbstractType
at)
, [Char]
"Declared: " forall a. [a] -> [a] -> [a]
++ forall a. PP a => a -> [Char]
pretty (AbstractType -> Kind
atKind AbstractType
at)
, [Char]
"Built-in: " forall a. [a] -> [a] -> [a]
++ forall a. PP a => a -> [Char]
pretty (forall t. HasKind t => t -> Kind
kindOf TCon
tcon)
]
Maybe TCon
_ -> TC -> TCon
TC forall a b. (a -> b) -> a -> b
$ UserTC -> TC
TCAbstract forall a b. (a -> b) -> a -> b
$ Name -> Kind -> UserTC
UserTC (AbstractType -> Name
atName AbstractType
at) (AbstractType -> Kind
atKind AbstractType
at)
instance Eq TVar where
TVBound TParam
x == :: TVar -> TVar -> Bool
== TVBound TParam
y = TParam
x forall a. Eq a => a -> a -> Bool
== TParam
y
TVFree Int
x Kind
_ Set TParam
_ TVarInfo
_ == TVFree Int
y Kind
_ Set TParam
_ TVarInfo
_ = Int
x forall a. Eq a => a -> a -> Bool
== Int
y
TVar
_ == TVar
_ = Bool
False
instance Ord TVar where
compare :: TVar -> TVar -> Ordering
compare (TVFree Int
x Kind
_ Set TParam
_ TVarInfo
_) (TVFree Int
y Kind
_ Set TParam
_ TVarInfo
_) = forall a. Ord a => a -> a -> Ordering
compare Int
x Int
y
compare (TVFree Int
_ Kind
_ Set TParam
_ TVarInfo
_) TVar
_ = Ordering
LT
compare TVar
_ (TVFree Int
_ Kind
_ Set TParam
_ TVarInfo
_) = Ordering
GT
compare (TVBound TParam
x) (TVBound TParam
y) = forall a. Ord a => a -> a -> Ordering
compare TParam
x TParam
y
isFreeTV :: TVar -> Bool
isFreeTV :: TVar -> Bool
isFreeTV (TVFree {}) = Bool
True
isFreeTV TVar
_ = Bool
False
isBoundTV :: TVar -> Bool
isBoundTV :: TVar -> Bool
isBoundTV (TVBound {}) = Bool
True
isBoundTV TVar
_ = Bool
False
tIsError :: Type -> Maybe Type
tIsError :: Type -> Maybe Type
tIsError Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (TError Kind
_) [Type
t] -> forall a. a -> Maybe a
Just Type
t
TCon (TError Kind
_) [Type]
_ -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"tIsError" [[Char]
"Malformed error"]
Type
_ -> forall a. Maybe a
Nothing
tHasErrors :: Type -> Bool
tHasErrors :: Type -> Bool
tHasErrors Type
ty =
case Type -> Type
tNoUser Type
ty of
TCon (TError Kind
_) [Type]
_ -> Bool
True
TCon TCon
_ [Type]
ts -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
tHasErrors [Type]
ts
TRec RecordMap Ident Type
mp -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
tHasErrors RecordMap Ident Type
mp
Type
_ -> Bool
False
tIsNat' :: Type -> Maybe Nat'
tIsNat' :: Type -> Maybe Nat'
tIsNat' Type
ty =
case Type -> Type
tNoUser Type
ty of
TCon (TC (TCNum Integer
x)) [] -> forall a. a -> Maybe a
Just (Integer -> Nat'
Nat Integer
x)
TCon (TC TC
TCInf) [] -> forall a. a -> Maybe a
Just Nat'
Inf
Type
_ -> forall a. Maybe a
Nothing
tIsNum :: Type -> Maybe Integer
tIsNum :: Type -> Maybe Integer
tIsNum Type
ty = do Nat Integer
x <- Type -> Maybe Nat'
tIsNat' Type
ty
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x
tIsInf :: Type -> Bool
tIsInf :: Type -> Bool
tIsInf Type
ty = Type -> Maybe Nat'
tIsNat' Type
ty forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Nat'
Inf
tIsVar :: Type -> Maybe TVar
tIsVar :: Type -> Maybe TVar
tIsVar Type
ty = case Type -> Type
tNoUser Type
ty of
TVar TVar
x -> forall a. a -> Maybe a
Just TVar
x
Type
_ -> forall a. Maybe a
Nothing
tIsFun :: Type -> Maybe (Type, Type)
tIsFun :: Type -> Maybe (Type, Type)
tIsFun Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (TC TC
TCFun) [Type
a, Type
b] -> forall a. a -> Maybe a
Just (Type
a, Type
b)
Type
_ -> forall a. Maybe a
Nothing
tIsSeq :: Type -> Maybe (Type, Type)
tIsSeq :: Type -> Maybe (Type, Type)
tIsSeq Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (TC TC
TCSeq) [Type
n, Type
a] -> forall a. a -> Maybe a
Just (Type
n, Type
a)
Type
_ -> forall a. Maybe a
Nothing
tIsBit :: Type -> Bool
tIsBit :: Type -> Bool
tIsBit Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (TC TC
TCBit) [] -> Bool
True
Type
_ -> Bool
False
tIsInteger :: Type -> Bool
tIsInteger :: Type -> Bool
tIsInteger Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (TC TC
TCInteger) [] -> Bool
True
Type
_ -> Bool
False
tIsIntMod :: Type -> Maybe Type
tIsIntMod :: Type -> Maybe Type
tIsIntMod Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (TC TC
TCIntMod) [Type
n] -> forall a. a -> Maybe a
Just Type
n
Type
_ -> forall a. Maybe a
Nothing
tIsRational :: Type -> Bool
tIsRational :: Type -> Bool
tIsRational Type
ty =
case Type -> Type
tNoUser Type
ty of
TCon (TC TC
TCRational) [] -> Bool
True
Type
_ -> Bool
False
tIsFloat :: Type -> Maybe (Type, Type)
tIsFloat :: Type -> Maybe (Type, Type)
tIsFloat Type
ty =
case Type -> Type
tNoUser Type
ty of
TCon (TC TC
TCFloat) [Type
e, Type
p] -> forall a. a -> Maybe a
Just (Type
e, Type
p)
Type
_ -> forall a. Maybe a
Nothing
tIsTuple :: Type -> Maybe [Type]
tIsTuple :: Type -> Maybe [Type]
tIsTuple Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (TC (TCTuple Int
_)) [Type]
ts -> forall a. a -> Maybe a
Just [Type]
ts
Type
_ -> forall a. Maybe a
Nothing
tIsRec :: Type -> Maybe (RecordMap Ident Type)
tIsRec :: Type -> Maybe (RecordMap Ident Type)
tIsRec Type
ty = case Type -> Type
tNoUser Type
ty of
TRec RecordMap Ident Type
fs -> forall a. a -> Maybe a
Just RecordMap Ident Type
fs
Type
_ -> forall a. Maybe a
Nothing
tIsBinFun :: TFun -> Type -> Maybe (Type,Type)
tIsBinFun :: TFun -> Type -> Maybe (Type, Type)
tIsBinFun TFun
f Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (TF TFun
g) [Type
a,Type
b] | TFun
f forall a. Eq a => a -> a -> Bool
== TFun
g -> forall a. a -> Maybe a
Just (Type
a,Type
b)
Type
_ -> forall a. Maybe a
Nothing
tSplitFun :: TFun -> Type -> [Type]
tSplitFun :: TFun -> Type -> [Type]
tSplitFun TFun
f Type
t0 = Type -> [Type] -> [Type]
go Type
t0 []
where go :: Type -> [Type] -> [Type]
go Type
ty [Type]
xs = case TFun -> Type -> Maybe (Type, Type)
tIsBinFun TFun
f Type
ty of
Just (Type
a,Type
b) -> Type -> [Type] -> [Type]
go Type
a (Type -> [Type] -> [Type]
go Type
b [Type]
xs)
Maybe (Type, Type)
Nothing -> Type
ty forall a. a -> [a] -> [a]
: [Type]
xs
pIsFin :: Prop -> Maybe Type
pIsFin :: Type -> Maybe Type
pIsFin Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PFin) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsPrime :: Prop -> Maybe Type
pIsPrime :: Type -> Maybe Type
pIsPrime Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PPrime) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsGeq :: Prop -> Maybe (Type,Type)
pIsGeq :: Type -> Maybe (Type, Type)
pIsGeq Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PGeq) [Type
t1,Type
t2] -> forall a. a -> Maybe a
Just (Type
t1,Type
t2)
Type
_ -> forall a. Maybe a
Nothing
pIsEqual :: Prop -> Maybe (Type,Type)
pIsEqual :: Type -> Maybe (Type, Type)
pIsEqual Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PEqual) [Type
t1,Type
t2] -> forall a. a -> Maybe a
Just (Type
t1,Type
t2)
Type
_ -> forall a. Maybe a
Nothing
pIsZero :: Prop -> Maybe Type
pIsZero :: Type -> Maybe Type
pIsZero Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PZero) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsLogic :: Prop -> Maybe Type
pIsLogic :: Type -> Maybe Type
pIsLogic Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PLogic) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsRing :: Prop -> Maybe Type
pIsRing :: Type -> Maybe Type
pIsRing Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PRing) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsField :: Prop -> Maybe Type
pIsField :: Type -> Maybe Type
pIsField Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PField) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsIntegral :: Prop -> Maybe Type
pIsIntegral :: Type -> Maybe Type
pIsIntegral Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PIntegral) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsRound :: Prop -> Maybe Type
pIsRound :: Type -> Maybe Type
pIsRound Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PRound) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsEq :: Prop -> Maybe Type
pIsEq :: Type -> Maybe Type
pIsEq Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PEq) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsCmp :: Prop -> Maybe Type
pIsCmp :: Type -> Maybe Type
pIsCmp Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PCmp) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsSignedCmp :: Prop -> Maybe Type
pIsSignedCmp :: Type -> Maybe Type
pIsSignedCmp Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PSignedCmp) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsLiteral :: Prop -> Maybe (Type, Type)
pIsLiteral :: Type -> Maybe (Type, Type)
pIsLiteral Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PLiteral) [Type
t1, Type
t2] -> forall a. a -> Maybe a
Just (Type
t1, Type
t2)
Type
_ -> forall a. Maybe a
Nothing
pIsLiteralLessThan :: Prop -> Maybe (Type, Type)
pIsLiteralLessThan :: Type -> Maybe (Type, Type)
pIsLiteralLessThan Type
ty =
case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PLiteralLessThan) [Type
t1, Type
t2] -> forall a. a -> Maybe a
Just (Type
t1, Type
t2)
Type
_ -> forall a. Maybe a
Nothing
pIsFLiteral :: Prop -> Maybe (Type,Type,Type,Type)
pIsFLiteral :: Type -> Maybe (Type, Type, Type, Type)
pIsFLiteral Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PFLiteral) [Type
t1,Type
t2,Type
t3,Type
t4] -> forall a. a -> Maybe a
Just (Type
t1,Type
t2,Type
t3,Type
t4)
Type
_ -> forall a. Maybe a
Nothing
pIsTrue :: Prop -> Bool
pIsTrue :: Type -> Bool
pIsTrue Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PTrue) [Type]
_ -> Bool
True
Type
_ -> Bool
False
pIsWidth :: Prop -> Maybe Type
pIsWidth :: Type -> Maybe Type
pIsWidth Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (TF TFun
TCWidth) [Type
t1] -> forall a. a -> Maybe a
Just Type
t1
Type
_ -> forall a. Maybe a
Nothing
pIsValidFloat :: Prop -> Maybe (Type,Type)
pIsValidFloat :: Type -> Maybe (Type, Type)
pIsValidFloat Type
ty = case Type -> Type
tNoUser Type
ty of
TCon (PC PC
PValidFloat) [Type
a,Type
b] -> forall a. a -> Maybe a
Just (Type
a,Type
b)
Type
_ -> forall a. Maybe a
Nothing
tNum :: Integral a => a -> Type
tNum :: forall a. Integral a => a -> Type
tNum a
n = TCon -> [Type] -> Type
TCon (TC -> TCon
TC (Integer -> TC
TCNum (forall a. Integral a => a -> Integer
toInteger a
n))) []
tZero :: Type
tZero :: Type
tZero = forall a. Integral a => a -> Type
tNum (Int
0 :: Int)
tOne :: Type
tOne :: Type
tOne = forall a. Integral a => a -> Type
tNum (Int
1 :: Int)
tTwo :: Type
tTwo :: Type
tTwo = forall a. Integral a => a -> Type
tNum (Int
2 :: Int)
tInf :: Type
tInf :: Type
tInf = TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCInf) []
tNat' :: Nat' -> Type
tNat' :: Nat' -> Type
tNat' Nat'
n' = case Nat'
n' of
Nat'
Inf -> Type
tInf
Nat Integer
n -> forall a. Integral a => a -> Type
tNum Integer
n
tAbstract :: UserTC -> [Type] -> Type
tAbstract :: UserTC -> [Type] -> Type
tAbstract UserTC
u [Type]
ts = TCon -> [Type] -> Type
TCon (TC -> TCon
TC (UserTC -> TC
TCAbstract UserTC
u)) [Type]
ts
tNewtype :: Newtype -> [Type] -> Type
tNewtype :: Newtype -> [Type] -> Type
tNewtype Newtype
nt [Type]
ts = Newtype -> [Type] -> Type
TNewtype Newtype
nt [Type]
ts
tBit :: Type
tBit :: Type
tBit = TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCBit) []
tInteger :: Type
tInteger :: Type
tInteger = TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCInteger) []
tRational :: Type
tRational :: Type
tRational = TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCRational) []
tFloat :: Type -> Type -> Type
tFloat :: Type -> Type -> Type
tFloat Type
e Type
p = TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCFloat) [ Type
e, Type
p ]
tIntMod :: Type -> Type
tIntMod :: Type -> Type
tIntMod Type
n = TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCIntMod) [Type
n]
tArray :: Type -> Type -> Type
tArray :: Type -> Type -> Type
tArray Type
a Type
b = TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCArray) [Type
a, Type
b]
tWord :: Type -> Type
tWord :: Type -> Type
tWord Type
a = Type -> Type -> Type
tSeq Type
a Type
tBit
tSeq :: Type -> Type -> Type
tSeq :: Type -> Type -> Type
tSeq Type
a Type
b = TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCSeq) [Type
a,Type
b]
tChar :: Type
tChar :: Type
tChar = Type -> Type
tWord (forall a. Integral a => a -> Type
tNum (Int
8 :: Int))
tString :: Int -> Type
tString :: Int -> Type
tString Int
len = Type -> Type -> Type
tSeq (forall a. Integral a => a -> Type
tNum Int
len) Type
tChar
tRec :: RecordMap Ident Type -> Type
tRec :: RecordMap Ident Type -> Type
tRec = RecordMap Ident Type -> Type
TRec
tTuple :: [Type] -> Type
tTuple :: [Type] -> Type
tTuple [Type]
ts = TCon -> [Type] -> Type
TCon (TC -> TCon
TC (Int -> TC
TCTuple (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts))) [Type]
ts
tFun :: Type -> Type -> Type
tFun :: Type -> Type -> Type
tFun Type
a Type
b = TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCFun) [Type
a,Type
b]
tNoUser :: Type -> Type
tNoUser :: Type -> Type
tNoUser Type
t = case Type
t of
TUser Name
_ [Type]
_ Type
a -> Type -> Type
tNoUser Type
a
Type
_ -> Type
t
tError :: Type -> Type
tError :: Type -> Type
tError Type
t = TCon -> [Type] -> Type
TCon (Kind -> TCon
TError (Kind
k Kind -> Kind -> Kind
:-> Kind
k)) [Type
t]
where k :: Kind
k = forall t. HasKind t => t -> Kind
kindOf Type
t
tf1 :: TFun -> Type -> Type
tf1 :: TFun -> Type -> Type
tf1 TFun
f Type
x = TCon -> [Type] -> Type
TCon (TFun -> TCon
TF TFun
f) [Type
x]
tf2 :: TFun -> Type -> Type -> Type
tf2 :: TFun -> Type -> Type -> Type
tf2 TFun
f Type
x Type
y = TCon -> [Type] -> Type
TCon (TFun -> TCon
TF TFun
f) [Type
x,Type
y]
tf3 :: TFun -> Type -> Type -> Type -> Type
tf3 :: TFun -> Type -> Type -> Type -> Type
tf3 TFun
f Type
x Type
y Type
z = TCon -> [Type] -> Type
TCon (TFun -> TCon
TF TFun
f) [Type
x,Type
y,Type
z]
tSub :: Type -> Type -> Type
tSub :: Type -> Type -> Type
tSub = TFun -> Type -> Type -> Type
tf2 TFun
TCSub
tMul :: Type -> Type -> Type
tMul :: Type -> Type -> Type
tMul = TFun -> Type -> Type -> Type
tf2 TFun
TCMul
tDiv :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tDiv = TFun -> Type -> Type -> Type
tf2 TFun
TCDiv
tMod :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tMod = TFun -> Type -> Type -> Type
tf2 TFun
TCMod
tExp :: Type -> Type -> Type
tExp :: Type -> Type -> Type
tExp = TFun -> Type -> Type -> Type
tf2 TFun
TCExp
tMin :: Type -> Type -> Type
tMin :: Type -> Type -> Type
tMin = TFun -> Type -> Type -> Type
tf2 TFun
TCMin
tCeilDiv :: Type -> Type -> Type
tCeilDiv :: Type -> Type -> Type
tCeilDiv = TFun -> Type -> Type -> Type
tf2 TFun
TCCeilDiv
tCeilMod :: Type -> Type -> Type
tCeilMod :: Type -> Type -> Type
tCeilMod = TFun -> Type -> Type -> Type
tf2 TFun
TCCeilMod
tLenFromThenTo :: Type -> Type -> Type -> Type
tLenFromThenTo :: Type -> Type -> Type -> Type
tLenFromThenTo = TFun -> Type -> Type -> Type -> Type
tf3 TFun
TCLenFromThenTo
(=#=) :: Type -> Type -> Prop
Type
x =#= :: Type -> Type -> Type
=#= Type
y = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PEqual) [Type
x,Type
y]
(=/=) :: Type -> Type -> Prop
Type
x =/= :: Type -> Type -> Type
=/= Type
y = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PNeq) [Type
x,Type
y]
pZero :: Type -> Prop
pZero :: Type -> Type
pZero Type
t = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PZero) [Type
t]
pLogic :: Type -> Prop
pLogic :: Type -> Type
pLogic Type
t = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PLogic) [Type
t]
pRing :: Type -> Prop
pRing :: Type -> Type
pRing Type
t = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PRing) [Type
t]
pIntegral :: Type -> Prop
pIntegral :: Type -> Type
pIntegral Type
t = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PIntegral) [Type
t]
pField :: Type -> Prop
pField :: Type -> Type
pField Type
t = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PField) [Type
t]
pRound :: Type -> Prop
pRound :: Type -> Type
pRound Type
t = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PRound) [Type
t]
pEq :: Type -> Prop
pEq :: Type -> Type
pEq Type
t = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PEq) [Type
t]
pCmp :: Type -> Prop
pCmp :: Type -> Type
pCmp Type
t = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PCmp) [Type
t]
pSignedCmp :: Type -> Prop
pSignedCmp :: Type -> Type
pSignedCmp Type
t = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PSignedCmp) [Type
t]
pLiteral :: Type -> Type -> Prop
pLiteral :: Type -> Type -> Type
pLiteral Type
x Type
y = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PLiteral) [Type
x, Type
y]
pLiteralLessThan :: Type -> Type -> Prop
pLiteralLessThan :: Type -> Type -> Type
pLiteralLessThan Type
x Type
y = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PLiteralLessThan) [Type
x, Type
y]
(>==) :: Type -> Type -> Prop
Type
x >== :: Type -> Type -> Type
>== Type
y = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PGeq) [Type
x,Type
y]
pHas :: Selector -> Type -> Type -> Prop
pHas :: Selector -> Type -> Type -> Type
pHas Selector
l Type
ty Type
fi = TCon -> [Type] -> Type
TCon (PC -> TCon
PC (Selector -> PC
PHas Selector
l)) [Type
ty,Type
fi]
pTrue :: Prop
pTrue :: Type
pTrue = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PTrue) []
pAnd :: [Prop] -> Prop
pAnd :: [Type] -> Type
pAnd [] = Type
pTrue
pAnd [Type
x] = Type
x
pAnd (Type
x : [Type]
xs)
| Just Type
_ <- Type -> Maybe Type
tIsError Type
x = Type
x
| Type -> Bool
pIsTrue Type
x = Type
rest
| Just Type
_ <- Type -> Maybe Type
tIsError Type
rest = Type
rest
| Type -> Bool
pIsTrue Type
rest = Type
x
| Bool
otherwise = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PAnd) [Type
x, Type
rest]
where rest :: Type
rest = [Type] -> Type
pAnd [Type]
xs
pSplitAnd :: Prop -> [Prop]
pSplitAnd :: Type -> [Type]
pSplitAnd Type
p0 = [Type] -> [Type]
go [Type
p0]
where
go :: [Type] -> [Type]
go [] = []
go (Type
q : [Type]
qs) =
case Type -> Type
tNoUser Type
q of
TCon (PC PC
PAnd) [Type
l,Type
r] -> [Type] -> [Type]
go (Type
l forall a. a -> [a] -> [a]
: Type
r forall a. a -> [a] -> [a]
: [Type]
qs)
TCon (PC PC
PTrue) [Type]
_ -> [Type] -> [Type]
go [Type]
qs
Type
_ -> Type
q forall a. a -> [a] -> [a]
: [Type] -> [Type]
go [Type]
qs
pFin :: Type -> Prop
pFin :: Type -> Type
pFin Type
ty =
case Type -> Type
tNoUser Type
ty of
TCon (TC (TCNum Integer
_)) [Type]
_ -> Type
pTrue
TCon (TC TC
TCInf) [Type]
_ -> Type -> Type
tError Type
prop
Type
_ -> Type
prop
where
prop :: Type
prop = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PFin) [Type
ty]
pValidFloat :: Type -> Type -> Type
pValidFloat :: Type -> Type -> Type
pValidFloat Type
e Type
p = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PValidFloat) [Type
e,Type
p]
pPrime :: Type -> Prop
pPrime :: Type -> Type
pPrime Type
ty =
case Type -> Type
tNoUser Type
ty of
TCon (TC TC
TCInf) [Type]
_ -> Type -> Type
tError Type
prop
Type
_ -> Type
prop
where
prop :: Type
prop = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PPrime) [Type
ty]
pNegNumeric :: Prop -> [Prop]
pNegNumeric :: Type -> [Type]
pNegNumeric Type
prop =
case Type -> Type
tNoUser Type
prop of
TCon TCon
tcon [Type]
tys ->
case TCon
tcon of
PC PC
pc ->
case PC
pc of
PC
PEqual -> [TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PNeq) [Type]
tys]
PC
PNeq -> [TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PEqual) [Type]
tys]
PC
PGeq -> [TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PNeq) [Type]
tys, TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PGeq) (forall a. [a] -> [a]
reverse [Type]
tys)]
PC
PFin | [Type
ty] <- [Type]
tys -> [Type
ty Type -> Type -> Type
=#= Type
tInf]
| Bool
otherwise -> forall {a}. a
bad
PC
PTrue -> [TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PEqual) [Type
tZero, Type
tOne]]
PC
_ -> forall {a}. a
bad
TError Kind
_ki -> [Type
prop]
TC TC
_tc -> forall {a}. a
bad
TF TFun
_tf -> forall {a}. a
bad
Type
_ -> forall {a}. a
bad
where
bad :: a
bad = forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"pNegNumeric"
[ [Char]
"Unexpeceted numeric constraint:"
, forall a. PP a => a -> [Char]
pretty Type
prop
]
noFreeVariables :: FVS t => t -> Bool
noFreeVariables :: forall t. FVS t => t -> Bool
noFreeVariables = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. TVar -> Bool
isFreeTV) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. FVS t => t -> Set TVar
fvs
freeParams :: FVS t => t -> Set TParam
freeParams :: forall t. FVS t => t -> Set TParam
freeParams t
x = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map TVar -> Set TParam
params (forall a. Set a -> [a]
Set.toList (forall t. FVS t => t -> Set TVar
fvs t
x)))
where
params :: TVar -> Set TParam
params (TVFree Int
_ Kind
_ Set TParam
tps TVarInfo
_) = Set TParam
tps
params (TVBound TParam
tp) = forall a. a -> Set a
Set.singleton TParam
tp
class FVS t where
fvs :: t -> Set TVar
instance FVS Type where
fvs :: Type -> Set TVar
fvs = Type -> Set TVar
go
where
go :: Type -> Set TVar
go Type
ty =
case Type
ty of
TCon TCon
_ [Type]
ts -> forall t. FVS t => t -> Set TVar
fvs [Type]
ts
TVar TVar
x -> forall a. a -> Set a
Set.singleton TVar
x
TUser Name
_ [Type]
_ Type
t -> Type -> Set TVar
go Type
t
TRec RecordMap Ident Type
fs -> forall t. FVS t => t -> Set TVar
fvs (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs)
TNewtype Newtype
_nt [Type]
ts -> forall t. FVS t => t -> Set TVar
fvs [Type]
ts
class FreeAbstract t where
freeAbstract :: t -> Set UserTC
instance FreeAbstract a => FreeAbstract [a] where
freeAbstract :: [a] -> Set UserTC
freeAbstract = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall t. FreeAbstract t => t -> Set UserTC
freeAbstract
instance (FreeAbstract a, FreeAbstract b) => FreeAbstract (a,b) where
freeAbstract :: (a, b) -> Set UserTC
freeAbstract (a
a,b
b) = forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall t. FreeAbstract t => t -> Set UserTC
freeAbstract a
a) (forall t. FreeAbstract t => t -> Set UserTC
freeAbstract b
b)
instance FreeAbstract TCon where
freeAbstract :: TCon -> Set UserTC
freeAbstract TCon
tc =
case TCon
tc of
TC (TCAbstract UserTC
ut) -> forall a. a -> Set a
Set.singleton UserTC
ut
TCon
_ -> forall a. Set a
Set.empty
instance FreeAbstract Type where
freeAbstract :: Type -> Set UserTC
freeAbstract Type
ty =
case Type
ty of
TCon TCon
tc [Type]
ts -> forall t. FreeAbstract t => t -> Set UserTC
freeAbstract (TCon
tc,[Type]
ts)
TVar {} -> forall a. Set a
Set.empty
TUser Name
_ [Type]
_ Type
t -> forall t. FreeAbstract t => t -> Set UserTC
freeAbstract Type
t
TRec RecordMap Ident Type
fs -> forall t. FreeAbstract t => t -> Set UserTC
freeAbstract (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs)
TNewtype Newtype
_nt [Type]
ts -> forall t. FreeAbstract t => t -> Set UserTC
freeAbstract [Type]
ts
instance FVS a => FVS (Maybe a) where
fvs :: Maybe a -> Set TVar
fvs Maybe a
Nothing = forall a. Set a
Set.empty
fvs (Just a
x) = forall t. FVS t => t -> Set TVar
fvs a
x
instance FVS a => FVS [a] where
fvs :: [a] -> Set TVar
fvs [a]
xs = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map forall t. FVS t => t -> Set TVar
fvs [a]
xs)
instance (FVS a, FVS b) => FVS (a,b) where
fvs :: (a, b) -> Set TVar
fvs (a
x,b
y) = forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall t. FVS t => t -> Set TVar
fvs a
x) (forall t. FVS t => t -> Set TVar
fvs b
y)
instance FVS Schema where
fvs :: Schema -> Set TVar
fvs (Forall [TParam]
as [Type]
ps Type
t) =
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall t. FVS t => t -> Set TVar
fvs [Type]
ps) (forall t. FVS t => t -> Set TVar
fvs Type
t)) Set TVar
bound
where bound :: Set TVar
bound = forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as)
instance PP TParam where
ppPrec :: Int -> TParam -> Doc
ppPrec = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty
instance PP (WithNames TParam) where
ppPrec :: Int -> WithNames TParam -> Doc
ppPrec Int
_ (WithNames TParam
p NameMap
mp) = forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
mp (TParam -> TVar
tpVar TParam
p)
addTNames :: [TParam] -> NameMap -> NameMap
addTNames :: [TParam] -> NameMap -> NameMap
addTNames [TParam]
as NameMap
ns = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert) NameMap
ns
forall a b. (a -> b) -> a -> b
$ [(Int, [Char])]
named forall a. [a] -> [a] -> [a]
++ forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
unnamed_nums [[Char]]
numNames
forall a. [a] -> [a] -> [a]
++ forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
unnamed_vals [[Char]]
valNames
where avail :: [[Char]] -> [[Char]]
avail [[Char]]
xs = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [[Char]]
used) ([[Char]] -> [[Char]]
nameList [[Char]]
xs)
numNames :: [[Char]]
numNames = [[Char]] -> [[Char]]
avail [[Char]
"n",[Char]
"m",[Char]
"i",[Char]
"j",[Char]
"k"]
valNames :: [[Char]]
valNames = [[Char]] -> [[Char]]
avail [[Char]
"a",[Char]
"b",[Char]
"c",[Char]
"d",[Char]
"e"]
nm :: TParam -> (Int, Maybe Name, Kind)
nm TParam
x = (TParam -> Int
tpUnique TParam
x, TParam -> Maybe Name
tpName TParam
x, TParam -> Kind
tpKind TParam
x)
named :: [(Int, [Char])]
named = [ (Int
u,forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
pp Name
n)) | (Int
u,Just Name
n,Kind
_) <- forall a b. (a -> b) -> [a] -> [b]
map TParam -> (Int, Maybe Name, Kind)
nm [TParam]
as ]
unnamed_nums :: [Int]
unnamed_nums = [ Int
u | (Int
u,Maybe Name
Nothing,Kind
KNum) <- forall a b. (a -> b) -> [a] -> [b]
map TParam -> (Int, Maybe Name, Kind)
nm [TParam]
as ]
unnamed_vals :: [Int]
unnamed_vals = [ Int
u | (Int
u,Maybe Name
Nothing,Kind
KType) <- forall a b. (a -> b) -> [a] -> [b]
map TParam -> (Int, Maybe Name, Kind)
nm [TParam]
as ]
used :: [[Char]]
used = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Int, [Char])]
named forall a. [a] -> [a] -> [a]
++ forall a. IntMap a -> [a]
IntMap.elems NameMap
ns
ppNewtypeShort :: Newtype -> Doc
ppNewtypeShort :: Newtype -> Doc
ppNewtypeShort Newtype
nt =
[Char] -> Doc
text [Char]
"newtype" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (Newtype -> Name
ntName Newtype
nt) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
9) [TParam]
ps)
where
ps :: [TParam]
ps = Newtype -> [TParam]
ntParams Newtype
nt
nm :: NameMap
nm = [TParam] -> NameMap -> NameMap
addTNames [TParam]
ps NameMap
emptyNameMap
ppNewtypeFull :: Newtype -> Doc
ppNewtypeFull :: Newtype -> Doc
ppNewtypeFull Newtype
nt =
[Char] -> Doc
text [Char]
"newtype" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (Newtype -> Name
ntName Newtype
nt) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
9) [TParam]
ps)
Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Doc
cs Doc -> Doc -> Doc
$$ (Doc
"=" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (Newtype -> Name
ntConName Newtype
nt) Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 Doc
fs))
where
ps :: [TParam]
ps = Newtype -> [TParam]
ntParams Newtype
nt
nm :: NameMap
nm = [TParam] -> NameMap -> NameMap
addTNames [TParam]
ps NameMap
emptyNameMap
fs :: Doc
fs = [Doc] -> Doc
vcat [ forall a. PP a => a -> Doc
pp Ident
f Doc -> Doc -> Doc
<.> Doc
":" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Type
t | (Ident
f,Type
t) <- forall a b. RecordMap a b -> [(a, b)]
canonicalFields (Newtype -> RecordMap Ident Type
ntFields Newtype
nt) ]
cs :: Doc
cs = [Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp (Newtype -> [Type]
ntConstraints Newtype
nt))
instance PP Schema where
ppPrec :: Int -> Schema -> Doc
ppPrec = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty
instance PP (WithNames Schema) where
ppPrec :: Int -> WithNames Schema -> Doc
ppPrec Int
_ (WithNames Schema
s NameMap
ns)
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [TParam]
sVars Schema
s) Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [Type]
sProps Schema
s) = Doc
body
| Bool
otherwise = Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
sep ([Doc]
vars forall a. [a] -> [a] -> [a]
++ [Doc]
props forall a. [a] -> [a] -> [a]
++ [Doc
body]))
where
body :: Doc
body = forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 (Schema -> Type
sType Schema
s)
vars :: [Doc]
vars = case Schema -> [TParam]
sVars Schema
s of
[] -> []
[TParam]
vs -> [Int -> Doc -> Doc
nest Int
1 (Doc -> Doc
braces ([Doc] -> Doc
commaSepFill (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [TParam]
vs)))]
props :: [Doc]
props = case Schema -> [Type]
sProps Schema
s of
[] -> []
[Type]
ps -> [Int -> Doc -> Doc
nest Int
1 (Doc -> Doc
parens ([Doc] -> Doc
commaSepFill (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [Type]
ps))) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"=>"]
ns1 :: NameMap
ns1 = [TParam] -> NameMap -> NameMap
addTNames (Schema -> [TParam]
sVars Schema
s) NameMap
ns
instance PP TySyn where
ppPrec :: Int -> TySyn -> Doc
ppPrec = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty
instance PP (WithNames TySyn) where
ppPrec :: Int -> WithNames TySyn -> Doc
ppPrec Int
_ (WithNames TySyn
ts NameMap
ns) =
Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep
[ [Doc] -> Doc
fsep ([[Char] -> Doc
text [Char]
"type"] forall a. [a] -> [a] -> [a]
++ [Doc]
ctr forall a. [a] -> [a] -> [a]
++ [Doc]
lhs forall a. [a] -> [a] -> [a]
++ [Char -> Doc
char Char
'='])
, forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 (TySyn -> Type
tsDef TySyn
ts)
]
where ns1 :: NameMap
ns1 = [TParam] -> NameMap -> NameMap
addTNames (TySyn -> [TParam]
tsParams TySyn
ts) NameMap
ns
ctr :: [Doc]
ctr = case Kind -> Kind
kindResult (forall t. HasKind t => t -> Kind
kindOf TySyn
ts) of
Kind
KProp -> [[Char] -> Doc
text [Char]
"constraint"]
Kind
_ -> []
n :: Name
n = TySyn -> Name
tsName TySyn
ts
lhs :: [Doc]
lhs = case (Name -> Maybe Fixity
nameFixity Name
n, TySyn -> [TParam]
tsParams TySyn
ts) of
(Just Fixity
_, [TParam
x, TParam
y]) ->
[forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 TParam
x, forall a. PP a => a -> Doc
pp (Name -> Ident
nameIdent Name
n), forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 TParam
y]
(Maybe Fixity
_, [TParam]
ps) ->
[forall a. PP a => a -> Doc
pp Name
n] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [TParam]
ps
instance PP Newtype where
ppPrec :: Int -> Newtype -> Doc
ppPrec = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty
instance PP (WithNames Newtype) where
ppPrec :: Int -> WithNames Newtype -> Doc
ppPrec Int
_ (WithNames Newtype
nt NameMap
_) = Newtype -> Doc
ppNewtypeShort Newtype
nt
instance PP (WithNames Type) where
ppPrec :: Int -> WithNames Type -> Doc
ppPrec Int
prec ty0 :: WithNames Type
ty0@(WithNames Type
ty NameMap
nmMap) =
case Type
ty of
TVar TVar
a -> forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nmMap TVar
a
TNewtype Newtype
nt [Type]
ts -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (forall a. PP a => a -> Doc
pp (Newtype -> Name
ntName Newtype
nt) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Type]
ts)
TRec RecordMap Ident Type
fs -> [Doc] -> Doc
ppRecord
[ forall a. PP a => a -> Doc
pp Ident
l Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t | (Ident
l,Type
t) <- forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
displayFields RecordMap Ident Type
fs ]
Type
_ | Just Infix Ident (WithNames Type)
tinf <- WithNames Type -> Maybe (Infix Ident (WithNames Type))
isTInfix WithNames Type
ty0 -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
2)
forall a b. (a -> b) -> a -> b
$ forall thing op.
(PP thing, PP op) =>
Int -> (thing -> Maybe (Infix op thing)) -> Infix op thing -> Doc
ppInfix Int
2 WithNames Type -> Maybe (Infix Ident (WithNames Type))
isTInfix Infix Ident (WithNames Type)
tinf
TUser Name
c [Type]
ts Type
t ->
(NameDisp -> Doc) -> Doc
withNameDisp forall a b. (a -> b) -> a -> b
$ \NameDisp
disp ->
case Name -> Maybe OrigName
asOrigName Name
c of
Just OrigName
og | NameFormat
NotInScope <- OrigName -> NameDisp -> NameFormat
getNameFormat OrigName
og NameDisp
disp ->
forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
prec Type
t
Maybe OrigName
_ ->
case [Type]
ts of
[] -> forall a. PP a => a -> Doc
pp Name
c
[Type]
_ -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (forall a. PP a => a -> Doc
pp Name
c forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Type]
ts)
TCon (TC TC
tc) [Type]
ts ->
case (TC
tc,[Type]
ts) of
(TCNum Integer
n, []) -> Integer -> Doc
integer Integer
n
(TC
TCInf, []) -> [Char] -> Doc
text [Char]
"inf"
(TC
TCBit, []) -> [Char] -> Doc
text [Char]
"Bit"
(TC
TCInteger, []) -> [Char] -> Doc
text [Char]
"Integer"
(TC
TCRational, []) -> [Char] -> Doc
text [Char]
"Rational"
(TC
TCIntMod, [Type
n]) -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"Z" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
n
(TC
TCSeq, [Type
t1,TCon (TC TC
TCBit) []]) -> Doc -> Doc
brackets (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1)
(TC
TCSeq, [Type
t1,Type
t2]) -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
4)
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1) Doc -> Doc -> Doc
<.> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
4 Type
t2
(TC
TCFun, [Type
t1,Type
t2]) -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
1)
forall a b. (a -> b) -> a -> b
$ forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
2 Type
t1 Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"->" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
1 Type
t2
(TCTuple Int
_, [Type]
fs) -> [Doc] -> Doc
ppTuple forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0) [Type]
fs
(TC
_, [Type]
_) -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (forall a. PP a => a -> Doc
pp TC
tc forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Type]
ts))
TCon (PC PC
pc) [Type]
ts ->
case (PC
pc,[Type]
ts) of
(PC
PEqual, [Type
t1,Type
t2]) -> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1 Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"==" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t2
(PC
PNeq , [Type
t1,Type
t2]) -> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1 Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"!=" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t2
(PC
PGeq, [Type
t1,Type
t2]) -> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1 Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
">=" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t2
(PC
PFin, [Type
t1]) -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"fin" Doc -> Doc -> Doc
<+> (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1)
(PC
PPrime, [Type
t1]) -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"prime" Doc -> Doc -> Doc
<+> (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1)
(PHas Selector
x, [Type
t1,Type
t2]) -> Selector -> Doc
ppSelector Selector
x Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"of"
Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1 Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"is" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t2
(PC
PAnd, [Type
t1,Type
t2]) -> Int -> Doc -> Doc
nest Int
1 (Doc -> Doc
parens ([Doc] -> Doc
commaSepFill (forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0) (Type
t1 forall a. a -> [a] -> [a]
: Type -> [Type]
pSplitAnd Type
t2))))
(PC
PRing, [Type
t1]) -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
(PC
PField, [Type
t1]) -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
(PC
PIntegral, [Type
t1]) -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
(PC
PRound, [Type
t1]) -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
(PC
PCmp, [Type
t1]) -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
(PC
PSignedCmp, [Type
t1]) -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
(PC
PLiteral, [Type
t1,Type
t2]) -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1 Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t2
(PC
PLiteralLessThan, [Type
t1,Type
t2]) -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1 Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t2
(PC
_, [Type]
_) -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (forall a. PP a => a -> Doc
pp PC
pc forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Type]
ts)
TCon TCon
f [Type]
ts -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (forall a. PP a => a -> Doc
pp TCon
f forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Type]
ts)
where
go :: Int -> a -> Doc
go Int
p a
t = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nmMap Int
p a
t
isTInfix :: WithNames Type -> Maybe (Infix Ident (WithNames Type))
isTInfix (WithNames (TCon TCon
tc [Type
ieLeft',Type
ieRight']) NameMap
_) =
do let ieLeft :: WithNames Type
ieLeft = forall a. a -> NameMap -> WithNames a
WithNames Type
ieLeft' NameMap
nmMap
ieRight :: WithNames Type
ieRight = forall a. a -> NameMap -> WithNames a
WithNames Type
ieRight' NameMap
nmMap
(Ident
ieOp, Fixity
ieFixity) <- TCon -> Maybe (Ident, Fixity)
infixPrimTy TCon
tc
forall (m :: * -> *) a. Monad m => a -> m a
return Infix { Fixity
Ident
WithNames Type
ieFixity :: Fixity
ieRight :: WithNames Type
ieLeft :: WithNames Type
ieOp :: Ident
ieFixity :: Fixity
ieOp :: Ident
ieRight :: WithNames Type
ieLeft :: WithNames Type
.. }
isTInfix (WithNames (TUser Name
n [Type
ieLeft',Type
ieRight'] Type
_) NameMap
_)
| Ident -> Bool
isInfixIdent (Name -> Ident
nameIdent Name
n) =
do let ieLeft :: WithNames Type
ieLeft = forall a. a -> NameMap -> WithNames a
WithNames Type
ieLeft' NameMap
nmMap
ieRight :: WithNames Type
ieRight = forall a. a -> NameMap -> WithNames a
WithNames Type
ieRight' NameMap
nmMap
ieFixity :: Fixity
ieFixity = forall a. a -> Maybe a -> a
fromMaybe Fixity
defaultFixity (Name -> Maybe Fixity
nameFixity Name
n)
ieOp :: Ident
ieOp = Name -> Ident
nameIdent Name
n
forall (m :: * -> *) a. Monad m => a -> m a
return Infix { Fixity
Ident
WithNames Type
ieOp :: Ident
ieFixity :: Fixity
ieRight :: WithNames Type
ieLeft :: WithNames Type
ieFixity :: Fixity
ieRight :: WithNames Type
ieLeft :: WithNames Type
ieOp :: Ident
.. }
isTInfix WithNames Type
_ = forall a. Maybe a
Nothing
instance PP (WithNames TVar) where
ppPrec :: Int -> WithNames TVar -> Doc
ppPrec Int
_ (WithNames TVar
tv NameMap
mp) =
case TVar
tv of
TVBound {} -> Doc
nmTxt
TVFree {} -> Doc
"?" Doc -> Doc -> Doc
<.> Doc
nmTxt
where
nmTxt :: Doc
nmTxt
| Just [Char]
a <- forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (TVar -> Int
tvUnique TVar
tv) NameMap
mp = [Char] -> Doc
text [Char]
a
| Bool
otherwise =
case TVar
tv of
TVBound TParam
x ->
let declNm :: a -> Doc
declNm a
n = forall a. PP a => a -> Doc
pp a
n Doc -> Doc -> Doc
<.> Doc
"`" Doc -> Doc -> Doc
<.> Int -> Doc
int (TParam -> Int
tpUnique TParam
x) in
case TParam -> TPFlavor
tpFlav TParam
x of
TPModParam Name
n -> forall a. PPName a => a -> Doc
ppPrefixName Name
n
TPFlavor
TPUnifyVar -> Kind -> TypeSource -> Int -> Doc
pickTVarName (TParam -> Kind
tpKind TParam
x) (TVarInfo -> TypeSource
tvarDesc (TParam -> TVarInfo
tpInfo TParam
x)) (TParam -> Int
tpUnique TParam
x)
TPSchemaParam Name
n -> forall a. PP a => a -> Doc
declNm Name
n
TPTySynParam Name
n -> forall a. PP a => a -> Doc
declNm Name
n
TPPropSynParam Name
n -> forall a. PP a => a -> Doc
declNm Name
n
TPNewtypeParam Name
n -> forall a. PP a => a -> Doc
declNm Name
n
TPPrimParam Name
n -> forall a. PP a => a -> Doc
declNm Name
n
TVFree Int
x Kind
k Set TParam
_ TVarInfo
d -> Kind -> TypeSource -> Int -> Doc
pickTVarName Kind
k (TVarInfo -> TypeSource
tvarDesc TVarInfo
d) Int
x
pickTVarName :: Kind -> TypeSource -> Int -> Doc
pickTVarName :: Kind -> TypeSource -> Int -> Doc
pickTVarName Kind
k TypeSource
src Int
uni =
[Char] -> Doc
text forall a b. (a -> b) -> a -> b
$
case TypeSource
src of
TVFromModParam Name
n -> forall a. PP a => a -> [Char]
using Name
n
TVFromSignature Name
n -> forall a. PP a => a -> [Char]
using Name
n
TypeSource
TypeWildCard -> ShowS
mk forall a b. (a -> b) -> a -> b
$ case Kind
k of
Kind
KNum -> [Char]
"n"
Kind
_ -> [Char]
"a"
TypeOfRecordField Ident
i -> forall a. PP a => a -> [Char]
using Ident
i
TypeOfTupleField Int
n -> ShowS
mk ([Char]
"tup_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n)
TypeSource
TypeOfSeqElement -> ShowS
mk [Char]
"a"
TypeSource
LenOfSeq -> ShowS
mk [Char]
"n"
TypeParamInstNamed Name
_ Ident
i -> forall a. PP a => a -> [Char]
using Ident
i
TypeParamInstPos Name
f Int
n -> ShowS
mk (forall a. PP a => a -> [Char]
sh Name
f forall a. [a] -> [a] -> [a]
++ [Char]
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n)
DefinitionOf Name
x ->
case Name -> NameInfo
nameInfo Name
x of
GlobalName NameSource
SystemName OrigName
og
| OrigName -> ModPath
ogModule OrigName
og forall a. Eq a => a -> a -> Bool
== ModName -> ModPath
TopModule ModName
exprModName -> ShowS
mk [Char]
"it"
NameInfo
_ -> forall a. PP a => a -> [Char]
using Name
x
TypeSource
LenOfCompGen -> ShowS
mk [Char]
"n"
TypeSource
GeneratorOfListComp -> [Char]
"seq"
TypeSource
TypeOfIfCondExpr -> [Char]
"b"
TypeOfArg ArgDescr
ad -> ShowS
mk (case ArgDescr -> Maybe Int
argDescrNumber ArgDescr
ad of
Maybe Int
Nothing -> [Char]
"arg"
Just Int
n -> [Char]
"arg_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n)
TypeSource
TypeOfRes -> [Char]
"res"
TypeSource
FunApp -> [Char]
"fun"
TypeSource
TypeFromUserAnnotation -> [Char]
"user"
TypeSource
TypeErrorPlaceHolder -> [Char]
"err"
where
sh :: a -> [Char]
sh a
a = forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
pp a
a)
using :: a -> [Char]
using a
a = ShowS
mk (forall a. PP a => a -> [Char]
sh a
a)
mk :: ShowS
mk [Char]
a = [Char]
a forall a. [a] -> [a] -> [a]
++ [Char]
"`" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
uni
instance PP TVar where
ppPrec :: Int -> TVar -> Doc
ppPrec = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty
instance PP Type where
ppPrec :: Int -> Type -> Doc
ppPrec Int
n Type
t = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty Int
n Type
t
instance PP TVarInfo where
ppPrec :: Int -> TVarInfo -> Doc
ppPrec Int
_ TVarInfo
tvinfo = [Doc] -> Doc
hsep forall a b. (a -> b) -> a -> b
$ [forall a. PP a => a -> Doc
pp (TVarInfo -> TypeSource
tvarDesc TVarInfo
tvinfo)] forall a. [a] -> [a] -> [a]
++ [Doc]
loc
where
loc :: [Doc]
loc = if Range
rng forall a. Eq a => a -> a -> Bool
== Range
emptyRange then [] else [Doc
"at" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Range
rng]
rng :: Range
rng = TVarInfo -> Range
tvarSource TVarInfo
tvinfo
instance PP ArgDescr where
ppPrec :: Int -> ArgDescr -> Doc
ppPrec Int
_ ArgDescr
ad = [Doc] -> Doc
hsep ([Doc
which, Doc
"argument"] forall a. [a] -> [a] -> [a]
++ [Doc]
ofFun)
where
which :: Doc
which = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"function" forall a. (Integral a, Show a, Eq a) => a -> Doc
ordinal (ArgDescr -> Maybe Int
argDescrNumber ArgDescr
ad)
ofFun :: [Doc]
ofFun = case ArgDescr -> Maybe Name
argDescrFun ArgDescr
ad of
Maybe Name
Nothing -> []
Just Name
f -> [Doc
"of" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Name
f]
instance PP TypeSource where
ppPrec :: Int -> TypeSource -> Doc
ppPrec Int
_ TypeSource
tvsrc =
case TypeSource
tvsrc of
TVFromModParam Name
m -> Doc
"module parameter" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Name
m
TVFromSignature Name
x -> Doc
"signature variable" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (forall a. PP a => a -> Doc
pp Name
x)
TypeSource
TypeWildCard -> Doc
"type wildcard (_)"
TypeOfRecordField Ident
l -> Doc
"type of field" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (forall a. PP a => a -> Doc
pp Ident
l)
TypeOfTupleField Int
n -> Doc
"type of" Doc -> Doc -> Doc
<+> forall a. (Integral a, Show a, Eq a) => a -> Doc
ordinal Int
n Doc -> Doc -> Doc
<+> Doc
"tuple field"
TypeSource
TypeOfSeqElement -> Doc
"type of sequence member"
TypeSource
LenOfSeq -> Doc
"length of sequence"
TypeParamInstNamed Name
f Ident
i -> Doc
"type argument" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (forall a. PP a => a -> Doc
pp Ident
i) Doc -> Doc -> Doc
<+>
Doc
"of" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (forall a. PP a => a -> Doc
pp Name
f)
TypeParamInstPos Name
f Int
i -> forall a. (Integral a, Show a, Eq a) => a -> Doc
ordinal Int
i Doc -> Doc -> Doc
<+> Doc
"type argument of" Doc -> Doc -> Doc
<+>
Doc -> Doc
quotes (forall a. PP a => a -> Doc
pp Name
f)
DefinitionOf Name
x -> Doc
"the type of" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (forall a. PP a => a -> Doc
pp Name
x)
TypeSource
LenOfCompGen -> Doc
"length of comprehension generator"
TypeOfArg ArgDescr
ad -> Doc
"type of" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp ArgDescr
ad
TypeSource
TypeOfRes -> Doc
"type of function result"
TypeSource
TypeOfIfCondExpr -> Doc
"type of `if` condition"
TypeSource
TypeFromUserAnnotation -> Doc
"user annotation"
TypeSource
GeneratorOfListComp -> Doc
"generator in a list comprehension"
TypeSource
FunApp -> Doc
"function call"
TypeSource
TypeErrorPlaceHolder -> Doc
"type error place-holder"
instance PP ModParamNames where
ppPrec :: Int -> ModParamNames -> Doc
ppPrec Int
_ ModParamNames
ps =
let tps :: [ModTParam]
tps = forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
ps)
in
[Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp [ModTParam]
tps forall a. [a] -> [a] -> [a]
++
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ModParamNames -> [Located Type]
mpnConstraints ModParamNames
ps) then [] else
[ Doc
"type constraint" Doc -> Doc -> Doc
<+>
Doc -> Doc
parens ([Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP a => a -> Doc
pp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
thing) (ModParamNames -> [Located Type]
mpnConstraints ModParamNames
ps)))
] forall a. [a] -> [a] -> [a]
++
[ forall a. PP a => a -> Doc
pp TySyn
t | TySyn
t <- forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name TySyn
mpnTySyn ModParamNames
ps) ] forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp (forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
ps))
instance PP ModTParam where
ppPrec :: Int -> ModTParam -> Doc
ppPrec Int
_ ModTParam
p =
Doc
"type" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (ModTParam -> Name
mtpName ModTParam
p) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (ModTParam -> Kind
mtpKind ModTParam
p)
instance PP ModVParam where
ppPrec :: Int -> ModVParam -> Doc
ppPrec Int
_ ModVParam
p = forall a. PP a => a -> Doc
pp (ModVParam -> Name
mvpName ModVParam
p) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (ModVParam -> Schema
mvpType ModVParam
p)