-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Types
-- Description      : This module exports the types used in Crucible
--                    expressions.
-- Copyright        : (c) Galois, Inc 2014
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module exports the types used in Crucible expressions.
--
-- These types are largely used as indexes to various GADTs and type
-- families as a way to let the GHC typechecker help us keep expressions
-- of the embedded CFG language apart.
--
-- In addition, we provide a value-level reification of the type
-- indices that can be examined by pattern matching, called 'TypeRepr'.
-- The 'KnownRepr' class computes the value-level representation
-- of a given type index, when the type is known at compile time.
-- Similar setups exist for other components of the type system:
-- bitvector data and type contexts.
------------------------------------------------------------------------
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Lang.Crucible.Types
  ( -- * CrucibleType data kind
    type CrucibleType
    -- ** Constructors for kind CrucibleType
  , AnyType
  , UnitType
  , BoolType
  , NatType
  , IntegerType
  , RealValType
  , SymbolicStructType
  , ComplexRealType
  , BVType
  , FloatType
  , IEEEFloatType
  , CharType
  , StringType
  , FunctionHandleType
  , MaybeType
  , RecursiveType
  , IntrinsicType
  , VectorType
  , SequenceType
  , StructType
  , VariantType
  , ReferenceType
  , WordMapType

  , StringMapType
  , SymbolicArrayType

    -- * IsRecursiveType
  , IsRecursiveType(..)

    -- * Base type injection
  , BaseToType
  , baseToType

  , AsBaseType(..)
  , asBaseType

    -- * Other stuff
  , CtxRepr
  , pattern KnownBV

    -- * Representation of Crucible types
  , TypeRepr(..)

    -- * Re-exports
  , module Data.Parameterized.Ctx
  , module Data.Parameterized.NatRepr
  , module Data.Parameterized.SymbolRepr
  , module What4.BaseTypes
  , module What4.InterpretedFloatingPoint
  ) where

import           Data.Hashable
import           Data.Type.Equality
import           GHC.TypeNats (Nat, KnownNat)
import           Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Ctx
import           Data.Parameterized.NatRepr
import           Data.Parameterized.SymbolRepr
import qualified Data.Parameterized.TH.GADT as U
import           Prettyprinter

import           What4.BaseTypes
import           What4.InterpretedFloatingPoint

------------------------------------------------------------------------
-- Crucible types


-- | This typeclass is used to register recursive Crucible types
--   with the compiler.  This class defines, for a given symbol,
--   both the type-level and the representative-level unrolling
--   of a named recursive type.
--
--   The symbol constitutes a unique compile-time identifier for the
--   recursive type, allowing recursive types to be unrolled at run
--   time without requiring dynamic checks.
--
--   Parameter @nm@ has kind 'Symbol'.
class IsRecursiveType (nm::Symbol) where
  type UnrollType nm (ctx :: Ctx CrucibleType) :: CrucibleType
  unrollType :: SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)

type CtxRepr = Ctx.Assignment TypeRepr

