{-# 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 -> 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 String
"==" PC -> TCon
PC PC
PEqual (Int -> Fixity
n Int
20)
, String -> (PC -> TCon) -> PC -> Fixity -> (TCon, (Ident, Fixity))
forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"!=" PC -> TCon
PC PC
PNeq (Int -> Fixity
n Int
20)
, String -> (PC -> TCon) -> PC -> Fixity -> (TCon, (Ident, Fixity))
forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
">=" PC -> TCon
PC PC
PGeq (Int -> Fixity
n Int
30)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"+" TFun -> TCon
TF TFun
TCAdd (Int -> Fixity
l Int
80)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"-" TFun -> TCon
TF TFun
TCSub (Int -> Fixity
l Int
80)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"*" TFun -> TCon
TF TFun
TCMul (Int -> Fixity
l Int
90)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"/" TFun -> TCon
TF TFun
TCDiv (Int -> Fixity
l Int
90)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"%" TFun -> TCon
TF TFun
TCMod (Int -> Fixity
l Int
90)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"^^" TFun -> TCon
TF TFun
TCExp (Int -> Fixity
r Int
95)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
forall {t} {a} {b}. String -> (t -> a) -> t -> b -> (a, (Ident, b))
tInfix String
"/^" TFun -> TCon
TF TFun
TCCeilDiv (Int -> Fixity
l Int
90)
, String
-> (TFun -> TCon) -> TFun -> Fixity -> (TCon, (Ident, Fixity))
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 ModPath -> ModPath -> Bool
forall a. Eq a => a -> a -> Bool
== ModName -> ModPath
M.TopModule 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
| ModPath
m ModPath -> ModPath -> Bool
forall a. Eq a => a -> a -> Bool
== ModName -> ModPath
M.TopModule ModName
floatName -> 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
builtInFloat
| ModPath
m ModPath -> ModPath -> Bool
forall a. Eq a => a -> a -> Bool
== ModName -> ModPath
M.TopModule ModName
arrayName -> 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
builtInArray
NameInfo
_ -> Maybe TCon
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 = [(Ident, TCon)] -> Map Ident TCon
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ String
"Float" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCFloat
, String
"ValidFloat" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PValidFloat
]
builtInTypes :: Map Ident TCon
builtInTypes = [(Ident, TCon)] -> Map Ident TCon
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[
String
"inf" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCInf
, String
"Bit" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCBit
, String
"Integer" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCInteger
, String
"Rational" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCRational
, String
"Z" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCIntMod
, String
"==" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PEqual
, String
"!=" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PNeq
, String
">=" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PGeq
, String
"fin" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PFin
, String
"prime" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PPrime
, String
"Zero" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PZero
, String
"Logic" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PLogic
, String
"Ring" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PRing
, String
"Integral" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PIntegral
, String
"Field" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PField
, String
"Round" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PRound
, String
"Eq" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PEq
, String
"Cmp" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PCmp
, String
"SignedCmp" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PSignedCmp
, String
"Literal" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PLiteral
, String
"LiteralLessThan" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PLiteralLessThan
, String
"FLiteral" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PFLiteral
, String
"+" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCAdd
, String
"-" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCSub
, String
"*" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMul
, String
"/" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCDiv
, String
"%" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMod
, String
"^^" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCExp
, String
"width" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCWidth
, String
"min" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMin
, String
"max" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCMax
, String
"/^" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCCeilDiv
, String
"%^" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCCeilMod
, String
"lengthFromThenTo" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TFun -> TCon
TF TFun
TCLenFromThenTo
]
builtInArray :: Map Ident TCon
builtInArray = [(Ident, TCon)] -> Map Ident TCon
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ String
"Array" String -> TCon -> (Ident, TCon)
forall {b}. String -> b -> (Ident, b)
~> TC -> TCon
TC TC
TCArray
]
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
$c== :: Kind -> Kind -> Bool
== :: Kind -> Kind -> Bool
$c/= :: Kind -> Kind -> Bool
/= :: 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
$ccompare :: Kind -> Kind -> Ordering
compare :: Kind -> Kind -> Ordering
$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
>= :: Kind -> Kind -> Bool
$cmax :: Kind -> Kind -> Kind
max :: Kind -> Kind -> Kind
$cmin :: Kind -> Kind -> Kind
min :: Kind -> Kind -> 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
$cshowsPrec :: Int -> Kind -> ShowS
showsPrec :: Int -> Kind -> ShowS
$cshow :: Kind -> String
show :: Kind -> String
$cshowList :: [Kind] -> ShowS
showList :: [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
$cfrom :: forall x. Kind -> Rep Kind x
from :: forall x. Kind -> Rep Kind x
$cto :: forall x. Rep Kind x -> Kind
to :: forall x. Rep Kind x -> Kind
Generic, Kind -> ()
(Kind -> ()) -> NFData Kind
forall a. (a -> ()) -> NFData a
$crnf :: Kind -> ()
rnf :: Kind -> ()
NFData)
class HasKind t where
kindOf :: t -> Kind
instance HasKind TCon where
kindOf :: TCon -> Kind
kindOf (TC TC
tc) = TC -> Kind
forall t. HasKind t => t -> Kind
kindOf TC
tc
kindOf (PC PC
pc) = PC -> Kind
forall t. HasKind t => t -> Kind
kindOf PC
pc
kindOf (TF TFun
tf) = TFun -> Kind
forall t. HasKind t => t -> Kind
kindOf TFun
tf
kindOf (TError 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 -> (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
forall a b. (a -> b -> b) -> b -> [a] -> b
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)
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
(Int -> TCon -> ShowS)
-> (TCon -> String) -> ([TCon] -> ShowS) -> Show TCon
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TCon -> ShowS
showsPrec :: Int -> TCon -> ShowS
$cshow :: TCon -> String
show :: TCon -> String
$cshowList :: [TCon] -> ShowS
showList :: [TCon] -> ShowS
Show, TCon -> TCon -> Bool
(TCon -> TCon -> Bool) -> (TCon -> TCon -> Bool) -> Eq TCon
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TCon -> TCon -> Bool
== :: TCon -> TCon -> Bool
$c/= :: TCon -> TCon -> Bool
/= :: 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
$ccompare :: TCon -> TCon -> Ordering
compare :: TCon -> TCon -> Ordering
$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
>= :: TCon -> TCon -> Bool
$cmax :: TCon -> TCon -> TCon
max :: TCon -> TCon -> TCon
$cmin :: TCon -> TCon -> TCon
min :: TCon -> TCon -> 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
$cfrom :: forall x. TCon -> Rep TCon x
from :: forall x. TCon -> Rep TCon x
$cto :: forall x. Rep TCon x -> TCon
to :: forall x. Rep TCon x -> TCon
Generic, TCon -> ()
(TCon -> ()) -> NFData TCon
forall a. (a -> ()) -> NFData a
$crnf :: TCon -> ()
rnf :: 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
(Int -> PC -> ShowS)
-> (PC -> String) -> ([PC] -> ShowS) -> Show PC
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PC -> ShowS
showsPrec :: Int -> PC -> ShowS
$cshow :: PC -> String
show :: PC -> String
$cshowList :: [PC] -> ShowS
showList :: [PC] -> ShowS
Show, PC -> PC -> Bool
(PC -> PC -> Bool) -> (PC -> PC -> Bool) -> Eq PC
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PC -> PC -> Bool
== :: PC -> PC -> Bool
$c/= :: PC -> PC -> Bool
/= :: 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
$ccompare :: PC -> PC -> Ordering
compare :: PC -> PC -> Ordering
$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
>= :: PC -> PC -> Bool
$cmax :: PC -> PC -> PC
max :: PC -> PC -> PC
$cmin :: PC -> PC -> PC
min :: PC -> PC -> 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
$cfrom :: forall x. PC -> Rep PC x
from :: forall x. PC -> Rep PC x
$cto :: forall x. Rep PC x -> PC
to :: forall x. Rep PC x -> PC
Generic, PC -> ()
(PC -> ()) -> NFData PC
forall a. (a -> ()) -> NFData a
$crnf :: PC -> ()
rnf :: PC -> ()
NFData)
data TC = TCNum Integer
| TCInf
| TCBit
| TCInteger
| TCFloat
| TCIntMod
| TCRational
| TCArray
| TCSeq
| TCFun
| TCTuple Int
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
$cshowsPrec :: Int -> TC -> ShowS
showsPrec :: Int -> TC -> ShowS
$cshow :: TC -> String
show :: TC -> String
$cshowList :: [TC] -> ShowS
showList :: [TC] -> ShowS
Show, TC -> TC -> Bool
(TC -> TC -> Bool) -> (TC -> TC -> Bool) -> Eq TC
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TC -> TC -> Bool
== :: TC -> TC -> Bool
$c/= :: TC -> TC -> Bool
/= :: 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
$ccompare :: TC -> TC -> Ordering
compare :: TC -> TC -> Ordering
$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
>= :: TC -> TC -> Bool
$cmax :: TC -> TC -> TC
max :: TC -> TC -> TC
$cmin :: TC -> TC -> TC
min :: TC -> TC -> 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
$cfrom :: forall x. TC -> Rep TC x
from :: forall x. TC -> Rep TC x
$cto :: forall x. Rep TC x -> TC
to :: forall x. Rep TC x -> TC
Generic, TC -> ()
(TC -> ()) -> NFData TC
forall a. (a -> ()) -> NFData a
$crnf :: TC -> ()
rnf :: TC -> ()
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
$cshowsPrec :: Int -> TFun -> ShowS
showsPrec :: Int -> TFun -> ShowS
$cshow :: TFun -> String
show :: TFun -> String
$cshowList :: [TFun] -> ShowS
showList :: [TFun] -> ShowS
Show, TFun -> TFun -> Bool
(TFun -> TFun -> Bool) -> (TFun -> TFun -> Bool) -> Eq TFun
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TFun -> TFun -> Bool
== :: TFun -> TFun -> Bool
$c/= :: TFun -> TFun -> Bool
/= :: 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
$ccompare :: TFun -> TFun -> Ordering
compare :: TFun -> TFun -> Ordering
$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
>= :: TFun -> TFun -> Bool
$cmax :: TFun -> TFun -> TFun
max :: TFun -> TFun -> TFun
$cmin :: TFun -> TFun -> TFun
min :: TFun -> TFun -> TFun
Ord, TFun
TFun -> TFun -> Bounded TFun
forall a. a -> a -> Bounded a
$cminBound :: TFun
minBound :: TFun
$cmaxBound :: TFun
maxBound :: 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
$csucc :: TFun -> TFun
succ :: TFun -> TFun
$cpred :: TFun -> TFun
pred :: TFun -> TFun
$ctoEnum :: Int -> TFun
toEnum :: Int -> TFun
$cfromEnum :: TFun -> Int
fromEnum :: TFun -> Int
$cenumFrom :: TFun -> [TFun]
enumFrom :: TFun -> [TFun]
$cenumFromThen :: TFun -> TFun -> [TFun]
enumFromThen :: TFun -> TFun -> [TFun]
$cenumFromTo :: TFun -> TFun -> [TFun]
enumFromTo :: TFun -> TFun -> [TFun]
$cenumFromThenTo :: TFun -> TFun -> TFun -> [TFun]
enumFromThenTo :: TFun -> TFun -> 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
$cfrom :: forall x. TFun -> Rep TFun x
from :: forall x. TFun -> Rep TFun x
$cto :: forall x. Rep TFun x -> TFun
to :: forall x. Rep TFun x -> TFun
Generic, TFun -> ()
(TFun -> ()) -> NFData TFun
forall a. (a -> ()) -> NFData a
$crnf :: TFun -> ()
rnf :: 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1) ([Doc] -> Doc
sep [Int -> Kind -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
1 Kind
l, String -> Doc
text String
"->", Int -> Kind -> Doc
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) = TC -> Doc
forall a. PP a => a -> Doc
pp TC
tc
ppPrec Int
_ (PC PC
tc) = PC -> Doc
forall a. PP a => a -> Doc
pp PC
tc
ppPrec Int
_ (TF TFun
tc) = TFun -> Doc
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 (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
-Int
1) Doc
comma
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"