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

-- | 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 = \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 :: Assoc -> Int -> Fixity
Fixity { fAssoc :: Assoc
fAssoc = Assoc
RightAssoc, fLevel :: Int
fLevel = Int
x }
  l :: Int -> Fixity
l Int
x = Fixity :: Assoc -> Int -> Fixity
Fixity { fAssoc :: Assoc
fAssoc = Assoc
LeftAssoc,  fLevel :: Int
fLevel = Int
x }
  n :: Int -> Fixity
n Int
x = Fixity :: Assoc -> Int -> Fixity
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.Declared ModName
m NameSource
_
      | 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
      | ModName
m ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== 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
      | ModName
m ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== 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)

  -- Built-in types from Float.cry
  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
    ]

  -- Built-in types from Cryptol.cry
  builtInTypes :: Map Ident TCon
builtInTypes = [(Ident, TCon)] -> Map Ident TCon
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ -- Types
      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

      -- Predicate contstructors
    , 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
"FLiteral"          String -> TCon -> (Ident, TCon)
forall b. String -> b -> (Ident, b)
~> PC -> TCon
PC PC
PFLiteral

    -- Type functions
    , 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
    ]

  -- Built-in types from Array.cry
  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 :->

-- | 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 -> 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 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 -> (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 UserTC
x -> UserTC -> Kind
forall t. HasKind t => t -> Kind
kindOf UserTC
x
      TCAbstract UserTC
x -> UserTC -> Kind
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
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



-- | Type constants.
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
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 _@
            | PPrime        -- ^ @prime _@

            -- classes
            | PHas Selector -- ^ @Has sel type field@ does not appear in schemas
            | PZero         -- ^ @Zero _@
            | PLogic        -- ^ @Logic _@
            | PRing         -- ^ @Ring _@
            | PIntegral     -- ^ @Integral _@
            | PField        -- ^ @Field _@
            | PRound        -- ^ @Round _@
            | PEq           -- ^ @Eq _@
            | PCmp          -- ^ @Cmp _@
            | PSignedCmp    -- ^ @SignedCmp _@
            | PLiteral      -- ^ @Literal _ _@
            | PFLiteral     -- ^ @FLiteral _ _ _@

            | PValidFloat   -- ^ @ValidFloat _ _@ constraints on supported
                            -- floating point representaitons

            | 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
            | TCFloat                  -- ^ Float
            | TCIntMod                 -- ^ @Z _@
            | TCRational               -- ^ @Rational@
            | TCArray                  -- ^ @Array _ _@
            | 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 Name
x Kind
_ == :: UserTC -> UserTC -> Bool
== UserTC Name
y Kind
_ = Name
x Name -> Name -> Bool
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
_) = Name -> Name -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Name
x Name
y






-- | 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 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
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
      TCNewtype UserTC
u -> UserTC -> Doc
forall a. PP a => a -> Doc
pp UserTC
u
      TCAbstract UserTC
u -> UserTC -> Doc
forall a. PP a => a -> Doc
pp UserTC
u

instance PP UserTC where
  ppPrec :: Int -> UserTC -> Doc
ppPrec Int
p (UserTC Name
x Kind
_) = Int -> Name -> Doc
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"