{-# 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
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
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"