-- | This data kind describes the types of values and expressions that
--   can occur in Crucible CFGs.
data CrucibleType where
   -- | An injection of solver interface types into Crucible types
   BaseToType :: BaseType -> CrucibleType

   -- | A dynamic type that can contain values of any type.
   AnyType :: CrucibleType

   -- | A type containing a single value "Unit"
   UnitType :: CrucibleType

   -- | A type for natural numbers.
   NatType :: CrucibleType

   -- | A type index for floating point numbers, whose interpretation
   --   depends on the symbolic backend.
   FloatType :: FloatInfo -> CrucibleType
   -- | A single character, as a 16-bit wide char.
   CharType :: CrucibleType
   -- | A function handle taking a context of formal arguments and a return type
   FunctionHandleType :: Ctx CrucibleType -> CrucibleType -> CrucibleType

   -- The Maybe type lifted into crucible expressions
   MaybeType :: CrucibleType -> CrucibleType

   -- A finite (one-dimensional) sequence of values.  Vectors are
   -- optimized for random-access indexing and updating.  Vectors
   -- of different lengths may not be combined at join points.
   VectorType :: CrucibleType -> CrucibleType

   -- Sequences of values, represented as linked lists of cons cells.  Sequences
   -- only allow access to the front. Unlike Vectors, sequences of
   -- different lengths may be combined at join points.
   SequenceType :: CrucibleType -> CrucibleType

   -- A structure is an aggregate type consisting of a sequence of values.
   -- The type of each value is known statically.
   StructType :: Ctx CrucibleType -> CrucibleType

   -- The type of mutable reference cells.
   ReferenceType :: CrucibleType -> CrucibleType

   -- A variant is a disjoint union of the types listed in the context.
   VariantType :: Ctx CrucibleType -> CrucibleType

   -- A finite map from bitvector values to the given crucible type.
   -- The nat index gives the width of the bitvector values used to index
   -- the map.
   WordMapType :: Nat -> BaseType -> CrucibleType

   -- Named recursive types, named by the given symbol.  To use recursive types
   -- you must provide an instance of the IsRecursiveType class that gives
   -- the unfolding of this recursive type.  The RollRecursive and UnrollRecursive
   -- operations witness the isomorphism between a recursive type and its one-step
   -- unrolling.  Similar to Haskell's newtype, recursive types do not necessarily
   -- have to mention the recursive type being defined; in which case, the type
   -- is simply a new named type which is isomorphic to its definition.
   RecursiveType :: Symbol -> Ctx CrucibleType -> CrucibleType

   -- Named intrinsic types.  Intrinsic types are a way to extend the
   -- crucible type system after-the-fact and add new type
   -- implementations.  Core crucible provides no operations on
   -- intrinsic types; they must be provided as built-in override
   -- functions, or via the language extension mechanism.  See the
   -- `IntrinsicClass` typeclass and the `Intrinsic` type family
   -- defined in "Lang.Crucible.Simulator.Intrinsics".
   --
   -- The context of crucible types are type arguments to the intrinsic type.
   IntrinsicType :: Symbol -> Ctx CrucibleType -> CrucibleType

   -- A partial map from strings to values.
   StringMapType :: CrucibleType -> CrucibleType

type BaseToType      = 'BaseToType                -- ^ @:: 'BaseType' -> 'CrucibleType'@.
type BoolType        = BaseToType BaseBoolType    -- ^ @:: 'CrucibleType'@.
type BVType w        = BaseToType (BaseBVType w)  -- ^ @:: 'Nat' -> 'CrucibleType'@.
type ComplexRealType = BaseToType BaseComplexType -- ^ @:: 'CrucibleType'@.
type IntegerType     = BaseToType BaseIntegerType -- ^ @:: 'CrucibleType'@.
type StringType si   = BaseToType (BaseStringType si) -- ^ @:: 'StringInfo' -> 'CrucibleType'@.
type RealValType     = BaseToType BaseRealType    -- ^ @:: 'CrucibleType'@.
type IEEEFloatType p = BaseToType (BaseFloatType p) -- ^ @:: FloatPrecision -> CrucibleType@

type SymbolicArrayType idx xs = BaseToType (BaseArrayType idx xs) -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'BaseType' -> 'CrucibleType'@.
type SymbolicStructType flds = BaseToType (BaseStructType flds) -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'CrucibleType'@.


-- | A dynamic type that can contain values of any type.
type AnyType  = 'AnyType  -- ^ @:: 'CrucibleType'@.

-- | A single character, as a 16-bit wide char.
type CharType = 'CharType -- ^ @:: 'CrucibleType'@.

-- | A type index for floating point numbers, whose interpretation
--   depends on the symbolic backend.
type FloatType    = 'FloatType    -- ^ @:: 'FloatInfo' -> 'CrucibleType'@.


-- | A function handle taking a context of formal arguments and a return type.
type FunctionHandleType = 'FunctionHandleType -- ^ @:: 'Ctx' 'CrucibleType' -> 'CrucibleType' -> 'CrucibleType'@.

