-- A pruner that uses twee. Does not respect types.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-}
module QuickSpec.Internal.Pruning.UntypedTwee where

import QuickSpec.Internal.Testing
import QuickSpec.Internal.Pruning
import QuickSpec.Internal.Prop
import QuickSpec.Internal.Term
import QuickSpec.Internal.Type
import Data.Lens.Light
import qualified Twee
import qualified Twee.Equation as Twee
import qualified Twee.KBO as KBO
import qualified Twee.Base as Twee
import Twee hiding (Config(..))
import Twee.Rule hiding (normalForms)
import Twee.Proof hiding (Config, defaultConfig)
import Twee.Base(Ordered(..), Labelled)
import Control.Monad.Trans.Reader
import Control.Monad.Trans.State.Strict hiding (State)
import Control.Monad.Trans.Class
import Control.Monad.IO.Class
import QuickSpec.Internal.Terminal
import qualified Data.Set as Set
import Data.Set(Set)
import qualified Data.Map.Strict as Map
import qualified Data.IntMap as IntMap
import Control.Monad

data Config =
  Config {
    Config -> Int
cfg_max_term_size :: Int,
    Config -> Int
cfg_max_cp_depth :: Int }

lens_max_term_size :: Lens Config Int
lens_max_term_size = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Int
cfg_max_term_size (\Int
x Config
y -> Config
y { cfg_max_term_size :: Int
cfg_max_term_size = Int
x })
lens_max_cp_depth :: Lens Config Int
lens_max_cp_depth = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Int
cfg_max_cp_depth (\Int
x Config
y -> Config
y { cfg_max_cp_depth :: Int
cfg_max_cp_depth = Int
x })

data Extended fun = Minimal | Skolem Twee.Var | Function fun
  deriving (Extended fun -> Extended fun -> Bool
forall fun. Eq fun => Extended fun -> Extended fun -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Extended fun -> Extended fun -> Bool
$c/= :: forall fun. Eq fun => Extended fun -> Extended fun -> Bool
== :: Extended fun -> Extended fun -> Bool
$c== :: forall fun. Eq fun => Extended fun -> Extended fun -> Bool
Eq, Extended fun -> Extended fun -> Bool
Extended fun -> Extended fun -> Ordering
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 {fun}. Ord fun => Eq (Extended fun)
forall fun. Ord fun => Extended fun -> Extended fun -> Bool
forall fun. Ord fun => Extended fun -> Extended fun -> Ordering
forall fun. Ord fun => Extended fun -> Extended fun -> Extended fun
min :: Extended fun -> Extended fun -> Extended fun
$cmin :: forall fun. Ord fun => Extended fun -> Extended fun -> Extended fun
max :: Extended fun -> Extended fun -> Extended fun
$cmax :: forall fun. Ord fun => Extended fun -> Extended fun -> Extended fun
>= :: Extended fun -> Extended fun -> Bool
$c>= :: forall fun. Ord fun => Extended fun -> Extended fun -> Bool
> :: Extended fun -> Extended fun -> Bool
$c> :: forall fun. Ord fun => Extended fun -> Extended fun -> Bool
<= :: Extended fun -> Extended fun -> Bool
$c<= :: forall fun. Ord fun => Extended fun -> Extended fun -> Bool
< :: Extended fun -> Extended fun -> Bool
$c< :: forall fun. Ord fun => Extended fun -> Extended fun -> Bool
compare :: Extended fun -> Extended fun -> Ordering
$ccompare :: forall fun. Ord fun => Extended fun -> Extended fun -> Ordering
Ord, Typeable)

instance (Ord fun, Typeable fun) => Labelled (Extended fun)

instance Sized fun => Sized (Extended fun) where
  size :: Extended fun -> Int
size (Function fun
f) = forall a. Sized a => a -> Int
size fun
f
  size Extended fun
_ = Int
1

