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