{-|
Copyright        : (c) Galois, Inc 2015
Maintainer       : Joe Hendrix <jhendrix@galois.com>

The type of machine words, including bit vectors and floating point
-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Macaw.Types
  ( module Data.Macaw.Types -- export everything
  , GHC.TypeLits.KnownNat
  , GHC.TypeLits.Nat
  , Data.Parameterized.NatRepr.NatRepr(..)
  , Data.Parameterized.NatRepr.knownNat
  ) where

import qualified Data.Kind as Kind
import           Data.Parameterized.Classes
import qualified Data.Parameterized.List as P
import           Data.Parameterized.NatRepr
import           Data.Parameterized.TH.GADT
import           Data.Parameterized.TraversableFC
import           GHC.TypeLits
import qualified Language.Haskell.TH.Syntax as TH
import           Prettyprinter

-- FIXME: move
n0 :: NatRepr 0
n0 :: NatRepr 0
n0 = NatRepr 0
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

n1 :: NatRepr 1
n1 :: NatRepr 1
n1 = NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

n4 :: NatRepr 4
n4 :: NatRepr 4
n4 = NatRepr 4
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

n8 :: NatRepr 8
n8 :: NatRepr 8
n8 = NatRepr 8
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

n16 :: NatRepr 16
n16 :: NatRepr 16
n16 = NatRepr 16
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

n32 :: NatRepr 32
n32 :: NatRepr 32
n32 = NatRepr 32
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

n64 :: NatRepr 64
n64 :: NatRepr 64
n64 = NatRepr 64
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

n80 :: NatRepr 80
n80 :: NatRepr 80
n80 = NatRepr 80
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

n128 :: NatRepr 128
n128 :: NatRepr 128
n128 = NatRepr 128
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

n256 :: NatRepr 256
n256 :: NatRepr 256
n256 = NatRepr 256
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

n512 :: NatRepr 512
n512 :: NatRepr 512
n512 = NatRepr 512
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

------------------------------------------------------------------------
-- Floating point sizes

data FloatInfo
  = HalfFloat   -- ^ 16 bit binary IEE754*
  | SingleFloat -- ^ 32 bit binary IEE754
  | DoubleFloat -- ^ 64 bit binary IEE754
  | QuadFloat   -- ^ 128 bit binary IEE754
  | X86_80Float -- ^ X86 80-bit extended floats

type HalfFloat   = 'HalfFloat
type SingleFloat = 'SingleFloat
type DoubleFloat = 'DoubleFloat
type QuadFloat   = 'QuadFloat
type X86_80Float = 'X86_80Float

data FloatInfoRepr (fi :: FloatInfo) where
  HalfFloatRepr   :: FloatInfoRepr HalfFloat
  SingleFloatRepr :: FloatInfoRepr SingleFloat
  DoubleFloatRepr :: FloatInfoRepr DoubleFloat
  QuadFloatRepr   :: FloatInfoRepr QuadFloat
  X86_80FloatRepr :: FloatInfoRepr X86_80Float

deriving instance Eq (FloatInfoRepr fi)

instance KnownRepr FloatInfoRepr HalfFloat where
  knownRepr :: FloatInfoRepr 'HalfFloat
knownRepr = FloatInfoRepr 'HalfFloat
HalfFloatRepr
instance KnownRepr FloatInfoRepr SingleFloat where
  knownRepr :: FloatInfoRepr 'SingleFloat
knownRepr = FloatInfoRepr 'SingleFloat
SingleFloatRepr
instance KnownRepr FloatInfoRepr DoubleFloat where
  knownRepr :: FloatInfoRepr 'DoubleFloat
knownRepr = FloatInfoRepr 'DoubleFloat
DoubleFloatRepr
instance KnownRepr FloatInfoRepr QuadFloat where
  knownRepr :: FloatInfoRepr 'QuadFloat
knownRepr = FloatInfoRepr 'QuadFloat
QuadFloatRepr
instance KnownRepr FloatInfoRepr X86_80Float where
  knownRepr :: FloatInfoRepr 'X86_80Float
knownRepr = FloatInfoRepr 'X86_80Float
X86_80FloatRepr

instance Hashable (FloatInfoRepr fi) where
  hashWithSalt :: Int -> FloatInfoRepr fi -> Int
hashWithSalt Int
s FloatInfoRepr fi
r =
    let i ::Int
        i :: Int
i = case FloatInfoRepr fi
r of
              FloatInfoRepr fi
HalfFloatRepr   -> Int
0
              FloatInfoRepr fi
SingleFloatRepr -> Int
1
              FloatInfoRepr fi
DoubleFloatRepr -> Int
2
              FloatInfoRepr fi
QuadFloatRepr   -> Int
3
              FloatInfoRepr fi
X86_80FloatRepr -> Int
4
     in Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Int
i

instance HashableF FloatInfoRepr where
  hashWithSaltF :: forall (fi :: FloatInfo). Int -> FloatInfoRepr fi -> Int
hashWithSaltF = Int -> FloatInfoRepr tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt

instance Show (FloatInfoRepr fi) where
  show :: FloatInfoRepr fi -> String
show FloatInfoRepr fi
HalfFloatRepr   = String
"half"
  show FloatInfoRepr fi
SingleFloatRepr = String
"single"
  show FloatInfoRepr fi
DoubleFloatRepr = String
"double"
  show FloatInfoRepr fi
QuadFloatRepr   = String
"quad"
  show FloatInfoRepr fi
X86_80FloatRepr = String
"x87_80"

instance ShowF FloatInfoRepr where

instance Pretty (FloatInfoRepr fi) where
  pretty :: forall ann. FloatInfoRepr fi -> Doc ann
pretty = FloatInfoRepr fi -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow

deriving instance TH.Lift (FloatInfoRepr fi)

type family FloatInfoBytes (fi :: FloatInfo) :: Nat where
  FloatInfoBytes HalfFloat   = 2
  FloatInfoBytes SingleFloat = 4
  FloatInfoBytes DoubleFloat = 8
  FloatInfoBytes QuadFloat   = 16
  FloatInfoBytes X86_80Float = 10

floatInfoBytes :: FloatInfoRepr fi -> NatRepr (FloatInfoBytes fi)
floatInfoBytes :: forall (fi :: FloatInfo).
FloatInfoRepr fi -> NatRepr (FloatInfoBytes fi)
floatInfoBytes = \case
  FloatInfoRepr fi
HalfFloatRepr   -> NatRepr 2
NatRepr (FloatInfoBytes fi)
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
  FloatInfoRepr fi
SingleFloatRepr -> NatRepr 4
NatRepr (FloatInfoBytes fi)
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
  FloatInfoRepr fi
DoubleFloatRepr -> NatRepr 8
NatRepr (FloatInfoBytes fi)
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
  FloatInfoRepr fi
QuadFloatRepr   -> NatRepr 16
NatRepr (FloatInfoBytes fi)
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
  FloatInfoRepr fi
X86_80FloatRepr -> NatRepr 10
NatRepr (FloatInfoBytes fi)
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

floatInfoBytesIsPos :: FloatInfoRepr fi -> LeqProof 1 (FloatInfoBytes fi)
floatInfoBytesIsPos :: forall (fi :: FloatInfo).
FloatInfoRepr fi -> LeqProof 1 (FloatInfoBytes fi)
floatInfoBytesIsPos = \case
  FloatInfoRepr fi
HalfFloatRepr   -> LeqProof 1 2
LeqProof 1 (FloatInfoBytes fi)
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
  FloatInfoRepr fi
SingleFloatRepr -> LeqProof 1 4
LeqProof 1 (FloatInfoBytes fi)
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
  FloatInfoRepr fi
DoubleFloatRepr -> LeqProof 1 8
LeqProof 1 (FloatInfoBytes fi)
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
  FloatInfoRepr fi
QuadFloatRepr   -> LeqProof 1 16
LeqProof 1 (FloatInfoBytes fi)
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
  FloatInfoRepr fi
X86_80FloatRepr -> LeqProof 1 10
LeqProof 1 (FloatInfoBytes fi)
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof

type FloatInfoBits (fi :: FloatInfo) = 8 * FloatInfoBytes fi

floatInfoBits :: FloatInfoRepr fi -> NatRepr (FloatInfoBits fi)
floatInfoBits :: forall (fi :: FloatInfo).
FloatInfoRepr fi -> NatRepr (FloatInfoBits fi)
floatInfoBits = NatRepr 8
-> NatRepr (FloatInfoBytes fi) -> NatRepr (8 * FloatInfoBytes fi)
forall (n :: Nat) (m :: Nat).
NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @8) (NatRepr (FloatInfoBytes fi) -> NatRepr (8 * FloatInfoBytes fi))
-> (FloatInfoRepr fi -> NatRepr (FloatInfoBytes fi))
-> FloatInfoRepr fi
-> NatRepr (8 * FloatInfoBytes fi)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FloatInfoRepr fi -> NatRepr (FloatInfoBytes fi)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> NatRepr (FloatInfoBytes fi)
floatInfoBytes