-- | Named recursive types, named by the given symbol. To use
-- recursive types you must provide an instance of the
-- 'IsRecursiveType' class that gives the unfolding of this recursive
-- type. The 'Lang.Crucible.CFG.Expr.RollRecursive' and
-- 'Lang.Crucible.CFG.Expr.UnrollRecursive' operations witness the
-- isomorphism between a recursive type and its one-step unrolling.
-- Similar to Haskell's @newtype@, recursive types do not necessarily
-- have to mention the recursive type being defined; in which case,
-- the type is simply a new named type which is isomorphic to its
-- definition.
type RecursiveType = 'RecursiveType -- ^ @:: 'Symbol' -> 'Ctx' 'CrucibleType' -> 'CrucibleType'@.

-- | Named intrinsic types. Intrinsic types are a way to extend the
-- Crucible type system after-the-fact and add new type
-- implementations. Core Crucible provides no operations on intrinsic
-- types; they must be provided as built-in override functions. See
-- the 'Lang.Crucible.Simulator.Intrinsics.IntrinsicClass' typeclass
-- and the 'Lang.Crucible.Simulator.Intrinsics.Intrinsic' type family
-- defined in "Lang.Crucible.Simulator.Intrinsics".
type IntrinsicType ctx = 'IntrinsicType ctx -- ^ @:: 'Symbol' -> 'Ctx' 'CrucibleType' -> 'CrucibleType'@.

-- | The type of mutable reference cells.
type ReferenceType = 'ReferenceType -- ^ @:: 'CrucibleType' -> 'CrucibleType'@.

-- | The 'Maybe' type lifted into Crucible expressions.
type MaybeType = 'MaybeType -- ^ @:: 'CrucibleType' -> 'CrucibleType'@.

-- | A partial map from strings to values.
type StringMapType = 'StringMapType -- ^ @:: 'CrucibleType' -> 'CrucibleType'@.

-- | A structure is an aggregate type consisting of a sequence of
-- values. The type of each value is known statically.
type StructType = 'StructType -- ^ @:: 'Ctx' 'CrucibleType' -> 'CrucibleType'@.

-- | A type containing a single value "Unit".
type UnitType      = 'UnitType      -- ^ @:: 'CrucibleType'@.

-- | A type for natural numbers.
type NatType       = 'NatType       -- ^ @:: 'CrucibleType'@.

-- | A variant is a disjoint union of the types listed in the context.
type VariantType   = 'VariantType   -- ^ @:: 'Ctx' 'CrucibleType' -> 'CrucibleType'@.

-- | A finite (one-dimensional) sequence of values.  Vectors are
-- optimized for random-access indexing and updating.  Vectors
-- of different lengths may not be combined at join points.
type VectorType    = 'VectorType    -- ^ @:: 'CrucibleType' -> 'CrucibleType'@.

-- | Sequences of values, represented as linked lists of cons cells.  Sequences
-- only allow access to the front. Unlike Vectors, sequences of
-- different lengths may be combined at join points.
type SequenceType  = 'SequenceType  -- ^ @:: 'CrucibleType' -> 'CrucibleType'@.

-- | A finite map from bitvector values to the given Crucible type.
-- The 'Nat' index gives the width of the bitvector values used to
-- index the map.
type WordMapType   = 'WordMapType   -- ^ @:: 'Nat' -> 'BaseType' -> 'CrucibleType'@.

----------------------------------------------------------------
-- Base Type Injection

baseToType :: BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType :: forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType BaseTypeRepr bt
bt =
  case BaseTypeRepr bt
bt of
    BaseTypeRepr bt
BaseBoolRepr -> TypeRepr (BaseToType bt)
TypeRepr BoolType
BoolRepr
    BaseTypeRepr bt
BaseIntegerRepr -> TypeRepr (BaseToType bt)
TypeRepr IntegerType
IntegerRepr
    BaseTypeRepr bt
