-----------------------------------------------------------------------
-- |
-- 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 OverloadedStrings #-}
{-# 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
  , ppTypeRepr
  , ppIntrinsicDefault

    -- * 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.Functor.Identity (Identity(..))
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           Data.Parameterized.TraversableFC
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|] [])

-- Helper, not exported
prettyCtx ::
  Monad f =>
  -- | How to print 'IntrinsicRepr', see 'ppIntrinsicDefault'
  (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (Doc ann)) ->
  Ctx.Assignment TypeRepr ctx ->
  f (Doc ann)
-- The following specialization is used in the 'Pretty' instance and doesn't
-- need to generate code for (>>=), so it seems worth specializing for it.
{-# SPECIALIZE
  prettyCtx :: 
    (forall s ctx. SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)) ->
    Ctx.Assignment TypeRepr tp ->
    Identity (Doc ann) #-}
prettyCtx :: forall (f :: Type -> Type) ann (ctx :: Ctx CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx' -> f (Doc ann))
-> Assignment TypeRepr ctx -> f (Doc ann)
prettyCtx forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx' -> f (Doc ann)
f = ([Doc ann] -> Doc ann) -> f [Doc ann] -> f (Doc ann)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (f [Doc ann] -> f (Doc ann))
-> (Assignment TypeRepr ctx -> f [Doc ann])
-> Assignment TypeRepr ctx
-> f (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: CrucibleType).
 [Doc ann] -> TypeRepr x -> f [Doc ann])
-> [Doc ann] -> Assignment TypeRepr ctx -> f [Doc ann]
forall {k} {l} (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
       b (f :: k -> Type) (c :: l).
(FoldableFC t, Monad m) =>
(forall (x :: k). b -> f x -> m b) -> b -> t f c -> m b
foldlMFC (\[Doc ann]
l TypeRepr x
t -> (Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
:[Doc ann]
l) (Doc ann -> [Doc ann]) -> f (Doc ann) -> f [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx' -> f (Doc ann))
-> TypeRepr x -> f (Doc ann)
forall (f :: Type -> Type) ann (tp :: CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
ppTypeRepr SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx' -> f (Doc ann)
f TypeRepr x
t) []

-- Helper, not exported
prettyBaseCtx :: Ctx.Assignment BaseTypeRepr ctx -> Doc ann
prettyBaseCtx :: forall (ctx :: Ctx BaseType) ann.
Assignment BaseTypeRepr ctx -> Doc ann
prettyBaseCtx = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann)
-> (Assignment BaseTypeRepr ctx -> [Doc ann])
-> Assignment BaseTypeRepr ctx
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: BaseType). BaseTypeRepr x -> Doc ann)
-> forall (x :: Ctx BaseType).
   Assignment BaseTypeRepr x -> [Doc ann]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: BaseType -> Type) a.
(forall (x :: BaseType). f x -> a)
-> forall (x :: Ctx BaseType). Assignment f x -> [a]
toListFC BaseTypeRepr x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BaseTypeRepr x -> Doc ann
forall (x :: BaseType). BaseTypeRepr x -> Doc ann
pretty

-- | Pretty-print a type.
--
-- Attempts to be consistent with the syntax provided in the @crucible-syntax@
-- package.
--
-- This is monadic mostly to allow failure, e.g., in case the caller finds an
-- intrinsic type that it doesn\'t expect.
ppTypeRepr ::
  Monad f =>
  -- | How to print 'IntrinsicRepr', see 'ppIntrinsicDefault'
  (forall s ctx. SymbolRepr s -> CtxRepr ctx -> f (Doc ann)) ->
  TypeRepr tp ->
  f (Doc ann)
-- The following specialization is used in the 'Pretty' instance and doesn't
-- need to generate code for (>>=), so it seems worth specializing for it.
{-# SPECIALIZE
  ppTypeRepr :: 
    (forall s ctx. SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)) ->
    TypeRepr tp ->
    Identity (Doc ann) #-}
ppTypeRepr :: forall (f :: Type -> Type) ann (tp :: CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
ppTypeRepr forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f TypeRepr tp
x =
  case TypeRepr tp
x of
    TypeRepr tp
AnyRepr -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
"Any"
    TypeRepr tp
UnitRepr -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
"Unit"
    TypeRepr tp
BoolRepr -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
"Bool"
    TypeRepr tp
NatRepr -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
"Nat"
    TypeRepr tp
IntegerRepr -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
"Integer"
    TypeRepr tp
RealValRepr -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
"RealVal"
    TypeRepr tp
ComplexRealRepr -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
"ComplexReal"
    BVRepr NatRepr n
n -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"Bitvector" 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
n))
    IntrinsicRepr SymbolRepr nm
