GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-15 18:52:13 +03:00
Code Issues Projects Releases Wiki Activity

Move all built-in types to the same place; add precedence and documentaiton

Browse Source
This commit is contained in:
Iavor Diatchki 2018-07-26 09:06:37 +03:00
parent f4e7100e59
commit 19c71fa4aa
5 changed files with 442 additions and 313 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

99
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -34,7 +34,7 @@ import Cryptol.Prims.Syntax
import Cryptol.Parser.AST
import Cryptol.Parser.Position
import Cryptol.TypeCheck.Type (TCon(..))
import Cryptol.Utils.Ident (packIdent,packInfix)
import Cryptol.Utils.Ident (packInfix)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP
@ -585,13 +585,13 @@ translateProp ty = go ty
TLocated t' r -> (`CLocated` r) <$> go t'
TApp (PC x) [l,r]
| PEqual <- x -> CEqual <$> rename l <*> rename r
| PNeq <- x -> CNeq <$> rename l <*> rename r
| PGeq <- x -> CGeq <$> rename l <*> rename r
TUser n [l,r]
| i == packIdent "==" -> CEqual <$> rename l <*> rename r
| i == packIdent ">=" -> CGeq <$> rename l <*> rename r
| i == packIdent "<=" -> CGeq <$> rename r <*> rename l
| i == packIdent "!=" -> CNeq <$> rename l <*> rename r
where
i = getIdent n
| isLeq n -> CGeq <$> rename r <*> rename l
TUser n ts -> CUser <$> renameType n <*> traverse rename ts
@ -603,10 +603,10 @@ translateProp ty = go ty
-- | Check to see if this identifier is a reserved type/type-function.
isReserved :: PName -> Bool
isReserved pn = Map.member pn tfunNames || isReservedTyCon pn
isReserved pn = case primTyFromPName pn of
Just _ -> True
_ -> False
isReservedTyCon :: PName -> Bool
isReservedTyCon pn = Map.member pn tconNames
-- | Resolve fixity, then rename the resulting type.
instance Rename Type where
@ -621,16 +621,9 @@ instance Rename Type where
go (TUser pn ps)
-- all type functions
| Just (arity,fun) <- Map.lookup pn tfunNames =
do when (arity /= length ps) (record (MalformedBuiltin ty0 pn))
ps' <- traverse go ps
return (TApp (TF fun) ps')
-- built-in types like Bit and inf
| Just tc <- Map.lookup pn tconNames =
| Just pt <- primTyFromPName pn =
do ps' <- traverse go ps
return (TApp (TC tc) ps')
return (TApp (primTyCon pt) ps')
go (TUser qn ps) = TUser <$> renameType qn <*> traverse go ps
go (TApp f xs) = TApp f <$> traverse go xs
@ -678,42 +671,31 @@ resolveTypeFixity = go
type TOp = Type PName -> Type PName -> Type PName
infixProps :: [PName]
infixProps = map (mkUnqual . packInfix) [ "==", ">=", "<=", "!=" ]
mkTInfix :: Type PName -> (TOp,Fixity) -> Type PName -> RenameM (Type PName)
-- only if the function is one of props
mkTInfix t@(TUser o1 [x,y]) op@(o2,f2) z
| o1 `elem` infixProps =
do let f1 = Fixity NonAssoc 0
case compareFixity f1 f2 of
FCLeft -> return (o2 t z)
FCRight -> do r <- mkTInfix y op z
return (TUser o1 [x,r])
mkTInfix t op@(o2,f2) z =
case t of
TLocated t1 _ -> mkTInfix t1 op z
-- Just reconstruct with the TUser part being an application. If this was
-- a real error, it will be caught during renaming.
FCError -> return (o2 t z)
TUser op1 [x,y] | isLeq op1 -> doFixity (TUser op1) leqFixity x y
TApp tc [x,y]
| Just pt <- primTyFromTC tc
, Just f1 <- primTyFixity pt -> doFixity (TApp tc) f1 x y
-- In this case, we know the fixities of both sides.
mkTInfix t@(TApp (TF o1) [x,y]) op@(o2,f2) z
| Just (a1,p1) <- Map.lookup o1 tBinOpPrec =
case compareFixity (Fixity a1 p1) f2 of
FCLeft -> return (o2 t z)
FCRight -> do r <- mkTInfix y op z
return (TApp (TF o1) [x,r])
_ -> return (o2 t z)
-- As the fixity table is known, and this is a case where the fixity came
-- from that table, it's a real error if the fixities didn't work out.
FCError -> panic "Renamer" [ "fixity problem for type operators"
, show (o2 t z) ]
where
doFixity mk f1 x y =
case compareFixity f1 f2 of
FCLeft -> return (o2 t z)
FCRight -> do r <- mkTInfix y op z
return (mk [x,r])
mkTInfix (TLocated t _) op z =
mkTInfix t op z
-- As the fixity table is known, and this is a case where the fixity came
-- from that table, it's a real error if the fixities didn't work out.
FCError -> panic "Renamer" [ "fixity problem for type operators"
, show (o2 t z) ]
mkTInfix t (op,_) z =
return (op t z)
-- | When possible, rewrite the type operator to a known constructor, otherwise
@ -721,7 +703,7 @@ mkTInfix t (op,_) z =
lookupFixity :: Located PName -> (TOp,Fixity)
lookupFixity op =
case lkp of
Just (p,f) -> (\x y -> TApp (TF p) [x,y], f)
Just res -> res
-- unknown type operator, just use default fixity
-- NOTE: this works for the props defined above, as all other operators
@ -730,9 +712,22 @@ lookupFixity op =
where
sym = thing op
lkp = do (_,n) <- Map.lookup (thing op) tfunNames
(fAssoc,fLevel) <- Map.lookup n tBinOpPrec
return (n,Fixity { .. })
lkp = do pt <- primTyFromPName (thing op)
fi <- primTyFixity pt
return (\x y -> TApp (primTyCon pt) [x,y], fi)
`mplus`
do guard (isLeq sym)
return (\x y -> TUser sym [x,y], leqFixity)
leqFixity :: Fixity
leqFixity = Fixity NonAssoc 30
leqIdent :: Ident
leqIdent = packInfix "<="
isLeq :: PName -> Bool
isLeq x = getIdent x == leqIdent
-- | Rename a binding.
instance Rename Bind where

2
src/Cryptol/Parser.y
View File

@ -31,7 +31,7 @@ import Data.Text(Text)
import qualified Data.Text as T
import Control.Monad(liftM2,msum)
import Cryptol.Prims.Syntax
import Cryptol.Prims.Syntax(TFun(..))
import Cryptol.Parser.AST
import Cryptol.Parser.Position
import Cryptol.Parser.LexerUtils hiding (mkIdent)

16
src/Cryptol/Parser/AST.hs
View File

@ -29,7 +29,7 @@ module Cryptol.Parser.AST
, Schema(..)
, TParam(..)
, Kind(..)
, Type(..), tconNames
, Type(..)
, Prop(..)
-- * Declarations
@ -75,14 +75,13 @@ import Cryptol.Parser.Fixity
import Cryptol.Parser.Name
import Cryptol.Parser.Position
import Cryptol.Parser.Selector
import Cryptol.TypeCheck.Type (TCon(..), TC(..))
import Cryptol.TypeCheck.Type (TCon(..))
import Cryptol.Utils.Ident
import Cryptol.Utils.PP
import Data.List(intersperse)
import Data.Bits(shiftR)
import Data.Maybe (catMaybes)
import qualified Data.Map as Map
import Numeric(showIntAtBase)
import GHC.Generics (Generic)
@ -336,17 +335,6 @@ data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@
| TInfix (Type n) (Located n) Fixity (Type n) -- ^ @ ty + ty @
deriving (Eq, Show, Generic, NFData, Functor)
-- | NOTE: the renamer assumed that these don't have type parameters.
-- If this changes, we should update it.
-- XXX: As in the case of TApp, this would all go away if these were
-- just declared.
tconNames :: Map.Map PName TC
tconNames = Map.fromList
[ (mkUnqual (packIdent "Bit"), TCBit)
, (mkUnqual (packIdent "Integer"), TCInteger)
, (mkUnqual (packIdent "Z"), TCIntMod)
, (mkUnqual (packIdent "inf"), TCInf)
]
data Prop n = CFin (Type n) -- ^ @ fin x @
| CEqual (Type n) (Type n) -- ^ @ x == 10 @

434
src/Cryptol/Prims/Syntax.hs
View File

@ -1,26 +1,315 @@
-- |
-- Module : Cryptol.Prims.Syntax
-- Copyright : (c) 2013-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.Prims.Syntax
( TFun(..), tBinOpPrec, tfunNames
) where
import Cryptol.Parser.Name (PName,mkUnqual)
import Cryptol.Utils.Ident (packIdent,packInfix)
import Cryptol.Utils.PP
import qualified Data.Map as Map
{-# Language DeriveGeneric, DeriveAnyClass #-}
module Cryptol.Prims.Syntax where
import GHC.Generics (Generic)
import Control.DeepSeq
import qualified Data.Map as Map
-- | Built-in types.
import Cryptol.Parser.Name
import Cryptol.Parser.Selector
import Cryptol.Parser.Fixity
import qualified Cryptol.ModuleSystem.Name as M
import Cryptol.Utils.Ident
import Cryptol.Utils.PP
-- | Information about a user visible built-in type.
data PrimTy = PrimTy
{ primTyCon :: !TCon -- ^ Use this ty-con (renamer)
, primTyIdent :: !Ident -- ^ This is what it's called
, primTyDoc :: !String -- ^ Documentation
, primTyFixity :: !(Maybe Fixity) -- ^ Precedence, for infix ones
}
instance Eq PrimTy where
x == y = primTyCon x == primTyCon y
instance Ord PrimTy where
compare x y = compare (primTyCon x) (primTyCon y)
-- | This list should contain all user-visible built-in types.
primTyList :: [ PrimTy ]
primTyList =
[ -- Value type constructors -------------------------------------------------
tPrefix "inf" TC TCInf
"A numeric type representing infinity."
, tPrefix "Bit" TC TCBit
"The type of boolean values."
, tPrefix "Integer" TC TCInteger
"The type of unbounded integers."
, tPrefix "Z" TC TCIntMod
"`Z n` is the type of integers, modulo `n`."
-- Predicate constructors --------------------------------------------------
, tInfix "==" PC PEqual (n 20)
"Assert that two numeric types are equal."
, tInfix "!=" PC PNeq (n 20)
"Assert that two numeric types are different."
, tInfix ">=" PC PGeq (n 30)
"Assert that the first numeric type is larger than, or equal to the second."
, tPrefix "fin" PC PFin
"Assert that a numeric type is a proper natural number (not `inf`)."
, tPrefix "Zero" PC PZero
"Value types that have a notion of `zero`."
, tPrefix "Logic" PC PLogic
"Value types that support logical operations."
, tPrefix "Arith" PC PArith
"Value types that support arithmetic."
, tPrefix "Cmp" PC PCmp
"Value types that support unsigned comparisons."
, tPrefix "SignedCmp" PC PSignedCmp
"Values types that support signed comparisons."
, tPrefix "Literal" PC PLiteral
"`Literal n a` asserts that type `a` contains the value `n`."
-- Type functions ------------------------------------------------
, tInfix "+" TF TCAdd (l 80)
"Add numeric types."
, tInfix "-" TF TCSub (l 80)
"Subtract numeric types"
, tInfix "*" TF TCMul (l 90)
"Multiply numeric types"
, tInfix "/" TF TCDiv (l 90)
"Divide numeric types, rounding down."
, tInfix "%" TF TCMod (l 90)
"Reminder of numeric type division."
, tInfix "^^" TF TCExp (r 95)
"Exponentiate numeric types."
, tPrefix "width" TF TCWidth
"The number of bits required to represent the value of a numeric type."
, tPrefix "min" TF TCMin
"The smallest of two numeric types."
, tPrefix "max" TF TCMax
"The largest of two numeric types."
, tInfix "/^" TF TCCeilDiv (l 90)
"Divide numeric types, rounding up."
, tInfix "%^" TF TCCeilMod (l 90)
"How much we need to add to make a proper multiple of the second argument."
, tPrefix "lengthFromThen" TF TCLenFromThen
"The length of an enumeration."
, tPrefix "lengthFromThenTo" TF TCLenFromThenTo
"The length of an enumeration."
]
where
r x = Fixity { fAssoc = RightAssoc, fLevel = x }
l x = Fixity { fAssoc = LeftAssoc, fLevel = x }
n x = Fixity { fAssoc = NonAssoc, fLevel = x }
tPrefix x mk tc d =
PrimTy { primTyCon = mk tc
, primTyIdent = packIdent x
, primTyDoc = d
, primTyFixity = Nothing
}
tInfix x mk tc f d =
PrimTy { primTyCon = mk tc
, primTyIdent = packInfix x
, primTyDoc = d
, primTyFixity = Just f
}
--------------------------------------------------------------------------------
-- Indexes for quick access
-- | Construct an index for quick lookup of primtys.
primTyIx :: Ord a => (PrimTy -> Maybe a) -> a -> Maybe PrimTy
primTyIx toKey = \x -> Map.lookup x mp
where mp = Map.fromList [ (k,x) | x <- primTyList, Just k <- [ toKey x ] ]
{-# Inline primTyIx #-}
-- | Lookup a prim type by a parser name.
primTyFromPName :: PName -> Maybe PrimTy
primTyFromPName = primTyIx $ \t -> Just (mkUnqual (primTyIdent t))
-- | Lookup if a ty con is a primitive.
primTyFromTC :: TCon -> Maybe PrimTy
primTyFromTC = primTyIx $ \t -> Just (primTyCon t)
-- | Lookup a 'TFun' prim type.
primTyFromTF :: TFun -> Maybe PrimTy
primTyFromTF = primTyIx $ \t ->
case primTyCon t of
TF tf -> Just tf
_ -> Nothing
-- | Lookup a 'PC' prim type.
primTyFromPC :: PC -> Maybe PrimTy
primTyFromPC = primTyIx $ \t ->
case primTyCon t of
PC tf -> Just tf
_ -> Nothing
--------------------------------------------------------------------------------
infixr 5 :->
-- | Kinds, classify types.
data Kind = KType
| KNum
| KProp
| Kind :-> Kind
deriving (Eq, Ord, Show, Generic, NFData)
class HasKind t where
kindOf :: t -> Kind
instance HasKind TCon where
kindOf (TC tc) = kindOf tc
kindOf (PC pc) = kindOf pc
kindOf (TF tf) = kindOf tf
kindOf (TError k _) = k
instance HasKind UserTC where
kindOf (UserTC _ k) = k
instance HasKind TC where
kindOf tcon =
case tcon of
TCNum _ -> KNum
TCInf -> KNum
TCBit -> KType
TCInteger -> KType
TCIntMod -> KNum :-> KType
TCSeq -> KNum :-> KType :-> KType
TCFun -> KType :-> KType :-> KType
TCTuple n -> foldr (:->) KType (replicate n KType)
TCNewtype x -> kindOf x
instance HasKind PC where
kindOf pc =
case pc of
PEqual -> KNum :-> KNum :-> KProp
PNeq -> KNum :-> KNum :-> KProp
PGeq -> KNum :-> KNum :-> KProp
PFin -> KNum :-> KProp
PHas _ -> KType :-> KType :-> KProp
PZero -> KType :-> KProp
PLogic -> KType :-> KProp
PArith -> KType :-> KProp
PCmp -> KType :-> KProp
PSignedCmp -> KType :-> KProp
PLiteral -> KNum :-> KType :-> KProp
PAnd -> KProp :-> KProp :-> KProp
PTrue -> KProp
instance HasKind TFun where
kindOf tfun =
case tfun of
TCWidth -> KNum :-> KNum
TCAdd -> KNum :-> KNum :-> KNum
TCSub -> KNum :-> KNum :-> KNum
TCMul -> KNum :-> KNum :-> KNum
TCDiv -> KNum :-> KNum :-> KNum
TCMod -> KNum :-> KNum :-> KNum
TCExp -> KNum :-> KNum :-> KNum
TCMin -> KNum :-> KNum :-> KNum
TCMax -> KNum :-> KNum :-> KNum
TCCeilDiv -> KNum :-> KNum :-> KNum
TCCeilMod -> KNum :-> KNum :-> KNum
TCLenFromThen -> KNum :-> KNum :-> KNum :-> KNum
TCLenFromThenTo -> KNum :-> KNum :-> KNum :-> KNum
-- | Type constants.
data TCon = TC TC | PC PC | TF TFun | TError Kind TCErrorMessage
deriving (Show, Eq, Ord, Generic, NFData)
-- | Predicate symbols.
-- If you add additional user-visible constructors, please update 'primTys'.
data PC = PEqual -- ^ @_ == _@
| PNeq -- ^ @_ /= _@
| PGeq -- ^ @_ >= _@
| PFin -- ^ @fin _@
-- classes
| PHas Selector -- ^ @Has sel type field@ does not appear in schemas
| PZero -- ^ @Zero _@
| PLogic -- ^ @Logic _@
| PArith -- ^ @Arith _@
| PCmp -- ^ @Cmp _@
| PSignedCmp -- ^ @SignedCmp _@
| PLiteral -- ^ @Literal _ _@
| PAnd -- ^ This is useful when simplifying things in place
| PTrue -- ^ Ditto
deriving (Show, Eq, Ord, Generic, NFData)
-- | 1-1 constants.
-- If you add additional user-visible constructors, please update 'primTys'.
data TC = TCNum Integer -- ^ Numbers
| TCInf -- ^ Inf
| TCBit -- ^ Bit
| TCInteger -- ^ Integer
| TCIntMod -- ^ @Z _@
| TCSeq -- ^ @[_] _@
| TCFun -- ^ @_ -> _@
| TCTuple Int -- ^ @(_, _, _)@
| TCNewtype UserTC -- ^ user-defined, @T@
deriving (Show, Eq, Ord, Generic, NFData)
data UserTC = UserTC M.Name Kind
deriving (Show, Generic, NFData)
instance Eq UserTC where
UserTC x _ == UserTC y _ = x == y
instance Ord UserTC where
compare (UserTC x _) (UserTC y _) = compare x y
data TCErrorMessage = TCErrorMessage
{ tcErrorMessage :: !String
-- XXX: Add location?
} deriving (Show, Eq, Ord, Generic, NFData)
-- | Built-in type functions.
-- If you add additional user-visible constructors,
-- please update 'primTys' in "Cryptol.Prims.Types".
data TFun
= TCAdd -- ^ @ : Num -> Num -> Num @
@ -44,42 +333,87 @@ data TFun
deriving (Show, Eq, Ord, Bounded, Enum, Generic, NFData)
tBinOpPrec :: Map.Map TFun (Assoc,Int)
tBinOpPrec = mkMap t_table
where
mkMap t = Map.fromList [ (op,(a,n)) | ((a,ops),n) <- zip t [1..] , op <- ops ]
-- lowest to highest
t_table =
[ (LeftAssoc, [ TCAdd, TCSub ])
, (LeftAssoc, [ TCMul, TCDiv, TCMod, TCCeilDiv, TCCeilMod ])
, (RightAssoc, [ TCExp ])
]
-- | Type functions, with their arity and function constructor.
tfunNames :: Map.Map PName (Int,TFun)
tfunNames = Map.fromList
[ tinfix "+" 2 TCAdd
, tinfix "-" 2 TCSub
, tinfix "*" 2 TCMul
, tinfix "/" 2 TCDiv
, tinfix "%" 2 TCMod
, tinfix "^^" 2 TCExp
, tprefix "width" 1 TCWidth
, tprefix "min" 2 TCMin
, tprefix "max" 2 TCMax
, tprefix "/^" 2 TCCeilDiv
, tprefix "%^" 2 TCCeilMod
, tprefix "lengthFromThen" 3 TCLenFromThen
, tprefix "lengthFromThenTo" 3 TCLenFromThenTo
]
where
--------------------------------------------------------------------------------
-- Pretty printing
instance PP Kind where
ppPrec p k = case k of
KType -> char '*'
KNum -> char '#'
KProp -> text "Prop"
l :-> r -> optParens (p >= 1) (sep [ppPrec 1 l, text "->", ppPrec 0 r])
instance PP TCon where
ppPrec _ (TC tc) = pp tc
ppPrec _ (PC tc) = pp tc
ppPrec _ (TF tc) = pp tc
ppPrec _ (TError _ msg) = pp msg
instance PPName TCon where
ppNameFixity (TC _) = Nothing
ppNameFixity (PC _) = Nothing
ppNameFixity (TF tf) = ppNameFixity tf
ppNameFixity (TError _ _) = Nothing
ppPrefixName (TC tc) = pp tc
ppPrefixName (PC pc) = pp pc
ppPrefixName (TF tf) = ppPrefixName tf
ppPrefixName (TError _ msg) = pp msg
ppInfixName (TC tc) = pp tc
ppInfixName (PC pc) = pp pc
ppInfixName (TF tf) = ppInfixName tf
ppInfixName (TError _ msg) = pp msg
instance PP TCErrorMessage where
ppPrec _ tc = parens (text "error:" <+> text (tcErrorMessage tc))
instance PP PC where
ppPrec _ x =
case x of
PEqual -> text "(==)"
PNeq -> text "(/=)"
PGeq -> text "(>=)"
PFin -> text "fin"
PHas sel -> parens (ppSelector sel)
PZero -> text "Zero"
PLogic -> text "Logic"
PArith -> text "Arith"
PCmp -> text "Cmp"
PSignedCmp -> text "SignedCmp"
PLiteral -> text "Literal"
PTrue -> text "True"
PAnd -> text "(&&)"
instance PP TC where
ppPrec _ x =
case x of
TCNum n -> integer n
TCInf -> text "inf"
TCBit -> text "Bit"
TCInteger -> text "Integer"
TCIntMod -> text "Z"
TCSeq -> text "[]"
TCFun -> text "(->)"
TCTuple 0 -> text "()"
TCTuple 1 -> text "(one tuple?)"
TCTuple n -> parens $ hcat $ replicate (n-1) comma
TCNewtype u -> pp u
instance PP UserTC where
ppPrec p (UserTC x _) = ppPrec p x
tprefix n a p = (mkUnqual (packIdent n), (a,p))
tinfix n a p = (mkUnqual (packInfix n), (a,p))
instance PPName TFun where
ppNameFixity f = Map.lookup f tBinOpPrec
ppNameFixity f =
do pt <- primTyFromTF f
fi <- primTyFixity pt
return (fAssoc fi, fLevel fi)
ppPrefixName TCAdd = text "(+)"
ppPrefixName TCSub = text "(-)"

204
src/Cryptol/TypeCheck/Type.hs
View File

@ -3,13 +3,14 @@
{-# Language PatternGuards #-}
{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.Type
(module Cryptol.TypeCheck.Type, TFun(..)) where
( module Cryptol.TypeCheck.Type
, module Cryptol.Prims.Syntax
) where
import GHC.Generics (Generic)
import Control.DeepSeq
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import Data.Set (Set)
import qualified Data.Set as Set
@ -17,6 +18,7 @@ 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.Prims.Syntax
@ -28,17 +30,9 @@ import Prelude
infix 4 =#=, >==
infixr 5 `tFun`
infixr 5 :->
-- | Kinds, classify types.
data Kind = KType
| KNum
| KProp
| Kind :-> Kind
deriving (Eq, Ord, Show, Generic, NFData)
-- | The types of polymorphic values.
data Schema = Forall { sVars :: [TParam], sProps :: [Prop], sType :: Type }
deriving (Eq, Show, Generic, NFData)
@ -167,52 +161,6 @@ tvSourceName tvs =
type Prop = Type
-- | Type constants.
data TCon = TC TC | PC PC | TF TFun | TError Kind TCErrorMessage
deriving (Show, Eq, Ord, Generic, NFData)
-- | Predicate symbols.
data PC = PEqual -- ^ @_ == _@
| PNeq -- ^ @_ /= _@
| PGeq -- ^ @_ >= _@
| PFin -- ^ @fin _@
-- classes
| PHas Selector -- ^ @Has sel type field@ does not appear in schemas
| PZero -- ^ @Zero _@
| PLogic -- ^ @Logic _@
| PArith -- ^ @Arith _@
| PCmp -- ^ @Cmp _@
| PSignedCmp -- ^ @SignedCmp _@
| PLiteral -- ^ @Literal _ _@
| PAnd -- ^ This is useful when simplifying things in place
| PTrue -- ^ Ditto
deriving (Show, Eq, Ord, Generic, NFData)
-- | 1-1 constants.
data TC = TCNum Integer -- ^ Numbers
| TCInf -- ^ Inf
| TCBit -- ^ Bit
| TCInteger -- ^ Integer
| TCIntMod -- ^ @Z _@
| TCSeq -- ^ @[_] _@
| TCFun -- ^ @_ -> _@
| TCTuple Int -- ^ @(_, _, _)@
| TCNewtype UserTC -- ^ user-defined, @T@
deriving (Show, Eq, Ord, Generic, NFData)
data UserTC = UserTC Name Kind
deriving (Show, Generic, NFData)
data TCErrorMessage = TCErrorMessage
{ tcErrorMessage :: !String
-- XXX: Add location?
} deriving (Show, Eq, Ord, Generic, NFData)
@ -243,71 +191,10 @@ data Newtype = Newtype { ntName :: Name
--------------------------------------------------------------------------------
class HasKind t where
kindOf :: t -> Kind
instance HasKind TVar where
kindOf (TVFree _ k _ _) = k
kindOf (TVBound tp) = kindOf tp
instance HasKind TCon where
kindOf (TC tc) = kindOf tc
kindOf (PC pc) = kindOf pc
kindOf (TF tf) = kindOf tf
kindOf (TError k _) = k
instance HasKind UserTC where
kindOf (UserTC _ k) = k
instance HasKind TC where
kindOf tcon =
case tcon of
TCNum _ -> KNum
TCInf -> KNum
TCBit -> KType
TCInteger -> KType
TCIntMod -> KNum :-> KType
TCSeq -> KNum :-> KType :-> KType
TCFun -> KType :-> KType :-> KType
TCTuple n -> foldr (:->) KType (replicate n KType)
TCNewtype x -> kindOf x
instance HasKind PC where
kindOf pc =
case pc of
PEqual -> KNum :-> KNum :-> KProp
PNeq -> KNum :-> KNum :-> KProp
PGeq -> KNum :-> KNum :-> KProp
PFin -> KNum :-> KProp
PHas _ -> KType :-> KType :-> KProp
PZero -> KType :-> KProp
PLogic -> KType :-> KProp
PArith -> KType :-> KProp
PCmp -> KType :-> KProp
PSignedCmp -> KType :-> KProp
PLiteral -> KNum :-> KType :-> KProp
PAnd -> KProp :-> KProp :-> KProp
PTrue -> KProp
instance HasKind TFun where
kindOf tfun =
case tfun of
TCWidth -> KNum :-> KNum
TCAdd -> KNum :-> KNum :-> KNum
TCSub -> KNum :-> KNum :-> KNum
TCMul -> KNum :-> KNum :-> KNum
TCDiv -> KNum :-> KNum :-> KNum
TCMod -> KNum :-> KNum :-> KNum
TCExp -> KNum :-> KNum :-> KNum
TCMin -> KNum :-> KNum :-> KNum
TCMax -> KNum :-> KNum :-> KNum
TCCeilDiv -> KNum :-> KNum :-> KNum
TCCeilMod -> KNum :-> KNum :-> KNum
TCLenFromThen -> KNum :-> KNum :-> KNum :-> KNum
TCLenFromThenTo -> KNum :-> KNum :-> KNum :-> KNum
instance HasKind Type where
kindOf ty =
case ty of
@ -391,14 +278,6 @@ newtypeConType nt =
as = ntParams nt
instance Eq UserTC where
UserTC x _ == UserTC y _ = x == y
instance Ord UserTC where
compare (UserTC x _) (UserTC y _) = compare x y
instance Eq TVar where
TVBound x == TVBound y = x == y
TVFree x _ _ _ == TVFree y _ _ _ = x == y
@ -915,19 +794,15 @@ instance PP (WithNames Type) where
isTInfix (WithNames (TCon (TF ieOp) [ieLeft',ieRight']) _) =
do let ieLeft = WithNames ieLeft' nmMap
ieRight = WithNames ieRight' nmMap
(ieAssoc,iePrec) <- Map.lookup ieOp tBinOpPrec
pt <- primTyFromTF ieOp
fi <- primTyFixity pt
let ieAssoc = fAssoc fi
iePrec = fLevel fi
return Infix { .. }
isTInfix _ = Nothing
instance PP Kind where
ppPrec p k = case k of
KType -> char '*'
KNum -> char '#'
KProp -> text "Prop"
l :-> r -> optParens (p >= 1) (sep [ppPrec 1 l, text "->", ppPrec 0 r])
instance PP (WithNames TVar) where
ppPrec _ (WithNames (TVBound x) mp) =
@ -972,72 +847,9 @@ pickTVarName k src uni =
instance PP TVar where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP Type where
ppPrec n t = ppWithNamesPrec IntMap.empty n t
instance PP TCon where
ppPrec _ (TC tc) = pp tc
ppPrec _ (PC tc) = pp tc
ppPrec _ (TF tc) = pp tc
ppPrec _ (TError _ msg) = pp msg
instance PPName TCon where
ppNameFixity (TC _) = Nothing
ppNameFixity (PC _) = Nothing
ppNameFixity (TF tf) = ppNameFixity tf
ppNameFixity (TError _ _) = Nothing
ppPrefixName (TC tc) = pp tc
ppPrefixName (PC pc) = pp pc
ppPrefixName (TF tf) = ppPrefixName tf
ppPrefixName (TError _ msg) = pp msg
ppInfixName (TC tc) = pp tc
ppInfixName (PC pc) = pp pc
ppInfixName (TF tf) = ppInfixName tf
ppInfixName (TError _ msg) = pp msg
instance PP TCErrorMessage where
ppPrec _ tc = parens (text "error:" <+> text (tcErrorMessage tc))
instance PP PC where
ppPrec _ x =
case x of
PEqual -> text "(==)"
PNeq -> text "(/=)"
PGeq -> text "(>=)"
PFin -> text "fin"
PHas sel -> parens (ppSelector sel)
PZero -> text "Zero"
PLogic -> text "Logic"
PArith -> text "Arith"
PCmp -> text "Cmp"
PSignedCmp -> text "SignedCmp"
PLiteral -> text "Literal"
PTrue -> text "True"
PAnd -> text "(&&)"
instance PP TC where
ppPrec _ x =
case x of
TCNum n -> integer n
TCInf -> text "inf"
TCBit -> text "Bit"
TCInteger -> text "Integer"
TCIntMod -> text "Z"
TCSeq -> text "[]"
TCFun -> text "(->)"
TCTuple 0 -> text "()"
TCTuple 1 -> text "(one tuple?)"
TCTuple n -> parens $ hcat $ replicate (n-1) comma
TCNewtype u -> pp u
instance PP UserTC where
ppPrec p (UserTC x _) = ppPrec p x
instance PP TVarInfo where
ppPrec _ tvinfo = pp (tvarDesc tvinfo) <+> loc
where