-- |
-- 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. 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 -> ()
forall a. (a -> ()) -> NFData a
rnf :: TValue -> ()
$crnf :: TValue -> ()
NFData, TValue -> TValue -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TValue -> TValue -> Bool
$c/= :: TValue -> TValue -> Bool
== :: TValue -> TValue -> Bool
$c== :: 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 (forall a. Integral a => a -> Type
tNum Integer
e) (forall a. Integral a => a -> Type
tNum Integer
p)
    TVIntMod Integer
n  -> Type -> Type
tIntMod (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 (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 (forall a b. (a -> b) -> [a] -> [b]
map TValue -> Type
tValTy [TValue]
ts)
    TVRec RecordMap Ident TValue
fs    -> RecordMap Ident Type -> Type
tRec (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 (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 (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) = forall a. Integral a => a -> Type
tNum Integer
n

tNumValTy :: Either Nat' TValue -> Type
tNumValTy :: Either Nat' TValue -> Type
tNumValTy = 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 = 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 = 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   -> 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeEnv] -> ShowS
$cshowList :: [TypeEnv] -> ShowS
show :: TypeEnv -> String
$cshow :: TypeEnv -> String
showsPrec :: Int -> TypeEnv -> ShowS
$cshowsPrec :: Int -> TypeEnv -> ShowS
Show)

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

instance Semigroup TypeEnv where
  TypeEnv
l <> :: TypeEnv -> TypeEnv -> TypeEnv
<> TypeEnv
r = TypeEnv
    { envTypeMap :: IntMap (Either Nat' TValue)
envTypeMap  = 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 = 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 = 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 -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalType" [String
"type variable not bound", 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    -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ RecordMap Ident TValue -> TValue
TVRec (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 -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue -> TValue
TVNewtype Newtype
nt [Either Nat' TValue]
tvs 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 = 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, [])     -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ TValue
TVBit
        (TC
TCInteger, []) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ TValue
TVInteger
        (TC
TCRational, []) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ TValue
TVRational
        (TC
TCFloat, [Type
e,Type
p])-> forall a b. b -> Either a b
Right 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   -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalType" [String
"invalid type Z inf"]
                             Nat Integer
m -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ Integer -> TValue
TVIntMod Integer
m
        (TC
TCArray, [Type
a, Type
b]) -> forall a b. b -> Either a b
Right 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]) -> forall a b. b -> Either a b
Right 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]) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ TValue -> TValue -> TValue
TVFun (Type -> TValue
val Type
a) (Type -> TValue
val Type
b)
        (TCTuple Int
_, [Type]
_)  -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ [TValue] -> TValue
TVTuple (forall a b. (a -> b) -> [a] -> [b]
map Type -> TValue
val [Type]
ts)
        (TCNum Integer
n, [])   -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Integer -> Nat'
Nat Integer
n
        (TC
TCInf, [])     -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Nat'
Inf
        (TCAbstract UserTC
u,[Type]
vs) ->
            case forall t. HasKind t => t -> Kind
kindOf Type
ty of
              Kind
KType -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ UserTC -> [Either Nat' TValue] -> TValue
TVAbstract UserTC
u (forall a b. (a -> b) -> [a] -> [b]
map (TypeEnv -> Type -> Either Nat' TValue
evalType TypeEnv
env) [Type]
vs)
              Kind
k -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalType"
                [ String
"Unsupported"
                , String
"*** Abstract type of kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp Kind
k)
                , String
"*** Name: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp UserTC
u)
                ]

        (TC, [Type])
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalType" [String
"not a value type", forall a. Show a => a -> String
show Type
ty]
    TCon (TF TFun
f) [Type]
ts      -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ TFun -> [Nat'] -> Nat'
evalTF TFun
f (forall a b. (a -> b) -> [a] -> [b]
map Type -> Nat'
num [Type]
ts)
    TCon (PC PC
p) [Type]
_       -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalType" [String
"invalid predicate symbol", forall a. Show a => a -> String
show PC
p]
    TCon (TError Kind
_) [Type]
ts -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalType"
                             forall a b. (a -> b) -> a -> b
$ String
"Lingering invalid type" forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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   -> 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 = 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]
_ = 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'
_ -> 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
_ -> 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  = forall {a}. Maybe a -> a
mb 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  = forall {a}. Maybe a -> a
mb 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  = forall {a}. Maybe a -> a
mb 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  = forall {a}. Maybe a -> a
mb 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  = forall {a}. Maybe a -> a
mb 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  = forall {a}. Maybe a -> a
mb forall a b. (a -> b) -> a -> b
$ Nat' -> Nat' -> Nat' -> Maybe Nat'
nLenFromThenTo Nat'
x Nat'
y Nat'
z
  | Bool
otherwise  = forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalTF"
                        [String
"Unexpected type function:", forall a. Show a => a -> String
show Type
ty]

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