instance KBO.Sized (Extended fun) where
  size :: Extended fun -> Integer
size Extended fun
_ = Integer
1

instance Arity fun => Arity (Extended fun) where
  arity :: Extended fun -> Int
arity (Function fun
f) = forall f. Arity f => f -> Int
arity fun
f
  arity (Skolem Var
_) = Int
0
  arity Extended fun
Minimal = Int
0

instance (Ord fun, Typeable fun) => Twee.Minimal (Extended fun) where
  minimal :: Fun (Extended fun)
minimal = forall f. Labelled f => f -> Fun f
Twee.fun forall fun. Extended fun
Minimal

instance EqualsBonus (Extended fun)

instance (Ord fun, Typeable fun, Pretty fun) => Pretty (Extended fun) where
  pPrintPrec :: PrettyLevel -> Rational -> Extended fun -> Doc
pPrintPrec PrettyLevel
l Rational
p (Function fun
f) = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
p fun
f
  pPrintPrec PrettyLevel
_ Rational
_ Extended fun
Minimal = String -> Doc
text String
"?"
  pPrintPrec PrettyLevel
_ Rational
_ (Skolem (Twee.V Int
x)) = String -> Doc
text (String
"sk" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
x)

instance (Ord fun, Typeable fun, PrettyTerm fun) => PrettyTerm (Extended fun) where
  termStyle :: Extended fun -> TermStyle
termStyle (Function fun
f) = forall f. PrettyTerm f => f -> TermStyle
termStyle fun
f
  termStyle Extended fun
_ = TermStyle
curried