BaseRealRepr -> TypeRepr (BaseToType bt)
TypeRepr RealValType
RealValRepr
    BaseStringRepr StringInfoRepr si
si -> StringInfoRepr si -> TypeRepr (StringType si)
forall (tp :: StringInfo).
StringInfoRepr tp -> TypeRepr (StringType tp)
StringRepr StringInfoRepr si
si
    BaseBVRepr NatRepr w
w -> NatRepr w -> TypeRepr (BVType w)
forall (tp :: Natural).
(1 <= tp) =>
NatRepr tp -> TypeRepr (BVType tp)
BVRepr NatRepr w
w
    BaseTypeRepr bt
BaseComplexRepr -> TypeRepr (BaseToType bt)
TypeRepr ComplexRealType
ComplexRealRepr
    BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx BaseTypeRepr xs
xs -> Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> TypeRepr (SymbolicArrayType (idx ::> tp) xs)
forall (tp :: Ctx BaseType) (ret :: BaseType) (t :: BaseType).
Assignment BaseTypeRepr (tp ::> ret)
-> BaseTypeRepr t -> TypeRepr (SymbolicArrayType (tp ::> ret) t)
SymbolicArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx BaseTypeRepr xs
xs
    BaseStructRepr Assignment BaseTypeRepr ctx
flds -> Assignment BaseTypeRepr ctx -> TypeRepr (SymbolicStructType ctx)
forall (tp :: Ctx BaseType).
Assignment BaseTypeRepr tp -> TypeRepr (SymbolicStructType tp)
SymbolicStructRepr Assignment BaseTypeRepr ctx
flds
    BaseFloatRepr FloatPrecisionRepr fpp
ps -> FloatPrecisionRepr fpp -> TypeRepr (IEEEFloatType fpp)
forall (tp :: FloatPrecision).
FloatPrecisionRepr tp -> TypeRepr (IEEEFloatType tp)
IEEEFloatRepr FloatPrecisionRepr fpp
ps

data AsBaseType tp where
  AsBaseType  :: tp ~ BaseToType bt => BaseTypeRepr bt -> AsBaseType tp
  NotBaseType :: AsBaseType tp

asBaseType :: TypeRepr tp -> AsBaseType tp
asBaseType :: forall (tp :: CrucibleType). TypeRepr tp -> AsBaseType tp
asBaseType TypeRepr tp
tp =
  case TypeRepr tp
tp of
    TypeRepr tp
BoolRepr -> BaseTypeRepr 'BaseBoolType -> AsBaseType tp
forall (tp :: CrucibleType) (tp :: BaseType).
(tp ~ BaseToType tp) =>
BaseTypeRepr tp -> AsBaseType tp
AsBaseType BaseTypeRepr 'BaseBoolType
BaseBoolRepr
    TypeRepr tp
IntegerRepr -> BaseTypeRepr 'BaseIntegerType -> AsBaseType tp
forall (tp :: CrucibleType) (tp :: BaseType).
(tp ~ BaseToType tp) =>
BaseTypeRepr tp -> AsBaseType tp
AsBaseType BaseTypeRepr 'BaseIntegerType
BaseIntegerRepr
    TypeRepr tp
RealValRepr -> BaseTypeRepr 'BaseRealType -> AsBaseType tp
forall (tp :: CrucibleType) (tp :: BaseType).
(tp ~ BaseToType tp) =>
BaseTypeRepr tp -> AsBaseType tp
AsBaseType BaseTypeRepr 'BaseRealType
BaseRealRepr
    StringRepr StringInfoRepr si
si -> BaseTypeRepr (BaseStringType si) -> AsBaseType tp
forall (tp :: CrucibleType) (tp :: BaseType).
(tp ~ BaseToType tp) =>
BaseTypeRepr tp -> AsBaseType tp
AsBaseType (StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
BaseStringRepr StringInfoRepr si
si)
    BVRepr NatRepr n