floatInfoBitsIsPos :: FloatInfoRepr fi -> LeqProof 1 (FloatInfoBits fi)
floatInfoBitsIsPos :: forall (fi :: FloatInfo).
FloatInfoRepr fi -> LeqProof 1 (FloatInfoBits fi)
floatInfoBitsIsPos = \case
  FloatInfoRepr fi
HalfFloatRepr   -> LeqProof 1 16
LeqProof 1 (FloatInfoBits fi)
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
  FloatInfoRepr fi
SingleFloatRepr -> LeqProof 1 32
LeqProof 1 (FloatInfoBits fi)
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
  FloatInfoRepr fi
DoubleFloatRepr -> LeqProof 1 64
LeqProof 1 (FloatInfoBits fi)
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
  FloatInfoRepr fi
QuadFloatRepr   -> LeqProof 1 128
LeqProof 1 (FloatInfoBits fi)
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof
  FloatInfoRepr fi
X86_80FloatRepr -> LeqProof 1 80
LeqProof 1 (FloatInfoBits fi)
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof

$(return [])

------------------------------------------------------------------------
-- Type

data Type
  = -- | A bitvector with the given number of bits.
    BVType Nat
    -- | A floating point in the given format.
  | FloatType FloatInfo
    -- | A Boolean value
  | BoolType
    -- | A tuple of types
  | TupleType [Type]
    -- | A vector of types
  | VecType Nat Type


