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