w -> BaseTypeRepr (BaseBVType n) -> AsBaseType tp
forall (tp :: CrucibleType) (tp :: BaseType).
(tp ~ BaseToType tp) =>
BaseTypeRepr tp -> AsBaseType tp
AsBaseType (NatRepr n -> BaseTypeRepr (BaseBVType n)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr n
w)
    TypeRepr tp
ComplexRealRepr -> BaseTypeRepr 'BaseComplexType -> AsBaseType tp
forall (tp :: CrucibleType) (tp :: BaseType).
(tp ~ BaseToType tp) =>
BaseTypeRepr tp -> AsBaseType tp
AsBaseType BaseTypeRepr 'BaseComplexType
BaseComplexRepr
    SymbolicArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx BaseTypeRepr t
xs ->
      BaseTypeRepr (BaseArrayType (idx ::> tp) t) -> AsBaseType tp
forall (tp :: CrucibleType) (tp :: BaseType).
(tp ~ BaseToType tp) =>
BaseTypeRepr tp -> AsBaseType tp
AsBaseType (Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr t -> BaseTypeRepr (BaseArrayType (idx ::> tp) t)
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx BaseTypeRepr t
xs)
    IEEEFloatRepr FloatPrecisionRepr ps
ps ->
      BaseTypeRepr (BaseFloatType ps) -> AsBaseType tp
forall (tp :: CrucibleType) (tp :: BaseType).
(tp ~ BaseToType tp) =>
BaseTypeRepr tp -> AsBaseType tp
AsBaseType (FloatPrecisionRepr ps -> BaseTypeRepr (BaseFloatType ps)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr ps
ps)
    SymbolicStructRepr Assignment BaseTypeRepr ctx
