{-# 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
data TValue
= TVBit
| TVInteger
| TVIntMod Integer
| TVSeq Integer TValue
| TVStream TValue
| TVTuple [TValue]
| TVRec [(Ident, TValue)]
| TVFun TValue TValue
| TVAbstract UserTC [Either Nat' TValue]
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)
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)
isTBit :: TValue -> Bool
isTBit :: TValue -> Bool
isTBit TVBit = Bool
True
isTBit _ = Bool
False
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
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 TypeEnv = Map.Map TVar (Either Nat' TValue)
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)
]
_ -> 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
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
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"]
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)