1-----------------------------------------------------------------------
2-- |
3-- Module           : What4.BaseTypes
4-- Description      : This module exports the types used in solver expressions.
5-- Copyright        : (c) Galois, Inc 2014-2020
6-- License          : BSD3
7-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
8-- Stability        : provisional
9--
10-- This module exports the types used in solver expressions.
11--
12-- These types are largely used as indexes to various GADTs and type
13-- families as a way to let the GHC typechecker help us keep expressions
14-- used by solvers apart.
15--
16-- In addition, we provide a value-level reification of the type
17-- indices that can be examined by pattern matching, called 'BaseTypeRepr'.
18------------------------------------------------------------------------
19{-# LANGUAGE ConstraintKinds#-}
20{-# LANGUAGE DataKinds #-}
21{-# LANGUAGE FlexibleContexts #-}
22{-# LANGUAGE FlexibleInstances #-}
23{-# LANGUAGE GADTs #-}
24{-# LANGUAGE MultiParamTypeClasses #-}
25{-# LANGUAGE PolyKinds #-}
26{-# LANGUAGE ScopedTypeVariables #-}
27{-# LANGUAGE StandaloneDeriving #-}
28{-# LANGUAGE TemplateHaskell #-}
29{-# LANGUAGE TypeApplications #-}
30{-# LANGUAGE TypeFamilies #-}
31{-# LANGUAGE TypeOperators #-}
32{-# LANGUAGE UndecidableInstances #-}
33module What4.BaseTypes
34  ( -- * BaseType data kind
35    type BaseType
36    -- ** Constructors for kind BaseType
37  , BaseBoolType
38  , BaseIntegerType
39  , BaseRealType
40  , BaseStringType
41  , BaseBVType
42  , BaseFloatType
43  , BaseComplexType
44  , BaseStructType
45  , BaseArrayType
46    -- * StringInfo data kind
47  , StringInfo
48    -- ** Constructors for StringInfo
49  , Char8
50  , Char16
51  , Unicode
52    -- * FloatPrecision data kind
53  , type FloatPrecision
54  , type FloatPrecisionBits
55    -- ** Constructors for kind FloatPrecision
56  , FloatingPointPrecision
57    -- ** FloatingPointPrecision aliases
58  , Prec16
59  , Prec32
60  , Prec64
61  , Prec80
62  , Prec128
63    -- * Representations of base types
64  , BaseTypeRepr(..)
65  , FloatPrecisionRepr(..)
66  , StringInfoRepr(..)
67  , arrayTypeIndices
68  , arrayTypeResult
69  , floatPrecisionToBVType
70  , lemmaFloatPrecisionIsPos
71  , module Data.Parameterized.NatRepr
72
73    -- * KnownRepr
74  , KnownRepr(..)  -- Re-export from 'Data.Parameterized.Classes'
75  , KnownCtx
76  ) where
77
78
79import           Data.Hashable
80import           Data.Kind
81import           Data.Parameterized.Classes
82import qualified Data.Parameterized.Context as Ctx
83import           Data.Parameterized.NatRepr
84import           Data.Parameterized.TH.GADT
85import           GHC.TypeNats as TypeNats
86import           Prettyprinter
87
88--------------------------------------------------------------------------------
89-- KnownCtx
90
91-- | A Context where all the argument types are 'KnownRepr' instances
92type KnownCtx f = KnownRepr (Ctx.Assignment f)
93
94
95------------------------------------------------------------------------
96-- StringInfo
97
98data StringInfo
99     -- | 8-bit characters
100   = Char8
101     -- | 16-bit characters
102   | Char16
103     -- | Unicode code-points
104   | Unicode
105
106
107type Char8   = 'Char8   -- ^ @:: 'StringInfo'@.
108type Char16  = 'Char16  -- ^ @:: 'StringInfo'@.
109type Unicode = 'Unicode -- ^ @:: 'StringInfo'@.
110
111------------------------------------------------------------------------
112-- BaseType
113
114-- | This data kind enumerates the Crucible solver interface types,
115-- which are types that may be represented symbolically.
116data BaseType
117     -- | @BaseBoolType@ denotes Boolean values.
118   = BaseBoolType
119     -- | @BaseIntegerType@ denotes an integer.
120   | BaseIntegerType
121     -- | @BaseRealType@ denotes a real number.
122   | BaseRealType
123     -- | @BaseBVType n@ denotes a bitvector with @n@-bits.
124   | BaseBVType TypeNats.Nat
125     -- | @BaseFloatType fpp@ denotes a floating-point number with @fpp@
126     -- precision.
127   | BaseFloatType FloatPrecision
128     -- | @BaseStringType@ denotes a sequence of Unicode codepoints
129   | BaseStringType StringInfo
130     -- | @BaseComplexType@ denotes a complex number with real components.
131   | BaseComplexType
132     -- | @BaseStructType tps@ denotes a sequence of values with types @tps@.
133   | BaseStructType (Ctx.Ctx BaseType)
134     -- | @BaseArrayType itps rtp@ denotes a function mapping indices @itps@
135     -- to values of type @rtp@.
136     --
137     -- It does not have bounds as one would normally expect from an
138     -- array in a programming language, but the solver does provide
139     -- operations for doing pointwise updates.
140   | BaseArrayType  (Ctx.Ctx BaseType) BaseType
141
142type BaseBoolType    = 'BaseBoolType    -- ^ @:: 'BaseType'@.
143type BaseIntegerType = 'BaseIntegerType -- ^ @:: 'BaseType'@.
144type BaseRealType    = 'BaseRealType    -- ^ @:: 'BaseType'@.
145type BaseBVType      = 'BaseBVType      -- ^ @:: 'TypeNats.Nat' -> 'BaseType'@.
146type BaseFloatType   = 'BaseFloatType   -- ^ @:: 'FloatPrecision' -> 'BaseType'@.
147type BaseStringType  = 'BaseStringType  -- ^ @:: 'BaseType'@.
148type BaseComplexType = 'BaseComplexType -- ^ @:: 'BaseType'@.
149type BaseStructType  = 'BaseStructType  -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'BaseType'@.
150type BaseArrayType   = 'BaseArrayType   -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'BaseType' -> 'BaseType'@.
151
152-- | This data kind describes the types of floating-point formats.
153-- This consist of the standard IEEE 754-2008 binary floating point formats.
154data FloatPrecision where
155  FloatingPointPrecision :: TypeNats.Nat   -- number of bits for the exponent field
156                         -> TypeNats.Nat   -- number of bits for the significand field
157                         -> FloatPrecision
158type FloatingPointPrecision = 'FloatingPointPrecision -- ^ @:: 'GHC.TypeNats.Nat' -> 'GHC.TypeNats.Nat' -> 'FloatPrecision'@.
159
160-- | This computes the number of bits occupied by a floating-point format.
161type family FloatPrecisionBits (fpp :: FloatPrecision) :: Nat where
162  FloatPrecisionBits (FloatingPointPrecision eb sb) = eb + sb
163
164-- | Floating-point precision aliases
165type Prec16  = FloatingPointPrecision  5  11
166type Prec32  = FloatingPointPrecision  8  24
167type Prec64  = FloatingPointPrecision 11  53
168type Prec80  = FloatingPointPrecision 15  65
169type Prec128 = FloatingPointPrecision 15 113
170
171------------------------------------------------------------------------
172-- BaseTypeRepr
173
174-- | A runtime representation of a solver interface type. Parameter @bt@
175-- has kind 'BaseType'.
176data BaseTypeRepr (bt::BaseType) :: Type where
177   BaseBoolRepr    :: BaseTypeRepr BaseBoolType
178   BaseBVRepr      :: (1 <= w) => !(NatRepr w) -> BaseTypeRepr (BaseBVType w)
179   BaseIntegerRepr :: BaseTypeRepr BaseIntegerType
180   BaseRealRepr    :: BaseTypeRepr BaseRealType
181   BaseFloatRepr   :: !(FloatPrecisionRepr fpp) -> BaseTypeRepr (BaseFloatType fpp)
182   BaseStringRepr  :: StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
183   BaseComplexRepr :: BaseTypeRepr BaseComplexType
184
185   -- The representation of a struct type.
186   BaseStructRepr :: !(Ctx.Assignment BaseTypeRepr ctx)
187                  -> BaseTypeRepr (BaseStructType ctx)
188
189   BaseArrayRepr :: !(Ctx.Assignment BaseTypeRepr (idx Ctx.::> tp))
190                 -> !(BaseTypeRepr xs)
191                 -> BaseTypeRepr (BaseArrayType (idx Ctx.::> tp) xs)
192
193data FloatPrecisionRepr (fpp :: FloatPrecision) where
194  FloatingPointPrecisionRepr
195    :: (2 <= eb, 2 <= sb)
196    => !(NatRepr eb)
197    -> !(NatRepr sb)
198    -> FloatPrecisionRepr (FloatingPointPrecision eb sb)
199
200data StringInfoRepr (si::StringInfo) where
201  Char8Repr     :: StringInfoRepr Char8
202  Char16Repr    :: StringInfoRepr Char16
203  UnicodeRepr   :: StringInfoRepr Unicode
204
205-- | Return the type of the indices for an array type.
206arrayTypeIndices :: BaseTypeRepr (BaseArrayType idx tp)
207                 -> Ctx.Assignment BaseTypeRepr idx
208arrayTypeIndices (BaseArrayRepr i _) = i
209
210-- | Return the result type of an array type.
211arrayTypeResult :: BaseTypeRepr (BaseArrayType idx tp) -> BaseTypeRepr tp
212arrayTypeResult (BaseArrayRepr _ rtp) = rtp
213
214floatPrecisionToBVType
215  :: FloatPrecisionRepr (FloatingPointPrecision eb sb)
216  -> BaseTypeRepr (BaseBVType (eb + sb))
217floatPrecisionToBVType fpp@(FloatingPointPrecisionRepr eb sb)
218  | LeqProof <- lemmaFloatPrecisionIsPos fpp
219  = BaseBVRepr $ addNat eb sb
220
221lemmaFloatPrecisionIsPos
222  :: forall eb' sb'
223   . FloatPrecisionRepr (FloatingPointPrecision eb' sb')
224  -> LeqProof 1 (eb' + sb')
225lemmaFloatPrecisionIsPos (FloatingPointPrecisionRepr eb sb)
226  | LeqProof <- leqTrans (LeqProof @1 @2) (LeqProof @2 @eb')
227  , LeqProof <- leqTrans (LeqProof @1 @2) (LeqProof @2 @sb')
228  = leqAddPos eb sb
229
230instance KnownRepr BaseTypeRepr BaseBoolType where
231  knownRepr = BaseBoolRepr
232instance KnownRepr BaseTypeRepr BaseIntegerType where
233  knownRepr = BaseIntegerRepr
234instance KnownRepr BaseTypeRepr BaseRealType where
235  knownRepr = BaseRealRepr
236instance KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si) where
237  knownRepr = BaseStringRepr knownRepr
238instance (1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w) where
239  knownRepr = BaseBVRepr knownNat
240instance (KnownRepr FloatPrecisionRepr fpp) => KnownRepr BaseTypeRepr (BaseFloatType fpp) where
241  knownRepr = BaseFloatRepr knownRepr
242instance KnownRepr BaseTypeRepr BaseComplexType where
243  knownRepr = BaseComplexRepr
244
245instance KnownRepr (Ctx.Assignment BaseTypeRepr) ctx
246      => KnownRepr BaseTypeRepr (BaseStructType ctx) where
247  knownRepr = BaseStructRepr knownRepr
248
249instance ( KnownRepr (Ctx.Assignment BaseTypeRepr) idx
250         , KnownRepr BaseTypeRepr tp
251         , KnownRepr BaseTypeRepr t
252         )
253      => KnownRepr BaseTypeRepr (BaseArrayType (idx Ctx.::> tp) t) where
254  knownRepr = BaseArrayRepr knownRepr knownRepr
255
256instance (2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es) where
257  knownRepr = FloatingPointPrecisionRepr knownNat knownNat
258
259instance KnownRepr StringInfoRepr Char8 where
260  knownRepr = Char8Repr
261instance KnownRepr StringInfoRepr Char16 where
262  knownRepr = Char16Repr
263instance KnownRepr StringInfoRepr Unicode where
264  knownRepr = UnicodeRepr
265
266
267-- Force BaseTypeRepr, etc. to be in context for next slice.
268$(return [])
269
270instance HashableF BaseTypeRepr where
271  hashWithSaltF = hashWithSalt
272instance Hashable (BaseTypeRepr bt) where
273  hashWithSalt = $(structuralHashWithSalt [t|BaseTypeRepr|] [])
274
275instance HashableF FloatPrecisionRepr where
276  hashWithSaltF = hashWithSalt
277instance Hashable (FloatPrecisionRepr fpp) where
278  hashWithSalt = $(structuralHashWithSalt [t|FloatPrecisionRepr|] [])
279
280instance HashableF StringInfoRepr where
281  hashWithSaltF = hashWithSalt
282instance Hashable (StringInfoRepr si) where
283  hashWithSalt = $(structuralHashWithSalt [t|StringInfoRepr|] [])
284
285instance Pretty (BaseTypeRepr bt) where
286  pretty = viaShow
287instance Show (BaseTypeRepr bt) where
288  showsPrec = $(structuralShowsPrec [t|BaseTypeRepr|])
289instance ShowF BaseTypeRepr
290
291instance Pretty (FloatPrecisionRepr fpp) where
292  pretty = viaShow
293instance Show (FloatPrecisionRepr fpp) where
294  showsPrec = $(structuralShowsPrec [t|FloatPrecisionRepr|])
295instance ShowF FloatPrecisionRepr
296
297instance Pretty (StringInfoRepr si) where
298  pretty = viaShow
299instance Show (StringInfoRepr si) where
300  showsPrec = $(structuralShowsPrec [t|StringInfoRepr|])
301instance ShowF StringInfoRepr
302
303instance TestEquality BaseTypeRepr where
304  testEquality = $(structuralTypeEquality [t|BaseTypeRepr|]
305                   [ (TypeApp (ConType [t|NatRepr|]) AnyType, [|testEquality|])
306                   , (TypeApp (ConType [t|FloatPrecisionRepr|]) AnyType, [|testEquality|])
307                   , (TypeApp (ConType [t|StringInfoRepr|]) AnyType, [|testEquality|])
308                   , (TypeApp (ConType [t|BaseTypeRepr|]) AnyType, [|testEquality|])
309                   , ( TypeApp (TypeApp (ConType [t|Ctx.Assignment|]) AnyType) AnyType
310                     , [|testEquality|]
311                     )
312                   ]
313                  )
314
315instance OrdF BaseTypeRepr where
316  compareF = $(structuralTypeOrd [t|BaseTypeRepr|]
317                   [ (TypeApp (ConType [t|NatRepr|]) AnyType, [|compareF|])
318                   , (TypeApp (ConType [t|FloatPrecisionRepr|]) AnyType, [|compareF|])
319                   , (TypeApp (ConType [t|StringInfoRepr|]) AnyType, [|compareF|])
320                   , (TypeApp (ConType [t|BaseTypeRepr|]) AnyType, [|compareF|])
321                   , (TypeApp (TypeApp (ConType [t|Ctx.Assignment|]) AnyType) AnyType
322                     , [|compareF|]
323                     )
324                   ]
325                  )
326
327instance TestEquality FloatPrecisionRepr where
328  testEquality = $(structuralTypeEquality [t|FloatPrecisionRepr|]
329      [(TypeApp (ConType [t|NatRepr|]) AnyType, [|testEquality|])]
330    )
331instance OrdF FloatPrecisionRepr where
332  compareF = $(structuralTypeOrd [t|FloatPrecisionRepr|]
333      [(TypeApp (ConType [t|NatRepr|]) AnyType, [|compareF|])]
334    )
335
336instance TestEquality StringInfoRepr where
337  testEquality = $(structuralTypeEquality [t|StringInfoRepr|] [])
338instance OrdF StringInfoRepr where
339  compareF = $(structuralTypeOrd [t|StringInfoRepr|] [])
340