{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

module Copilot.Verifier.FloatMode
  ( FloatMode(..)
  , withFloatMode
  , withInterpretedFloatExprBuilder
  ) where

import qualified What4.Expr.Builder as W4
import qualified What4.InterpretedFloatingPoint as W4

-- | How the verifier should interpret floating-point operations.
data FloatMode
  = -- | Floating-point values are treated as bitvectors of the appropriate
    -- width, and all operations on them are translated as uninterpreted
    -- functions. This is the verifier's default interpretation, and it is what
    -- allows the verifier to perform any reasoning at all over floating-point
    -- operations that are not native to SMT-LIB (@sin@, @cos@, @tan@, etc.).
    FloatUninterpreted

  | -- | Floating-point values are treated as bit-precise IEEE-754 floats. This
    -- interpretation can perform deeper reasoning about floating-point
    -- operations that are native to SMT-LIB, but at the expense of causing the
    -- verifier to throw an error if it encounters operations that are not
    -- native to SMT-LIB (@sin@, @cos@, @tan@, etc.). Use at your own risk.
    FloatIEEE
  deriving Int -> FloatMode -> ShowS
[FloatMode] -> ShowS
FloatMode -> String
(Int -> FloatMode -> ShowS)
-> (FloatMode -> String)
-> ([FloatMode] -> ShowS)
-> Show FloatMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FloatMode -> ShowS
showsPrec :: Int -> FloatMode -> ShowS
$cshow :: FloatMode -> String
show :: FloatMode -> String
$cshowList :: [FloatMode] -> ShowS
showList :: [FloatMode] -> ShowS
Show

-- | Convert a 'FloatMode' into a What4 'W4.FloatModeRepr' and pass it to a
-- continuation.
withFloatMode ::
  FloatMode ->
  (forall fm. W4.FloatModeRepr fm -> r) ->
  r
withFloatMode :: forall r.
FloatMode -> (forall (fm :: FloatMode). FloatModeRepr fm -> r) -> r
withFloatMode FloatMode
fm forall (fm :: FloatMode). FloatModeRepr fm -> r
k =
  case FloatMode
fm of
    FloatMode
FloatUninterpreted ->
      FloatModeRepr 'FloatUninterpreted -> r
forall (fm :: FloatMode). FloatModeRepr fm -> r
k FloatModeRepr 'FloatUninterpreted
W4.FloatUninterpretedRepr
    FloatMode
FloatIEEE ->
      FloatModeRepr 'FloatIEEE -> r
forall (fm :: FloatMode). FloatModeRepr fm -> r
k FloatModeRepr 'FloatIEEE
W4.FloatIEEERepr

-- | Match on a 'W4.FloatModeRepr', compute evidence that it gives rise to an
-- instance of 'W4.IsInterpretedFloatExprBuilder', and pass the evidence to a
-- continutation.
withInterpretedFloatExprBuilder ::
  W4.ExprBuilder t st (W4.Flags fm) ->
  W4.FloatModeRepr fm ->
  (W4.IsInterpretedFloatExprBuilder (W4.ExprBuilder t st (W4.Flags fm)) => r) ->
  r
withInterpretedFloatExprBuilder :: forall t (st :: * -> *) (fm :: FloatMode) r.
ExprBuilder t st (Flags fm)
-> FloatModeRepr fm
-> (IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) =>
    r)
-> r
withInterpretedFloatExprBuilder ExprBuilder t st (Flags fm)
_sym FloatModeRepr fm
fm IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) => r
k =
  case FloatModeRepr fm
fm of
    FloatModeRepr fm
W4.FloatUninterpretedRepr -> r
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) => r
k
    FloatModeRepr fm
W4.FloatIEEERepr -> r
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) => r
k
    FloatModeRepr fm
W4.FloatRealRepr -> r
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) => r
k