{-# Language DeriveGeneric, DeriveAnyClass #-}
module Cryptol.TypeCheck.TCon where
import qualified Data.Map as Map
import GHC.Generics (Generic)
import Control.DeepSeq
import Cryptol.Parser.Selector
import Cryptol.Parser.Fixity
import qualified Cryptol.ModuleSystem.Name as M
import Cryptol.Utils.Ident
import Cryptol.Utils.PP
infixPrimTy :: TCon -> Maybe (Ident,Fixity)
infixPrimTy :: TCon -> Maybe (Ident, Fixity)
infixPrimTy = \tc :: TCon
tc -> TCon -> Map TCon (Ident, Fixity) -> Maybe (Ident, Fixity)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TCon
tc Map TCon (Ident, Fixity)
mp
where
mp :: Map TCon (Ident, Fixity)
mp = [(TCon, (Ident, Fixity))] -> Map TCon (Ident, Fixity)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ String -> (PC -> TCon) -> PC -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix "==" PC -> TCon
PC PC
PEqual (Int -> Fixity
n 20)
, String -> (PC -> TCon) -> PC -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix "!=" PC -> TCon
PC PC
PNeq (Int -> Fixity
n 20)
, String -> (PC -> TCon) -> PC -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix ">=" PC -> TCon
PC PC
PGeq (Int -> Fixity
n 30)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix "+" TFun -> TCon
TF TFun
TCAdd (Int -> Fixity
l 80)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix "-" TFun -> TCon
TF TFun
TCSub (Int -> Fixity
l 80)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix "*" TFun -> TCon
TF TFun
TCMul (Int -> Fixity
l 90)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix "/" TFun -> TCon
TF TFun
TCDiv (Int -> Fixity
l 90)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix "%" TFun -> TCon
TF TFun
TCMod (Int -> Fixity
l 90)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix "^^" TFun -> TCon
TF TFun
TCExp (Int -> Fixity
r 95)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix "/^" TFun -> TCon
TF TFun
TCCeilDiv (Int -> Fixity
l 90)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall t a b. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix "%^" TFun -> TCon
TF TFun
TCCeilMod (Int -> Fixity
l 90)
]
r :: Int -> Fixity
r x :: Int
x = $WFixity :: Assoc -> Int -> Fixity
Fixity { fAssoc :: Assoc
fAssoc = Assoc
RightAssoc, fLevel :: Int
fLevel = Int
x }
l :: Int -> Fixity
l x :: Int
x = $WFixity :: Assoc -> Int -> Fixity
Fixity { fAssoc :: Assoc
fAssoc = Assoc
LeftAssoc, fLevel :: Int
fLevel = Int
x }
n :: Int -> Fixity
n x :: Int
x = $WFixity :: Assoc -> Int -> Fixity
Fixity { fAssoc :: Assoc
fAssoc = Assoc
NonAssoc, fLevel :: Int
fLevel = Int
x }
tInfix :: String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix x :: String
x mk :: t -> a
mk tc :: t
tc f :: b
f = (t -> a
mk t
tc, (String -> Ident
packIdent String
x, b
f))
builtInType :: M.Name -> Maybe TCon
builtInType :: Name -> Maybe TCon
builtInType nm :: Name
nm =
case Name -> NameInfo
M.nameInfo Name
nm of
M.Declared m :: ModName
m _
| ModName
m ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
preludeName -> Ident -> Map Ident TCon -> Maybe TCon
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Name -> Ident
M.nameIdent Name
nm) Map Ident TCon
builtInTypes
_ -> Maybe TCon
forall a. Maybe a
Nothing
where
x :: String
x ~> :: String -> b -> (Ident, b)
~> y :: b
y = (String -> Ident
packIdent String
x, b
y)
builtInTypes :: Map Ident TCon
builtInTypes = [(Ident, TCon)] -> Map Ident TCon
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[
"inf" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCInf
, "Bit" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCBit
, "Integer" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCInteger
, "Z" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCIntMod
, "==" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PEqual
, "!=" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PNeq
, ">=" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PGeq
, "fin" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PFin
, "Zero" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PZero
, "Logic" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PLogic
, "Arith" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PArith
, "Cmp" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PCmp
, "SignedCmp" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PSignedCmp
, "Literal" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PLiteral
, "+" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCAdd
, "-" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCSub
, "*" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMul
, "/" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCDiv
, "%" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMod
, "^^" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCExp
, "width" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCWidth
, "min" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMin
, "max" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMax
, "/^" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCCeilDiv
, "%^" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCCeilMod
, "lengthFromThenTo" String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCLenFromThenTo
]
infixr 5 :->
data Kind = KType
| KNum
| KProp
| Kind :-> Kind
deriving (Kind -> Kind -> Bool
(Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Kind -> Kind -> Bool
$c/= :: Kind -> Kind -> Bool
== :: Kind -> Kind -> Bool
$c== :: Kind -> Kind -> Bool
Eq, Eq Kind
Eq Kind =>
(Kind -> Kind -> Ordering)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Kind)
-> (Kind -> Kind -> Kind)
-> Ord Kind
Kind -> Kind -> Bool
Kind -> Kind -> Ordering
Kind -> Kind -> Kind
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Kind -> Kind -> Kind
$cmin :: Kind -> Kind -> Kind
max :: Kind -> Kind -> Kind
$cmax :: Kind -> Kind -> Kind
>= :: Kind -> Kind -> Bool
$c>= :: Kind -> Kind -> Bool
> :: Kind -> Kind -> Bool
$c> :: Kind -> Kind -> Bool
<= :: Kind -> Kind -> Bool
$c<= :: Kind -> Kind -> Bool
< :: Kind -> Kind -> Bool
$c< :: Kind -> Kind -> Bool
compare :: Kind -> Kind -> Ordering
$ccompare :: Kind -> Kind -> Ordering
$cp1Ord :: Eq Kind
Ord, Int -> Kind -> ShowS
[Kind] -> ShowS
Kind -> String
(Int -> Kind -> ShowS)
-> (Kind -> String) -> ([Kind] -> ShowS) -> Show Kind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Kind] -> ShowS
$cshowList :: [Kind] -> ShowS
show :: Kind -> String
$cshow :: Kind -> String
showsPrec :: Int -> Kind -> ShowS
$cshowsPrec :: Int -> Kind -> ShowS
Show, (forall x. Kind -> Rep Kind x)
-> (forall x. Rep Kind x -> Kind) -> Generic Kind
forall x. Rep Kind x -> Kind
forall x. Kind -> Rep Kind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Kind x -> Kind
$cfrom :: forall x. Kind -> Rep Kind x
Generic, Kind -> ()
(Kind -> ()) -> NFData Kind
forall a. (a -> ()) -> NFData a
rnf :: Kind -> ()
$crnf :: Kind -> ()
NFData)
class HasKind t where
kindOf :: t -> Kind
instance HasKind TCon where
kindOf :: TCon -> Kind
kindOf (TC tc :: TC
tc) = TC -> Kind
forall t. HasKind t => t -> Kind
kindOf TC
tc
kindOf (PC pc :: PC
pc) = PC -> Kind
forall t. HasKind t => t -> Kind
kindOf PC
pc
kindOf (TF tf :: TFun
tf) = TFun -> Kind
forall t. HasKind t => t -> Kind
kindOf TFun
tf
kindOf (TError k :: Kind
k _) = Kind
k
instance HasKind UserTC where
kindOf :: UserTC -> Kind
kindOf (UserTC _ k :: Kind
k) = Kind
k
instance HasKind TC where
kindOf :: TC -> Kind
kindOf tcon :: TC
tcon =
case TC
tcon of
TCNum _ -> Kind
KNum
TCInf -> Kind
KNum
TCBit -> Kind
KType
TCInteger -> Kind
KType
TCIntMod -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KType
TCSeq -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KType
TCFun -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KType
TCTuple n :: Int
n -> (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 (Int -> Kind -> [Kind]
forall a. Int -> a -> [a]
replicate Int
n Kind
KType)
TCNewtype x :: UserTC
x -> UserTC -> Kind
forall t. HasKind t => t -> Kind
kindOf UserTC
x
TCAbstract x :: UserTC
x -> UserTC -> Kind
forall t. HasKind t => t -> Kind
kindOf UserTC
x
instance HasKind PC where
kindOf :: PC -> Kind
kindOf pc :: PC
pc =
case PC
pc of
PEqual -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KProp
PNeq -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KProp
PGeq -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KProp
PFin -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KProp
PHas _ -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PZero -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PLogic -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PArith -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PCmp -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PSignedCmp -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PLiteral -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PAnd -> Kind
KProp Kind -> Kind -> Kind
:-> Kind
KProp Kind -> Kind -> Kind
:-> Kind
KProp
PTrue -> Kind
KProp
instance HasKind TFun where
kindOf :: TFun -> Kind
kindOf tfun :: TFun
tfun =
case TFun
tfun of
TCWidth -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCAdd -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCSub -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCMul -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCDiv -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCMod -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCExp -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCMin -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCMax -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCCeilDiv -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCCeilMod -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TCLenFromThenTo -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
data TCon = TC TC | PC PC | TF TFun | TError Kind TCErrorMessage
deriving (Int -> TCon -> ShowS
[TCon] -> ShowS
TCon -> String
(Int -> TCon -> ShowS)
-> (TCon -> String) -> ([TCon] -> ShowS) -> Show TCon
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TCon] -> ShowS
$cshowList :: [TCon] -> ShowS
show :: TCon -> String
$cshow :: TCon -> String
showsPrec :: Int -> TCon -> ShowS
$cshowsPrec :: Int -> TCon -> ShowS
Show, TCon -> TCon -> Bool
(TCon -> TCon -> Bool) -> (TCon -> TCon -> Bool) -> Eq TCon
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TCon -> TCon -> Bool
$c/= :: TCon -> TCon -> Bool
== :: TCon -> TCon -> Bool
$c== :: TCon -> TCon -> Bool
Eq, Eq TCon
Eq TCon =>
(TCon -> TCon -> Ordering)
-> (TCon -> TCon -> Bool)
-> (TCon -> TCon -> Bool)
-> (TCon -> TCon -> Bool)
-> (TCon -> TCon -> Bool)
-> (TCon -> TCon -> TCon)
-> (TCon -> TCon -> TCon)
-> Ord TCon
TCon -> TCon -> Bool
TCon -> TCon -> Ordering
TCon -> TCon -> TCon
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TCon -> TCon -> TCon
$cmin :: TCon -> TCon -> TCon
max :: TCon -> TCon -> TCon
$cmax :: TCon -> TCon -> TCon
>= :: TCon -> TCon -> Bool
$c>= :: TCon -> TCon -> Bool
> :: TCon -> TCon -> Bool
$c> :: TCon -> TCon -> Bool
<= :: TCon -> TCon -> Bool
$c<= :: TCon -> TCon -> Bool
< :: TCon -> TCon -> Bool
$c< :: TCon -> TCon -> Bool
compare :: TCon -> TCon -> Ordering
$ccompare :: TCon -> TCon -> Ordering
$cp1Ord :: Eq TCon
Ord, (forall x. TCon -> Rep TCon x)
-> (forall x. Rep TCon x -> TCon) -> Generic TCon
forall x. Rep TCon x -> TCon
forall x. TCon -> Rep TCon x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TCon x -> TCon
$cfrom :: forall x. TCon -> Rep TCon x
Generic, TCon -> ()
(TCon -> ()) -> NFData TCon
forall a. (a -> ()) -> NFData a
rnf :: TCon -> ()
$crnf :: TCon -> ()
NFData)
data PC = PEqual
| PNeq
| PGeq
| PFin
| PHas Selector
| PZero
| PLogic
| PArith
| PCmp
| PSignedCmp
| PLiteral
| PAnd
| PTrue
deriving (Int -> PC -> ShowS
[PC] -> ShowS
PC -> String
(Int -> PC -> ShowS)
-> (PC -> String) -> ([PC] -> ShowS) -> Show PC
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PC] -> ShowS
$cshowList :: [PC] -> ShowS
show :: PC -> String
$cshow :: PC -> String
showsPrec :: Int -> PC -> ShowS
$cshowsPrec :: Int -> PC -> ShowS
Show, PC -> PC -> Bool
(PC -> PC -> Bool) -> (PC -> PC -> Bool) -> Eq PC
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PC -> PC -> Bool
$c/= :: PC -> PC -> Bool
== :: PC -> PC -> Bool
$c== :: PC -> PC -> Bool
Eq, Eq PC
Eq PC =>
(PC -> PC -> Ordering)
-> (PC -> PC -> Bool)
-> (PC -> PC -> Bool)
-> (PC -> PC -> Bool)
-> (PC -> PC -> Bool)
-> (PC -> PC -> PC)
-> (PC -> PC -> PC)
-> Ord PC
PC -> PC -> Bool
PC -> PC -> Ordering
PC -> PC -> PC
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PC -> PC -> PC
$cmin :: PC -> PC -> PC
max :: PC -> PC -> PC
$cmax :: PC -> PC -> PC
>= :: PC -> PC -> Bool
$c>= :: PC -> PC -> Bool
> :: PC -> PC -> Bool
$c> :: PC -> PC -> Bool
<= :: PC -> PC -> Bool
$c<= :: PC -> PC -> Bool
< :: PC -> PC -> Bool
$c< :: PC -> PC -> Bool
compare :: PC -> PC -> Ordering
$ccompare :: PC -> PC -> Ordering
$cp1Ord :: Eq PC
Ord, (forall x. PC -> Rep PC x)
-> (forall x. Rep PC x -> PC) -> Generic PC
forall x. Rep PC x -> PC
forall x. PC -> Rep PC x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PC x -> PC
$cfrom :: forall x. PC -> Rep PC x
Generic, PC -> ()
(PC -> ()) -> NFData PC
forall a. (a -> ()) -> NFData a
rnf :: PC -> ()
$crnf :: PC -> ()
NFData)
data TC = TCNum Integer
| TCInf
| TCBit
| TCInteger
| TCIntMod
| TCSeq
| TCFun
| TCTuple Int
| TCAbstract UserTC
| TCNewtype UserTC
deriving (Int -> TC -> ShowS
[TC] -> ShowS
TC -> String
(Int -> TC -> ShowS)
-> (TC -> String) -> ([TC] -> ShowS) -> Show TC
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TC] -> ShowS
$cshowList :: [TC] -> ShowS
show :: TC -> String
$cshow :: TC -> String
showsPrec :: Int -> TC -> ShowS
$cshowsPrec :: Int -> TC -> ShowS
Show, TC -> TC -> Bool
(TC -> TC -> Bool) -> (TC -> TC -> Bool) -> Eq TC
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TC -> TC -> Bool
$c/= :: TC -> TC -> Bool
== :: TC -> TC -> Bool
$c== :: TC -> TC -> Bool
Eq, Eq TC
Eq TC =>
(TC -> TC -> Ordering)
-> (TC -> TC -> Bool)
-> (TC -> TC -> Bool)
-> (TC -> TC -> Bool)
-> (TC -> TC -> Bool)
-> (TC -> TC -> TC)
-> (TC -> TC -> TC)
-> Ord TC
TC -> TC -> Bool
TC -> TC -> Ordering
TC -> TC -> TC
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TC -> TC -> TC
$cmin :: TC -> TC -> TC
max :: TC -> TC -> TC
$cmax :: TC -> TC -> TC
>= :: TC -> TC -> Bool
$c>= :: TC -> TC -> Bool
> :: TC -> TC -> Bool
$c> :: TC -> TC -> Bool
<= :: TC -> TC -> Bool
$c<= :: TC -> TC -> Bool
< :: TC -> TC -> Bool
$c< :: TC -> TC -> Bool
compare :: TC -> TC -> Ordering
$ccompare :: TC -> TC -> Ordering
$cp1Ord :: Eq TC
Ord, (forall x. TC -> Rep TC x)
-> (forall x. Rep TC x -> TC) -> Generic TC
forall x. Rep TC x -> TC
forall x. TC -> Rep TC x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TC x -> TC
$cfrom :: forall x. TC -> Rep TC x
Generic, TC -> ()
(TC -> ()) -> NFData TC
forall a. (a -> ()) -> NFData a
rnf :: TC -> ()
$crnf :: TC -> ()
NFData)
data UserTC = UserTC M.Name Kind
deriving (Int -> UserTC -> ShowS
[UserTC] -> ShowS
UserTC -> String
(Int -> UserTC -> ShowS)
-> (UserTC -> String) -> ([UserTC] -> ShowS) -> Show UserTC
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UserTC] -> ShowS
$cshowList :: [UserTC] -> ShowS
show :: UserTC -> String
$cshow :: UserTC -> String
showsPrec :: Int -> UserTC -> ShowS
$cshowsPrec :: Int -> UserTC -> ShowS
Show, (forall x. UserTC -> Rep UserTC x)
-> (forall x. Rep UserTC x -> UserTC) -> Generic UserTC
forall x. Rep UserTC x -> UserTC
forall x. UserTC -> Rep UserTC x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep UserTC x -> UserTC
$cfrom :: forall x. UserTC -> Rep UserTC x
Generic, UserTC -> ()
(UserTC -> ()) -> NFData UserTC
forall a. (a -> ()) -> NFData a
rnf :: UserTC -> ()
$crnf :: UserTC -> ()
NFData)
instance Eq UserTC where
UserTC x :: Name
x _ == :: UserTC -> UserTC -> Bool
== UserTC y :: Name
y _ = Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
instance Ord UserTC where
compare :: UserTC -> UserTC -> Ordering
compare (UserTC x :: Name
x _) (UserTC y :: Name
y _) = Name -> Name -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Name
x Name
y
data TCErrorMessage = TCErrorMessage
{ TCErrorMessage -> String
tcErrorMessage :: !String
} deriving (Int -> TCErrorMessage -> ShowS
[TCErrorMessage] -> ShowS
TCErrorMessage -> String
(Int -> TCErrorMessage -> ShowS)
-> (TCErrorMessage -> String)
-> ([TCErrorMessage] -> ShowS)
-> Show TCErrorMessage
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TCErrorMessage] -> ShowS
$cshowList :: [TCErrorMessage] -> ShowS
show :: TCErrorMessage -> String
$cshow :: TCErrorMessage -> String
showsPrec :: Int -> TCErrorMessage -> ShowS
$cshowsPrec :: Int -> TCErrorMessage -> ShowS
Show, TCErrorMessage -> TCErrorMessage -> Bool
(TCErrorMessage -> TCErrorMessage -> Bool)
-> (TCErrorMessage -> TCErrorMessage -> Bool) -> Eq TCErrorMessage
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TCErrorMessage -> TCErrorMessage -> Bool
$c/= :: TCErrorMessage -> TCErrorMessage -> Bool
== :: TCErrorMessage -> TCErrorMessage -> Bool
$c== :: TCErrorMessage -> TCErrorMessage -> Bool
Eq, Eq TCErrorMessage
Eq TCErrorMessage =>
(TCErrorMessage -> TCErrorMessage -> Ordering)
-> (TCErrorMessage -> TCErrorMessage -> Bool)
-> (TCErrorMessage -> TCErrorMessage -> Bool)
-> (TCErrorMessage -> TCErrorMessage -> Bool)
-> (TCErrorMessage -> TCErrorMessage -> Bool)
-> (TCErrorMessage -> TCErrorMessage -> TCErrorMessage)
-> (TCErrorMessage -> TCErrorMessage -> TCErrorMessage)
-> Ord TCErrorMessage
TCErrorMessage -> TCErrorMessage -> Bool
TCErrorMessage -> TCErrorMessage -> Ordering
TCErrorMessage -> TCErrorMessage -> TCErrorMessage
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage
$cmin :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage
max :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage
$cmax :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage
>= :: TCErrorMessage -> TCErrorMessage -> Bool
$c>= :: TCErrorMessage -> TCErrorMessage -> Bool
> :: TCErrorMessage -> TCErrorMessage -> Bool
$c> :: TCErrorMessage -> TCErrorMessage -> Bool
<= :: TCErrorMessage -> TCErrorMessage -> Bool
$c<= :: TCErrorMessage -> TCErrorMessage -> Bool
< :: TCErrorMessage -> TCErrorMessage -> Bool
$c< :: TCErrorMessage -> TCErrorMessage -> Bool
compare :: TCErrorMessage -> TCErrorMessage -> Ordering
$ccompare :: TCErrorMessage -> TCErrorMessage -> Ordering
$cp1Ord :: Eq TCErrorMessage
Ord, (forall x. TCErrorMessage -> Rep TCErrorMessage x)
-> (forall x. Rep TCErrorMessage x -> TCErrorMessage)
-> Generic TCErrorMessage
forall x. Rep TCErrorMessage x -> TCErrorMessage
forall x. TCErrorMessage -> Rep TCErrorMessage x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TCErrorMessage x -> TCErrorMessage
$cfrom :: forall x. TCErrorMessage -> Rep TCErrorMessage x
Generic, TCErrorMessage -> ()
(TCErrorMessage -> ()) -> NFData TCErrorMessage
forall a. (a -> ()) -> NFData a
rnf :: TCErrorMessage -> ()
$crnf :: TCErrorMessage -> ()
NFData)
data TFun
= TCAdd
| TCSub
| TCMul
| TCDiv
| TCMod
| TCExp
| TCWidth
| TCMin
| TCMax
| TCCeilDiv
| TCCeilMod
| TCLenFromThenTo
deriving (Int -> TFun -> ShowS
[TFun] -> ShowS
TFun -> String
(Int -> TFun -> ShowS)
-> (TFun -> String) -> ([TFun] -> ShowS) -> Show TFun
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TFun] -> ShowS
$cshowList :: [TFun] -> ShowS
show :: TFun -> String
$cshow :: TFun -> String
showsPrec :: Int -> TFun -> ShowS
$cshowsPrec :: Int -> TFun -> ShowS
Show, TFun -> TFun -> Bool
(TFun -> TFun -> Bool) -> (TFun -> TFun -> Bool) -> Eq TFun
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TFun -> TFun -> Bool
$c/= :: TFun -> TFun -> Bool
== :: TFun -> TFun -> Bool
$c== :: TFun -> TFun -> Bool
Eq, Eq TFun
Eq TFun =>
(TFun -> TFun -> Ordering)
-> (TFun -> TFun -> Bool)
-> (TFun -> TFun -> Bool)
-> (TFun -> TFun -> Bool)
-> (TFun -> TFun -> Bool)
-> (TFun -> TFun -> TFun)
-> (TFun -> TFun -> TFun)
-> Ord TFun
TFun -> TFun -> Bool
TFun -> TFun -> Ordering
TFun -> TFun -> TFun
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TFun -> TFun -> TFun
$cmin :: TFun -> TFun -> TFun
max :: TFun -> TFun -> TFun
$cmax :: TFun -> TFun -> TFun
>= :: TFun -> TFun -> Bool
$c>= :: TFun -> TFun -> Bool
> :: TFun -> TFun -> Bool
$c> :: TFun -> TFun -> Bool
<= :: TFun -> TFun -> Bool
$c<= :: TFun -> TFun -> Bool
< :: TFun -> TFun -> Bool
$c< :: TFun -> TFun -> Bool
compare :: TFun -> TFun -> Ordering
$ccompare :: TFun -> TFun -> Ordering
$cp1Ord :: Eq TFun
Ord, TFun
TFun -> TFun -> Bounded TFun
forall a. a -> a -> Bounded a
maxBound :: TFun
$cmaxBound :: TFun
minBound :: TFun
$cminBound :: TFun
Bounded, Int -> TFun
TFun -> Int
TFun -> [TFun]
TFun -> TFun
TFun -> TFun -> [TFun]
TFun -> TFun -> TFun -> [TFun]
(TFun -> TFun)
-> (TFun -> TFun)
-> (Int -> TFun)
-> (TFun -> Int)
-> (TFun -> [TFun])
-> (TFun -> TFun -> [TFun])
-> (TFun -> TFun -> [TFun])
-> (TFun -> TFun -> TFun -> [TFun])
-> Enum TFun
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: TFun -> TFun -> TFun -> [TFun]
$cenumFromThenTo :: TFun -> TFun -> TFun -> [TFun]
enumFromTo :: TFun -> TFun -> [TFun]
$cenumFromTo :: TFun -> TFun -> [TFun]
enumFromThen :: TFun -> TFun -> [TFun]
$cenumFromThen :: TFun -> TFun -> [TFun]
enumFrom :: TFun -> [TFun]
$cenumFrom :: TFun -> [TFun]
fromEnum :: TFun -> Int
$cfromEnum :: TFun -> Int
toEnum :: Int -> TFun
$ctoEnum :: Int -> TFun
pred :: TFun -> TFun
$cpred :: TFun -> TFun
succ :: TFun -> TFun
$csucc :: TFun -> TFun
Enum, (forall x. TFun -> Rep TFun x)
-> (forall x. Rep TFun x -> TFun) -> Generic TFun
forall x. Rep TFun x -> TFun
forall x. TFun -> Rep TFun x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TFun x -> TFun
$cfrom :: forall x. TFun -> Rep TFun x
Generic, TFun -> ()
(TFun -> ()) -> NFData TFun
forall a. (a -> ()) -> NFData a
rnf :: TFun -> ()
$crnf :: TFun -> ()
NFData)
instance PP Kind where
ppPrec :: Int -> Kind -> Doc
ppPrec p :: Int
p k :: Kind
k = case Kind
k of
KType -> Char -> Doc
char '*'
KNum -> Char -> Doc
char '#'
KProp -> String -> Doc
text "Prop"
l :: Kind
l :-> r :: Kind
r -> Bool -> Doc -> Doc
optParens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 1) ([Doc] -> Doc
sep [Int -> Kind -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec 1 Kind
l, String -> Doc
text "->", Int -> Kind -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec 0 Kind
r])
instance PP TCon where
ppPrec :: Int -> TCon -> Doc
ppPrec _ (TC tc :: TC
tc) = TC -> Doc
forall a. PP a => a -> Doc
pp TC
tc
ppPrec _ (PC tc :: PC
tc) = PC -> Doc
forall a. PP a => a -> Doc
pp PC
tc
ppPrec _ (TF tc :: TFun
tc) = TFun -> Doc
forall a. PP a => a -> Doc
pp TFun
tc
ppPrec _ (TError _ msg :: TCErrorMessage
msg) = TCErrorMessage -> Doc
forall a. PP a => a -> Doc
pp TCErrorMessage
msg
instance PP TCErrorMessage where
ppPrec :: Int -> TCErrorMessage -> Doc
ppPrec _ tc :: TCErrorMessage
tc = Doc -> Doc
parens (String -> Doc
text "error:" Doc -> Doc -> Doc
<+> String -> Doc
text (TCErrorMessage -> String
tcErrorMessage TCErrorMessage
tc))
instance PP PC where
ppPrec :: Int -> PC -> Doc
ppPrec _ x :: PC
x =
case PC
x of
PEqual -> String -> Doc
text "(==)"
PNeq -> String -> Doc
text "(/=)"
PGeq -> String -> Doc
text "(>=)"
PFin -> String -> Doc
text "fin"
PHas sel :: Selector
sel -> Doc -> Doc
parens (Selector -> Doc
ppSelector Selector
sel)
PZero -> String -> Doc
text "Zero"
PLogic -> String -> Doc
text "Logic"
PArith -> String -> Doc
text "Arith"
PCmp -> String -> Doc
text "Cmp"
PSignedCmp -> String -> Doc
text "SignedCmp"
PLiteral -> String -> Doc
text "Literal"
PTrue -> String -> Doc
text "True"
PAnd -> String -> Doc
text "(&&)"
instance PP TC where
ppPrec :: Int -> TC -> Doc
ppPrec _ x :: TC
x =
case TC
x 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 -> String -> Doc
text "Z"
TCSeq -> String -> Doc
text "[]"
TCFun -> String -> Doc
text "(->)"
TCTuple 0 -> String -> Doc
text "()"
TCTuple 1 -> String -> Doc
text "(one tuple?)"
TCTuple n :: Int
n -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) Doc
comma
TCNewtype u :: UserTC
u -> UserTC -> Doc
forall a. PP a => a -> Doc
pp UserTC
u
TCAbstract u :: UserTC
u -> UserTC -> Doc
forall a. PP a => a -> Doc
pp UserTC
u
instance PP UserTC where
ppPrec :: Int -> UserTC -> Doc
ppPrec p :: Int
p (UserTC x :: Name
x _) = Int -> Name -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
p Name
x
instance PP TFun where
ppPrec :: Int -> TFun -> Doc
ppPrec _ tcon :: TFun
tcon =
case TFun
tcon of
TCAdd -> String -> Doc
text "+"
TCSub -> String -> Doc
text "-"
TCMul -> String -> Doc
text "*"
TCDiv -> String -> Doc
text "/"
TCMod -> String -> Doc
text "%"
TCExp -> String -> Doc
text "^^"
TCWidth -> String -> Doc
text "width"
TCMin -> String -> Doc
text "min"
TCMax -> String -> Doc
text "max"
TCCeilDiv -> String -> Doc
text "/^"
TCCeilMod -> String -> Doc
text "%^"
TCLenFromThenTo -> String -> Doc
text "lengthFromThenTo"