{-# LANGUAGE TypeFamilies, PatternGuards, RecordWildCards, ScopedTypeVariables, OverloadedStrings #-}
module Twee.Proof(
Proof, Derivation(..), Axiom(..),
certify, equation, derivation,
lemma, autoSubst, simpleLemma, axiom, symm, trans, cong, congPath,
simplify, steps, usedLemmas, usedAxioms, usedLemmasAndSubsts, usedAxiomsAndSubsts,
groundAxiomsAndSubsts, eliminateDefinitions, eliminateDefinitionsFromGoal,
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
data Proof f =
Proof {
forall f. Proof f -> Equation f
equation :: !(Equation f),
forall f. Proof f -> Derivation f
derivation :: !(Derivation f) }
deriving Int -> Proof f -> ShowS
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
data Derivation f =
UseLemma {-# UNPACK #-} !(Proof f) !(Subst f)
| UseAxiom {-# UNPACK #-} !(Axiom f) !(Subst f)
| Refl !(Term f)
| Symm !(Derivation f)
| Trans !(Derivation f) !(Derivation f)
| Cong {-# UNPACK #-} !(Fun f) ![Derivation f]
deriving (Derivation f -> Derivation f -> Bool
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
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)
data Axiom f =
Axiom {
forall f. Axiom f -> Int
axiom_number :: {-# UNPACK #-} !Int,
forall f. Axiom f -> String
axiom_name :: !String,
forall f. Axiom f -> Equation f
axiom_eqn :: !(Equation f) }
deriving (Axiom f -> Axiom f -> Bool
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, Axiom f -> Axiom f -> Bool
Axiom f -> Axiom f -> Ordering
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
Ord, Int -> Axiom f -> ShowS
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)
{-# INLINEABLE certify #-}
certify :: Function f => Derivation f -> Proof f
certify :: forall f. Function f => Derivation f -> Proof f
certify Derivation f
p =
forall symbol a. symbol -> a -> a
stamp String
"certify proof" forall a b. (a -> b) -> a -> b
$
case forall {m :: * -> *} {t}.
(Monad m, Alternative m) =>
Derivation t -> m (Equation t)
check Derivation f
p of
Maybe (Equation f)
Nothing -> forall a. HasCallStack => String -> a
error (String
"Invalid proof created!\n" forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Derivation f
p)
Just Equation f
eqn -> forall f. Equation f -> Derivation f -> Proof f
Proof Equation f
eqn Derivation f
p
where
check :: Derivation (BuildFun (Builder (BuildFun (Builder t))))
-> m (Equation (BuildFun (Builder (BuildFun (Builder t)))))
check (UseLemma Proof (BuildFun (Builder (BuildFun (Builder t))))
proof Subst (BuildFun (Builder (BuildFun (Builder t))))
sub) =
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (BuildFun (Builder (BuildFun (Builder t))))
sub (forall f. Proof f -> Equation f
equation Proof (BuildFun (Builder (BuildFun (Builder t))))
proof))
check (UseAxiom Axiom{Int
String
Equation (BuildFun (Builder (BuildFun (Builder t))))
axiom_eqn :: Equation (BuildFun (Builder (BuildFun (Builder t))))
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 (BuildFun (Builder (BuildFun (Builder t))))
sub) =
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (BuildFun (Builder (BuildFun (Builder t))))
sub Equation (BuildFun (Builder (BuildFun (Builder t))))
axiom_eqn)
check (Refl Term (BuildFun (Builder (BuildFun (Builder t))))
t) =
forall (m :: * -> *) a. Monad m => a -> m a
return (Term (BuildFun (Builder (BuildFun (Builder t))))
t forall f. Term f -> Term f -> Equation f
:=: Term (BuildFun (Builder (BuildFun (Builder t))))
t)
check (Symm Derivation (BuildFun (Builder (BuildFun (Builder t))))
p) = do
Term (BuildFun (Builder (BuildFun (Builder t))))
t :=: Term (BuildFun (Builder (BuildFun (Builder t))))
u <- Derivation (BuildFun (Builder (BuildFun (Builder t))))
-> m (Equation (BuildFun (Builder (BuildFun (Builder t)))))
check Derivation (BuildFun (Builder (BuildFun (Builder t))))
p
forall (m :: * -> *) a. Monad m => a -> m a
return (Term (BuildFun (Builder (BuildFun (Builder t))))
u forall f. Term f -> Term f -> Equation f
:=: Term (BuildFun (Builder (BuildFun (Builder t))))
t)
check (Trans Derivation (BuildFun (Builder (BuildFun (Builder t))))
p Derivation (BuildFun (Builder (BuildFun (Builder t))))
q) = do
Term (BuildFun (Builder (BuildFun (Builder t))))
t :=: Term (BuildFun (Builder (BuildFun (Builder t))))
u1 <- Derivation (BuildFun (Builder (BuildFun (Builder t))))
-> m (Equation (BuildFun (Builder (BuildFun (Builder t)))))
check Derivation (BuildFun (Builder (BuildFun (Builder t))))
p
Term (BuildFun (Builder (BuildFun (Builder t))))
u2 :=: Term (BuildFun (Builder (BuildFun (Builder t))))
v <- Derivation (BuildFun (Builder (BuildFun (Builder t))))
-> m (Equation (BuildFun (Builder (BuildFun (Builder t)))))
check Derivation (BuildFun (Builder (BuildFun (Builder t))))
q
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term (BuildFun (Builder (BuildFun (Builder t))))
u1 forall a. Eq a => a -> a -> Bool
== Term (BuildFun (Builder (BuildFun (Builder t))))
u2)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term (BuildFun (Builder (BuildFun (Builder t))))
t forall f. Term f -> Term f -> Equation f
:=: Term (BuildFun (Builder (BuildFun (Builder t))))
v)
check (Cong Fun (BuildFun (Builder (BuildFun (Builder t))))
f [Derivation (BuildFun (Builder (BuildFun (Builder t))))]
ps) = do
[Equation (BuildFun (Builder (BuildFun (Builder t))))]
eqns <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Derivation (BuildFun (Builder (BuildFun (Builder t))))
-> m (Equation (BuildFun (Builder (BuildFun (Builder t)))))
check [Derivation (BuildFun (Builder (BuildFun (Builder t))))]
ps
forall (m :: * -> *) a. Monad m => a -> m a
return
(forall a. Build a => a -> Term (BuildFun a)
build (forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun (BuildFun (Builder (BuildFun (Builder t))))
f (forall a b. (a -> b) -> [a] -> [b]
map forall f. Equation f -> Term f
eqn_lhs [Equation (BuildFun (Builder (BuildFun (Builder t))))]
eqns)) forall f. Term f -> Term f -> Equation f
:=:
forall a. Build a => a -> Term (BuildFun a)
build (forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun (BuildFun (Builder (BuildFun (Builder t))))
f (forall a b. (a -> b) -> [a] -> [b]
map forall f. Equation f -> Term f
eqn_rhs [Equation (BuildFun (Builder (BuildFun (Builder t))))]
eqns)))
instance Eq (Proof f) where
Proof f
x == :: Proof f -> Proof f -> Bool
== Proof f
y = forall a. Ord a => a -> a -> Ordering
compare Proof f
x Proof f
y forall a. Eq a => a -> a -> Bool
== Ordering
EQ
instance Ord (Proof f) where
compare :: Proof f -> Proof f -> Ordering
compare = forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing 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) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Subst f
sub
termsDL (UseAxiom Axiom f
_ Subst f
sub) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Subst f
sub
termsDL (Refl Term f
t) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Term f
t
termsDL (Symm Derivation f
p) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Derivation f
p
termsDL (Trans Derivation f
p Derivation f
q) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Derivation f
p forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Derivation f
q
termsDL (Cong Fun f
_ [Derivation f]
ps) = 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) = forall f. Proof f -> Subst f -> Derivation f
UseLemma Proof f
lemma (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Derivation f)
sub Subst f
s)
subst_ Var -> BuilderOf (Derivation f)
sub (UseAxiom Axiom f
axiom Subst f
s) = forall f. Axiom f -> Subst f -> Derivation f
UseAxiom Axiom f
axiom (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Derivation f)
sub Subst f
s)
subst_ Var -> BuilderOf (Derivation f)
sub (Refl Term f
t) = forall f. Term f -> Derivation f
Refl (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Derivation f)
sub Term f
t)
subst_ Var -> BuilderOf (Derivation f)
sub (Symm Derivation f
p) = forall f. Derivation f -> Derivation f
symm (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) = forall f. Derivation f -> Derivation f -> Derivation f
trans (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Derivation f)
sub Derivation f
p) (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) = forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Derivation f)
sub [Derivation f]
ps)
instance Function f => Pretty (Proof f) where
pPrint :: Proof f -> Doc
pPrint = forall f.
Function f =>
Config f
-> (Axiom f -> String) -> (Proof f -> String) -> Proof f -> Doc
pPrintLemma forall f. Config f
defaultConfig (forall a. Pretty a => a -> String
prettyShow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Axiom f -> Int
axiom_number) (forall a. Pretty a => a -> String
prettyShow forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
<+> forall a. Pretty a => a -> Doc
pPrint (forall f. Proof f -> Equation f
equation Proof f
lemma), 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 [forall a. Pretty a => a -> Doc
pPrint Axiom f
axiom, 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 [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 [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 [forall a. Pretty a => a -> Doc
pPrint Derivation f
p, 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 (forall a. Pretty a => a -> Doc
pPrint Fun f
fforall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map 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 [forall a. Pretty a => a -> Doc
pPrint Int
axiom_number, String -> Doc
text String
axiom_name, 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 :: forall f a.
(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
op [Derivation f]
ds =
forall s a. State s a -> s -> s
execState (forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Derivation f -> StateT (Map (Proof f) a) Identity ()
foldGoal [Derivation f]
ds) forall k a. Map k a
Map.empty
where
foldGoal :: Derivation f -> StateT (Map (Proof f) a) Identity ()
foldGoal Derivation f
p = 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 (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 <- forall (m :: * -> *) s. Monad m => StateT s m s
get
case 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return a
x
Maybe a
Nothing -> do
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 (forall f. Derivation f -> [Proof f]
usedLemmas (forall f. Proof f -> Derivation f
derivation Proof f
p))
Map (Proof f) a
m <- forall (m :: * -> *) s. Monad m => StateT s m s
get
case 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 -> 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 (forall f. Proof f -> Derivation f
derivation Proof f
p)
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (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)
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
mapLemmas :: Function f => (Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas :: forall f.
Function f =>
(Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas Derivation f -> Derivation f
f [Derivation f]
ds = forall a b. (a -> b) -> [a] -> [b]
map (forall f. Proof f -> Derivation f
derivation 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 = forall f. Function f => Derivation f -> Proof f
certify forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Derivation f
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f.
Minimal f =>
(Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas (\Proof f
pf -> forall a. a -> Maybe a
Just (forall f. Function f => Proof f -> Derivation f
simpleLemma (Map (Proof f) (Proof f)
lem forall k a. Ord k => Map k a -> k -> a
Map.! Proof f
pf)))
lem :: Map (Proof f) (Proof f)
lem = 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 :: forall f. Function f => [Derivation f] -> [Proof f]
allLemmas [Derivation f]
ds =
forall a. [a] -> [a]
reverse [Proof f
p | (()
_, Proof f
p, [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 = 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 -> 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
_) =
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) <- 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 :: forall f.
Minimal f =>
(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 ->
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub (forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
eraseExcept (forall f. Subst f -> [Var]
substDomain Subst f
sub) Derivation f
r)
unfoldLemmas Proof f -> Maybe (Derivation f)
lem (Symm Derivation f
p) = forall f. Derivation f -> Derivation f
symm (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) = forall f. Derivation f -> Derivation f -> Derivation f
trans (forall f.
Minimal f =>
(Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas Proof f -> Maybe (Derivation f)
lem Derivation f
p) (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) = forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f (forall a b. (a -> b) -> [a] -> [b]
map (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 :: forall f. Proof f -> Subst f -> Derivation f
lemma Proof f
p Subst f
sub = forall f. Proof f -> Subst f -> Derivation f
UseLemma Proof f
p Subst f
sub
simpleLemma :: Function f => Proof f -> Derivation f
simpleLemma :: forall f. Function f => Proof f -> Derivation f
simpleLemma Proof f
p =
forall f. Proof f -> Subst f -> Derivation f
UseLemma Proof f
p (forall f. Equation f -> Subst f
autoSubst (forall f. Proof f -> Equation f
equation Proof f
p))
axiom :: Axiom f -> Derivation f
axiom :: forall f. 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
..} =
forall f. Axiom f -> Subst f -> Derivation f
UseAxiom Axiom f
ax (forall f. Equation f -> Subst f
autoSubst Equation f
axiom_eqn)
autoSubst :: Equation f -> Subst f
autoSubst :: forall f. Equation f -> Subst f
autoSubst Equation f
eqn =
forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$
forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst [(Var
x, forall a. Build a => a -> Term (BuildFun a)
build (forall f. Var -> Builder f
var Var
x)) | Var
x <- forall a. Symbolic a => a -> [Var]
vars Equation f
eqn]
symm :: Derivation f -> Derivation f
symm :: forall f. Derivation f -> Derivation f
symm (Refl Term f
t) = 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) = forall f. Derivation f -> Derivation f -> Derivation f
trans (forall f. Derivation f -> Derivation f
symm Derivation f
q) (forall f. Derivation f -> Derivation f
symm Derivation f
p)
symm (Cong Fun f
f [Derivation f]
ps) = forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f (forall a b. (a -> b) -> [a] -> [b]
map forall f. Derivation f -> Derivation f
symm [Derivation f]
ps)
symm Derivation f
p = forall f. Derivation f -> Derivation f
Symm Derivation f
p
trans :: Derivation f -> Derivation f -> Derivation f
trans :: forall f. 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 =
forall f. Derivation f -> Derivation f -> Derivation f
Trans Derivation f
p (forall f. Derivation f -> Derivation f -> Derivation f
trans Derivation f
q Derivation f
r)
trans Derivation f
p Derivation f
q = forall f. Derivation f -> Derivation f -> Derivation f
Trans Derivation f
p Derivation f
q
cong :: Fun f -> [Derivation f] -> Derivation f
cong :: forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f [Derivation f]
ps =
case forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall a b. (a -> b) -> [a] -> [b]
map forall {f}. Derivation f -> Maybe (Term f)
unRefl [Derivation f]
ps) of
Maybe [Term f]
Nothing -> forall f. Fun f -> [Derivation f] -> Derivation f
Cong Fun f
f [Derivation f]
ps
Just [Term f]
ts -> forall f. Term f -> Derivation f
Refl (forall a. Build a => a -> Term (BuildFun a)
build (forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
f [Term f]
ts))
where
unRefl :: Derivation f -> Maybe (Term f)
unRefl (Refl Term f
t) = forall a. a -> Maybe a
Just Term f
t
unRefl Derivation f
_ = forall a. Maybe a
Nothing
flattenDerivation :: Function f => Derivation f -> Derivation f
flattenDerivation :: forall f. Function f => Derivation f -> Derivation f
flattenDerivation Derivation f
p =
forall f. Equation f -> [Derivation f] -> Derivation f
fromSteps (forall f. Proof f -> Equation f
equation (forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)) (forall f. Function f => Derivation f -> [Derivation f]
steps Derivation f
p)
simplify :: Function f => Derivation f -> Derivation f
simplify :: forall f. Function f => Derivation f -> Derivation f
simplify (Symm Derivation f
p) = forall f. Derivation f -> Derivation f
symm (forall f. Function f => Derivation f -> Derivation f
simplify Derivation f
p)
simplify (Trans Derivation f
p Derivation f
q) = forall f. Derivation f -> Derivation f -> Derivation f
trans (forall f. Function f => Derivation f -> Derivation f
simplify Derivation f
p) (forall f. Function f => Derivation f -> Derivation f
simplify Derivation f
q)
simplify (Cong Fun f
f [Derivation f]
ps) = forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f (forall a b. (a -> b) -> [a] -> [b]
map forall f. Function f => Derivation f -> Derivation f
simplify [Derivation f]
ps)
simplify Derivation f
p
| Term f
t forall a. Eq a => a -> a -> Bool
== Term f
u = forall f. Term f -> Derivation f
Refl Term f
t
| Bool
otherwise = Derivation f
p
where
Term f
t :=: Term f
u = forall f. Proof f -> Equation f
equation (forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)
steps :: Function f => Derivation f -> [Derivation f]
steps :: forall f. Function f => Derivation f -> [Derivation f]
steps = forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
Derivation f -> [Derivation f]
steps1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall a b. (a -> b) -> [a] -> [b]
map forall f. Derivation f -> Derivation f
symm (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 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) =
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ 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) <- 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 = forall f. Proof f -> Equation f
equation (forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)
inside :: Int -> Derivation f -> Derivation f
inside Int
i Derivation f
p =
forall f. Fun f -> [Derivation f] -> Derivation f
Cong Fun f
f forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map forall f. Term f -> Derivation f
Refl (forall a. Int -> [a] -> [a]
take Int
i (forall f. TermList f -> [Term f]
unpack TermList f
us)) forall a. [a] -> [a] -> [a]
++
[Derivation f
p] forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map forall f. Term f -> Derivation f
Refl (forall a. Int -> [a] -> [a]
drop (Int
iforall a. Num a => a -> a -> a
+Int
1) (forall f. TermList f -> [Term f]
unpack TermList f
ts))
fromSteps :: Equation f -> [Derivation f] -> Derivation f
fromSteps :: forall f. Equation f -> [Derivation f] -> Derivation f
fromSteps (Term f
t :=: Term f
_) [] = forall f. Term f -> Derivation f
Refl Term f
t
fromSteps Equation f
_ [Derivation f]
ps = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall f. Derivation f -> Derivation f -> Derivation f
Trans [Derivation f]
ps
usedLemmas :: Derivation f -> [Proof f]
usedLemmas :: forall f. Derivation f -> [Proof f]
usedLemmas Derivation f
p = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall f. Derivation f -> [(Proof f, Subst f)]
usedLemmasAndSubsts Derivation f
p)
usedLemmasAndSubsts :: Derivation f -> [(Proof f, Subst f)]
usedLemmasAndSubsts :: forall f. Derivation f -> [(Proof f, Subst f)]
usedLemmasAndSubsts Derivation f
p = 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)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 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) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id (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
_ = forall a. a -> a
id
usedAxioms :: Derivation f -> [Axiom f]
usedAxioms :: forall f. Derivation f -> [Axiom f]
usedAxioms Derivation f
p = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall f. Derivation f -> [(Axiom f, Subst f)]
usedAxiomsAndSubsts Derivation f
p)
usedAxiomsAndSubsts :: Derivation f -> [(Axiom f, Subst f)]
usedAxiomsAndSubsts :: forall f. Derivation f -> [(Axiom f, Subst f)]
usedAxiomsAndSubsts Derivation f
p = 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)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 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) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id (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
_ = forall a. a -> a
id
groundAxiomsAndSubsts :: Function f => Derivation f -> Map (Axiom f) (Set (Subst f))
groundAxiomsAndSubsts :: forall f.
Function f =>
Derivation f -> Map (Axiom f) (Set (Subst f))
groundAxiomsAndSubsts Derivation f
p = 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 = forall f a.
(Labelled f, PrettyTerm f) =>
(Map (Proof f) a -> Derivation f -> a)
-> [Derivation f] -> Map (Proof f) a
foldLemmas 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) =
forall k a. k -> a -> Map k a
Map.singleton Axiom f
axiom (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) =
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (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 forall k a. Ord k => Map k a -> k -> a
Map.! Proof f
lemma)
where
substAndErase :: Subst f -> Subst f
substAndErase Subst f
sub' =
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
eraseExcept (forall a. Symbolic a => a -> [Var]
vars Subst f
sub) (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) = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith 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) = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Ord a => Set a -> Set a -> Set a
Set.union (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
_ = forall k a. Map k a
Map.empty
eliminateDefinitionsFromGoal :: Function f => [Axiom f] -> ProvedGoal f -> ProvedGoal f
eliminateDefinitionsFromGoal :: forall f. Function f => [Axiom f] -> ProvedGoal f -> ProvedGoal f
eliminateDefinitionsFromGoal [Axiom f]
axioms ProvedGoal f
pg =
ProvedGoal f
pg {
pg_proof :: Proof f
pg_proof = forall f. Function f => Derivation f -> Proof f
certify (forall f. Function f => [Axiom f] -> Derivation f -> Derivation f
eliminateDefinitions [Axiom f]
axioms (forall f. Proof f -> Derivation f
derivation (forall f. ProvedGoal f -> Proof f
pg_proof ProvedGoal f
pg))) }
eliminateDefinitions :: Function f => [Axiom f] -> Derivation f -> Derivation f
eliminateDefinitions :: forall f. Function f => [Axiom f] -> Derivation f -> Derivation f
eliminateDefinitions [] Derivation f
p = Derivation f
p
eliminateDefinitions [Axiom f]
axioms Derivation f
p = forall a. [a] -> a
head (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 forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Axiom f)
axSet =
forall f. Term f -> Derivation f
Refl (Term f -> Term f
term (forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub (forall f. Equation f -> Term f
eqn_rhs (forall f. Axiom f -> Equation f
axiom_eqn Axiom f
axiom))))
| Bool
otherwise = 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) =
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) = forall f. Term f -> Derivation f
Refl (Term f -> Term f
term Term f
t)
elim (Symm Derivation f
p) = forall f. Derivation f -> Derivation f
Symm (Derivation f -> Derivation f
elim Derivation f
p)
elim (Trans Derivation f
p Derivation f
q) = 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 (forall a. Build a => a -> Term (BuildFun a)
build (forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
f (forall a b. (a -> b) -> [a] -> [b]
map forall f. Var -> Builder f
var [Var]
vs))) of
Maybe (Term f, Subst f)
Nothing -> forall f. Fun f -> [Derivation f] -> Derivation f
Cong Fun f
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 forall a. [a] -> Int -> a
!! Int
x in
forall {f}. IntMap (Derivation f) -> Term f -> Derivation f
replace (TermList f -> Derivation f
proof forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap (TermList f)
sub) Term f
rhs
where
vs :: [Var]
vs = forall a b. (a -> b) -> [a] -> [b]
map Int -> Var
V [Int
0..forall (t :: * -> *) a. Foldable t => t a -> Int
length [Derivation f]
psforall a. Num a => a -> a -> a
-Int
1]
qs :: [Derivation f]
qs = forall a b. (a -> b) -> [a] -> [b]
map (forall f. Function f => Proof f -> Derivation f
simpleLemma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Function f => Derivation f -> Proof f
certify forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation f -> Derivation f
elim) [Derivation f]
ps
elimSubst :: Subst f -> Subst f
elimSubst (Subst IntMap (TermList f)
sub) = forall f. IntMap (TermList f) -> Subst f
Subst (forall f. Term f -> TermList f
singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f -> Term f
term forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {f}. TermList f -> Term f
unsingleton 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 = forall a. Build a => a -> Term (BuildFun a)
build forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> Builder f
term'
term' :: Term f -> Builder f
term' (Var Var
x) = 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 -> forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
f (forall a b. (a -> b) -> [a] -> [b]
map Term f -> Builder f
term' (forall f. TermList f -> [Term f]
unpack TermList f
ts))
Just (Term f
rhs, Subst f
sub) ->
Term f -> Builder f
term' (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 =
forall a. [a] -> Maybe a
listToMaybe 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
_) <- 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 = forall f. Term f -> Term f -> Maybe (Subst f)
match Term f
l Term f
t
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)) =
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault forall a. HasCallStack => a
undefined Int
x IntMap (Derivation f)
sub
replace IntMap (Derivation f)
sub (App Fun f
f TermList f
ts) =
forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f (forall a b. (a -> b) -> [a] -> [b]
map (IntMap (Derivation f) -> Term f -> Derivation f
replace IntMap (Derivation f)
sub) (forall f. TermList f -> [Term f]
unpack TermList f
ts))
axSet :: Set (Axiom f)
axSet = forall a. Ord a => [a] -> Set a
Set.fromList [Axiom f]
axioms
idx :: Index f (Derivation f)
idx = forall a f.
(Symbolic a, ConstantOf a ~ f) =>
[(Term f, a)] -> Index f a
Index.fromList [(forall f. Equation f -> Term f
eqn_lhs (forall f. Axiom f -> Equation f
axiom_eqn Axiom f
ax), forall f. Axiom f -> Derivation f
axiom Axiom f
ax) | Axiom f
ax <- [Axiom f]
axioms]
congPath :: [Int] -> Term f -> Derivation f -> Derivation f
congPath :: forall f. [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 forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term f]
ts =
forall f. Fun f -> [Derivation f] -> Derivation f
cong Fun f
f forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map forall f. Term f -> Derivation f
Refl (forall a. Int -> [a] -> [a]
take Int
n [Term f]
ts) forall a. [a] -> [a] -> [a]
++
[forall f. [Int] -> Term f -> Derivation f -> Derivation f
congPath [Int]
ns ([Term f]
ts forall a. [a] -> Int -> a
!! Int
n) Derivation f
p] forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map forall f. Term f -> Derivation f
Refl (forall a. Int -> [a] -> [a]
drop (Int
nforall a. Num a => a -> a -> a
+Int
1) [Term f]
ts)
where
ts :: [Term f]
ts = forall f. TermList f -> [Term f]
unpack TermList f
t
congPath [Int]
_ Term f
_ Derivation f
_ = forall a. HasCallStack => String -> a
error String
"bad path"
data Config f =
Config {
forall f. Config f -> Bool
cfg_all_lemmas :: !Bool,
forall f. Config f -> Bool
cfg_no_lemmas :: !Bool,
forall f. Config f -> Bool
cfg_ground_proof :: !Bool,
forall f. Config f -> Bool
cfg_show_instances :: !Bool,
forall f. Config f -> Bool
cfg_use_colour :: !Bool,
forall f. Config f -> Axiom f -> Bool
cfg_show_uses_of_axioms :: Axiom f -> Bool }
defaultConfig :: Config f
defaultConfig :: forall f. Config f
defaultConfig =
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 = forall a b. a -> b -> a
const Bool
False }
data Presentation f =
Presentation {
forall f. Presentation f -> [Axiom f]
pres_axioms :: [Axiom f],
forall f. Presentation f -> [Proof f]
pres_lemmas :: [Proof f],
forall f. Presentation f -> [ProvedGoal f]
pres_goals :: [ProvedGoal f] }
deriving Int -> Presentation f -> ShowS
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
data ProvedGoal f =
ProvedGoal {
forall f. ProvedGoal f -> Int
pg_number :: Int,
forall f. ProvedGoal f -> String
pg_name :: String,
forall f. ProvedGoal f -> Proof f
pg_proof :: Proof f,
forall f. ProvedGoal f -> Equation f
pg_goal_hint :: Equation f,
forall f. ProvedGoal f -> Subst f
pg_witness_hint :: Subst f }
deriving Int -> ProvedGoal f -> ShowS
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
provedGoal :: Int -> String -> Proof f -> ProvedGoal f
provedGoal :: forall f. Int -> String -> Proof f -> ProvedGoal f
provedGoal Int
number String
name Proof f
proof =
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 = forall f. Proof f -> Equation f
equation Proof f
proof,
pg_witness_hint :: Subst f
pg_witness_hint = forall f. Subst f
emptySubst }
checkProvedGoal :: Function f => ProvedGoal f -> ProvedGoal f
checkProvedGoal :: forall f. Function f => 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
..}
| 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 forall a. Eq a => a -> a -> Bool
== forall f. Proof f -> Equation f
equation Proof f
pg_proof =
ProvedGoal f
pg
| Bool
otherwise =
forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show 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
<+> forall a. Pretty a => a -> Doc
pPrint Equation f
pg_goal_hint Doc -> Doc -> Doc
$$
String -> Doc
text String
"with witness" Doc -> Doc -> 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
<+> forall a. Pretty a => a -> Doc
pPrint (forall f. Proof f -> Equation f
equation Proof f
pg_proof)
instance Function f => Pretty (Presentation f) where
pPrint :: Presentation f -> Doc
pPrint = forall f. Function f => Config f -> Presentation f -> Doc
pPrintPresentation forall f. Config f
defaultConfig
present :: Function f => Config f -> [ProvedGoal f] -> Presentation f
present :: forall f.
Function f =>
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 =
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 =
forall f.
Function f =>
(Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas forall f. Function f => Derivation f -> Derivation f
flattenDerivation forall a b. (a -> b) -> a -> b
$
forall f.
Function f =>
Config f -> [Derivation f] -> [Derivation f]
simplifyProof Config f
config forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall f. Proof f -> Derivation f
derivation forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. ProvedGoal f -> Proof f
pg_proof) [ProvedGoal f]
goals
goals' :: [ProvedGoal f]
goals' =
[ forall f. Function f => ProvedGoal f -> ProvedGoal f
decodeGoal (ProvedGoal f
goal{pg_proof :: Proof f
pg_proof = forall f. Function f => Derivation f -> Proof f
certify Derivation f
p})
| (ProvedGoal f
goal, Derivation f
p) <- forall a b. [a] -> [b] -> [(a, b)]
zip [ProvedGoal f]
goals [Derivation f]
ps ]
axioms :: [Axiom f]
axioms = forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall f. Derivation f -> [Axiom f]
usedAxioms forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Proof f -> Derivation f
derivation forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. ProvedGoal f -> Proof f
pg_proof) [ProvedGoal f]
goals' forall a. [a] -> [a] -> [a]
++
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall f. Derivation f -> [Axiom f]
usedAxioms forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Proof f -> Derivation f
derivation) [Proof f]
lemmas
lemmas :: [Proof f]
lemmas = forall f. Function f => [Derivation f] -> [Proof f]
allLemmas (forall a b. (a -> b) -> [a] -> [b]
map (forall f. Proof f -> Derivation f
derivation forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. ProvedGoal f -> Proof f
pg_proof) [ProvedGoal f]
goals')
groundProof :: Function f => [Derivation f] -> [Derivation f]
groundProof :: forall f. Function f => [Derivation f] -> [Derivation f]
groundProof [Derivation f]
ds
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Symbolic a => a -> Bool
isGround forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Proof f -> Equation f
equation) (forall f. Function f => [Derivation f] -> [Proof f]
allLemmas [Derivation f]
ds) = [Derivation f]
ds
| Bool
otherwise = forall f. Function f => [Derivation f] -> [Derivation f]
groundProof (forall f.
Function f =>
(Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas forall {f}.
(Ordered 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) =
forall f. Function f => Proof f -> Derivation f
simpleLemma forall a b. (a -> b) -> a -> b
$ forall f. Function f => Derivation f -> Proof f
certify forall a b. (a -> b) -> a -> b
$
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
eraseExcept (forall a. Symbolic a => a -> [Var]
vars Subst f
sub) forall a b. (a -> b) -> a -> b
$
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub forall a b. (a -> b) -> a -> b
$
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) = forall f. Derivation f -> Derivation f
Symm (Derivation f -> Derivation f
f Derivation f
p)
f (Trans Derivation f
p Derivation f
q) = 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) = forall f. Fun f -> [Derivation f] -> Derivation f
Cong Fun f
fun (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 :: forall f.
Function f =>
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 =
forall f. Function f => [Derivation f] -> [Derivation f]
canonicaliseLemmas (forall b a. Eq b => (a -> b) -> (a -> a) -> a -> a
fixpointOn forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
[Derivation f] -> ([Derivation f], [(Equation f, Derivation f)])
key [Derivation f] -> [Derivation f]
simp' (forall b a. Eq b => (a -> b) -> (a -> a) -> a -> a
fixpointOn forall {f}.
(Ordered 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 =
(forall f. Function f => [Derivation f] -> [Derivation f]
inlineUsedOnceLemmas forall {a}. (a -> a) -> Bool -> a -> a
`onlyIf` Bool -> Bool
not Bool
cfg_all_lemmas) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall f.
Function f =>
Config f -> [Derivation f] -> [Derivation f]
inlineTrivialLemmas Config f
config forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall f. Function f => [Derivation f] -> [Derivation f]
tightenProof
simp :: [Derivation f] -> [Derivation f]
simp = [Derivation f] -> [Derivation f]
simpCore forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Function f => [Derivation f] -> [Derivation f]
generaliseProof
simp' :: [Derivation f] -> [Derivation f]
simp' = ([Derivation f] -> [Derivation f]
simpCore forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Function f => [Derivation f] -> [Derivation f]
groundProof) 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, [(forall f. Proof f -> Equation f
equation Proof f
p, forall f. Proof f -> Derivation f
derivation Proof f
p) | Proof f
p <- 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 = forall a. a -> a
id
simplificationPass ::
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 :: 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
lemma Map (Proof f) (Derivation f) -> Derivation f -> Derivation f
goal [Derivation f]
p = forall a b. (a -> b) -> [a] -> [b]
map (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 = forall f a.
(Labelled f, PrettyTerm f) =>
(Map (Proof f) a -> Derivation f -> a)
-> [Derivation f] -> Map (Proof f) a
foldLemmas (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall f.
Minimal f =>
(Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
unfoldLemmas (\Proof f
lemma -> forall a. a -> Maybe a
Just (Map (Proof f) (Derivation f)
lem 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 :: forall f.
Function f =>
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
..} =
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 (forall a b. a -> b -> a
const 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 = forall f. Proof f -> Derivation f
derivation Proof f
p
| (Derivation f
q:[Derivation f]
_) <- forall {f}.
Map (Proof f) (Derivation f) -> Equation f -> [Derivation f]
subsuming Map (Proof f) (Derivation f)
lem (forall f. Proof f -> Equation f
equation Proof f
p) = Derivation f
q
| Bool
otherwise = 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
||
forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Function f => Equation f -> Bool
invisible) (forall a b. (a -> b) -> [a] -> [b]
map (forall f. Proof f -> Equation f
equation forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Function f => Derivation f -> Proof f
certify) (forall f. Function f => Derivation f -> [Derivation f]
steps (forall f. Proof f -> Derivation f
derivation Proof f
p)))) forall a. Ord a => a -> a -> Bool
<= Int
1 Bool -> Bool -> Bool
||
(Bool -> Bool
not Bool
cfg_all_lemmas Bool -> Bool -> Bool
&&
(forall a. Maybe a -> Bool
isJust (forall f. Function f => Term f -> Maybe (Equation f)
decodeEquality (forall f. Equation f -> Term f
eqn_lhs (forall f. Proof f -> Equation f
equation Proof f
p))) Bool -> Bool -> Bool
||
forall a. Maybe a -> Bool
isJust (forall f. Function f => Term f -> Maybe (Equation f)
decodeEquality (forall f. Equation f -> Term f
eqn_rhs (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) =
forall {a}.
Symbolic a =>
Map (Proof (ConstantOf a)) a -> Equation (ConstantOf a) -> [a]
subsuming1 Map (Proof f) (Derivation f)
lem (Term f
t forall f. Term f -> Term f -> Equation f
:=: Term f
u) forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map forall f. Derivation f -> Derivation f
symm (forall {a}.
Symbolic a =>
Map (Proof (ConstantOf a)) a -> Equation (ConstantOf a) -> [a]
subsuming1 Map (Proof f) (Derivation f)
lem (Term f
u 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 =
[ 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) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (Proof (ConstantOf a)) a
lem,
Subst (ConstantOf a)
sub <- forall a. Maybe a -> [a]
maybeToList (forall f. Equation f -> Equation f -> Maybe (Subst f)
matchEquation (forall f. Proof f -> Equation f
equation Proof (ConstantOf a)
q) Equation (ConstantOf a)
eq) ]
inlineUsedOnceLemmas :: Function f => [Derivation f] -> [Derivation f]
inlineUsedOnceLemmas :: forall f. Function f => [Derivation f] -> [Derivation f]
inlineUsedOnceLemmas [Derivation f]
ds =
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 (forall a b. a -> b -> a
const Proof f -> Derivation f
inlineOnce) (forall a b. a -> b -> a
const forall a. a -> a
id) [Derivation f]
ds
where
uses :: Map (Proof f) Int
uses = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Num a => a -> a -> a
(+) forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map forall {f}. Derivation f -> Map (Proof f) Int
countUses [Derivation f]
ds forall a. [a] -> [a] -> [a]
++ forall k a. Map k a -> [a]
Map.elems (forall f a.
(Labelled f, PrettyTerm f) =>
(Map (Proof f) a -> Derivation f -> a)
-> [Derivation f] -> Map (Proof f) a
foldLemmas (forall a b. a -> b -> a
const forall {f}. Derivation f -> Map (Proof f) Int
countUses) [Derivation f]
ds)
countUses :: Derivation f -> Map (Proof f) Int
countUses Derivation f
p =
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. Num a => a -> a -> a
(+) (forall a b. [a] -> [b] -> [(a, b)]
zip (forall f. Derivation f -> [Proof f]
usedLemmas Derivation f
p) (forall a. a -> [a]
repeat (Int
1 :: Int)))
inlineOnce :: Proof f -> Derivation f
inlineOnce Proof f
p
| Proof f -> Bool
usedOnce Proof f
p = forall f. Proof f -> Derivation f
derivation Proof f
p
| Bool
otherwise = forall f. Function f => Proof f -> Derivation f
simpleLemma Proof f
p
where
usedOnce :: Proof f -> Bool
usedOnce Proof f
p =
case 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 :: forall f. Function f => [Derivation f] -> [Derivation f]
tightenProof = forall f.
Function f =>
(Derivation f -> Derivation f) -> [Derivation f] -> [Derivation f]
mapLemmas forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
Derivation f -> Derivation f
tightenLemma
where
tightenLemma :: Derivation f -> Derivation f
tightenLemma Derivation f
p =
forall f. Equation f -> [Derivation f] -> Derivation f
fromSteps Equation f
eq (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall b a. Eq b => (a -> b) -> (a -> a) -> a -> a
fixpointOn forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall {a}.
Symbolic a =>
Equation (ConstantOf a)
-> [(a, Equation (ConstantOf a))] -> [(a, Equation (ConstantOf a))]
tightenSteps Equation f
eq) (forall a b. [a] -> [b] -> [(a, b)]
zip [Derivation f]
ps [Equation f]
eqs)))
where
eq :: Equation f
eq = forall f. Proof f -> Equation f
equation (forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)
ps :: [Derivation f]
ps = forall f. Function f => Derivation f -> [Derivation f]
steps Derivation f
p
eqs :: [Equation f]
eqs = forall a b. (a -> b) -> [a] -> [b]
map (forall f. Proof f -> Equation f
equation forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. [a] -> a
head ([[(a, Equation (ConstantOf a))]]
cands forall a. [a] -> [a] -> [a]
++ [[(a, Equation (ConstantOf a))]
steps])
where
cands :: [[(a, Equation (ConstantOf a))]]
cands =
[ forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub ([(a, Equation (ConstantOf a))]
before forall a. [a] -> [a] -> [a]
++ [(a, Equation (ConstantOf a))]
after)
| ([(a, Equation (ConstantOf a))]
before, [(a, Equation (ConstantOf a))]
mid1) <- forall a. [a] -> [([a], [a])]
splits [(a, Equation (ConstantOf a))]
steps,
(mid :: [(a, Equation (ConstantOf a))]
mid@((a, Equation (ConstantOf a))
_:[(a, Equation (ConstantOf a))]
_), [(a, Equation (ConstantOf a))]
after) <- forall a. [a] -> [a]
reverse (forall a. [a] -> [([a], [a])]
splits [(a, Equation (ConstantOf a))]
mid1),
let Term (ConstantOf a)
t :=: Term (ConstantOf a)
_ = forall a b. (a, b) -> b
snd (forall a. [a] -> a
head [(a, Equation (ConstantOf a))]
mid)
Term (ConstantOf a)
_ :=: Term (ConstantOf a)
u = forall a b. (a, b) -> b
snd (forall a. [a] -> a
last [(a, Equation (ConstantOf a))]
mid),
Subst (ConstantOf a)
sub <- forall a. Maybe a -> [a]
maybeToList (forall f. Term f -> Term f -> Maybe (Subst f)
unify Term (ConstantOf a)
t Term (ConstantOf a)
u),
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub Equation (ConstantOf a)
eq forall a. Eq a => a -> a -> Bool
== Equation (ConstantOf a)
eq ] forall a. [a] -> [a] -> [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))]
_)) <- forall a. [a] -> [([a], [a])]
splits [(a, Equation (ConstantOf a))]
steps,
let Term (ConstantOf a)
t :=: Term (ConstantOf a)
_ = forall a b. (a, b) -> b
snd (forall a. [a] -> a
head [(a, Equation (ConstantOf a))]
after)
Term (ConstantOf a)
_ :=: Term (ConstantOf a)
u = forall a b. (a, b) -> b
snd (forall a. [a] -> a
last [(a, Equation (ConstantOf a))]
after),
Subst (ConstantOf a)
sub <- forall a. Maybe a -> [a]
maybeToList (forall f. Term f -> Term f -> Maybe (Subst f)
match Term (ConstantOf a)
t Term (ConstantOf a)
u),
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub (forall f. Equation f -> Term f
eqn_lhs Equation (ConstantOf a)
eq) forall a. Eq a => a -> a -> Bool
== forall f. Equation f -> Term f
eqn_lhs Equation (ConstantOf a)
eq ] forall a. [a] -> [a] -> [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) <- forall a. [a] -> [a]
reverse (forall a. [a] -> [([a], [a])]
splits [(a, Equation (ConstantOf a))]
steps),
let Term (ConstantOf a)
t :=: Term (ConstantOf a)
_ = forall a b. (a, b) -> b
snd (forall a. [a] -> a
head [(a, Equation (ConstantOf a))]
before)
Term (ConstantOf a)
_ :=: Term (ConstantOf a)
u = forall a b. (a, b) -> b
snd (forall a. [a] -> a
last [(a, Equation (ConstantOf a))]
before),
Subst (ConstantOf a)
sub <- forall a. Maybe a -> [a]
maybeToList (forall f. Term f -> Term f -> Maybe (Subst f)
match Term (ConstantOf a)
u Term (ConstantOf a)
t),
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub (forall f. Equation f -> Term f
eqn_rhs Equation (ConstantOf a)
eq) forall a. Eq a => a -> a -> Bool
== forall f. Equation f -> Term f
eqn_rhs Equation (ConstantOf a)
eq ]
generaliseProof :: Function f => [Derivation f] -> [Derivation f]
generaliseProof :: forall f. Function f => [Derivation f] -> [Derivation f]
generaliseProof =
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 (forall a b. a -> b -> a
const forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
Proof f -> Derivation f
generaliseLemma) (forall a b. a -> b -> a
const forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
Derivation f -> Derivation f
generaliseGoal)
where
generaliseLemma :: Proof f -> Derivation f
generaliseLemma Proof f
p = forall f. Proof f -> Subst f -> Derivation f
lemma (forall f. Function f => Derivation f -> Proof f
certify Derivation f
q) Subst f
sub
where
(Derivation f
q, Subst f
sub) = forall {f}.
(Ordered 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 = 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) = forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
Proof f -> (Derivation f, Subst f)
generalise (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 = forall f. Proof f -> Equation f
equation Proof f
p
n :: Int
n = forall a. Symbolic a => a -> Int
freshVar Equation f
eq
qs :: [Derivation f]
qs = forall s a. State s a -> s -> a
evalState (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {m :: * -> *} {f}.
Monad m =>
Derivation f -> StateT Int m (Derivation f)
generaliseStep (forall f. Function f => Derivation f -> [Derivation f]
steps (forall f. Proof f -> Derivation f
derivation Proof f
p))) Int
n
Just Subst f
sub1 = forall f. [(Term f, Term f)] -> Maybe (Subst f)
unifyMany (forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
[Derivation f] -> [(Term f, Term f)]
stepsConstraints [Derivation f]
qs)
q :: Derivation f
q = forall a. Symbolic a => a -> a
canonicalise (forall f. Equation f -> [Derivation f] -> Derivation f
fromSteps Equation f
eq (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 = forall f. Equation f -> Equation f -> Maybe (Subst f)
matchEquation (forall f. Proof f -> Equation f
equation (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
_) =
forall {m :: * -> *} {f} {b}.
Monad m =>
[Var] -> (Subst f -> b) -> StateT Int m b
freshen (forall a. Symbolic a => a -> [Var]
vars (forall f. Axiom f -> Equation f
axiom_eqn Axiom f
axiom)) (forall f. Axiom f -> Subst f -> Derivation f
UseAxiom Axiom f
axiom)
generaliseStep (UseLemma Proof f
lemma Subst f
_) =
forall {m :: * -> *} {f} {b}.
Monad m =>
[Var] -> (Subst f -> b) -> StateT Int m b
freshen (forall a. Symbolic a => a -> [Var]
vars (forall f. Proof f -> Equation f
equation Proof f
lemma)) (forall f. Proof f -> Subst f -> Derivation f
UseLemma Proof f
lemma)
generaliseStep (Refl Term f
_) = do
Int
n <- forall (m :: * -> *) s. Monad m => StateT s m s
get
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int
nforall a. Num a => a -> a -> a
+Int
1)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall f. Term f -> Derivation f
Refl (forall a. Build a => a -> Term (BuildFun a)
build (forall f. Var -> Builder f
var (Int -> Var
V Int
n))))
generaliseStep (Symm Derivation f
p) =
forall f. Derivation f -> Derivation f
Symm 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) =
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 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) =
forall f. Fun f -> [Derivation f] -> Derivation f
Cong Fun f
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall (m :: * -> *) s. Monad m => StateT s m s
get
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int
n forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs)
let Just Subst f
sub = forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst [(Var
x, forall a. Build a => a -> Term (BuildFun a)
build (forall f. Var -> Builder f
var (Int -> Var
V Int
i))) | (Var
x, Int
i) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Ord a => [a] -> [a]
usort [Var]
xs) [Int
n..]]
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 = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {f} {f}. Equation f -> Equation f -> (Term f, Term f)
combine [Equation f]
eqs (forall a. [a] -> [a]
tail [Equation f]
eqs)
where
eqs :: [Equation f]
eqs = forall a b. (a -> b) -> [a] -> [b]
map (forall f. Proof f -> Equation f
equation forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall f. Function f => [Derivation f] -> [Derivation f]
canonicaliseLemmas =
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 (forall a b. a -> b -> a
const forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
Proof f -> Derivation f
canonicaliseLemma) (forall a b. a -> b -> a
const forall a. Symbolic a => a -> a
canonicalise)
where
canonicaliseLemma :: Proof f -> Derivation f
canonicaliseLemma Proof f
p
| Term f
u forall f. Ordered f => Term f -> Term f -> Bool
`lessEqSkolem` Term f
t = Derivation f -> Derivation f
canon (forall f. Proof f -> Derivation f
derivation Proof f
p)
| Bool
otherwise = forall f. Derivation f -> Derivation f
symm (Derivation f -> Derivation f
canon (forall f. Derivation f -> Derivation f
symm (forall f. Proof f -> Derivation f
derivation Proof f
p)))
where
Term f
t :=: Term f
u = forall f. Proof f -> Equation f
equation Proof f
p
symbolic :: Proof f -> (Equation f, Derivation f)
symbolic Proof f
p = (forall f. Proof f -> Equation f
equation Proof f
p, forall f. Proof f -> Derivation f
derivation Proof f
p)
before :: (Equation f, Derivation f)
before = forall {f}. Proof f -> (Equation f, Derivation f)
symbolic Proof f
p
after :: (Equation f, Derivation f)
after = forall a. Symbolic a => a -> a
canonicalise (forall {f}. Proof f -> (Equation f, Derivation f)
symbolic Proof f
p)
Just Subst f
sub1 = forall f. [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyList (forall a. Symbolic a => a -> [TermListOf a]
terms (Equation f, Derivation f)
before) (forall a. Symbolic a => a -> [TermListOf a]
terms (Equation f, Derivation f)
after)
Just Subst f
sub2 = forall f. [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyList (forall a. Symbolic a => a -> [TermListOf a]
terms (Equation f, Derivation f)
after) (forall a. Symbolic a => a -> [TermListOf a]
terms (Equation f, Derivation f)
before)
canon :: Derivation f -> Derivation f
canon Derivation f
p = forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub2 (forall f. Function f => Proof f -> Derivation f
simpleLemma (forall f. Function f => Derivation f -> Proof f
certify (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 :: forall f. Function f => Equation f -> Bool
invisible (Term f
t :=: Term f
u) = forall a. Show a => a -> String
show (forall a. Pretty a => a -> Doc
pPrint Term f
t) forall a. Eq a => a -> a -> Bool
== forall a. Show a => a -> String
show (forall a. Pretty a => a -> Doc
pPrint Term f
u)
pPrintLemma :: Function f => Config f -> (Axiom f -> String) -> (Proof f -> String) -> Proof f -> Doc
pPrintLemma :: forall f.
Function f =>
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
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Derivation f]
qs = String -> Doc
text String
"Reflexivity."
| forall f. Proof f -> Equation f
equation (forall f. Function f => Derivation f -> Proof f
certify (forall f. Equation f -> [Derivation f] -> Derivation f
fromSteps (forall f. Proof f -> Equation f
equation Proof f
p) [Derivation f]
qs)) forall a. Eq a => a -> a -> Bool
== forall f. Proof f -> Equation f
equation Proof f
p =
[Doc] -> Doc
vcat (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Int] -> Derivation f -> Doc
pp [[Int]]
hl [Derivation f]
qs) Doc -> Doc -> Doc
$$ forall a. Pretty a => a -> Doc
ppTerm (forall f. Equation f -> Term f
eqn_rhs (forall f. Proof f -> Equation f
equation Proof f
p))
| Bool
otherwise = forall a. HasCallStack => String -> a
error String
"lemma changed by pretty-printing!"
where
qs :: [Derivation f]
qs = forall f. Function f => Derivation f -> [Derivation f]
steps (forall f. Proof f -> Derivation f
derivation Proof f
p)
hl :: [[Int]]
hl = forall a b. (a -> b) -> [a] -> [b]
map forall {a} {f}. (Num a, Enum a) => Derivation f -> [a]
highlightStep [Derivation f]
qs
pp :: [Int] -> Derivation f -> Doc
pp [Int]
_ Derivation f
p | forall f. Function f => Equation f -> Bool
invisible (forall f. Proof f -> Equation f
equation (forall f. Function f => Derivation f -> Proof f
certify Derivation f
p)) = Doc
pPrintEmpty
pp [Int]
h Derivation f
p =
forall a. Pretty a => a -> Doc
ppTerm (forall f. [String] -> Maybe [Int] -> Term f -> HighlightedTerm f
HighlightedTerm [String
green | Bool
cfg_use_colour] (forall a. a -> Maybe a
Just [Int]
h) (forall f. Equation f -> Term f
eqn_lhs (forall f. Proof f -> Equation f
equation (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
iforall a. a -> [a] -> [a]
:Derivation f -> [a]
highlightStep Derivation f
p
where
[(a
i, Derivation f
p)] = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {f}. Derivation f -> Bool
isRefl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (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
<#> 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] = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall f. Subst f -> [(Var, Term f)]
substToList Subst f
sub)) =
String -> Doc
text String
" with " Doc -> Doc -> 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
pPrintSubst :: Function f => Subst f -> Doc
pPrintSubst :: forall f. Function f => Subst f -> Doc
pPrintSubst Subst f
sub =
[Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma
[ forall a. Pretty a => a -> Doc
pPrint Var
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"->" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint Term f
t
| (Var
x, Term f
t) <- forall f. Subst f -> [(Var, Term f)]
substToList Subst f
sub ])
pPrintPresentation :: forall f. Function f => Config f -> Presentation f -> Doc
pPrintPresentation :: forall f. Function f => Config f -> Presentation f -> Doc
pPrintPresentation Config f
config (Presentation [Axiom f]
axioms [Proof f]
lemmas [ProvedGoal f]
goals) =
[Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
intersperse (String -> Doc
text String
"") forall a b. (a -> b) -> a -> b
$
[Doc] -> Doc
vcat [ forall f.
Function f =>
String -> String -> Maybe String -> Equation f -> Doc
describeEquation String
"Axiom" (Axiom f -> String
axiomNum Axiom f
axiom) (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 (forall f. Function f => Equation f -> Bool
invisible Equation f
eqn) ]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) forall a. Maybe a
Nothing (forall f. Proof f -> Equation f
equation Proof f
p) forall f. Subst f
emptySubst Proof f
p
| Proof f
p <- [Proof f]
lemmas,
Bool -> Bool
not (forall f. Function f => Equation f -> Bool
invisible (forall f. Proof f -> Equation f
equation Proof f
p)) ] forall a. [a] -> [a] -> [a]
++
[ String
-> String
-> Maybe String
-> Equation f
-> Subst f
-> Proof f
-> Doc
pp String
"Goal" (forall a. Show a => a -> String
show Integer
num) (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
..}) <- 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 =
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
$$
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 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Axiom f]
axioms [Integer
1..])
lemmaNums :: Map (Proof f) Int
lemmaNums = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Proof f]
lemmas [forall (t :: * -> *) a. Foldable t => t a -> Int
length [Axiom f]
axiomsforall a. Num a => a -> a -> a
+Int
1..])
axiomNum :: Axiom f -> String
axiomNum Axiom f
x = forall a. Show a => a -> String
show (forall a. HasCallStack => Maybe a -> a
fromJust (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 = forall a. Show a => a -> String
show (forall a. HasCallStack => Maybe a -> a
fromJust (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 forall a. Eq a => a -> a -> Bool
== 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 forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
[ forall a. Pretty a => a -> Doc
pPrint Var
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint Term f
t
| (Var
x, Term f
t) <- forall f. Subst f -> [(Var, Term f)]
substToList Subst f
sub ],
if forall f. Minimal f => Fun f
minimal forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a. Symbolic a => a -> [FunOf a]
funs Subst f
sub then
String -> Doc
text String
"where" Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (forall a. Pretty a => a -> Doc
pPrint (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
| forall f. Config f -> Axiom f -> Bool
cfg_show_uses_of_axioms Config f
config Axiom f
axiom Bool -> Bool -> Bool
&& Bool -> Bool
not (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
[ forall a. Pretty a => a -> Doc
pPrint Int
i Doc -> Doc -> Doc
<#> String -> Doc
text String
"." Doc -> Doc -> Doc
<+> forall f. Function f => Subst f -> Doc
pPrintSubst Subst f
sub
| (Int
i, Subst f
sub) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1 :: Int ..] [Subst f]
uses ])
| Bool
otherwise = Doc
pPrintEmpty
where
uses :: [Subst f]
uses = 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 = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. Set a
Set.empty Axiom f
axiom Map (Axiom f) (Set (Subst f))
usesMap
usesMap :: Map (Axiom f) (Set (Subst f))
usesMap =
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Ord a => Set a -> Set a -> Set a
Set.union
[ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (forall a. Ord a => a -> Set a -> Set a
Set.delete forall f. Subst f
emptySubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall a f. (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
ground)
(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 = forall f. Proof f -> Derivation f
derivation (forall f. ProvedGoal f -> Proof f
pg_proof ProvedGoal f
goal) ]
describeEquation ::
Function f =>
String -> String -> Maybe String -> Equation f -> Doc
describeEquation :: forall f.
Function f =>
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
" (" forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
")")) Doc -> Doc -> Doc
<#>
String -> Doc
text String
":" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint Equation f
eqn Doc -> Doc -> Doc
<#> String -> Doc
text String
"."
decodeEquality :: Function f => Term f -> Maybe (Equation f)
decodeEquality :: forall f. Function f => Term f -> Maybe (Equation f)
decodeEquality (App Fun f
equals (Cons Term f
t (Cons Term f
u TermList f
Empty)))
| forall f. EqualsBonus f => f -> Bool
isEquals Fun f
equals = forall a. a -> Maybe a
Just (Term f
t forall f. Term f -> Term f -> Equation f
:=: Term f
u)
decodeEquality Term f
_ = forall a. Maybe a
Nothing
decodeGoal :: Function f => ProvedGoal f -> ProvedGoal f
decodeGoal :: forall f. Function f => ProvedGoal f -> ProvedGoal f
decodeGoal ProvedGoal f
pg =
case 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) ->
forall f. Function f => ProvedGoal f -> ProvedGoal f
checkProvedGoal forall a b. (a -> b) -> a -> b
$
ProvedGoal f
pg {
pg_name :: String
pg_name = String
name,
pg_proof :: Proof f
pg_proof = 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 :: forall f.
Function f =>
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
..}
| Term f -> Bool
isFalseTerm Term f
u = [Derivation f] -> Maybe (String, Subst f, Equation f, Derivation f)
extract (forall f. Function f => Derivation f -> [Derivation f]
steps Derivation f
deriv)
| Term f -> Bool
isFalseTerm Term f
t = [Derivation f] -> Maybe (String, Subst f, Equation f, Derivation f)
extract (forall f. Function f => Derivation f -> [Derivation f]
steps (forall f. Derivation f -> Derivation f
symm Derivation f
deriv))
| Bool
otherwise = forall a. Maybe a
Nothing
where
isFalseTerm, isTrueTerm :: Term f -> Bool
isFalseTerm :: Term f -> Bool
isFalseTerm (App Fun f
false TermList f
_) = 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
_) = forall f. EqualsBonus f => f -> Bool
isTrue Fun f
true
isTrueTerm Term f
_ = Bool
False
Term f
t :=: Term f
u = forall f. Proof f -> Equation f
equation Proof f
pg_proof
deriv :: Derivation f
deriv = forall f. Proof f -> Derivation f
derivation Proof f
pg_proof
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
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term f -> Bool
isTrueTerm (forall f. Equation f -> Term f
eqn_rhs Equation f
axiom_eqn))
(Term f
t :=: Term f
u) <- forall f. Function f => Term f -> Maybe (Equation f)
decodeEquality (forall f. Equation f -> Term f
eqn_lhs Equation f
axiom_eqn)
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term f
t forall a. Eq a => a -> a -> Bool
== Term f
u)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
t)
decodeReflexivity Derivation f
_ = forall a. Maybe a
Nothing
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
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term f -> Bool
isFalseTerm (forall f. Equation f -> Term f
eqn_rhs Equation f
axiom_eqn))
Equation f
eqn <- forall f. Function f => Term f -> Maybe (Equation f)
decodeEquality (forall f. Equation f -> Term f
eqn_lhs Equation f
axiom_eqn)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
axiom_name, Equation f
eqn, Subst f
sub)
decodeConjecture Derivation 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
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 (forall f. Term f -> Derivation f
Refl Term f
t) (forall f. Term f -> Derivation f
Refl Term f
t) [Derivation f]
ps
extract [] = 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 (forall f. Term f -> Derivation f
Refl Term f
t) (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 =
forall (m :: * -> *) a. Monad m => a -> m a
return (String
name, Subst f
sub, Equation f
eqn, forall f. Derivation f -> Derivation f
symm Derivation f
p1 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, 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 forall f. Derivation f -> Derivation f -> Derivation f
`trans` Derivation f
p1') (Derivation f
p2 forall f. Derivation f -> Derivation f -> Derivation f
`trans` Derivation f
p2') [Derivation f]
ps
cont Derivation f
_ Derivation f
_ [Derivation f]
_ = forall a. Maybe a
Nothing