1-- | 2-- Module : Cryptol.Eval.Type 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8 9{-# LANGUAGE Safe, PatternGuards #-} 10{-# LANGUAGE DeriveAnyClass #-} 11{-# LANGUAGE DeriveGeneric #-} 12module Cryptol.Eval.Type where 13 14import Cryptol.Backend.Monad (evalPanic) 15import Cryptol.TypeCheck.AST 16import Cryptol.TypeCheck.PP(pp) 17import Cryptol.TypeCheck.Solver.InfNat 18import Cryptol.Utils.Panic (panic) 19import Cryptol.Utils.Ident (Ident) 20import Cryptol.Utils.RecordMap 21 22import Data.Maybe(fromMaybe) 23import qualified Data.IntMap.Strict as IntMap 24import GHC.Generics (Generic) 25import Control.DeepSeq 26 27-- | An evaluated type of kind *. 28-- These types do not contain type variables, type synonyms, or type functions. 29data TValue 30 = TVBit -- ^ @ Bit @ 31 | TVInteger -- ^ @ Integer @ 32 | TVFloat Integer Integer -- ^ @ Float e p @ 33 | TVIntMod Integer -- ^ @ Z n @ 34 | TVRational -- ^ @Rational@ 35 | TVArray TValue TValue -- ^ @ Array a b @ 36 | TVSeq Integer TValue -- ^ @ [n]a @ 37 | TVStream TValue -- ^ @ [inf]t @ 38 | TVTuple [TValue] -- ^ @ (a, b, c )@ 39 | TVRec (RecordMap Ident TValue) -- ^ @ { x : a, y : b, z : c } @ 40 | TVFun TValue TValue -- ^ @ a -> b @ 41 | TVNewtype Newtype 42 [Either Nat' TValue] 43 (RecordMap Ident TValue) -- ^ a named newtype 44 | TVAbstract UserTC [Either Nat' TValue] -- ^ an abstract type 45 deriving (Generic, NFData, Eq) 46 47-- | Convert a type value back into a regular type 48tValTy :: TValue -> Type 49tValTy tv = 50 case tv of 51 TVBit -> tBit 52 TVInteger -> tInteger 53 TVFloat e p -> tFloat (tNum e) (tNum p) 54 TVIntMod n -> tIntMod (tNum n) 55 TVRational -> tRational 56 TVArray a b -> tArray (tValTy a) (tValTy b) 57 TVSeq n t -> tSeq (tNum n) (tValTy t) 58 TVStream t -> tSeq tInf (tValTy t) 59 TVTuple ts -> tTuple (map tValTy ts) 60 TVRec fs -> tRec (fmap tValTy fs) 61 TVFun t1 t2 -> tFun (tValTy t1) (tValTy t2) 62 TVNewtype nt vs _ -> tNewtype nt (map tNumValTy vs) 63 TVAbstract u vs -> tAbstract u (map tNumValTy vs) 64 65tNumTy :: Nat' -> Type 66tNumTy Inf = tInf 67tNumTy (Nat n) = tNum n 68 69tNumValTy :: Either Nat' TValue -> Type 70tNumValTy = either tNumTy tValTy 71 72 73instance Show TValue where 74 showsPrec p v = showsPrec p (tValTy v) 75 76 77-- Utilities ------------------------------------------------------------------- 78 79-- | True if the evaluated value is @Bit@ 80isTBit :: TValue -> Bool 81isTBit TVBit = True 82isTBit _ = False 83 84-- | Produce a sequence type value 85tvSeq :: Nat' -> TValue -> TValue 86tvSeq (Nat n) t = TVSeq n t 87tvSeq Inf t = TVStream t 88 89-- | Coerce an extended natural into an integer, 90-- for values known to be finite 91finNat' :: Nat' -> Integer 92finNat' n' = 93 case n' of 94 Nat x -> x 95 Inf -> panic "Cryptol.Eval.Value.finNat'" [ "Unexpected `inf`" ] 96 97 98-- Type Evaluation ------------------------------------------------------------- 99 100newtype TypeEnv = 101 TypeEnv 102 { envTypeMap :: IntMap.IntMap (Either Nat' TValue) } 103 104instance Monoid TypeEnv where 105 mempty = TypeEnv mempty 106 107instance Semigroup TypeEnv where 108 l <> r = TypeEnv 109 { envTypeMap = IntMap.union (envTypeMap l) (envTypeMap r) } 110 111lookupTypeVar :: TVar -> TypeEnv -> Maybe (Either Nat' TValue) 112lookupTypeVar tv env = IntMap.lookup (tvUnique tv) (envTypeMap env) 113 114bindTypeVar :: TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv 115bindTypeVar tv ty env = env{ envTypeMap = IntMap.insert (tvUnique tv) ty (envTypeMap env) } 116 117-- | Evaluation for types (kind * or #). 118evalType :: TypeEnv -> Type -> Either Nat' TValue 119evalType env ty = 120 case ty of 121 TVar tv -> 122 case lookupTypeVar tv env of 123 Just v -> v 124 Nothing -> evalPanic "evalType" ["type variable not bound", show tv] 125 126 TUser _ _ ty' -> evalType env ty' 127 TRec fields -> Right $ TVRec (fmap val fields) 128 129 TNewtype nt ts -> Right $ TVNewtype nt tvs $ evalNewtypeBody env nt tvs 130 where tvs = map (evalType env) ts 131 132 TCon (TC c) ts -> 133 case (c, ts) of 134 (TCBit, []) -> Right $ TVBit 135 (TCInteger, []) -> Right $ TVInteger 136 (TCRational, []) -> Right $ TVRational 137 (TCFloat, [e,p])-> Right $ TVFloat (inum e) (inum p) 138 (TCIntMod, [n]) -> case num n of 139 Inf -> evalPanic "evalType" ["invalid type Z inf"] 140 Nat m -> Right $ TVIntMod m 141 (TCArray, [a, b]) -> Right $ TVArray (val a) (val b) 142 (TCSeq, [n, t]) -> Right $ tvSeq (num n) (val t) 143 (TCFun, [a, b]) -> Right $ TVFun (val a) (val b) 144 (TCTuple _, _) -> Right $ TVTuple (map val ts) 145 (TCNum n, []) -> Left $ Nat n 146 (TCInf, []) -> Left $ Inf 147 (TCAbstract u,vs) -> 148 case kindOf ty of 149 KType -> Right $ TVAbstract u (map (evalType env) vs) 150 k -> evalPanic "evalType" 151 [ "Unsupported" 152 , "*** Abstract type of kind: " ++ show (pp k) 153 , "*** Name: " ++ show (pp u) 154 ] 155 156 _ -> evalPanic "evalType" ["not a value type", show ty] 157 TCon (TF f) ts -> Left $ evalTF f (map num ts) 158 TCon (PC p) _ -> evalPanic "evalType" ["invalid predicate symbol", show p] 159 TCon (TError _) ts -> evalPanic "evalType" 160 $ "Lingering invalid type" : map (show . pp) ts 161 where 162 val = evalValType env 163 num = evalNumType env 164 inum x = case num x of 165 Nat i -> i 166 Inf -> evalPanic "evalType" 167 ["Expecting a finite size, but got `inf`"] 168 169-- | Evaluate the body of a newtype, given evaluated arguments 170evalNewtypeBody :: TypeEnv -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue 171evalNewtypeBody env0 nt args = fmap (evalValType env') (ntFields nt) 172 where 173 env' = loop env0 (ntParams nt) args 174 175 loop env [] [] = env 176 loop env (p:ps) (a:as) = loop (bindTypeVar (TVBound p) a env) ps as 177 loop _ _ _ = evalPanic "evalNewtype" ["type parameter/argument mismatch"] 178 179-- | Evaluation for value types (kind *). 180evalValType :: TypeEnv -> Type -> TValue 181evalValType env ty = 182 case evalType env ty of 183 Left _ -> evalPanic "evalValType" ["expected value type, found numeric type"] 184 Right t -> t 185 186-- | Evaluation for number types (kind #). 187evalNumType :: TypeEnv -> Type -> Nat' 188evalNumType env ty = 189 case evalType env ty of 190 Left n -> n 191 Right _ -> evalPanic "evalValType" ["expected numeric type, found value type"] 192 193 194-- | Reduce type functions, raising an exception for undefined values. 195evalTF :: TFun -> [Nat'] -> Nat' 196evalTF f vs 197 | TCAdd <- f, [x,y] <- vs = nAdd x y 198 | TCSub <- f, [x,y] <- vs = mb $ nSub x y 199 | TCMul <- f, [x,y] <- vs = nMul x y 200 | TCDiv <- f, [x,y] <- vs = mb $ nDiv x y 201 | TCMod <- f, [x,y] <- vs = mb $ nMod x y 202 | TCWidth <- f, [x] <- vs = nWidth x 203 | TCExp <- f, [x,y] <- vs = nExp x y 204 | TCMin <- f, [x,y] <- vs = nMin x y 205 | TCMax <- f, [x,y] <- vs = nMax x y 206 | TCCeilDiv <- f, [x,y] <- vs = mb $ nCeilDiv x y 207 | TCCeilMod <- f, [x,y] <- vs = mb $ nCeilMod x y 208 | TCLenFromThenTo <- f, [x,y,z] <- vs = mb $ nLenFromThenTo x y z 209 | otherwise = evalPanic "evalTF" 210 ["Unexpected type function:", show ty] 211 212 where mb = fromMaybe (evalPanic "evalTF" ["type cannot be demoted", show (pp ty)]) 213 ty = TCon (TF f) (map tNat' vs) 214