name CtxRepr ctx
tys -> SymbolRepr nm -> CtxRepr ctx -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f SymbolRepr nm
name CtxRepr ctx
tys
    RecursiveRepr SymbolRepr nm
name CtxRepr ctx
tys ->
      Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Doc ann
"Rec" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (SymbolRepr nm -> Text
forall (nm :: Symbol). SymbolRepr nm -> Text
symbolRepr SymbolRepr nm
name)) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) (Doc ann -> Doc ann) -> f (Doc ann) -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> CtxRepr ctx -> f (Doc ann)
forall (f :: Type -> Type) ann (ctx :: Ctx CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx' -> f (Doc ann))
-> Assignment TypeRepr ctx -> f (Doc ann)
prettyCtx SymbolRepr s -> CtxRepr ctx' -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f CtxRepr ctx
tys
    FloatRepr FloatInfoRepr flt
fr -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"Float" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FloatInfoRepr flt -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FloatInfoRepr flt -> Doc ann
pretty FloatInfoRepr flt
fr))
    IEEEFloatRepr FloatPrecisionRepr ps
fr -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"IEEEFloat" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FloatPrecisionRepr ps -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FloatPrecisionRepr ps -> Doc ann
pretty FloatPrecisionRepr ps
fr))
    TypeRepr tp
CharRepr -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
"Char"
    StringRepr StringInfoRepr si
s -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"String" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> StringInfoRepr si -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StringInfoRepr si -> Doc ann
pretty StringInfoRepr si
s))
    FunctionHandleRepr CtxRepr ctx
args TypeRepr ret
ret ->
      (\Doc ann
args' Doc ann
ret' -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"->" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
args' Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
ret'))
      (Doc ann -> Doc ann -> Doc ann)
-> f (Doc ann) -> f (Doc ann -> Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> CtxRepr ctx -> f (Doc ann)
forall (f :: Type -> Type) ann (ctx :: Ctx CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx' -> f (Doc ann))
-> Assignment TypeRepr ctx -> f (Doc ann)
prettyCtx SymbolRepr s -> CtxRepr ctx' -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f CtxRepr ctx
args
      f (Doc ann -> Doc ann) -> f (Doc ann) -> f (Doc ann)
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr ret -> f (Doc ann)
forall (f :: Type -> Type) ann (tp :: CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
ppTypeRepr SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f TypeRepr ret
ret
    MaybeRepr TypeRepr tp
tp -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc ann
"Maybe" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) (Doc ann -> Doc ann) -> f (Doc ann) -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
forall (f :: Type -> Type) ann (tp :: CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
ppTypeRepr SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f TypeRepr tp
tp
    SequenceRepr TypeRepr tp
s -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc ann
"Sequence" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) (Doc ann -> Doc ann) -> f (Doc ann) -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
forall (f :: Type -> Type) ann (tp :: CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
ppTypeRepr SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f TypeRepr tp
s
    VariantRepr CtxRepr ctx
variants -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc ann
"Variant" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) (Doc ann -> Doc ann) -> f (Doc ann) -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> CtxRepr ctx -> f (Doc ann)
forall (f :: Type -> Type) ann (ctx :: Ctx CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx' -> f (Doc ann))
-> Assignment TypeRepr ctx -> f (Doc ann)
prettyCtx SymbolRepr s -> CtxRepr ctx' -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f CtxRepr ctx
variants
    VectorRepr TypeRepr tp
elems -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc ann
"Vector" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) (Doc ann -> Doc ann) -> f (Doc ann) -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
forall (f :: Type -> Type) ann (tp :: CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
ppTypeRepr SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f TypeRepr tp
elems
    StructRepr CtxRepr ctx
fields -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc ann
"Struct" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) (Doc ann -> Doc ann) -> f (Doc ann) -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> CtxRepr ctx -> f (Doc ann)
forall (f :: Type -> Type) ann (ctx :: Ctx CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx' -> f (Doc ann))
-> Assignment TypeRepr ctx -> f (Doc ann)
prettyCtx SymbolRepr s -> CtxRepr ctx' -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f CtxRepr ctx
fields
    ReferenceRepr TypeRepr a
t -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc ann
"Reference" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) (Doc ann -> Doc ann) -> f (Doc ann) -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr a -> f (Doc ann)
forall (f :: Type -> Type) ann (tp :: CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
ppTypeRepr SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f TypeRepr a
t
    WordMapRepr NatRepr n
n BaseTypeRepr tp
t -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"WorldMap" 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
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> BaseTypeRepr tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BaseTypeRepr tp -> Doc ann
pretty BaseTypeRepr tp
t))
    StringMapRepr TypeRepr tp
s -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc ann
"StringMap" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) (Doc ann -> Doc ann) -> f (Doc ann) -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
forall (f :: Type -> Type) ann (tp :: CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
ppTypeRepr SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
forall (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> f (Doc ann)
f TypeRepr tp
s
    SymbolicArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idxs BaseTypeRepr t
a ->
      Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"SymbolicArray" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Assignment BaseTypeRepr (idx ::> tp) -> Doc ann
forall (ctx :: Ctx BaseType) ann.
Assignment BaseTypeRepr ctx -> Doc ann
prettyBaseCtx Assignment BaseTypeRepr (idx ::> tp)
idxs Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> BaseTypeRepr t -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BaseTypeRepr t -> Doc ann
pretty BaseTypeRepr t
a))
    SymbolicStructRepr Assignment BaseTypeRepr ctx
fields ->
      Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"SymbolicStruct" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Assignment BaseTypeRepr ctx -> Doc ann
forall (ctx :: Ctx BaseType) ann.
Assignment BaseTypeRepr ctx -> Doc ann
prettyBaseCtx Assignment BaseTypeRepr ctx
fields))

