{-# LANGUAGE NamedFieldPuns, ViewPatterns, ExistentialQuantification, GADTs #-}
{-# LANGUAGE Safe #-}
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
{ 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 = liftM
instance Applicative (ProofScheme a) where
pure = return
(<*>) = ap
instance Monad (ProofScheme a) where
(Proof p) >>= f = Proof $ p >>= (\a -> case f a of Proof p' -> p')
return a = Proof (return a)
data Action where
Check :: Prover -> Action
Assume :: PropId -> Action
Admit :: Action
check :: Prover -> Proof a
check prover = Proof $ tell [Check prover]
prove :: Core.Spec -> PropId -> UProof -> IO Bool
prove spec propId (execWriter -> actions) = do
thms <- processActions [] actions
putStr $ "Finished: " ++ propId ++ ": proof "
if (elem propId thms) then (putStrLn "checked successfully") else (putStrLn "failed")
return $ elem propId thms
where
processActions context [] = return context
processActions context (action:nextActions) = case action of
Check (Prover { startProver, askProver, closeProver }) -> do
prover <- startProver spec
(Output status infos) <- askProver prover context [propId]
closeProver prover
case status of
Sat -> do
putStrLn $ propId ++ ": sat " ++ "(" ++ intercalate ", " infos ++ ")"
processActions (propId : context) nextActions
Valid -> do
putStrLn $ propId ++ ": valid " ++ "(" ++ intercalate ", " infos ++ ")"
processActions (propId : context) nextActions
Invalid -> do
putStrLn $ propId ++ ": invalid " ++ "(" ++ intercalate ", " infos ++ ")"
processActions context nextActions
Error -> do
putStrLn $ propId ++ ": error " ++ "(" ++ intercalate ", " infos ++ ")"
processActions context nextActions
Unknown -> do
putStrLn $ propId ++ ": unknown " ++ "(" ++ intercalate ", " infos ++ ")"
processActions context nextActions
Assume propId' -> do
putStrLn $ propId' ++ ": assumption"
processActions (propId' : context) nextActions
Admit -> do
putStrLn $ propId ++ ": admitted"
processActions (propId : context) nextActions
combine :: Prover -> Prover -> Prover
combine
(Prover { proverName = proverNameL
, startProver = startProverL
, askProver = askProverL
, closeProver = closeProverL
})
(Prover { proverName = proverNameR
, startProver = startProverR
, askProver = askProverR
, closeProver = closeProverR
})
= Prover
{ proverName = proverNameL ++ "_" ++ proverNameR
, startProver = \spec -> do
proverL <- startProverL spec
proverR <- startProverR spec
return (proverL, proverR)
, askProver = \(stL, stR) assumptions toCheck ->
liftA2 (combineOutputs proverNameL proverNameR)
(askProverL stL assumptions toCheck)
(askProverR stR assumptions toCheck)
, closeProver = \(stL, stR) -> do
closeProverL stL
closeProverR stR
}
combineOutputs :: [Char] -> [Char] -> Output -> Output -> Output
combineOutputs nameL nameR (Output stL msgL) (Output stR msgR) =
Output (combineSt stL stR) infos
where
combineSt Error _ = Error
combineSt _ Error = Error
combineSt Valid Invalid = Error
combineSt Invalid Valid = Error
combineSt Invalid _ = Invalid
combineSt _ Invalid = Invalid
combineSt Valid _ = Valid
combineSt _ Valid = Valid
combineSt Sat _ = Sat
combineSt _ Sat = Sat
combineSt Unknown Unknown = Unknown
prefixMsg = case (stL, stR) of
(Valid, Invalid) -> ["The two provers don't agree"]
_ -> []
decoName s = "<" ++ s ++ ">"
infos =
prefixMsg
++ [decoName nameL]
++ msgL
++ [decoName nameR]
++ msgR