-- |
-- 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 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. 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, TValue -> TValue -> Bool
(TValue -> TValue -> Bool)
-> (TValue -> TValue -> Bool) -> Eq TValue
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 (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)
    TVNewtype Newtype
nt [Either Nat' TValue]
vs RecordMap Ident TValue
_ -> Newtype -> [Type] -> Type
tNewtype Newtype
nt ((Either Nat' TValue -> Type) -> [Either Nat' TValue] -> [Type]
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 ((Either Nat' TValue -> Type) -> [Either Nat' TValue] -> [Type]
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) = Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n

tNumValTy :: Either Nat' TValue -> Type
tNumValTy :: Either Nat' TValue -> Type
tNumValTy = (Nat' -> Type) -> (TValue -> Type) -> Either Nat' TValue -> Type
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 = 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 -------------------------------------------------------------

newtype TypeEnv =
  TypeEnv
  { TypeEnv -> IntMap (Either Nat' TValue)
envTypeMap  :: IntMap.IntMap (Either Nat' TValue) }

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

instance Semigroup TypeEnv where
  TypeEnv
l <> :: TypeEnv -> TypeEnv -> TypeEnv
<> TypeEnv
r = TypeEnv :: IntMap (Either Nat' TValue) -> TypeEnv
TypeEnv
    { envTypeMap :: IntMap (Either Nat' TValue)
envTypeMap  = IntMap (Either Nat' TValue)
-> IntMap (Either Nat' TValue) -> IntMap (Either Nat' TValue)
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 = Int -> IntMap (Either Nat' TValue) -> Maybe (Either Nat' TValue)
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 = Int
-> Either Nat' TValue
-> IntMap (Either Nat' TValue)
-> IntMap (Either Nat' TValue)
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 -> 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)

    TNewtype Newtype
nt [Type]
ts -> 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
$ Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue -> TValue
TVNewtype Newtype
nt [Either Nat' TValue]
tvs (RecordMap Ident TValue -> TValue)
-> RecordMap Ident TValue -> TValue
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 = (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]
ts

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

        (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`"]

-- | 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 = (Type -> TValue) -> RecordMap Ident Type -> RecordMap Ident TValue
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]
_ = String -> [String] -> TypeEnv
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'
_ -> 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 (String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalTF" [String
"type cannot be demoted", Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. PP a => a -> Doc
pp 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)