-- | A default printer for 'IntrinsicRepr', suitable for use with 'ppTypeRepr'.
ppIntrinsicDefault :: SymbolRepr s -> CtxRepr ctx -> Doc ann
ppIntrinsicDefault :: forall (s :: Symbol) (ctx :: Ctx CrucibleType) ann.
SymbolRepr s -> CtxRepr ctx -> Doc ann
ppIntrinsicDefault SymbolRepr s
name CtxRepr ctx
tys = Identity (Doc ann) -> Doc ann
forall a. Identity a -> a
runIdentity (SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)
forall ann (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)
go SymbolRepr s
name CtxRepr ctx
tys)
  where
  go :: forall ann s ctx. SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)
  go :: forall ann (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)
go SymbolRepr s
name' CtxRepr ctx
tys' =
    Doc ann -> Identity (Doc ann)
forall a. a -> Identity a
Identity (Doc ann -> Identity (Doc ann)) -> Doc ann -> Identity (Doc ann)
forall a b. (a -> b) -> a -> b
$
      Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
        Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (SymbolRepr s -> Text
forall (nm :: Symbol). SymbolRepr nm -> Text
symbolRepr SymbolRepr s
name') Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Identity (Doc ann) -> Doc ann
forall a. Identity a -> a
runIdentity ((forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx' -> Identity (Doc ann))
-> CtxRepr ctx -> Identity (Doc ann)
forall (f :: Type -> Type) ann (ctx :: Ctx CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx' -> f (Doc ann))
-> Assignment TypeRepr ctx -> f (Doc ann)
prettyCtx SymbolRepr s -> CtxRepr ctx' -> Identity (Doc ann)
forall ann (s :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)
forall (s :: Symbol) (ctx' :: Ctx CrucibleType).
SymbolRepr s -> CtxRepr ctx' -> Identity (Doc ann)
go CtxRepr ctx
tys')

-- | Pretty-print a type. Based on 'ppTypeRepr', using 'ppIntrinsicDefault'.
instance Pretty (TypeRepr tp) where
  pretty :: forall ann. TypeRepr tp -> Doc ann
pretty =
    Identity (Doc ann) -> Doc ann
forall a. Identity a -> a
runIdentity (Identity (Doc ann) -> Doc ann)
-> (TypeRepr tp -> Identity (Doc ann)) -> TypeRepr tp -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann))
-> TypeRepr tp -> Identity (Doc ann)
forall (f :: Type -> Type) ann (tp :: CrucibleType).
Monad f =>
(forall (s :: Symbol) (ctx :: Ctx CrucibleType).
 SymbolRepr s -> CtxRepr ctx -> f (Doc ann))
-> TypeRepr tp -> f (Doc ann)
ppTypeRepr (\SymbolRepr s
name CtxRepr ctx
tys -> Doc ann -> Identity (Doc ann)
forall a. a -> Identity a
Identity (SymbolRepr s -> CtxRepr ctx -> Doc ann
forall (s :: Symbol) (ctx :: Ctx CrucibleType) ann.
SymbolRepr s -> CtxRepr ctx -> Doc ann
ppIntrinsicDefault SymbolRepr s
name CtxRepr ctx
tys))

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 EqF TypeRepr where
  eqF :: forall (tp :: CrucibleType). TypeRepr tp -> TypeRepr tp -> Bool
eqF TypeRepr a
x TypeRepr a
y = Maybe (a :~: a) -> Bool
forall a. Maybe a -> Bool
isJust (TypeRepr a -> TypeRepr a -> Maybe (a :~: a)
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 a
x TypeRepr a
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|])
                   ]
                  )