Type.hs

-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2013-2015 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE Safe, PatternGuards #-}

module Cryptol.Eval.Type (evalType, evalTF) where

import Cryptol.Eval.Env
import Cryptol.Eval.Error
import Cryptol.Eval.Value(TValue(..),numTValue)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat

import Data.Maybe(fromMaybe)


-- Type Evaluation -------------------------------------------------------------

-- | Evaluation for types.
evalType :: EvalEnv -> Type -> TValue
evalType env = TValue . go
  where
  go ty =
    case ty of
      TVar tv ->
        case lookupType tv env of
          Just (TValue v)   -> v
          Nothing  -> evalPanic "evalType" ["type variable not bound", show tv]

      TCon (TF f) ts -> tValTy $ evalTF f $ map (evalType env) ts
      TCon tc ts     -> TCon tc (map go ts)
      TUser _ _ ty'  -> go ty'
      TRec fields    -> TRec [ (f,go t) | (f,t) <- fields ]

-- | Reduce type functions, rising an exception for undefined values.
evalTF :: TFun -> [TValue] -> TValue
evalTF tf vs = TValue $ cvt $ evalTF' tf $ map numTValue vs

-- | Reduce type functions, rising an exception for undefined values.
evalTF' :: TFun -> [Nat'] -> Nat'
evalTF' f vs
  | TCAdd           <- f, [x,y]   <- vs  =      nAdd x y
  | TCSub           <- f, [x,y]   <- vs  = mb $ nSub x y
  | TCMul           <- f, [x,y]   <- vs  =      nMul x y
  | TCDiv           <- f, [x,y]   <- vs  = mb $ nDiv x y
  | TCMod           <- f, [x,y]   <- vs  = mb $ nMod x y
  | TCLg2           <- f, [x]     <- vs  =      nLg2 x
  | TCWidth         <- f, [x]     <- vs  =      nWidth x
  | TCExp           <- f, [x,y]   <- vs  =      nExp x y
  | TCMin           <- f, [x,y]   <- vs  =      nMin x y
  | TCMax           <- f, [x,y]   <- vs  =      nMax x y
  | TCLenFromThen   <- f, [x,y,z] <- vs  = mb $ nLenFromThen x y z
  | TCLenFromThenTo <- f, [x,y,z] <- vs  = mb $ nLenFromThenTo x y z
  | otherwise  = evalPanic "evalTF"
                        ["Unexpected type function:", show ty]

  where mb = fromMaybe (typeCannotBeDemoted ty)
        ty = TCon (TF f) (map cvt vs)


cvt :: Nat' -> Type
cvt (Nat n) = tNum n
cvt Inf     = tInf