flds -> BaseTypeRepr (BaseStructType ctx) -> AsBaseType tp
forall (tp :: CrucibleType) (tp :: BaseType).
(tp ~ BaseToType tp) =>
BaseTypeRepr tp -> AsBaseType tp
AsBaseType (Assignment BaseTypeRepr ctx -> BaseTypeRepr (BaseStructType ctx)
forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr ('BaseStructType ctx)
BaseStructRepr Assignment BaseTypeRepr ctx
flds)
    TypeRepr tp
_ -> AsBaseType tp
forall (tp :: CrucibleType). AsBaseType tp
NotBaseType

----------------------------------------------------------------
-- Type representatives

-- | A family of representatives for Crucible types. Parameter @tp@
-- has kind 'CrucibleType'.
data TypeRepr (tp::CrucibleType) where
   AnyRepr :: TypeRepr AnyType
   UnitRepr :: TypeRepr UnitType
   BoolRepr :: TypeRepr BoolType
   NatRepr  :: TypeRepr NatType
   IntegerRepr :: TypeRepr IntegerType
   RealValRepr :: TypeRepr RealValType
   ComplexRealRepr :: TypeRepr ComplexRealType
   BVRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
   IntrinsicRepr :: !(SymbolRepr nm)
                 -> !(CtxRepr ctx)
                 -> TypeRepr (IntrinsicType nm ctx)
   RecursiveRepr :: IsRecursiveType nm
                 => SymbolRepr nm
                 -> CtxRepr ctx
                 -> TypeRepr (RecursiveType nm ctx)

   -- | This is a representation of floats that works at known fixed
   -- mantissa and exponent widths, but the symbolic backend may pick
   -- the representation.
   FloatRepr :: !(FloatInfoRepr flt) -> TypeRepr (FloatType flt)

   -- | This is a float with user-definable mantissa and exponent that
   -- maps directly to the what4 base type.
   IEEEFloatRepr :: !(FloatPrecisionRepr ps) -> TypeRepr (IEEEFloatType ps)

   CharRepr :: TypeRepr CharType
   StringRepr :: StringInfoRepr si -> TypeRepr (StringType si)
   FunctionHandleRepr :: !(CtxRepr ctx)
                      -> !(TypeRepr ret)
                      -> TypeRepr (FunctionHandleType ctx ret)

   MaybeRepr   :: !(TypeRepr tp) -> TypeRepr (MaybeType tp)
   SequenceRepr:: !(TypeRepr tp) -> TypeRepr (SequenceType tp)
   VectorRepr  :: !(TypeRepr tp) -> TypeRepr (VectorType tp)
   StructRepr  :: !(CtxRepr ctx) -> TypeRepr (StructType ctx)
   VariantRepr :: !(CtxRepr ctx) -> TypeRepr (VariantType ctx)
   ReferenceRepr :: !(TypeRepr a) -> TypeRepr (ReferenceType a)

   WordMapRepr :: (1 <= n)
               => !(NatRepr n)
               -> !(BaseTypeRepr tp)
               -> TypeRepr (WordMapType n tp)

   StringMapRepr :: !(TypeRepr tp) -> TypeRepr (StringMapType tp)

   SymbolicArrayRepr :: !(Ctx.Assignment BaseTypeRepr (idx::>tp))
                     -> !(BaseTypeRepr t)
                     -> TypeRepr (SymbolicArrayType (idx::>tp) t)

   -- A reference to a symbolic struct.
   SymbolicStructRepr :: Ctx.Assignment BaseTypeRepr ctx
                      -> TypeRepr (SymbolicStructType ctx)

------------------------------------------------------------------------------
-- Representable class instances

instance KnownRepr TypeRepr AnyType             where knownRepr :: TypeRepr AnyType
knownRepr = TypeRepr AnyType
AnyRepr
instance KnownRepr TypeRepr UnitType            where knownRepr :: TypeRepr UnitType
knownRepr = TypeRepr UnitType
UnitRepr
instance KnownRepr TypeRepr CharType            where knownRepr :: TypeRepr CharType
knownRepr = TypeRepr CharType
CharRepr
instance KnownRepr TypeRepr NatType             where knownRepr :: TypeRepr NatType
knownRepr = TypeRepr NatType
NatRepr

instance KnownRepr BaseTypeRepr bt => KnownRepr TypeRepr (BaseToType bt) where
  knownRepr :: TypeRepr (BaseToType bt)
knownRepr = BaseTypeRepr bt -> TypeRepr (BaseToType bt)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType BaseTypeRepr bt
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownCtx TypeRepr ctx => KnownRepr TypeRepr (StructType ctx) where
  knownRepr :: TypeRepr (StructType ctx)
knownRepr = CtxRepr ctx -> TypeRepr (StructType ctx)
forall (tp :: Ctx CrucibleType).
CtxRepr tp -> TypeRepr (StructType tp)
StructRepr CtxRepr ctx
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownCtx TypeRepr ctx => KnownRepr TypeRepr (VariantType ctx) where
  knownRepr :: TypeRepr (VariantType ctx)
knownRepr = CtxRepr ctx -> TypeRepr (VariantType ctx)
forall (tp :: Ctx CrucibleType).
CtxRepr tp -> TypeRepr (VariantType tp)
VariantRepr CtxRepr ctx
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownRepr TypeRepr a => KnownRepr TypeRepr (ReferenceType a) where
  knownRepr :: TypeRepr (ReferenceType a)
knownRepr = TypeRepr a -> TypeRepr (ReferenceType a)
forall (tp :: CrucibleType).
TypeRepr tp -> TypeRepr (ReferenceType tp)
ReferenceRepr TypeRepr a
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance (KnownSymbol s, KnownCtx TypeRepr ctx) => KnownRepr TypeRepr (IntrinsicType s ctx) where
  knownRepr :: TypeRepr (IntrinsicType s ctx)
knownRepr = SymbolRepr s -> CtxRepr ctx -> TypeRepr (IntrinsicType s ctx)
forall (tp :: Symbol) (ret :: Ctx CrucibleType).
SymbolRepr tp -> CtxRepr ret -> TypeRepr (IntrinsicType tp ret)
IntrinsicRepr SymbolRepr s
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol CtxRepr ctx
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance (KnownSymbol s, KnownCtx TypeRepr ctx, IsRecursiveType s) => KnownRepr TypeRepr (RecursiveType s ctx) where
  knownRepr :: TypeRepr (RecursiveType s ctx)
knownRepr = SymbolRepr s -> CtxRepr ctx -> TypeRepr (RecursiveType s ctx)
forall (tp :: Symbol) (ret :: Ctx CrucibleType).
IsRecursiveType tp =>
SymbolRepr tp -> CtxRepr ret -> TypeRepr (RecursiveType tp ret)
RecursiveRepr SymbolRepr s
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol CtxRepr ctx
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance (1 <= w, KnownNat w, KnownRepr BaseTypeRepr tp)
      => KnownRepr TypeRepr (WordMapType w tp) where
  knownRepr :: TypeRepr (WordMapType w tp)
knownRepr = NatRepr w -> BaseTypeRepr tp -> TypeRepr (WordMapType w tp)
forall (tp :: Natural) (ret :: BaseType).
(1 <= tp) =>
NatRepr tp -> BaseTypeRepr ret -> TypeRepr (WordMapType tp ret)
WordMapRepr (NatRepr w
forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr w) (BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr :: BaseTypeRepr tp)

instance (KnownCtx TypeRepr ctx, KnownRepr TypeRepr ret)
      => KnownRepr TypeRepr (FunctionHandleType ctx ret) where
  knownRepr :: TypeRepr (FunctionHandleType ctx ret)
knownRepr = CtxRepr ctx
-> TypeRepr ret -> TypeRepr (FunctionHandleType ctx ret)
forall (tp :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr tp -> TypeRepr ret -> TypeRepr (FunctionHandleType tp ret)
FunctionHandleRepr CtxRepr ctx
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr TypeRepr ret
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownRepr FloatInfoRepr flt => KnownRepr TypeRepr (FloatType flt) where
  knownRepr :: TypeRepr (FloatType flt)
knownRepr = FloatInfoRepr flt -> TypeRepr (FloatType flt)
forall (tp :: FloatInfo).
FloatInfoRepr tp -> TypeRepr (FloatType tp)
FloatRepr FloatInfoRepr flt
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownRepr FloatPrecisionRepr ps => KnownRepr TypeRepr (IEEEFloatType ps) where
  knownRepr :: TypeRepr (IEEEFloatType ps)
knownRepr = FloatPrecisionRepr ps -> TypeRepr (IEEEFloatType ps)
forall (tp :: FloatPrecision).
FloatPrecisionRepr tp -> TypeRepr (IEEEFloatType tp)
IEEEFloatRepr FloatPrecisionRepr ps
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (VectorType tp) where
  knownRepr :: TypeRepr (VectorType tp)
knownRepr = TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp :: CrucibleType).
TypeRepr tp -> TypeRepr (VectorType tp)
VectorRepr TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (SequenceType tp) where
  knownRepr :: TypeRepr (SequenceType tp)
knownRepr = TypeRepr tp -> TypeRepr (SequenceType tp)
forall (tp :: CrucibleType).
TypeRepr tp -> TypeRepr (SequenceType tp)
SequenceRepr TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (MaybeType tp) where
  knownRepr :: TypeRepr (MaybeType tp)
knownRepr = TypeRepr tp -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). TypeRepr tp -> TypeRepr (MaybeType tp)
MaybeRepr TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (StringMapType tp) where
  knownRepr :: TypeRepr (StringMapType tp)
