cryptol-3.0.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
| TPNewtypeParam 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
newtypeParam :: Name -> TPFlavor
newtypeParam = TPNewtypeParam
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
TPNewtypeParam 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
| TNewtype !Newtype ![Type]
-- ^ A newtype
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
| 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)
-- | Named records
data Newtype = Newtype { ntName :: Name
, ntParams :: [TParam]
, ntConstraints :: [Prop]
, ntConName :: !Name
, ntFields :: RecordMap Ident Type
, ntDoc :: Maybe Text
} deriving (Show, Generic, NFData)
instance Eq Newtype where
x == y = ntName x == ntName y
instance Ord Newtype where
compare x y = compare (ntName x) (ntName y)
-- | Information about an abstract type.
data AbstractType = AbstractType
{ atName :: Name
, atKind :: Kind
, atCtrs :: ([TParam], [Prop])
, atFixitiy :: Maybe Fixity
, atDoc :: Maybe Text
} deriving (Show, Generic, NFData)
--------------------------------------------------------------------------------
instance HasKind AbstractType where
kindOf at = foldr (:->) (atKind at) (map kindOf (fst (atCtrs at)))
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
TNewtype{} -> KType
instance HasKind TySyn where
kindOf ts = foldr (:->) (kindOf (tsDef ts)) (map kindOf (tsParams ts))
instance HasKind Newtype where
kindOf nt = foldr (:->) KType (map kindOf (ntParams nt))
instance HasKind TParam where
kindOf p = tpKind p
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
TNewtype ntx xs == TNewtype 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
(TNewtype x xs, TNewtype 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 p = TVBound p
-- | 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
newtypeConType :: Newtype -> Schema
newtypeConType nt =
Forall as (ntConstraints nt)
$ TRec (ntFields nt) `tFun` TNewtype nt (map (TVar . tpVar) as)
where
as = ntParams nt
abstractTypeTC :: AbstractType -> TCon
abstractTypeTC at =
case builtInType (atName at) of
Just tcon
| kindOf tcon == atKind at -> tcon
| otherwise ->
panic "abstractTypeTC"
[ "Mismatch between built-in and declared type."
, "Name: " ++ pretty (atName at)
, "Declared: " ++ pretty (atKind at)
, "Built-in: " ++ pretty (kindOf tcon)
]
_ -> TC $ TCAbstract $ UserTC (atName at) (atKind at)
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
tAbstract :: UserTC -> [Type] -> Type
tAbstract u ts = TCon (TC (TCAbstract u)) ts
tNewtype :: Newtype -> [Type] -> Type
tNewtype nt ts = TNewtype nt ts
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)
TNewtype _nt ts -> fvs ts
-- | Find the abstract types mentioned in a type.
class FreeAbstract t where
freeAbstract :: t -> Set UserTC
instance FreeAbstract a => FreeAbstract [a] where
freeAbstract = Set.unions . map freeAbstract
instance (FreeAbstract a, FreeAbstract b) => FreeAbstract (a,b) where
freeAbstract (a,b) = Set.union (freeAbstract a) (freeAbstract b)
instance FreeAbstract TCon where
freeAbstract tc =
case tc of
TC (TCAbstract ut) -> Set.singleton ut
_ -> Set.empty
instance FreeAbstract Type where
freeAbstract ty =
case ty of
TCon tc ts -> freeAbstract (tc,ts)
TVar {} -> Set.empty
TUser _ _ t -> freeAbstract t
TRec fs -> freeAbstract (recordElements fs)
TNewtype _nt ts -> freeAbstract 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
ppNewtypeShort :: Newtype -> Doc
ppNewtypeShort nt =
text "newtype" <+> pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
where
ps = ntParams nt
nm = addTNames ps emptyNameMap
ppNewtypeFull :: Newtype -> Doc
ppNewtypeFull nt =
text "newtype" <+> pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
$$ nest 2 (cs $$ ("=" <+> pp (ntConName nt) $$ nest 2 fs))
where
ps = ntParams nt
nm = addTNames ps emptyNameMap
fs = vcat [ pp f <.> ":" <+> pp t | (f,t) <- canonicalFields (ntFields nt) ]
cs = vcat (map pp (ntConstraints nt))
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 Newtype where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames Newtype) where
ppPrec _ (WithNames nt _) = ppNewtypeShort 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
TNewtype 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
TPNewtypeParam 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"
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"
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)