{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE NamedFieldPuns            #-}
{-# LANGUAGE Safe                      #-}
{-# LANGUAGE ViewPatterns              #-}

-- | Connection to theorem provers.
module Copilot.Theorem.Prove
  ( Output  (..)
  , Status  (..)
  , Prover  (..)
  , PropId, PropRef (..)
  , Proof, UProof, ProofScheme (..)
  , Action (..)
  , Universal, Existential
  , check
  , prove
  , combine
  ) where

import qualified Copilot.Core as Core

import Data.List (intercalate)
import Control.Applicative (liftA2)
import Control.Monad.Writer

-- | Output produced by a prover, containing the 'Status' of the proof and
-- additional information.
data Output = Output Status [String]

-- | Status returned by a prover when given a specification and a property to
-- prove.
data Status = Sat | Valid | Invalid | Unknown | Error

-- | A connection to a prover able to check the satisfiability of
-- specifications.
--
-- The most important is `askProver`, which takes 3 arguments :
--
-- *  The prover descriptor
--
-- *  A list of properties names which are assumptions
--
-- *  A properties that have to be deduced from these assumptions
data Prover = forall r . Prover
  { Prover -> PropId
proverName  :: String
  , ()
startProver :: Core.Spec -> IO r
  , ()
askProver   :: r -> [PropId] -> [PropId] -> IO Output
  , ()
closeProver :: r -> IO ()
  }

-- | A unique property identifier
type PropId = String

-- | Reference to a property.
data PropRef a where
  PropRef :: PropId -> PropRef a

-- | Empty datatype to mark proofs of universally quantified predicates.
data Universal

-- | Empty datatype to mark proofs of existentially quantified predicates.
data Existential

-- | A proof scheme with unit result.
type Proof a = ProofScheme a ()

-- | A sequence of computations that generate a trace of required prover
-- 'Action's.
type UProof = Writer [Action] ()

-- | A proof scheme is a sequence of computations that compute a result and
-- generate a trace of required prover 'Action's.
data ProofScheme a b where
  Proof :: Writer [Action] b -> ProofScheme a b

instance Functor (ProofScheme a) where
  fmap :: forall a b. (a -> b) -> ProofScheme a a -> ProofScheme a b
fmap = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Applicative (ProofScheme a) where
  pure :: forall a. a -> ProofScheme a a
pure = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b.
ProofScheme a (a -> b) -> ProofScheme a a -> ProofScheme a b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad (ProofScheme a) where
  (Proof Writer [Action] a
p) >>= :: forall a b.
ProofScheme a a -> (a -> ProofScheme a b) -> ProofScheme a b
>>= a -> ProofScheme a b
f = forall b a. Writer [Action] b -> ProofScheme a b
Proof forall a b. (a -> b) -> a -> b
$ Writer [Action] a
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a
a -> case a -> ProofScheme a b
f a
a of Proof WriterT [Action] Identity b
p' -> WriterT [Action] Identity b
p')
  return :: forall a. a -> ProofScheme a a
return a
a = forall b a. Writer [Action] b -> ProofScheme a b
Proof (forall (m :: * -> *) a. Monad m => a -> m a
return a
a)

-- | Prover actions.
data Action where
  Check  :: Prover -> Action
  Assume :: PropId -> Action
  Admit  :: Action

-- | Record a requirement for satisfiability checking.
check :: Prover -> Proof a
check :: forall a. Prover -> Proof a
check Prover
prover = forall b a. Writer [Action] b -> ProofScheme a b
Proof forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Prover -> Action
Check Prover
prover]

-- | Try to prove a property in a specification with a given proof scheme.
--
-- Return 'True' if a proof of satisfiability or validity is found, false
-- otherwise.
prove :: Core.Spec -> PropId -> UProof -> IO Bool
prove :: Spec -> PropId -> UProof -> IO Bool
prove Spec
spec PropId
propId (forall w a. Writer w a -> w
execWriter -> [Action]
actions) = do

    [PropId]
thms <- [PropId] -> [Action] -> IO [PropId]
processActions [] [Action]
actions
    PropId -> IO ()
putStr forall a b. (a -> b) -> a -> b
$ PropId
"Finished: " forall a. [a] -> [a] -> [a]
++ PropId
propId forall a. [a] -> [a] -> [a]
++ PropId
": proof "
    if (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem PropId
propId [PropId]
thms) then (PropId -> IO ()
putStrLn PropId
"checked successfully") else (PropId -> IO ()
putStrLn PropId
"failed")
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem PropId
propId [PropId]
thms

    where
      processActions :: [PropId] -> [Action] -> IO [PropId]
processActions [PropId]
context [] = forall (m :: * -> *) a. Monad m => a -> m a
return [PropId]
context
      processActions [PropId]
context (Action
action:[Action]
nextActions) = case Action
action of
        Check (Prover { Spec -> IO r
startProver :: Spec -> IO r
startProver :: ()
startProver, r -> [PropId] -> [PropId] -> IO Output
askProver :: r -> [PropId] -> [PropId] -> IO Output
askProver :: ()
askProver, r -> IO ()
closeProver :: r -> IO ()
closeProver :: ()
closeProver }) -> do
          r
prover <- Spec -> IO r
startProver Spec
spec
          (Output Status
status [PropId]
infos) <- r -> [PropId] -> [PropId] -> IO Output
askProver r
prover [PropId]
context [PropId
propId]
          r -> IO ()
closeProver r
prover
          case Status
status of
            Status
Sat     -> do
              PropId -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ PropId
propId forall a. [a] -> [a] -> [a]
++ PropId
": sat " forall a. [a] -> [a] -> [a]
++ PropId
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate PropId
", " [PropId]
infos forall a. [a] -> [a] -> [a]
++ PropId
")"
              [PropId] -> [Action] -> IO [PropId]
processActions (PropId
propId forall a. a -> [a] -> [a]
: [PropId]
context) [Action]
nextActions
            Status
Valid   -> do
              PropId -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ PropId
propId forall a. [a] -> [a] -> [a]
++ PropId
": valid " forall a. [a] -> [a] -> [a]
++ PropId
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate PropId
", " [PropId]
infos forall a. [a] -> [a] -> [a]
++ PropId
")"
              [PropId] -> [Action] -> IO [PropId]
processActions (PropId
propId forall a. a -> [a] -> [a]
: [PropId]
context) [Action]
nextActions
            Status
Invalid -> do
              PropId -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ PropId
propId forall a. [a] -> [a] -> [a]
++ PropId
": invalid " forall a. [a] -> [a] -> [a]
++ PropId
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate PropId
", " [PropId]
infos forall a. [a] -> [a] -> [a]
++ PropId
")"
              [PropId] -> [Action] -> IO [PropId]
processActions [PropId]
context [Action]
nextActions
            Status
Error   -> do
              PropId -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ PropId
propId forall a. [a] -> [a] -> [a]
++ PropId
": error " forall a. [a] -> [a] -> [a]
++ PropId
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate PropId
", " [PropId]
infos forall a. [a] -> [a] -> [a]
++ PropId
")"
              [PropId] -> [Action] -> IO [PropId]
processActions [PropId]
context [Action]
nextActions
            Status
Unknown -> do
              PropId -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ PropId
propId forall a. [a] -> [a] -> [a]
++ PropId
": unknown " forall a. [a] -> [a] -> [a]
++ PropId
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate PropId
", " [PropId]
infos forall a. [a] -> [a] -> [a]
++ PropId
")"
              [PropId] -> [Action] -> IO [PropId]
processActions [PropId]
context [Action]
nextActions

        Assume PropId
propId' -> do
          PropId -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ PropId
propId' forall a. [a] -> [a] -> [a]
++ PropId
": assumption"
          [PropId] -> [Action] -> IO [PropId]
processActions (PropId
propId' forall a. a -> [a] -> [a]
: [PropId]
context) [Action]
nextActions

        Action
Admit -> do
          PropId -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ PropId
propId forall a. [a] -> [a] -> [a]
++ PropId
": admitted"
          [PropId] -> [Action] -> IO [PropId]
processActions (PropId
propId forall a. a -> [a] -> [a]
: [PropId]
context) [Action]
nextActions

-- | Combine two provers producing a new prover that will run both provers in
-- parallel and combine their outputs.
--
-- The results produced by the provers must be consistent. For example, if one
-- of the provers indicates that a property is 'Valid' while another indicates
-- that it is 'Invalid', the combination of both provers will return an
-- 'Error'.
combine :: Prover -> Prover -> Prover
combine :: Prover -> Prover -> Prover
combine
  (Prover { proverName :: Prover -> PropId
proverName  = PropId
proverNameL
          , startProver :: ()
startProver = Spec -> IO r
startProverL
          , askProver :: ()
askProver   = r -> [PropId] -> [PropId] -> IO Output
askProverL
          , closeProver :: ()
closeProver = r -> IO ()
closeProverL
          })

  (Prover { proverName :: Prover -> PropId
proverName  = PropId
proverNameR
          , startProver :: ()
startProver = Spec -> IO r
startProverR
          , askProver :: ()
askProver   = r -> [PropId] -> [PropId] -> IO Output
askProverR
          , closeProver :: ()
closeProver = r -> IO ()
closeProverR
          })

 = Prover
  { proverName :: PropId
proverName  = PropId
proverNameL forall a. [a] -> [a] -> [a]
++ PropId
"_" forall a. [a] -> [a] -> [a]
++ PropId
proverNameR
  , startProver :: Spec -> IO (r, r)
startProver = \Spec
spec -> do
      r
proverL <- Spec -> IO r
startProverL Spec
spec
      r
proverR <- Spec -> IO r
startProverR Spec
spec
      forall (m :: * -> *) a. Monad m => a -> m a
return (r
proverL, r
proverR)

  , askProver :: (r, r) -> [PropId] -> [PropId] -> IO Output
askProver = \(r
stL, r
stR) [PropId]
assumptions [PropId]
toCheck ->
      forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (PropId -> PropId -> Output -> Output -> Output
combineOutputs PropId
proverNameL PropId
proverNameR)
        (r -> [PropId] -> [PropId] -> IO Output
askProverL r
stL [PropId]
assumptions [PropId]
toCheck)
        (r -> [PropId] -> [PropId] -> IO Output
askProverR r
stR [PropId]
assumptions [PropId]
toCheck)

  , closeProver :: (r, r) -> IO ()
closeProver = \(r
stL, r
stR) -> do
      r -> IO ()
closeProverL r
stL
      r -> IO ()
closeProverR r
stR
  }

combineOutputs :: [Char] -> [Char] -> Output -> Output -> Output
combineOutputs :: PropId -> PropId -> Output -> Output -> Output
combineOutputs PropId
nameL PropId
nameR (Output Status
stL [PropId]
msgL) (Output Status
stR [PropId]
msgR) =
  Status -> [PropId] -> Output
Output (Status -> Status -> Status
combineSt Status
stL Status
stR) [PropId]
infos

  where
    combineSt :: Status -> Status -> Status
combineSt Status
Error Status
_         = Status
Error
    combineSt  Status
_ Status
Error        = Status
Error

    combineSt Status
Valid Status
Invalid   = Status
Error
    combineSt Status
Invalid Status
Valid   = Status
Error

    combineSt Status
Invalid Status
_       = Status
Invalid
    combineSt Status
_ Status
Invalid       = Status
Invalid

    combineSt Status
Valid Status
_         = Status
Valid
    combineSt Status
_ Status
Valid         = Status
Valid

    combineSt Status
Sat Status
_           = Status
Sat
    combineSt Status
_ Status
Sat           = Status
Sat

    combineSt Status
Unknown Status
Unknown = Status
Unknown

    prefixMsg :: [PropId]
prefixMsg = case (Status
stL, Status
stR) of
      (Status
Valid, Status
Invalid) -> [PropId
"The two provers don't agree"]
      (Status, Status)
_ -> []

    decoName :: PropId -> PropId
decoName PropId
s = PropId
"<" forall a. [a] -> [a] -> [a]
++ PropId
s forall a. [a] -> [a] -> [a]
++ PropId
">"

    infos :: [PropId]
infos =
      [PropId]
prefixMsg
      forall a. [a] -> [a] -> [a]
++ [PropId -> PropId
decoName PropId
nameL]
      forall a. [a] -> [a] -> [a]
++ [PropId]
msgL
      forall a. [a] -> [a] -> [a]
++ [PropId -> PropId
decoName PropId
nameR]
      forall a. [a] -> [a] -> [a]
++ [PropId]
msgR