    -- |
    -- 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.Eval.Monad
    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 Data.Maybe(fromMaybe)
    import qualified Data.Map.Strict as Map
    import GHC.Generics (Generic)
    import GHC.Stack(HasCallStack)
    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 @
      | TVIntMod Integer          -- ^ @ Z n @
      | TVSeq Integer TValue      -- ^ @ [n]a @
      | TVStream TValue           -- ^ @ [inf]t @
      | TVTuple [TValue]          -- ^ @ (a, b, c )@
      | TVRec [(Ident, TValue)]   -- ^ @ { x : a, y : b, z : c } @
      | TVFun TValue TValue       -- ^ @ a -> b @
      | 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
    $cto :: forall x. Rep TValue x -> TValue
    $cfrom :: forall x. TValue -> Rep TValue x
    Generic, TValue -> ()
    (TValue -> ()) -> NFData TValue
    forall a. (a -> ()) -> NFData a
    rnf :: TValue -> ()
    $crnf :: TValue -> ()
    NFData)

    -- | Convert a type value back into a regular type
    tValTy :: TValue -> Type
    tValTy :: TValue -> Type
    tValTy tv :: TValue
    tv =
      case TValue
    tv of
        TVBit       -> Type
    tBit
        TVInteger   -> Type
    tInteger
        TVIntMod n :: Integer
    n  -> Type -> Type
    tIntMod (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n)
        TVSeq n :: Integer
    n t :: TValue
    t   -> Type -> Type -> Type
    tSeq (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n) (TValue -> Type
    tValTy TValue
    t)
        TVStream t :: TValue
    t  -> Type -> Type -> Type
    tSeq Type
    tInf (TValue -> Type
    tValTy TValue
    t)
        TVTuple ts :: [TValue]
    ts  -> [Type] -> Type
    tTuple ((TValue -> Type) -> [TValue] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map TValue -> Type
    tValTy [TValue]
    ts)
        TVRec fs :: [(Ident, TValue)]
    fs    -> [(Ident, Type)] -> Type
    tRec [ (Ident
    f, TValue -> Type
    tValTy TValue
    t) | (f :: Ident
    f, t :: TValue
    t) <- [(Ident, TValue)]
    fs ]
        TVFun t1 :: TValue
    t1 t2 :: TValue
    t2 -> Type -> Type -> Type
    tFun (TValue -> Type
    tValTy TValue
    t1) (TValue -> Type
    tValTy TValue
    t2)
        TVAbstract u :: UserTC
    u vs :: [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
    arg [Either Nat' TValue]
    vs)
          where arg :: Either Nat' TValue -> Type
    arg x :: Either Nat' TValue
    x = case Either Nat' TValue
    x of
                          Left Inf     -> Type
    tInf
                          Left (Nat n :: Integer
    n) -> Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n
                          Right v :: TValue
    v      -> TValue -> Type
    tValTy TValue
    v

    instance Show TValue where
      showsPrec :: Int -> TValue -> ShowS
    showsPrec p :: Int
    p v :: 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 TVBit = Bool
    True
    isTBit _ = Bool
    False

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

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

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

    type TypeEnv = Map.Map TVar (Either Nat' TValue)

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

        TUser _ _ ty' :: Type
    ty'  -> HasCallStack => TypeEnv -> Type -> Either Nat' TValue
    TypeEnv -> Type -> Either Nat' TValue
    evalType TypeEnv
    env Type
    ty'
        TRec fields :: [(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
    $ [(Ident, TValue)] -> TValue
    TVRec [ (Ident
    f, Type -> TValue
    val Type
    t) | (f :: Ident
    f, t :: Type
    t) <- [(Ident, Type)]
    fields ]
        TCon (TC c :: TC
    c) ts :: [Type]
    ts ->
          case (TC
    c, [Type]
    ts) of
            (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
            (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
            (TCIntMod, [n :: Type
    n]) -> case Type -> Nat'
    num Type
    n of
                                 Inf   -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "evalType" ["invalid type Z inf"]
                                 Nat m :: 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
            (TCSeq, [n :: Type
    n, t :: 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)
            (TCFun, [a :: Type
    a, b :: 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 _, _)  -> 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 n :: 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
            (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 u :: UserTC
    u,vs :: [Type]
    vs) ->
                case Type -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Type
    ty of
                  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 (HasCallStack => TypeEnv -> Type -> Either Nat' TValue
    TypeEnv -> Type -> Either Nat' TValue
    evalType TypeEnv
    env) [Type]
    vs)
                  k :: Kind
    k -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "evalType"
                    [ "Unsupported"
                    , "*** 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)
                    , "*** 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)
                    ]

            -- FIXME: What about TCNewtype?
            _ -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "evalType" ["not a value type", Type -> String
    forall a. Show a => a -> String
    show Type
    ty]
        TCon (TF f :: TFun
    f) ts :: [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
    $ HasCallStack => TFun -> [Nat'] -> Nat'
    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 p :: PC
    p) _       -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "evalType" ["invalid predicate symbol", PC -> String
    forall a. Show a => a -> String
    show PC
    p]
        TCon (TError _ x :: TCErrorMessage
    x) _ -> String -> [String] -> Either Nat' TValue
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "evalType"
                                    ["Lingering typer error", Doc -> String
    forall a. Show a => a -> String
    show (TCErrorMessage -> Doc
    forall a. PP a => a -> Doc
    pp TCErrorMessage
    x)]
      where
        val :: Type -> TValue
    val = HasCallStack => TypeEnv -> Type -> TValue
    TypeEnv -> Type -> TValue
    evalValType TypeEnv
    env
        num :: Type -> Nat'
    num = HasCallStack => TypeEnv -> Type -> Nat'
    TypeEnv -> Type -> Nat'
    evalNumType TypeEnv
    env

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

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

    -- | Reduce type functions, raising an exception for undefined values.
    evalTF :: HasCallStack => TFun -> [Nat'] -> Nat'
    evalTF :: TFun -> [Nat'] -> Nat'
    evalTF f :: TFun
    f vs :: [Nat']
    vs
      | TFun
    TCAdd           <- TFun
    f, [x :: Nat'
    x,y :: Nat'
    y]   <- [Nat']
    vs  =      Nat' -> Nat' -> Nat'
    nAdd Nat'
    x Nat'
    y
      | TFun
    TCSub           <- TFun
    f, [x :: Nat'
    x,y :: 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, [x :: Nat'
    x,y :: Nat'
    y]   <- [Nat']
    vs  =      Nat' -> Nat' -> Nat'
    nMul Nat'
    x Nat'
    y
      | TFun
    TCDiv           <- TFun
    f, [x :: Nat'
    x,y :: 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, [x :: Nat'
    x,y :: 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, [x :: Nat'
    x]     <- [Nat']
    vs  =      Nat' -> Nat'
    nWidth Nat'
    x
      | TFun
    TCExp           <- TFun
    f, [x :: Nat'
    x,y :: Nat'
    y]   <- [Nat']
    vs  =      Nat' -> Nat' -> Nat'
    nExp Nat'
    x Nat'
    y
      | TFun
    TCMin           <- TFun
    f, [x :: Nat'
    x,y :: Nat'
    y]   <- [Nat']
    vs  =      Nat' -> Nat' -> Nat'
    nMin Nat'
    x Nat'
    y
      | TFun
    TCMax           <- TFun
    f, [x :: Nat'
    x,y :: Nat'
    y]   <- [Nat']
    vs  =      Nat' -> Nat' -> Nat'
    nMax Nat'
    x Nat'
    y
      | TFun
    TCCeilDiv       <- TFun
    f, [x :: Nat'
    x,y :: 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, [x :: Nat'
    x,y :: 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, [x :: Nat'
    x,y :: Nat'
    y,z :: 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 "evalTF"
                            ["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 (Type -> a
    forall a. Type -> a
    typeCannotBeDemoted 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)