instance (Sized fun, Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where
  lessEq :: Term (Extended fun) -> Term (Extended fun) -> Bool
lessEq = forall f.
(Function f, Sized f, Weighted f) =>
Term f -> Term f -> Bool
KBO.lessEq
  lessIn :: Model (Extended fun)
-> Term (Extended fun) -> Term (Extended fun) -> Maybe Strictness
lessIn = forall f.
(Function f, Sized f, Weighted f) =>
Model f -> Term f -> Term f -> Maybe Strictness
KBO.lessIn
  lessEqSkolem :: Term (Extended fun) -> Term (Extended fun) -> Bool
lessEqSkolem = forall f.
(Function f, Sized f, Weighted f) =>
Term f -> Term f -> Bool
KBO.lessEqSkolem

newtype Pruner fun m a =
  Pruner (ReaderT (Twee.Config (Extended fun)) (StateT (State (Extended fun)) m) a)
  deriving (forall a b. a -> Pruner fun m b -> Pruner fun m a
forall a b. (a -> b) -> Pruner fun m a -> Pruner fun m b
forall fun (m :: * -> *) a b.
Functor m =>
a -> Pruner fun m b -> Pruner fun m a
forall fun (m :: * -> *) a b.
Functor m =>
(a -> b) -> Pruner fun m a -> Pruner fun m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Pruner fun m b -> Pruner fun m a
$c<$ :: forall fun (m :: * -> *) a b.
Functor m =>
a -> Pruner fun m b -> Pruner fun m a
fmap :: forall a b. (a -> b) -> Pruner fun m a -> Pruner fun m b
$cfmap :: forall fun (m :: * -> *) a b.
Functor m =>
(a -> b) -> Pruner fun m a -> Pruner fun m b
Functor, forall a. a -> Pruner fun m a
forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m a
forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall a b.
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
forall a b c.
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
forall {fun} {m :: * -> *}. Monad m => Functor (Pruner fun m)
forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m a
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
forall fun (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m a
$c<* :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m a
*> :: forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
$c*> :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
liftA2 :: forall a b c.
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
$cliftA2 :: forall fun (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
<*> :: forall a b.
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
$c<*> :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
pure :: forall a. a -> Pruner fun m a
$cpure :: forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
Applicative, forall a. a -> Pruner fun m a
forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall a b.
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
forall fun (m :: * -> *). Monad m => Applicative (Pruner fun m)
forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> Pruner fun m a
$creturn :: forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
>> :: forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
$c>> :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
>>= :: forall a b.
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
$c>>= :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
Monad, forall a. IO a -> Pruner fun m a
forall {fun} {m :: * -> *}. MonadIO m => Monad (Pruner fun m)
forall fun (m :: * -> *) a. MonadIO m => IO a -> Pruner fun m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> Pruner fun m a
$cliftIO :: forall fun (m :: * -> *) a. MonadIO m => IO a -> Pruner fun m a
MonadIO, MonadTester testcase term, String -> Pruner fun m ()
forall {fun} {m :: * -> *}. MonadTerminal m => Monad (Pruner fun m)
forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
forall (m :: * -> *).
Monad m
-> (String -> m ())
-> (String -> m ())
-> (String -> m ())
-> MonadTerminal m
putTemp :: String -> Pruner fun m ()
$cputTemp :: forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
putLine :: String -> Pruner fun m ()
$cputLine :: forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
putText :: String -> Pruner fun m ()
$cputText :: forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
MonadTerminal)

instance MonadTrans (Pruner fun) where
  lift :: forall (m :: * -> *) a. Monad m => m a -> Pruner fun m a
lift = forall fun (m :: * -> *) a.
ReaderT (Config (Extended fun)) (StateT (State (Extended fun)) m) a
-> Pruner fun m a
Pruner forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

run :: (Typeable fun, Ord fun, Sized fun, Monad m) => Config -> Pruner fun m a -> m a
run :: forall fun (m :: * -> *) a.
(Typeable fun, Ord fun, Sized fun, Monad m) =>
Config -> Pruner fun m a -> m a
run Config{Int
cfg_max_cp_depth :: Int
cfg_max_term_size :: Int
cfg_max_cp_depth :: Config -> Int
cfg_max_term_size :: Config -> Int
..} (Pruner ReaderT (Config (Extended fun)) (StateT (State (Extended fun)) m) a
x) =
  forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT (Config (Extended fun)) (StateT (State (Extended fun)) m) a
x Config (Extended fun)
config) (forall f. Config f -> State f
initialState Config (Extended fun)
config)
  where
    config :: Config (Extended fun)
config =
      forall f. Config f
defaultConfig {
        cfg_accept_term :: Maybe (Term (Extended fun) -> Bool)
Twee.cfg_accept_term = forall a. a -> Maybe a
Just (\Term (Extended fun)
t -> forall a. Sized a => a -> Int
size Term (Extended fun)
t forall a. Ord a => a -> a -> Bool
<= Int
cfg_max_term_size),
        cfg_max_cp_depth :: Int
Twee.cfg_max_cp_depth = Int
cfg_max_cp_depth }

instance (Labelled fun, Sized fun) => Sized (Twee.Term fun) where
  size :: Term fun -> Int
size (Twee.Var Var
_) = Int
1
  size (Twee.App Fun fun
f TermList fun
ts) =
    forall a. Sized a => a -> Int
size (forall f. Labelled f => Fun f -> f
Twee.fun_value Fun fun
f) forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b. (a -> b) -> [a] -> [b]
map forall a. Sized a => a -> Int
size (forall f. TermList f -> [Term f]
Twee.unpack TermList fun
ts))

instance KBO.Weighted (Extended fun) where
  argWeight :: Extended fun -> Integer
argWeight Extended fun
_ = Integer
1

type Norm fun = Twee.Term (Extended fun)

instance (Ord fun, Typed fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun, Monad m) =>
  MonadPruner (Term fun) (Norm fun) (Pruner fun m) where
  normaliser :: Pruner fun m (Term fun -> Norm fun)
normaliser = forall fun (m :: * -> *) a.
ReaderT (Config (Extended fun)) (StateT (State (Extended fun)) m) a
-> Pruner fun m a
Pruner forall a b. (a -> b) -> a -> b
$ do
    State (Extended fun)
state <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *) s. Monad m => StateT s m s
get
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \Term fun
t ->
      let u :: Norm fun
