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