-- | An example showing the usage of the What4 backend in copilot-theorem for
-- structs and arrays. Particular focus is on nested structs.
-- For general usage of structs, refer to the general structs example.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Copilot.Verifier.Examples.ShouldPass.Structs where

import Control.Monad (void, forM_, when)
import qualified Prelude as P

import Language.Copilot
import Copilot.Compile.C99
import Copilot.Theorem.What4
import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )


-- | Definition for `Volts`.
data Volts = Volts
  { Volts -> Field "numVolts" Word16
numVolts :: Field "numVolts" Word16
  , Volts -> Field "flag" Bool
flag     :: Field "flag"     Bool
  }

-- | `Struct` instance for `Volts`.
instance Struct Volts where
  typeName :: Volts -> String
typeName Volts
_ = String
"volts"
  toValues :: Volts -> [Value Volts]
toValues Volts
vlts = [ Type Word16 -> Field "numVolts" Word16 -> Value Volts
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type Word16
Word16 (Volts -> Field "numVolts" Word16
numVolts Volts
vlts)
                  , Type Bool -> Field "flag" Bool -> Value Volts
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type Bool
Bool   (Volts -> Field "flag" Bool
flag Volts
vlts)
                  ]

-- | `Volts` instance for `Typed`.
instance Typed Volts where
  typeOf :: Type Volts
typeOf = Volts -> Type Volts
forall a. (Typed a, Struct a) => a -> Type a
Struct (Field "numVolts" Word16 -> Field "flag" Bool -> Volts
Volts (Word16 -> Field "numVolts" Word16
forall (s :: Symbol) t. t -> Field s t
Field Word16
0) (Bool -> Field "flag" Bool
forall (s :: Symbol) t. t -> Field s t
Field Bool
False))

data Battery = Battery
  { Battery -> Field "temp" Word16
temp  :: Field "temp"  Word16
  , Battery -> Field "volts" (Array 10 Volts)
volts :: Field "volts" (Array 10 Volts)
  , Battery -> Field "other" (Array 10 (Array 5 Word32))
other :: Field "other" (Array 10 (Array 5 Word32))
  }

-- | `Battery` instance for `Struct`.
instance Struct Battery where
  typeName :: Battery -> String
typeName Battery
_ = String
"battery"
  toValues :: Battery -> [Value Battery]
toValues Battery
battery = [ Type Word16 -> Field "temp" Word16 -> Value Battery
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type Word16
forall a. Typed a => Type a
typeOf (Battery -> Field "temp" Word16
temp Battery
battery)
                     , Type (Array 10 Volts)
-> Field "volts" (Array 10 Volts) -> Value Battery
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type (Array 10 Volts)
forall a. Typed a => Type a
typeOf (Battery -> Field "volts" (Array 10 Volts)
volts Battery
battery)
                     , Type (Array 10 (Array 5 Word32))
-> Field "other" (Array 10 (Array 5 Word32)) -> Value Battery
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type (Array 10 (Array 5 Word32))
forall a. Typed a => Type a
typeOf (Battery -> Field "other" (Array 10 (Array 5 Word32))
other Battery
battery)
                     ]

-- | `Battery` instance for `Typed`. Note that `undefined` is used as an
-- argument to `Field`. This argument is never used, so `undefined` will never
-- throw an error.
instance Typed Battery where
  typeOf :: Type Battery
typeOf = Battery -> Type Battery
forall a. (Typed a, Struct a) => a -> Type a
Struct (Field "temp" Word16
-> Field "volts" (Array 10 Volts)
-> Field "other" (Array 10 (Array 5 Word32))
-> Battery
Battery (Word16 -> Field "temp" Word16
forall (s :: Symbol) t. t -> Field s t
Field Word16
0) (Array 10 Volts -> Field "volts" (Array 10 Volts)
forall (s :: Symbol) t. t -> Field s t
Field Array 10 Volts
forall a. HasCallStack => a
undefined) (Array 10 (Array 5 Word32)
-> Field "other" (Array 10 (Array 5 Word32))
forall (s :: Symbol) t. t -> Field s t
Field Array 10 (Array 5 Word32)
forall a. HasCallStack => a
undefined))

spec :: Spec
spec :: Spec
spec = do
  let battery :: Stream Battery
      battery :: Stream Battery
battery = String -> Maybe [Battery] -> Stream Battery
forall a. Typed a => String -> Maybe [a] -> Stream a
extern String
"battery" Maybe [Battery]
forall a. Maybe a
Nothing

  -- Check equality, indexing into nested structs and arrays. Note that this is
  -- trivial by equality.
  WriterT [SpecItem] Identity (PropRef Universal) -> Spec