u = forall fun.
(Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun,
 Sized fun) =>
State (Extended fun) -> Term fun -> Norm fun
normaliseTwee State (Extended fun)
state Term fun
t in
      Norm fun
u
      -- traceShow (text "normalise:" <+> pPrint t <+> text "->" <+> pPrint u) u

  add :: Prop (Term fun) -> Pruner fun m Bool
add ([] :=>: Term fun
t :=: Term fun
u) = forall fun (m :: * -> *) a.
ReaderT (Config (Extended fun)) (StateT (State (Extended fun)) m) a
-> Pruner fun m a
Pruner forall a b. (a -> b) -> a -> b
$ do
    State (Extended fun)
state <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *) s. Monad m => StateT s m s
get
    Config (Extended fun)
config <- forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
    let (Term fun
t' :=: Term fun
u') = forall fun a. Symbolic fun a => a -> a
canonicalise (Term fun
t forall a. a -> a -> Equation a
:=: Term fun
u)
    if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (forall fun.
(Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun,
 Sized fun) =>
State (Extended fun) -> Term fun -> Set (Norm fun)
normalFormsTwee State (Extended fun)
state Term fun
t') (forall fun.
(Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun,
 Sized fun) =>
State (Extended fun) -> Term fun -> Set (Norm fun)
normalFormsTwee State (Extended fun)
state Term fun
u'))) then
      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    else do
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put forall a b. (a -> b) -> a -> b
$! forall fun.
(Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun,
 Sized fun) =>
Config (Extended fun)
-> Term fun
-> Term fun
-> State (Extended fun)
-> State (Extended fun)
addTwee Config (Extended fun)
config Term fun
t Term fun
u State (Extended fun)
state)
      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

  add Prop (Term fun)
_ =
    forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    --error "twee pruner doesn't support non-unit equalities"

  decodeNormalForm :: (Type -> Maybe (Term fun))
-> Norm fun -> Pruner fun m (Maybe (Term fun))
decodeNormalForm Type -> Maybe (Term fun)
hole Norm fun
t = forall (m :: * -> *) a. Monad m => a -> m a
return (Norm fun -> Type -> Maybe (Term fun)
decode Norm fun
t (forall a. HasCallStack => String -> a
error String
"ambiguously-typed term"))
    where
      decode :: Norm fun -> Type -> Maybe (Term fun)
decode (Twee.Var (Twee.V Int
n)) Type
ty =
        forall a. a -> Maybe a
Just (forall f. Var -> Term f
Var (Type -> Int -> Var
V Type
ty Int
n))
      decode (Twee.App (Twee.F Int
_ Extended fun
Minimal) TermList (Extended fun)
Twee.Empty) Type
ty =
        Type -> Maybe (Term fun)
hole Type
ty
      decode (Twee.App (Twee.F Int
_ (Skolem (Twee.V Int
n))) TermList (Extended fun)
Twee.Empty) Type
ty =
        forall a. a -> Maybe a
Just (forall f. Var -> Term f
Var (Type -> Int -> Var
V Type
ty Int
n))
      decode (Twee.App (Twee.F Int
_ (Function fun
f)) TermList (Extended fun)
ts) Type
_ =
        (forall f. f -> Term f
Fun fun
f forall {f}. Term f -> [Term f] -> Term f
:@:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Norm fun -> Type -> Maybe (Term fun)
decode (forall f. TermList f -> [Term f]
Twee.unpack TermList (Extended fun)
ts) [Type]
args
        where
          args :: [Type]
args = Type -> [Type]
typeArgs (forall a. Typed a => a -> Type
typ fun
f)
      decode Norm fun
_ Type
_ = forall a. HasCallStack => String -> a
error String
"ill-typed term"

  normTheorems :: Pruner fun m [Theorem (Norm fun)]
normTheorems = forall fun (m :: * -> *) a.
ReaderT (Config (Extended fun)) (StateT (State (Extended fun)) m) a
-> Pruner fun m a
Pruner forall a b. (a -> b) -> a -> b
$ do
    State (Extended fun)
state <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *) s. Monad m => StateT s m s
get
    let actives :: [Active (Extended fun)]
actives = forall a. IntMap a -> [a]
IntMap.elems (forall f. State f -> IntMap (Active f)
Twee.st_active_set State (Extended fun)
state)
    let
      toTheorem :: Active f -> Theorem (Term f)
toTheorem Active f
active =
        forall norm.
Prop norm -> [(Prop norm, [Prop norm])] -> Theorem norm
Theorem
          (forall {f}. Equation f -> Prop (Term f)
toProp (forall f. Proof f -> Equation f
equation Proof f
proof))
          (forall a b. (a -> b) -> [a] -> [b]
map forall {s}.
Substitution s =>
(Axiom (SubstFun s), Set s)
-> (Prop (Term (SubstFun s)), [Prop (Term (SubstFun s))])
toAxiom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
Map.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f.
Function f =>
Derivation f -> Map (Axiom f) (Set (Subst f))
groundAxiomsAndSubsts forall a b. (a -> b) -> a -> b
$ Derivation f
deriv)
        where
          proof :: Proof f
proof = forall f. Active f -> Proof f
Twee.active_proof Active f
active
          deriv :: Derivation f
deriv = forall f. Proof f -> Derivation f
derivation Proof f
proof
          toProp :: Equation f -> Prop (Term f)
toProp (Term f
t Twee.:=: Term f
u) = [] forall a. [Equation a] -> Equation a -> Prop a
:=>: Term f
t forall a. a -> a -> Equation a
:=: Term f
u
          toAxiom :: (Axiom (SubstFun s), Set s)
-> (Prop (Term (SubstFun s)), [Prop (Term (SubstFun s))])
toAxiom (Axiom (SubstFun s)
ax, Set s
subs) = (forall {f}. Equation f -> Prop (Term f)
toProp Equation (SubstFun s)
eqn, forall a b. (a -> b) -> [a] -> [b]
map forall {f}. Equation f -> Prop (Term f)
toProp [forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
Twee.subst s
sub Equation (SubstFun s)
eqn | s
sub <- forall a. Set a -> [a]
Set.toList Set s
subs])
            where
              eqn :: Equation (SubstFun s)
eqn = forall f. Axiom f -> Equation f
axiom_eqn Axiom (SubstFun s)
ax

    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
Active f -> Theorem (Term f)
toTheorem [Active (Extended fun)]
actives)

normaliseTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
  State (Extended fun) -> Term fun -> Norm fun
normaliseTwee :: forall fun.
(Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun,
 Sized fun) =>
State (Extended fun) -> Term fun -> Norm fun
normaliseTwee State (Extended fun)
state Term fun
t =
  forall f. Term f -> Reduction f -> Term f
result Term (Extended fun)
u (forall f. Function f => State f -> Term f -> Reduction f
normaliseTerm State (Extended fun)
state Term (Extended fun)
u)
  where
    u :: Term (Extended fun)
u = forall f. Function f => State f -> Term f -> Term f
simplifyTerm State (Extended fun)
state (forall f. (Ord f, Typeable f) => Term f -> Term (Extended f)
skolemise Term fun
t)

normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
  State (Extended fun) -> Term fun -> Set (Norm fun)
normalFormsTwee :: forall fun.
(Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun,
 Sized fun) =>
State (Extended fun) -> Term fun -> Set (Norm fun)
normalFormsTwee State (Extended fun)
state Term fun
t =
  forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey forall f. Term f -> Reduction f -> Term f
result (forall f.
Function f =>
State f -> Term f -> Map (Term f) (Reduction f)
normalForms State (Extended fun)
state (forall f. (Ord f, Typeable f) => Term f -> Term (Extended f)
skolemise Term fun
t))

addTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>
  Twee.Config (Extended fun) -> Term fun -> Term fun -> State (Extended fun) -> State (Extended fun)
addTwee :: forall fun.
(Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun,
 Sized fun) =>
Config (Extended fun)
-> Term fun
-> Term fun
-> State (Extended fun)
-> State (Extended fun)
addTwee Config (Extended fun)
config Term fun
t Term fun
u State (Extended fun)
state =
  forall f. Function f => Config f -> State f -> State f
interreduce Config (Extended fun)
config forall a b. (a -> b) -> a -> b
$
  forall f. Function f => Config f -> State f -> State f
completePure Config (Extended fun)
config forall a b. (a -> b) -> a -> b
$
    forall f. Function f => Config f -> State f -> Axiom f -> State f
addAxiom Config (Extended fun)
config State (Extended fun)
state Axiom (Extended fun)
axiom
  where
    axiom :: Axiom (Extended fun)
axiom = forall f. Int -> String -> Equation f -> Axiom f
Axiom Int
0 (forall a. Pretty a => a -> String
prettyShow (Term fun
t forall a. a -> a -> Equation a
:=: Term fun
u)) (forall f. (Ord f, Typeable f) => Term f -> Term (Extended f)
toTwee Term fun
t forall f. Term f -> Term f -> Equation f
Twee.:=: forall f. (Ord f, Typeable f) => Term f -> Term (Extended f)
toTwee Term fun
u)

toTwee :: (Ord f, Typeable f) =>
  Term f -> Twee.Term (Extended f)
toTwee :: forall f. (Ord f, Typeable f) => Term f -> Term (Extended f)
toTwee = forall a. Build a => a -> Term (BuildFun a)
Twee.build forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {fun}.
(Ord fun, Typeable fun) =>
Term fun -> Builder (Extended fun)
tt
  where
    tt :: Term fun -> Builder (Extended fun)
tt (Var (V Type
_ Int
x)) =
      forall f. Var -> Builder f
Twee.var (Int -> Var
Twee.V Int
x)
    tt (Fun fun
f :@: [Term fun]
ts) =
      forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
Twee.app (forall f. Labelled f => f -> Fun f
Twee.fun (forall fun. fun -> Extended fun
Function fun
f)) (forall a b. (a -> b) -> [a] -> [b]
map Term fun -> Builder (Extended fun)
tt [Term fun]
ts)
    tt Term fun
_ = forall a. HasCallStack => String -> a
error String
"partially applied term"

skolemise :: (Ord f, Typeable f) =>
  Term f -> Twee.Term (Extended f)
skolemise :: forall f. (Ord f, Typeable f) => Term f -> Term (Extended f)
skolemise = forall a. Build a => a -> Term (BuildFun a)
Twee.build forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {fun}.
(Ord fun, Typeable fun) =>
Term fun -> Builder (Extended fun)
sk
  where
    sk :: Term fun -> Builder (Extended fun)
sk (Var (V Type
_ Int
x)) =
      forall f. Fun f -> Builder f
Twee.con (forall f. Labelled f => f -> Fun f
Twee.fun (forall fun. Var -> Extended fun
Skolem (Int -> Var
Twee.V Int
x)))
    sk (Fun fun
f :@: [Term fun]
ts) =
      forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
Twee.app (forall f. Labelled f => f -> Fun f
Twee.fun (forall fun. fun -> Extended fun
Function fun
f)) (forall a b. (a -> b) -> [a] -> [b]
map Term fun -> Builder (Extended fun)
sk [Term fun]
ts)
    sk Term fun
_ = forall a. HasCallStack => String -> a
error String
"partially applied term"