-- Return number of bytes in the type.
type family TypeBytes (tp :: Type) :: Nat where
  TypeBytes (BVType  8) = 1
  TypeBytes (BVType 16) = 2
  TypeBytes (BVType 32) = 4
  TypeBytes (BVType 64) = 8
  TypeBytes (FloatType fi) = FloatInfoBytes fi
  TypeBytes (VecType n tp) = n * TypeBytes tp

-- Return number of bits in the type.
type family TypeBits (tp :: Type) :: Nat where
  TypeBits (BVType n) = n
  TypeBits (FloatType fi) = 8 * FloatInfoBytes fi

type BVType = 'BVType

type FloatType = 'FloatType

type BoolType = 'BoolType

type TupleType = 'TupleType

type VecType = 'VecType

-- | The bitvector associated with the given floating-point format.
type FloatBVType (fi :: FloatInfo) = BVType (FloatInfoBits fi)

$(pure [])


-- | A runtime representation of @Type@ for case matching purposes.
data TypeRepr (tp :: Type) where
  BoolTypeRepr :: TypeRepr BoolType
  BVTypeRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
  FloatTypeRepr :: !(FloatInfoRepr fi) -> TypeRepr (FloatType fi)
  TupleTypeRepr :: !(P.List TypeRepr ctx) -> TypeRepr (TupleType ctx)
  VecTypeRepr :: NatRepr n -> TypeRepr tp -> TypeRepr (VecType n tp)

type_width :: TypeRepr (BVType n) -> NatRepr n
type_width :: forall (n :: Nat). TypeRepr (BVType n) -> NatRepr n
type_width (BVTypeRepr NatRepr n
n) = NatRepr n
NatRepr n
n

-- Pretty print using an s-expression syntax.
instance Pretty (TypeRepr tp) where
  pretty :: forall ann. TypeRepr tp -> Doc ann
pretty TypeRepr tp
BoolTypeRepr = Doc ann
"bool"
  pretty (BVTypeRepr NatRepr n
w) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"bv" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> NatRepr n -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow NatRepr n
w)
  pretty (FloatTypeRepr FloatInfoRepr fi
fi) = FloatInfoRepr fi -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow FloatInfoRepr fi
fi
  pretty (TupleTypeRepr List TypeRepr ctx
z) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ((forall (x :: Type). Doc ann -> TypeRepr x -> Doc ann)
-> forall (x :: [Type]). Doc ann -> List TypeRepr x -> Doc ann
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). b -> f x -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: Type -> Type) b.
(forall (x :: Type). b -> f x -> b)
-> forall (x :: [Type]). b -> List f x -> b
foldlFC (\Doc ann
l TypeRepr x
tp -> Doc ann
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeRepr x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeRepr x -> Doc ann
pretty TypeRepr x
tp) Doc ann
"tuple" List TypeRepr ctx
z)
  pretty (VecTypeRepr NatRepr n
c TypeRepr tp
tp) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"vec" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> NatRepr n -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow NatRepr n
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeRepr tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeRepr tp -> Doc ann
pretty TypeRepr tp
tp)

instance Show (TypeRepr tp) where
  show :: TypeRepr tp -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (TypeRepr tp -> Doc Any) -> TypeRepr tp -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRepr tp -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeRepr tp -> Doc ann
pretty

instance ShowF TypeRepr

instance KnownRepr TypeRepr BoolType where
  knownRepr :: TypeRepr 'BoolType
knownRepr = TypeRepr 'BoolType
BoolTypeRepr

instance (KnownNat n, 1 <= n) => KnownRepr TypeRepr (BVType n) where
  knownRepr :: TypeRepr (BVType n)
knownRepr = NatRepr n -> TypeRepr (BVType n)
forall (n :: Nat). (1 <= n) => NatRepr n -> TypeRepr (BVType n)
BVTypeRepr NatRepr n
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

