{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ViewPatterns #-}
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
data Output = Output Status [String]
data Status = Sat | Valid | Invalid | Unknown | Error
data Prover = forall r . Prover
{ Prover -> PropId
proverName :: String
, ()
startProver :: Core.Spec -> IO r
, ()
askProver :: r -> [PropId] -> [PropId] -> IO Output
, ()
closeProver :: r -> IO ()
}
type PropId = String
data PropRef a where
PropRef :: PropId -> PropRef a
data Universal
data Existential
type Proof a = ProofScheme a ()
type UProof = Writer [Action] ()
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)
data Action where
Check :: Prover -> Action
Assume :: PropId -> Action
Admit :: Action
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]
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 :: 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