-- | Equational proofs which are checked for correctedness.
{-# LANGUAGE TypeFamilies, PatternGuards, RecordWildCards, ScopedTypeVariables, OverloadedStrings #-}
module Twee.Proof(
  -- * Constructing proofs
  Proof, Derivation(..), Axiom(..),
  certify, equation, derivation,
  -- ** Smart constructors for derivations
  lemma, autoSubst, simpleLemma, axiom, symm, trans, cong, congPath,

  -- * Analysing proofs
  simplify, steps, usedLemmas, usedAxioms, usedLemmasAndSubsts, usedAxiomsAndSubsts,
  groundAxiomsAndSubsts, eliminateDefinitions, eliminateDefinitionsFromGoal,

  -- * Pretty-printing proofs
  Config(..), defaultConfig, Presentation(..),
  ProvedGoal(..), provedGoal, checkProvedGoal,
  pPrintPresentation, present, describeEquation) where

import Twee.Base hiding (invisible)
import Twee.Equation
import Twee.Utils
import qualified Twee.Index as Index
import Control.Monad
import Data.Maybe
import Data.List hiding (singleton)
import Data.Ord
import qualified Data.Set as Set
import Data.Set(Set)
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import qualified Data.IntMap.Strict as IntMap
import Control.Monad.Trans.State.Strict
import Data.Graph
import Twee.Profile

----------------------------------------------------------------------
-- Equational proofs. Only valid proofs can be constructed.
----------------------------------------------------------------------

-- | A checked proof. If you have a value of type @Proof f@,
-- it should jolly well represent a valid proof!
--
-- The only way to construct a @Proof f@ is by using 'certify'.
data Proof f =
  Proof {
    Proof f -> Equation f
equation   :: !(Equation f),
    Proof f -> Derivation f
derivation :: !(Derivation f) }
  deriving Int -> Proof f -> ShowS
[Proof f] -> ShowS
Proof f -> String
(Int -> Proof f -> ShowS)
-> (Proof f -> String) -> ([Proof f] -> ShowS) -> Show (Proof f)
forall f. (Labelled f, Show f) => Int -> Proof f -> ShowS
forall f. (Labelled f, Show f) => [Proof f] -> ShowS
forall f. (Labelled f, Show f) => Proof f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Proof f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Proof f] -> ShowS
show :: Proof f -> String
$cshow :: forall f. (Labelled f, Show f) => Proof f -> String
showsPrec :: Int -> Proof f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Proof f -> ShowS
Show

-- | A derivation is an unchecked proof. It might be wrong!
-- The way to check it is to call 'certify' to turn it into a 'Proof'.
data Derivation f =
    -- | Apply an existing rule (with proof!) to the root of a term
    UseLemma {-# UNPACK #-} !(Proof f) !(Subst f)
    -- | Apply an axiom to the root of a term
  | UseAxiom {-# UNPACK #-} !(Axiom f) !(Subst f)
    -- | Reflexivity. @'Refl' t@ proves @t = t@.
  | Refl !(Term f)
    -- | Symmetry
  | Symm !(Derivation f)
    -- | Transivitity
  | Trans !(Derivation f) !(Derivation f)
    -- | Congruence.
    -- Parallel, i.e., takes a function symbol and one derivation for each
    -- argument of that function.
  | Cong {-# UNPACK #-} !(Fun f) ![Derivation f]
  deriving (Derivation f -> Derivation f -> Bool
(Derivation f -> Derivation f -> Bool)
-> (Derivation f -> Derivation f -> Bool) -> Eq (Derivation f)
forall f. Derivation f -> Derivation f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Derivation f -> Derivation f -> Bool
$c/= :: forall f. Derivation f -> Derivation f -> Bool
== :: Derivation f -> Derivation f -> Bool
$c== :: forall f. Derivation f -> Derivation f -> Bool
Eq, Int -> Derivation f -> ShowS
[Derivation f] -> ShowS
Derivation f -> String
(Int -> Derivation f -> ShowS)
-> (Derivation f -> String)
-> ([Derivation f] -> ShowS)
-> Show (Derivation f)
forall f. (Labelled f, Show f) => Int -> Derivation f -> ShowS
forall f. (Labelled f, Show f) => [Derivation f] -> ShowS
forall f. (Labelled f, Show f) => Derivation f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Derivation f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Derivation f] -> ShowS
show :: Derivation f -> String
$cshow :: forall f. (Labelled f, Show f) => Derivation f -> String
showsPrec :: Int -> Derivation f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Derivation f -> ShowS
Show)

--  | An axiom, which comes without proof.
data Axiom f =
  Axiom {
    -- | The number of the axiom.
    -- Has no semantic meaning; for convenience only.
    Axiom f -> Int
axiom_number :: {-# UNPACK #-} !Int,
    -- | A description of the axiom.
    -- Has no semantic meaning; for convenience only.
    Axiom f -> String
axiom_name :: !String,
    -- | The equation which the axiom asserts.
    Axiom f -> Equation f
axiom_eqn :: !(Equation f) }
  deriving (Axiom f -> Axiom f -> Bool
(Axiom f -> Axiom f -> Bool)
-> (Axiom f -> Axiom f -> Bool) -> Eq (Axiom f)
forall f. Axiom f -> Axiom f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Axiom f -> Axiom f -> Bool
$c/= :: forall f. Axiom f -> Axiom f -> Bool
== :: Axiom f -> Axiom f -> Bool
$c== :: forall f. Axiom f -> Axiom f -> Bool
Eq, Eq (Axiom f)
Eq (Axiom f)
-> (Axiom f -> Axiom f -> Ordering)
-> (Axiom f -> Axiom f -> Bool)
-> (Axiom f -> Axiom f -> Bool)
-> (Axiom f -> Axiom f -> Bool)
-> (Axiom f -> Axiom f -> Bool)
-> (Axiom f -> Axiom f -> Axiom f)
-> (Axiom f -> Axiom f -> Axiom f)
-> Ord (Axiom f)
Axiom f -> Axiom f -> Bool
Axiom f -> Axiom f -> Ordering
Axiom f -> Axiom f -> Axiom f
forall f. Eq (Axiom f)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f. Axiom f -> Axiom f -> Bool
forall f. Axiom f -> Axiom f -> Ordering
forall f. Axiom f -> Axiom f -> Axiom f
min :: Axiom f -> Axiom f -> Axiom f
$cmin :: forall f. Axiom f -> Axiom f -> Axiom f
max :: Axiom f -> Axiom f -> Axiom f
$cmax :: forall f. Axiom f -> Axiom f -> Axiom f
>= :: Axiom f -> Axiom f -> Bool
$c>= :: forall f. Axiom f -> Axiom f -> Bool
> :: Axiom f -> Axiom f -> Bool
$c> :: forall f. Axiom f -> Axiom f -> Bool
<= :: Axiom f -> Axiom f -> Bool
$c<= :: forall f. Axiom f -> Axiom f -> Bool
< :: Axiom f -> Axiom f -> Bool
$c< :: forall f. Axiom f -> Axiom f -> Bool
compare :: Axiom f -> Axiom f -> Ordering
$ccompare :: forall f. Axiom f -> Axiom f -> Ordering
$cp1Ord :: forall f. Eq (Axiom f)
Ord, Int -> Axiom f -> ShowS
[Axiom f] -> ShowS
Axiom f -> String
(Int -> Axiom f -> ShowS)
-> (Axiom f -> String) -> ([Axiom f] -> ShowS) -> Show (Axiom f)
forall f. (Labelled f, Show f) => Int -> Axiom f -> ShowS
forall f. (Labelled f, Show f) => [Axiom f] -> ShowS
forall f. (Labelled f, Show f) => Axiom f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Axiom f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Axiom f] -> ShowS
show :: Axiom f -> String
$cshow :: forall f. (Labelled f, Show f) => Axiom f -> String
showsPrec :: Int -> Axiom f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Axiom f -> ShowS
Show)

-- | Checks a 'Derivation' and, if it is correct, returns a
-- certified 'Proof'.
--
-- If the 'Derivation' is incorrect, throws an exception.

-- This is the trusted core of the module.
{-# INLINEABLE certify #-}
certify :: Function f => Derivation f -> Proof f
certify :: Derivation f -> Proof f
certify Derivation f
p =
  String -> Proof f -> Proof f
forall symbol a. symbol -> a -> a
stamp String
"certify proof" (Proof f -> Proof f) -> Proof f -> Proof f
forall a b. (a -> b) -> a -> b
$
  case Derivation f -> Maybe (Equation f)
forall (m :: * -> *) f.
(Monad m, Alternative m) =>
Derivation f -> m (Equation f)
check Derivation f
p of
    Maybe (Equation f)
Nothing -> String -> Proof f
forall a. HasCallStack => String -> a
error (String
"Invalid proof created!\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Derivation f -> String
forall a. Pretty a => a -> String
prettyShow Derivation f
p)
    Just Equation f
eqn -> Equation f -> Derivation f -> Proof f
forall f. Equation f -> Derivation f -> Proof f
Proof Equation f
eqn Derivation f
p
  where
    check :: Derivation f -> m (Equation f)
check (UseLemma Proof f
proof Subst f
sub) =
      Equation f -> m (Equation f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst f -> Equation f -> Equation f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
proof))
    check (UseAxiom Axiom{Int
String
Equation f
axiom_eqn :: Equation f
axiom_name :: String
axiom_number :: Int
axiom_eqn :: forall f. Axiom f -> Equation f
axiom_name :: forall f. Axiom f -> String
axiom_number :: forall f. Axiom f -> Int
..} Subst f
sub) =
      Equation f -> m (Equation f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst f -> Equation f -> Equation f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Equation f
axiom_eqn)
    check (Refl Term f
t) =
      Equation f -> m (Equation f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
t)
    check (Symm Derivation f
p) = do
      Term f
t :=: Term f
u <- Derivation f -> m (Equation f)
check Derivation f
p
      Equation f -> m (Equation f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term f
u Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
t)
    check (Trans Derivation f
p Derivation f
q) = do
      Term f
t :=: Term f
u1 <- Derivation f -> m (Equation f)
check Derivation f
p
      Term f
u2 :=: Term f
v <- Derivation f -> m (Equation f)
check Derivation f
q
      Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term f
u1 Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u2)
      Equation f -> m (Equation f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
v)
    check (Cong Fun f
f [Derivation f]
ps) = do
      [Equation f]
eqns <- (Derivation f -> m (Equation f))
-> [Derivation f] -> m [Equation f]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Derivation f -> m (Equation f)
check [Derivation f]
ps
      Equation f -> m (Equation f)
forall (m :: * -> *) a. Monad m => a -> m a
return
        (Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Fun (BuildFun [Term f]) -> [Term f] -> Builder (BuildFun [Term f])
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
Fun (BuildFun [Term f])
f ((Equation f -> Term f) -> [Equation f] -> [Term f]
forall a b. (a -> b) -> [a] -> [b]
map Equation f -> Term f
forall f. Equation f -> Term f
eqn_lhs [Equation f]
eqns)) Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=:
         Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Fun (BuildFun [Term f]) -> [Term f] -> Builder (BuildFun [Term f])
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
Fun (BuildFun [Term f])
f ((Equation f -> Term f) -> [Equation f] -> [Term f]
forall a b. (a -> b) -> [a] -> [b]
map Equation f -> Term f
forall f. Equation f -> Term f
eqn_rhs [Equation f]
eqns)))

----------------------------------------------------------------------
-- Everything below this point need not be trusted, since all proof
-- construction goes through the "certify" function.
--
-- N.B.: For this reason, the code below must never directly invoke
-- the Proof constructor!
----------------------------------------------------------------------

-- Typeclass instances.
instance Eq (Proof f) where
  Proof f
x == :: Proof f -> Proof f -> Bool
== Proof f
y = Proof f -> Proof f -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Proof f
x Proof f
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ
instance Ord (Proof f) where
  -- Don't look at the proof itself, to prevent exponential blowup
  -- when a proof contains UseLemma
  compare :: Proof f -> Proof f -> Ordering
compare = (Proof f -> Equation f) -> Proof f -> Proof f -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Proof f -> Equation f
forall f. Proof f -> Equation f
equation

instance Symbolic (Derivation f) where
  type ConstantOf (Derivation f) = f
  termsDL :: Derivation f -> DList (TermListOf (Derivation f))
termsDL (UseLemma Proof f
_ Subst f
sub) = Subst f -> DList (TermListOf (Subst f))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Subst f
sub
  termsDL (UseAxiom Axiom f
_ Subst f
sub) = Subst f -> DList (TermListOf (Subst f))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Subst f
sub
  termsDL (Refl Term f
t) = Term f -> DList (TermListOf (Term f))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Term f
t
  termsDL (Symm Derivation f
p) = Derivation f -> DList (TermListOf (Derivation f))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Derivation f
p
  termsDL (Trans Derivation f
p Derivation f
q) = Derivation f -> DList (TermListOf (Derivation f))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Derivation f
p DList (TermList f) -> DList (TermList f) -> DList (TermList f)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Derivation f -> DList (TermListOf (Derivation f))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Derivation f
q
  termsDL (Cong Fun f
_ [Derivation f]
ps) = [Derivation f] -> DList (TermListOf [Derivation f])
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL [Derivation f]
ps

  subst_ :: (Var -> BuilderOf (Derivation f)) -> Derivation f -> Derivation f
subst_ Var -> BuilderOf (Derivation f)
sub (UseLemma Proof f
lemma Subst f
s) = Proof f -> Subst f -> Derivation f
forall f. Proof f -> Subst f -> Derivation f
UseLemma Proof f
lemma ((Var -> BuilderOf (Subst f)) -> Subst f -> Subst f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Subst f)
Var -> BuilderOf (Derivation f)
sub Subst f
s)
  subst_ Var -> BuilderOf (Derivation f)
sub (UseAxiom Axiom f
axiom Subst f
s) = Axiom f -> Subst f -> Derivation f
forall f. Axiom f -> Subst f -> Derivation f
UseAxiom Axiom f
axiom ((Var -> BuilderOf (Subst f)) -> Subst f -> Subst f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Subst f)
Var -> BuilderOf (Derivation f)
sub Subst f
s)
  subst_ Var -> BuilderOf (Derivation f)
sub (Refl Term f
t) = Term f -> Derivation f
forall f. Term f -> Derivation f
Refl ((Var -> BuilderOf (Term f)) -> Term f -> Term f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Term f)
Var -> BuilderOf (Derivation f)
sub Term f
t)
  subst_ Var -> BuilderOf (Derivation f)
sub (Symm Derivation f
p) = Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm ((Var -> BuilderOf (Derivation f)) -> Derivation f -> Derivation f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Derivation f)
sub Derivation f
p)
  subst_ Var -> BuilderOf (Derivation f)
sub (Trans Derivation f
p Derivation f
q) = Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
trans ((Var -> BuilderOf (Derivation f)) -> Derivation f -> Derivation f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Derivation f)
sub Derivation f
p) ((Var -> BuilderOf (Derivation f)) -> Derivation f -> Derivation f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Derivation f)
sub Derivation f
q)
  subst_ Var -> BuilderOf (Derivation f)
sub (Cong Fun f
f [Derivation f]
ps) = Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f ((Var -> BuilderOf [Derivation f])
-> [Derivation f] -> [Derivation f]
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf [Derivation f]
Var -> BuilderOf (Derivation f)
sub [Derivation f]
ps)

instance Function f => Pretty (Proof f) where
  pPrint :: Proof f -> Doc
pPrint = Config f
-> (Axiom f -> String) -> (Proof f -> String) -> Proof f -> Doc
forall f.
Function f =>
Config f
-> (Axiom f -> String) -> (Proof f -> String) -> Proof f -> Doc
pPrintLemma Config f
forall f. Config f
defaultConfig (Int -> String
forall a. Pretty a => a -> String
prettyShow (Int -> String) -> (Axiom f -> Int) -> Axiom f -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Axiom f -> Int
forall f. Axiom f -> Int
axiom_number) (Equation f -> String
forall a. Pretty a => a -> String
prettyShow (Equation f -> String)
-> (Proof f -> Equation f) -> Proof f -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof f -> Equation f
forall f. Proof f -> Equation f
equation)
instance (Labelled f, PrettyTerm f) => Pretty (Derivation f) where
  pPrint :: Derivation f -> Doc
pPrint (UseLemma Proof f
lemma Subst f
sub) =
    String -> Doc
text String
"subst" Doc -> Doc -> Doc
<#> [Doc] -> Doc
pPrintTuple [String -> Doc
text String
"lemma" Doc -> Doc -> Doc
<+> Equation f -> Doc
forall a. Pretty a => a -> Doc
pPrint (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
lemma), Subst f -> Doc
forall a. Pretty a => a -> Doc
pPrint Subst f
sub]
  pPrint (UseAxiom Axiom f
axiom Subst f
sub) =
    String -> Doc
text String
"subst" Doc -> Doc -> Doc
<#> [Doc] -> Doc
pPrintTuple [Axiom f -> Doc
forall a. Pretty a => a -> Doc
pPrint Axiom f
axiom, Subst f -> Doc
forall a. Pretty a => a -> Doc
pPrint Subst f
sub]
  pPrint (Refl Term f
t) =
    String -> Doc
text String
"refl" Doc -> Doc -> Doc
<#> [Doc] -> Doc
pPrintTuple [Term f -> Doc
forall a. Pretty a => a -> Doc
pPrint Term f
t]
  pPrint (Symm Derivation f
p) =
    String -> Doc
text String
"symm" Doc -> Doc -> Doc
<#> [Doc] -> Doc
pPrintTuple [Derivation f -> Doc
forall a. Pretty a => a -> Doc
pPrint Derivation f
p]
  pPrint (Trans Derivation f
p Derivation f
q) =
    String -> Doc
