{-# 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 qualified Data.IntMap as IntMap
import Data.Set (Set)
import qualified Data.Set as Set
import Data.List(sortBy)
import Data.Ord(comparing)
import Cryptol.Parser.Selector
import Cryptol.Parser.Fixity
import Cryptol.Parser.Position(Range,emptyRange)
import Cryptol.ModuleSystem.Name
import Cryptol.Utils.Ident (Ident)
import Cryptol.TypeCheck.TCon
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Solver.InfNat
import Cryptol.Utils.Panic(panic)
import Prelude
infix 4 =#=, >==
infixr 5 `tFun`
data Schema = Forall { Schema -> [TParam]
sVars :: [TParam], Schema -> [Prop]
sProps :: [Prop], Schema -> Prop
sType :: Type }
deriving (Schema -> Schema -> Bool
(Schema -> Schema -> Bool)
-> (Schema -> Schema -> Bool) -> Eq Schema
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 -> String
(Int -> Schema -> ShowS)
-> (Schema -> String) -> ([Schema] -> ShowS) -> Show Schema
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Schema] -> ShowS
$cshowList :: [Schema] -> ShowS
show :: Schema -> String
$cshow :: Schema -> String
showsPrec :: Int -> Schema -> ShowS
$cshowsPrec :: Int -> Schema -> ShowS
Show, (forall x. Schema -> Rep Schema x)
-> (forall x. Rep Schema x -> Schema) -> Generic Schema
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 -> ()
(Schema -> ()) -> NFData 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. TParam -> Rep TParam x)
-> (forall x. Rep TParam x -> TParam) -> Generic TParam
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 -> ()
(TParam -> ()) -> NFData TParam
forall a. (a -> ()) -> NFData a
rnf :: TParam -> ()
$crnf :: TParam -> ()
NFData, Int -> TParam -> ShowS
[TParam] -> ShowS
TParam -> String
(Int -> TParam -> ShowS)
-> (TParam -> String) -> ([TParam] -> ShowS) -> Show TParam
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TParam] -> ShowS
$cshowList :: [TParam] -> ShowS
show :: TParam -> String
$cshow :: TParam -> String
showsPrec :: Int -> TParam -> ShowS
$cshowsPrec :: Int -> TParam -> ShowS
Show)
data TPFlavor = TPModParam Name
| TPOther (Maybe Name)
deriving ((forall x. TPFlavor -> Rep TPFlavor x)
-> (forall x. Rep TPFlavor x -> TPFlavor) -> Generic TPFlavor
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 -> ()
(TPFlavor -> ()) -> NFData TPFlavor
forall a. (a -> ()) -> NFData a
rnf :: TPFlavor -> ()
$crnf :: TPFlavor -> ()
NFData, Int -> TPFlavor -> ShowS
[TPFlavor] -> ShowS
TPFlavor -> String
(Int -> TPFlavor -> ShowS)
-> (TPFlavor -> String) -> ([TPFlavor] -> ShowS) -> Show TPFlavor
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TPFlavor] -> ShowS
$cshowList :: [TPFlavor] -> ShowS
show :: TPFlavor -> String
$cshow :: TPFlavor -> String
showsPrec :: Int -> TPFlavor -> ShowS
$cshowsPrec :: Int -> TPFlavor -> ShowS
Show)
tMono :: Type -> Schema
tMono :: Prop -> Schema
tMono = [TParam] -> [Prop] -> Prop -> Schema
Forall [] []
isMono :: Schema -> Maybe Type
isMono :: Schema -> Maybe Prop
isMono s :: Schema
s =
case Schema
s of
Forall [] [] t :: Prop
t -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t
_ -> Maybe Prop
forall a. Maybe a
Nothing
schemaParam :: Name -> TPFlavor
schemaParam :: Name -> TPFlavor
schemaParam x :: Name
x = Maybe Name -> TPFlavor
TPOther (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x)
tySynParam :: Name -> TPFlavor
tySynParam :: Name -> TPFlavor
tySynParam x :: Name
x = Maybe Name -> TPFlavor
TPOther (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x)
propSynParam :: Name -> TPFlavor
propSynParam :: Name -> TPFlavor
propSynParam x :: Name
x = Maybe Name -> TPFlavor
TPOther (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x)
newtypeParam :: Name -> TPFlavor
newtypeParam :: Name -> TPFlavor
newtypeParam x :: Name
x = Maybe Name -> TPFlavor
TPOther (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x)
modTyParam :: Name -> TPFlavor
modTyParam :: Name -> TPFlavor
modTyParam = Name -> TPFlavor
TPModParam
tpfName :: TPFlavor -> Maybe Name
tpfName :: TPFlavor -> Maybe Name
tpfName f :: TPFlavor
f =
case TPFlavor
f of
TPModParam x :: Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
TPOther x :: Maybe Name
x -> Maybe Name
x
tpName :: TParam -> Maybe Name
tpName :: TParam -> Maybe Name
tpName = TPFlavor -> Maybe Name
tpfName (TPFlavor -> Maybe Name)
-> (TParam -> TPFlavor) -> TParam -> Maybe Name
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 ![(Ident,Type)]
deriving (Int -> Prop -> ShowS
[Prop] -> ShowS
Prop -> String
(Int -> Prop -> ShowS)
-> (Prop -> String) -> ([Prop] -> ShowS) -> Show Prop
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Prop] -> ShowS
$cshowList :: [Prop] -> ShowS
show :: Prop -> String
$cshow :: Prop -> String
showsPrec :: Int -> Prop -> ShowS
$cshowsPrec :: Int -> Prop -> ShowS
Show, (forall x. Prop -> Rep Prop x)
-> (forall x. Rep Prop x -> Prop) -> Generic Prop
forall x. Rep Prop x -> Prop
forall x. Prop -> Rep Prop x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Prop x -> Prop
$cfrom :: forall x. Prop -> Rep Prop x
Generic, Prop -> ()
(Prop -> ()) -> NFData Prop
forall a. (a -> ()) -> NFData a
rnf :: Prop -> ()
$crnf :: Prop -> ()
NFData)
data TVar = TVFree !Int Kind (Set TParam) TVarInfo
| TVBound {-# UNPACK #-} !TParam
deriving (Int -> TVar -> ShowS
[TVar] -> ShowS
TVar -> String
(Int -> TVar -> ShowS)
-> (TVar -> String) -> ([TVar] -> ShowS) -> Show TVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TVar] -> ShowS
$cshowList :: [TVar] -> ShowS
show :: TVar -> String
$cshow :: TVar -> String
showsPrec :: Int -> TVar -> ShowS
$cshowsPrec :: Int -> TVar -> ShowS
Show, (forall x. TVar -> Rep TVar x)
-> (forall x. Rep TVar x -> TVar) -> Generic TVar
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 -> ()
(TVar -> ()) -> NFData TVar
forall a. (a -> ()) -> NFData a
rnf :: TVar -> ()
$crnf :: TVar -> ()
NFData)
tvInfo :: TVar -> TVarInfo
tvInfo :: TVar -> TVarInfo
tvInfo tv :: TVar
tv =
case TVar
tv of
TVFree _ _ _ d :: TVarInfo
d -> TVarInfo
d
TVBound tp :: TParam
tp -> TParam -> TVarInfo
tpInfo TParam
tp
data TVarInfo = TVarInfo { TVarInfo -> Range
tvarSource :: Range
, TVarInfo -> TVarSource
tvarDesc :: TVarSource
}
deriving (Int -> TVarInfo -> ShowS
[TVarInfo] -> ShowS
TVarInfo -> String
(Int -> TVarInfo -> ShowS)
-> (TVarInfo -> String) -> ([TVarInfo] -> ShowS) -> Show TVarInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TVarInfo] -> ShowS
$cshowList :: [TVarInfo] -> ShowS
show :: TVarInfo -> String
$cshow :: TVarInfo -> String
showsPrec :: Int -> TVarInfo -> ShowS
$cshowsPrec :: Int -> TVarInfo -> ShowS
Show, (forall x. TVarInfo -> Rep TVarInfo x)
-> (forall x. Rep TVarInfo x -> TVarInfo) -> Generic TVarInfo
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 -> ()
(TVarInfo -> ()) -> NFData TVarInfo
forall a. (a -> ()) -> NFData a
rnf :: TVarInfo -> ()
$crnf :: TVarInfo -> ()
NFData)
data TVarSource = TVFromModParam Name
| TVFromSignature Name
| TypeWildCard
| TypeOfRecordField Ident
| TypeOfTupleField Int
| TypeOfSeqElement
| LenOfSeq
| TypeParamInstNamed Name Ident
| TypeParamInstPos Name Int
| DefinitionOf Name
| LenOfCompGen
| TypeOfArg (Maybe Int)
| TypeOfRes
| TypeErrorPlaceHolder
deriving (Int -> TVarSource -> ShowS
[TVarSource] -> ShowS
TVarSource -> String
(Int -> TVarSource -> ShowS)
-> (TVarSource -> String)
-> ([TVarSource] -> ShowS)
-> Show TVarSource
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TVarSource] -> ShowS
$cshowList :: [TVarSource] -> ShowS
show :: TVarSource -> String
$cshow :: TVarSource -> String
showsPrec :: Int -> TVarSource -> ShowS
$cshowsPrec :: Int -> TVarSource -> ShowS
Show, (forall x. TVarSource -> Rep TVarSource x)
-> (forall x. Rep TVarSource x -> TVarSource) -> Generic TVarSource
forall x. Rep TVarSource x -> TVarSource
forall x. TVarSource -> Rep TVarSource x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TVarSource x -> TVarSource
$cfrom :: forall x. TVarSource -> Rep TVarSource x
Generic, TVarSource -> ()
(TVarSource -> ()) -> NFData TVarSource
forall a. (a -> ()) -> NFData a
rnf :: TVarSource -> ()
$crnf :: TVarSource -> ()
NFData)
tvSourceName :: TVarSource -> Maybe Name
tvSourceName :: TVarSource -> Maybe Name
tvSourceName tvs :: TVarSource
tvs =
case TVarSource
tvs of
TVFromModParam x :: Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
TVFromSignature x :: Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
TypeParamInstNamed x :: Name
x _ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
TypeParamInstPos x :: Name
x _ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
DefinitionOf x :: Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
_ -> Maybe Name
forall a. Maybe a
Nothing
type Prop = Type
data TySyn = TySyn { TySyn -> Name
tsName :: Name
, TySyn -> [TParam]
tsParams :: [TParam]
, TySyn -> [Prop]
tsConstraints :: [Prop]
, TySyn -> Prop
tsDef :: Type
, TySyn -> Maybe String
tsDoc :: !(Maybe String)
}
deriving (Int -> TySyn -> ShowS
[TySyn] -> ShowS
TySyn -> String
(Int -> TySyn -> ShowS)
-> (TySyn -> String) -> ([TySyn] -> ShowS) -> Show TySyn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TySyn] -> ShowS
$cshowList :: [TySyn] -> ShowS
show :: TySyn -> String
$cshow :: TySyn -> String
showsPrec :: Int -> TySyn -> ShowS
$cshowsPrec :: Int -> TySyn -> ShowS
Show, (forall x. TySyn -> Rep TySyn x)
-> (forall x. Rep TySyn x -> TySyn) -> Generic TySyn
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 -> ()
(TySyn -> ()) -> NFData TySyn
forall a. (a -> ()) -> NFData a
rnf :: TySyn -> ()
$crnf :: TySyn -> ()
NFData)
data Newtype = Newtype { Newtype -> Name
ntName :: Name
, Newtype -> [TParam]
ntParams :: [TParam]
, Newtype -> [Prop]
ntConstraints :: [Prop]
, Newtype -> [(Ident, Prop)]
ntFields :: [(Ident,Type)]
, Newtype -> Maybe String
ntDoc :: Maybe String
} deriving (Int -> Newtype -> ShowS
[Newtype] -> ShowS
Newtype -> String
(Int -> Newtype -> ShowS)
-> (Newtype -> String) -> ([Newtype] -> ShowS) -> Show Newtype
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Newtype] -> ShowS
$cshowList :: [Newtype] -> ShowS
show :: Newtype -> String
$cshow :: Newtype -> String
showsPrec :: Int -> Newtype -> ShowS
$cshowsPrec :: Int -> Newtype -> ShowS
Show, (forall x. Newtype -> Rep Newtype x)
-> (forall x. Rep Newtype x -> Newtype) -> Generic Newtype
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 -> ()
(Newtype -> ()) -> NFData Newtype
forall a. (a -> ()) -> NFData a
rnf :: Newtype -> ()
$crnf :: Newtype -> ()
NFData)
data AbstractType = AbstractType
{ AbstractType -> Name
atName :: Name
, AbstractType -> Kind
atKind :: Kind
, AbstractType -> ([TParam], [Prop])
atCtrs :: ([TParam], [Prop])
, AbstractType -> Maybe Fixity
atFixitiy :: Maybe Fixity
, AbstractType -> Maybe String
atDoc :: Maybe String
} deriving (Int -> AbstractType -> ShowS
[AbstractType] -> ShowS
AbstractType -> String
(Int -> AbstractType -> ShowS)
-> (AbstractType -> String)
-> ([AbstractType] -> ShowS)
-> Show AbstractType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AbstractType] -> ShowS
$cshowList :: [AbstractType] -> ShowS
show :: AbstractType -> String
$cshow :: AbstractType -> String
showsPrec :: Int -> AbstractType -> ShowS
$cshowsPrec :: Int -> AbstractType -> ShowS
Show, (forall x. AbstractType -> Rep AbstractType x)
-> (forall x. Rep AbstractType x -> AbstractType)
-> Generic AbstractType
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 -> ()
(AbstractType -> ()) -> NFData AbstractType
forall a. (a -> ()) -> NFData a
rnf :: AbstractType -> ()
$crnf :: AbstractType -> ()
NFData)
instance HasKind TVar where
kindOf :: TVar -> Kind
kindOf (TVFree _ k :: Kind
k _ _) = Kind
k
kindOf (TVBound tp :: TParam
tp) = TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf TParam
tp
instance HasKind Type where
kindOf :: Prop -> Kind
kindOf ty :: Prop
ty =
case Prop
ty of
TVar a :: TVar
a -> TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
a
TCon c :: TCon
c ts :: [Prop]
ts -> Kind -> [Prop] -> Kind
forall a. Kind -> [a] -> Kind
quickApply (TCon -> Kind
forall t. HasKind t => t -> Kind
kindOf TCon
c) [Prop]
ts
TUser _ _ t :: Prop
t -> Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t
TRec {} -> Kind
KType
instance HasKind TySyn where
kindOf :: TySyn -> Kind
kindOf ts :: TySyn
ts = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) (Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf (TySyn -> Prop
tsDef TySyn
ts)) ((TParam -> Kind) -> [TParam] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf (TySyn -> [TParam]
tsParams TySyn
ts))
instance HasKind Newtype where
kindOf :: Newtype -> Kind
kindOf nt :: Newtype
nt = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) Kind
KType ((TParam -> Kind) -> [TParam] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf (Newtype -> [TParam]
ntParams Newtype
nt))
instance HasKind TParam where
kindOf :: TParam -> Kind
kindOf p :: TParam
p = TParam -> Kind
tpKind TParam
p
quickApply :: Kind -> [a] -> Kind
quickApply :: Kind -> [a] -> Kind
quickApply k :: Kind
k [] = Kind
k
quickApply (_ :-> k :: Kind
k) (_ : ts :: [a]
ts) = Kind -> [a] -> Kind
forall a. Kind -> [a] -> Kind
quickApply Kind
k [a]
ts
quickApply k :: Kind
k _ = String -> [String] -> Kind
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.TypeCheck.AST.quickApply"
[ "Applying a non-function kind:", Kind -> String
forall a. Show a => a -> String
show Kind
k ]
kindResult :: Kind -> Kind
kindResult :: Kind -> Kind
kindResult (_ :-> k :: Kind
k) = Kind -> Kind
kindResult Kind
k
kindResult k :: Kind
k = Kind
k
instance Eq Type where
TUser _ _ x :: Prop
x == :: Prop -> Prop -> Bool
== y :: Prop
y = Prop
x Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
y
x :: Prop
x == TUser _ _ y :: Prop
y = Prop
y Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
x
TCon x :: TCon
x xs :: [Prop]
xs == TCon y :: TCon
y ys :: [Prop]
ys = TCon
x TCon -> TCon -> Bool
forall a. Eq a => a -> a -> Bool
== TCon
y Bool -> Bool -> Bool
&& [Prop]
xs [Prop] -> [Prop] -> Bool
forall a. Eq a => a -> a -> Bool
== [Prop]
ys
TVar x :: TVar
x == TVar y :: TVar
y = TVar
x TVar -> TVar -> Bool
forall a. Eq a => a -> a -> Bool
== TVar
y
TRec xs :: [(Ident, Prop)]
xs == TRec ys :: [(Ident, Prop)]
ys = [(Ident, Prop)] -> [(Ident, Prop)]
forall b. [(Ident, b)] -> [(Ident, b)]
norm [(Ident, Prop)]
xs [(Ident, Prop)] -> [(Ident, Prop)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(Ident, Prop)] -> [(Ident, Prop)]
forall b. [(Ident, b)] -> [(Ident, b)]
norm [(Ident, Prop)]
ys
where norm :: [(Ident, b)] -> [(Ident, b)]
norm = ((Ident, b) -> (Ident, b) -> Ordering)
-> [(Ident, b)] -> [(Ident, b)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Ident, b) -> Ident) -> (Ident, b) -> (Ident, b) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Ident, b) -> Ident
forall a b. (a, b) -> a
fst)
_ == _ = Bool
False
instance Ord Type where
compare :: Prop -> Prop -> Ordering
compare x0 :: Prop
x0 y0 :: Prop
y0 =
case (Prop
x0,Prop
y0) of
(TUser _ _ t :: Prop
t, _) -> Prop -> Prop -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Prop
t Prop
y0
(_, TUser _ _ t :: Prop
t) -> Prop -> Prop -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Prop
x0 Prop
t
(TVar x :: TVar
x, TVar y :: TVar
y) -> TVar -> TVar -> Ordering
forall a. Ord a => a -> a -> Ordering
compare TVar
x TVar
y
(TVar {}, _) -> Ordering
LT
(_, TVar {}) -> Ordering
GT
(TCon x :: TCon
x xs :: [Prop]
xs, TCon y :: TCon
y ys :: [Prop]
ys) -> (TCon, [Prop]) -> (TCon, [Prop]) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (TCon
x,[Prop]
xs) (TCon
y,[Prop]
ys)
(TCon {}, _) -> Ordering
LT
(_,TCon {}) -> Ordering
GT
(TRec xs :: [(Ident, Prop)]
xs, TRec ys :: [(Ident, Prop)]
ys) -> [(Ident, Prop)] -> [(Ident, Prop)] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([(Ident, Prop)] -> [(Ident, Prop)]
forall b. [(Ident, b)] -> [(Ident, b)]
norm [(Ident, Prop)]
xs) ([(Ident, Prop)] -> [(Ident, Prop)]
forall b. [(Ident, b)] -> [(Ident, b)]
norm [(Ident, Prop)]
ys)
where norm :: [(Ident, b)] -> [(Ident, b)]
norm = ((Ident, b) -> (Ident, b) -> Ordering)
-> [(Ident, b)] -> [(Ident, b)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Ident, b) -> Ident) -> (Ident, b) -> (Ident, b) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Ident, b) -> Ident
forall a b. (a, b) -> a
fst)
instance Eq TParam where
x :: TParam
x == :: TParam -> TParam -> Bool
== y :: TParam
y = TParam -> Int
tpUnique TParam
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== TParam -> Int
tpUnique TParam
y
instance Ord TParam where
compare :: TParam -> TParam -> Ordering
compare x :: TParam
x y :: TParam
y = Int -> Int -> Ordering
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 p :: TParam
p = TParam -> TVar
TVBound TParam
p
type SType = Type
newtypeConType :: Newtype -> Schema
newtypeConType :: Newtype -> Schema
newtypeConType nt :: Newtype
nt =
[TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as (Newtype -> [Prop]
ntConstraints Newtype
nt)
(Prop -> Schema) -> Prop -> Schema
forall a b. (a -> b) -> a -> b
$ [(Ident, Prop)] -> Prop
TRec (Newtype -> [(Ident, Prop)]
ntFields Newtype
nt) Prop -> Prop -> Prop
`tFun` TCon -> [Prop] -> Prop
TCon (Newtype -> TCon
newtypeTyCon Newtype
nt) ((TParam -> Prop) -> [TParam] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Prop
TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
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 at :: AbstractType
at =
case Name -> Maybe TCon
builtInType (AbstractType -> Name
atName AbstractType
at) of
Just tcon :: TCon
tcon -> TCon
tcon
_ -> TC -> TCon
TC (TC -> TCon) -> TC -> TCon
forall a b. (a -> b) -> a -> b
$ UserTC -> TC
TCAbstract (UserTC -> TC) -> UserTC -> TC
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 x :: TParam
x == :: TVar -> TVar -> Bool
== TVBound y :: TParam
y = TParam
x TParam -> TParam -> Bool
forall a. Eq a => a -> a -> Bool
== TParam
y
TVFree x :: Int
x _ _ _ == TVFree y :: Int
y _ _ _ = Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y
_ == _ = Bool
False
instance Ord TVar where
compare :: TVar -> TVar -> Ordering
compare (TVFree x :: Int
x _ _ _) (TVFree y :: Int
y _ _ _) = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
x Int
y
compare (TVFree _ _ _ _) _ = Ordering
LT
compare _ (TVFree _ _ _ _) = Ordering
GT
compare (TVBound x :: TParam
x) (TVBound y :: TParam
y) = TParam -> TParam -> Ordering
forall a. Ord a => a -> a -> Ordering
compare TParam
x TParam
y
isFreeTV :: TVar -> Bool
isFreeTV :: TVar -> Bool
isFreeTV (TVFree {}) = Bool
True
isFreeTV _ = Bool
False
isBoundTV :: TVar -> Bool
isBoundTV :: TVar -> Bool
isBoundTV (TVBound {}) = Bool
True
isBoundTV _ = Bool
False
tIsError :: Type -> Maybe TCErrorMessage
tIsError :: Prop -> Maybe TCErrorMessage
tIsError ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TError _ x :: TCErrorMessage
x) _ -> TCErrorMessage -> Maybe TCErrorMessage
forall a. a -> Maybe a
Just TCErrorMessage
x
_ -> Maybe TCErrorMessage
forall a. Maybe a
Nothing
tIsNat' :: Type -> Maybe Nat'
tIsNat' :: Prop -> Maybe Nat'
tIsNat' ty :: Prop
ty =
case Prop -> Prop
tNoUser Prop
ty of
TCon (TC (TCNum x :: Integer
x)) [] -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (Integer -> Nat'
Nat Integer
x)
TCon (TC TCInf) [] -> Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
_ -> Maybe Nat'
forall a. Maybe a
Nothing
tIsNum :: Type -> Maybe Integer
tIsNum :: Prop -> Maybe Integer
tIsNum ty :: Prop
ty = do Nat x :: Integer
x <- Prop -> Maybe Nat'
tIsNat' Prop
ty
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x
tIsInf :: Type -> Bool
tIsInf :: Prop -> Bool
tIsInf ty :: Prop
ty = Prop -> Maybe Nat'
tIsNat' Prop
ty Maybe Nat' -> Maybe Nat' -> Bool
forall a. Eq a => a -> a -> Bool
== Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just Nat'
Inf
tIsVar :: Type -> Maybe TVar
tIsVar :: Prop -> Maybe TVar
tIsVar ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TVar x :: TVar
x -> TVar -> Maybe TVar
forall a. a -> Maybe a
Just TVar
x
_ -> Maybe TVar
forall a. Maybe a
Nothing
tIsFun :: Type -> Maybe (Type, Type)
tIsFun :: Prop -> Maybe (Prop, Prop)
tIsFun ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TC TCFun) [a :: Prop
a, b :: Prop
b] -> (Prop, Prop) -> Maybe (Prop, Prop)
forall a. a -> Maybe a
Just (Prop
a, Prop
b)
_ -> Maybe (Prop, Prop)
forall a. Maybe a
Nothing
tIsSeq :: Type -> Maybe (Type, Type)
tIsSeq :: Prop -> Maybe (Prop, Prop)
tIsSeq ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TC TCSeq) [n :: Prop
n, a :: Prop
a] -> (Prop, Prop) -> Maybe (Prop, Prop)
forall a. a -> Maybe a
Just (Prop
n, Prop
a)
_ -> Maybe (Prop, Prop)
forall a. Maybe a
Nothing
tIsBit :: Type -> Bool
tIsBit :: Prop -> Bool
tIsBit ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TC TCBit) [] -> Bool
True
_ -> Bool
False
tIsInteger :: Type -> Bool
tIsInteger :: Prop -> Bool
tIsInteger ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TC TCInteger) [] -> Bool
True
_ -> Bool
False
tIsIntMod :: Type -> Maybe Type
tIsIntMod :: Prop -> Maybe Prop
tIsIntMod ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TC TCIntMod) [n :: Prop
n] -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
n
_ -> Maybe Prop
forall a. Maybe a
Nothing
tIsTuple :: Type -> Maybe [Type]
tIsTuple :: Prop -> Maybe [Prop]
tIsTuple ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TC (TCTuple _)) ts :: [Prop]
ts -> [Prop] -> Maybe [Prop]
forall a. a -> Maybe a
Just [Prop]
ts
_ -> Maybe [Prop]
forall a. Maybe a
Nothing
tIsRec :: Type -> Maybe [(Ident, Type)]
tIsRec :: Prop -> Maybe [(Ident, Prop)]
tIsRec ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TRec fs :: [(Ident, Prop)]
fs -> [(Ident, Prop)] -> Maybe [(Ident, Prop)]
forall a. a -> Maybe a
Just [(Ident, Prop)]
fs
_ -> Maybe [(Ident, Prop)]
forall a. Maybe a
Nothing
tIsBinFun :: TFun -> Type -> Maybe (Type,Type)
tIsBinFun :: TFun -> Prop -> Maybe (Prop, Prop)
tIsBinFun f :: TFun
f ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TF g :: TFun
g) [a :: Prop
a,b :: Prop
b] | TFun
f TFun -> TFun -> Bool
forall a. Eq a => a -> a -> Bool
== TFun
g -> (Prop, Prop) -> Maybe (Prop, Prop)
forall a. a -> Maybe a
Just (Prop
a,Prop
b)
_ -> Maybe (Prop, Prop)
forall a. Maybe a
Nothing
tSplitFun :: TFun -> Type -> [Type]
tSplitFun :: TFun -> Prop -> [Prop]
tSplitFun f :: TFun
f t0 :: Prop
t0 = Prop -> [Prop] -> [Prop]
go Prop
t0 []
where go :: Prop -> [Prop] -> [Prop]
go ty :: Prop
ty xs :: [Prop]
xs = case TFun -> Prop -> Maybe (Prop, Prop)
tIsBinFun TFun
f Prop
ty of
Just (a :: Prop
a,b :: Prop
b) -> Prop -> [Prop] -> [Prop]
go Prop
a (Prop -> [Prop] -> [Prop]
go Prop
b [Prop]
xs)
Nothing -> Prop
ty Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
xs
pIsFin :: Prop -> Maybe Type
pIsFin :: Prop -> Maybe Prop
pIsFin ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (PC PFin) [t1 :: Prop
t1] -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t1
_ -> Maybe Prop
forall a. Maybe a
Nothing
pIsGeq :: Prop -> Maybe (Type,Type)
pIsGeq :: Prop -> Maybe (Prop, Prop)
pIsGeq ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (PC PGeq) [t1 :: Prop
t1,t2 :: Prop
t2] -> (Prop, Prop) -> Maybe (Prop, Prop)
forall a. a -> Maybe a
Just (Prop
t1,Prop
t2)
_ -> Maybe (Prop, Prop)
forall a. Maybe a
Nothing
pIsEq :: Prop -> Maybe (Type,Type)
pIsEq :: Prop -> Maybe (Prop, Prop)
pIsEq ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (PC PEqual) [t1 :: Prop
t1,t2 :: Prop
t2] -> (Prop, Prop) -> Maybe (Prop, Prop)
forall a. a -> Maybe a
Just (Prop
t1,Prop
t2)
_ -> Maybe (Prop, Prop)
forall a. Maybe a
Nothing
pIsZero :: Prop -> Maybe Type
pIsZero :: Prop -> Maybe Prop
pIsZero ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (PC PZero) [t1 :: Prop
t1] -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t1
_ -> Maybe Prop
forall a. Maybe a
Nothing
pIsLogic :: Prop -> Maybe Type
pIsLogic :: Prop -> Maybe Prop
pIsLogic ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (PC PLogic) [t1 :: Prop
t1] -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t1
_ -> Maybe Prop
forall a. Maybe a
Nothing
pIsArith :: Prop -> Maybe Type
pIsArith :: Prop -> Maybe Prop
pIsArith ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (PC PArith) [t1 :: Prop
t1] -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t1
_ -> Maybe Prop
forall a. Maybe a
Nothing
pIsCmp :: Prop -> Maybe Type
pIsCmp :: Prop -> Maybe Prop
pIsCmp ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (PC PCmp) [t1 :: Prop
t1] -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t1
_ -> Maybe Prop
forall a. Maybe a
Nothing
pIsSignedCmp :: Prop -> Maybe Type
pIsSignedCmp :: Prop -> Maybe Prop
pIsSignedCmp ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (PC PSignedCmp) [t1 :: Prop
t1] -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t1
_ -> Maybe Prop
forall a. Maybe a
Nothing
pIsLiteral :: Prop -> Maybe (Type, Type)
pIsLiteral :: Prop -> Maybe (Prop, Prop)
pIsLiteral ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (PC PLiteral) [t1 :: Prop
t1, t2 :: Prop
t2] -> (Prop, Prop) -> Maybe (Prop, Prop)
forall a. a -> Maybe a
Just (Prop
t1, Prop
t2)
_ -> Maybe (Prop, Prop)
forall a. Maybe a
Nothing
pIsTrue :: Prop -> Bool
pIsTrue :: Prop -> Bool
pIsTrue ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (PC PTrue) _ -> Bool
True
_ -> Bool
False
pIsWidth :: Prop -> Maybe Type
pIsWidth :: Prop -> Maybe Prop
pIsWidth ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TF TCWidth) [t1 :: Prop
t1] -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t1
_ -> Maybe Prop
forall a. Maybe a
Nothing
tNum :: Integral a => a -> Type
tNum :: a -> Prop
tNum n :: a
n = TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC (Integer -> TC
TCNum (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n))) []
tZero :: Type
tZero :: Prop
tZero = Int -> Prop
forall a. Integral a => a -> Prop
tNum (0 :: Int)
tOne :: Type
tOne :: Prop
tOne = Int -> Prop
forall a. Integral a => a -> Prop
tNum (1 :: Int)
tTwo :: Type
tTwo :: Prop
tTwo = Int -> Prop
forall a. Integral a => a -> Prop
tNum (2 :: Int)
tInf :: Type
tInf :: Prop
tInf = TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC TC
TCInf) []
tNat' :: Nat' -> Type
tNat' :: Nat' -> Prop
tNat' n' :: Nat'
n' = case Nat'
n' of
Inf -> Prop
tInf
Nat n :: Integer
n -> Integer -> Prop
forall a. Integral a => a -> Prop
tNum Integer
n
tAbstract :: UserTC -> [Type] -> Type
tAbstract :: UserTC -> [Prop] -> Prop
tAbstract u :: UserTC
u ts :: [Prop]
ts = TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC (UserTC -> TC
TCAbstract UserTC
u)) [Prop]
ts
tBit :: Type
tBit :: Prop
tBit = TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC TC
TCBit) []
tInteger :: Type
tInteger :: Prop
tInteger = TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC TC
TCInteger) []
tIntMod :: Type -> Type
tIntMod :: Prop -> Prop
tIntMod n :: Prop
n = TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC TC
TCIntMod) [Prop
n]
tWord :: Type -> Type
tWord :: Prop -> Prop
tWord a :: Prop
a = Prop -> Prop -> Prop
tSeq Prop
a Prop
tBit
tSeq :: Type -> Type -> Type
tSeq :: Prop -> Prop -> Prop
tSeq a :: Prop
a b :: Prop
b = TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC TC
TCSeq) [Prop
a,Prop
b]
tChar :: Type
tChar :: Prop
tChar = Prop -> Prop
tWord (Int -> Prop
forall a. Integral a => a -> Prop
tNum (8 :: Int))
tString :: Int -> Type
tString :: Int -> Prop
tString len :: Int
len = Prop -> Prop -> Prop
tSeq (Int -> Prop
forall a. Integral a => a -> Prop
tNum Int
len) Prop
tChar
tRec :: [(Ident,Type)] -> Type
tRec :: [(Ident, Prop)] -> Prop
tRec = [(Ident, Prop)] -> Prop
TRec
tTuple :: [Type] -> Type
tTuple :: [Prop] -> Prop
tTuple ts :: [Prop]
ts = TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC (Int -> TC
TCTuple ([Prop] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Prop]
ts))) [Prop]
ts
newtypeTyCon :: Newtype -> TCon
newtypeTyCon :: Newtype -> TCon
newtypeTyCon nt :: Newtype
nt = TC -> TCon
TC (TC -> TCon) -> TC -> TCon
forall a b. (a -> b) -> a -> b
$ UserTC -> TC
TCNewtype (UserTC -> TC) -> UserTC -> TC
forall a b. (a -> b) -> a -> b
$ Name -> Kind -> UserTC
UserTC (Newtype -> Name
ntName Newtype
nt) (Newtype -> Kind
forall t. HasKind t => t -> Kind
kindOf Newtype
nt)
tFun :: Type -> Type -> Type
tFun :: Prop -> Prop -> Prop
tFun a :: Prop
a b :: Prop
b = TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC TC
TCFun) [Prop
a,Prop
b]
tNoUser :: Type -> Type
tNoUser :: Prop -> Prop
tNoUser t :: Prop
t = case Prop
t of
TUser _ _ a :: Prop
a -> Prop -> Prop
tNoUser Prop
a
_ -> Prop
t
tBadNumber :: TCErrorMessage -> Type
tBadNumber :: TCErrorMessage -> Prop
tBadNumber = Kind -> TCErrorMessage -> Prop
tError Kind
KNum
tError :: Kind -> TCErrorMessage -> Type
tError :: Kind -> TCErrorMessage -> Prop
tError k :: Kind
k msg :: TCErrorMessage
msg = TCon -> [Prop] -> Prop
TCon (Kind -> TCErrorMessage -> TCon
TError Kind
k TCErrorMessage
msg) []
tf1 :: TFun -> Type -> Type
tf1 :: TFun -> Prop -> Prop
tf1 f :: TFun
f x :: Prop
x = TCon -> [Prop] -> Prop
TCon (TFun -> TCon
TF TFun
f) [Prop
x]
tf2 :: TFun -> Type -> Type -> Type
tf2 :: TFun -> Prop -> Prop -> Prop
tf2 f :: TFun
f x :: Prop
x y :: Prop
y = TCon -> [Prop] -> Prop
TCon (TFun -> TCon
TF TFun
f) [Prop
x,Prop
y]
tf3 :: TFun -> Type -> Type -> Type -> Type
tf3 :: TFun -> Prop -> Prop -> Prop -> Prop
tf3 f :: TFun
f x :: Prop
x y :: Prop
y z :: Prop
z = TCon -> [Prop] -> Prop
TCon (TFun -> TCon
TF TFun
f) [Prop
x,Prop
y,Prop
z]
tSub :: Type -> Type -> Type
tSub :: Prop -> Prop -> Prop
tSub = TFun -> Prop -> Prop -> Prop
tf2 TFun
TCSub
tMul :: Type -> Type -> Type
tMul :: Prop -> Prop -> Prop
tMul = TFun -> Prop -> Prop -> Prop
tf2 TFun
TCMul
tDiv :: Type -> Type -> Type
tDiv :: Prop -> Prop -> Prop
tDiv = TFun -> Prop -> Prop -> Prop
tf2 TFun
TCDiv
tMod :: Type -> Type -> Type
tMod :: Prop -> Prop -> Prop
tMod = TFun -> Prop -> Prop -> Prop
tf2 TFun
TCMod
tExp :: Type -> Type -> Type
tExp :: Prop -> Prop -> Prop
tExp = TFun -> Prop -> Prop -> Prop
tf2 TFun
TCExp
tMin :: Type -> Type -> Type
tMin :: Prop -> Prop -> Prop
tMin = TFun -> Prop -> Prop -> Prop
tf2 TFun
TCMin
tCeilDiv :: Type -> Type -> Type
tCeilDiv :: Prop -> Prop -> Prop
tCeilDiv = TFun -> Prop -> Prop -> Prop
tf2 TFun
TCCeilDiv
tCeilMod :: Type -> Type -> Type
tCeilMod :: Prop -> Prop -> Prop
tCeilMod = TFun -> Prop -> Prop -> Prop
tf2 TFun
TCCeilMod
tLenFromThenTo :: Type -> Type -> Type -> Type
tLenFromThenTo :: Prop -> Prop -> Prop -> Prop
tLenFromThenTo = TFun -> Prop -> Prop -> Prop -> Prop
tf3 TFun
TCLenFromThenTo
(=#=) :: Type -> Type -> Prop
x :: Prop
x =#= :: Prop -> Prop -> Prop
=#= y :: Prop
y = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PEqual) [Prop
x,Prop
y]
(=/=) :: Type -> Type -> Prop
x :: Prop
x =/= :: Prop -> Prop -> Prop
=/= y :: Prop
y = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PNeq) [Prop
x,Prop
y]
pZero :: Type -> Prop
pZero :: Prop -> Prop
pZero t :: Prop
t = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PZero) [Prop
t]
pLogic :: Type -> Prop
pLogic :: Prop -> Prop
pLogic t :: Prop
t = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PLogic) [Prop
t]
pArith :: Type -> Prop
pArith :: Prop -> Prop
pArith t :: Prop
t = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PArith) [Prop
t]
pCmp :: Type -> Prop
pCmp :: Prop -> Prop
pCmp t :: Prop
t = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PCmp) [Prop
t]
pSignedCmp :: Type -> Prop
pSignedCmp :: Prop -> Prop
pSignedCmp t :: Prop
t = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PSignedCmp) [Prop
t]
pLiteral :: Type -> Type -> Prop
pLiteral :: Prop -> Prop -> Prop
pLiteral x :: Prop
x y :: Prop
y = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PLiteral) [Prop
x, Prop
y]
(>==) :: Type -> Type -> Prop
x :: Prop
x >== :: Prop -> Prop -> Prop
>== y :: Prop
y = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PGeq) [Prop
x,Prop
y]
pHas :: Selector -> Type -> Type -> Prop
pHas :: Selector -> Prop -> Prop -> Prop
pHas l :: Selector
l ty :: Prop
ty fi :: Prop
fi = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC (Selector -> PC
PHas Selector
l)) [Prop
ty,Prop
fi]
pTrue :: Prop
pTrue :: Prop
pTrue = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PTrue) []
pAnd :: [Prop] -> Prop
pAnd :: [Prop] -> Prop
pAnd [] = Prop
pTrue
pAnd [x :: Prop
x] = Prop
x
pAnd (x :: Prop
x : xs :: [Prop]
xs)
| Just _ <- Prop -> Maybe TCErrorMessage
tIsError Prop
x = Prop
x
| Prop -> Bool
pIsTrue Prop
x = Prop
rest
| Just _ <- Prop -> Maybe TCErrorMessage
tIsError Prop
rest = Prop
rest
| Prop -> Bool
pIsTrue Prop
rest = Prop
x
| Bool
otherwise = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PAnd) [Prop
x, Prop
rest]
where rest :: Prop
rest = [Prop] -> Prop
pAnd [Prop]
xs
pSplitAnd :: Prop -> [Prop]
pSplitAnd :: Prop -> [Prop]
pSplitAnd p0 :: Prop
p0 = [Prop] -> [Prop]
go [Prop
p0]
where
go :: [Prop] -> [Prop]
go [] = []
go (q :: Prop
q : qs :: [Prop]
qs) =
case Prop -> Prop
tNoUser Prop
q of
TCon (PC PAnd) [l :: Prop
l,r :: Prop
r] -> [Prop] -> [Prop]
go (Prop
l Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: Prop
r Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
qs)
TCon (PC PTrue) _ -> [Prop] -> [Prop]
go [Prop]
qs
_ -> Prop
q Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop] -> [Prop]
go [Prop]
qs
pFin :: Type -> Prop
pFin :: Prop -> Prop
pFin ty :: Prop
ty =
case Prop -> Prop
tNoUser Prop
ty of
TCon (TC (TCNum _)) _ -> Prop
pTrue
TCon (TC TCInf) _ -> TCErrorMessage -> Prop
pError (String -> TCErrorMessage
TCErrorMessage "`inf` is not finite.")
_ -> TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
PFin) [Prop
ty]
pError :: TCErrorMessage -> Prop
pError :: TCErrorMessage -> Prop
pError msg :: TCErrorMessage
msg = TCon -> [Prop] -> Prop
TCon (Kind -> TCErrorMessage -> TCon
TError Kind
KProp TCErrorMessage
msg) []
noFreeVariables :: FVS t => t -> Bool
noFreeVariables :: t -> Bool
noFreeVariables = (TVar -> Bool) -> [TVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (TVar -> Bool) -> TVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TVar -> Bool
isFreeTV) ([TVar] -> Bool) -> (t -> [TVar]) -> t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> [TVar]) -> (t -> Set TVar) -> t -> [TVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Set TVar
forall t. FVS t => t -> Set TVar
fvs
class FVS t where
fvs :: t -> Set TVar
instance FVS Type where
fvs :: Prop -> Set TVar
fvs = Prop -> Set TVar
go
where
go :: Prop -> Set TVar
go ty :: Prop
ty =
case Prop
ty of
TCon _ ts :: [Prop]
ts -> [Prop] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Prop]
ts
TVar x :: TVar
x -> TVar -> Set TVar
forall a. a -> Set a
Set.singleton TVar
x
TUser _ _ t :: Prop
t -> Prop -> Set TVar
go Prop
t
TRec fs :: [(Ident, Prop)]
fs -> [Prop] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (((Ident, Prop) -> Prop) -> [(Ident, Prop)] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Prop) -> Prop
forall a b. (a, b) -> b
snd [(Ident, Prop)]
fs)
instance FVS a => FVS (Maybe a) where
fvs :: Maybe a -> Set TVar
fvs Nothing = Set TVar
forall a. Set a
Set.empty
fvs (Just x :: a
x) = a -> Set TVar
forall t. FVS t => t -> Set TVar
fvs a
x
instance FVS a => FVS [a] where
fvs :: [a] -> Set TVar
fvs xs :: [a]
xs = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((a -> Set TVar) -> [a] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map a -> Set TVar
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 (x :: a
x,y :: b
y) = Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union (a -> Set TVar
forall t. FVS t => t -> Set TVar
fvs a
x) (b -> Set TVar
forall t. FVS t => t -> Set TVar
fvs b
y)
instance FVS Schema where
fvs :: Schema -> Set TVar
fvs (Forall as :: [TParam]
as ps :: [Prop]
ps t :: Prop
t) =
Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([Prop] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Prop]
ps) (Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Prop
t)) Set TVar
bound
where bound :: Set TVar
bound = [TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as)
instance PP TParam where
ppPrec :: Int -> TParam -> Doc
ppPrec = NameMap -> Int -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty
instance PP (WithNames TParam) where
ppPrec :: Int -> WithNames TParam -> Doc
ppPrec _ (WithNames p :: TParam
p mp :: NameMap
mp) = NameMap -> TVar -> Doc
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 as :: [TParam]
as ns :: NameMap
ns = ((Int, String) -> NameMap -> NameMap)
-> NameMap -> [(Int, String)] -> NameMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Int -> String -> NameMap -> NameMap)
-> (Int, String) -> NameMap -> NameMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> String -> NameMap -> NameMap
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert) NameMap
ns
([(Int, String)] -> NameMap) -> [(Int, String)] -> NameMap
forall a b. (a -> b) -> a -> b
$ [(Int, String)]
named [(Int, String)] -> [(Int, String)] -> [(Int, String)]
forall a. [a] -> [a] -> [a]
++ [Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
unnamed_nums [String]
numNames
[(Int, String)] -> [(Int, String)] -> [(Int, String)]
forall a. [a] -> [a] -> [a]
++ [Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
unnamed_vals [String]
valNames
where avail :: [String] -> [String]
avail xs :: [String]
xs = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
used) ([String] -> [String]
nameList [String]
xs)
numNames :: [String]
numNames = [String] -> [String]
avail ["n","m","i","j","k"]
valNames :: [String]
valNames = [String] -> [String]
avail ["a","b","c","d","e"]
nm :: TParam -> (Int, Maybe Name, Kind)
nm x :: TParam
x = (TParam -> Int
tpUnique TParam
x, TParam -> Maybe Name
tpName TParam
x, TParam -> Kind
tpKind TParam
x)
named :: [(Int, String)]
named = [ (Int
u,Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
n)) | (u :: Int
u,Just n :: Name
n,_) <- (TParam -> (Int, Maybe Name, Kind))
-> [TParam] -> [(Int, Maybe Name, Kind)]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> (Int, Maybe Name, Kind)
nm [TParam]
as ]
unnamed_nums :: [Int]
unnamed_nums = [ Int
u | (u :: Int
u,Nothing,KNum) <- (TParam -> (Int, Maybe Name, Kind))
-> [TParam] -> [(Int, Maybe Name, Kind)]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> (Int, Maybe Name, Kind)
nm [TParam]
as ]
unnamed_vals :: [Int]
unnamed_vals = [ Int
u | (u :: Int
u,Nothing,KType) <- (TParam -> (Int, Maybe Name, Kind))
-> [TParam] -> [(Int, Maybe Name, Kind)]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> (Int, Maybe Name, Kind)
nm [TParam]
as ]
used :: [String]
used = ((Int, String) -> String) -> [(Int, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, String) -> String
forall a b. (a, b) -> b
snd [(Int, String)]
named [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ NameMap -> [String]
forall a. IntMap a -> [a]
IntMap.elems NameMap
ns
ppNewtypeShort :: Newtype -> Doc
ppNewtypeShort :: Newtype -> Doc
ppNewtypeShort nt :: Newtype
nt =
String -> Doc
text "newtype" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp (Newtype -> Name
ntName Newtype
nt) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ((TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Int -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm 9) [TParam]
ps)
where
ps :: [TParam]
ps = Newtype -> [TParam]
ntParams Newtype
nt
nm :: NameMap
nm = [TParam] -> NameMap -> NameMap
addTNames [TParam]
ps NameMap
emptyNameMap
instance PP Schema where
ppPrec :: Int -> Schema -> Doc
ppPrec = NameMap -> Int -> Schema -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty
instance PP (WithNames Schema) where
ppPrec :: Int -> WithNames Schema -> Doc
ppPrec _ (WithNames s :: Schema
s ns :: NameMap
ns)
| [TParam] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [TParam]
sVars Schema
s) Bool -> Bool -> Bool
&& [Prop] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [Prop]
sProps Schema
s) = Doc
body
| Bool
otherwise = Doc -> Int -> Doc -> Doc
hang (Doc
vars Doc -> Doc -> Doc
<+> Doc
props) 2 Doc
body
where
body :: Doc
body = NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 (Schema -> Prop
sType Schema
s)
vars :: Doc
vars = case Schema -> [TParam]
sVars Schema
s of
[] -> Doc
empty
vs :: [TParam]
vs -> Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
commaSep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [TParam]
vs
props :: Doc
props = case Schema -> [Prop]
sProps Schema
s of
[] -> Doc
empty
ps :: [Prop]
ps -> Doc -> Doc
parens ([Doc] -> Doc
commaSep ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [Prop]
ps)) Doc -> Doc -> Doc
<+> String -> Doc
text "=>"
ns1 :: NameMap
ns1 = [TParam] -> NameMap -> NameMap
addTNames (Schema -> [TParam]
sVars Schema
s) NameMap
ns
instance PP TySyn where
ppPrec :: Int -> TySyn -> Doc
ppPrec = NameMap -> Int -> TySyn -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty
instance PP (WithNames TySyn) where
ppPrec :: Int -> WithNames TySyn -> Doc
ppPrec _ (WithNames ts :: TySyn
ts ns :: NameMap
ns) =
String -> Doc
text "type" Doc -> Doc -> Doc
<+> Doc
ctr Doc -> Doc -> Doc
<+> Doc
lhs Doc -> Doc -> Doc
<+> Char -> Doc
char '=' Doc -> Doc -> Doc
<+> NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 (TySyn -> Prop
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 (TySyn -> Kind
forall t. HasKind t => t -> Kind
kindOf TySyn
ts) of
KProp -> String -> Doc
text "constraint"
_ -> Doc
empty
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 _, [x :: TParam
x, y :: TParam
y]) ->
NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 TParam
x Doc -> Doc -> Doc
<+> Ident -> Doc
forall a. PP a => a -> Doc
pp (Name -> Ident
nameIdent Name
n) Doc -> Doc -> Doc
<+> NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 TParam
y
(_, ps :: [TParam]
ps) ->
Name -> Doc
forall a. PP a => a -> Doc
pp Name
n Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep ((TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [TParam]
ps)
instance PP Newtype where
ppPrec :: Int -> Newtype -> Doc
ppPrec = NameMap -> Int -> Newtype -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty
instance PP (WithNames Newtype) where
ppPrec :: Int -> WithNames Newtype -> Doc
ppPrec _ (WithNames nt :: Newtype
nt _) = Newtype -> Doc
ppNewtypeShort Newtype
nt
instance PP (WithNames Type) where
ppPrec :: Int -> WithNames Prop -> Doc
ppPrec prec :: Int
prec ty0 :: WithNames Prop
ty0@(WithNames ty :: Prop
ty nmMap :: NameMap
nmMap) =
case Prop
ty of
TVar a :: TVar
a -> NameMap -> TVar -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nmMap TVar
a
TRec fs :: [(Ident, Prop)]
fs -> Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma
[ Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
l Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t | (l :: Ident
l,t :: Prop
t) <- [(Ident, Prop)]
fs ]
_ | Just tinf :: Infix Ident (WithNames Prop)
tinf <- WithNames Prop -> Maybe (Infix Ident (WithNames Prop))
isTInfix WithNames Prop
ty0 -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 2)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int
-> (WithNames Prop -> Maybe (Infix Ident (WithNames Prop)))
-> Infix Ident (WithNames Prop)
-> Doc
forall thing op.
(PP thing, PP op) =>
Int -> (thing -> Maybe (Infix op thing)) -> Infix op thing -> Doc
ppInfix 2 WithNames Prop -> Maybe (Infix Ident (WithNames Prop))
isTInfix Infix Ident (WithNames Prop)
tinf
TUser c :: Name
c [] _ -> Name -> Doc
forall a. PP a => a -> Doc
pp Name
c
TUser c :: Name
c ts :: [Prop]
ts _ -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. PP a => a -> Doc
pp Name
c Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4) [Prop]
ts)
TCon (TC tc :: TC
tc) ts :: [Prop]
ts ->
case (TC
tc,[Prop]
ts) of
(TCNum n :: Integer
n, []) -> Integer -> Doc
integer Integer
n
(TCInf, []) -> String -> Doc
text "inf"
(TCBit, []) -> String -> Doc
text "Bit"
(TCInteger, []) -> String -> Doc
text "Integer"
(TCIntMod, [n :: Prop
n]) -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "Z" Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4 Prop
n
(TCSeq, [t1 :: Prop
t1,TCon (TC TCBit) []]) -> Doc -> Doc
brackets (Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t1)
(TCSeq, [t1 :: Prop
t1,t2 :: Prop
t2]) -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets (Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t1) Doc -> Doc -> Doc
<.> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 3 Prop
t2
(TCFun, [t1 :: Prop
t1,t2 :: Prop
t2]) -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 2 Prop
t1 Doc -> Doc -> Doc
<+> String -> Doc
text "->" Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 1 Prop
t2
(TCTuple _, fs :: [Prop]
fs) -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0) [Prop]
fs
(_, _) -> TC -> Doc
forall a. PP a => a -> Doc
pp TC
tc Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4) [Prop]
ts)
TCon (PC pc :: PC
pc) ts :: [Prop]
ts ->
case (PC
pc,[Prop]
ts) of
(PEqual, [t1 :: Prop
t1,t2 :: Prop
t2]) -> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t1 Doc -> Doc -> Doc
<+> String -> Doc
text "==" Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t2
(PNeq , [t1 :: Prop
t1,t2 :: Prop
t2]) -> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t1 Doc -> Doc -> Doc
<+> String -> Doc
text "!=" Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t2
(PGeq, [t1 :: Prop
t1,t2 :: Prop
t2]) -> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t1 Doc -> Doc -> Doc
<+> String -> Doc
text ">=" Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t2
(PFin, [t1 :: Prop
t1]) -> String -> Doc
text "fin" Doc -> Doc -> Doc
<+> (Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4 Prop
t1)
(PHas x :: Selector
x, [t1 :: Prop
t1,t2 :: Prop
t2]) -> Selector -> Doc
ppSelector Selector
x Doc -> Doc -> Doc
<+> String -> Doc
text "of"
Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t1 Doc -> Doc -> Doc
<+> String -> Doc
text "is" Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 0 Prop
t2
(PArith, [t1 :: Prop
t1]) -> PC -> Doc
forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4 Prop
t1
(PCmp, [t1 :: Prop
t1]) -> PC -> Doc
forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4 Prop
t1
(PSignedCmp, [t1 :: Prop
t1]) -> PC -> Doc
forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4 Prop
t1
(PLiteral, [t1 :: Prop
t1,t2 :: Prop
t2]) -> PC -> Doc
forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4 Prop
t1 Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4 Prop
t2
(_, _) -> PC -> Doc
forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4) [Prop]
ts)
TCon f :: TCon
f ts :: [Prop]
ts -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TCon -> Doc
forall a. PP a => a -> Doc
pp TCon
f Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go 4) [Prop]
ts)
where
go :: Int -> a -> Doc
go p :: Int
p t :: a
t = NameMap -> Int -> a -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nmMap Int
p a
t
isTInfix :: WithNames Prop -> Maybe (Infix Ident (WithNames Prop))
isTInfix (WithNames (TCon tc :: TCon
tc [ieLeft' :: Prop
ieLeft',ieRight' :: Prop
ieRight']) _) =
do let ieLeft :: WithNames Prop
ieLeft = Prop -> NameMap -> WithNames Prop
forall a. a -> NameMap -> WithNames a
WithNames Prop
ieLeft' NameMap
nmMap
ieRight :: WithNames Prop
ieRight = Prop -> NameMap -> WithNames Prop
forall a. a -> NameMap -> WithNames a
WithNames Prop
ieRight' NameMap
nmMap
(ieOp :: Ident
ieOp,fi :: Fixity
fi) <- TCon -> Maybe (Ident, Fixity)
infixPrimTy TCon
tc
let ieAssoc :: Assoc
ieAssoc = Fixity -> Assoc
fAssoc Fixity
fi
iePrec :: Int
iePrec = Fixity -> Int
fLevel Fixity
fi
Infix Ident (WithNames Prop)
-> Maybe (Infix Ident (WithNames Prop))
forall (m :: * -> *) a. Monad m => a -> m a
return Infix :: forall op thing.
op -> thing -> thing -> Int -> Assoc -> Infix op thing
Infix { .. }
isTInfix (WithNames (TUser n :: Name
n [ieLeft' :: Prop
ieLeft',ieRight' :: Prop
ieRight'] _) _) =
do let ieLeft :: WithNames Prop
ieLeft = Prop -> NameMap -> WithNames Prop
forall a. a -> NameMap -> WithNames a
WithNames Prop
ieLeft' NameMap
nmMap
ieRight :: WithNames Prop
ieRight = Prop -> NameMap -> WithNames Prop
forall a. a -> NameMap -> WithNames a
WithNames Prop
ieRight' NameMap
nmMap
Fixity
fi <- Name -> Maybe Fixity
nameFixity Name
n
let ieAssoc :: Assoc
ieAssoc = Fixity -> Assoc
fAssoc Fixity
fi
iePrec :: Int
iePrec = Fixity -> Int
fLevel Fixity
fi
ieOp :: Ident
ieOp = Name -> Ident
nameIdent Name
n
Infix Ident (WithNames Prop)
-> Maybe (Infix Ident (WithNames Prop))
forall (m :: * -> *) a. Monad m => a -> m a
return Infix :: forall op thing.
op -> thing -> thing -> Int -> Assoc -> Infix op thing
Infix { .. }
isTInfix _ = Maybe (Infix Ident (WithNames Prop))
forall a. Maybe a
Nothing
instance PP (WithNames TVar) where
ppPrec :: Int -> WithNames TVar -> Doc
ppPrec _ (WithNames (TVBound x :: TParam
x) mp :: NameMap
mp) =
case Int -> NameMap -> Maybe String
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (TParam -> Int
tpUnique TParam
x) NameMap
mp of
Just a :: String
a -> String -> Doc
text String
a
Nothing ->
case TParam -> TPFlavor
tpFlav TParam
x of
TPModParam n :: Name
n -> Name -> Doc
forall a. PPName a => a -> Doc
ppPrefixName Name
n
TPOther (Just n :: Name
n) -> Name -> Doc
forall a. PP a => a -> Doc
pp Name
n Doc -> Doc -> Doc
<.> "`" Doc -> Doc -> Doc
<.> Int -> Doc
int (TParam -> Int
tpUnique TParam
x)
_ -> Kind -> TVarSource -> Int -> Doc
pickTVarName (TParam -> Kind
tpKind TParam
x) (TVarInfo -> TVarSource
tvarDesc (TParam -> TVarInfo
tpInfo TParam
x)) (TParam -> Int
tpUnique TParam
x)
ppPrec _ (WithNames (TVFree x :: Int
x k :: Kind
k _ d :: TVarInfo
d) _) =
Char -> Doc
char '?' Doc -> Doc -> Doc
<.> Kind -> TVarSource -> Int -> Doc
pickTVarName Kind
k (TVarInfo -> TVarSource
tvarDesc TVarInfo
d) Int
x
pickTVarName :: Kind -> TVarSource -> Int -> Doc
pickTVarName :: Kind -> TVarSource -> Int -> Doc
pickTVarName k :: Kind
k src :: TVarSource
src uni :: Int
uni =
String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
case TVarSource
src of
TVFromModParam n :: Name
n -> Name -> String
forall a. PP a => a -> String
using Name
n
TVFromSignature n :: Name
n -> Name -> String
forall a. PP a => a -> String
using Name
n
TypeWildCard -> ShowS
mk ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ case Kind
k of
KNum -> "n"
_ -> "a"
TypeOfRecordField i :: Ident
i -> Ident -> String
forall a. PP a => a -> String
using Ident
i
TypeOfTupleField n :: Int
n -> ShowS
mk ("tup_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
TypeOfSeqElement -> ShowS
mk "a"
LenOfSeq -> ShowS
mk "n"
TypeParamInstNamed _ i :: Ident
i -> Ident -> String
forall a. PP a => a -> String
using Ident
i
TypeParamInstPos f :: Name
f n :: Int
n -> ShowS
mk (Name -> String
forall a. PP a => a -> String
sh Name
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
DefinitionOf x :: Name
x -> Name -> String
forall a. PP a => a -> String
using Name
x
LenOfCompGen -> ShowS
mk "n"
TypeOfArg mb :: Maybe Int
mb -> ShowS
mk (case Maybe Int
mb of
Nothing -> "arg"
Just n :: Int
n -> "arg_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
TypeOfRes -> "res"
TypeErrorPlaceHolder -> "err"
where
sh :: a -> String
sh a :: a
a = Doc -> String
forall a. Show a => a -> String
show (a -> Doc
forall a. PP a => a -> Doc
pp a
a)
using :: a -> String
using a :: a
a = ShowS
mk (a -> String
forall a. PP a => a -> String
sh a
a)
mk :: ShowS
mk a :: String
a = String
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ "`" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
uni
instance PP TVar where
ppPrec :: Int -> TVar -> Doc
ppPrec = NameMap -> Int -> TVar -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty
instance PP Type where
ppPrec :: Int -> Prop -> Doc
ppPrec n :: Int
n t :: Prop
t = NameMap -> Int -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty Int
n Prop
t
instance PP TVarInfo where
ppPrec :: Int -> TVarInfo -> Doc
ppPrec _ tvinfo :: TVarInfo
tvinfo = TVarSource -> Doc
forall a. PP a => a -> Doc
pp (TVarInfo -> TVarSource
tvarDesc TVarInfo
tvinfo) Doc -> Doc -> Doc
<+> Doc
loc
where
loc :: Doc
loc = if Range
rng Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
emptyRange then Doc
empty else "at" Doc -> Doc -> Doc
<+> Range -> Doc
forall a. PP a => a -> Doc
pp Range
rng
rng :: Range
rng = TVarInfo -> Range
tvarSource TVarInfo
tvinfo
instance PP TVarSource where
ppPrec :: Int -> TVarSource -> Doc
ppPrec _ tvsrc :: TVarSource
tvsrc =
case TVarSource
tvsrc of
TVFromModParam m :: Name
m -> "module parameter" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
m
TVFromSignature x :: Name
x -> "signature variable" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Name -> Doc
forall a. PP a => a -> Doc
pp Name
x)
TypeWildCard -> "type wildcard (_)"
TypeOfRecordField l :: Ident
l -> "type of field" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
l)
TypeOfTupleField n :: Int
n -> "type of" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. (Integral a, Show a, Eq a) => a -> Doc
ordinal Int
n Doc -> Doc -> Doc
<+> "tuple field"
TypeOfSeqElement -> "type of sequence member"
LenOfSeq -> "length of sequence"
TypeParamInstNamed f :: Name
f i :: Ident
i -> "type argument" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
i) Doc -> Doc -> Doc
<+>
"of" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Name -> Doc
forall a. PP a => a -> Doc
pp Name
f)
TypeParamInstPos f :: Name
f i :: Int
i -> Int -> Doc
forall a. (Integral a, Show a, Eq a) => a -> Doc
ordinal Int
i Doc -> Doc -> Doc
<+> "type argument of" Doc -> Doc -> Doc
<+>
Doc -> Doc
quotes (Name -> Doc
forall a. PP a => a -> Doc
pp Name
f)
DefinitionOf x :: Name
x -> "the type of" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Name -> Doc
forall a. PP a => a -> Doc
pp Name
x)
LenOfCompGen -> "length of comprehension generator"
TypeOfArg mb :: Maybe Int
mb ->
case Maybe Int
mb of
Nothing -> "type of function argument"
Just n :: Int
n -> "type of" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. (Integral a, Show a, Eq a) => a -> Doc
ordinal Int
n Doc -> Doc -> Doc
<+> "function argument"
TypeOfRes -> "type of function result"
TypeErrorPlaceHolder -> "type error place-holder"