knownRepr = TypeRepr tp -> TypeRepr (StringMapType tp)
forall (tp :: CrucibleType).
TypeRepr tp -> TypeRepr (StringMapType tp)
StringMapRepr TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

-- | Pattern synonym specifying bitvector TypeReprs.  Intended to be use
--   with type applications, e.g., @KnownBV \@32@.
pattern KnownBV :: forall n. (1 <= n, KnownNat n) => TypeRepr (BVType n)
pattern $mKnownBV :: forall {r} {n :: Natural}.
(1 <= n, KnownNat n) =>
TypeRepr (BVType n) -> ((# #) -> r) -> ((# #) -> r) -> r
$bKnownBV :: forall (n :: Natural). (1 <= n, KnownNat n) => TypeRepr (BVType n)
KnownBV <- BVRepr (testEquality (knownRepr :: NatRepr n) -> Just Refl)
  where KnownBV = TypeRepr (BVType n)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

------------------------------------------------------------------------
-- Misc typeclass instances

-- Force TypeRepr, etc. to be in context for next slice.
$(return [])

instance HashableF TypeRepr where
  hashWithSaltF :: forall (tp :: CrucibleType). Int -> TypeRepr tp -> Int
hashWithSaltF = Int -> TypeRepr tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt
instance Hashable (TypeRepr ty) where
  hashWithSalt :: Int -> TypeRepr ty -> Int
hashWithSalt = $(U.structuralHashWithSalt [t|TypeRepr|] [])

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

instance Show (TypeRepr tp) where
  showsPrec :: Int -> TypeRepr tp -> ShowS
showsPrec = $(U.structuralShowsPrec [t|TypeRepr|])
instance ShowF TypeRepr


instance TestEquality TypeRepr where
  testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality = $(U.structuralTypeEquality [t|TypeRepr|]
                   [ (U.TypeApp (U.ConType [t|NatRepr|]) U.AnyType, [|testEquality|])
                   , (U.TypeApp (U.ConType [t|SymbolRepr|]) U.AnyType, [|testEquality|])
                   , (U.TypeApp (U.ConType [t|FloatInfoRepr|]) U.AnyType, [|testEquality|])
                   , (U.TypeApp (U.ConType [t|FloatPrecisionRepr|]) U.AnyType, [|testEquality|])
                   , (U.TypeApp (U.ConType [t|CtxRepr|]) U.AnyType, [|testEquality|])
                   , (U.TypeApp (U.ConType [t|BaseTypeRepr|]) U.AnyType, [|testEquality|])
                   , (U.TypeApp (U.ConType [t|StringInfoRepr|])  U.AnyType, [|testEquality|])
                   , (U.TypeApp (U.ConType [t|TypeRepr|]) U.AnyType, [|testEquality|])
                   , (U.TypeApp (U.TypeApp (U.ConType [t|Ctx.Assignment|]) U.AnyType) U.AnyType
                     , [|testEquality|])
                   ]
                  )
instance Eq (TypeRepr tp) where
  TypeRepr tp
x == :: TypeRepr tp -> TypeRepr tp -> Bool
== TypeRepr tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (TypeRepr tp -> TypeRepr tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr tp
x TypeRepr tp
y)

instance OrdF TypeRepr where
  compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
TypeRepr x -> TypeRepr y -> OrderingF x y
compareF = $(U.structuralTypeOrd [t|TypeRepr|]
                   [ (U.TypeApp (U.ConType [t|NatRepr|]) U.AnyType, [|compareF|])
                   , (U.TypeApp (U.ConType [t|SymbolRepr|]) U.AnyType, [|compareF|])
                   , (U.TypeApp (U.ConType [t|FloatInfoRepr|]) U.AnyType, [|compareF|])
                   , (U.TypeApp (U.ConType [t|FloatPrecisionRepr|]) U.AnyType, [|compareF|])
                   , (U.TypeApp (U.ConType [t|BaseTypeRepr|])  U.AnyType, [|compareF|])
                   , (U.TypeApp (U.ConType [t|StringInfoRepr|])  U.AnyType, [|compareF|])
                   , (U.TypeApp (U.ConType [t|TypeRepr|])      U.AnyType, [|compareF|])
                   , (U.TypeApp (U.ConType [t|CtxRepr|])      U.AnyType, [|compareF|])
                   , (U.TypeApp (U.TypeApp (U.ConType [t|Ctx.Assignment|]) U.AnyType) U.AnyType
                     , [|compareF|])
                   ]
                  )