{-# LANGUAGE PatternSynonyms, ViewPatterns, TypeSynonymInstances, FlexibleInstances, TypeFamilies, ConstraintKinds, DeriveGeneric, DeriveAnyClass, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, TypeOperators, DeriveFunctor, FlexibleContexts, DeriveTraversable #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
module QuickSpec.Internal.Term(module QuickSpec.Internal.Term, module Twee.Base, module Twee.Pretty) where
import QuickSpec.Internal.Type
import QuickSpec.Internal.Utils
import Control.Monad
import GHC.Generics(Generic)
import Test.QuickCheck(CoArbitrary(..))
import Data.DList(DList)
import qualified Data.DList as DList
import Twee.Base(Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)
import Twee.Pretty
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import Data.List
import Data.Ord
import Data.Maybe
data Term f = Var {-# UNPACK #-} !Var | Fun !f | !(Term f) :$: !(Term f)
deriving (Term f -> Term f -> Bool
forall f. Eq f => Term f -> Term f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term f -> Term f -> Bool
$c/= :: forall f. Eq f => Term f -> Term f -> Bool
== :: Term f -> Term f -> Bool
$c== :: forall f. Eq f => Term f -> Term f -> Bool
Eq, Term f -> Term f -> Bool
Term f -> Term f -> 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 {f}. Ord f => Eq (Term f)
forall f. Ord f => Term f -> Term f -> Bool
forall f. Ord f => Term f -> Term f -> Ordering
forall f. Ord f => Term f -> Term f -> Term f
min :: Term f -> Term f -> Term f
$cmin :: forall f. Ord f => Term f -> Term f -> Term f
max :: Term f -> Term f -> Term f
$cmax :: forall f. Ord f => Term f -> Term f -> Term f
>= :: Term f -> Term f -> Bool
$c>= :: forall f. Ord f => Term f -> Term f -> Bool
> :: Term f -> Term f -> Bool
$c> :: forall f. Ord f => Term f -> Term f -> Bool
<= :: Term f -> Term f -> Bool
$c<= :: forall f. Ord f => Term f -> Term f -> Bool
< :: Term f -> Term f -> Bool
$c< :: forall f. Ord f => Term f -> Term f -> Bool
compare :: Term f -> Term f -> Ordering
$ccompare :: forall f. Ord f => Term f -> Term f -> Ordering
Ord, Int -> Term f -> ShowS
forall f. Show f => Int -> Term f -> ShowS
forall f. Show f => [Term f] -> ShowS
forall f. Show f => Term f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term f] -> ShowS
$cshowList :: forall f. Show f => [Term f] -> ShowS
show :: Term f -> String
$cshow :: forall f. Show f => Term f -> String
showsPrec :: Int -> Term f -> ShowS
$cshowsPrec :: forall f. Show f => Int -> Term f -> ShowS
Show, forall a b. a -> Term b -> Term a
forall a b. (a -> b) -> Term a -> Term 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 -> Term b -> Term a
$c<$ :: forall a b. a -> Term b -> Term a
fmap :: forall a b. (a -> b) -> Term a -> Term b
$cfmap :: forall a b. (a -> b) -> Term a -> Term b
Functor, forall a. Eq a => a -> Term a -> Bool
forall a. Num a => Term a -> a
forall a. Ord a => Term a -> a
forall m. Monoid m => Term m -> m
forall a. Term a -> Bool
forall a. Term a -> Int
forall a. Term a -> [a]
forall a. (a -> a -> a) -> Term a -> a
forall m a. Monoid m => (a -> m) -> Term a -> m
forall b a. (b -> a -> b) -> b -> Term a -> b
forall a b. (a -> b -> b) -> b -> Term a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Term a -> a
$cproduct :: forall a. Num a => Term a -> a
sum :: forall a. Num a => Term a -> a
$csum :: forall a. Num a => Term a -> a
minimum :: forall a. Ord a => Term a -> a
$cminimum :: forall a. Ord a => Term a -> a
maximum :: forall a. Ord a => Term a -> a
$cmaximum :: forall a. Ord a => Term a -> a
elem :: forall a. Eq a => a -> Term a -> Bool
$celem :: forall a. Eq a => a -> Term a -> Bool
length :: forall a. Term a -> Int
$clength :: forall a. Term a -> Int
null :: forall a. Term a -> Bool
$cnull :: forall a. Term a -> Bool
toList :: forall a. Term a -> [a]
$ctoList :: forall a. Term a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Term a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Term a -> a
foldr1 :: forall a. (a -> a -> a) -> Term a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Term a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Term a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Term a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Term a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Term a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Term a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Term a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Term a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Term a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Term a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Term a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Term a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Term a -> m
fold :: forall m. Monoid m => Term m -> m
$cfold :: forall m. Monoid m => Term m -> m
Foldable, Functor Term
Foldable Term
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Term (m a) -> m (Term a)
forall (f :: * -> *) a. Applicative f => Term (f a) -> f (Term a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Term a -> m (Term b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Term a -> f (Term b)
sequence :: forall (m :: * -> *) a. Monad m => Term (m a) -> m (Term a)
$csequence :: forall (m :: * -> *) a. Monad m => Term (m a) -> m (Term a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Term a -> m (Term b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Term a -> m (Term b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Term (f a) -> f (Term a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Term (f a) -> f (Term a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Term a -> f (Term b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Term a -> f (Term b)
Traversable)
data Var = V { Var -> Type
var_ty :: !Type, Var -> Int
var_id :: {-# UNPACK #-} !Int }
deriving (Var -> Var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
Ord, Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show, forall x. Rep Var x -> Var
forall x. Var -> Rep Var x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Var x -> Var
$cfrom :: forall x. Var -> Rep Var x
Generic)
instance CoArbitrary Var where
coarbitrary :: forall b. Var -> Gen b -> Gen b
coarbitrary = forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Int
var_id
instance Typed Var where
typ :: Var -> Type
typ Var
x = Var -> Type
var_ty Var
x
otherTypesDL :: Var -> DList Type
otherTypesDL Var
_ = forall (m :: * -> *) a. MonadPlus m => m a
mzero
typeSubst_ :: (Var -> Builder TyCon) -> Var -> Var
typeSubst_ Var -> Builder TyCon
sub (V Type
ty Int
x) = Type -> Int -> Var
V (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Type
ty) Int
x
match :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
match :: forall f. Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
match (Var Var
x) Term f
t = forall a. a -> Maybe a
Just (forall k a. k -> a -> Map k a
Map.singleton Var
x Term f
t)
match (Fun f
f) (Fun f
g)
| f
f forall a. Eq a => a -> a -> Bool
== f
g = forall a. a -> Maybe a
Just forall k a. Map k a
Map.empty
| Bool
otherwise = forall a. Maybe a
Nothing
match (Term f
f :$: Term f
x) (Term f
g :$: Term f
y) = do
Map Var (Term f)
m1 <- forall f. Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
match Term f
f Term f
g
Map Var (Term f)
m2 <- forall f. Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
match Term f
x Term f
y
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Term f
t forall a. Eq a => a -> a -> Bool
== Term f
u | (Term f
t, Term f
u) <- forall k a. Map k a -> [a]
Map.elems (forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith (,) Map Var (Term f)
m1 Map Var (Term f)
m2)])
forall (m :: * -> *) a. Monad m => a -> m a
return (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Var (Term f)
m1 Map Var (Term f)
m2)
unify :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
unify :: forall f. Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
unify Term f
t Term f
u = forall {f}.
Eq f =>
Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop forall k a. Map k a
Map.empty [(Term f
t, Term f
u)]
where
loop :: Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop Map Var (Term f)
sub [] = forall a. a -> Maybe a
Just Map Var (Term f)
sub
loop Map Var (Term f)
sub ((Fun f
f, Fun f
g):[(Term f, Term f)]
xs)
| f
f forall a. Eq a => a -> a -> Bool
== f
g = Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop Map Var (Term f)
sub [(Term f, Term f)]
xs
loop Map Var (Term f)
sub ((Term f
f :$: Term f
x, Term f
g :$: Term f
y):[(Term f, Term f)]
xs) =
Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop Map Var (Term f)
sub ((Term f
f, Term f
g)forall a. a -> [a] -> [a]
:(Term f
x, Term f
y)forall a. a -> [a] -> [a]
:[(Term f, Term f)]
xs)
loop Map Var (Term f)
sub ((Var Var
x, Term f
t):[(Term f, Term f)]
xs)
| Term f
t forall a. Eq a => a -> a -> Bool
== forall f. Var -> Term f
Var Var
x = Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop Map Var (Term f)
sub [(Term f, Term f)]
xs
| Var
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall f a. Symbolic f a => a -> [Var]
vars Term f
t = forall a. Maybe a
Nothing
| Bool
otherwise =
Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop
(forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
x Term f
t (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall {f}. Var -> Term f -> Term f -> Term f
replace Var
x Term f
t) Map Var (Term f)
sub))
[(forall {f}. Var -> Term f -> Term f -> Term f
replace Var
x Term f
t Term f
u, forall {f}. Var -> Term f -> Term f -> Term f
replace Var
x Term f
t Term f
v) | (Term f
u, Term f
v) <- [(Term f, Term f)]
xs]
loop Map Var (Term f)
sub ((Term f
t, Var Var
x):[(Term f, Term f)]
xs) = Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop Map Var (Term f)
sub ((forall f. Var -> Term f
Var Var
x, Term f
t)forall a. a -> [a] -> [a]
:[(Term f, Term f)]
xs)
replace :: Var -> Term f -> Term f -> Term f
replace Var
x Term f
t (Var Var
y) | Var
x forall a. Eq a => a -> a -> Bool
== Var
y = Term f
t
replace Var
_ Term f
_ Term f
t = Term f
t
class Symbolic f a | a -> f where
termsDL :: a -> DList (Term f)
subst :: (Var -> Term f) -> a -> a
instance Symbolic f (Term f) where
termsDL :: Term f -> DList (Term f)
termsDL = forall (m :: * -> *) a. Monad m => a -> m a
return
subst :: (Var -> Term f) -> Term f -> Term f
subst Var -> Term f
sub (Var Var
x) = Var -> Term f
sub Var
x
subst Var -> Term f
_ (Fun f
x) = forall f. f -> Term f
Fun f
x
subst Var -> Term f
sub (Term f
t :$: Term f
u) = forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst Var -> Term f
sub Term f
t forall f. Term f -> Term f -> Term f
:$: forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst Var -> Term f
sub Term f
u
instance Symbolic f a => Symbolic f [a] where
termsDL :: [a] -> DList (Term f)
termsDL = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall f a. Symbolic f a => a -> DList (Term f)
termsDL
subst :: (Var -> Term f) -> [a] -> [a]
subst Var -> Term f
sub = forall a b. (a -> b) -> [a] -> [b]
map (forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst Var -> Term f
sub)
class Sized a where
size :: a -> Int
instance Sized f => Sized (Term f) where
size :: Term f -> Int
size (Var Var
_) = Int
1
size (Fun f
f) = forall a. Sized a => a -> Int
size f
f
size (Term f
t :$: Term f
u) =
forall a. Sized a => a -> Int
size Term f
t forall a. Num a => a -> a -> a
+ forall a. Sized a => a -> Int
size Term f
u forall a. Num a => a -> a -> a
+
case Term f
t of
Var Var
_ -> Int
1
Term f
_ -> Int
0
instance Pretty Var where
pPrint :: Var -> Doc
pPrint Var
x = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"X" Doc -> Doc -> Doc
<#> forall a. Pretty a => a -> Doc
pPrint (Var -> Int
var_id Var
xforall a. Num a => a -> a -> a
+Int
1) Doc -> Doc -> Doc
<+> String -> Doc
text String
"::" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint (Var -> Type
var_ty Var
x)
instance PrettyTerm f => Pretty (Term f) where
pPrintPrec :: PrettyLevel -> Rational -> Term f -> Doc
pPrintPrec PrettyLevel
l Rational
p (Var Var
x :@: [Term f]
ts) =
TermStyle
-> forall a.
Pretty a =>
PrettyLevel -> Rational -> Doc -> [a] -> Doc
pPrintTerm TermStyle
curried PrettyLevel
l Rational
p (forall a. Pretty a => a -> Doc
pPrint Var
x) [Term f]
ts
pPrintPrec PrettyLevel
l Rational
p (Fun f
f :@: [Term f]
ts) =
TermStyle
-> forall a.
Pretty a =>
PrettyLevel -> Rational -> Doc -> [a] -> Doc
pPrintTerm (forall f. PrettyTerm f => f -> TermStyle
termStyle f
f) PrettyLevel
l Rational
p (forall a. Pretty a => a -> Doc
pPrint f
f) [Term f]
ts
terms :: Symbolic f a => a -> [Term f]
terms :: forall f a. Symbolic f a => a -> [Term f]
terms = forall a. DList a -> [a]
DList.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f a. Symbolic f a => a -> DList (Term f)
termsDL
funs :: Symbolic f a => a -> [f]
funs :: forall f a. Symbolic f a => a -> [f]
funs a
x = [ f
f | Term f
t <- forall f a. Symbolic f a => a -> [Term f]
terms a
x, Fun f
f <- forall f. Term f -> [Term f]
subterms Term f
t ]
vars :: Symbolic f a => a -> [Var]
vars :: forall f a. Symbolic f a => a -> [Var]
vars a
x = [ Var
v | Term f
t <- forall f a. Symbolic f a => a -> [Term f]
terms a
x, Var Var
v <- forall f. Term f -> [Term f]
subterms Term f
t ]
pattern f $b:@: :: forall {f}. Term f -> [Term f] -> Term f
$m:@: :: forall {r} {f}.
Term f -> (Term f -> [Term f] -> r) -> ((# #) -> r) -> r
:@: ts <- (getApp -> (f, ts)) where
Term f
f :@: [Term f]
ts = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall f. Term f -> Term f -> Term f
(:$:) Term f
f [Term f]
ts
getApp :: Term f -> (Term f, [Term f])
getApp :: forall f. Term f -> (Term f, [Term f])
getApp (Term f
t :$: Term f
u) = (Term f
f, [Term f]
ts forall a. [a] -> [a] -> [a]
++ [Term f
u])
where
(Term f
f, [Term f]
ts) = forall f. Term f -> (Term f, [Term f])
getApp Term f
t
getApp Term f
t = (Term f
t, [])
freeVar :: Symbolic f a => a -> Int
freeVar :: forall f a. Symbolic f a => a -> Int
freeVar a
x = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0forall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map (forall a. Enum a => a -> a
succ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Int
var_id) (forall f a. Symbolic f a => a -> [Var]
vars a
x))
occ :: (Eq f, Symbolic f a) => f -> a -> Int
occ :: forall f a. (Eq f, Symbolic f a) => f -> a -> Int
occ f
x a
t = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== f
x) (forall f a. Symbolic f a => a -> [f]
funs a
t))
occVar :: Symbolic f a => Var -> a -> Int
occVar :: forall f a. Symbolic f a => Var -> a -> Int
occVar Var
x a
t = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== Var
x) (forall f a. Symbolic f a => a -> [Var]
vars a
t))
mapVar :: (Var -> Var) -> Term f -> Term f
mapVar :: forall f. (Var -> Var) -> Term f -> Term f
mapVar Var -> Var
f (Var Var
x) = forall f. Var -> Term f
Var (Var -> Var
f Var
x)
mapVar Var -> Var
_ (Fun f
x) = forall f. f -> Term f
Fun f
x
mapVar Var -> Var
f (Term f
t :$: Term f
u) = forall f. (Var -> Var) -> Term f -> Term f
mapVar Var -> Var
f Term f
t forall f. Term f -> Term f -> Term f
:$: forall f. (Var -> Var) -> Term f -> Term f
mapVar Var -> Var
f Term f
u
mapFun :: (f -> g) -> Term f -> Term g
mapFun :: forall a b. (a -> b) -> Term a -> Term b
mapFun f -> g
_ (Var Var
x) = forall f. Var -> Term f
Var Var
x
mapFun f -> g
f (Fun f
x) = forall f. f -> Term f
Fun (f -> g
f f
x)
mapFun f -> g
f (Term f
t :$: Term f
u) = forall a b. (a -> b) -> Term a -> Term b
mapFun f -> g
f Term f
t forall f. Term f -> Term f -> Term f
:$: forall a b. (a -> b) -> Term a -> Term b
mapFun f -> g
f Term f
u
flatMapFun :: (f -> Term g) -> Term f -> Term g
flatMapFun :: forall f g. (f -> Term g) -> Term f -> Term g
flatMapFun f -> Term g
_ (Var Var
x) = forall f. Var -> Term f
Var Var
x
flatMapFun f -> Term g
f (Fun f
x) = f -> Term g
f f
x
flatMapFun f -> Term g
f (Term f
t :$: Term f
u) =
forall f g. (f -> Term g) -> Term f -> Term g
flatMapFun f -> Term g
f Term f
t forall f. Term f -> Term f -> Term f
:$: forall f g. (f -> Term g) -> Term f -> Term g
flatMapFun f -> Term g
f Term f
u
data OrId f = Id | NotId f
eliminateId :: Term (OrId f) -> Maybe (Term f)
eliminateId :: forall f. Term (OrId f) -> Maybe (Term f)
eliminateId Term (OrId f)
t = do
OrId (Term f)
t <- forall f. Term (OrId f) -> Maybe (OrId (Term f))
elim Term (OrId f)
t
case OrId (Term f)
t of
OrId (Term f)
Id -> forall a. Maybe a
Nothing
NotId Term f
t -> forall a. a -> Maybe a
Just Term f
t
where
elim :: Term (OrId f) -> Maybe (OrId (Term f))
elim :: forall f. Term (OrId f) -> Maybe (OrId (Term f))
elim (Var Var
x) = forall a. a -> Maybe a
Just (forall f. f -> OrId f
NotId (forall f. Var -> Term f
Var Var
x))
elim (Fun (NotId f
f)) = forall a. a -> Maybe a
Just (forall f. f -> OrId f
NotId (forall f. f -> Term f
Fun f
f))
elim (Fun OrId f
Id) = forall a. a -> Maybe a
Just forall f. OrId f
Id
elim (Term (OrId f)
t :$: Term (OrId f)
u) = do
OrId (Term f)
t <- forall f. Term (OrId f) -> Maybe (OrId (Term f))
elim Term (OrId f)
t
OrId (Term f)
u <- forall f. Term (OrId f) -> Maybe (OrId (Term f))
elim Term (OrId f)
u
case (OrId (Term f)
t, OrId (Term f)
u) of
(OrId (Term f)
Id, OrId (Term f)
_) -> forall a. a -> Maybe a
Just OrId (Term f)
u
(NotId Term f
_, OrId (Term f)
Id) -> forall a. Maybe a
Nothing
(NotId Term f
t, NotId Term f
u) -> forall a. a -> Maybe a
Just (forall f. f -> OrId f
NotId (Term f
t forall f. Term f -> Term f -> Term f
:$: Term f
u))
subterms :: Term f -> [Term f]
subterms :: forall f. Term f -> [Term f]
subterms Term f
t = Term f
tforall a. a -> [a] -> [a]
:forall f. Term f -> [Term f]
properSubterms Term f
t
properSubterms :: Term f -> [Term f]
properSubterms :: forall f. Term f -> [Term f]
properSubterms (Term f
t :$: Term f
u) = forall f. Term f -> [Term f]
subterms Term f
t forall a. [a] -> [a] -> [a]
++ forall f. Term f -> [Term f]
subterms Term f
u
properSubterms Term f
_ = []
subtermsFO :: Term f -> [Term f]
subtermsFO :: forall f. Term f -> [Term f]
subtermsFO Term f
t = Term f
tforall a. a -> [a] -> [a]
:forall f. Term f -> [Term f]
properSubtermsFO Term f
t
properSubtermsFO :: Term f -> [Term f]
properSubtermsFO :: forall f. Term f -> [Term f]
properSubtermsFO (Term f
_f :@: [Term f]
ts) = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall f. Term f -> [Term f]
subtermsFO [Term f]
ts
properSubtermsFO Term f
_ = []
canonicalise :: Symbolic fun a => a -> a
canonicalise :: forall fun a. Symbolic fun a => a -> a
canonicalise a
t = forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst (\Var
x -> forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. HasCallStack => a
undefined Var
x Map Var (Term fun)
sub) a
t
where
sub :: Map Var (Term fun)
sub =
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[(Var
x, forall f. Var -> Term f
Var (Type -> Int -> Var
V Type
ty Int
n))
| (x :: Var
x@(V Type
ty Int
_), Int
n) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Eq a => [a] -> [a]
nub (forall f a. Symbolic f a => a -> [Var]
vars a
t)) [Int
0..]]
evalTerm :: (Typed fun, Apply a, Monad m) => (Var -> m a) -> (fun -> m a) -> Term fun -> m a
evalTerm :: forall fun a (m :: * -> *).
(Typed fun, Apply a, Monad m) =>
(Var -> m a) -> (fun -> m a) -> Term fun -> m a
evalTerm Var -> m a
var fun -> m a
fun = Term fun -> m a
eval
where
eval :: Term fun -> m a
eval (Var Var
x) = Var -> m a
var Var
x
eval (Fun fun
f) = fun -> m a
fun fun
f
eval (Term fun
t :$: Term fun
u) = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. Apply a => a -> a -> a
apply (Term fun -> m a
eval Term fun
t) (Term fun -> m a
eval Term fun
u)
instance Typed f => Typed (Term f) where
typ :: Term f -> Type
typ (Var Var
x) = forall a. Typed a => a -> Type
typ Var
x
typ (Fun f
f) = forall a. Typed a => a -> Type
typ f
f
typ (Term f
t :$: Term f
_) = Int -> Type -> Type
typeDrop Int
1 (forall a. Typed a => a -> Type
typ Term f
t)
otherTypesDL :: Term f -> DList Type
otherTypesDL (Var Var
_) = forall a. Monoid a => a
mempty
otherTypesDL (Fun f
f) = forall a. Typed a => a -> DList Type
typesDL f
f
otherTypesDL (Term f
t :$: Term f
u) = forall a. Typed a => a -> DList Type
typesDL Term f
t forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Typed a => a -> DList Type
typesDL Term f
u
typeSubst_ :: (Var -> Builder TyCon) -> Term f -> Term f
typeSubst_ Var -> Builder TyCon
sub = Term f -> Term f
tsub
where
tsub :: Term f -> Term f
tsub (Var Var
x) = forall f. Var -> Term f
Var (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Var
x)
tsub (Fun f
f) = forall f. f -> Term f
Fun (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub f
f)
tsub (Term f
t :$: Term f
u) =
forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Term f
t forall f. Term f -> Term f -> Term f
:$: forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Term f
u
instance (PrettyTerm f, Typed f) => Apply (Term f) where
tryApply :: Term f -> Term f -> Maybe (Term f)
tryApply Term f
t Term f
u = do
forall a. Apply a => a -> a -> Maybe a
tryApply (forall a. Typed a => a -> Type
typ Term f
t) (forall a. Typed a => a -> Type
typ Term f
u)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term f
t forall f. Term f -> Term f -> Term f
:$: Term f
u)
depth :: Term f -> Int
depth :: forall a. Term a -> Int
depth Var{} = Int
1
depth Fun{} = Int
1
depth (Term f
t :$: Term f
u) = forall a. Term a -> Int
depth Term f
t forall a. Ord a => a -> a -> a
`max` (Int
1forall a. Num a => a -> a -> a
+forall a. Term a -> Int
depth Term f
u)
type Measure f = (Int, Int, Int, Int, MeasureFuns f, Int, [Var])
measure :: (Sized f, Typed f) => Term f -> Measure f
measure :: forall f. (Sized f, Typed f) => Term f -> Measure f
measure Term f
t =
(forall a. Term a -> Int
depth Term f
t, forall a. Sized a => a -> Int
size Term f
t, forall {a}. Typed a => Term a -> Int
missing Term f
t, -forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall f a. Symbolic f a => a -> [Var]
vars Term f
t), forall f. Term f -> MeasureFuns f
MeasureFuns (forall {f}. Term f -> Term f
skel Term f
t),
-forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Ord a => [a] -> [a]
usort (forall f a. Symbolic f a => a -> [Var]
vars Term f
t)), forall f a. Symbolic f a => a -> [Var]
vars Term f
t)
where
skel :: Term f -> Term f
skel (Var (V Type
ty Int
_)) = forall f. Var -> Term f
Var (Type -> Int -> Var
V Type
ty Int
0)
skel (Fun f
f) = forall f. f -> Term f
Fun f
f
skel (Term f
t :$: Term f
u) = Term f -> Term f
skel Term f
t forall f. Term f -> Term f -> Term f
:$: Term f -> Term f
skel Term f
u
missing :: Term a -> Int
missing (Fun a
f :@: [Term a]
ts) =
Type -> Int
typeArity (forall a. Typed a => a -> Type
typ a
f) forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term a]
ts 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 Term a -> Int
missing [Term a]
ts)
missing (Var Var
_ :@: [Term a]
ts) =
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b. (a -> b) -> [a] -> [b]
map Term a -> Int
missing [Term a]
ts)
newtype MeasureFuns f = MeasureFuns (Term f)
instance Ord f => Eq (MeasureFuns f) where
MeasureFuns f
t == :: MeasureFuns f -> MeasureFuns f -> Bool
== MeasureFuns f
u = forall a. Ord a => a -> a -> Ordering
compare MeasureFuns f
t MeasureFuns f
u forall a. Eq a => a -> a -> Bool
== Ordering
EQ
instance Ord f => Ord (MeasureFuns f) where
compare :: MeasureFuns f -> MeasureFuns f -> Ordering
compare (MeasureFuns Term f
t) (MeasureFuns Term f
u) = forall f. Ord f => Term f -> Term f -> Ordering
compareFuns Term f
t Term f
u
compareFuns :: Ord f => Term f -> Term f -> Ordering
compareFuns :: forall f. Ord f => Term f -> Term f -> Ordering
compareFuns (Term f
f :@: [Term f]
ts) (Term f
g :@: [Term f]
us) =
forall f. Ord f => Term f -> Term f -> Ordering
compareHead Term f
f Term f
g forall a. Monoid a => a -> a -> a
`mappend` forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (forall a b. (a -> b) -> [a] -> [b]
map forall f. Term f -> MeasureFuns f
MeasureFuns) [Term f]
ts [Term f]
us
where
compareHead :: Term a -> Term a -> Ordering
compareHead (Var Var
x) (Var Var
y) = forall a. Ord a => a -> a -> Ordering
compare Var
x Var
y
compareHead (Var Var
_) Term a
_ = Ordering
LT
compareHead Term a
_ (Var Var
_) = Ordering
GT
compareHead (Fun a
f) (Fun a
g) = forall a. Ord a => a -> a -> Ordering
compare a
f a
g
compareHead Term a
_ Term a
_ = forall a. HasCallStack => String -> a
error String
"viewApp"
data a :+: b = Inl a | Inr b deriving ((a :+: b) -> (a :+: b) -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => (a :+: b) -> (a :+: b) -> Bool
/= :: (a :+: b) -> (a :+: b) -> Bool
$c/= :: forall a b. (Eq a, Eq b) => (a :+: b) -> (a :+: b) -> Bool
== :: (a :+: b) -> (a :+: b) -> Bool
$c== :: forall a b. (Eq a, Eq b) => (a :+: b) -> (a :+: b) -> Bool
Eq, (a :+: b) -> (a :+: b) -> Bool
(a :+: b) -> (a :+: b) -> 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 {a} {b}. (Ord a, Ord b) => Eq (a :+: b)
forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Bool
forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Ordering
forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> a :+: b
min :: (a :+: b) -> (a :+: b) -> a :+: b
$cmin :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> a :+: b
max :: (a :+: b) -> (a :+: b) -> a :+: b
$cmax :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> a :+: b
>= :: (a :+: b) -> (a :+: b) -> Bool
$c>= :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Bool
> :: (a :+: b) -> (a :+: b) -> Bool
$c> :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Bool
<= :: (a :+: b) -> (a :+: b) -> Bool
$c<= :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Bool
< :: (a :+: b) -> (a :+: b) -> Bool
$c< :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Bool
compare :: (a :+: b) -> (a :+: b) -> Ordering
$ccompare :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Ordering
Ord)
instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where
size :: (fun1 :+: fun2) -> Int
size (Inl fun1
x) = forall a. Sized a => a -> Int
size fun1
x
size (Inr fun2
x) = forall a. Sized a => a -> Int
size fun2
x
instance (Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) where
typ :: (fun1 :+: fun2) -> Type
typ (Inl fun1
x) = forall a. Typed a => a -> Type
typ fun1
x
typ (Inr fun2
x) = forall a. Typed a => a -> Type
typ fun2
x
otherTypesDL :: (fun1 :+: fun2) -> DList Type
otherTypesDL (Inl fun1
x) = forall a. Typed a => a -> DList Type
otherTypesDL fun1
x
otherTypesDL (Inr fun2
x) = forall a. Typed a => a -> DList Type
otherTypesDL fun2
x
typeSubst_ :: (Var -> Builder TyCon) -> (fun1 :+: fun2) -> fun1 :+: fun2
typeSubst_ Var -> Builder TyCon
sub (Inl fun1
x) = forall a b. a -> a :+: b
Inl (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub fun1
x)
typeSubst_ Var -> Builder TyCon
sub (Inr fun2
x) = forall a b. b -> a :+: b
Inr (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub fun2
x)
instance (Pretty fun1, Pretty fun2) => Pretty (fun1 :+: fun2) where
pPrintPrec :: PrettyLevel -> Rational -> (fun1 :+: fun2) -> Doc
pPrintPrec PrettyLevel
l Rational
p (Inl fun1
x) = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
p fun1
x
pPrintPrec PrettyLevel
l Rational
p (Inr fun2
x) = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
p fun2
x
instance (PrettyTerm fun1, PrettyTerm fun2) => PrettyTerm (fun1 :+: fun2) where
termStyle :: (fun1 :+: fun2) -> TermStyle
termStyle (Inl fun1
x) = forall f. PrettyTerm f => f -> TermStyle
termStyle fun1
x
termStyle (Inr fun2
x) = forall f. PrettyTerm f => f -> TermStyle
termStyle fun2
x