{-# Language OverloadedStrings, DeriveGeneric, DeriveAnyClass, Safe #-}
module Cryptol.TypeCheck.TCon where
import qualified Data.Map as Map
import GHC.Generics (Generic)
import Control.DeepSeq
import Cryptol.Parser.Selector
import qualified Cryptol.ModuleSystem.Name as M
import Cryptol.Utils.Fixity
import Cryptol.Utils.Ident
import Cryptol.Utils.PP
infixPrimTy :: TCon -> Maybe (Ident,Fixity)
infixPrimTy :: TCon -> Maybe (Ident, Fixity)
infixPrimTy = \TCon
tc -> 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 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"==" PC -> TCon
PC PC
PEqual (Int -> Fixity
n Int
20)
, forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"!=" PC -> TCon
PC PC
PNeq (Int -> Fixity
n Int
20)
, forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
">=" PC -> TCon
PC PC
PGeq (Int -> Fixity
n Int
30)
, forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"+" TFun -> TCon
TF TFun
TCAdd (Int -> Fixity
l Int
80)
, forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"-" TFun -> TCon
TF TFun
TCSub (Int -> Fixity
l Int
80)
, forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"*" TFun -> TCon
TF TFun
TCMul (Int -> Fixity
l Int
90)
, forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"/" TFun -> TCon
TF TFun
TCDiv (Int -> Fixity
l Int
90)
, forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"%" TFun -> TCon
TF TFun
TCMod (Int -> Fixity
l Int
90)
, forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"^^" TFun -> TCon
TF TFun
TCExp (Int -> Fixity
r Int
95)
, forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"/^" TFun -> TCon
TF TFun
TCCeilDiv (Int -> Fixity
l Int
90)
, forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"%^" TFun -> TCon
TF TFun
TCCeilMod (Int -> Fixity
l Int
90)
]
r :: Int -> Fixity
r Int
x = Fixity { fAssoc :: Assoc
fAssoc = Assoc
RightAssoc, fLevel :: Int
fLevel = Int
x }
l :: Int -> Fixity
l Int
x = Fixity { fAssoc :: Assoc
fAssoc = Assoc
LeftAssoc, fLevel :: Int
fLevel = Int
x }
n :: Int -> Fixity
n Int
x = Fixity { fAssoc :: Assoc
fAssoc = Assoc
NonAssoc, fLevel :: Int
fLevel = Int
x }
tInfix :: String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
x t -> a
mk t
tc b
f = (t -> a
mk t
tc, (String -> Ident
packIdent String
x, b
f))
builtInType :: M.Name -> Maybe TCon
builtInType :: Name -> Maybe TCon
builtInType Name
nm =
case Name -> NameInfo
M.nameInfo Name
nm of
M.GlobalName NameSource
_ OrigName { ogModule :: OrigName -> ModPath
ogModule = ModPath
m }
| ModPath
m forall a. Eq a => a -> a -> Bool
== ModName -> ModPath
M.TopModule ModName
preludeName -> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Name -> Ident
M.nameIdent Name
nm) Map Ident TCon
builtInTypes
| ModPath
m forall a. Eq a => a -> a -> Bool
== ModName -> ModPath
M.TopModule ModName
floatName -> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Name -> Ident
M.nameIdent Name
nm) Map Ident TCon
builtInFloat
| ModPath
m forall a. Eq a => a -> a -> Bool
== ModName -> ModPath
M.TopModule ModName
arrayName -> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Name -> Ident
M.nameIdent Name
nm) Map Ident TCon
builtInArray
NameInfo
_ -> forall a. Maybe a
Nothing
where
String
x ~> :: String -> b -> (Ident, b)
~> b
y = (String -> Ident
packIdent String
x, b
y)
builtInFloat :: Map Ident TCon
builtInFloat = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ String
"Float" forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCFloat
, String
"ValidFloat" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PValidFloat
]
builtInTypes :: Map Ident TCon
builtInTypes = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[
String
"inf" forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCInf
, String
"Bit" forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCBit
, String
"Integer" forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCInteger
, String
"Rational" forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCRational
, String
"Z" forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCIntMod
, String
"==" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PEqual
, String
"!=" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PNeq
, String
">=" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PGeq
, String
"fin" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PFin
, String
"prime" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PPrime
, String
"Zero" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PZero
, String
"Logic" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PLogic
, String
"Ring" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PRing
, String
"Integral" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PIntegral
, String
"Field" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PField
, String
"Round" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PRound
, String
"Eq" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PEq
, String
"Cmp" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PCmp
, String
"SignedCmp" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PSignedCmp
, String
"Literal" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PLiteral
, String
"LiteralLessThan" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PLiteralLessThan
, String
"FLiteral" forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PFLiteral
, String
"+" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCAdd
, String
"-" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCSub
, String
"*" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMul
, String
"/" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCDiv
, String
"%" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMod
, String
"^^" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCExp
, String
"width" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCWidth
, String
"min" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMin
, String
"max" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMax
, String
"/^" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCCeilDiv
, String
"%^" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCCeilMod
, String
"lengthFromThenTo" forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCLenFromThenTo
]
builtInArray :: Map Ident TCon
builtInArray = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ String
"Array" forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCArray
]
infixr 5 :->
data Kind = KType
| KNum
| KProp
| Kind :-> Kind
deriving (Kind -> Kind -> Bool
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
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
Ord, Int -> Kind -> ShowS
[Kind] -> ShowS
Kind -> String
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. 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 -> ()
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) = forall t. HasKind t => t -> Kind
kindOf TC
tc
kindOf (PC PC
pc) = forall t. HasKind t => t -> Kind
kindOf PC
pc
kindOf (TF TFun
tf) = forall t. HasKind t => t -> Kind
kindOf TFun
tf
kindOf (TError Kind
k) = Kind
k
instance HasKind UserTC where
kindOf :: UserTC -> Kind
kindOf (UserTC Name
_ Kind
k) = Kind
k
instance HasKind TC where
kindOf :: TC -> Kind
kindOf TC
tcon =
case TC
tcon of
TCNum Integer
_ -> Kind
KNum
TC
TCInf -> Kind
KNum
TC
TCBit -> Kind
KType
TC
TCInteger -> Kind
KType
TC
TCRational -> Kind
KType
TC
TCFloat -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KType
TC
TCIntMod -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KType
TC
TCArray -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KType
TC
TCSeq -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KType
TC
TCFun -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KType
TCTuple Int
n -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) Kind
KType (forall a. Int -> a -> [a]
replicate Int
n Kind
KType)
TCAbstract UserTC
x -> forall t. HasKind t => t -> Kind
kindOf UserTC
x
instance HasKind PC where
kindOf :: PC -> Kind
kindOf PC
pc =
case PC
pc of
PC
PEqual -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KProp
PC
PNeq -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KProp
PC
PGeq -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KProp
PC
PFin -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KProp
PC
PPrime -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KProp
PHas Selector
_ -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PZero -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PLogic -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PRing -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PIntegral -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PField -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PRound -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PEq -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PCmp -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PSignedCmp -> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PLiteral -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PLiteralLessThan -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PFLiteral -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KType Kind -> Kind -> Kind
:-> Kind
KProp
PC
PValidFloat -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KProp
PC
PAnd -> Kind
KProp Kind -> Kind -> Kind
:-> Kind
KProp Kind -> Kind -> Kind
:-> Kind
KProp
PC
PTrue -> Kind
KProp
instance HasKind TFun where
kindOf :: TFun -> Kind
kindOf TFun
tfun =
case TFun
tfun of
TFun
TCWidth -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
TCAdd -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
TCSub -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
TCMul -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
TCDiv -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
TCMod -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
TCExp -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
TCMin -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
TCMax -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
TCCeilDiv -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
TCCeilMod -> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum Kind -> Kind -> Kind
:-> Kind
KNum
TFun
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
deriving (Int -> TCon -> ShowS
[TCon] -> ShowS
TCon -> String
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
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
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
Ord, 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 -> ()
forall a. (a -> ()) -> NFData a
rnf :: TCon -> ()
$crnf :: TCon -> ()
NFData)
data PC = PEqual
| PNeq
| PGeq
| PFin
| PPrime
| PHas Selector
| PZero
| PLogic
| PRing
| PIntegral
| PField
| PRound
| PEq
| PCmp
| PSignedCmp
| PLiteral
| PLiteralLessThan
| PFLiteral
| PValidFloat
| PAnd
| PTrue
deriving (Int -> PC -> ShowS
[PC] -> ShowS
PC -> String
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
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
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
Ord, 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 -> ()
forall a. (a -> ()) -> NFData a
rnf :: PC -> ()
$crnf :: PC -> ()
NFData)
data TC = TCNum Integer
| TCInf
| TCBit
| TCInteger
| TCFloat
| TCIntMod
| TCRational
| TCArray
| TCSeq
| TCFun
| TCTuple Int
| TCAbstract UserTC
deriving (Int -> TC -> ShowS
[TC] -> ShowS
TC -> String
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
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
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
Ord, 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 -> ()
forall a. (a -> ()) -> NFData a
rnf :: TC -> ()
$crnf :: TC -> ()
NFData)
data UserTC = UserTC M.Name Kind
deriving (Int -> UserTC -> ShowS
[UserTC] -> ShowS
UserTC -> String
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. 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 -> ()
forall a. (a -> ()) -> NFData a
rnf :: UserTC -> ()
$crnf :: UserTC -> ()
NFData)
instance Eq UserTC where
UserTC Name
x Kind
_ == :: UserTC -> UserTC -> Bool
== UserTC Name
y Kind
_ = Name
x forall a. Eq a => a -> a -> Bool
== Name
y
instance Ord UserTC where
compare :: UserTC -> UserTC -> Ordering
compare (UserTC Name
x Kind
_) (UserTC Name
y Kind
_) = forall a. Ord a => a -> a -> Ordering
compare Name
x Name
y
data TFun
= TCAdd
| TCSub
| TCMul
| TCDiv
| TCMod
| TCExp
| TCWidth
| TCMin
| TCMax
| TCCeilDiv
| TCCeilMod
| TCLenFromThenTo
deriving (Int -> TFun -> ShowS
[TFun] -> ShowS
TFun -> String
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
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
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
Ord, 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]
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. 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 -> ()
forall a. (a -> ()) -> NFData a
rnf :: TFun -> ()
$crnf :: TFun -> ()
NFData)
instance PP Kind where
ppPrec :: Int -> Kind -> Doc
ppPrec Int
p Kind
k = case Kind
k of
Kind
KType -> Char -> Doc
char Char
'*'
Kind
KNum -> Char -> Doc
char Char
'#'
Kind
KProp -> String -> Doc
text String
"Prop"
Kind
l :-> Kind
r -> Bool -> Doc -> Doc
optParens (Int
p forall a. Ord a => a -> a -> Bool
>= Int
1) ([Doc] -> Doc
sep [forall a. PP a => Int -> a -> Doc
ppPrec Int
1 Kind
l, String -> Doc
text String
"->", forall a. PP a => Int -> a -> Doc
ppPrec Int
0 Kind
r])
instance PP TCon where
ppPrec :: Int -> TCon -> Doc
ppPrec Int
_ (TC TC
tc) = forall a. PP a => a -> Doc
pp TC
tc
ppPrec Int
_ (PC PC
tc) = forall a. PP a => a -> Doc
pp PC
tc
ppPrec Int
_ (TF TFun
tc) = forall a. PP a => a -> Doc
pp TFun
tc
ppPrec Int
_ (TError Kind
_) = Doc
"Error"
instance PP PC where
ppPrec :: Int -> PC -> Doc
ppPrec Int
_ PC
x =
case PC
x of
PC
PEqual -> String -> Doc
text String
"(==)"
PC
PNeq -> String -> Doc
text String
"(/=)"
PC
PGeq -> String -> Doc
text String
"(>=)"
PC
PFin -> String -> Doc
text String
"fin"
PC
PPrime -> String -> Doc
text String
"prime"
PHas Selector
sel -> Doc -> Doc
parens (Selector -> Doc
ppSelector Selector
sel)
PC
PZero -> String -> Doc
text String
"Zero"
PC
PLogic -> String -> Doc
text String
"Logic"
PC
PRing -> String -> Doc
text String
"Ring"
PC
PIntegral -> String -> Doc
text String
"Integral"
PC
PField -> String -> Doc
text String
"Field"
PC
PRound -> String -> Doc
text String
"Round"
PC
PEq -> String -> Doc
text String
"Eq"
PC
PCmp -> String -> Doc
text String
"Cmp"
PC
PSignedCmp -> String -> Doc
text String
"SignedCmp"
PC
PLiteral -> String -> Doc
text String
"Literal"
PC
PLiteralLessThan -> String -> Doc
text String
"LiteralLessThan"
PC
PFLiteral -> String -> Doc
text String
"FLiteral"
PC
PValidFloat -> String -> Doc
text String
"ValidFloat"
PC
PTrue -> String -> Doc
text String
"True"
PC
PAnd -> String -> Doc
text String
"(&&)"
instance PP TC where
ppPrec :: Int -> TC -> Doc
ppPrec Int
_ TC
x =
case TC
x of
TCNum Integer
n -> Integer -> Doc
integer Integer
n
TC
TCInf -> String -> Doc
text String
"inf"
TC
TCBit -> String -> Doc
text String
"Bit"
TC
TCInteger -> String -> Doc
text String
"Integer"
TC
TCIntMod -> String -> Doc
text String
"Z"
TC
TCRational -> String -> Doc
text String
"Rational"
TC
TCArray -> String -> Doc
text String
"Array"
TC
TCFloat -> String -> Doc
text String
"Float"
TC
TCSeq -> String -> Doc
text String
"[]"
TC
TCFun -> String -> Doc
text String
"(->)"
TCTuple Int
0 -> String -> Doc
text String
"()"
TCTuple Int
1 -> String -> Doc
text String
"(one tuple?)"
TCTuple Int
n -> Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hcat forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate (Int
nforall a. Num a => a -> a -> a
-Int
1) Doc
comma
TCAbstract UserTC
u -> forall a. PP a => a -> Doc
pp UserTC
u
instance PP UserTC where
ppPrec :: Int -> UserTC -> Doc
ppPrec Int
p (UserTC Name
x Kind
_) = forall a. PP a => Int -> a -> Doc
ppPrec Int
p Name
x
instance PP TFun where
ppPrec :: Int -> TFun -> Doc
ppPrec Int
_ TFun
tcon =
case TFun
tcon of
TFun
TCAdd -> String -> Doc
text String
"+"
TFun
TCSub -> String -> Doc
text String
"-"
TFun
TCMul -> String -> Doc
text String
"*"
TFun
TCDiv -> String -> Doc
text String
"/"
TFun
TCMod -> String -> Doc
text String
"%"
TFun
TCExp -> String -> Doc
text String
"^^"
TFun
TCWidth -> String -> Doc
text String
"width"
TFun
TCMin -> String -> Doc
text String
"min"
TFun
TCMax -> String -> Doc
text String
"max"
TFun
TCCeilDiv -> String -> Doc
text String
"/^"
TFun
TCCeilMod -> String -> Doc
text String
"%^"
TFun
TCLenFromThenTo -> String -> Doc
text String
"lengthFromThenTo"