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