-- |
-- 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, typeCannotBeDemoted)
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 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 @
  | 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 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 (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)
    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
arg [Either Nat' TValue]
vs)
      where arg :: Either Nat' TValue -> Type
arg Either Nat' TValue
x = case Either Nat' TValue
x of
                      Left Nat'
Inf     -> Type
tInf
                      Left (Nat Integer
n) -> Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n
                      Right TValue
v      -> TValue -> Type
tValTy TValue
v


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

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

type TypeEnv = IntMap.IntMap (Either Nat' TValue)


-- | 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 Int -> TypeEnv -> Maybe (Either Nat' TValue)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (TVar -> Int
tvUnique 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> TValue
val RecordMap Ident Type
fields)
    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)
                ]

        -- FIXME: What about TCNewtype?
        (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`"]

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