    -- |
    -- Module      :  Cryptol.Eval.Type
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE Safe, PatternGuards #-}
    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE DeriveGeneric #-}
    module Cryptol.Eval.Type where

    import Cryptol.Backend.Monad (evalPanic)
    import Cryptol.TypeCheck.AST
    import Cryptol.TypeCheck.PP(pp)
    import Cryptol.TypeCheck.Solver.InfNat
    import Cryptol.Utils.Panic (panic)
    import Cryptol.Utils.Ident (Ident)
    import Cryptol.Utils.RecordMap
    import Cryptol.Utils.Types

    import Data.Maybe(fromMaybe)
    import qualified Data.IntMap.Strict as IntMap
    import GHC.Generics (Generic)
    import Control.DeepSeq

    -- | An evaluated type of kind *.
    -- These types do not contain type variables, type synonyms, or type functions.
    data TValue
      = TVBit                     -- ^ @ Bit @
      | TVInteger                 -- ^ @ Integer @
      | TVFloat Integer Integer   -- ^ @ Float e p @
      | TVIntMod Integer          -- ^ @ Z n @
      | TVRational                -- ^ @Rational@
      | TVArray TValue TValue     -- ^ @ Array a b @
      | TVSeq Integer TValue      -- ^ @ [n]a @
      | TVStream TValue           -- ^ @ [inf]t @
      | TVTuple [TValue]          -- ^ @ (a, b, c )@
      | TVRec (RecordMap Ident TValue) -- ^ @ { x : a, y : b, z : c } @
      | TVFun TValue TValue       -- ^ @ a -> b @
      | TVNewtype Newtype
                  [Either Nat' TValue]
                  (RecordMap Ident TValue)     -- ^ a named newtype
      | TVAbstract UserTC [Either Nat' TValue] -- ^ an abstract type
        deriving ((forall x. TValue -> Rep TValue x)
    -> (forall x. Rep TValue x -> TValue) -> Generic TValue
    forall x. Rep TValue x -> TValue
    forall x. TValue -> Rep TValue x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. TValue -> Rep TValue x
    from :: forall x. TValue -> Rep TValue x
    $cto :: forall x. Rep TValue x -> TValue
    to :: forall x. Rep TValue x -> TValue
    Generic, TValue -> ()
    (TValue -> ()) -> NFData TValue
    forall a. (a -> ()) -> NFData a
    $crnf :: TValue -> ()
    rnf :: TValue -> ()
    NFData, TValue -> TValue -> Bool
    (TValue -> TValue -> Bool)
    -> (TValue -> TValue -> Bool) -> Eq TValue
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: TValue -> TValue -> Bool
    == :: TValue -> TValue -> Bool
    $c/= :: TValue -> TValue -> Bool
    /= :: TValue -> TValue -> Bool
    Eq)

    -- | Convert a type value back into a regular type
    tValTy :: TValue -> Type
    tValTy :: TValue -> Type
    tValTy TValue
    tv =
      case TValue
    tv of
        TValue
    TVBit       -> Type
    tBit
        TValue
    TVInteger   -> Type
    tInteger
        TVFloat Integer
    e Integer
    p -> Type -> Type -> Type
    tFloat (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    e) (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    p)
        TVIntMod Integer
    n  -> Type -> Type
    tIntMod (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n)
        TValue
    TVRational  -> Type
    tRational
        TVArray TValue
    a TValue
    b -> Type -> Type -> Type
    tArray (TValue -> Type
    tValTy TValue
    a) (TValue -> Type
    tValTy TValue
    b)
        TVSeq Integer
    n TValue
    t   -> Type -> Type -> Type
    tSeq (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n) (TValue -> Type
    tValTy TValue
    t)
        TVStream TValue
    t  -> Type -> Type -> Type
    tSeq Type
    tInf (TValue -> Type
    tValTy TValue
    t)
        TVTuple [TValue]
    ts  -> [Type] -> Type
    tTuple ((TValue -> Type) -> [TValue] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map TValue -> Type
    tValTy [TValue]
    ts)
        TVRec RecordMap Ident TValue
    fs    -> RecordMap Ident Type -> Type
    tRec ((TValue -> Type) -> RecordMap Ident TValue -> RecordMap Ident Type
    forall a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap TValue -> Type
    tValTy RecordMap Ident TValue
    fs)
        TVFun TValue
    t1 TValue
    t2 -> Type -> Type -> Type
    tFun (TValue -> Type
    tValTy TValue
    t1) (TValue -> Type
    tValTy TValue
    t2)
        TVNewtype Newtype
    nt [Either Nat' TValue]
    vs RecordMap Ident TValue
    _ -> Newtype -> [Type] -> Type
    tNewtype Newtype
    nt ((Either Nat' TValue -> Type) -> [Either Nat' TValue] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Either Nat' TValue -> Type
    tNumValTy [Either Nat' TValue]
    vs)
        TVAbstract UserTC
    u [Either Nat' TValue]
    vs -> UserTC -> [Type] -> Type
    tAbstract UserTC
    u ((Either Nat' TValue -> Type) -> [Either Nat' TValue] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Either Nat' TValue -> Type
    tNumValTy [Either Nat' TValue]
    vs)

    tNumTy :: Nat' -> Type
    tNumTy :: Nat' -> Type
    tNumTy Nat'
    Inf     = Type
    tInf
    tNumTy (Nat Integer
    n) = Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n

    tNumValTy :: Either Nat' TValue -> Type
    tNumValTy :: Either Nat' TValue -> Type
    tNumValTy = (Nat' -> Type) -> (TValue -> Type) -> Either Nat' TValue -> Type
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either Nat' -> Type
    tNumTy TValue -> Type
    tValTy

    instance Show TValue where
      showsPrec :: Int -> TValue -> ShowS
    showsPrec Int
    p TValue
    v = Int -> Type -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p (TValue -> Type
    tValTy TValue
    v)

    -- Utilities -------------------------------------------------------------------

    -- | True if the evaluated value is @Bit@
    isTBit :: TValue -> Bool
    isTBit :: TValue -> Bool
    isTBit TValue
    TVBit = Bool
    True
    isTBit TValue
    _ = Bool
    False

    -- | Produce a sequence type value
    tvSeq :: Nat' -> TValue -> TValue
    tvSeq :: Nat' -> TValue -> TValue
    tvSeq (Nat Integer
    n) TValue
    t = Integer -> TValue -> TValue
    TVSeq Integer
    n TValue
    t
    tvSeq Nat'
    Inf     TValue
    t = TValue -> TValue
    TVStream TValue
    t

    -- | The Cryptol @Float64@ type.
    tvFloat64 :: TValue
    tvFloat64 :: TValue
    tvFloat64 = (Integer -> Integer -> TValue) -> (Integer, Integer) -> TValue
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Integer -> Integer -> TValue
    TVFloat (Integer, Integer)
    float64ExpPrec

    -- | Coerce an extended natural into an integer,
    --   for values known to be finite
    finNat' :: Nat' -> Integer
    finNat' :: Nat' -> Integer
    finNat' Nat'
    n' =
      case Nat'
    n' of
        Nat Integer
    x -> Integer
    x
        Nat'
    Inf   -> String -> [String] -> Integer
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.Eval.Value.finNat'" [ String
    "Unexpected `inf`" ]

    -- Type Evaluation -------------------------------------------------------------

    newtype TypeEnv =
      TypeEnv
      { TypeEnv -> IntMap (Either Nat' TValue)
    envTypeMap  :: IntMap.IntMap (Either Nat' TValue) }
      deriving (Int -> TypeEnv -> ShowS
    [TypeEnv] -> ShowS
    TypeEnv -> String
    (Int -> TypeEnv -> ShowS)
    -> (TypeEnv -> String) -> ([TypeEnv] -> ShowS) -> Show TypeEnv
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> TypeEnv -> ShowS
    showsPrec :: Int -> TypeEnv -> ShowS
    $cshow :: TypeEnv -> String
    show :: TypeEnv -> String
    $cshowList :: [TypeEnv] -> ShowS
    showList :: [TypeEnv] -> ShowS
    Show)

    instance Monoid TypeEnv where
      mempty :: TypeEnv
    mempty = IntMap (Either Nat' TValue) -> TypeEnv
    TypeEnv IntMap (Either Nat' TValue)
    forall a. Monoid a => a
    mempty

    instance Semigroup TypeEnv where
      TypeEnv
    l <> :: TypeEnv -> TypeEnv -> TypeEnv
    <> TypeEnv
    r = TypeEnv
        { envTypeMap :: IntMap (Either Nat' TValue)
    envTypeMap  = IntMap (Either Nat' TValue)
    -> IntMap (Either Nat' TValue) -> IntMap (Either Nat' TValue)
    forall a. IntMap a -> IntMap a -> IntMap a
    IntMap.union (TypeEnv -> IntMap (Either Nat' TValue)
    envTypeMap TypeEnv
    l) (TypeEnv -> IntMap (Either Nat' TValue)
    envTypeMap TypeEnv
    r) }

    lookupTypeVar :: TVar -> TypeEnv -> Maybe (Either Nat' TValue)
    lookupTypeVar :: TVar -> TypeEnv -> Maybe (Either Nat' TValue)
    lookupTypeVar TVar
    tv TypeEnv
    env = Int -> IntMap (Either Nat' TValue) -> Maybe (Either Nat' TValue)
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup (TVar -> Int
    tvUnique TVar
    tv) (TypeEnv -> IntMap (Either Nat' TValue)
    envTypeMap TypeEnv
    env)

    bindTypeVar :: TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
    bindTypeVar :: TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
    bindTypeVar TVar
    tv Either Nat' TValue
    ty TypeEnv
    env = TypeEnv
    env{ envTypeMap :: IntMap (Either Nat' TValue)
    envTypeMap = Int
    -> Either Nat' TValue
    -> IntMap (Either Nat' TValue)
    -> IntMap (Either Nat' TValue)
    forall a. Int -> a -> IntMap a -> IntMap a
    IntMap.insert (TVar -> Int
    tvUnique TVar
    tv) Either Nat' TValue
    ty (TypeEnv -> IntMap (Either Nat' TValue)
    envTypeMap TypeEnv
    env) }

    -- | Evaluation for types (kind * or #).
    evalType :: TypeEnv -> Type -> Either Nat' TValue
    evalType :: TypeEnv -> Type -> Either Nat' TValue
    evalType TypeEnv
    env Type
    ty =
      case Type
    ty of
        TVar TVar
    tv ->
          case TVar -> TypeEnv -> Maybe (Either Nat' TValue)
    lookupTypeVar TVar
    tv TypeEnv
    env of
            Just Either Nat' TValue
    v -> Either Nat' TValue
    v
            Maybe (Either Nat' TValue)
    Nothing -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalType" [String
    "type variable not bound", TVar -> String
    forall a. Show a => a -> String
    show TVar
    tv]

        TUser Name
    _ [Type]
    _ Type
    ty'  -> TypeEnv -> Type -> Either Nat' TValue
    evalType TypeEnv
    env Type
    ty'
        TRec RecordMap Ident Type
    fields    -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ RecordMap Ident TValue -> TValue
    TVRec ((Type -> TValue) -> RecordMap Ident Type -> RecordMap Ident TValue
    forall a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Type -> TValue
    val RecordMap Ident Type
    fields)

        TNewtype Newtype
    nt [Type]
    ts -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue -> TValue
    TVNewtype Newtype
    nt [Either Nat' TValue]
    tvs (RecordMap Ident TValue -> TValue)
    -> RecordMap Ident TValue -> TValue
    forall a b. (a -> b) -> a -> b
    $ TypeEnv
    -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue
    evalNewtypeBody TypeEnv
    env Newtype
    nt [Either Nat' TValue]
    tvs
            where tvs :: [Either Nat' TValue]
    tvs = (Type -> Either Nat' TValue) -> [Type] -> [Either Nat' TValue]
    forall a b. (a -> b) -> [a] -> [b]
    map (TypeEnv -> Type -> Either Nat' TValue
    evalType TypeEnv
    env) [Type]
    ts

        TCon (TC TC
    c) [Type]
    ts ->
          case (TC
    c, [Type]
    ts) of
            (TC
    TCBit, [])     -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ TValue
    TVBit
            (TC
    TCInteger, []) -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ TValue
    TVInteger
            (TC
    TCRational, []) -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ TValue
    TVRational
            (TC
    TCFloat, [Type
    e,Type
    p])-> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer -> TValue
    TVFloat (Type -> Integer
    inum Type
    e) (Type -> Integer
    inum Type
    p)
            (TC
    TCIntMod, [Type
    n]) -> case Type -> Nat'
    num Type
    n of
                                 Nat'
    Inf   -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalType" [String
    "invalid type Z inf"]
                                 Nat Integer
    m -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ Integer -> TValue
    TVIntMod Integer
    m
            (TC
    TCArray, [Type
    a, Type
    b]) -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ TValue -> TValue -> TValue
    TVArray (Type -> TValue
    val Type
    a) (Type -> TValue
    val Type
    b)
            (TC
    TCSeq, [Type
    n, Type
    t]) -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ Nat' -> TValue -> TValue
    tvSeq (Type -> Nat'
    num Type
    n) (Type -> TValue
    val Type
    t)
            (TC
    TCFun, [Type
    a, Type
    b]) -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ TValue -> TValue -> TValue
    TVFun (Type -> TValue
    val Type
    a) (Type -> TValue
    val Type
    b)
            (TCTuple Int
    _, [Type]
    _)  -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ [TValue] -> TValue
    TVTuple ((Type -> TValue) -> [Type] -> [TValue]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> TValue
    val [Type]
    ts)
            (TCNum Integer
    n, [])   -> Nat' -> Either Nat' TValue
    forall a b. a -> Either a b
    Left (Nat' -> Either Nat' TValue) -> Nat' -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ Integer -> Nat'
    Nat Integer
    n
            (TC
    TCInf, [])     -> Nat' -> Either Nat' TValue
    forall a b. a -> Either a b
    Left (Nat' -> Either Nat' TValue) -> Nat' -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ Nat'
    Inf
            (TCAbstract UserTC
    u,[Type]
    vs) ->
                case Type -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Type
    ty of
                  Kind
    KType -> TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right (TValue -> Either Nat' TValue) -> TValue -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ UserTC -> [Either Nat' TValue] -> TValue
    TVAbstract UserTC
    u ((Type -> Either Nat' TValue) -> [Type] -> [Either Nat' TValue]
    forall a b. (a -> b) -> [a] -> [b]
    map (TypeEnv -> Type -> Either Nat' TValue
    evalType TypeEnv
    env) [Type]
    vs)
                  Kind
    k -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalType"
                    [ String
    "Unsupported"
                    , String
    "*** Abstract type of kind: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    k)
                    , String
    "*** Name: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (UserTC -> Doc
    forall a. PP a => a -> Doc
    pp UserTC
    u)
                    ]

            (TC, [Type])
    _ -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalType" [String
    "not a value type", Type -> String
    forall a. Show a => a -> String
    show Type
    ty]
        TCon (TF TFun
    f) [Type]
    ts      -> Nat' -> Either Nat' TValue
    forall a b. a -> Either a b
    Left (Nat' -> Either Nat' TValue) -> Nat' -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ TFun -> [Nat'] -> Nat'
    evalTF TFun
    f ((Type -> Nat') -> [Type] -> [Nat']
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Nat'
    num [Type]
    ts)
        TCon (PC PC
    p) [Type]
    _       -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalType" [String
    "invalid predicate symbol", PC -> String
    forall a. Show a => a -> String
    show PC
    p]
        TCon (TError Kind
    _) [Type]
    ts -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalType"
                                 ([String] -> Either Nat' TValue) -> [String] -> Either Nat' TValue
    forall a b. (a -> b) -> a -> b
    $ String
    "Lingering invalid type" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (Type -> String) -> [Type] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> String
    forall a. Show a => a -> String
    show (Doc -> String) -> (Type -> Doc) -> Type -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Doc
    forall a. PP a => a -> Doc
    pp) [Type]
    ts
      where
        val :: Type -> TValue
    val = TypeEnv -> Type -> TValue
    evalValType TypeEnv
    env
        num :: Type -> Nat'
    num = TypeEnv -> Type -> Nat'
    evalNumType TypeEnv
    env
        inum :: Type -> Integer
    inum Type
    x = case Type -> Nat'
    num Type
    x of
                   Nat Integer
    i -> Integer
    i
                   Nat'
    Inf   -> String -> [String] -> Integer
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalType"
                                      [String
    "Expecting a finite size, but got `inf`"]

    -- | Evaluate the body of a newtype, given evaluated arguments
    evalNewtypeBody :: TypeEnv -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue
    evalNewtypeBody :: TypeEnv
    -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue
    evalNewtypeBody TypeEnv
    env0 Newtype
    nt [Either Nat' TValue]
    args = (Type -> TValue) -> RecordMap Ident Type -> RecordMap Ident TValue
    forall a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (TypeEnv -> Type -> TValue
    evalValType TypeEnv
    env') (Newtype -> RecordMap Ident Type
    ntFields Newtype
    nt)
      where
      env' :: TypeEnv
    env' = TypeEnv -> [TParam] -> [Either Nat' TValue] -> TypeEnv
    loop TypeEnv
    env0 (Newtype -> [TParam]
    ntParams Newtype
    nt) [Either Nat' TValue]
    args

      loop :: TypeEnv -> [TParam] -> [Either Nat' TValue] -> TypeEnv
    loop TypeEnv
    env [] [] = TypeEnv
    env
      loop TypeEnv
    env (TParam
    p:[TParam]
    ps) (Either Nat' TValue
    a:[Either Nat' TValue]
    as) = TypeEnv -> [TParam] -> [Either Nat' TValue] -> TypeEnv
    loop (TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
    bindTypeVar (TParam -> TVar
    TVBound TParam
    p) Either Nat' TValue
    a TypeEnv
    env) [TParam]
    ps [Either Nat' TValue]
    as
      loop TypeEnv
    _ [TParam]
    _ [Either Nat' TValue]
    _ = String -> [String] -> TypeEnv
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalNewtype" [String
    "type parameter/argument mismatch"]

    -- | Evaluation for value types (kind *).
    evalValType :: TypeEnv -> Type -> TValue
    evalValType :: TypeEnv -> Type -> TValue
    evalValType TypeEnv
    env Type
    ty =
      case TypeEnv -> Type -> Either Nat' TValue
    evalType TypeEnv
    env Type
    ty of
        Left Nat'
    _ -> String -> [String] -> TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalValType" [String
    "expected value type, found numeric type"]
        Right TValue
    t -> TValue
    t

    -- | Evaluation for number types (kind #).
    evalNumType :: TypeEnv -> Type -> Nat'
    evalNumType :: TypeEnv -> Type -> Nat'
    evalNumType TypeEnv
    env Type
    ty =
      case TypeEnv -> Type -> Either Nat' TValue
    evalType TypeEnv
    env Type
    ty of
        Left Nat'
    n -> Nat'
    n
        Right TValue
    _ -> String -> [String] -> Nat'
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalValType" [String
    "expected numeric type, found value type"]

    -- | Reduce type functions, raising an exception for undefined values.
    evalTF :: TFun -> [Nat'] -> Nat'
    evalTF :: TFun -> [Nat'] -> Nat'
    evalTF TFun
    f [Nat']
    vs
      | TFun
    TCAdd           <- TFun
    f, [Nat'
    x,Nat'
    y]   <- [Nat']
    vs  =      Nat' -> Nat' -> Nat'
    nAdd Nat'
    x Nat'
    y
      | TFun
    TCSub           <- TFun
    f, [Nat'
    x,Nat'
    y]   <- [Nat']
    vs  = Maybe Nat' -> Nat'
    forall {a}. Maybe a -> a
    mb (Maybe Nat' -> Nat') -> Maybe Nat' -> Nat'
    forall a b. (a -> b) -> a -> b
    $ Nat' -> Nat' -> Maybe Nat'
    nSub Nat'
    x Nat'
    y
      | TFun
    TCMul           <- TFun
    f, [Nat'
    x,Nat'
    y]   <- [Nat']
    vs  =      Nat' -> Nat' -> Nat'
    nMul Nat'
    x Nat'
    y
      | TFun
    TCDiv           <- TFun
    f, [Nat'
    x,Nat'
    y]   <- [Nat']
    vs  = Maybe Nat' -> Nat'
    forall {a}. Maybe a -> a
    mb (Maybe Nat' -> Nat') -> Maybe Nat' -> Nat'
    forall a b. (a -> b) -> a -> b
    $ Nat' -> Nat' -> Maybe Nat'
    nDiv Nat'
    x Nat'
    y
      | TFun
    TCMod           <- TFun
    f, [Nat'
    x,Nat'
    y]   <- [Nat']
    vs  = Maybe Nat' -> Nat'
    forall {a}. Maybe a -> a
    mb (Maybe Nat' -> Nat') -> Maybe Nat' -> Nat'
    forall a b. (a -> b) -> a -> b
    $ Nat' -> Nat' -> Maybe Nat'
    nMod Nat'
    x Nat'
    y
      | TFun
    TCWidth         <- TFun
    f, [Nat'
    x]     <- [Nat']
    vs  =      Nat' -> Nat'
    nWidth Nat'
    x
      | TFun
    TCExp           <- TFun
    f, [Nat'
    x,Nat'
    y]   <- [Nat']
    vs  =      Nat' -> Nat' -> Nat'
    nExp Nat'
    x Nat'
    y
      | TFun
    TCMin           <- TFun
    f, [Nat'
    x,Nat'
    y]   <- [Nat']
    vs  =      Nat' -> Nat' -> Nat'
    nMin Nat'
    x Nat'
    y
      | TFun
    TCMax           <- TFun
    f, [Nat'
    x,Nat'
    y]   <- [Nat']
    vs  =      Nat' -> Nat' -> Nat'
    nMax Nat'
    x Nat'
    y
      | TFun
    TCCeilDiv       <- TFun
    f, [Nat'
    x,Nat'
    y]   <- [Nat']
    vs  = Maybe Nat' -> Nat'
    forall {a}. Maybe a -> a
    mb (Maybe Nat' -> Nat') -> Maybe Nat' -> Nat'
    forall a b. (a -> b) -> a -> b
    $ Nat' -> Nat' -> Maybe Nat'
    nCeilDiv Nat'
    x Nat'
    y
      | TFun
    TCCeilMod       <- TFun
    f, [Nat'
    x,Nat'
    y]   <- [Nat']
    vs  = Maybe Nat' -> Nat'
    forall {a}. Maybe a -> a
    mb (Maybe Nat' -> Nat') -> Maybe Nat' -> Nat'
    forall a b. (a -> b) -> a -> b
    $ Nat' -> Nat' -> Maybe Nat'
    nCeilMod Nat'
    x Nat'
    y
      | TFun
    TCLenFromThenTo <- TFun
    f, [Nat'
    x,Nat'
    y,Nat'
    z] <- [Nat']
    vs  = Maybe Nat' -> Nat'
    forall {a}. Maybe a -> a
    mb (Maybe Nat' -> Nat') -> Maybe Nat' -> Nat'
    forall a b. (a -> b) -> a -> b
    $ Nat' -> Nat' -> Nat' -> Maybe Nat'
    nLenFromThenTo Nat'
    x Nat'
    y Nat'
    z
      | Bool
    otherwise  = String -> [String] -> Nat'
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalTF"
                            [String
    "Unexpected type function:", Type -> String
    forall a. Show a => a -> String
    show Type
    ty]

      where mb :: Maybe a -> a
    mb = a -> Maybe a -> a
    forall a. a -> Maybe a -> a
    fromMaybe (String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalTF" [String
    "type cannot be demoted", Doc -> String
    forall a. Show a => a -> String
    show (Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    ty)])
            ty :: Type
    ty = TCon -> [Type] -> Type
    TCon (TFun -> TCon
    TF TFun
    f) ((Nat' -> Type) -> [Nat'] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Nat' -> Type
    tNat' [Nat']
    vs)