text String
"trans" Doc -> Doc -> Doc
<#> [Doc] -> Doc
pPrintTuple [Derivation f -> Doc
forall a. Pretty a => a -> Doc
pPrint Derivation f
p, Derivation f -> Doc
forall a. Pretty a => a -> Doc
pPrint Derivation f
q]
  pPrint (Cong Fun f
f [Derivation f]
ps) =
    String -> Doc
text String
"cong" Doc -> Doc -> Doc
<#> [Doc] -> Doc
pPrintTuple (Fun f -> Doc
forall a. Pretty a => a -> Doc
pPrint Fun f
fDoc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:(Derivation f -> Doc) -> [Derivation f] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> Doc
forall a. Pretty a => a -> Doc
pPrint [Derivation f]
ps)

instance (Labelled f, PrettyTerm f) => Pretty (Axiom f) where
  pPrint :: Axiom f -> Doc
pPrint Axiom{Int
String
Equation f
axiom_eqn :: Equation f
axiom_name :: String
axiom_number :: Int
axiom_eqn :: forall f. Axiom f -> Equation f
axiom_name :: forall f. Axiom f -> String
axiom_number :: forall f. Axiom f -> Int
..} =
    String -> Doc
text String
"axiom" Doc -> Doc -> Doc
<#>
    [Doc] -> Doc
pPrintTuple [Int -> Doc
forall a. Pretty a => a -> Doc
pPrint Int
axiom_number, String -> Doc
text String
axiom_name, Equation f -> Doc
forall a. Pretty a => a -> Doc
pPrint Equation f
axiom_eqn]

foldLemmas :: (Labelled f, PrettyTerm f) => (Map (Proof f) a -> Derivation f -> a) -> [Derivation f] -> Map (Proof f) a
foldLemmas :: (Map (Proof f) a -> Derivation f -> a)
-> [Derivation f] -> Map (Proof f) a
foldLemmas Map (Proof f) a -> Derivation f -> a
op [Derivation f]
ds =
  State (Map (Proof f) a) () -> Map (Proof f) a -> Map (Proof f) a
forall s a. State s a -> s -> s
execState ((Derivation f -> State (Map (Proof f) a) ())
-> [Derivation f] -> State (Map (Proof f) a) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Derivation f -> State (Map (Proof f) a) ()
foldGoal [Derivation f]
ds) Map (Proof f) a
forall k a. Map k a
Map.empty
  where
    foldGoal :: Derivation f -> State (Map (Proof f) a) ()
foldGoal Derivation f
p = (Proof f -> StateT (Map (Proof f) a) Identity a)
-> [Proof f] -> State (Map (Proof f) a) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Proof f -> StateT (Map (Proof f) a) Identity a
foldLemma (Derivation f -> [Proof f]
forall f. Derivation f -> [Proof f]
usedLemmas Derivation f
p)
    foldLemma :: Proof f -> StateT (Map (Proof f) a) Identity a
foldLemma Proof f
p = do
      Map (Proof f) a
m <- StateT (Map (Proof f) a) Identity (Map (Proof f) a)
forall (m :: * -> *) s. Monad m => StateT s m s
get
      case Proof f -> Map (Proof f) a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Proof f
p Map (Proof f) a
m of
        Just a