instance (KnownRepr FloatInfoRepr fi) => KnownRepr TypeRepr (FloatType fi) where
  knownRepr :: TypeRepr (FloatType fi)
knownRepr = FloatInfoRepr fi -> TypeRepr (FloatType fi)
forall (n :: FloatInfo). FloatInfoRepr n -> TypeRepr (FloatType n)
FloatTypeRepr FloatInfoRepr fi
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance (KnownRepr (P.List TypeRepr) l) => KnownRepr TypeRepr  (TupleType l) where
  knownRepr :: TypeRepr (TupleType l)
knownRepr = List TypeRepr l -> TypeRepr (TupleType l)
forall (n :: [Type]). List TypeRepr n -> TypeRepr (TupleType n)
TupleTypeRepr List TypeRepr l
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance (KnownNat n, KnownRepr TypeRepr r) => KnownRepr TypeRepr (VecType n r) where
  knownRepr :: TypeRepr (VecType n r)
knownRepr = NatRepr n -> TypeRepr r -> TypeRepr (VecType n r)
forall (n :: Nat) (tp :: Type).
NatRepr n -> TypeRepr tp -> TypeRepr (VecType n tp)
VecTypeRepr NatRepr n
forall (n :: Nat). KnownNat n => NatRepr n
knownNat TypeRepr r
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

$(pure [])

instance TestEquality TypeRepr where
  testEquality :: forall (a :: Type) (b :: Type).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality = $(structuralTypeEquality [t|TypeRepr|]
    [ (ConType [t|NatRepr|]       `TypeApp` AnyType, [|testEquality|])
    , (ConType [t|TypeRepr|]      `TypeApp` AnyType, [|testEquality|])
    , (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|testEquality|])
    , ( ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType
      , [|testEquality|]
      )
    ])

instance OrdF TypeRepr where
  compareF :: forall (x :: Type) (y :: Type).
TypeRepr x -> TypeRepr y -> OrderingF x y
compareF = $(structuralTypeOrd [t|TypeRepr|]
    [ (ConType [t|NatRepr|]       `TypeApp` AnyType, [|compareF|])
    , (ConType [t|TypeRepr|]      `TypeApp` AnyType, [|compareF|])
    , (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|compareF|])
    , (ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType, [|compareF|])
    ])

instance TestEquality FloatInfoRepr where
  testEquality :: forall (a :: FloatInfo) (b :: FloatInfo).
FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b)
testEquality = $(structuralTypeEquality [t|FloatInfoRepr|] [])
instance OrdF FloatInfoRepr where
  compareF :: forall (x :: FloatInfo) (y :: FloatInfo).
FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y
compareF = $(structuralTypeOrd [t|FloatInfoRepr|] [])

floatBVTypeRepr :: FloatInfoRepr fi -> TypeRepr (FloatBVType fi)
floatBVTypeRepr :: forall (fi :: FloatInfo).
FloatInfoRepr fi -> TypeRepr (FloatBVType fi)
floatBVTypeRepr FloatInfoRepr fi
fi | LeqProof 1 (FloatInfoBits fi)
LeqProof <- FloatInfoRepr fi -> LeqProof 1 (FloatInfoBits fi)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> LeqProof 1 (FloatInfoBits fi)
floatInfoBitsIsPos FloatInfoRepr fi
fi =
  NatRepr (FloatInfoBits fi) -> TypeRepr (BVType (FloatInfoBits fi))
forall (n :: Nat). (1 <= n) => NatRepr n -> TypeRepr (BVType n)
BVTypeRepr (NatRepr (FloatInfoBits fi)
 -> TypeRepr (BVType (FloatInfoBits fi)))
-> NatRepr (FloatInfoBits fi)
-> TypeRepr (BVType (FloatInfoBits fi))
forall a b. (a -> b) -> a -> b
$ FloatInfoRepr fi -> NatRepr (FloatInfoBits fi)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> NatRepr (FloatInfoBits fi)
floatInfoBits FloatInfoRepr fi
fi

------------------------------------------------------------------------
--

-- | A multi-parameter type class that allows one to represent that a
-- parameterized type value has some representative type such as a TypeRepr.
class HasRepr (f :: k -> Kind.Type) (v :: k -> Kind.Type) | f -> v where
  typeRepr :: f tp -> v tp

typeWidth :: HasRepr f TypeRepr => f (BVType w) -> NatRepr w
typeWidth :: forall (f :: Type -> Type) (w :: Nat).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth f (BVType w)
x =
  case f (BVType w) -> TypeRepr (BVType w)
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). f tp -> TypeRepr tp
typeRepr f (BVType w)
x of
    BVTypeRepr NatRepr n
w -> NatRepr w
NatRepr n
w