    {-# 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        (ap, liftM)
    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 = (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 :: forall a. a -> ProofScheme a a
    pure = a -> ProofScheme a a
    forall a. a -> ProofScheme a a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      <*> :: forall a b.
    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 Writer [Action] a
    p) >>= :: forall a b.
    ProofScheme a a -> (a -> ProofScheme a b) -> ProofScheme a b
    >>= 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 a b.
    WriterT [Action] Identity a
    -> (a -> WriterT [Action] Identity b)
    -> WriterT [Action] Identity b
    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 Writer [Action] b
    p' -> Writer [Action] b
    p')
      return :: forall a. a -> ProofScheme a a
    return a
    a = Writer [Action] a -> ProofScheme a a
    forall b a. Writer [Action] b -> ProofScheme a b
    Proof (a -> Writer [Action] a
    forall a. a -> WriterT [Action] Identity a
    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 = Writer [Action] () -> ProofScheme a ()
    forall b a. Writer [Action] b -> ProofScheme a b
    Proof (Writer [Action] () -> ProofScheme a ())
    -> Writer [Action] () -> ProofScheme 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]

    -- | 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 -> Writer [Action] () -> IO Bool
    prove Spec
    spec PropId
    propId (Writer [Action] () -> [Action]
    forall w a. Writer w a -> w
    execWriter -> [Action]
    actions) = do

        thms <- [PropId] -> [Action] -> IO [PropId]
    processActions [] [Action]
    actions
        putStr $ "Finished: " ++ propId ++ ": proof "
        if (elem propId thms) then (putStrLn "checked successfully") else (putStrLn "failed")
        return $ elem propId thms

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

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

            Action
    Admit -> do
              PropId -> IO ()
    putStrLn (PropId -> IO ()) -> PropId -> IO ()
    forall a b. (a -> b) -> a -> b
    $ PropId
    propId PropId -> PropId -> PropId
    forall a. [a] -> [a] -> [a]
    ++ PropId
    ": admitted"
              [PropId] -> [Action] -> IO [PropId]
    processActions (PropId
    propId PropId -> [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 PropId -> PropId -> PropId
    forall a. [a] -> [a] -> [a]
    ++ PropId
    "_" PropId -> PropId -> PropId
    forall a. [a] -> [a] -> [a]
    ++ PropId
    proverNameR
      , startProver :: Spec -> IO (r, r)
    startProver = \Spec
    spec -> do
          proverL <- Spec -> IO r
    startProverL Spec
    spec
          proverR <- startProverR spec
          return (proverL, proverR)

      , askProver :: (r, r) -> [PropId] -> [PropId] -> IO Output
    askProver = \(r
    stL, r
    stR) [PropId]
    assumptions [PropId]
    toCheck ->
          (Output -> Output -> Output) -> IO Output -> IO Output -> IO Output
    forall a b c. (a -> b -> c) -> IO a -> IO b -> IO c
    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
    "<" PropId -> PropId -> PropId
    forall a. [a] -> [a] -> [a]
    ++ PropId
    s PropId -> PropId -> PropId
    forall a. [a] -> [a] -> [a]
    ++ PropId
    ">"

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