module Copilot.Compile.C99.Witness
( ExprInst (..) , exprInst
, AssignInst (..) , assignInst
, EqEInst (..) , eqEInst
, OrdEInst (..) , ordEInst
, NumEInst (..) , numEInst
, IntegralEInst (..) , integralEInst
, FloatingEInst (..) , floatingEInst
, BitsEInst (..) , bitsEInst
) where
import qualified Language.Atom as A
import qualified Copilot.Core as C
import Data.Bits
badInst :: a
badInst = C.impossible "witnesses" "copilot-c99"
data ExprInst a = A.Expr a => ExprInst
exprInst :: C.Type a -> ExprInst a
exprInst t =
case t of
C.Bool -> ExprInst
C.Int8 -> ExprInst ; C.Int16 -> ExprInst
C.Int32 -> ExprInst ; C.Int64 -> ExprInst
C.Word8 -> ExprInst ; C.Word16 -> ExprInst
C.Word32 -> ExprInst ; C.Word64 -> ExprInst
C.Float -> ExprInst ; C.Double -> ExprInst
data AssignInst a = A.Assign a => AssignInst
assignInst :: C.Type a -> AssignInst a
assignInst t =
case t of
C.Bool -> AssignInst
C.Int8 -> AssignInst ; C.Int16 -> AssignInst
C.Int32 -> AssignInst ; C.Int64 -> AssignInst
C.Word8 -> AssignInst ; C.Word16 -> AssignInst
C.Word32 -> AssignInst ; C.Word64 -> AssignInst
C.Float -> AssignInst ; C.Double -> AssignInst
data EqEInst a = A.EqE a => EqEInst
eqEInst :: Eq a => C.Type a -> EqEInst a
eqEInst t =
case t of
C.Bool -> EqEInst
C.Int8 -> EqEInst ; C.Int16 -> EqEInst
C.Int32 -> EqEInst ; C.Int64 -> EqEInst
C.Word8 -> EqEInst ; C.Word16 -> EqEInst
C.Word32 -> EqEInst ; C.Word64 -> EqEInst
C.Float -> EqEInst ; C.Double -> EqEInst
data OrdEInst a = A.OrdE a => OrdEInst
ordEInst :: Ord a => C.Type a -> OrdEInst a
ordEInst t =
case t of
C.Bool -> badInst
C.Int8 -> OrdEInst ; C.Int16 -> OrdEInst
C.Int32 -> OrdEInst ; C.Int64 -> OrdEInst
C.Word8 -> OrdEInst ; C.Word16 -> OrdEInst
C.Word32 -> OrdEInst ; C.Word64 -> OrdEInst
C.Float -> OrdEInst ; C.Double -> OrdEInst
data NumEInst a = A.NumE a => NumEInst
numEInst :: Num a => C.Type a -> NumEInst a
numEInst t =
case t of
C.Bool -> badInst
C.Int8 -> NumEInst ; C.Int16 -> NumEInst
C.Int32 -> NumEInst ; C.Int64 -> NumEInst
C.Word8 -> NumEInst ; C.Word16 -> NumEInst
C.Word32 -> NumEInst ; C.Word64 -> NumEInst
C.Float -> NumEInst ; C.Double -> NumEInst
data IntegralEInst a = A.IntegralE a => IntegralEInst
integralEInst :: Integral a => C.Type a -> IntegralEInst a
integralEInst t =
case t of
C.Bool -> badInst
C.Int8 -> IntegralEInst ; C.Int16 -> IntegralEInst
C.Int32 -> IntegralEInst ; C.Int64 -> IntegralEInst
C.Word8 -> IntegralEInst ; C.Word16 -> IntegralEInst
C.Word32 -> IntegralEInst ; C.Word64 -> IntegralEInst
C.Float -> badInst
C.Double -> badInst
data FloatingEInst a = A.FloatingE a => FloatingEInst
floatingEInst :: Floating a => C.Type a -> FloatingEInst a
floatingEInst t =
case t of
C.Float -> FloatingEInst
C.Double -> FloatingEInst
_ -> badInst
data BitsEInst a = ( A.Expr a, A.OrdE a, A.EqE a, A.IntegralE a, Bits a ) => BitsEInst
bitsEInst :: Bits a => C.Type a -> BitsEInst a
bitsEInst t =
case t of
C.Bool -> badInst
C.Int8 -> BitsEInst
C.Int16 -> BitsEInst
C.Int32 -> BitsEInst
C.Int64 -> BitsEInst
C.Word8 -> BitsEInst
C.Word16 -> BitsEInst
C.Word32 -> BitsEInst
C.Word64 -> BitsEInst
C.Float -> badInst
C.Double -> badInst