forall (f :: * -> *) a. Functor f => f a -> f ()
void (WriterT [SpecItem] Identity (PropRef Universal) -> Spec)
-> WriterT [SpecItem] Identity (PropRef Universal) -> Spec
forall a b. (a -> b) -> a -> b
$ String
-> Prop Universal
-> WriterT [SpecItem] Identity (PropRef Universal)
forall a. String -> Prop a -> Writer [SpecItem] (PropRef a)
prop String
"Example 1" (Prop Universal -> WriterT [SpecItem] Identity (PropRef Universal))
-> Prop Universal
-> WriterT [SpecItem] Identity (PropRef Universal)
forall a b. (a -> b) -> a -> b
$ Stream Bool -> Prop Universal
forAll (Stream Bool -> Prop Universal) -> Stream Bool -> Prop Universal
forall a b. (a -> b) -> a -> b
$
    (((Stream Battery
batteryStream Battery
-> (Battery -> Field "volts" (Array 10 Volts))
-> Stream (Array 10 Volts)
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#Battery -> Field "volts" (Array 10 Volts)
volts) Stream (Array 10 Volts) -> Stream Word32 -> Stream Volts
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
0)Stream Volts -> (Volts -> Field "numVolts" Word16) -> Stream Word16
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#Volts -> Field "numVolts" Word16
numVolts) Stream Word16 -> Stream Word16 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== (((Stream Battery
batteryStream Battery
-> (Battery -> Field "volts" (Array 10 Volts))
-> Stream (Array 10 Volts)
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#Battery -> Field "volts" (Array 10 Volts)
volts) Stream (Array 10 Volts) -> Stream Word32 -> Stream Volts
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
0)Stream Volts -> (Volts -> Field "numVolts" Word16) -> Stream Word16
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#Volts -> Field "numVolts" Word16
numVolts)

  -- Same as previous example, but get a different array index (so should be
  -- false).
  WriterT [SpecItem] Identity (PropRef Universal) -> Spec
forall (f :: * -> *) a. Functor f => f a -> f ()
void (WriterT [SpecItem] Identity (PropRef Universal) -> Spec)
-> WriterT [SpecItem] Identity (PropRef Universal) -> Spec
forall a b. (a -> b) -> a -> b
$ String
-> Prop Universal
-> WriterT [SpecItem] Identity (PropRef Universal)
forall a. String -> Prop a -> Writer [SpecItem] (PropRef a)
prop String
"Example 2" (Prop Universal -> WriterT [SpecItem] Identity (PropRef Universal))
-> Prop Universal
-> WriterT [SpecItem] Identity (PropRef Universal)
forall a b. (a -> b) -> a -> b
$ Stream Bool -> Prop Universal
forAll (Stream Bool -> Prop Universal) -> Stream Bool -> Prop Universal
forall a b. (a -> b) -> a -> b
$
    (((Stream Battery
batteryStream Battery
-> (Battery -> Field "other" (Array 10 (Array 5 Word32)))
-> Stream (Array 10 (Array 5 Word32))
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#Battery -> Field "other" (Array 10 (Array 5 Word32))
other) Stream (Array 10 (Array 5 Word32))
-> Stream Word32 -> Stream (Array 5 Word32)
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
2) Stream (Array 5 Word32) -> Stream Word32 -> Stream Word32
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
3) Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== (((Stream Battery
batteryStream Battery
-> (Battery -> Field "other" (Array 10 (Array 5 Word32)))
-> Stream (Array 10 (Array 5 Word32))
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#Battery -> Field "other" (Array 10 (Array 5 Word32))
other) Stream (Array 10 (Array 5 Word32))
-> Stream Word32 -> Stream (Array 5 Word32)
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
2) Stream (Array 5 Word32) -> Stream Word32 -> Stream Word32
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
4)

  -- Same as previous example, but in trigger form
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"otherTrig" ((((Stream Battery
batteryStream Battery
-> (Battery -> Field "other" (Array 10 (Array 5 Word32)))
-> Stream (Array 10 (Array 5 Word32))
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#Battery -> Field "other" (Array 10 (Array 5 Word32))
other) Stream (Array 10 (Array 5 Word32))
-> Stream Word32 -> Stream (Array 5 Word32)
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
2) Stream (Array 5 Word32) -> Stream Word32 -> Stream Word32
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
3) Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== (((Stream Battery
batteryStream Battery
-> (Battery -> Field "other" (Array 10 (Array 5 Word32)))
-> Stream (Array 10 (Array 5 Word32))
forall (f :: Symbol) t s.
(KnownSymbol f, Typed t, Typed s, Struct s) =>
Stream s -> (s -> Field f t) -> Stream t
#Battery -> Field "other" (Array 10 (Array 5 Word32))
other) Stream (Array 10 (Array 5 Word32))
-> Stream Word32 -> Stream (Array 5 Word32)
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
2) Stream (Array 5 Word32) -> Stream Word32 -> Stream Word32
forall (n :: Nat) t.
(KnownNat n, Typed t) =>
Stream (Array n t) -> Stream Word32 -> Stream t
! Stream Word32
4))
                      [Stream Battery -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Battery
battery]

verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb = do
  Spec
spec' <- Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
spec

  -- Use Z3 to prove the properties.
  [(String, SatResult)]
results <- Solver -> Spec -> IO [(String, SatResult)]
prove Solver
Z3 Spec
spec'

  -- Print the results.
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Verbosity
verb Verbosity -> Verbosity -> Bool
forall a. Ord a => a -> a -> Bool
P.>= Verbosity
Default) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
    [(String, SatResult)] -> ((String, SatResult) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(String, SatResult)]
results (((String, SatResult) -> IO ()) -> IO ())
-> ((String, SatResult) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(String
nm, SatResult
res) -> do
      String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
nm String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
": "
      case SatResult
res of
        SatResult
Valid   -> String -> IO ()
putStrLn String
"valid"
        SatResult
Invalid -> String -> IO ()
putStrLn String
"invalid"
        SatResult
Unknown -> String -> IO ()
putStrLn String
"unknown"

  VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions{verbosity = verb}
                    CSettings
mkDefaultCSettings [] String
"structs" Spec
spec'