cryptol-3.1.0: src/Cryptol/TypeCheck/Type.hs
{-# Language Safe, DeriveGeneric, DeriveAnyClass, RecordWildCards #-}
{-# Language FlexibleInstances, FlexibleContexts #-}
{-# Language PatternGuards #-}
{-# Language OverloadedStrings #-}
{-| This module contains types related to typechecking and the output of the
typechecker. In particular, it should contain the types needed by
interface files (see 'Crytpol.ModuleSystem.Interface'), which are (kind of)
the output of the typechker.
-}
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`
--------------------------------------------------------------------------------
-- Module parameters
type FunctorParams = Map Ident ModParam
-- | Compute the names from all functor parameters
allParamNames :: FunctorParams -> ModParamNames
allParamNames mps =
ModParamNames
{ mpnTypes = Map.unions (map mpnTypes ps)
, mpnConstraints = concatMap mpnConstraints ps
, mpnFuns = Map.unions (map mpnFuns ps)
, mpnTySyn = Map.unions (map mpnTySyn ps)
, mpnDoc = Nothing
}
where
ps = map mpParameters (Map.elems mps)
-- | A module parameter. Corresponds to a "signature import".
-- A single module parameter can bring multiple things in scope.
data ModParam = ModParam
{ mpName :: Ident
-- ^ The name of a functor parameter.
, mpQual :: !(Maybe ModName)
-- ^ This is the qualifier for the parameter. We use it to
-- derive parameter names when doing `_` imports.
, mpIface :: ImpName Name
-- ^ The interface corresponding to this parameter.
-- This is thing in `import interface`
, mpParameters :: ModParamNames
{- ^ These are the actual parameters, not the ones in the interface
For example if the same interface is used for multiple parameters
the `ifmpParameters` would all be different. -}
} deriving (Show, Generic, NFData)
-- | Information about the names brought in through an "interface import".
-- This is also used to keep information about.
data ModParamNames = ModParamNames
{ mpnTypes :: Map Name ModTParam
-- ^ Type parameters
, mpnTySyn :: !(Map Name TySyn)
-- ^ Type synonyms
, mpnConstraints :: [Located Prop]
-- ^ Constraints on param. types
, mpnFuns :: Map.Map Name ModVParam
-- ^ Value parameters
, mpnDoc :: !(Maybe Text)
-- ^ Documentation about the interface.
} deriving (Show, Generic, NFData)
-- | A type parameter of a module.
data ModTParam = ModTParam
{ mtpName :: Name
, mtpKind :: Kind
, mtpDoc :: Maybe Text
} deriving (Show,Generic,NFData)
-- | This is how module parameters appear in actual types.
mtpParam :: ModTParam -> TParam
mtpParam mtp = TParam { tpUnique = nameUnique (mtpName mtp)
, tpKind = mtpKind mtp
, tpFlav = TPModParam (mtpName mtp)
, tpInfo = desc
}
where desc = TVarInfo { tvarDesc = TVFromModParam (mtpName mtp)
, tvarSource = nameLoc (mtpName mtp)
}
-- | A value parameter of a module.
data ModVParam = ModVParam
{ mvpName :: Name
, mvpType :: Schema
, mvpDoc :: Maybe Text
, mvpFixity :: Maybe Fixity -- XXX: This should be in the name?
} deriving (Show,Generic,NFData)
--------------------------------------------------------------------------------
-- | The types of polymorphic values.
data Schema = Forall { sVars :: [TParam], sProps :: [Prop], sType :: Type }
deriving (Eq, Show, Generic, NFData)
-- | Type parameters.
data TParam = TParam { tpUnique :: !Int -- ^ Parameter identifier
, tpKind :: Kind -- ^ Kind of parameter
, tpFlav :: TPFlavor
-- ^ What sort of type parameter is this
, tpInfo :: !TVarInfo
-- ^ A description for better messages.
}
deriving (Generic, NFData, Show)
data TPFlavor = TPModParam Name
| TPUnifyVar
| TPSchemaParam Name
| TPTySynParam Name
| TPPropSynParam Name
| TPNominalParam Name
| TPPrimParam Name
deriving (Generic, NFData, Show)
tMono :: Type -> Schema
tMono = Forall [] []
isMono :: Schema -> Maybe Type
isMono s =
case s of
Forall [] [] t -> Just t
_ -> Nothing
schemaParam :: Name -> TPFlavor
schemaParam = TPSchemaParam
tySynParam :: Name -> TPFlavor
tySynParam = TPTySynParam
propSynParam :: Name -> TPFlavor
propSynParam = TPPropSynParam
nominalParam :: Name -> TPFlavor
nominalParam = TPNominalParam
primParam :: Name -> TPFlavor
primParam = TPPrimParam
modTyParam :: Name -> TPFlavor
modTyParam = TPModParam
tpfName :: TPFlavor -> Maybe Name
tpfName f =
case f of
TPUnifyVar -> Nothing
TPModParam x -> Just x
TPSchemaParam x -> Just x
TPTySynParam x -> Just x
TPPropSynParam x -> Just x
TPNominalParam x -> Just x
TPPrimParam x -> Just x
tpName :: TParam -> Maybe Name
tpName = tpfName . tpFlav
-- | The internal representation of types.
-- These are assumed to be kind correct.
data Type = TCon !TCon ![Type]
-- ^ Type constant with args
| TVar TVar
-- ^ Type variable (free or bound)
| TUser !Name ![Type] !Type
{- ^ This is just a type annotation, for a type that
was written as a type synonym. It is useful so that we
can use it to report nicer errors.
Example: @TUser T ts t@ is really just the type @t@ that
was written as @T ts@ by the user. -}
| TRec !(RecordMap Ident Type)
-- ^ Record type
| TNominal !NominalType ![Type]
-- ^ A nominal types
deriving (Show, Generic, NFData)
-- | Type variables.
data TVar = TVFree !Int Kind (Set TParam) TVarInfo
-- ^ Unique, kind, ids of bound type variables that are in scope.
-- The last field gives us some info for nicer warnings/errors.
| TVBound {-# UNPACK #-} !TParam
deriving (Show, Generic, NFData)
tvInfo :: TVar -> TVarInfo
tvInfo tv =
case tv of
TVFree _ _ _ d -> d
TVBound tp -> tpInfo tp
tvUnique :: TVar -> Int
tvUnique (TVFree u _ _ _) = u
tvUnique (TVBound TParam { tpUnique = u }) = u
data TVarInfo = TVarInfo { tvarSource :: !Range -- ^ Source code that gave rise
, tvarDesc :: !TypeSource -- ^ Description
}
deriving (Show, Generic, NFData)
-- | Explains how this type came to be, for better error messages.
data TypeSource = TVFromModParam Name -- ^ Name of module parameter
| TVFromSignature Name -- ^ A variable in a signature
| TypeWildCard
| TypeOfRecordField Ident
| TypeOfTupleField Int
| TypeOfSeqElement
| LenOfSeq
| TypeParamInstNamed {-Fun-}Name {-Param-}Ident
| TypeParamInstPos {-Fun-}Name {-Pos (from 1)-}Int
| DefinitionOf Name
| LenOfCompGen
| TypeOfArg ArgDescr
| TypeOfRes
| FunApp
| TypeOfIfCondExpr
| TypeFromUserAnnotation
| GeneratorOfListComp
| CasedExpression
| ConPat
| TypeErrorPlaceHolder
deriving (Show, Generic, NFData)
data ArgDescr = ArgDescr
{ argDescrFun :: Maybe Name
, argDescrNumber :: Maybe Int
}
deriving (Show,Generic,NFData)
noArgDescr :: ArgDescr
noArgDescr = ArgDescr { argDescrFun = Nothing, argDescrNumber = Nothing }
-- | Get the names of something that is related to the tvar.
tvSourceName :: TypeSource -> Maybe Name
tvSourceName tvs =
case tvs of
TVFromModParam x -> Just x
TVFromSignature x -> Just x
TypeParamInstNamed x _ -> Just x
TypeParamInstPos x _ -> Just x
DefinitionOf x -> Just x
TypeOfArg x -> argDescrFun x
_ -> Nothing
-- | A type annotated with information on how it came about.
data TypeWithSource = WithSource
{ twsType :: Type
, twsSource :: TypeSource
, twsRange :: !(Maybe Range)
}
-- | The type is supposed to be of kind 'KProp'.
type Prop = Type
-- | Type synonym.
data TySyn = TySyn { tsName :: Name -- ^ Name
, tsParams :: [TParam] -- ^ Parameters
, tsConstraints :: [Prop] -- ^ Ensure body is OK
, tsDef :: Type -- ^ Definition
, tsDoc :: !(Maybe Text) -- ^ Documentation
}
deriving (Show, Generic, NFData)
-- | Nominal types
data NominalType = NominalType
{ ntName :: Name
, ntParams :: [TParam]
, ntKind :: !Kind -- ^ Result kind
, ntConstraints :: [Prop]
, ntDef :: NominalTypeDef
, ntFixity :: !(Maybe Fixity)
, ntDoc :: Maybe Text
} deriving (Show, Generic, NFData)
-- | Definition of a nominal type
data NominalTypeDef =
Struct StructCon
| Enum [EnumCon]
| Abstract
deriving (Show, Generic, NFData)
-- | Constructor for a struct (aka newtype)
data StructCon = StructCon
{ ntConName :: !Name
, ntFields :: RecordMap Ident Type
} deriving (Show, Generic, NFData)
-- | Constructor for an enumeration
data EnumCon = EnumCon
{ ecName :: Name
, ecNumber :: !Int -- ^ Number of constructor in the declaration
, ecFields :: [Type]
, ecPublic :: Bool
, ecDoc :: Maybe Text
} deriving (Show,Generic,NFData)
instance Eq NominalType where
x == y = ntName x == ntName y
instance Ord NominalType where
compare x y = compare (ntName x) (ntName y)
--------------------------------------------------------------------------------
instance HasKind TVar where
kindOf (TVFree _ k _ _) = k
kindOf (TVBound tp) = kindOf tp
instance HasKind Type where
kindOf ty =
case ty of
TVar a -> kindOf a
TCon c ts -> quickApply (kindOf c) ts
TUser _ _ t -> kindOf t
TRec {} -> KType
TNominal nt ts ->
case ntDef nt of
Struct {} -> KType
Enum {} -> KType
Abstract -> quickApply (kindOf nt) ts
instance HasKind TySyn where
kindOf ts = foldr (:->) (kindOf (tsDef ts)) (map kindOf (tsParams ts))
instance HasKind NominalType where
kindOf nt = foldr (:->) (ntKind nt) (map kindOf (ntParams nt))
instance HasKind TParam where
kindOf = tpKind
quickApply :: Kind -> [a] -> Kind
quickApply k [] = k
quickApply (_ :-> k) (_ : ts) = quickApply k ts
quickApply k _ = panic "Cryptol.TypeCheck.AST.quickApply"
[ "Applying a non-function kind:", show k ]
kindResult :: Kind -> Kind
kindResult (_ :-> k) = kindResult k
kindResult k = k
--------------------------------------------------------------------------------
-- | Syntactic equality, ignoring type synonyms and record order.
instance Eq Type where
TUser _ _ x == y = x == y
x == TUser _ _ y = y == x
TCon x xs == TCon y ys = x == y && xs == ys
TVar x == TVar y = x == y
TRec xs == TRec ys = xs == ys
TNominal ntx xs == TNominal nty ys = ntx == nty && xs == ys
_ == _ = False
instance Ord Type where
compare x0 y0 =
case (x0,y0) of
(TUser _ _ t, _) -> compare t y0
(_, TUser _ _ t) -> compare x0 t
(TVar x, TVar y) -> compare x y
(TVar {}, _) -> LT
(_, TVar {}) -> GT
(TCon x xs, TCon y ys) -> compare (x,xs) (y,ys)
(TCon {}, _) -> LT
(_,TCon {}) -> GT
(TRec xs, TRec ys) -> compare xs ys
(TRec{}, _) -> LT
(_, TRec{}) -> GT
(TNominal x xs, TNominal y ys) -> compare (x,xs) (y,ys)
instance Eq TParam where
x == y = tpUnique x == tpUnique y
instance Ord TParam where
compare x y = compare (tpUnique x) (tpUnique y)
tpVar :: TParam -> TVar
tpVar = TVBound
-- | The type is "simple" (i.e., it contains no type functions).
type SType = Type
--------------------------------------------------------------------
-- Superclass
-- | Compute the set of all @Prop@s that are implied by the
-- given prop via superclass constraints.
superclassSet :: Prop -> Set Prop
superclassSet (TCon (PC PPrime) [n]) =
Set.fromList [ pFin n, n >== tTwo ]
superclassSet (TCon (PC p0) [t]) = go p0
where
super p = Set.insert (TCon (PC p) [t]) (go p)
go PRing = super PZero
go PLogic = super PZero
go PField = super PRing
go PIntegral = super PRing
go PRound = super PField <> super PCmp
go PCmp = super PEq
go PSignedCmp = super PEq
go _ = mempty
superclassSet _ = mempty
nominalTypeConTypes :: NominalType -> [(Name,Schema)]
nominalTypeConTypes nt =
case ntDef nt of
Struct s -> [ ( ntConName s
, Forall as ctrs (TRec (ntFields s) `tFun` resT)
) ]
Enum cs -> [ ( ecName c
, Forall as ctrs (foldr tFun resT (ecFields c))
)
| c <- cs
]
Abstract -> []
where
as = ntParams nt
ctrs = ntConstraints nt
resT = TNominal nt (map (TVar . tpVar) as)
nominalTypeIsAbstract :: NominalType -> Bool
nominalTypeIsAbstract nt =
case ntDef nt of
Abstract -> True
_ -> False
instance Eq TVar where
TVBound x == TVBound y = x == y
TVFree x _ _ _ == TVFree y _ _ _ = x == y
_ == _ = False
instance Ord TVar where
compare (TVFree x _ _ _) (TVFree y _ _ _) = compare x y
compare (TVFree _ _ _ _) _ = LT
compare _ (TVFree _ _ _ _) = GT
compare (TVBound x) (TVBound y) = compare x y
--------------------------------------------------------------------------------
-- Queries
isFreeTV :: TVar -> Bool
isFreeTV (TVFree {}) = True
isFreeTV _ = False
isBoundTV :: TVar -> Bool
isBoundTV (TVBound {}) = True
isBoundTV _ = False
tIsError :: Type -> Maybe Type
tIsError ty = case tNoUser ty of
TCon (TError _) [t] -> Just t
TCon (TError _) _ -> panic "tIsError" ["Malformed error"]
_ -> Nothing
tHasErrors :: Type -> Bool
tHasErrors ty =
case tNoUser ty of
TCon (TError _) _ -> True
TCon _ ts -> any tHasErrors ts
TRec mp -> any tHasErrors mp
_ -> False
tIsNat' :: Type -> Maybe Nat'
tIsNat' ty =
case tNoUser ty of
TCon (TC (TCNum x)) [] -> Just (Nat x)
TCon (TC TCInf) [] -> Just Inf
_ -> Nothing
tIsNum :: Type -> Maybe Integer
tIsNum ty = do Nat x <- tIsNat' ty
return x
tIsInf :: Type -> Bool
tIsInf ty = tIsNat' ty == Just Inf
tIsVar :: Type -> Maybe TVar
tIsVar ty = case tNoUser ty of
TVar x -> Just x
_ -> Nothing
tIsFun :: Type -> Maybe (Type, Type)
tIsFun ty = case tNoUser ty of
TCon (TC TCFun) [a, b] -> Just (a, b)
_ -> Nothing
tIsSeq :: Type -> Maybe (Type, Type)
tIsSeq ty = case tNoUser ty of
TCon (TC TCSeq) [n, a] -> Just (n, a)
_ -> Nothing
tIsBit :: Type -> Bool
tIsBit ty = case tNoUser ty of
TCon (TC TCBit) [] -> True
_ -> False
tIsInteger :: Type -> Bool
tIsInteger ty = case tNoUser ty of
TCon (TC TCInteger) [] -> True
_ -> False
tIsIntMod :: Type -> Maybe Type
tIsIntMod ty = case tNoUser ty of
TCon (TC TCIntMod) [n] -> Just n
_ -> Nothing
tIsRational :: Type -> Bool
tIsRational ty =
case tNoUser ty of
TCon (TC TCRational) [] -> True
_ -> False
tIsFloat :: Type -> Maybe (Type, Type)
tIsFloat ty =
case tNoUser ty of
TCon (TC TCFloat) [e, p] -> Just (e, p)
_ -> Nothing
tIsTuple :: Type -> Maybe [Type]
tIsTuple ty = case tNoUser ty of
TCon (TC (TCTuple _)) ts -> Just ts
_ -> Nothing
tIsRec :: Type -> Maybe (RecordMap Ident Type)
tIsRec ty = case tNoUser ty of
TRec fs -> Just fs
_ -> Nothing
tIsBinFun :: TFun -> Type -> Maybe (Type,Type)
tIsBinFun f ty = case tNoUser ty of
TCon (TF g) [a,b] | f == g -> Just (a,b)
_ -> Nothing
-- | Split up repeated occurances of the given binary type-level function.
tSplitFun :: TFun -> Type -> [Type]
tSplitFun f t0 = go t0 []
where go ty xs = case tIsBinFun f ty of
Just (a,b) -> go a (go b xs)
Nothing -> ty : xs
pIsFin :: Prop -> Maybe Type
pIsFin ty = case tNoUser ty of
TCon (PC PFin) [t1] -> Just t1
_ -> Nothing
pIsPrime :: Prop -> Maybe Type
pIsPrime ty = case tNoUser ty of
TCon (PC PPrime) [t1] -> Just t1
_ -> Nothing
pIsGeq :: Prop -> Maybe (Type,Type)
pIsGeq ty = case tNoUser ty of
TCon (PC PGeq) [t1,t2] -> Just (t1,t2)
_ -> Nothing
pIsEqual :: Prop -> Maybe (Type,Type)
pIsEqual ty = case tNoUser ty of
TCon (PC PEqual) [t1,t2] -> Just (t1,t2)
_ -> Nothing
pIsZero :: Prop -> Maybe Type
pIsZero ty = case tNoUser ty of
TCon (PC PZero) [t1] -> Just t1
_ -> Nothing
pIsLogic :: Prop -> Maybe Type
pIsLogic ty = case tNoUser ty of
TCon (PC PLogic) [t1] -> Just t1
_ -> Nothing
pIsRing :: Prop -> Maybe Type
pIsRing ty = case tNoUser ty of
TCon (PC PRing) [t1] -> Just t1
_ -> Nothing
pIsField :: Prop -> Maybe Type
pIsField ty = case tNoUser ty of
TCon (PC PField) [t1] -> Just t1
_ -> Nothing
pIsIntegral :: Prop -> Maybe Type
pIsIntegral ty = case tNoUser ty of
TCon (PC PIntegral) [t1] -> Just t1
_ -> Nothing
pIsRound :: Prop -> Maybe Type
pIsRound ty = case tNoUser ty of
TCon (PC PRound) [t1] -> Just t1
_ -> Nothing
pIsEq :: Prop -> Maybe Type
pIsEq ty = case tNoUser ty of
TCon (PC PEq) [t1] -> Just t1
_ -> Nothing
pIsCmp :: Prop -> Maybe Type
pIsCmp ty = case tNoUser ty of
TCon (PC PCmp) [t1] -> Just t1
_ -> Nothing
pIsSignedCmp :: Prop -> Maybe Type
pIsSignedCmp ty = case tNoUser ty of
TCon (PC PSignedCmp) [t1] -> Just t1
_ -> Nothing
pIsLiteral :: Prop -> Maybe (Type, Type)
pIsLiteral ty = case tNoUser ty of
TCon (PC PLiteral) [t1, t2] -> Just (t1, t2)
_ -> Nothing
pIsLiteralLessThan :: Prop -> Maybe (Type, Type)
pIsLiteralLessThan ty =
case tNoUser ty of
TCon (PC PLiteralLessThan) [t1, t2] -> Just (t1, t2)
_ -> Nothing
pIsFLiteral :: Prop -> Maybe (Type,Type,Type,Type)
pIsFLiteral ty = case tNoUser ty of
TCon (PC PFLiteral) [t1,t2,t3,t4] -> Just (t1,t2,t3,t4)
_ -> Nothing
pIsTrue :: Prop -> Bool
pIsTrue ty = case tNoUser ty of
TCon (PC PTrue) _ -> True
_ -> False
pIsWidth :: Prop -> Maybe Type
pIsWidth ty = case tNoUser ty of
TCon (TF TCWidth) [t1] -> Just t1
_ -> Nothing
pIsValidFloat :: Prop -> Maybe (Type,Type)
pIsValidFloat ty = case tNoUser ty of
TCon (PC PValidFloat) [a,b] -> Just (a,b)
_ -> Nothing
--------------------------------------------------------------------------------
tNum :: Integral a => a -> Type
tNum n = TCon (TC (TCNum (toInteger n))) []
tZero :: Type
tZero = tNum (0 :: Int)
tOne :: Type
tOne = tNum (1 :: Int)
tTwo :: Type
tTwo = tNum (2 :: Int)
tInf :: Type
tInf = TCon (TC TCInf) []
tNat' :: Nat' -> Type
tNat' n' = case n' of
Inf -> tInf
Nat n -> tNum n
tNominal :: NominalType -> [Type] -> Type
tNominal = TNominal
tBit :: Type
tBit = TCon (TC TCBit) []
tInteger :: Type
tInteger = TCon (TC TCInteger) []
tRational :: Type
tRational = TCon (TC TCRational) []
tFloat :: Type -> Type -> Type
tFloat e p = TCon (TC TCFloat) [ e, p ]
tIntMod :: Type -> Type
tIntMod n = TCon (TC TCIntMod) [n]
tArray :: Type -> Type -> Type
tArray a b = TCon (TC TCArray) [a, b]
tWord :: Type -> Type
tWord a = tSeq a tBit
tSeq :: Type -> Type -> Type
tSeq a b = TCon (TC TCSeq) [a,b]
tChar :: Type
tChar = tWord (tNum (8 :: Int))
tString :: Int -> Type
tString len = tSeq (tNum len) tChar
tRec :: RecordMap Ident Type -> Type
tRec = TRec
tTuple :: [Type] -> Type
tTuple ts = TCon (TC (TCTuple (length ts))) ts
-- | Make a function type.
tFun :: Type -> Type -> Type
tFun a b = TCon (TC TCFun) [a,b]
-- | Eliminate outermost type synonyms.
tNoUser :: Type -> Type
tNoUser t = case t of
TUser _ _ a -> tNoUser a
_ -> t
--------------------------------------------------------------------------------
-- Construction of type functions
-- | Make an error value of the given type to replace
-- the given malformed type (the argument to the error function)
tError :: Type -> Type
tError t = TCon (TError (k :-> k)) [t]
where k = kindOf t
tf1 :: TFun -> Type -> Type
tf1 f x = TCon (TF f) [x]
tf2 :: TFun -> Type -> Type -> Type
tf2 f x y = TCon (TF f) [x,y]
tf3 :: TFun -> Type -> Type -> Type -> Type
tf3 f x y z = TCon (TF f) [x,y,z]
tSub :: Type -> Type -> Type
tSub = tf2 TCSub
tMul :: Type -> Type -> Type
tMul = tf2 TCMul
tDiv :: Type -> Type -> Type
tDiv = tf2 TCDiv
tMod :: Type -> Type -> Type
tMod = tf2 TCMod
tExp :: Type -> Type -> Type
tExp = tf2 TCExp
tMin :: Type -> Type -> Type
tMin = tf2 TCMin
tCeilDiv :: Type -> Type -> Type
tCeilDiv = tf2 TCCeilDiv
tCeilMod :: Type -> Type -> Type
tCeilMod = tf2 TCCeilMod
tLenFromThenTo :: Type -> Type -> Type -> Type
tLenFromThenTo = tf3 TCLenFromThenTo
--------------------------------------------------------------------------------
-- Construction of constraints.
-- | Equality for numeric types.
(=#=) :: Type -> Type -> Prop
x =#= y = TCon (PC PEqual) [x,y]
(=/=) :: Type -> Type -> Prop
x =/= y = TCon (PC PNeq) [x,y]
pZero :: Type -> Prop
pZero t = TCon (PC PZero) [t]
pLogic :: Type -> Prop
pLogic t = TCon (PC PLogic) [t]
pRing :: Type -> Prop
pRing t = TCon (PC PRing) [t]
pIntegral :: Type -> Prop
pIntegral t = TCon (PC PIntegral) [t]
pField :: Type -> Prop
pField t = TCon (PC PField) [t]
pRound :: Type -> Prop
pRound t = TCon (PC PRound) [t]
pEq :: Type -> Prop
pEq t = TCon (PC PEq) [t]
pCmp :: Type -> Prop
pCmp t = TCon (PC PCmp) [t]
pSignedCmp :: Type -> Prop
pSignedCmp t = TCon (PC PSignedCmp) [t]
pLiteral :: Type -> Type -> Prop
pLiteral x y = TCon (PC PLiteral) [x, y]
pLiteralLessThan :: Type -> Type -> Prop
pLiteralLessThan x y = TCon (PC PLiteralLessThan) [x, y]
-- | Make a greater-than-or-equal-to constraint.
(>==) :: Type -> Type -> Prop
x >== y = TCon (PC PGeq) [x,y]
-- | A @Has@ constraint, used for tuple and record selection.
pHas :: Selector -> Type -> Type -> Prop
pHas l ty fi = TCon (PC (PHas l)) [ty,fi]
pTrue :: Prop
pTrue = TCon (PC PTrue) []
pAnd :: [Prop] -> Prop
pAnd [] = pTrue
pAnd [x] = x
pAnd (x : xs)
| Just _ <- tIsError x = x
| pIsTrue x = rest
| Just _ <- tIsError rest = rest
| pIsTrue rest = x
| otherwise = TCon (PC PAnd) [x, rest]
where rest = pAnd xs
pSplitAnd :: Prop -> [Prop]
pSplitAnd p0 = go [p0]
where
go [] = []
go (q : qs) =
case tNoUser q of
TCon (PC PAnd) [l,r] -> go (l : r : qs)
TCon (PC PTrue) _ -> go qs
_ -> q : go qs
pFin :: Type -> Prop
pFin ty =
case tNoUser ty of
TCon (TC (TCNum _)) _ -> pTrue
TCon (TC TCInf) _ -> tError prop -- XXX: should we be doing this here??
_ -> prop
where
prop = TCon (PC PFin) [ty]
pValidFloat :: Type -> Type -> Type
pValidFloat e p = TCon (PC PValidFloat) [e,p]
pPrime :: Type -> Prop
pPrime ty =
case tNoUser ty of
TCon (TC TCInf) _ -> tError prop
_ -> prop
where
prop = TCon (PC PPrime) [ty]
-- Negation --------------------------------------------------------------------
{-| `pNegNumeric` negates a simple (i.e., not And, not prime, etc) prop
over numeric type vars. The result is a conjunction of properties. -}
pNegNumeric :: Prop -> [Prop]
pNegNumeric prop =
case tNoUser prop of
TCon tcon tys ->
case tcon of
PC pc ->
case pc of
-- not (x == y) <=> x /= y
PEqual -> [TCon (PC PNeq) tys]
-- not (x /= y) <=> x == y
PNeq -> [TCon (PC PEqual) tys]
-- not (x >= y) <=> x /= y and y >= x
PGeq -> [TCon (PC PNeq) tys, TCon (PC PGeq) (reverse tys)]
-- not (fin x) <=> x == Inf
PFin | [ty] <- tys -> [ty =#= tInf]
| otherwise -> bad
-- not True <=> 0 == 1
PTrue -> [TCon (PC PEqual) [tZero, tOne]]
_ -> bad
TError _ki -> [prop] -- propogates `TError`
TC _tc -> bad
TF _tf -> bad
_ -> bad
where
bad = panic "pNegNumeric"
[ "Unexpeceted numeric constraint:"
, pretty prop
]
--------------------------------------------------------------------------------
noFreeVariables :: FVS t => t -> Bool
noFreeVariables = all (not . isFreeTV) . Set.toList . fvs
freeParams :: FVS t => t -> Set TParam
freeParams x = Set.unions (map params (Set.toList (fvs x)))
where
params (TVFree _ _ tps _) = tps
params (TVBound tp) = Set.singleton tp
class FVS t where
fvs :: t -> Set TVar
instance FVS Type where
fvs = go
where
go ty =
case ty of
TCon _ ts -> fvs ts
TVar x -> Set.singleton x
TUser _ _ t -> go t
TRec fs -> fvs (recordElements fs)
TNominal _nt ts -> fvs ts
instance FVS a => FVS (Maybe a) where
fvs Nothing = Set.empty
fvs (Just x) = fvs x
instance FVS a => FVS [a] where
fvs xs = Set.unions (map fvs xs)
instance (FVS a, FVS b) => FVS (a,b) where
fvs (x,y) = Set.union (fvs x) (fvs y)
instance FVS Schema where
fvs (Forall as ps t) =
Set.difference (Set.union (fvs ps) (fvs t)) bound
where bound = Set.fromList (map tpVar as)
-- Pretty Printing -------------------------------------------------------------
instance PP TParam where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames TParam) where
ppPrec _ (WithNames p mp) = ppWithNames mp (tpVar p)
addTNames :: [TParam] -> NameMap -> NameMap
addTNames as ns = foldr (uncurry IntMap.insert) ns
$ named ++ zip unnamed_nums numNames
++ zip unnamed_vals valNames
where avail xs = filter (`notElem` used) (nameList xs)
numNames = avail ["n","m","i","j","k"]
valNames = avail ["a","b","c","d","e"]
nm x = (tpUnique x, tpName x, tpKind x)
named = [ (u,show (pp n)) | (u,Just n,_) <- map nm as ]
unnamed_nums = [ u | (u,Nothing,KNum) <- map nm as ]
unnamed_vals = [ u | (u,Nothing,KType) <- map nm as ]
used = map snd named ++ IntMap.elems ns
ppNominalShort :: NominalType -> Doc
ppNominalShort nt =
kw <+> pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
where
ps = ntParams nt
nm = addTNames ps emptyNameMap
kw = case ntDef nt of
Struct {} -> "newtype"
Enum {} -> "enum"
Abstract {} -> "primitive type"
ppNominalFull :: NominalType -> Doc
ppNominalFull nt =
case ntDef nt of
Struct con -> ppKWDef "newtype" ("=" <+> pp (ntConName con) $$ nest 2 fs)
where fs = vcat [ pp f <.> ":" <+> pp t
| (f,t) <- canonicalFields (ntFields con) ]
Enum cons ->
ppKWDef "enum" $
vcat [ pref <+> pp (ecName con) <+> hsep (map (ppPrec 1) (ecFields con))
| (pref,con) <- zip ("=" : repeat "|") cons
]
Abstract ->
"primitive type" <+> paramBinds <+> ctrs <+> ppTyUse <+>
":" <+> pp (ntKind nt)
where
paramBinds =
case ps of
[] -> mempty
_ -> braces (commaSep (map ppBind ps))
ppBind p = ppWithNamesPrec nm 0 p <+> ":" <+> pp (kindOf p)
ppC = ppWithNamesPrec nm 0
ctrs = case ntConstraints nt of
[] -> mempty
_ -> parens (commaSep (map ppC (ntConstraints nt))) <+> "=>"
where
ps = ntParams nt
cs = vcat (map pp (ntConstraints nt))
nm = addTNames ps emptyNameMap
ppTyUse = pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
ppKWDef kw def = (kw <+> ppTyUse) $$ nest 2 (cs $$ def)
instance PP Schema where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames Schema) where
ppPrec _ (WithNames s ns)
| null (sVars s) && null (sProps s) = body
| otherwise = nest 2 (sep (vars ++ props ++ [body]))
where
body = ppWithNames ns1 (sType s)
vars = case sVars s of
[] -> []
vs -> [nest 1 (braces (commaSepFill (map (ppWithNames ns1) vs)))]
props = case sProps s of
[] -> []
ps -> [nest 1 (parens (commaSepFill (map (ppWithNames ns1) ps))) <+> text "=>"]
ns1 = addTNames (sVars s) ns
instance PP TySyn where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames TySyn) where
ppPrec _ (WithNames ts ns) =
nest 2 $ sep
[ fsep ([text "type"] ++ ctr ++ lhs ++ [char '='])
, ppWithNames ns1 (tsDef ts)
]
where ns1 = addTNames (tsParams ts) ns
ctr = case kindResult (kindOf ts) of
KProp -> [text "constraint"]
_ -> []
n = tsName ts
lhs = case (nameFixity n, tsParams ts) of
(Just _, [x, y]) ->
[ppWithNames ns1 x, pp (nameIdent n), ppWithNames ns1 y]
(_, ps) ->
[pp n] ++ map (ppWithNames ns1) ps
instance PP NominalType where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames NominalType) where
ppPrec _ (WithNames nt _) = ppNominalShort nt -- XXX: do the full thing?
-- | The precedence levels used by this pretty-printing instance
-- correspond with parser non-terminals as follows:
--
-- * 0-1: @type@
--
-- * 2: @infix_type@
--
-- * 3: @app_type@
--
-- * 4: @dimensions atype@
--
-- * 5: @atype@
instance PP (WithNames Type) where
ppPrec prec ty0@(WithNames ty nmMap) =
case ty of
TVar a -> ppWithNames nmMap a
TNominal nt ts -> optParens (prec > 3)
(fsep (pp (ntName nt) : map (go 5) ts))
TRec fs -> ppRecord
[ pp l <+> text ":" <+> go 0 t | (l,t) <- displayFields fs ]
_ | Just tinf <- isTInfix ty0 -> optParens (prec > 2)
$ ppInfix 2 isTInfix tinf
TUser c ts t ->
withNameDisp $ \disp ->
case asOrigName c of
Just og | NotInScope <- getNameFormat og disp ->
go prec t -- unfold type synonym if not in scope
_ ->
case ts of
[] -> pp c
_ -> optParens (prec > 3) $ fsep (pp c : map (go 5) ts)
TCon (TC tc) ts ->
case (tc,ts) of
(TCNum n, []) -> integer n
(TCInf, []) -> text "inf"
(TCBit, []) -> text "Bit"
(TCInteger, []) -> text "Integer"
(TCRational, []) -> text "Rational"
(TCIntMod, [n]) -> optParens (prec > 3) $ text "Z" <+> go 5 n
(TCSeq, [t1,TCon (TC TCBit) []]) -> brackets (go 0 t1)
(TCSeq, [t1,t2]) -> optParens (prec > 4)
$ brackets (go 0 t1) <.> go 4 t2
(TCFun, [t1,t2]) -> optParens (prec > 1)
$ go 2 t1 <+> text "->" <+> go 1 t2
(TCTuple _, fs) -> ppTuple $ map (go 0) fs
(_, _) -> optParens (prec > 3) $ fsep (pp tc : (map (go 5) ts))
TCon (PC pc) ts ->
case (pc,ts) of
(PEqual, [t1,t2]) -> go 0 t1 <+> text "==" <+> go 0 t2
(PNeq , [t1,t2]) -> go 0 t1 <+> text "!=" <+> go 0 t2
(PGeq, [t1,t2]) -> go 0 t1 <+> text ">=" <+> go 0 t2
(PFin, [t1]) -> optParens (prec > 3) $ text "fin" <+> (go 5 t1)
(PPrime, [t1]) -> optParens (prec > 3) $ text "prime" <+> (go 5 t1)
(PHas x, [t1,t2]) -> ppSelector x <+> text "of"
<+> go 0 t1 <+> text "is" <+> go 0 t2
(PAnd, [t1,t2]) -> nest 1 (parens (commaSepFill (map (go 0) (t1 : pSplitAnd t2))))
(PRing, [t1]) -> pp pc <+> go 5 t1
(PField, [t1]) -> pp pc <+> go 5 t1
(PIntegral, [t1]) -> pp pc <+> go 5 t1
(PRound, [t1]) -> pp pc <+> go 5 t1
(PCmp, [t1]) -> pp pc <+> go 5 t1
(PSignedCmp, [t1]) -> pp pc <+> go 5 t1
(PLiteral, [t1,t2]) -> pp pc <+> go 5 t1 <+> go 5 t2
(PLiteralLessThan, [t1,t2]) -> pp pc <+> go 5 t1 <+> go 5 t2
(_, _) -> optParens (prec > 3) $ fsep (pp pc : map (go 5) ts)
TCon f ts -> optParens (prec > 3) $ fsep (pp f : map (go 5) ts)
where
go p t = ppWithNamesPrec nmMap p t
isTInfix (WithNames (TCon tc [ieLeft',ieRight']) _) =
do let ieLeft = WithNames ieLeft' nmMap
ieRight = WithNames ieRight' nmMap
(ieOp, ieFixity) <- infixPrimTy tc
return Infix { .. }
isTInfix (WithNames (TUser n [ieLeft',ieRight'] _) _)
| isInfixIdent (nameIdent n) =
do let ieLeft = WithNames ieLeft' nmMap
ieRight = WithNames ieRight' nmMap
ieFixity = fromMaybe defaultFixity (nameFixity n)
ieOp = nameIdent n
return Infix { .. }
isTInfix _ = Nothing
instance PP (WithNames TVar) where
ppPrec _ (WithNames tv mp) =
case tv of
TVBound {} -> nmTxt
TVFree {} -> "?" <.> nmTxt
where
nmTxt
| Just a <- IntMap.lookup (tvUnique tv) mp = text a
| otherwise =
case tv of
TVBound x ->
let declNm n = pp n <.> "`" <.> int (tpUnique x) in
case tpFlav x of
TPModParam n -> ppPrefixName n
TPUnifyVar -> pickTVarName (tpKind x) (tvarDesc (tpInfo x)) (tpUnique x)
TPSchemaParam n -> declNm n
TPTySynParam n -> declNm n
TPPropSynParam n -> declNm n
TPNominalParam n -> declNm n
TPPrimParam n -> declNm n
TVFree x k _ d -> pickTVarName k (tvarDesc d) x
pickTVarName :: Kind -> TypeSource -> Int -> Doc
pickTVarName k src uni =
text $
case src of
TVFromModParam n -> using n
TVFromSignature n -> using n
TypeWildCard -> mk $ case k of
KNum -> "n"
_ -> "a"
TypeOfRecordField i -> using i
TypeOfTupleField n -> mk ("tup_" ++ show n)
TypeOfSeqElement -> mk "a"
LenOfSeq -> mk "n"
TypeParamInstNamed _ i -> using i
TypeParamInstPos f n -> mk (sh f ++ "_" ++ show n)
DefinitionOf x ->
case nameInfo x of
GlobalName SystemName og
| ogModule og == TopModule exprModName -> mk "it"
_ -> using x
LenOfCompGen -> mk "n"
GeneratorOfListComp -> "seq"
TypeOfIfCondExpr -> "b"
TypeOfArg ad -> mk (case argDescrNumber ad of
Nothing -> "arg"
Just n -> "arg_" ++ show n)
TypeOfRes -> "res"
FunApp -> "fun"
TypeFromUserAnnotation -> "user"
TypeErrorPlaceHolder -> "err"
CasedExpression -> "case"
ConPat -> "conp"
where
sh a = show (pp a)
using a = mk (sh a)
mk a = a ++ "`" ++ show uni
instance PP TVar where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP Type where
ppPrec n t = ppWithNamesPrec IntMap.empty n t
instance PP TVarInfo where
ppPrec _ tvinfo = hsep $ [pp (tvarDesc tvinfo)] ++ loc
where
loc = if rng == emptyRange then [] else ["at" <+> pp rng]
rng = tvarSource tvinfo
instance PP ArgDescr where
ppPrec _ ad = hsep ([which, "argument"] ++ ofFun)
where
which = maybe "function" ordinal (argDescrNumber ad)
ofFun = case argDescrFun ad of
Nothing -> []
Just f -> ["of" <+> pp f]
instance PP TypeSource where
ppPrec _ tvsrc =
case tvsrc of
TVFromModParam m -> "module parameter" <+> pp m
TVFromSignature x -> "signature variable" <+> quotes (pp x)
TypeWildCard -> "type wildcard (_)"
TypeOfRecordField l -> "type of field" <+> quotes (pp l)
TypeOfTupleField n -> "type of" <+> ordinal n <+> "tuple field"
TypeOfSeqElement -> "type of sequence member"
LenOfSeq -> "length of sequence"
TypeParamInstNamed f i -> "type argument" <+> quotes (pp i) <+>
"of" <+> quotes (pp f)
TypeParamInstPos f i -> ordinal i <+> "type argument of" <+>
quotes (pp f)
DefinitionOf x -> "the type of" <+> quotes (pp x)
LenOfCompGen -> "length of comprehension generator"
TypeOfArg ad -> "type of" <+> pp ad
TypeOfRes -> "type of function result"
TypeOfIfCondExpr -> "type of `if` condition"
TypeFromUserAnnotation -> "user annotation"
GeneratorOfListComp -> "generator in a list comprehension"
FunApp -> "function call"
TypeErrorPlaceHolder -> "type error place-holder"
CasedExpression -> "cased expression"
ConPat -> "constructor pattern"
instance PP ModParamNames where
ppPrec _ ps =
let tps = Map.elems (mpnTypes ps)
in
vcat $ map pp tps ++
if null (mpnConstraints ps) then [] else
[ "type constraint" <+>
parens (commaSep (map (pp . thing) (mpnConstraints ps)))
] ++
[ pp t | t <- Map.elems (mpnTySyn ps) ] ++
map pp (Map.elems (mpnFuns ps))
instance PP ModTParam where
ppPrec _ p =
"type" <+> pp (mtpName p) <+> ":" <+> pp (mtpKind p)
instance PP ModVParam where
ppPrec _ p = pp (mvpName p) <+> ":" <+> pp (mvpType p)