{-# 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

-- | This is used for pretty prinitng.
-- XXX: it would be nice to just rely in the info from the Prelude.
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
    [ -- Types
      "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

      -- Predicate contstructors
    , "=="                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

    -- Type functions
    , "+"                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 :->

-- | Kinds, classify types.
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



-- | Type constants.
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)


-- | 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 (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)

-- | 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              -- ^ @(_, _, _)@
            | TCAbstract UserTC        -- ^ An abstract type
            | TCNewtype UserTC         -- ^ user-defined, @T@
              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
    -- XXX: Add location?
  } 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)


-- | Built-in type functions.
-- If you add additional user-visible constructors,
-- please update 'primTys' in "Cryptol.Prims.Types".
data TFun

  = TCAdd                 -- ^ @ : Num -> Num -> Num @
  | TCSub                 -- ^ @ : Num -> Num -> Num @
  | TCMul                 -- ^ @ : Num -> Num -> Num @
  | TCDiv                 -- ^ @ : Num -> Num -> Num @
  | TCMod                 -- ^ @ : Num -> Num -> Num @
  | TCExp                 -- ^ @ : Num -> Num -> Num @
  | TCWidth               -- ^ @ : Num -> Num @
  | TCMin                 -- ^ @ : Num -> Num -> Num @
  | TCMax                 -- ^ @ : Num -> Num -> Num @
  | TCCeilDiv             -- ^ @ : Num -> Num -> Num @
  | TCCeilMod             -- ^ @ : Num -> Num -> Num @

  -- Computing the lengths of explicit enumerations
  | TCLenFromThenTo       -- ^ @ : Num -> Num -> Num -> Num@
    -- Example: @[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]@

    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)



--------------------------------------------------------------------------------
-- Pretty printing

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"