x -> a -> StateT (Map (Proof f) a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
        Maybe a
Nothing -> do
          (Proof f -> StateT (Map (Proof f) a) Identity a)
-> [Proof f] -> State (Map (Proof f) a) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Proof f -> StateT (Map (Proof f) a) Identity a
foldLemma (Derivation f -> [Proof f]
forall f. Derivation f -> [Proof f]
usedLemmas (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p))
          Map (Proof f) a
m <- StateT (Map (Proof f) a) Identity (Map (Proof f) a)
forall (m :: * -> *) s. Monad m => StateT s m s
get
          case Proof f -> Map (Proof f) a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Proof f
p Map (Proof f) a
m of
            Just a
x  -> a -> StateT (Map (Proof f) a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
            Maybe a
Nothing -> do
              let x :: a
x = Map (Proof f) a -> Derivation f -> a
op Map (Proof f) a
m (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p)
              Map (Proof f) a -> State (Map (Proof f) a) ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Proof f -> a -> Map (Proof f) a -> Map (Proof f) a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Proof f
p a
x Map (Proof f) a
m)
              a -> StateT (Map (Proof f) a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

mapLemmas :: Function f => (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas :: (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas Derivation f -> Derivation f
f [Derivation f]
ds = (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation (Proof f -> Derivation f)
-> (Derivation f -> Proof f) -> Derivation f -> Derivation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Proof f) (Proof f) -> Derivation f -> Proof f
op Map (Proof f) (Proof f)
lem) [Derivation f]
ds
  where
    op :: Map (Proof f) (Proof f) -> Derivation f -> Proof f
op Map (Proof f) (Proof f)
lem = Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify (Derivation f -> Proof f)
-> (Derivation f -> Derivation f) -> Derivation f -> Proof f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Derivation f
f (Derivation f -> Derivation f)
-> (Derivation f -> Derivation f) -> Derivation f -> Derivation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
forall f.
Minimal f =>
(Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas (\Proof f
pf -> Derivation f -> Maybe (Derivation f)
forall a. a -> Maybe a
Just (Proof f -> Derivation f
forall f. Function f => Proof f -> Derivation f
simpleLemma (Map (Proof f) (Proof f)
lem Map (Proof f) (Proof f) -> Proof f -> Proof f
forall k a. Ord k => Map k a -> k -> a
Map.! Proof f
pf)))
    lem :: Map (Proof f) (Proof f)
lem = (Map (Proof f) (Proof f) -> Derivation f -> Proof f)
-> [Derivation f] -> Map (Proof f) (Proof f)
forall f a.
(Labelled f, PrettyTerm f) =>
(Map (Proof f) a -> Derivation f -> a)
-> [Derivation f] -> Map (Proof f) a
foldLemmas Map (Proof f) (Proof f) -> Derivation f -> Proof f
op [Derivation f]
ds

allLemmas :: Function f => [Derivation f] -> [Proof f]
allLemmas :: [Derivation f] -> [Proof f]
allLemmas [Derivation f]
ds =
  [Proof f] -> [Proof f]
forall a. [a] -> [a]
reverse [Proof f
p | (()
_, Proof f
p, [Proof f]
_) <- (Int -> ((), Proof f, [Proof f]))
-> [Int] -> [((), Proof f, [Proof f])]
forall a b. (a -> b) -> [a] -> [b]
map Int -> ((), Proof f, [Proof f])
vertex (Graph -> [Int]
topSort Graph
graph)]
  where
    used :: Map (Proof f) [Proof f]
used = (Map (Proof f) [Proof f] -> Derivation f -> [Proof f])
-> [Derivation f] -> Map (Proof f) [Proof f]
forall f a.
(Labelled f, PrettyTerm f) =>
(Map (Proof f) a -> Derivation f -> a)
-> [Derivation f] -> Map (Proof f) a
foldLemmas (\Map (Proof f) [Proof f]
_ Derivation f
p -> Derivation f -> [Proof f]
forall f. Derivation f -> [Proof f]
usedLemmas Derivation f
p) [Derivation f]
ds
    (Graph
graph, Int -> ((), Proof f, [Proof f])
vertex, Proof f -> Maybe Int
_) =
      [((), Proof f, [Proof f])]
-> (Graph, Int -> ((), Proof f, [Proof f]), Proof f -> Maybe Int)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Int -> (node, key, [key]), key -> Maybe Int)
graphFromEdges
        [((), Proof f
p, [Proof f]
ps) | (Proof f
p, [Proof f]
ps) <- Map (Proof f) [Proof f] -> [(Proof f, [Proof f])]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Proof f) [Proof f]
used]

unfoldLemmas :: Minimal f => (Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas :: (Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas Proof f -> Maybe (Derivation f)
lem p :: Derivation f
p@(UseLemma Proof f
q Subst f
sub) =
  case Proof f -> Maybe (Derivation f)
lem Proof f
q of
    Maybe (Derivation f)
Nothing -> Derivation f
p
    Just Derivation f
r ->
      -- Get rid of any variables that are not bound by sub
      -- (e.g., ones which only occur internally in q)
      Subst f -> Derivation f -> Derivation f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub ([Var] -> Derivation f -> Derivation f
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
eraseExcept (Subst f -> [Var]
forall f. Subst f -> [Var]
substDomain Subst f
sub) Derivation f
r)
unfoldLemmas Proof f -> Maybe (Derivation f)
lem (Symm Derivation f
p) = Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm ((Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
forall f.
Minimal f =>
(Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas Proof f -> Maybe (Derivation f)
lem Derivation f
p)
unfoldLemmas Proof f -> Maybe (Derivation f)
lem (Trans Derivation f
p Derivation f
q) = Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
trans ((Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
forall f.
Minimal f =>
(Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas Proof f -> Maybe (Derivation f)
lem Derivation f
p) ((Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
forall f.
Minimal f =>
(Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas Proof f -> Maybe (Derivation f)
lem Derivation f
q)
unfoldLemmas Proof f -> Maybe (Derivation f)
lem (Cong Fun f
f [Derivation f]
ps) = Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f ((Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map ((Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
forall f.
Minimal f =>
(Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas Proof f -> Maybe (Derivation f)
lem) [Derivation f]
ps)
unfoldLemmas Proof f -> Maybe (Derivation f)
_ Derivation f
p = Derivation f
p

lemma :: Proof f -> Subst f -> Derivation f
lemma :: Proof f -> Subst f -> Derivation f
lemma Proof f
p Subst f
sub = Proof f -> Subst f -> Derivation f
forall f. Proof f -> Subst f -> Derivation f
UseLemma Proof f
p Subst f
sub

simpleLemma :: Function f => Proof f -> Derivation f
simpleLemma :: Proof f -> Derivation f
simpleLemma Proof f
p =
  Proof f -> Subst f -> Derivation f
forall f. Proof f -> Subst f -> Derivation f
UseLemma Proof f
p (Equation f -> Subst f
forall f. Equation f -> Subst f
autoSubst (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p))

axiom :: Axiom f -> Derivation f
axiom :: Axiom f -> Derivation f
axiom ax :: Axiom f
ax@Axiom{Int
String
Equation f
axiom_eqn :: Equation f
axiom_name :: String
axiom_number :: Int
axiom_eqn :: forall f. Axiom f -> Equation f
axiom_name :: forall f. Axiom f -> String
axiom_number :: forall f. Axiom f -> Int
..} =
  Axiom f -> Subst f -> Derivation f
forall f. Axiom f -> Subst f -> Derivation f
UseAxiom Axiom f
ax (Equation f -> Subst f
forall f. Equation f -> Subst f
autoSubst Equation f
axiom_eqn)

autoSubst :: Equation f -> Subst f
autoSubst :: Equation f -> Subst f
autoSubst Equation f
eqn =
  Maybe (Subst f) -> Subst f
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Subst f) -> Subst f) -> Maybe (Subst f) -> Subst f
forall a b. (a -> b) -> a -> b
$
  [(Var, Term f)] -> Maybe (Subst f)
forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst [(Var
x, Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Var -> Builder f
forall f. Var -> Builder f
var Var
x)) | Var
x <- Equation f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Equation f
eqn]

symm :: Derivation f -> Derivation f
symm :: Derivation f -> Derivation f
symm (Refl Term f
t) = Term f -> Derivation f
forall f. Term f -> Derivation f
Refl Term f
t
symm (Symm Derivation f
p) = Derivation f
p
symm (Trans Derivation f
p Derivation f
q) = Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
trans (Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm Derivation f
q) (Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm Derivation f
p)
symm (Cong Fun f
f [Derivation f]
ps) = Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f ((Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm [Derivation f]
ps)
symm Derivation f
p = Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Symm Derivation f
p

trans :: Derivation f -> Derivation f -> Derivation f
trans :: Derivation f -> Derivation f -> Derivation f
trans Refl{} Derivation f
p = Derivation f
p
trans Derivation f
p Refl{} = Derivation f
p
trans (Trans Derivation f
p Derivation f
q) Derivation f
r =
  -- Right-associate uses of transitivity.
  -- p cannot be a Trans (if it was created with the smart
  -- constructors) but q could be.
  Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
Trans Derivation f
p (Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
trans Derivation f
q Derivation f
r)
trans Derivation f
p Derivation f
q = Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
Trans Derivation f
p Derivation f
q

cong :: Fun f -> [Derivation f] -> Derivation f
cong :: Fun f -> [Derivation f] -> Derivation f
cong Fun f
f [Derivation f]
ps =
  case [Maybe (Term f)] -> Maybe [Term f]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Derivation f -> Maybe (Term f))
-> [Derivation f] -> [Maybe (Term f)]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> Maybe (Term f)
forall f. Derivation f -> Maybe (Term f)
unRefl [Derivation f]
ps) of
    Maybe [Term f]
Nothing -> Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
Cong Fun f
f [Derivation f]
ps
    Just [Term f]
ts -> Term f -> Derivation f
forall f. Term f -> Derivation f
Refl (Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Fun (BuildFun [Term f]) -> [Term f] -> Builder (BuildFun [Term f])
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
Fun (BuildFun [Term f])
f [Term f]
ts))
  where
    unRefl :: Derivation f -> Maybe (Term f)
unRefl (Refl Term f
t) = Term f -> Maybe (Term f)
forall a. a -> Maybe a
Just Term f
t
    unRefl Derivation f
_ = Maybe (Term f)
forall a. Maybe a
Nothing

-- Transform a proof so that each step uses exactly one axiom
-- or lemma. The proof will have the following form afterwards:
--   * Trans only occurs at the outermost level and is right-associated
--   * Each Cong has exactly one non-Refl argument (no parallel rewriting)
--   * Symm only occurs innermost, i.e., next to UseLemma or UseAxiom
--   * Refl only occurs as an argument to Cong, or outermost if the
--     whole proof is a single reflexivity step
flattenDerivation :: Function f => Derivation f -> Derivation f
flattenDerivation :: Derivation f -> Derivation f
flattenDerivation Derivation f
p =
  Equation f -> [Derivation f] -> Derivation f
forall f. Equation f -> [Derivation f] -> Derivation f
fromSteps (Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)) (Derivation f -> [Derivation f]
forall f. Function f => Derivation f -> [Derivation f]
steps Derivation f
p)

-- | Simplify a derivation so that:
--   * Symm occurs innermost
--   * Trans is right-associated
--   * Each Cong has at least one non-Refl argument
--   * Refl is not used unnecessarily
simplify :: Function f => Derivation f -> Derivation f
simplify :: Derivation f -> Derivation f
simplify (Symm Derivation f
p) = Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm (Derivation f -> Derivation f
forall f. Function f => Derivation f -> Derivation f
simplify Derivation f
p)
simplify (Trans Derivation f
p Derivation f
q) = Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
trans (Derivation f -> Derivation f
forall f. Function f => Derivation f -> Derivation f
simplify Derivation f
p) (Derivation f -> Derivation f
forall f. Function f => Derivation f -> Derivation f
simplify Derivation f
q)
simplify (Cong Fun f
f [Derivation f]
ps) = Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f ((Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> Derivation f
forall f. Function f => Derivation f -> Derivation f
simplify [Derivation f]
ps)
simplify Derivation f
p
  | Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u = Term f -> Derivation f
forall f. Term f -> Derivation f
Refl Term f
t
  | Bool
otherwise = Derivation f
p
  where
    Term f
t :=: Term f
u = Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)

-- | Transform a derivation into a list of single steps.
--   Each step has the following form:
--     * Trans does not occur
--     * Symm only occurs innermost, i.e., next to UseLemma or UseAxiom
--     * Each Cong has exactly one non-Refl argument (no parallel rewriting)
--     * Refl only occurs as an argument to Cong
steps :: Function f => Derivation f -> [Derivation f]
steps :: Derivation f -> [Derivation f]
steps = Derivation f -> [Derivation f]
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
Derivation f -> [Derivation f]
steps1 (Derivation f -> [Derivation f])
-> (Derivation f -> Derivation f) -> Derivation f -> [Derivation f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Derivation f
forall f. Function f => Derivation f -> Derivation f
simplify
  where
    steps1 :: Derivation f -> [Derivation f]
steps1 p :: Derivation f
p@UseAxiom{} = [Derivation f
p]
    steps1 p :: Derivation f
p@UseLemma{} = [Derivation f
p]
    steps1 (Refl Term f
_) = []
    steps1 (Symm Derivation f
p) = (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm ([Derivation f] -> [Derivation f]
forall a. [a] -> [a]
reverse (Derivation f -> [Derivation f]
steps1 Derivation f
p))
    steps1 (Trans Derivation f
p Derivation f
q) = Derivation f -> [Derivation f]
steps1 Derivation f
p [Derivation f] -> [Derivation f] -> [Derivation f]
forall a. [a] -> [a] -> [a]
++ Derivation f -> [Derivation f]
steps1 Derivation f
q
    steps1 p :: Derivation f
p@(Cong Fun f
f [Derivation f]
qs) =
      [[Derivation f]] -> [Derivation f]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Derivation f -> Derivation f
inside Int
i) (Derivation f -> [Derivation f]
steps1 Derivation f
q) | (Int
i, Derivation f
q) <- [Int] -> [Derivation f] -> [(Int, Derivation f)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Derivation f]
qs ]
      where
        App Fun f
_ TermList f
ts :=: App Fun f
_ TermList f
us = Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)
        inside :: Int -> Derivation f -> Derivation f
inside Int
i Derivation f
p =
          Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
Cong Fun f
f ([Derivation f] -> Derivation f) -> [Derivation f] -> Derivation f
forall a b. (a -> b) -> a -> b
$
            (Term f -> Derivation f) -> [Term f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map Term f -> Derivation f
forall f. Term f -> Derivation f
Refl (Int -> [Term f] -> [Term f]
forall a. Int -> [a] -> [a]
take Int
i (TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
us)) [Derivation f] -> [Derivation f] -> [Derivation f]
forall a. [a] -> [a] -> [a]
++
            [Derivation f
p] [Derivation f] -> [Derivation f] -> [Derivation f]
forall a. [a] -> [a] -> [a]
++
            (Term f -> Derivation f) -> [Term f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map Term f -> Derivation f
forall f. Term f -> Derivation f
Refl (Int -> [Term f] -> [Term f]
forall a. Int -> [a] -> [a]
drop (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
ts))

-- | Convert a list of steps (plus the equation it is proving)
-- back to a derivation.
fromSteps :: Equation f -> [Derivation f] -> Derivation f
fromSteps :: Equation f -> [Derivation f] -> Derivation f
fromSteps (Term f
t :=: Term f
_) [] = Term f -> Derivation f
forall f. Term f -> Derivation f
Refl Term f
t
fromSteps Equation f
_ [Derivation f]
ps = (Derivation f -> Derivation f -> Derivation f)
-> [Derivation f] -> Derivation f
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
Trans [Derivation f]
ps

-- | Find all lemmas which are used in a derivation.
usedLemmas :: Derivation f -> [Proof f]
usedLemmas :: Derivation f -> [Proof f]
usedLemmas Derivation f
p = ((Proof f, Subst f) -> Proof f)
-> [(Proof f, Subst f)] -> [Proof f]
forall a b. (a -> b) -> [a] -> [b]
map (Proof f, Subst f) -> Proof f
forall a b. (a, b) -> a
fst (Derivation f -> [(Proof f, Subst f)]
forall f. Derivation f -> [(Proof f, Subst f)]
usedLemmasAndSubsts Derivation f
p)

-- | Find all lemmas which are used in a derivation,
-- together with the substitutions used.
usedLemmasAndSubsts :: Derivation f -> [(Proof f, Subst f)]
usedLemmasAndSubsts :: Derivation f -> [(Proof f, Subst f)]
usedLemmasAndSubsts Derivation f
p = Derivation f -> [(Proof f, Subst f)] -> [(Proof f, Subst f)]
forall f.
Derivation f -> [(Proof f, Subst f)] -> [(Proof f, Subst f)]
lem Derivation f
p []
  where
    lem :: Derivation f -> [(Proof f, Subst f)] -> [(Proof f, Subst f)]
lem (UseLemma Proof f
p Subst f
sub) = ((Proof f
p, Subst f
sub)(Proof f, Subst f) -> [(Proof f, Subst f)] -> [(Proof f, Subst f)]
forall a. a -> [a] -> [a]
:)
    lem (Symm Derivation f
p) = Derivation f -> [(Proof f, Subst f)] -> [(Proof f, Subst f)]
lem Derivation f
p
    lem (Trans Derivation f
p Derivation f
q) = Derivation f -> [(Proof f, Subst f)] -> [(Proof f, Subst f)]
lem Derivation f
p ([(Proof f, Subst f)] -> [(Proof f, Subst f)])
-> ([(Proof f, Subst f)] -> [(Proof f, Subst f)])
-> [(Proof f, Subst f)]
-> [(Proof f, Subst f)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> [(Proof f, Subst f)] -> [(Proof f, Subst f)]
lem Derivation f
q
    lem (Cong Fun f
_ [Derivation f]
ps) = (([(Proof f, Subst f)] -> [(Proof f, Subst f)])
 -> ([(Proof f, Subst f)] -> [(Proof f, Subst f)])
 -> [(Proof f, Subst f)]
 -> [(Proof f, Subst f)])
-> ([(Proof f, Subst f)] -> [(Proof f, Subst f)])
-> [[(Proof f, Subst f)] -> [(Proof f, Subst f)]]
-> [(Proof f, Subst f)]
-> [(Proof f, Subst f)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([(Proof f, Subst f)] -> [(Proof f, Subst f)])
-> ([(Proof f, Subst f)] -> [(Proof f, Subst f)])
-> [(Proof f, Subst f)]
-> [(Proof f, Subst f)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) [(Proof f, Subst f)] -> [(Proof f, Subst f)]
forall a. a -> a
id ((Derivation f -> [(Proof f, Subst f)] -> [(Proof f, Subst f)])
-> [Derivation f] -> [[(Proof f, Subst f)] -> [(Proof f, Subst f)]]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> [(Proof f, Subst f)] -> [(Proof f, Subst f)]
lem [Derivation f]
ps)
    lem Derivation f
_ = [(Proof f, Subst f)] -> [(Proof f, Subst f)]
forall a. a -> a
id

-- | Find all axioms which are used in a derivation.
usedAxioms :: Derivation f -> [Axiom f]
usedAxioms :: Derivation f -> [Axiom f]
usedAxioms Derivation f
p = ((Axiom f, Subst f) -> Axiom f)
-> [(Axiom f, Subst f)] -> [Axiom f]
forall a b. (a -> b) -> [a] -> [b]
map (Axiom f, Subst f) -> Axiom f
forall a b. (a, b) -> a
fst (Derivation f -> [(Axiom f, Subst f)]
forall f. Derivation f -> [(Axiom f, Subst f)]
usedAxiomsAndSubsts Derivation f
p)

-- | Find all axioms which are used in a derivation,
-- together with the substitutions used.
usedAxiomsAndSubsts :: Derivation f -> [(Axiom f, Subst f)]
usedAxiomsAndSubsts :: Derivation f -> [(Axiom f, Subst f)]
usedAxiomsAndSubsts Derivation f
p = Derivation f -> [(Axiom f, Subst f)] -> [(Axiom f, Subst f)]
forall f.
Derivation f -> [(Axiom f, Subst f)] -> [(Axiom f, Subst f)]
ax Derivation f
p []
  where
    ax :: Derivation f -> [(Axiom f, Subst f)] -> [(Axiom f, Subst f)]
ax (UseAxiom Axiom f
axiom Subst f
sub) = ((Axiom f
axiom, Subst f
sub)(Axiom f, Subst f) -> [(Axiom f, Subst f)] -> [(Axiom f, Subst f)]
forall a. a -> [a] -> [a]
:)
    ax (Symm Derivation f
p) = Derivation f -> [(Axiom f, Subst f)] -> [(Axiom f, Subst f)]
ax Derivation f
p
    ax (Trans Derivation f
p Derivation f
q) = Derivation f -> [(Axiom f, Subst f)] -> [(Axiom f, Subst f)]
ax Derivation f
p ([(Axiom f, Subst f)] -> [(Axiom f, Subst f)])
-> ([(Axiom f, Subst f)] -> [(Axiom f, Subst f)])
-> [(Axiom f, Subst f)]
-> [(Axiom f, Subst f)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> [(Axiom f, Subst f)] -> [(Axiom f, Subst f)]
ax Derivation f
q
    ax (Cong Fun f
_ [Derivation f]
ps) = (([(Axiom f, Subst f)] -> [(Axiom f, Subst f)])
 -> ([(Axiom f, Subst f)] -> [(Axiom f, Subst f)])
 -> [(Axiom f, Subst f)]
 -> [(Axiom f, Subst f)])
-> ([(Axiom f, Subst f)] -> [(Axiom f, Subst f)])
-> [[(Axiom f, Subst f)] -> [(Axiom f, Subst f)]]
-> [(Axiom f, Subst f)]
-> [(Axiom f, Subst f)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([(Axiom f, Subst f)] -> [(Axiom f, Subst f)])
-> ([(Axiom f, Subst f)] -> [(Axiom f, Subst f)])
-> [(Axiom f, Subst f)]
-> [(Axiom f, Subst f)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) [(Axiom f, Subst f)] -> [(Axiom f, Subst f)]
forall a. a -> a
id ((Derivation f -> [(Axiom f, Subst f)] -> [(Axiom f, Subst f)])
-> [Derivation f] -> [[(Axiom f, Subst f)] -> [(Axiom f, Subst f)]]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> [(Axiom f, Subst f)] -> [(Axiom f, Subst f)]
ax [Derivation f]
ps)
    ax Derivation f
_ = [(Axiom f, Subst f)] -> [(Axiom f, Subst f)]
forall a. a -> a
id

-- | Find all ground instances of axioms which are used in the
-- expanded form of a derivation (no lemmas).
groundAxiomsAndSubsts :: Function f => Derivation f -> Map (Axiom f) (Set (Subst f))
groundAxiomsAndSubsts :: Derivation f -> Map (Axiom f) (Set (Subst f))
groundAxiomsAndSubsts Derivation f
p = Map (Proof f) (Map (Axiom f) (Set (Subst f)))
-> Derivation f -> Map (Axiom f) (Set (Subst f))
forall f.
Minimal f =>
Map (Proof f) (Map (Axiom f) (Set (Subst f)))
-> Derivation f -> Map (Axiom f) (Set (Subst f))
ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem Derivation f
p
  where
    lem :: Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem = (Map (Proof f) (Map (Axiom f) (Set (Subst f)))
 -> Derivation f -> Map (Axiom f) (Set (Subst f)))
-> [Derivation f] -> Map (Proof f) (Map (Axiom f) (Set (Subst f)))
forall f a.
(Labelled f, PrettyTerm f) =>
(Map (Proof f) a -> Derivation f -> a)
-> [Derivation f] -> Map (Proof f) a
foldLemmas Map (Proof f) (Map (Axiom f) (Set (Subst f)))
-> Derivation f -> Map (Axiom f) (Set (Subst f))
forall f.
Minimal f =>
Map (Proof f) (Map (Axiom f) (Set (Subst f)))
-> Derivation f -> Map (Axiom f) (Set (Subst f))
ax [Derivation f
p]

    ax :: Map (Proof f) (Map (Axiom f) (Set (Subst f)))
-> Derivation f -> Map (Axiom f) (Set (Subst f))
ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
_ (UseAxiom Axiom f
axiom Subst f
sub) =
      Axiom f -> Set (Subst f) -> Map (Axiom f) (Set (Subst f))
forall k a. k -> a -> Map k a
Map.singleton Axiom f
axiom (Subst f -> Set (Subst f)
forall a. a -> Set a
Set.singleton Subst f
sub)
    ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem (UseLemma Proof f
lemma Subst f
sub) =
      (Set (Subst f) -> Set (Subst f))
-> Map (Axiom f) (Set (Subst f)) -> Map (Axiom f) (Set (Subst f))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Subst f -> Subst f) -> Set (Subst f) -> Set (Subst f)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Subst f -> Subst f
substAndErase) (Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem Map (Proof f) (Map (Axiom f) (Set (Subst f)))
-> Proof f -> Map (Axiom f) (Set (Subst f))
forall k a. Ord k => Map k a -> k -> a
Map.! Proof f
lemma)
      where
        substAndErase :: Subst f -> Subst f
substAndErase Subst f
sub' =
          [Var] -> Subst f -> Subst f
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
eraseExcept (Subst f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Subst f
sub) (Subst f -> Subst f -> Subst f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Subst f
sub')
    ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem (Symm Derivation f
p) = Map (Proof f) (Map (Axiom f) (Set (Subst f)))
-> Derivation f -> Map (Axiom f) (Set (Subst f))
ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem Derivation f
p
    ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem (Trans Derivation f
p Derivation f
q) = (Set (Subst f) -> Set (Subst f) -> Set (Subst f))
-> Map (Axiom f) (Set (Subst f))
-> Map (Axiom f) (Set (Subst f))
-> Map (Axiom f) (Set (Subst f))
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set (Subst f) -> Set (Subst f) -> Set (Subst f)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map (Proof f) (Map (Axiom f) (Set (Subst f)))
-> Derivation f -> Map (Axiom f) (Set (Subst f))
ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem Derivation f
p) (Map (Proof f) (Map (Axiom f) (Set (Subst f)))
-> Derivation f -> Map (Axiom f) (Set (Subst f))
ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem Derivation f
q)
    ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem (Cong Fun f
_ [Derivation f]
ps) = (Set (Subst f) -> Set (Subst f) -> Set (Subst f))
-> [Map (Axiom f) (Set (Subst f))] -> Map (Axiom f) (Set (Subst f))
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith Set (Subst f) -> Set (Subst f) -> Set (Subst f)
forall a. Ord a => Set a -> Set a -> Set a
Set.union ((Derivation f -> Map (Axiom f) (Set (Subst f)))
-> [Derivation f] -> [Map (Axiom f) (Set (Subst f))]
forall a b. (a -> b) -> [a] -> [b]
map (Map (Proof f) (Map (Axiom f) (Set (Subst f)))
-> Derivation f -> Map (Axiom f) (Set (Subst f))
ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
lem) [Derivation f]
ps)
    ax Map (Proof f) (Map (Axiom f) (Set (Subst f)))
_ Derivation f
_ = Map (Axiom f) (Set (Subst f))
forall k a. Map k a
Map.empty

eliminateDefinitionsFromGoal :: Function f => [Axiom f] -> ProvedGoal f -> ProvedGoal f
eliminateDefinitionsFromGoal :: [Axiom f] -> ProvedGoal f -> ProvedGoal f
eliminateDefinitionsFromGoal [Axiom f]
axioms ProvedGoal f
pg =
  ProvedGoal f
pg {
    pg_proof :: Proof f
pg_proof = Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify ([Axiom f] -> Derivation f -> Derivation f
forall f. Function f => [Axiom f] -> Derivation f -> Derivation f
eliminateDefinitions [Axiom f]
axioms (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation (ProvedGoal f -> Proof f
forall f. ProvedGoal f -> Proof f
pg_proof ProvedGoal f
pg))) }

eliminateDefinitions :: Function f => [Axiom f] -> Derivation f -> Derivation f
eliminateDefinitions :: [Axiom f] -> Derivation f -> Derivation f
eliminateDefinitions [] Derivation f
p = Derivation f
p
eliminateDefinitions [Axiom f]
axioms Derivation f
p = [Derivation f] -> Derivation f
forall a. [a] -> a
head ((Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall f.
Function f =>
(Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas Derivation f -> Derivation f
elim [Derivation f
p])
  where
    elim :: Derivation f -> Derivation f
elim (UseAxiom Axiom f
axiom Subst f
sub)
      | Axiom f
axiom Axiom f -> Set (Axiom f) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Axiom f)
axSet =
        Term f -> Derivation f
forall f. Term f -> Derivation f
Refl (Term f -> Term f
term (Subst f -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub (Equation f -> Term f
forall f. Equation f -> Term f
eqn_rhs (Axiom f -> Equation f
forall f. Axiom f -> Equation f
axiom_eqn Axiom f
axiom))))
      | Bool
otherwise = Axiom f -> Subst f -> Derivation f
forall f. Axiom f -> Subst f -> Derivation f
UseAxiom Axiom f
axiom (Subst f -> Subst f
elimSubst Subst f
sub)
    elim (UseLemma Proof f
lemma Subst f
sub) =
      Proof f -> Subst f -> Derivation f
forall f. Proof f -> Subst f -> Derivation f
UseLemma Proof f
lemma (Subst f -> Subst f
elimSubst Subst f
sub)
    elim (Refl Term f
t) = Term f -> Derivation f
forall f. Term f -> Derivation f
Refl (Term f -> Term f
term Term f
t)
    elim (Symm Derivation f
p) = Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Symm (Derivation f -> Derivation f
elim Derivation f
p)
    elim (Trans Derivation f
p Derivation f
q) = Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
Trans (Derivation f -> Derivation f
elim Derivation f
p) (Derivation f -> Derivation f
elim Derivation f
q)
    elim (Cong Fun f
f [Derivation f]
ps) =
      case Term f -> Maybe (Term f, Subst f)
find (Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Fun (BuildFun [Builder f])
-> [Builder f] -> Builder (BuildFun [Builder f])
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
Fun (BuildFun [Builder f])
f ((Var -> Builder f) -> [Var] -> [Builder f]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Builder f
forall f. Var -> Builder f
var [Var]
vs))) of
        Maybe (Term f, Subst f)
Nothing -> Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
Cong Fun f
f ((Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> Derivation f
elim [Derivation f]
ps)
        Just (Term f
rhs, Subst IntMap (TermList f)
sub) ->
          let proof :: TermList f -> Derivation f
proof (Cons (Var (V Int
x)) TermList f
Empty) = [Derivation f]
qs [Derivation f] -> Int -> Derivation f
forall a. [a] -> Int -> a
!! Int
x in
          IntMap (Derivation f) -> Term f -> Derivation f
forall f. IntMap (Derivation f) -> Term f -> Derivation f
replace (TermList f -> Derivation f
proof (TermList f -> Derivation f)
-> IntMap (TermList f) -> IntMap (Derivation f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap (TermList f)
sub) Term f
rhs
      where
        vs :: [Var]
vs = (Int -> Var) -> [Int] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Var
V [Int
0..[Derivation f] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Derivation f]
psInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
        qs :: [Derivation f]
qs = (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map (Proof f -> Derivation f
forall f. Function f => Proof f -> Derivation f
simpleLemma (Proof f -> Derivation f)
-> (Derivation f -> Proof f) -> Derivation f -> Derivation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify (Derivation f -> Proof f)
-> (Derivation f -> Derivation f) -> Derivation f -> Proof f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Derivation f
elim) [Derivation f]
ps -- avoid duplicating proofs of ts

    elimSubst :: Subst f -> Subst f
elimSubst (Subst IntMap (TermList f)
sub) = IntMap (TermList f) -> Subst f
forall f. IntMap (TermList f) -> Subst f
Subst (Term f -> TermList f
forall f. Term f -> TermList f
singleton (Term f -> TermList f)
-> (Term f -> Term f) -> Term f -> TermList f
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f -> Term f
term (Term f -> TermList f)
-> (TermList f -> Term f) -> TermList f -> TermList f
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermList f -> Term f
forall f. TermList f -> Term f
unsingleton (TermList f -> TermList f)
-> IntMap (TermList f) -> IntMap (TermList f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap (TermList f)
sub)
      where
        unsingleton :: TermList f -> Term f
unsingleton (Cons Term f
t TermList f
Empty) = Term f
t

    term :: Term f -> Term f
term = Builder f -> Term f
forall a. Build a => a -> Term (BuildFun a)
build (Builder f -> Term f) -> (Term f -> Builder f) -> Term f -> Term f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> Builder f
term'
    term' :: Term f -> Builder f
term' (Var Var
x) = Var -> Builder f
forall f. Var -> Builder f
var Var
x
    term' t :: Term f
t@(App Fun f
f TermList f
ts) =
      case Term f -> Maybe (Term f, Subst f)
find Term f
t of
        Maybe (Term f, Subst f)
Nothing -> Fun (BuildFun [Builder f])
-> [Builder f] -> Builder (BuildFun [Builder f])
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
Fun (BuildFun [Builder f])
f ((Term f -> Builder f) -> [Term f] -> [Builder f]
forall a b. (a -> b) -> [a] -> [b]
map Term f -> Builder f
term' (TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
ts))
        Just (Term f
rhs, Subst f
sub) ->
          Term f -> Builder f
term' (Subst f -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
rhs)

    find :: Term f -> Maybe (Term f, Subst f)
find Term f
t =
      [(Term f, Subst f)] -> Maybe (Term f, Subst f)
forall a. [a] -> Maybe a
listToMaybe ([(Term f, Subst f)] -> Maybe (Term f, Subst f))
-> [(Term f, Subst f)] -> Maybe (Term f, Subst f)
forall a b. (a -> b) -> a -> b
$ do
        (Subst f
_, UseAxiom Axiom{axiom_eqn :: forall f. Axiom f -> Equation f
axiom_eqn = Term f
l :=: Term f
r} Subst f
_) <- Term f -> Index f (Derivation f) -> [(Subst f, Derivation f)]
forall f a. Term f -> Index f a -> [(Subst f, a)]
Index.matches Term f
t Index f (Derivation f)
idx
        let Just Subst f
sub = Term f -> Term f -> Maybe (Subst f)
forall f. Term f -> Term f -> Maybe (Subst f)
match Term f
l Term f
t
        (Term f, Subst f) -> [(Term f, Subst f)]
forall (m :: * -> *) a. Monad m => a -> m a
return (Term f
r, Subst f
sub)

    replace :: IntMap (Derivation f) -> Term f -> Derivation f
replace IntMap (Derivation f)
sub (Var (V Int
x)) =
      Derivation f -> Int -> IntMap (Derivation f) -> Derivation f
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault Derivation f
forall a. HasCallStack => a
undefined Int
x IntMap (Derivation f)
sub
    replace IntMap (Derivation f)
sub (App Fun f
f TermList f
ts) =
      Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f ((Term f -> Derivation f) -> [Term f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap (Derivation f) -> Term f -> Derivation f
replace IntMap (Derivation f)
sub) (TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
ts))

    axSet :: Set (Axiom f)
axSet = [Axiom f] -> Set (Axiom f)
forall a. Ord a => [a] -> Set a
Set.fromList [Axiom f]
axioms
    idx :: Index f (Derivation f)
idx = [(Term f, Derivation f)] -> Index f (Derivation f)
forall a f.
(Symbolic a, ConstantOf a ~ f) =>
[(Term f, a)] -> Index f a
Index.fromList [(Equation f -> Term f
forall f. Equation f -> Term f
eqn_lhs (Axiom f -> Equation f
forall f. Axiom f -> Equation f
axiom_eqn Axiom f
ax), Axiom f -> Derivation f
forall f. Axiom f -> Derivation f
axiom Axiom f
ax) | Axiom f
ax <- [Axiom f]
axioms]

-- | Applies a derivation at a particular path in a term.
congPath :: [Int] -> Term f -> Derivation f -> Derivation f
congPath :: [Int] -> Term f -> Derivation f -> Derivation f
congPath [] Term f
_ Derivation f
p = Derivation f
p
congPath (Int
n:[Int]
ns) (App Fun f
f TermList f
t) Derivation f
p | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Term f] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term f]
ts =
  Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f ([Derivation f] -> Derivation f) -> [Derivation f] -> Derivation f
forall a b. (a -> b) -> a -> b
$
    (Term f -> Derivation f) -> [Term f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map Term f -> Derivation f
forall f. Term f -> Derivation f
Refl (Int -> [Term f] -> [Term f]
forall a. Int -> [a] -> [a]
take Int
n [Term f]
ts) [Derivation f] -> [Derivation f] -> [Derivation f]
forall a. [a] -> [a] -> [a]
++
    [[Int] -> Term f -> Derivation f -> Derivation f
forall f. [Int] -> Term f -> Derivation f -> Derivation f
congPath [Int]
ns ([Term f]
ts [Term f] -> Int -> Term f
forall a. [a] -> Int -> a
!! Int
n) Derivation f
p] [Derivation f] -> [Derivation f] -> [Derivation f]
forall a. [a] -> [a] -> [a]
++
    (Term f -> Derivation f) -> [Term f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map Term f -> Derivation f
forall f. Term f -> Derivation f
Refl (Int -> [Term f] -> [Term f]
forall a. Int -> [a] -> [a]
drop (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [Term f]
ts)
  where
    ts :: [Term f]
ts = TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
t
congPath [Int]
_ Term f
_ Derivation f
_ = String -> Derivation f
forall a. HasCallStack => String -> a
error String
"bad path"

----------------------------------------------------------------------
-- Pretty-printing of proofs.
----------------------------------------------------------------------

-- | Options for proof presentation.
data Config f =
  Config {
    -- | Never inline lemmas.
    Config f -> Bool
cfg_all_lemmas :: !Bool,
    -- | Inline all lemmas.
    Config f -> Bool
cfg_no_lemmas :: !Bool,
    -- | Make the proof ground.
    Config f -> Bool
cfg_ground_proof :: !Bool,
    -- | Print out explicit substitutions.
    Config f -> Bool
cfg_show_instances :: !Bool,
    -- | Print out proofs in colour.
    Config f -> Bool
cfg_use_colour :: !Bool,
    -- | Print out which instances of some axioms were used.
    Config f -> Axiom f -> Bool
cfg_show_uses_of_axioms :: Axiom f -> Bool }

-- | The default configuration.
defaultConfig :: Config f
defaultConfig :: Config f
defaultConfig =
  Config :: forall f.
Bool
-> Bool -> Bool -> Bool -> Bool -> (Axiom f -> Bool) -> Config f
Config {
    cfg_all_lemmas :: Bool
cfg_all_lemmas = Bool
False,
    cfg_no_lemmas :: Bool
cfg_no_lemmas = Bool
False,
    cfg_ground_proof :: Bool
cfg_ground_proof = Bool
False,
    cfg_show_instances :: Bool
cfg_show_instances = Bool
False,
    cfg_use_colour :: Bool
cfg_use_colour = Bool
False,
    cfg_show_uses_of_axioms :: Axiom f -> Bool
cfg_show_uses_of_axioms = Bool -> Axiom f -> Bool
forall a b. a -> b -> a
const Bool
False }

-- | A proof, with all axioms and lemmas explicitly listed.
data Presentation f =
  Presentation {
    -- | The used axioms.
    Presentation f -> [Axiom f]
pres_axioms :: [Axiom f],
    -- | The used lemmas.
    Presentation f -> [Proof f]
pres_lemmas :: [Proof f],
    -- | The goals proved.
    Presentation f -> [ProvedGoal f]
pres_goals  :: [ProvedGoal f] }
  deriving Int -> Presentation f -> ShowS
[Presentation f] -> ShowS
Presentation f -> String
(Int -> Presentation f -> ShowS)
-> (Presentation f -> String)
-> ([Presentation f] -> ShowS)
-> Show (Presentation f)
forall f. (Labelled f, Show f) => Int -> Presentation f -> ShowS
forall f. (Labelled f, Show f) => [Presentation f] -> ShowS
forall f. (Labelled f, Show f) => Presentation f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Presentation f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Presentation f] -> ShowS
show :: Presentation f -> String
$cshow :: forall f. (Labelled f, Show f) => Presentation f -> String
showsPrec :: Int -> Presentation f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Presentation f -> ShowS
Show

-- Note: only the pg_proof field should be trusted!
-- The remaining fields are for information only.
data ProvedGoal f =
  ProvedGoal {
    ProvedGoal f -> Int
pg_number  :: Int,
    ProvedGoal f -> String
pg_name    :: String,
    ProvedGoal f -> Proof f
pg_proof   :: Proof f,

    -- Extra fields for existentially-quantified goals, giving the original goal
    -- and the existential witness. These fields are not verified. If you want
    -- to check them, use checkProvedGoal.
    --
    -- In general, subst pg_witness_hint pg_goal_hint == equation pg_proof.
    -- For non-existential goals, pg_goal_hint == equation pg_proof
    -- and pg_witness_hint is the empty substitution.
    ProvedGoal f -> Equation f
pg_goal_hint    :: Equation f,
    ProvedGoal f -> Subst f
pg_witness_hint :: Subst f }
  deriving Int -> ProvedGoal f -> ShowS
[ProvedGoal f] -> ShowS
ProvedGoal f -> String
(Int -> ProvedGoal f -> ShowS)
-> (ProvedGoal f -> String)
-> ([ProvedGoal f] -> ShowS)
-> Show (ProvedGoal f)
forall f. (Labelled f, Show f) => Int -> ProvedGoal f -> ShowS
forall f. (Labelled f, Show f) => [ProvedGoal f] -> ShowS
forall f. (Labelled f, Show f) => ProvedGoal f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProvedGoal f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [ProvedGoal f] -> ShowS
show :: ProvedGoal f -> String
$cshow :: forall f. (Labelled f, Show f) => ProvedGoal f -> String
showsPrec :: Int -> ProvedGoal f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> ProvedGoal f -> ShowS
Show

-- | Construct a @ProvedGoal@.
provedGoal :: Int -> String -> Proof f -> ProvedGoal f
provedGoal :: Int -> String -> Proof f -> ProvedGoal f
provedGoal Int
number String
name Proof f
proof =
  ProvedGoal :: forall f.
Int -> String -> Proof f -> Equation f -> Subst f -> ProvedGoal f
ProvedGoal {
    pg_number :: Int
pg_number = Int
number,
    pg_name :: String
pg_name = String
name,
    pg_proof :: Proof f
pg_proof = Proof f
proof,
    pg_goal_hint :: Equation f
pg_goal_hint = Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
proof,
    pg_witness_hint :: Subst f
pg_witness_hint = Subst f
forall f. Subst f
emptySubst }

-- | Check that pg_goal/pg_witness match up with pg_proof.
checkProvedGoal :: Function f => ProvedGoal f -> ProvedGoal f
checkProvedGoal :: ProvedGoal f -> ProvedGoal f
checkProvedGoal pg :: ProvedGoal f
pg@ProvedGoal{Int
String
Subst f
Equation f
Proof f
pg_witness_hint :: Subst f
pg_goal_hint :: Equation f
pg_proof :: Proof f
pg_name :: String
pg_number :: Int
pg_witness_hint :: forall f. ProvedGoal f -> Subst f
pg_goal_hint :: forall f. ProvedGoal f -> Equation f
pg_name :: forall f. ProvedGoal f -> String
pg_number :: forall f. ProvedGoal f -> Int
pg_proof :: forall f. ProvedGoal f -> Proof f
..}
  | Subst f -> Equation f -> Equation f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
pg_witness_hint Equation f
pg_goal_hint Equation f -> Equation f -> Bool
forall a. Eq a => a -> a -> Bool
== Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
pg_proof =
    ProvedGoal f
pg
  | Bool
otherwise =
    String -> ProvedGoal f
forall a. HasCallStack => String -> a
error (String -> ProvedGoal f) -> String -> ProvedGoal f
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$
      String -> Doc
text String
"Invalid ProvedGoal!" Doc -> Doc -> Doc
$$
      String -> Doc
text String
"Claims to prove" Doc -> Doc -> Doc
<+> Equation f -> Doc
forall a. Pretty a => a -> Doc
pPrint Equation f
pg_goal_hint Doc -> Doc -> Doc
$$
      String -> Doc
text String
"with witness" Doc -> Doc -> Doc
<+> Subst f -> Doc
forall a. Pretty a => a -> Doc
pPrint Subst f
pg_witness_hint Doc -> Doc -> Doc
<#> String -> Doc
text String
"," Doc -> Doc -> Doc
$$
      String -> Doc
text String
"but actually proves" Doc -> Doc -> Doc
<+> Equation f -> Doc
forall a. Pretty a => a -> Doc
pPrint (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
pg_proof)

instance Function f => Pretty (Presentation f) where
  pPrint :: Presentation f -> Doc
pPrint = Config f -> Presentation f -> Doc
forall f. Function f => Config f -> Presentation f -> Doc
pPrintPresentation Config f
forall f. Config f
defaultConfig

-- | Simplify and present a proof.
present :: Function f => Config f -> [ProvedGoal f] -> Presentation f
present :: Config f -> [ProvedGoal f] -> Presentation f
present config :: Config f
config@Config{Bool
Axiom f -> Bool
cfg_show_uses_of_axioms :: Axiom f -> Bool
cfg_use_colour :: Bool
cfg_show_instances :: Bool
cfg_ground_proof :: Bool
cfg_no_lemmas :: Bool
cfg_all_lemmas :: Bool
cfg_show_uses_of_axioms :: forall f. Config f -> Axiom f -> Bool
cfg_use_colour :: forall f. Config f -> Bool
cfg_show_instances :: forall f. Config f -> Bool
cfg_ground_proof :: forall f. Config f -> Bool
cfg_no_lemmas :: forall f. Config f -> Bool
cfg_all_lemmas :: forall f. Config f -> Bool
..} [ProvedGoal f]
goals =
  [Axiom f] -> [Proof f] -> [ProvedGoal f] -> Presentation f
forall f.
[Axiom f] -> [Proof f] -> [ProvedGoal f] -> Presentation f
Presentation [Axiom f]
axioms [Proof f]
lemmas [ProvedGoal f]
goals'
  where
    ps :: [Derivation f]
ps =
      (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall f.
Function f =>
(Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas Derivation f -> Derivation f
forall f. Function f => Derivation f -> Derivation f
flattenDerivation ([Derivation f] -> [Derivation f])
-> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> a -> b
$
      Config f -> [Derivation f] -> [Derivation f]
forall f.
Function f =>
Config f -> [Derivation f] -> [Derivation f]
simplifyProof Config f
config ([Derivation f] -> [Derivation f])
-> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> a -> b
$ (ProvedGoal f -> Derivation f) -> [ProvedGoal f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation (Proof f -> Derivation f)
-> (ProvedGoal f -> Proof f) -> ProvedGoal f -> Derivation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProvedGoal f -> Proof f
forall f. ProvedGoal f -> Proof f
pg_proof) [ProvedGoal f]
goals

    goals' :: [ProvedGoal f]
goals' =
      [ ProvedGoal f -> ProvedGoal f
forall f. Function f => ProvedGoal f -> ProvedGoal f
decodeGoal (ProvedGoal f
goal{pg_proof :: Proof f
pg_proof = Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
p})
      | (ProvedGoal f
goal, Derivation f
p) <- [ProvedGoal f] -> [Derivation f] -> [(ProvedGoal f, Derivation f)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ProvedGoal f]
goals [Derivation f]
ps ]

    axioms :: [Axiom f]
axioms = [Axiom f] -> [Axiom f]
forall a. Ord a => [a] -> [a]
usort ([Axiom f] -> [Axiom f]) -> [Axiom f] -> [Axiom f]
forall a b. (a -> b) -> a -> b
$
      (ProvedGoal f -> [Axiom f]) -> [ProvedGoal f] -> [Axiom f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Derivation f -> [Axiom f]
forall f. Derivation f -> [Axiom f]
usedAxioms (Derivation f -> [Axiom f])
-> (ProvedGoal f -> Derivation f) -> ProvedGoal f -> [Axiom f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation (Proof f -> Derivation f)
-> (ProvedGoal f -> Proof f) -> ProvedGoal f -> Derivation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProvedGoal f -> Proof f
forall f. ProvedGoal f -> Proof f
pg_proof) [ProvedGoal f]
goals' [Axiom f] -> [Axiom f] -> [Axiom f]
forall a. [a] -> [a] -> [a]
++
      (Proof f -> [Axiom f]) -> [Proof f] -> [Axiom f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Derivation f -> [Axiom f]
forall f. Derivation f -> [Axiom f]
usedAxioms (Derivation f -> [Axiom f])
-> (Proof f -> Derivation f) -> Proof f -> [Axiom f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation) [Proof f]
lemmas

    lemmas :: [Proof f]
lemmas = [Derivation f] -> [Proof f]
forall f. Function f => [Derivation f] -> [Proof f]
allLemmas ((ProvedGoal f -> Derivation f) -> [ProvedGoal f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation (Proof f -> Derivation f)
-> (ProvedGoal f -> Proof f) -> ProvedGoal f -> Derivation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProvedGoal f -> Proof f
forall f. ProvedGoal f -> Proof f
pg_proof) [ProvedGoal f]
goals')

groundProof :: Function f => [Derivation f] -> [Derivation f]
groundProof :: [Derivation f] -> [Derivation f]
groundProof [Derivation f]
ds
  | (Proof f -> Bool) -> [Proof f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Equation f -> Bool
forall a. Symbolic a => a -> Bool
isGround (Equation f -> Bool) -> (Proof f -> Equation f) -> Proof f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof f -> Equation f
forall f. Proof f -> Equation f
equation) ([Derivation f] -> [Proof f]
forall f. Function f => [Derivation f] -> [Proof f]
allLemmas [Derivation f]
ds) = [Derivation f]
ds
  | Bool
otherwise = [Derivation f] -> [Derivation f]
forall f. Function f => [Derivation f] -> [Derivation f]
groundProof ((Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall f.
Function f =>
(Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas Derivation f -> Derivation f
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
Derivation f -> Derivation f
f [Derivation f]
ds)
  where
    f :: Derivation f -> Derivation f
f (UseLemma Proof f
lemma Subst f
sub) =
      Proof f -> Derivation f
forall f. Function f => Proof f -> Derivation f
simpleLemma (Proof f -> Derivation f) -> Proof f -> Derivation f
forall a b. (a -> b) -> a -> b
$ Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify (Derivation f -> Proof f) -> Derivation f -> Proof f
forall a b. (a -> b) -> a -> b
$
      [Var] -> Derivation f -> Derivation f
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
eraseExcept (Subst f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Subst f
sub) (Derivation f -> Derivation f) -> Derivation f -> Derivation f
forall a b. (a -> b) -> a -> b
$
      Subst f -> Derivation f -> Derivation f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub (Derivation f -> Derivation f) -> Derivation f -> Derivation f
forall a b. (a -> b) -> a -> b
$
      Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
lemma
    f p :: Derivation f
p@UseAxiom{} = Derivation f
p
    f p :: Derivation f
p@Refl{} = Derivation f
p
    f (Symm Derivation f
p) = Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Symm (Derivation f -> Derivation f
f Derivation f
p)
    f (Trans Derivation f
p Derivation f
q) = Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
Trans (Derivation f -> Derivation f
f Derivation f
p) (Derivation f -> Derivation f
f Derivation f
q)
    f (Cong Fun f
fun [Derivation f]
ps) = Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
Cong Fun f
fun ((Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> Derivation f
f [Derivation f]
ps)

simplifyProof :: Function f => Config f -> [Derivation f] -> [Derivation f]
simplifyProof :: Config f -> [Derivation f] -> [Derivation f]
simplifyProof config :: Config f
config@Config{Bool
Axiom f -> Bool
cfg_show_uses_of_axioms :: Axiom f -> Bool
cfg_use_colour :: Bool
cfg_show_instances :: Bool
cfg_ground_proof :: Bool
cfg_no_lemmas :: Bool
cfg_all_lemmas :: Bool
cfg_show_uses_of_axioms :: forall f. Config f -> Axiom f -> Bool
cfg_use_colour :: forall f. Config f -> Bool
cfg_show_instances :: forall f. Config f -> Bool
cfg_ground_proof :: forall f. Config f -> Bool
cfg_no_lemmas :: forall f. Config f -> Bool
cfg_all_lemmas :: forall f. Config f -> Bool
..} [Derivation f]
goals =
  [Derivation f] -> [Derivation f]
forall f. Function f => [Derivation f] -> [Derivation f]
canonicaliseLemmas (([Derivation f] -> ([Derivation f], [(Equation f, Derivation f)]))
-> ([Derivation f] -> [Derivation f])
-> [Derivation f]
-> [Derivation f]
forall b a. Eq b => (a -> b) -> (a -> a) -> a -> a
fixpointOn [Derivation f] -> ([Derivation f], [(Equation f, Derivation f)])
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
[Derivation f] -> ([Derivation f], [(Equation f, Derivation f)])
key [Derivation f] -> [Derivation f]
simp' (([Derivation f] -> ([Derivation f], [(Equation f, Derivation f)]))
-> ([Derivation f] -> [Derivation f])
-> [Derivation f]
-> [Derivation f]
forall b a. Eq b => (a -> b) -> (a -> a) -> a -> a
fixpointOn [Derivation f] -> ([Derivation f], [(Equation f, Derivation f)])
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
[Derivation f] -> ([Derivation f], [(Equation f, Derivation f)])
key [Derivation f] -> [Derivation f]
simp [Derivation f]
goals))
  where
    simpCore :: [Derivation f] -> [Derivation f]
simpCore =
      ([Derivation f] -> [Derivation f]
forall f. Function f => [Derivation f] -> [Derivation f]
inlineUsedOnceLemmas ([Derivation f] -> [Derivation f])
-> Bool -> [Derivation f] -> [Derivation f]
forall a. (a -> a) -> Bool -> a -> a
`onlyIf` Bool -> Bool
not Bool
cfg_all_lemmas) ([Derivation f] -> [Derivation f])
-> ([Derivation f] -> [Derivation f])
-> [Derivation f]
-> [Derivation f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      Config f -> [Derivation f] -> [Derivation f]
forall f.
Function f =>
Config f -> [Derivation f] -> [Derivation f]
inlineTrivialLemmas Config f
config ([Derivation f] -> [Derivation f])
-> ([Derivation f] -> [Derivation f])
-> [Derivation f]
-> [Derivation f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      [Derivation f] -> [Derivation f]
forall f. Function f => [Derivation f] -> [Derivation f]
tightenProof

    simp :: [Derivation f] -> [Derivation f]
simp = [Derivation f] -> [Derivation f]
simpCore ([Derivation f] -> [Derivation f])
-> ([Derivation f] -> [Derivation f])
-> [Derivation f]
-> [Derivation f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Derivation f] -> [Derivation f]
forall f. Function f => [Derivation f] -> [Derivation f]
generaliseProof
    -- generaliseProof undoes the effect of groundProof!
    -- But we still want to run generaliseProof first, to simplify the proof
    simp' :: [Derivation f] -> [Derivation f]
simp' = ([Derivation f] -> [Derivation f]
simpCore ([Derivation f] -> [Derivation f])
-> ([Derivation f] -> [Derivation f])
-> [Derivation f]
-> [Derivation f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Derivation f] -> [Derivation f]
forall f. Function f => [Derivation f] -> [Derivation f]
groundProof) ([Derivation f] -> [Derivation f])
-> Bool -> [Derivation f] -> [Derivation f]
forall a. (a -> a) -> Bool -> a -> a
`onlyIf` Bool
cfg_ground_proof

    key :: [Derivation f] -> ([Derivation f], [(Equation f, Derivation f)])
key [Derivation f]
ds =
      ([Derivation f]
ds, [(Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p, Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p) | Proof f
p <- [Derivation f] -> [Proof f]
forall f. Function f => [Derivation f] -> [Proof f]
allLemmas [Derivation f]
ds])

    a -> a
pass onlyIf :: (a -> a) -> Bool -> a -> a
`onlyIf` Bool
True = a -> a
pass
    a -> a
_    `onlyIf` Bool
False = a -> a
forall a. a -> a
id

simplificationPass ::
  Function f =>
  -- A transformation on lemmas
  (Map (Proof f) (Derivation f) -> Proof f -> Derivation f) ->
  -- A transformation on goals
  (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f) ->
  [Derivation f] -> [Derivation f]
simplificationPass :: (Map (Proof f) (Derivation f) -> Proof f -> Derivation f)
-> (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> [Derivation f]
-> [Derivation f]
simplificationPass Map (Proof f) (Derivation f) -> Proof f -> Derivation f
lemma Map (Proof f) (Derivation f) -> Derivation f -> Derivation f
goal [Derivation f]
p = (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map ((Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> Map (Proof f) (Derivation f) -> Derivation f -> Derivation f
forall f t.
Minimal f =>
(Map (Proof f) (Derivation f) -> Derivation f -> t)
-> Map (Proof f) (Derivation f) -> Derivation f -> t
op Map (Proof f) (Derivation f) -> Derivation f -> Derivation f
goal Map (Proof f) (Derivation f)
lem) [Derivation f]
p
  where
    lem :: Map (Proof f) (Derivation f)
lem = (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> [Derivation f] -> Map (Proof f) (Derivation f)
forall f a.
(Labelled f, PrettyTerm f) =>
(Map (Proof f) a -> Derivation f -> a)
-> [Derivation f] -> Map (Proof f) a
foldLemmas ((Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> Map (Proof f) (Derivation f) -> Derivation f -> Derivation f
forall f t.
Minimal f =>
(Map (Proof f) (Derivation f) -> Derivation f -> t)
-> Map (Proof f) (Derivation f) -> Derivation f -> t
op (\Map (Proof f) (Derivation f)
lem -> Map (Proof f) (Derivation f) -> Proof f -> Derivation f
lemma Map (Proof f) (Derivation f)
lem (Proof f -> Derivation f)
-> (Derivation f -> Proof f) -> Derivation f -> Derivation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify)) [Derivation f]
p
    op :: (Map (Proof f) (Derivation f) -> Derivation f -> t)
-> Map (Proof f) (Derivation f) -> Derivation f -> t
op Map (Proof f) (Derivation f) -> Derivation f -> t
f Map (Proof f) (Derivation f)
lem Derivation f
p =
      Map (Proof f) (Derivation f) -> Derivation f -> t
f Map (Proof f) (Derivation f)
lem ((Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
forall f.
Minimal f =>
(Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas (\Proof f
lemma -> Derivation f -> Maybe (Derivation f)
forall a. a -> Maybe a
Just (Map (Proof f) (Derivation f)
lem Map (Proof f) (Derivation f) -> Proof f -> Derivation f
forall k a. Ord k => Map k a -> k -> a
Map.! Proof f
lemma)) Derivation f
p)

inlineTrivialLemmas :: Function f => Config f -> [Derivation f] -> [Derivation f]
inlineTrivialLemmas :: Config f -> [Derivation f] -> [Derivation f]
inlineTrivialLemmas Config{Bool
Axiom f -> Bool
cfg_show_uses_of_axioms :: Axiom f -> Bool
cfg_use_colour :: Bool
cfg_show_instances :: Bool
cfg_ground_proof :: Bool
cfg_no_lemmas :: Bool
cfg_all_lemmas :: Bool
cfg_show_uses_of_axioms :: forall f. Config f -> Axiom f -> Bool
cfg_use_colour :: forall f. Config f -> Bool
cfg_show_instances :: forall f. Config f -> Bool
cfg_ground_proof :: forall f. Config f -> Bool
cfg_no_lemmas :: forall f. Config f -> Bool
cfg_all_lemmas :: forall f. Config f -> Bool
..} =
  -- A lemma is trivial if one of the following holds:
  --   * It only has one step
  --   * It is subsumed by an earlier lemma
  --   * It has to do with $equals (for printing of the goal proof)
  --   * The option cfg_no_lemmas is true
  (Map (Proof f) (Derivation f) -> Proof f -> Derivation f)
-> (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> [Derivation f]
-> [Derivation f]
forall f.
Function f =>
(Map (Proof f) (Derivation f) -> Proof f -> Derivation f)
-> (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> [Derivation f]
-> [Derivation f]
simplificationPass Map (Proof f) (Derivation f) -> Proof f -> Derivation f
inlineTrivial ((Derivation f -> Derivation f)
-> Map (Proof f) (Derivation f) -> Derivation f -> Derivation f
forall a b. a -> b -> a
const Derivation f -> Derivation f
forall a. a -> a
id)
  where
    inlineTrivial :: Map (Proof f) (Derivation f) -> Proof f -> Derivation f
inlineTrivial Map (Proof f) (Derivation f)
lem Proof f
p
      | Proof f -> Bool
shouldInline Proof f
p = Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p
      | (Derivation f
q:[Derivation f]
_) <- Map (Proof f) (Derivation f) -> Equation f -> [Derivation f]
forall f.
Map (Proof f) (Derivation f) -> Equation f -> [Derivation f]
subsuming Map (Proof f) (Derivation f)
lem (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p) = Derivation f
q
      | Bool
otherwise = Proof f -> Derivation f
forall f. Function f => Proof f -> Derivation f
simpleLemma Proof f
p

    shouldInline :: Proof f -> Bool
shouldInline Proof f
p =
      Bool
cfg_no_lemmas Bool -> Bool -> Bool
||
      [Equation f] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Equation f -> Bool) -> [Equation f] -> [Equation f]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Equation f -> Bool) -> Equation f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation f -> Bool
forall f. Function f => Equation f -> Bool
invisible) ((Derivation f -> Equation f) -> [Derivation f] -> [Equation f]
forall a b. (a -> b) -> [a] -> [b]
map (Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Proof f -> Equation f)
-> (Derivation f -> Proof f) -> Derivation f -> Equation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify) (Derivation f -> [Derivation f]
forall f. Function f => Derivation f -> [Derivation f]
steps (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p)))) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 Bool -> Bool -> Bool
||
      (Bool -> Bool
not Bool
cfg_all_lemmas Bool -> Bool -> Bool
&&
       (Maybe (Equation f) -> Bool
forall a. Maybe a -> Bool
isJust (Term f -> Maybe (Equation f)
forall f. Function f => Term f -> Maybe (Equation f)
decodeEquality (Equation f -> Term f
forall f. Equation f -> Term f
eqn_lhs (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p))) Bool -> Bool -> Bool
||
        Maybe (Equation f) -> Bool
forall a. Maybe a -> Bool
isJust (Term f -> Maybe (Equation f)
forall f. Function f => Term f -> Maybe (Equation f)
decodeEquality (Equation f -> Term f
forall f. Equation f -> Term f
eqn_rhs (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p)))))

    subsuming :: Map (Proof f) (Derivation f) -> Equation f -> [Derivation f]
subsuming Map (Proof f) (Derivation f)
lem (Term f
t :=: Term f
u) =
      Map (Proof (ConstantOf (Derivation f))) (Derivation f)
-> Equation (ConstantOf (Derivation f)) -> [Derivation f]
forall a.
Symbolic a =>
Map (Proof (ConstantOf a)) a -> Equation (ConstantOf a) -> [a]
subsuming1 Map (Proof f) (Derivation f)
Map (Proof (ConstantOf (Derivation f))) (Derivation f)
lem (Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u) [Derivation f] -> [Derivation f] -> [Derivation f]
forall a. [a] -> [a] -> [a]
++
      (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm (Map (Proof (ConstantOf (Derivation f))) (Derivation f)
-> Equation (ConstantOf (Derivation f)) -> [Derivation f]
forall a.
Symbolic a =>
Map (Proof (ConstantOf a)) a -> Equation (ConstantOf a) -> [a]
subsuming1 Map (Proof f) (Derivation f)
Map (Proof (ConstantOf (Derivation f))) (Derivation f)
lem (Term f
u Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
t))
    subsuming1 :: Map (Proof (ConstantOf a)) a -> Equation (ConstantOf a) -> [a]
subsuming1 Map (Proof (ConstantOf a)) a
lem Equation (ConstantOf a)
eq =
      [ Subst (ConstantOf a) -> a -> a
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub a
d
      | (Proof (ConstantOf a)
q, a
d) <- Map (Proof (ConstantOf a)) a -> [(Proof (ConstantOf a), a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Proof (ConstantOf a)) a
lem,
        Subst (ConstantOf a)
sub <- Maybe (Subst (ConstantOf a)) -> [Subst (ConstantOf a)]
forall a. Maybe a -> [a]
maybeToList (Equation (ConstantOf a)
-> Equation (ConstantOf a) -> Maybe (Subst (ConstantOf a))
forall f. Equation f -> Equation f -> Maybe (Subst f)
matchEquation (Proof (ConstantOf a) -> Equation (ConstantOf a)
forall f. Proof f -> Equation f
equation Proof (ConstantOf a)
q) Equation (ConstantOf a)
eq) ]

inlineUsedOnceLemmas :: Function f => [Derivation f] -> [Derivation f]
inlineUsedOnceLemmas :: [Derivation f] -> [Derivation f]
inlineUsedOnceLemmas [Derivation f]
ds =
  -- Inline any lemma that's only used once in the proof
  (Map (Proof f) (Derivation f) -> Proof f -> Derivation f)
-> (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> [Derivation f]
-> [Derivation f]
forall f.
Function f =>
(Map (Proof f) (Derivation f) -> Proof f -> Derivation f)
-> (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> [Derivation f]
-> [Derivation f]
simplificationPass ((Proof f -> Derivation f)
-> Map (Proof f) (Derivation f) -> Proof f -> Derivation f
forall a b. a -> b -> a
const Proof f -> Derivation f
inlineOnce) ((Derivation f -> Derivation f)
-> Map (Proof f) (Derivation f) -> Derivation f -> Derivation f
forall a b. a -> b -> a
const Derivation f -> Derivation f
forall a. a -> a
id) [Derivation f]
ds
  where
    uses :: Map (Proof f) Int
uses = (Int -> Int -> Int) -> [Map (Proof f) Int] -> Map (Proof f) Int
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) ([Map (Proof f) Int] -> Map (Proof f) Int)
-> [Map (Proof f) Int] -> Map (Proof f) Int
forall a b. (a -> b) -> a -> b
$
      (Derivation f -> Map (Proof f) Int)
-> [Derivation f] -> [Map (Proof f) Int]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> Map (Proof f) Int
forall f. Derivation f -> Map (Proof f) Int
countUses [Derivation f]
ds [Map (Proof f) Int] -> [Map (Proof f) Int] -> [Map (Proof f) Int]
forall a. [a] -> [a] -> [a]
++ Map (Proof f) (Map (Proof f) Int) -> [Map (Proof f) Int]
forall k a. Map k a -> [a]
Map.elems ((Map (Proof f) (Map (Proof f) Int)
 -> Derivation f -> Map (Proof f) Int)
-> [Derivation f] -> Map (Proof f) (Map (Proof f) Int)
forall f a.
(Labelled f, PrettyTerm f) =>
(Map (Proof f) a -> Derivation f -> a)
-> [Derivation f] -> Map (Proof f) a
foldLemmas ((Derivation f -> Map (Proof f) Int)
-> Map (Proof f) (Map (Proof f) Int)
-> Derivation f
-> Map (Proof f) Int
forall a b. a -> b -> a
const Derivation f -> Map (Proof f) Int
forall f. Derivation f -> Map (Proof f) Int
countUses) [Derivation f]
ds)

    countUses :: Derivation f -> Map (Proof f) Int
countUses Derivation f
p =
      (Int -> Int -> Int) -> [(Proof f, Int)] -> Map (Proof f) Int
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) ([Proof f] -> [Int] -> [(Proof f, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Derivation f -> [Proof f]
forall f. Derivation f -> [Proof f]
usedLemmas Derivation f
p) (Int -> [Int]
forall a. a -> [a]
repeat (Int
1 :: Int)))

    inlineOnce :: Proof f -> Derivation f
inlineOnce Proof f
p
      | Proof f -> Bool
usedOnce Proof f
p = Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p
      | Bool
otherwise = Proof f -> Derivation f
forall f. Function f => Proof f -> Derivation f
simpleLemma Proof f
p
      where
        usedOnce :: Proof f -> Bool
usedOnce Proof f
p =
          case Proof f -> Map (Proof f) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Proof f
p Map (Proof f) Int
uses of
            Just Int
1 -> Bool
True
            Maybe Int
_ -> Bool
False

tightenProof :: Function f => [Derivation f] -> [Derivation f]
tightenProof :: [Derivation f] -> [Derivation f]
tightenProof = (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
forall f.
Function f =>
(Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas Derivation f -> Derivation f
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
Derivation f -> Derivation f
tightenLemma
  where
    tightenLemma :: Derivation f -> Derivation f
tightenLemma Derivation f
p =
      Equation f -> [Derivation f] -> Derivation f
forall f. Equation f -> [Derivation f] -> Derivation f
fromSteps Equation f
eq (((Derivation f, Equation f) -> Derivation f)
-> [(Derivation f, Equation f)] -> [Derivation f]
forall a b. (a -> b) -> [a] -> [b]
map (Derivation f, Equation f) -> Derivation f
forall a b. (a, b) -> a
fst (([(Derivation f, Equation f)] -> Int)
-> ([(Derivation f, Equation f)] -> [(Derivation f, Equation f)])
-> [(Derivation f, Equation f)]
-> [(Derivation f, Equation f)]
forall b a. Eq b => (a -> b) -> (a -> a) -> a -> a
fixpointOn [(Derivation f, Equation f)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation (ConstantOf (Derivation f))
-> [(Derivation f, Equation (ConstantOf (Derivation f)))]
-> [(Derivation f, Equation (ConstantOf (Derivation f)))]
forall a.
Symbolic a =>
Equation (ConstantOf a)
-> [(a, Equation (ConstantOf a))] -> [(a, Equation (ConstantOf a))]
tightenSteps Equation f
Equation (ConstantOf (Derivation f))
eq) ([Derivation f] -> [Equation f] -> [(Derivation f, Equation f)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Derivation f]
ps [Equation f]
eqs)))
      where
        eq :: Equation f
eq = Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)
        ps :: [Derivation f]
ps = Derivation f -> [Derivation f]
forall f. Function f => Derivation f -> [Derivation f]
steps Derivation f
p
        eqs :: [Equation f]
eqs = (Derivation f -> Equation f) -> [Derivation f] -> [Equation f]
forall a b. (a -> b) -> [a] -> [b]
map (Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Proof f -> Equation f)
-> (Derivation f -> Proof f) -> Derivation f -> Equation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify) [Derivation f]
ps

    tightenSteps :: Equation (ConstantOf a)
-> [(a, Equation (ConstantOf a))] -> [(a, Equation (ConstantOf a))]
tightenSteps Equation (ConstantOf a)
eq [(a, Equation (ConstantOf a))]
steps = [[(a, Equation (ConstantOf a))]] -> [(a, Equation (ConstantOf a))]
forall a. [a] -> a
head ([[(a, Equation (ConstantOf a))]]
cands [[(a, Equation (ConstantOf a))]]
-> [[(a, Equation (ConstantOf a))]]
-> [[(a, Equation (ConstantOf a))]]
forall a. [a] -> [a] -> [a]
++ [[(a, Equation (ConstantOf a))]
steps])
      where
        -- Look for a segment of ps which can be removed, in the
        -- sense that the terms at both ends of the segment are
        -- unifiable without altering eq.
        cands :: [[(a, Equation (ConstantOf a))]]
cands =
          [ Subst (ConstantOf a)
-> [(a, Equation (ConstantOf a))] -> [(a, Equation (ConstantOf a))]
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub ([(a, Equation (ConstantOf a))]
before [(a, Equation (ConstantOf a))]
-> [(a, Equation (ConstantOf a))] -> [(a, Equation (ConstantOf a))]
forall a. [a] -> [a] -> [a]
++ [(a, Equation (ConstantOf a))]
after)
          | ([(a, Equation (ConstantOf a))]
before, [(a, Equation (ConstantOf a))]
mid1) <- [(a, Equation (ConstantOf a))]
-> [([(a, Equation (ConstantOf a))],
     [(a, Equation (ConstantOf a))])]
forall a. [a] -> [([a], [a])]
splits [(a, Equation (ConstantOf a))]
steps,
            -- 'reverse' means we start with big segments.
            (mid :: [(a, Equation (ConstantOf a))]
mid@((a, Equation (ConstantOf a))
_:[(a, Equation (ConstantOf a))]
_), [(a, Equation (ConstantOf a))]
after) <- [([(a, Equation (ConstantOf a))], [(a, Equation (ConstantOf a))])]
-> [([(a, Equation (ConstantOf a))],
     [(a, Equation (ConstantOf a))])]
forall a. [a] -> [a]
reverse ([(a, Equation (ConstantOf a))]
-> [([(a, Equation (ConstantOf a))],
     [(a, Equation (ConstantOf a))])]
forall a. [a] -> [([a], [a])]
splits [(a, Equation (ConstantOf a))]
mid1),
            let Term (ConstantOf a)
t :=: Term (ConstantOf a)
_ = (a, Equation (ConstantOf a)) -> Equation (ConstantOf a)
forall a b. (a, b) -> b
snd ([(a, Equation (ConstantOf a))] -> (a, Equation (ConstantOf a))
forall a. [a] -> a
head [(a, Equation (ConstantOf a))]
mid)
                Term (ConstantOf a)
_ :=: Term (ConstantOf a)
u = (a, Equation (ConstantOf a)) -> Equation (ConstantOf a)
forall a b. (a, b) -> b
snd ([(a, Equation (ConstantOf a))] -> (a, Equation (ConstantOf a))
forall a. [a] -> a
last [(a, Equation (ConstantOf a))]
mid),
            Subst (ConstantOf a)
sub <- Maybe (Subst (ConstantOf a)) -> [Subst (ConstantOf a)]
forall a. Maybe a -> [a]
maybeToList (Term (ConstantOf a)
-> Term (ConstantOf a) -> Maybe (Subst (ConstantOf a))
forall f. Term f -> Term f -> Maybe (Subst f)
unify Term (ConstantOf a)
t Term (ConstantOf a)
u),
            Subst (ConstantOf a)
-> Equation (ConstantOf a) -> Equation (ConstantOf a)
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub Equation (ConstantOf a)
eq Equation (ConstantOf a) -> Equation (ConstantOf a) -> Bool
forall a. Eq a => a -> a -> Bool
== Equation (ConstantOf a)
eq ] [[(a, Equation (ConstantOf a))]]
-> [[(a, Equation (ConstantOf a))]]
-> [[(a, Equation (ConstantOf a))]]
forall a. [a] -> [a] -> [a]
++
          [ Subst (ConstantOf a)
-> [(a, Equation (ConstantOf a))] -> [(a, Equation (ConstantOf a))]
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub [(a, Equation (ConstantOf a))]
before
          | ([(a, Equation (ConstantOf a))]
before, after :: [(a, Equation (ConstantOf a))]
after@((a, Equation (ConstantOf a))
_:[(a, Equation (ConstantOf a))]
_)) <- [(a, Equation (ConstantOf a))]
-> [([(a, Equation (ConstantOf a))],
     [(a, Equation (ConstantOf a))])]
forall a. [a] -> [([a], [a])]
splits [(a, Equation (ConstantOf a))]
steps,
            let Term (ConstantOf a)
t :=: Term (ConstantOf a)
_ = (a, Equation (ConstantOf a)) -> Equation (ConstantOf a)
forall a b. (a, b) -> b
snd ([(a, Equation (ConstantOf a))] -> (a, Equation (ConstantOf a))
forall a. [a] -> a
head [(a, Equation (ConstantOf a))]
after)
                Term (ConstantOf a)
_ :=: Term (ConstantOf a)
u = (a, Equation (ConstantOf a)) -> Equation (ConstantOf a)
forall a b. (a, b) -> b
snd ([(a, Equation (ConstantOf a))] -> (a, Equation (ConstantOf a))
forall a. [a] -> a
last [(a, Equation (ConstantOf a))]
after),
            Subst (ConstantOf a)
sub <- Maybe (Subst (ConstantOf a)) -> [Subst (ConstantOf a)]
forall a. Maybe a -> [a]
maybeToList (Term (ConstantOf a)
-> Term (ConstantOf a) -> Maybe (Subst (ConstantOf a))
forall f. Term f -> Term f -> Maybe (Subst f)
match Term (ConstantOf a)
t Term (ConstantOf a)
u),
            Subst (ConstantOf a) -> Term (ConstantOf a) -> Term (ConstantOf a)
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub (Equation (ConstantOf a) -> Term (ConstantOf a)
forall f. Equation f -> Term f
eqn_lhs Equation (ConstantOf a)
eq) Term (ConstantOf a) -> Term (ConstantOf a) -> Bool
forall a. Eq a => a -> a -> Bool
== Equation (ConstantOf a) -> Term (ConstantOf a)
forall f. Equation f -> Term f
eqn_lhs Equation (ConstantOf a)
eq ] [[(a, Equation (ConstantOf a))]]
-> [[(a, Equation (ConstantOf a))]]
-> [[(a, Equation (ConstantOf a))]]
forall a. [a] -> [a] -> [a]
++
          [ Subst (ConstantOf a)
-> [(a, Equation (ConstantOf a))] -> [(a, Equation (ConstantOf a))]
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub [(a, Equation (ConstantOf a))]
after
          | (before :: [(a, Equation (ConstantOf a))]
before@((a, Equation (ConstantOf a))
_:[(a, Equation (ConstantOf a))]
_), [(a, Equation (ConstantOf a))]
after) <- [([(a, Equation (ConstantOf a))], [(a, Equation (ConstantOf a))])]
-> [([(a, Equation (ConstantOf a))],
     [(a, Equation (ConstantOf a))])]
forall a. [a] -> [a]
reverse ([(a, Equation (ConstantOf a))]
-> [([(a, Equation (ConstantOf a))],
     [(a, Equation (ConstantOf a))])]
forall a. [a] -> [([a], [a])]
splits [(a, Equation (ConstantOf a))]
steps),
            let Term (ConstantOf a)
t :=: Term (ConstantOf a)
_ = (a, Equation (ConstantOf a)) -> Equation (ConstantOf a)
forall a b. (a, b) -> b
snd ([(a, Equation (ConstantOf a))] -> (a, Equation (ConstantOf a))
forall a. [a] -> a
head [(a, Equation (ConstantOf a))]
before)
                Term (ConstantOf a)
_ :=: Term (ConstantOf a)
u = (a, Equation (ConstantOf a)) -> Equation (ConstantOf a)
forall a b. (a, b) -> b
snd ([(a, Equation (ConstantOf a))] -> (a, Equation (ConstantOf a))
forall a. [a] -> a
last [(a, Equation (ConstantOf a))]
before),
            Subst (ConstantOf a)
sub <- Maybe (Subst (ConstantOf a)) -> [Subst (ConstantOf a)]
forall a. Maybe a -> [a]
maybeToList (Term (ConstantOf a)
-> Term (ConstantOf a) -> Maybe (Subst (ConstantOf a))
forall f. Term f -> Term f -> Maybe (Subst f)
match Term (ConstantOf a)
u Term (ConstantOf a)
t),
            Subst (ConstantOf a) -> Term (ConstantOf a) -> Term (ConstantOf a)
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub (Equation (ConstantOf a) -> Term (ConstantOf a)
forall f. Equation f -> Term f
eqn_rhs Equation (ConstantOf a)
eq) Term (ConstantOf a) -> Term (ConstantOf a) -> Bool
forall a. Eq a => a -> a -> Bool
== Equation (ConstantOf a) -> Term (ConstantOf a)
forall f. Equation f -> Term f
eqn_rhs Equation (ConstantOf a)
eq ]

generaliseProof :: Function f => [Derivation f] -> [Derivation f]
generaliseProof :: [Derivation f] -> [Derivation f]
generaliseProof =
  (Map (Proof f) (Derivation f) -> Proof f -> Derivation f)
-> (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> [Derivation f]
-> [Derivation f]
forall f.
Function f =>
(Map (Proof f) (Derivation f) -> Proof f -> Derivation f)
-> (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> [Derivation f]
-> [Derivation f]
simplificationPass ((Proof f -> Derivation f)
-> Map (Proof f) (Derivation f) -> Proof f -> Derivation f
forall a b. a -> b -> a
const Proof f -> Derivation f
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
Proof f -> Derivation f
generaliseLemma) ((Derivation f -> Derivation f)
-> Map (Proof f) (Derivation f) -> Derivation f -> Derivation f
forall a b. a -> b -> a
const Derivation f -> Derivation f
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
Derivation f -> Derivation f
generaliseGoal)
  where
    generaliseLemma :: Proof f -> Derivation f
generaliseLemma Proof f
p = Proof f -> Subst f -> Derivation f
forall f. Proof f -> Subst f -> Derivation f
lemma (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
q) Subst f
sub
      where
        (Derivation f
q, Subst f
sub) = Proof f -> (Derivation f, Subst f)
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
Proof f -> (Derivation f, Subst f)
generalise Proof f
p
    generaliseGoal :: Derivation f -> Derivation f
generaliseGoal Derivation f
p = Subst f -> Derivation f -> Derivation f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Derivation f
q
      where
        (Derivation f
q, Subst f
sub) = Proof f -> (Derivation f, Subst f)
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
Proof f -> (Derivation f, Subst f)
generalise (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)

    generalise :: Proof f -> (Derivation f, Subst f)
generalise Proof f
p = (Derivation f
q, Subst f
sub)
      where
        eq :: Equation f
eq = Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p
        n :: Int
n = Equation f -> Int
forall a. Symbolic a => a -> Int
freshVar Equation f
eq
        qs :: [Derivation f]
qs = State Int [Derivation f] -> Int -> [Derivation f]
forall s a. State s a -> s -> a
evalState ((Derivation f -> StateT Int Identity (Derivation f))
-> [Derivation f] -> State Int [Derivation f]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Derivation f -> StateT Int Identity (Derivation f)
forall (m :: * -> *) f.
Monad m =>
Derivation f -> StateT Int m (Derivation f)
generaliseStep (Derivation f -> [Derivation f]
forall f. Function f => Derivation f -> [Derivation f]
steps (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p))) Int
n
        Just Subst f
sub1 = [(Term f, Term f)] -> Maybe (Subst f)
forall f. [(Term f, Term f)] -> Maybe (Subst f)
unifyMany ([Derivation f] -> [(Term f, Term f)]
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
[Derivation f] -> [(Term f, Term f)]
stepsConstraints [Derivation f]
qs)
        q :: Derivation f
q = Derivation f -> Derivation f
forall a. Symbolic a => a -> a
canonicalise (Equation f -> [Derivation f] -> Derivation f
forall f. Equation f -> [Derivation f] -> Derivation f
fromSteps Equation f
eq (Subst f -> [Derivation f] -> [Derivation f]
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub1 [Derivation f]
qs))
        Just Subst f
sub = Equation f -> Equation f -> Maybe (Subst f)
forall f. Equation f -> Equation f -> Maybe (Subst f)
matchEquation (Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
q)) Equation f
eq

    generaliseStep :: Derivation f -> StateT Int m (Derivation f)
generaliseStep (UseAxiom Axiom f
axiom Subst f
_) =
      [Var] -> (Subst f -> Derivation f) -> StateT Int m (Derivation f)
forall (m :: * -> *) f b.
Monad m =>
[Var] -> (Subst f -> b) -> StateT Int m b
freshen (Equation f -> [Var]
forall a. Symbolic a => a -> [Var]
vars (Axiom f -> Equation f
forall f. Axiom f -> Equation f
axiom_eqn Axiom f
axiom)) (Axiom f -> Subst f -> Derivation f
forall f. Axiom f -> Subst f -> Derivation f
UseAxiom Axiom f
axiom)
    generaliseStep (UseLemma Proof f
lemma Subst f
_) =
      [Var] -> (Subst f -> Derivation f) -> StateT Int m (Derivation f)
forall (m :: * -> *) f b.
Monad m =>
[Var] -> (Subst f -> b) -> StateT Int m b
freshen (Equation f -> [Var]
forall a. Symbolic a => a -> [Var]
vars (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
lemma)) (Proof f -> Subst f -> Derivation f
forall f. Proof f -> Subst f -> Derivation f
UseLemma Proof f
lemma)
    generaliseStep (Refl Term f
_) = do
      Int
n <- StateT Int m Int
forall (m :: * -> *) s. Monad m => StateT s m s
get
      Int -> StateT Int m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
      Derivation f -> StateT Int m (Derivation f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term f -> Derivation f
forall f. Term f -> Derivation f
Refl (Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Var -> Builder f
forall f. Var -> Builder f
var (Int -> Var
V Int
n))))
    generaliseStep (Symm Derivation f
p) =
      Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Symm (Derivation f -> Derivation f)
-> StateT Int m (Derivation f) -> StateT Int m (Derivation f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Derivation f -> StateT Int m (Derivation f)
generaliseStep Derivation f
p
    generaliseStep (Trans Derivation f
p Derivation f
q) =
      (Derivation f -> Derivation f -> Derivation f)
-> StateT Int m (Derivation f)
-> StateT Int m (Derivation f)
-> StateT Int m (Derivation f)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
Trans (Derivation f -> StateT Int m (Derivation f)
generaliseStep Derivation f
p) (Derivation f -> StateT Int m (Derivation f)
generaliseStep Derivation f
q)
    generaliseStep (Cong Fun f
f [Derivation f]
ps) =
      Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
Cong Fun f
f ([Derivation f] -> Derivation f)
-> StateT Int m [Derivation f] -> StateT Int m (Derivation f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Derivation f -> StateT Int m (Derivation f))
-> [Derivation f] -> StateT Int m [Derivation f]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Derivation f -> StateT Int m (Derivation f)
generaliseStep [Derivation f]
ps

    freshen :: [Var] -> (Subst f -> b) -> StateT Int m b
freshen [Var]
xs Subst f -> b
f = do
      Int
n <- StateT Int m Int
forall (m :: * -> *) s. Monad m => StateT s m s
get
      Int -> StateT Int m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs)
      let Just Subst f
sub = [(Var, Term f)] -> Maybe (Subst f)
forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst [(Var
x, Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Var -> Builder f
forall f. Var -> Builder f
var (Int -> Var
V Int
i))) | (Var
x, Int
i) <- [Var] -> [Int] -> [(Var, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort [Var]
xs) [Int
n..]]
      b -> StateT Int m b
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst f -> b
f Subst f
sub)

    stepsConstraints :: [Derivation f] -> [(Term f, Term f)]
stepsConstraints [Derivation f]
ps = (Equation f -> Equation f -> (Term f, Term f))
-> [Equation f] -> [Equation f] -> [(Term f, Term f)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Equation f -> Equation f -> (Term f, Term f)
forall f f. Equation f -> Equation f -> (Term f, Term f)
combine [Equation f]
eqs ([Equation f] -> [Equation f]
forall a. [a] -> [a]
tail [Equation f]
eqs)
      where
        eqs :: [Equation f]
eqs = (Derivation f -> Equation f) -> [Derivation f] -> [Equation f]
forall a b. (a -> b) -> [a] -> [b]
map (Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Proof f -> Equation f)
-> (Derivation f -> Proof f) -> Derivation f -> Equation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify) [Derivation f]
ps
        combine :: Equation f -> Equation f -> (Term f, Term f)
combine (Term f
_ :=: Term f
t) (Term f
u :=: Term f
_) = (Term f
t, Term f
u)

canonicaliseLemmas :: Function f => [Derivation f] -> [Derivation f]
canonicaliseLemmas :: [Derivation f] -> [Derivation f]
canonicaliseLemmas =
  (Map (Proof f) (Derivation f) -> Proof f -> Derivation f)
-> (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> [Derivation f]
-> [Derivation f]
forall f.
Function f =>
(Map (Proof f) (Derivation f) -> Proof f -> Derivation f)
-> (Map (Proof f) (Derivation f) -> Derivation f -> Derivation f)
-> [Derivation f]
-> [Derivation f]
simplificationPass ((Proof f -> Derivation f)
-> Map (Proof f) (Derivation f) -> Proof f -> Derivation f
forall a b. a -> b -> a
const Proof f -> Derivation f
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
Proof f -> Derivation f
canonicaliseLemma) ((Derivation f -> Derivation f)
-> Map (Proof f) (Derivation f) -> Derivation f -> Derivation f
forall a b. a -> b -> a
const Derivation f -> Derivation f
forall a. Symbolic a => a -> a
canonicalise)
  where
    -- Present the equation left-to-right, and with variables
    -- named canonically
    canonicaliseLemma :: Proof f -> Derivation f
canonicaliseLemma Proof f
p
      | Term f
u Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
`lessEqSkolem` Term f
t = Derivation f -> Derivation f
canon (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p)
      | Bool
otherwise = Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm (Derivation f -> Derivation f
canon (Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p)))
      where
        Term f
t :=: Term f
u = Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p
        -- This ensures that we also renumber variables in the derivation that
        -- do not occur in the equation, but that variables in the equation
        -- get priority.
        symbolic :: Proof f -> (Equation f, Derivation f)
symbolic Proof f
p = (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p, Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p)
        before :: (Equation f, Derivation f)
before = Proof f -> (Equation f, Derivation f)
forall f. Proof f -> (Equation f, Derivation f)
symbolic Proof f
p
        after :: (Equation f, Derivation f)
after = (Equation f, Derivation f) -> (Equation f, Derivation f)
forall a. Symbolic a => a -> a
canonicalise (Proof f -> (Equation f, Derivation f)
forall f. Proof f -> (Equation f, Derivation f)
symbolic Proof f
p)
        Just Subst f
sub1 = [TermList f] -> [TermList f] -> Maybe (Subst f)
forall f. [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyList ((Equation f, Derivation f)
-> [TermListOf (Equation f, Derivation f)]
forall a. Symbolic a => a -> [TermListOf a]
terms (Equation f, Derivation f)
before) ((Equation f, Derivation f)
-> [TermListOf (Equation f, Derivation f)]
forall a. Symbolic a => a -> [TermListOf a]
terms (Equation f, Derivation f)
after)
        Just Subst f
sub2 = [TermList f] -> [TermList f] -> Maybe (Subst f)
forall f. [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyList ((Equation f, Derivation f)
-> [TermListOf (Equation f, Derivation f)]
forall a. Symbolic a => a -> [TermListOf a]
terms (Equation f, Derivation f)
after) ((Equation f, Derivation f)
-> [TermListOf (Equation f, Derivation f)]
forall a. Symbolic a => a -> [TermListOf a]
terms (Equation f, Derivation f)
before)
        canon :: Derivation f -> Derivation f
canon Derivation f
p = Subst f -> Derivation f -> Derivation f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub2 (Proof f -> Derivation f
forall f. Function f => Proof f -> Derivation f
simpleLemma (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify (Subst f -> Derivation f -> Derivation f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub1 Derivation f
p)))

invisible :: Function f => Equation f -> Bool
invisible :: Equation f -> Bool
invisible (Term f
t :=: Term f
u) = Doc -> String
forall a. Show a => a -> String
show (Term f -> Doc
forall a. Pretty a => a -> Doc
pPrint Term f
t) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Doc -> String
forall a. Show a => a -> String
show (Term f -> Doc
forall a. Pretty a => a -> Doc
pPrint Term f
u)

-- Pretty-print the proof of a single lemma.
pPrintLemma :: Function f => Config f -> (Axiom f -> String) -> (Proof f -> String) -> Proof f -> Doc
pPrintLemma :: Config f
-> (Axiom f -> String) -> (Proof f -> String) -> Proof f -> Doc
pPrintLemma Config{Bool
Axiom f -> Bool
cfg_show_uses_of_axioms :: Axiom f -> Bool
cfg_use_colour :: Bool
cfg_show_instances :: Bool
cfg_ground_proof :: Bool
cfg_no_lemmas :: Bool
cfg_all_lemmas :: Bool
cfg_show_uses_of_axioms :: forall f. Config f -> Axiom f -> Bool
cfg_use_colour :: forall f. Config f -> Bool
cfg_show_instances :: forall f. Config f -> Bool
cfg_ground_proof :: forall f. Config f -> Bool
cfg_no_lemmas :: forall f. Config f -> Bool
cfg_all_lemmas :: forall f. Config f -> Bool
..} Axiom f -> String
axiomNum Proof f -> String
lemmaNum Proof f
p
  | [Derivation f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Derivation f]
qs = String -> Doc
text String
"Reflexivity."
  | Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify (Equation f -> [Derivation f] -> Derivation f
forall f. Equation f -> [Derivation f] -> Derivation f
fromSteps (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p) [Derivation f]
qs)) Equation f -> Equation f -> Bool
forall a. Eq a => a -> a -> Bool
== Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p =
    [Doc] -> Doc
vcat (([Int] -> Derivation f -> Doc)
-> [[Int]] -> [Derivation f] -> [Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Int] -> Derivation f -> Doc
pp [[Int]]
hl [Derivation f]
qs) Doc -> Doc -> Doc
$$ Term f -> Doc
forall a. Pretty a => a -> Doc
ppTerm (Equation f -> Term f
forall f. Equation f -> Term f
eqn_rhs (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p))
  | Bool
otherwise = String -> Doc
forall a. HasCallStack => String -> a
error String
"lemma changed by pretty-printing!"
  where
    qs :: [Derivation f]
qs = Derivation f -> [Derivation f]
forall f. Function f => Derivation f -> [Derivation f]
steps (Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
p)
    hl :: [[Int]]
hl = (Derivation f -> [Int]) -> [Derivation f] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map Derivation f -> [Int]
forall a f. (Num a, Enum a) => Derivation f -> [a]
highlightStep [Derivation f]
qs

    pp :: [Int] -> Derivation f -> Doc
pp [Int]
_ Derivation f
p | Equation f -> Bool
forall f. Function f => Equation f -> Bool
invisible (Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)) = Doc
pPrintEmpty
    pp [Int]
h Derivation f
p =
      HighlightedTerm f -> Doc
forall a. Pretty a => a -> Doc
ppTerm ([String] -> Maybe [Int] -> Term f -> HighlightedTerm f
forall f. [String] -> Maybe [Int] -> Term f -> HighlightedTerm f
HighlightedTerm [String
green | Bool
cfg_use_colour] ([Int] -> Maybe [Int]
forall a. a -> Maybe a
Just [Int]
h) (Equation f -> Term f
forall f. Equation f -> Term f
eqn_lhs (Proof f -> Equation f
forall f. Proof f -> Equation f
equation (Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)))) Doc -> Doc -> Doc
$$
      String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> [String] -> Doc -> Doc
highlight [String
bold | Bool
cfg_use_colour] (String -> Doc
text String
"{ by" Doc -> Doc -> Doc
<+> Derivation f -> Doc
ppStep Derivation f
p Doc -> Doc -> Doc
<+> String -> Doc
text String
"}")

    highlightStep :: Derivation f -> [a]
highlightStep UseAxiom{} = []
    highlightStep UseLemma{} = []
    highlightStep (Symm Derivation f
p) = Derivation f -> [a]
highlightStep Derivation f
p
    highlightStep (Cong Fun f
_ [Derivation f]
ps) = a
ia -> [a] -> [a]
forall a. a -> [a] -> [a]
:Derivation f -> [a]
highlightStep Derivation f
p
      where
        [(a
i, Derivation f
p)] = ((a, Derivation f) -> Bool)
-> [(a, Derivation f)] -> [(a, Derivation f)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((a, Derivation f) -> Bool) -> (a, Derivation f) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Bool
forall f. Derivation f -> Bool
isRefl (Derivation f -> Bool)
-> ((a, Derivation f) -> Derivation f) -> (a, Derivation f) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Derivation f) -> Derivation f
forall a b. (a, b) -> b
snd) ([a] -> [Derivation f] -> [(a, Derivation f)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a
0..] [Derivation f]
ps)

    ppTerm :: a -> Doc
ppTerm a
t = String -> Doc
text String
"  " Doc -> Doc -> Doc
<#> a -> Doc
forall a. Pretty a => a -> Doc
pPrint a
t

    ppStep :: Derivation f -> Doc
ppStep = Bool -> Derivation f -> Doc
pp Bool
True
      where
        pp :: Bool -> Derivation f -> Doc
pp Bool
dir (UseAxiom axiom :: Axiom f
axiom@Axiom{Int
String
Equation f
axiom_eqn :: Equation f
axiom_name :: String
axiom_number :: Int
axiom_eqn :: forall f. Axiom f -> Equation f
axiom_name :: forall f. Axiom f -> String
axiom_number :: forall f. Axiom f -> Int
..} Subst f
sub) =
          String -> Doc
text String
"axiom" Doc -> Doc -> Doc
<+> String -> Doc
text (Axiom f -> String
axiomNum Axiom f
axiom) Doc -> Doc -> Doc
<+> Doc -> Doc
parens (String -> Doc
text String
axiom_name) Doc -> Doc -> Doc
<+> Bool -> Doc
ppDir Bool
dir Doc -> Doc -> Doc
<#> Subst f -> Doc
showSubst Subst f
sub
        pp Bool
dir (UseLemma Proof f
lemma Subst f
sub) =
          String -> Doc
text String
"lemma" Doc -> Doc -> Doc
<+> String -> Doc
text (Proof f -> String
lemmaNum Proof f
lemma) Doc -> Doc -> Doc
<+> Bool -> Doc
ppDir Bool
dir Doc -> Doc -> Doc
<#> Subst f -> Doc
showSubst Subst f
sub
        pp Bool
dir (Symm Derivation f
p) =
          Bool -> Derivation f -> Doc
pp (Bool -> Bool
not Bool
dir) Derivation f
p
        pp Bool
dir (Cong Fun f
_ [Derivation f]
ps) = Bool -> Derivation f -> Doc
pp Bool
dir Derivation f
p
          where
            [Derivation f
p] = (Derivation f -> Bool) -> [Derivation f] -> [Derivation f]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Derivation f -> Bool) -> Derivation f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Bool
forall f. Derivation f -> Bool
isRefl) [Derivation f]
ps

    ppDir :: Bool -> Doc
ppDir Bool
True = Doc
pPrintEmpty
    ppDir Bool
False = String -> Doc
text String
"R->L"

    showSubst :: Subst f -> Doc
showSubst Subst f
sub
      | Bool
cfg_show_instances Bool -> Bool -> Bool
&& Bool -> Bool
not ([(Var, Term f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Subst f -> [(Var, Term f)]
forall f. Subst f -> [(Var, Term f)]
substToList Subst f
sub)) =
        String -> Doc
text String
" with " Doc -> Doc -> Doc
<#> Subst f -> Doc
forall f. Function f => Subst f -> Doc
pPrintSubst Subst f
sub
      | Bool
otherwise = Doc
pPrintEmpty

    isRefl :: Derivation f -> Bool
isRefl Refl{} = Bool
True
    isRefl Derivation f
_ = Bool
False

-- Pretty-print a substitution.
pPrintSubst :: Function f => Subst f -> Doc
pPrintSubst :: Subst f -> Doc
pPrintSubst Subst f
sub =
  [Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma
    [ Var -> Doc
forall a. Pretty a => a -> Doc
pPrint Var
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"->" Doc -> Doc -> Doc
<+> Term f -> Doc
forall a. Pretty a => a -> Doc
pPrint Term f
t
    | (Var
x, Term f
t) <- Subst f -> [(Var, Term f)]
forall f. Subst f -> [(Var, Term f)]
substToList Subst f
sub ])

-- | Print a presented proof.
pPrintPresentation :: forall f. Function f => Config f -> Presentation f -> Doc
pPrintPresentation :: Config f -> Presentation f -> Doc
pPrintPresentation Config f
config (Presentation [Axiom f]
axioms [Proof f]
lemmas [ProvedGoal f]
goals) =
  [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
intersperse (String -> Doc
text String
"") ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
    [Doc] -> Doc
vcat [ String -> String -> Maybe String -> Equation f -> Doc
forall f.
Function f =>
String -> String -> Maybe String -> Equation f -> Doc
describeEquation String
"Axiom" (Axiom f -> String
axiomNum Axiom f
axiom) (String -> Maybe String
forall a. a -> Maybe a
Just String
name) Equation f
eqn Doc -> Doc -> Doc
$$
           Axiom f -> Doc
ppAxiomUses Axiom f
axiom
         | axiom :: Axiom f
axiom@(Axiom Int
_ String
name Equation f
eqn) <- [Axiom f]
axioms,
           Bool -> Bool
not (Equation f -> Bool
forall f. Function f => Equation f -> Bool
invisible Equation f
eqn) ]Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
    [ String
-> String
-> Maybe String
-> Equation f
-> Subst f
-> Proof f
-> Doc
pp String
"Lemma" (Proof f -> String
lemmaNum Proof f
p) Maybe String
forall a. Maybe a
Nothing (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p) Subst f
forall f. Subst f
emptySubst Proof f
p
    | Proof f
p <- [Proof f]
lemmas,
      Bool -> Bool
not (Equation f -> Bool
forall f. Function f => Equation f -> Bool
invisible (Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
p)) ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
    [ String
-> String
-> Maybe String
-> Equation f
-> Subst f
-> Proof f
-> Doc
pp String
"Goal" (Integer -> String
forall a. Show a => a -> String
show Integer
num) (String -> Maybe String
forall a. a -> Maybe a
Just String
pg_name) Equation f
pg_goal_hint Subst f
pg_witness_hint Proof f
pg_proof
    | (Integer
num, ProvedGoal{Int
String
Subst f
Equation f
Proof f
pg_number :: Int
pg_proof :: Proof f
pg_witness_hint :: Subst f
pg_goal_hint :: Equation f
pg_name :: String
pg_witness_hint :: forall f. ProvedGoal f -> Subst f
pg_goal_hint :: forall f. ProvedGoal f -> Equation f
pg_name :: forall f. ProvedGoal f -> String
pg_number :: forall f. ProvedGoal f -> Int
pg_proof :: forall f. ProvedGoal f -> Proof f
..}) <- [Integer] -> [ProvedGoal f] -> [(Integer, ProvedGoal f)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
1..] [ProvedGoal f]
goals ]
  where
    pp :: String
-> String
-> Maybe String
-> Equation f
-> Subst f
-> Proof f
-> Doc
pp String
kind String
n Maybe String
mname Equation f
eqn Subst f
witness Proof f
p =
      String -> String -> Maybe String -> Equation f -> Doc
forall f.
Function f =>
String -> String -> Maybe String -> Equation f -> Doc
describeEquation String
kind String
n Maybe String
mname Equation f
eqn Doc -> Doc -> Doc
$$
      Subst f -> Doc
ppWitness Subst f
witness Doc -> Doc -> Doc
$$
      String -> Doc
text String
"Proof:" Doc -> Doc -> Doc
$$
      Config f
-> (Axiom f -> String) -> (Proof f -> String) -> Proof f -> Doc
forall f.
Function f =>
Config f
-> (Axiom f -> String) -> (Proof f -> String) -> Proof f -> Doc
pPrintLemma Config f
config Axiom f -> String
axiomNum Proof f -> String
lemmaNum Proof f
p

    axiomNums :: Map (Axiom f) Integer
axiomNums = [(Axiom f, Integer)] -> Map (Axiom f) Integer
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Axiom f] -> [Integer] -> [(Axiom f, Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Axiom f]
axioms [Integer
1..])
    lemmaNums :: Map (Proof f) Int
lemmaNums = [(Proof f, Int)] -> Map (Proof f) Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Proof f] -> [Int] -> [(Proof f, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Proof f]
lemmas [[Axiom f] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Axiom f]
axiomsInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1..])
    axiomNum :: Axiom f -> String
axiomNum Axiom f
x = Integer -> String
forall a. Show a => a -> String
show (Maybe Integer -> Integer
forall a. HasCallStack => Maybe a -> a
fromJust (Axiom f -> Map (Axiom f) Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Axiom f
x Map (Axiom f) Integer
axiomNums))
    lemmaNum :: Proof f -> String
lemmaNum Proof f
x = Int -> String
forall a. Show a => a -> String
show (Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Proof f -> Map (Proof f) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Proof f
x Map (Proof f) Int
lemmaNums))

    ppWitness :: Subst f -> Doc
ppWitness Subst f
sub
      | Subst f
sub Subst f -> Subst f -> Bool
forall a. Eq a => a -> a -> Bool
== Subst f
forall f. Subst f
emptySubst = Doc
pPrintEmpty
      | Bool
otherwise =
          [Doc] -> Doc
vcat [
            String -> Doc
text String
"The goal is true when:",
            Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
              [ Var -> Doc
forall a. Pretty a => a -> Doc
pPrint Var
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> Term f -> Doc
forall a. Pretty a => a -> Doc
pPrint Term f
t
              | (Var
x, Term f
t) <- Subst f -> [(Var, Term f)]
forall f. Subst f -> [(Var, Term f)]
substToList Subst f
sub ],
            if Fun f
forall f. Minimal f => Fun f
minimal Fun f -> [Fun f] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Subst f -> [FunOf (Subst f)]
forall a. Symbolic a => a -> [FunOf a]
funs Subst f
sub then
              String -> Doc
text String
"where" Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (Fun f -> Doc
forall a. Pretty a => a -> Doc
pPrint (Fun f
forall f. Minimal f => Fun f
minimal :: Fun f)) Doc -> Doc -> Doc
<+>
              String -> Doc
text String
"stands for an arbitrary term of your choice."
            else Doc
pPrintEmpty,
            String -> Doc
text String
""]

    ppAxiomUses :: Axiom f -> Doc
ppAxiomUses Axiom f
axiom
      | Config f -> Axiom f -> Bool
forall f. Config f -> Axiom f -> Bool
cfg_show_uses_of_axioms Config f
config Axiom f
axiom Bool -> Bool -> Bool
&& Bool -> Bool
not ([Subst f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst f]
uses) =
        String -> Doc
text String
"Used with:" Doc -> Doc -> Doc
$$
        Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat
          [ Int -> Doc
forall a. Pretty a => a -> Doc
pPrint Int
i Doc -> Doc -> Doc
<#> String -> Doc
text String
"." Doc -> Doc -> Doc
<+> Subst f -> Doc
forall f. Function f => Subst f -> Doc
pPrintSubst Subst f
sub
          | (Int
i, Subst f
sub) <- [Int] -> [Subst f] -> [(Int, Subst f)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1 :: Int ..] [Subst f]
uses ])
      | Bool
otherwise = Doc
pPrintEmpty
      where
        uses :: [Subst f]
uses = Set (Subst f) -> [Subst f]
forall a. Set a -> [a]
Set.toList (Axiom f -> Set (Subst f)
axiomUses Axiom f
axiom)

    axiomUses :: Axiom f -> Set (Subst f)
axiomUses Axiom f
axiom = Set (Subst f)
-> Axiom f -> Map (Axiom f) (Set (Subst f)) -> Set (Subst f)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set (Subst f)
forall a. Set a
Set.empty Axiom f
axiom Map (Axiom f) (Set (Subst f))
usesMap
    usesMap :: Map (Axiom f) (Set (Subst f))
usesMap =
      (Set (Subst f) -> Set (Subst f) -> Set (Subst f))
-> [Map (Axiom f) (Set (Subst f))] -> Map (Axiom f) (Set (Subst f))
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith Set (Subst f) -> Set (Subst f) -> Set (Subst f)
forall a. Ord a => Set a -> Set a -> Set a
Set.union
        [ (Set (Subst f) -> Set (Subst f))
-> Map (Axiom f) (Set (Subst f)) -> Map (Axiom f) (Set (Subst f))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Subst f -> Set (Subst f) -> Set (Subst f)
forall a. Ord a => a -> Set a -> Set a
Set.delete Subst f
forall f. Subst f
emptySubst (Set (Subst f) -> Set (Subst f))
-> (Set (Subst f) -> Set (Subst f))
-> Set (Subst f)
-> Set (Subst f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Subst f -> Subst f) -> Set (Subst f) -> Set (Subst f)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Subst f -> Subst f
forall a f. (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
ground)
            (Derivation f -> Map (Axiom f) (Set (Subst f))
forall f.
Function f =>
Derivation f -> Map (Axiom f) (Set (Subst f))
groundAxiomsAndSubsts Derivation f
p)
        | ProvedGoal f
goal <- [ProvedGoal f]
goals,
          let p :: Derivation f
p = Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation (ProvedGoal f -> Proof f
forall f. ProvedGoal f -> Proof f
pg_proof ProvedGoal f
goal) ]

-- | Format an equation nicely.
--
-- Used both here and in the main file.
describeEquation ::
  Function f =>
  String -> String -> Maybe String -> Equation f -> Doc
describeEquation :: String -> String -> Maybe String -> Equation f -> Doc
describeEquation String
kind String
num Maybe String
mname Equation f
eqn =
  String -> Doc
text String
kind Doc -> Doc -> Doc
<+> String -> Doc
text String
num Doc -> Doc -> Doc
<#>
  (case Maybe String
mname of
     Maybe String
Nothing -> String -> Doc
text String
""
     Just String
name -> String -> Doc
text (String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")")) Doc -> Doc -> Doc
<#>
  String -> Doc
text String
":" Doc -> Doc -> Doc
<+> Equation f -> Doc
forall a. Pretty a => a -> Doc
pPrint Equation f
eqn Doc -> Doc -> Doc
<#> String -> Doc
text String
"."

----------------------------------------------------------------------
-- Making proofs of existential goals more readable.
----------------------------------------------------------------------

-- The idea: the only axioms which mention $equals, $true and $false
-- are:
--   * $equals(x,x) = $true  (reflexivity)
--   * $equals(t,u) = $false (conjecture)
-- This implies that a proof $true = $false must have the following
-- structure, if we expand out all lemmas:
--   $true = $equals(s,s) = ... = $equals(t,u) = $false.
--
-- The substitution in the last step $equals(t,u) = $false is in fact the
-- witness to the existential.
--
-- Furthermore, we can make it so that the inner "..." doesn't use the $equals
-- axioms. If it does, one of the "..." steps results in either $true or $false,
-- and we can chop off everything before the $true or after the $false.
--
-- Once we have done that, every proof step in the "..." must be a congruence
-- step of the shape
--   $equals(t, u) = $equals(v, w).
-- This is because there are no other axioms which mention $equals. Hence we can
-- split the proof of $equals(s,s) = $equals(t,u) into separate proofs of s=t
-- and s=u.
--
-- What we have got out is:
--   * the witness to the existential
--   * a proof that both sides of the conjecture are equal
-- and we can present that to the user.

-- Decode $equals(t,u) into an equation t=u.
decodeEquality :: Function f => Term f -> Maybe (Equation f)
decodeEquality :: Term f -> Maybe (Equation f)
decodeEquality (App Fun f
equals (Cons Term f
t (Cons Term f
u TermList f
Empty)))
  | Fun f -> Bool
forall f. EqualsBonus f => f -> Bool
isEquals Fun f
equals = Equation f -> Maybe (Equation f)
forall a. a -> Maybe a
Just (Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u)
decodeEquality Term f
_ = Maybe (Equation f)
forall a. Maybe a
Nothing

-- Tries to transform a proof of $true = $false into a proof of
-- the original existentially-quantified formula.
decodeGoal :: Function f => ProvedGoal f -> ProvedGoal f
decodeGoal :: ProvedGoal f -> ProvedGoal f
decodeGoal ProvedGoal f
pg =
  case ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)
forall f.
Function f =>
ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)
maybeDecodeGoal ProvedGoal f
pg of
    Maybe (String, Subst f, Equation f, Derivation f)
Nothing -> ProvedGoal f
pg
    Just (String
name, Subst f
witness, Equation f
goal, Derivation f
deriv) ->
      ProvedGoal f -> ProvedGoal f
forall f. Function f => ProvedGoal f -> ProvedGoal f
checkProvedGoal (ProvedGoal f -> ProvedGoal f) -> ProvedGoal f -> ProvedGoal f
forall a b. (a -> b) -> a -> b
$
      ProvedGoal f
pg {
        pg_name :: String
pg_name = String
name,
        pg_proof :: Proof f
pg_proof = Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
deriv,
        pg_goal_hint :: Equation f
pg_goal_hint = Equation f
goal,
        pg_witness_hint :: Subst f
pg_witness_hint = Subst f
witness }

maybeDecodeGoal :: forall f. Function f =>
  ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)
maybeDecodeGoal :: ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)
maybeDecodeGoal ProvedGoal{Int
String
Subst f
Equation f
Proof f
pg_witness_hint :: Subst f
pg_goal_hint :: Equation f
pg_proof :: Proof f
pg_name :: String
pg_number :: Int
pg_witness_hint :: forall f. ProvedGoal f -> Subst f
pg_goal_hint :: forall f. ProvedGoal f -> Equation f
pg_name :: forall f. ProvedGoal f -> String
pg_number :: forall f. ProvedGoal f -> Int
pg_proof :: forall f. ProvedGoal f -> Proof f
..}
  --  N.B. presentWithGoals takes care of expanding any lemma which mentions
  --  $equals, and flattening the proof.
  | Term f -> Bool
isFalseTerm Term f
u = [Derivation f] -> Maybe (String, Subst f, Equation f, Derivation f)
extract (Derivation f -> [Derivation f]
forall f. Function f => Derivation f -> [Derivation f]
steps Derivation f
deriv)
    -- Orient the equation so that $false is the RHS.
  | Term f -> Bool
isFalseTerm Term f
t = [Derivation f] -> Maybe (String, Subst f, Equation f, Derivation f)
extract (Derivation f -> [Derivation f]
forall f. Function f => Derivation f -> [Derivation f]
steps (Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm Derivation f
deriv))
  | Bool
otherwise = Maybe (String, Subst f, Equation f, Derivation f)
forall a. Maybe a
Nothing
  where
    isFalseTerm, isTrueTerm :: Term f -> Bool
    isFalseTerm :: Term f -> Bool
isFalseTerm (App Fun f
false TermList f
_) = Fun f -> Bool
forall f. EqualsBonus f => f -> Bool
isFalse Fun f
false
    isFalseTerm Term f
_ = Bool
False
    isTrueTerm :: Term f -> Bool
isTrueTerm (App Fun f
true TermList f
_) = Fun f -> Bool
forall f. EqualsBonus f => f -> Bool
isTrue Fun f
true
    isTrueTerm Term f
_ = Bool
False

    Term f
t :=: Term f
u = Proof f -> Equation f
forall f. Proof f -> Equation f
equation Proof f
pg_proof
    deriv :: Derivation f
deriv = Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
pg_proof

    -- Detect $true = $equals(t, t).
    decodeReflexivity :: Derivation f -> Maybe (Term f)
    decodeReflexivity :: Derivation f -> Maybe (Term f)
decodeReflexivity (Symm (UseAxiom Axiom{Int
String
Equation f
axiom_eqn :: Equation f
axiom_name :: String
axiom_number :: Int
axiom_eqn :: forall f. Axiom f -> Equation f
axiom_name :: forall f. Axiom f -> String
axiom_number :: forall f. Axiom f -> Int
..} Subst f
sub)) = do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term f -> Bool
isTrueTerm (Equation f -> Term f
forall f. Equation f -> Term f
eqn_rhs Equation f
axiom_eqn))
      (Term f
t :=: Term f
u) <- Term f -> Maybe (Equation f)
forall f. Function f => Term f -> Maybe (Equation f)
decodeEquality (Equation f -> Term f
forall f. Equation f -> Term f
eqn_lhs Equation f
axiom_eqn)
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u)
      Term f -> Maybe (Term f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst f -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
t)
    decodeReflexivity Derivation f
_ = Maybe (Term f)
forall a. Maybe a
Nothing

    -- Detect $equals(t, u) = $false.
    decodeConjecture :: Derivation f -> Maybe (String, Equation f, Subst f)
    decodeConjecture :: Derivation f -> Maybe (String, Equation f, Subst f)
decodeConjecture (UseAxiom Axiom{Int
String
Equation f
axiom_eqn :: Equation f
axiom_name :: String
axiom_number :: Int
axiom_eqn :: forall f. Axiom f -> Equation f
axiom_name :: forall f. Axiom f -> String
axiom_number :: forall f. Axiom f -> Int
..} Subst f
sub) = do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term f -> Bool
isFalseTerm (Equation f -> Term f
forall f. Equation f -> Term f
eqn_rhs Equation f
axiom_eqn))
      Equation f
eqn <- Term f -> Maybe (Equation f)
forall f. Function f => Term f -> Maybe (Equation f)
decodeEquality (Equation f -> Term f
forall f. Equation f -> Term f
eqn_lhs Equation f
axiom_eqn)
      (String, Equation f, Subst f)
-> Maybe (String, Equation f, Subst f)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
axiom_name, Equation f
eqn, Subst f
sub)
    decodeConjecture Derivation f
_ = Maybe (String, Equation f, Subst f)
forall a. Maybe a
Nothing

    extract :: [Derivation f] -> Maybe (String, Subst f, Equation f, Derivation f)
extract (Derivation f
p:[Derivation f]
ps) = do
      -- Start by finding $true = $equals(t,u).
      Term f
t <- Derivation f -> Maybe (Term f)
decodeReflexivity Derivation f
p
      Derivation f
-> Derivation f
-> [Derivation f]
-> Maybe (String, Subst f, Equation f, Derivation f)
cont (Term f -> Derivation f
forall f. Term f -> Derivation f
Refl Term f
t) (Term f -> Derivation f
forall f. Term f -> Derivation f
Refl Term f
t) [Derivation f]
ps
    extract [] = Maybe (String, Subst f, Equation f, Derivation f)
forall a. Maybe a
Nothing

    cont :: Derivation f
-> Derivation f
-> [Derivation f]
-> Maybe (String, Subst f, Equation f, Derivation f)
cont Derivation f
p1 Derivation f
p2 (Derivation f
p:[Derivation f]
ps)
      | Just Term f
t <- Derivation f -> Maybe (Term f)
decodeReflexivity Derivation f
p =
        Derivation f
-> Derivation f
-> [Derivation f]
-> Maybe (String, Subst f, Equation f, Derivation f)
cont (Term f -> Derivation f
forall f. Term f -> Derivation f
Refl Term f
t) (Term f -> Derivation f
forall f. Term f -> Derivation f
Refl Term f
t) [Derivation f]
ps
      | Just (String
name, Equation f
eqn, Subst f
sub) <- Derivation f -> Maybe (String, Equation f, Subst f)
decodeConjecture Derivation f
p =
        -- If p1: s=t and p2: s=u
        -- then symm p1 `trans` p2: t=u.
        (String, Subst f, Equation f, Derivation f)
-> Maybe (String, Subst f, Equation f, Derivation f)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
name, Subst f
sub, Equation f
eqn, Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
symm Derivation f
p1 Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`trans` Derivation f
p2)
      | Cong Fun f
eq [Derivation f
p1', Derivation f
p2'] <- Derivation f
p, Fun f -> Bool
forall f. EqualsBonus f => f -> Bool
isEquals Fun f
eq =
        Derivation f
-> Derivation f
-> [Derivation f]
-> Maybe (String, Subst f, Equation f, Derivation f)
cont (Derivation f
p1 Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`trans` Derivation f
p1') (Derivation f
p2 Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`trans` Derivation f
p2') [Derivation f]
ps
    cont Derivation f
_ Derivation f
_ [Derivation f]
_ = Maybe (String, Subst f, Equation f, Derivation f)
forall a. Maybe a
Nothing