-- Based on: http://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html

module U.Core.ABT where

import Control.Lens (Lens', use, (.=))
import Control.Monad.State
import Data.Foldable qualified as Foldable
import Data.Set qualified as Set
import Debug.RecoverRTTI qualified as RTTI
import U.Core.ABT.Var (Var (freshIn))
import Unison.Debug qualified as Debug
import Unison.Prelude
import Unison.Util.Recursion
import Prelude hiding (abs, cycle)

data ABT f v r
  = Var v
  | Cycle r
  | Abs v r
  | Tm (f r)
  deriving stock (ABT f v r -> ABT f v r -> Bool
(ABT f v r -> ABT f v r -> Bool)
-> (ABT f v r -> ABT f v r -> Bool) -> Eq (ABT f v r)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (f :: * -> *) v r.
(Eq v, Eq r, Eq (f r)) =>
ABT f v r -> ABT f v r -> Bool
$c== :: forall (f :: * -> *) v r.
(Eq v, Eq r, Eq (f r)) =>
ABT f v r -> ABT f v r -> Bool
== :: ABT f v r -> ABT f v r -> Bool
$c/= :: forall (f :: * -> *) v r.
(Eq v, Eq r, Eq (f r)) =>
ABT f v r -> ABT f v r -> Bool
/= :: ABT f v r -> ABT f v r -> Bool
Eq, Int -> ABT f v r -> ShowS
[ABT f v r] -> ShowS
ABT f v r -> String
(Int -> ABT f v r -> ShowS)
-> (ABT f v r -> String)
-> ([ABT f v r] -> ShowS)
-> Show (ABT f v r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (f :: * -> *) v r.
(Show v, Show r, Show (f r)) =>
Int -> ABT f v r -> ShowS
forall (f :: * -> *) v r.
(Show v, Show r, Show (f r)) =>
[ABT f v r] -> ShowS
forall (f :: * -> *) v r.
(Show v, Show r, Show (f r)) =>
ABT f v r -> String
$cshowsPrec :: forall (f :: * -> *) v r.
(Show v, Show r, Show (f r)) =>
Int -> ABT f v r -> ShowS
showsPrec :: Int -> ABT f v r -> ShowS
$cshow :: forall (f :: * -> *) v r.
(Show v, Show r, Show (f r)) =>
ABT f v r -> String
show :: ABT f v r -> String
$cshowList :: forall (f :: * -> *) v r.
(Show v, Show r, Show (f r)) =>
[ABT f v r] -> ShowS
showList :: [ABT f v r] -> ShowS
Show, (forall a b. (a -> b) -> ABT f v a -> ABT f v b)
-> (forall a b. a -> ABT f v b -> ABT f v a) -> Functor (ABT f v)
forall a b. a -> ABT f v b -> ABT f v a
forall a b. (a -> b) -> ABT f v a -> ABT f v b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (f :: * -> *) v a b.
Functor f =>
a -> ABT f v b -> ABT f v a
forall (f :: * -> *) v a b.
Functor f =>
(a -> b) -> ABT f v a -> ABT f v b
$cfmap :: forall (f :: * -> *) v a b.
Functor f =>
(a -> b) -> ABT f v a -> ABT f v b
fmap :: forall a b. (a -> b) -> ABT f v a -> ABT f v b
$c<$ :: forall (f :: * -> *) v a b.
Functor f =>
a -> ABT f v b -> ABT f v a
<$ :: forall a b. a -> ABT f v b -> ABT f v a
Functor, (forall m. Monoid m => ABT f v m -> m)
-> (forall m a. Monoid m => (a -> m) -> ABT f v a -> m)
-> (forall m a. Monoid m => (a -> m) -> ABT f v a -> m)
-> (forall a b. (a -> b -> b) -> b -> ABT f v a -> b)
-> (forall a b. (a -> b -> b) -> b -> ABT f v a -> b)
-> (forall b a. (b -> a -> b) -> b -> ABT f v a -> b)
-> (forall b a. (b -> a -> b) -> b -> ABT f v a -> b)
-> (forall a. (a -> a -> a) -> ABT f v a -> a)
-> (forall a. (a -> a -> a) -> ABT f v a -> a)
-> (forall a. ABT f v a -> [a])
-> (forall a. ABT f v a -> Bool)
-> (forall a. ABT f v a -> Int)
-> (forall a. Eq a => a -> ABT f v a -> Bool)
-> (forall a. Ord a => ABT f v a -> a)
-> (forall a. Ord a => ABT f v a -> a)
-> (forall a. Num a => ABT f v a -> a)
-> (forall a. Num a => ABT f v a -> a)
-> Foldable (ABT f v)
forall a. Eq a => a -> ABT f v a -> Bool
forall a. Num a => ABT f v a -> a
forall a. Ord a => ABT f v a -> a
forall m. Monoid m => ABT f v m -> m
forall a. ABT f v a -> Bool
forall a. ABT f v a -> Int
forall a. ABT f v a -> [a]
forall a. (a -> a -> a) -> ABT f v a -> a
forall m a. Monoid m => (a -> m) -> ABT f v a -> m
forall b a. (b -> a -> b) -> b -> ABT f v a -> b
forall a b. (a -> b -> b) -> b -> ABT f v 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
forall (f :: * -> *) v a.
(Foldable f, Eq a) =>
a -> ABT f v a -> Bool
forall (f :: * -> *) v a. (Foldable f, Num a) => ABT f v a -> a
forall (f :: * -> *) v a. (Foldable f, Ord a) => ABT f v a -> a
forall (f :: * -> *) v m. (Foldable f, Monoid m) => ABT f v m -> m
forall (f :: * -> *) v a. Foldable f => ABT f v a -> Bool
forall (f :: * -> *) v a. Foldable f => ABT f v a -> Int
forall (f :: * -> *) v a. Foldable f => ABT f v a -> [a]
forall (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> ABT f v a -> a
forall (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> ABT f v a -> m
forall (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> ABT f v a -> b
forall (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> ABT f v a -> b
$cfold :: forall (f :: * -> *) v m. (Foldable f, Monoid m) => ABT f v m -> m
fold :: forall m. Monoid m => ABT f v m -> m
$cfoldMap :: forall (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> ABT f v a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> ABT f v a -> m
$cfoldMap' :: forall (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> ABT f v a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> ABT f v a -> m
$cfoldr :: forall (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> ABT f v a -> b
foldr :: forall a b. (a -> b -> b) -> b -> ABT f v a -> b
$cfoldr' :: forall (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> ABT f v a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> ABT f v a -> b
$cfoldl :: forall (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> ABT f v a -> b
foldl :: forall b a. (b -> a -> b) -> b -> ABT f v a -> b
$cfoldl' :: forall (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> ABT f v a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> ABT f v a -> b
$cfoldr1 :: forall (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> ABT f v a -> a
foldr1 :: forall a. (a -> a -> a) -> ABT f v a -> a
$cfoldl1 :: forall (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> ABT f v a -> a
foldl1 :: forall a. (a -> a -> a) -> ABT f v a -> a
$ctoList :: forall (f :: * -> *) v a. Foldable f => ABT f v a -> [a]
toList :: forall a. ABT f v a -> [a]
$cnull :: forall (f :: * -> *) v a. Foldable f => ABT f v a -> Bool
null :: forall a. ABT f v a -> Bool
$clength :: forall (f :: * -> *) v a. Foldable f => ABT f v a -> Int
length :: forall a. ABT f v a -> Int
$celem :: forall (f :: * -> *) v a.
(Foldable f, Eq a) =>
a -> ABT f v a -> Bool
elem :: forall a. Eq a => a -> ABT f v a -> Bool
$cmaximum :: forall (f :: * -> *) v a. (Foldable f, Ord a) => ABT f v a -> a
maximum :: forall a. Ord a => ABT f v a -> a
$cminimum :: forall (f :: * -> *) v a. (Foldable f, Ord a) => ABT f v a -> a
minimum :: forall a. Ord a => ABT f v a -> a
$csum :: forall (f :: * -> *) v a. (Foldable f, Num a) => ABT f v a -> a
sum :: forall a. Num a => ABT f v a -> a
$cproduct :: forall (f :: * -> *) v a. (Foldable f, Num a) => ABT f v a -> a
product :: forall a. Num a => ABT f v a -> a
Foldable, Functor (ABT f v)
Foldable (ABT f v)
(Functor (ABT f v), Foldable (ABT f v)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> ABT f v a -> f (ABT f v b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    ABT f v (f a) -> f (ABT f v a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ABT f v a -> m (ABT f v b))
-> (forall (m :: * -> *) a.
    Monad m =>
    ABT f v (m a) -> m (ABT f v a))
-> Traversable (ABT f v)
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 => ABT f v (m a) -> m (ABT f v a)
forall (f :: * -> *) a.
Applicative f =>
ABT f v (f a) -> f (ABT f v a)
forall (f :: * -> *) v. Traversable f => Functor (ABT f v)
forall (f :: * -> *) v. Traversable f => Foldable (ABT f v)
forall (f :: * -> *) v (m :: * -> *) a.
(Traversable f, Monad m) =>
ABT f v (m a) -> m (ABT f v a)
forall (f :: * -> *) v (f :: * -> *) a.
(Traversable f, Applicative f) =>
ABT f v (f a) -> f (ABT f v a)
forall (f :: * -> *) v (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> ABT f v a -> m (ABT f v b)
forall (f :: * -> *) v (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> ABT f v a -> f (ABT f v b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ABT f v a -> m (ABT f v b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ABT f v a -> f (ABT f v b)
$ctraverse :: forall (f :: * -> *) v (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> ABT f v a -> f (ABT f v b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ABT f v a -> f (ABT f v b)
$csequenceA :: forall (f :: * -> *) v (f :: * -> *) a.
(Traversable f, Applicative f) =>
ABT f v (f a) -> f (ABT f v a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
ABT f v (f a) -> f (ABT f v a)
$cmapM :: forall (f :: * -> *) v (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> ABT f v a -> m (ABT f v b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ABT f v a -> m (ABT f v b)
$csequence :: forall (f :: * -> *) v (m :: * -> *) a.
(Traversable f, Monad m) =>
ABT f v (m a) -> m (ABT f v a)
sequence :: forall (m :: * -> *) a. Monad m => ABT f v (m a) -> m (ABT f v a)
Traversable, (forall x. ABT f v r -> Rep (ABT f v r) x)
-> (forall x. Rep (ABT f v r) x -> ABT f v r)
-> Generic (ABT f v r)
forall x. Rep (ABT f v r) x -> ABT f v r
forall x. ABT f v r -> Rep (ABT f v r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (f :: * -> *) v r x. Rep (ABT f v r) x -> ABT f v r
forall (f :: * -> *) v r x. ABT f v r -> Rep (ABT f v r) x
$cfrom :: forall (f :: * -> *) v r x. ABT f v r -> Rep (ABT f v r) x
from :: forall x. ABT f v r -> Rep (ABT f v r) x
$cto :: forall (f :: * -> *) v r x. Rep (ABT f v r) x -> ABT f v r
to :: forall x. Rep (ABT f v r) x -> ABT f v r
Generic)

-- | At each level in the tree, we store the set of free variables and
-- a value of type `a`. Variables are of type `v`.
data Term f v a = Term {forall (f :: * -> *) v a. Term f v a -> Set v
freeVars :: Set v, forall (f :: * -> *) v a. Term f v a -> a
annotation :: a, forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out :: ABT f v (Term f v a)}
  deriving ((forall a b. (a -> b) -> Term f v a -> Term f v b)
-> (forall a b. a -> Term f v b -> Term f v a)
-> Functor (Term f v)
forall a b. a -> Term f v b -> Term f v a
forall a b. (a -> b) -> Term f v a -> Term f v b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (f :: * -> *) v a b.
Functor f =>
a -> Term f v b -> Term f v a
forall (f :: * -> *) v a b.
Functor f =>
(a -> b) -> Term f v a -> Term f v b
$cfmap :: forall (f :: * -> *) v a b.
Functor f =>
(a -> b) -> Term f v a -> Term f v b
fmap :: forall a b. (a -> b) -> Term f v a -> Term f v b
$c<$ :: forall (f :: * -> *) v a b.
Functor f =>
a -> Term f v b -> Term f v a
<$ :: forall a b. a -> Term f v b -> Term f v a
Functor, (forall m. Monoid m => Term f v m -> m)
-> (forall m a. Monoid m => (a -> m) -> Term f v a -> m)
-> (forall m a. Monoid m => (a -> m) -> Term f v a -> m)
-> (forall a b. (a -> b -> b) -> b -> Term f v a -> b)
-> (forall a b. (a -> b -> b) -> b -> Term f v a -> b)
-> (forall b a. (b -> a -> b) -> b -> Term f v a -> b)
-> (forall b a. (b -> a -> b) -> b -> Term f v a -> b)
-> (forall a. (a -> a -> a) -> Term f v a -> a)
-> (forall a. (a -> a -> a) -> Term f v a -> a)
-> (forall a. Term f v a -> [a])
-> (forall a. Term f v a -> Bool)
-> (forall a. Term f v a -> Int)
-> (forall a. Eq a => a -> Term f v a -> Bool)
-> (forall a. Ord a => Term f v a -> a)
-> (forall a. Ord a => Term f v a -> a)
-> (forall a. Num a => Term f v a -> a)
-> (forall a. Num a => Term f v a -> a)
-> Foldable (Term f v)
forall a. Eq a => a -> Term f v a -> Bool
forall a. Num a => Term f v a -> a
forall a. Ord a => Term f v a -> a
forall m. Monoid m => Term f v m -> m
forall a. Term f v a -> Bool
forall a. Term f v a -> Int
forall a. Term f v a -> [a]
forall a. (a -> a -> a) -> Term f v a -> a
forall m a. Monoid m => (a -> m) -> Term f v a -> m
forall b a. (b -> a -> b) -> b -> Term f v a -> b
forall a b. (a -> b -> b) -> b -> Term f v 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
forall (f :: * -> *) v a.
(Foldable f, Eq a) =>
a -> Term f v a -> Bool
forall (f :: * -> *) v a. (Foldable f, Num a) => Term f v a -> a
forall (f :: * -> *) v a. (Foldable f, Ord a) => Term f v a -> a
forall (f :: * -> *) v m. (Foldable f, Monoid m) => Term f v m -> m
forall (f :: * -> *) v a. Foldable f => Term f v a -> Bool
forall (f :: * -> *) v a. Foldable f => Term f v a -> Int
forall (f :: * -> *) v a. Foldable f => Term f v a -> [a]
forall (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> Term f v a -> a
forall (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> Term f v a -> m
forall (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> Term f v a -> b
forall (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> Term f v a -> b
$cfold :: forall (f :: * -> *) v m. (Foldable f, Monoid m) => Term f v m -> m
fold :: forall m. Monoid m => Term f v m -> m
$cfoldMap :: forall (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> Term f v a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Term f v a -> m
$cfoldMap' :: forall (f :: * -> *) v m a.
(Foldable f, Monoid m) =>
(a -> m) -> Term f v a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Term f v a -> m
$cfoldr :: forall (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> Term f v a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Term f v a -> b
$cfoldr' :: forall (f :: * -> *) v a b.
Foldable f =>
(a -> b -> b) -> b -> Term f v a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Term f v a -> b
$cfoldl :: forall (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> Term f v a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Term f v a -> b
$cfoldl' :: forall (f :: * -> *) v b a.
Foldable f =>
(b -> a -> b) -> b -> Term f v a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Term f v a -> b
$cfoldr1 :: forall (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> Term f v a -> a
foldr1 :: forall a. (a -> a -> a) -> Term f v a -> a
$cfoldl1 :: forall (f :: * -> *) v a.
Foldable f =>
(a -> a -> a) -> Term f v a -> a
foldl1 :: forall a. (a -> a -> a) -> Term f v a -> a
$ctoList :: forall (f :: * -> *) v a. Foldable f => Term f v a -> [a]
toList :: forall a. Term f v a -> [a]
$cnull :: forall (f :: * -> *) v a. Foldable f => Term f v a -> Bool
null :: forall a. Term f v a -> Bool
$clength :: forall (f :: * -> *) v a. Foldable f => Term f v a -> Int
length :: forall a. Term f v a -> Int
$celem :: forall (f :: * -> *) v a.
(Foldable f, Eq a) =>
a -> Term f v a -> Bool
elem :: forall a. Eq a => a -> Term f v a -> Bool
$cmaximum :: forall (f :: * -> *) v a. (Foldable f, Ord a) => Term f v a -> a
maximum :: forall a. Ord a => Term f v a -> a
$cminimum :: forall (f :: * -> *) v a. (Foldable f, Ord a) => Term f v a -> a
minimum :: forall a. Ord a => Term f v a -> a
$csum :: forall (f :: * -> *) v a. (Foldable f, Num a) => Term f v a -> a
sum :: forall a. Num a => Term f v a -> a
$cproduct :: forall (f :: * -> *) v a. (Foldable f, Num a) => Term f v a -> a
product :: forall a. Num a => Term f v a -> a
Foldable, (forall x. Term f v a -> Rep (Term f v a) x)
-> (forall x. Rep (Term f v a) x -> Term f v a)
-> Generic (Term f v a)
forall x. Rep (Term f v a) x -> Term f v a
forall x. Term f v a -> Rep (Term f v a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (f :: * -> *) v a x. Rep (Term f v a) x -> Term f v a
forall (f :: * -> *) v a x. Term f v a -> Rep (Term f v a) x
$cfrom :: forall (f :: * -> *) v a x. Term f v a -> Rep (Term f v a) x
from :: forall x. Term f v a -> Rep (Term f v a) x
$cto :: forall (f :: * -> *) v a x. Rep (Term f v a) x -> Term f v a
to :: forall x. Rep (Term f v a) x -> Term f v a
Generic, Functor (Term f v)
Foldable (Term f v)
(Functor (Term f v), Foldable (Term f v)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Term f v a -> f (Term f v b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Term f v (f a) -> f (Term f v a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Term f v a -> m (Term f v b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Term f v (m a) -> m (Term f v a))
-> Traversable (Term f v)
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 f v (m a) -> m (Term f v a)
forall (f :: * -> *) a.
Applicative f =>
Term f v (f a) -> f (Term f v a)
forall (f :: * -> *) v. Traversable f => Functor (Term f v)
forall (f :: * -> *) v. Traversable f => Foldable (Term f v)
forall (f :: * -> *) v (m :: * -> *) a.
(Traversable f, Monad m) =>
Term f v (m a) -> m (Term f v a)
forall (f :: * -> *) v (f :: * -> *) a.
(Traversable f, Applicative f) =>
Term f v (f a) -> f (Term f v a)
forall (f :: * -> *) v (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Term f v a -> m (Term f v b)
forall (f :: * -> *) v (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Term f v a -> f (Term f v b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Term f v a -> m (Term f v b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Term f v a -> f (Term f v b)
$ctraverse :: forall (f :: * -> *) v (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Term f v a -> f (Term f v b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Term f v a -> f (Term f v b)
$csequenceA :: forall (f :: * -> *) v (f :: * -> *) a.
(Traversable f, Applicative f) =>
Term f v (f a) -> f (Term f v a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Term f v (f a) -> f (Term f v a)
$cmapM :: forall (f :: * -> *) v (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Term f v a -> m (Term f v b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Term f v a -> m (Term f v b)
$csequence :: forall (f :: * -> *) v (m :: * -> *) a.
(Traversable f, Monad m) =>
Term f v (m a) -> m (Term f v a)
sequence :: forall (m :: * -> *) a. Monad m => Term f v (m a) -> m (Term f v a)
Traversable)

data Term' f v a x = Term' {forall (f :: * -> *) v a x. Term' f v a x -> Set v
freeVars' :: Set v, forall (f :: * -> *) v a x. Term' f v a x -> a
annotation' :: a, forall (f :: * -> *) v a x. Term' f v a x -> ABT f v x
out' :: ABT f v x}
  deriving ((forall a b. (a -> b) -> Term' f v a a -> Term' f v a b)
-> (forall a b. a -> Term' f v a b -> Term' f v a a)
-> Functor (Term' f v a)
forall a b. a -> Term' f v a b -> Term' f v a a
forall a b. (a -> b) -> Term' f v a a -> Term' f v a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (f :: * -> *) v a a b.
Functor f =>
a -> Term' f v a b -> Term' f v a a
forall (f :: * -> *) v a a b.
Functor f =>
(a -> b) -> Term' f v a a -> Term' f v a b
$cfmap :: forall (f :: * -> *) v a a b.
Functor f =>
(a -> b) -> Term' f v a a -> Term' f v a b
fmap :: forall a b. (a -> b) -> Term' f v a a -> Term' f v a b
$c<$ :: forall (f :: * -> *) v a a b.
Functor f =>
a -> Term' f v a b -> Term' f v a a
<$ :: forall a b. a -> Term' f v a b -> Term' f v a a
Functor)

instance (Functor f) => Recursive (Term f v a) (Term' f v a) where
  embed :: Term' f v a (Term f v a) -> Term f v a
embed (Term' Set v
vs a
a ABT f v (Term f v a)
abt) = Set v -> a -> ABT f v (Term f v a) -> Term f v a
forall (f :: * -> *) v a.
Set v -> a -> ABT f v (Term f v a) -> Term f v a
Term Set v
vs a
a ABT f v (Term f v a)
abt
  project :: Term f v a -> Term' f v a (Term f v a)
project (Term Set v
vs a
a ABT f v (Term f v a)
abt) = Set v -> a -> ABT f v (Term f v a) -> Term' f v a (Term f v a)
forall (f :: * -> *) v a x.
Set v -> a -> ABT f v x -> Term' f v a x
Term' Set v
vs a
a ABT f v (Term f v a)
abt

instance (Foldable f, Functor f, forall a. (Eq a) => Eq (f a), Var v) => Eq (Term f v a) where
  -- alpha equivalence, works by renaming any aligned Abs ctors to use a common fresh variable
  Term f v a
t1 == :: Term f v a -> Term f v a -> Bool
== Term f v a
t2 = ABT f v (Term f v a) -> ABT f v (Term f v a) -> Bool
go (Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
t1) (Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
t2)
    where
      go :: ABT f v (Term f v a) -> ABT f v (Term f v a) -> Bool
      go :: ABT f v (Term f v a) -> ABT f v (Term f v a) -> Bool
go (Var v
v) (Var v
v2) | v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2 = Bool
True
      go (Cycle Term f v a
t1) (Cycle Term f v a
t2) = Term f v a
t1 Term f v a -> Term f v a -> Bool
forall a. Eq a => a -> a -> Bool
== Term f v a
t2
      go (Abs v
v1 Term f v a
body1) (Abs v
v2 Term f v a
body2) =
        if v
v1 v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2
          then Term f v a
body1 Term f v a -> Term f v a -> Bool
forall a. Eq a => a -> a -> Bool
== Term f v a
body2
          else
            let v3 :: v
v3 = Term f v a -> Term f v a -> v -> v
forall v (f :: * -> *) a.
Var v =>
Term f v a -> Term f v a -> v -> v
freshInBoth Term f v a
body1 Term f v a
body2 v
v1
             in v -> v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
v1 v
v3 Term f v a
body1 Term f v a -> Term f v a -> Bool
forall a. Eq a => a -> a -> Bool
== v -> v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
v2 v
v3 Term f v a
body2
      go (Tm f (Term f v a)
f1) (Tm f (Term f v a)
f2) = f (Term f v a)
f1 f (Term f v a) -> f (Term f v a) -> Bool
forall a. Eq a => a -> a -> Bool
== f (Term f v a)
f2
      go ABT f v (Term f v a)
_ ABT f v (Term f v a)
_ = Bool
False

instance
  ( forall a. (Eq a) => Eq (f a),
    Foldable f,
    Functor f,
    forall a. (Ord a) => Ord (f a),
    Var v
  ) =>
  Ord (Term f v a)
  where
  -- alpha equivalence, works by renaming any aligned Abs ctors to use a common fresh variable
  Term f v a
t1 compare :: Term f v a -> Term f v a -> Ordering
`compare` Term f v a
t2 = ABT f v (Term f v a) -> ABT f v (Term f v a) -> Ordering
go (Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
t1) (Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
t2)
    where
      go :: ABT f v (Term f v a) -> ABT f v (Term f v a) -> Ordering
      go :: ABT f v (Term f v a) -> ABT f v (Term f v a) -> Ordering
go (Var v
v) (Var v
v2) = v
v v -> v -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` v
v2
      go (Cycle Term f v a
t1) (Cycle Term f v a
t2) = Term f v a
t1 Term f v a -> Term f v a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Term f v a
t2
      go (Abs v
v1 Term f v a
body1) (Abs v
v2 Term f v a
body2) =
        if v
v1 v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2
          then Term f v a
body1 Term f v a -> Term f v a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Term f v a
body2
          else
            let v3 :: v
v3 = Term f v a -> Term f v a -> v -> v
forall v (f :: * -> *) a.
Var v =>
Term f v a -> Term f v a -> v -> v
freshInBoth Term f v a
body1 Term f v a
body2 v
v1
             in v -> v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
v1 v
v3 Term f v a
body1 Term f v a -> Term f v a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` v -> v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
v2 v
v3 Term f v a
body2
      go (Tm f (Term f v a)
f1) (Tm f (Term f v a)
f2) = f (Term f v a) -> f (Term f v a) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare f (Term f v a)
f1 f (Term f v a)
f2
      go ABT f v (Term f v a)
t1 ABT f v (Term f v a)
t2 = ABT f v (Term f v a) -> Word
forall {f :: * -> *} {v} {r}. ABT f v r -> Word
tag ABT f v (Term f v a)
t1 Word -> Word -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` ABT f v (Term f v a) -> Word
forall {f :: * -> *} {v} {r}. ABT f v r -> Word
tag ABT f v (Term f v a)
t2
      tag :: ABT f v r -> Word
tag (Var v
_) = Word
0 :: Word
      tag (Tm f r
_) = Word
1
      tag (Abs v
_ r
_) = Word
2
      tag (Cycle r
_) = Word
3

instance (forall a. (Show a) => Show (f a), Show v) => Show (Term f v a) where
  showsPrec :: Int -> Term f v a -> ShowS
showsPrec Int
p (Term Set v
_ a
ann ABT f v (Term f v a)
out) = case ABT f v (Term f v a)
out of
    Var v
v -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
9) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ \String
x -> String
showAnn String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"Var " String -> ShowS
forall a. [a] -> [a] -> [a]
++ v -> String
forall a. Show a => a -> String
show v
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x
    Cycle Term f v a
body -> (\String
s -> String
showAnn String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"Cycle " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term f v a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Term f v a
body
    Abs v
v Term f v a
body -> Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (\String
s -> String
showAnn String -> ShowS
forall a. [a] -> [a] -> [a]
++ v -> String
forall a. Show a => a -> String
show v
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
". " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term f v a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Term f v a
body
    Tm f (Term f v a)
f -> (String
showAnn String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f (Term f v a) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p f (Term f v a)
f
    where
      showAnn :: String
showAnn =
        if DebugFlag -> Bool
Debug.shouldDebug DebugFlag
Debug.Annotations
          then String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. a -> String
RTTI.anythingToString a
ann String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
          else String
""

amap :: (Functor f) => (a -> a') -> Term f v a -> Term f v a'
amap :: forall (f :: * -> *) a a' v.
Functor f =>
(a -> a') -> Term f v a -> Term f v a'
amap = (a -> a') -> Term f v a -> Term f v a'
forall a b. (a -> b) -> Term f v a -> Term f v b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap

vmap :: (Functor f, Foldable f, Ord v') => (v -> v') -> Term f v a -> Term f v' a
vmap :: forall (f :: * -> *) v' v a.
(Functor f, Foldable f, Ord v') =>
(v -> v') -> Term f v a -> Term f v' a
vmap v -> v'
f (Term Set v
_ a
a ABT f v (Term f v a)
out) = case ABT f v (Term f v a)
out of
  Var v
v -> a -> v' -> Term f v' a
forall a v (f :: * -> *). a -> v -> Term f v a
var a
a (v -> v'
f v
v)
  Tm f (Term f v a)
fa -> a -> f (Term f v' a) -> Term f v' a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm a
a ((Term f v a -> Term f v' a) -> f (Term f v a) -> f (Term f v' a)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((v -> v') -> Term f v a -> Term f v' a
forall (f :: * -> *) v' v a.
(Functor f, Foldable f, Ord v') =>
(v -> v') -> Term f v a -> Term f v' a
vmap v -> v'
f) f (Term f v a)
fa)
  Cycle Term f v a
r -> a -> Term f v' a -> Term f v' a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle a
a ((v -> v') -> Term f v a -> Term f v' a
forall (f :: * -> *) v' v a.
(Functor f, Foldable f, Ord v') =>
(v -> v') -> Term f v a -> Term f v' a
vmap v -> v'
f Term f v a
r)
  Abs v
v Term f v a
body -> a -> v' -> Term f v' a -> Term f v' a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs a
a (v -> v'
f v
v) ((v -> v') -> Term f v a -> Term f v' a
forall (f :: * -> *) v' v a.
(Functor f, Foldable f, Ord v') =>
(v -> v') -> Term f v a -> Term f v' a
vmap v -> v'
f Term f v a
body)

vmapM :: (Applicative m, Traversable f, Foldable f, Ord v2) => (v -> m v2) -> Term f v a -> m (Term f v2 a)
vmapM :: forall (m :: * -> *) (f :: * -> *) v2 v a.
(Applicative m, Traversable f, Foldable f, Ord v2) =>
(v -> m v2) -> Term f v a -> m (Term f v2 a)
vmapM v -> m v2
f (Term Set v
_ a
a ABT f v (Term f v a)
out) = case ABT f v (Term f v a)
out of
  Var v
v -> a -> v2 -> Term f v2 a
forall a v (f :: * -> *). a -> v -> Term f v a
var a
a (v2 -> Term f v2 a) -> m v2 -> m (Term f v2 a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v -> m v2
f v
v
  Tm f (Term f v a)
fa -> a -> f (Term f v2 a) -> Term f v2 a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm a
a (f (Term f v2 a) -> Term f v2 a)
-> m (f (Term f v2 a)) -> m (Term f v2 a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term f v a -> m (Term f v2 a))
-> f (Term f v a) -> m (f (Term f v2 a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((v -> m v2) -> Term f v a -> m (Term f v2 a)
forall (m :: * -> *) (f :: * -> *) v2 v a.
(Applicative m, Traversable f, Foldable f, Ord v2) =>
(v -> m v2) -> Term f v a -> m (Term f v2 a)
vmapM v -> m v2
f) f (Term f v a)
fa
  Cycle Term f v a
r -> a -> Term f v2 a -> Term f v2 a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle a
a (Term f v2 a -> Term f v2 a) -> m (Term f v2 a) -> m (Term f v2 a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> m v2) -> Term f v a -> m (Term f v2 a)
forall (m :: * -> *) (f :: * -> *) v2 v a.
(Applicative m, Traversable f, Foldable f, Ord v2) =>
(v -> m v2) -> Term f v a -> m (Term f v2 a)
vmapM v -> m v2
f Term f v a
r
  Abs v
v Term f v a
body -> a -> v2 -> Term f v2 a -> Term f v2 a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs a
a (v2 -> Term f v2 a -> Term f v2 a)
-> m v2 -> m (Term f v2 a -> Term f v2 a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v -> m v2
f v
v m (Term f v2 a -> Term f v2 a)
-> m (Term f v2 a) -> m (Term f v2 a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (v -> m v2) -> Term f v a -> m (Term f v2 a)
forall (m :: * -> *) (f :: * -> *) v2 v a.
(Applicative m, Traversable f, Foldable f, Ord v2) =>
(v -> m v2) -> Term f v a -> m (Term f v2 a)
vmapM v -> m v2
f Term f v a
body

transform ::
  (Ord v, Foldable g, Functor g) =>
  (forall a. f a -> g a) ->
  Term f v a ->
  Term g v a
transform :: forall v (g :: * -> *) (f :: * -> *) a.
(Ord v, Foldable g, Functor g) =>
(forall a. f a -> g a) -> Term f v a -> Term g v a
transform forall a. f a -> g a
f Term f v a
t = case Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
t of
  Var v
v -> a -> v -> Term g v a
forall a v (f :: * -> *). a -> v -> Term f v a
var (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) v
v
  Abs v
v Term f v a
body -> a -> v -> Term g v a -> Term g v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) v
v ((forall a. f a -> g a) -> Term f v a -> Term g v a
forall v (g :: * -> *) (f :: * -> *) a.
(Ord v, Foldable g, Functor g) =>
(forall a. f a -> g a) -> Term f v a -> Term g v a
transform f a -> g a
forall a. f a -> g a
f Term f v a
body)
  Tm f (Term f v a)
subterms -> a -> g (Term g v a) -> Term g v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) ((Term f v a -> Term g v a) -> g (Term f v a) -> g (Term g v a)
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a. f a -> g a) -> Term f v a -> Term g v a
forall v (g :: * -> *) (f :: * -> *) a.
(Ord v, Foldable g, Functor g) =>
(forall a. f a -> g a) -> Term f v a -> Term g v a
transform f a -> g a
forall a. f a -> g a
f) (f (Term f v a) -> g (Term f v a)
forall a. f a -> g a
f f (Term f v a)
subterms))
  Cycle Term f v a
body -> a -> Term g v a -> Term g v a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) ((forall a. f a -> g a) -> Term f v a -> Term g v a
forall v (g :: * -> *) (f :: * -> *) a.
(Ord v, Foldable g, Functor g) =>
(forall a. f a -> g a) -> Term f v a -> Term g v a
transform f a -> g a
forall a. f a -> g a
f Term f v a
body)

transformM ::
  (Ord v, Monad m, Traversable g) =>
  (forall a. f a -> m (g a)) ->
  Term f v a ->
  m (Term g v a)
transformM :: forall v (m :: * -> *) (g :: * -> *) (f :: * -> *) a.
(Ord v, Monad m, Traversable g) =>
(forall a. f a -> m (g a)) -> Term f v a -> m (Term g v a)
transformM forall a. f a -> m (g a)
f Term f v a
t = case Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
t of
  Var v
v -> Term g v a -> m (Term g v a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term g v a -> m (Term g v a)) -> Term g v a -> m (Term g v a)
forall a b. (a -> b) -> a -> b
$ a -> v -> Term g v a
forall a v (f :: * -> *). a -> v -> Term f v a
var (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) v
v
  Abs v
v Term f v a
body -> a -> v -> Term g v a -> Term g v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) v
v (Term g v a -> Term g v a) -> m (Term g v a) -> m (Term g v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall a. f a -> m (g a)) -> Term f v a -> m (Term g v a)
forall v (m :: * -> *) (g :: * -> *) (f :: * -> *) a.
(Ord v, Monad m, Traversable g) =>
(forall a. f a -> m (g a)) -> Term f v a -> m (Term g v a)
transformM f a -> m (g a)
forall a. f a -> m (g a)
f Term f v a
body)
  Tm f (Term f v a)
subterms -> a -> g (Term g v a) -> Term g v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) (g (Term g v a) -> Term g v a)
-> m (g (Term g v a)) -> m (Term g v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term f v a -> m (Term g v a))
-> g (Term f v a) -> m (g (Term g v a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> g a -> f (g b)
traverse ((forall a. f a -> m (g a)) -> Term f v a -> m (Term g v a)
forall v (m :: * -> *) (g :: * -> *) (f :: * -> *) a.
(Ord v, Monad m, Traversable g) =>
(forall a. f a -> m (g a)) -> Term f v a -> m (Term g v a)
transformM f a -> m (g a)
forall a. f a -> m (g a)
f) (g (Term f v a) -> m (g (Term g v a)))
-> m (g (Term f v a)) -> m (g (Term g v a))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (Term f v a) -> m (g (Term f v a))
forall a. f a -> m (g a)
f f (Term f v a)
subterms)
  Cycle Term f v a
body -> a -> Term g v a -> Term g v a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) (Term g v a -> Term g v a) -> m (Term g v a) -> m (Term g v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall a. f a -> m (g a)) -> Term f v a -> m (Term g v a)
forall v (m :: * -> *) (g :: * -> *) (f :: * -> *) a.
(Ord v, Monad m, Traversable g) =>
(forall a. f a -> m (g a)) -> Term f v a -> m (Term g v a)
transformM f a -> m (g a)
forall a. f a -> m (g a)
f Term f v a
body)

abs :: (Ord v) => a -> v -> Term f v a -> Term f v a
abs :: forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs a
a v
v Term f v a
body = Set v -> a -> ABT f v (Term f v a) -> Term f v a
forall (f :: * -> *) v a.
Set v -> a -> ABT f v (Term f v a) -> Term f v a
Term (v -> Set v -> Set v
forall a. Ord a => a -> Set a -> Set a
Set.delete v
v (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
body)) a
a (v -> Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v r. v -> r -> ABT f v r
Abs v
v Term f v a
body)

var :: a -> v -> Term f v a
var :: forall a v (f :: * -> *). a -> v -> Term f v a
var a
a v
v = Set v -> a -> ABT f v (Term f v a) -> Term f v a
forall (f :: * -> *) v a.
Set v -> a -> ABT f v (Term f v a) -> Term f v a
Term (v -> Set v
forall a. a -> Set a
Set.singleton v
v) a
a (v -> ABT f v (Term f v a)
forall (f :: * -> *) v r. v -> ABT f v r
Var v
v)

cycle :: a -> Term f v a -> Term f v a
cycle :: forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle a
a Term f v a
t = Set v -> a -> ABT f v (Term f v a) -> Term f v a
forall (f :: * -> *) v a.
Set v -> a -> ABT f v (Term f v a) -> Term f v a
Term (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
t) a
a (Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v r. r -> ABT f v r
Cycle Term f v a
t)

tm :: (Foldable f, Ord v) => a -> f (Term f v a) -> Term f v a
tm :: forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm a
a f (Term f v a)
t = Set v -> a -> ABT f v (Term f v a) -> Term f v a
forall (f :: * -> *) v a.
Set v -> a -> ABT f v (Term f v a) -> Term f v a
Term ([Set v] -> Set v
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((Term f v a -> Set v) -> [Term f v a] -> [Set v]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars (f (Term f v a) -> [Term f v a]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList f (Term f v a)
t))) a
a (f (Term f v a) -> ABT f v (Term f v a)
forall (f :: * -> *) v r. f r -> ABT f v r
Tm f (Term f v a)
t)

-- * Traversals

-- | `visit f t` applies an effectful function to each subtree of
-- `t` and sequences the results. When `f` returns `Nothing`, `visit`
-- descends into the children of the current subtree. When `f` returns
-- `Just t2`, `visit` replaces the current subtree with `t2`. Thus:
-- `visit (const Nothing) t == pure t` and
-- `visit (const (Just (pure t2))) t == pure t2`
visit ::
  (Traversable f, Applicative g, Ord v) =>
  (Term f v a -> Maybe (g (Term f v a))) ->
  Term f v a ->
  g (Term f v a)
visit :: forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
visit Term f v a -> Maybe (g (Term f v a))
f Term f v a
t = (g (Term f v a) -> Maybe (g (Term f v a)) -> g (Term f v a))
-> Maybe (g (Term f v a)) -> g (Term f v a) -> g (Term f v a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip g (Term f v a) -> Maybe (g (Term f v a)) -> g (Term f v a)
forall a. a -> Maybe a -> a
fromMaybe (Term f v a -> Maybe (g (Term f v a))
f Term f v a
t) (g (Term f v a) -> g (Term f v a))
-> g (Term f v a) -> g (Term f v a)
forall a b. (a -> b) -> a -> b
$ case Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
t of
  Var v
_ -> Term f v a -> g (Term f v a)
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term f v a
t
  Cycle Term f v a
body -> a -> Term f v a -> Term f v a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) (Term f v a -> Term f v a) -> g (Term f v a) -> g (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
visit Term f v a -> Maybe (g (Term f v a))
f Term f v a
body
  Abs v
x Term f v a
e -> a -> v -> Term f v a -> Term f v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) v
x (Term f v a -> Term f v a) -> g (Term f v a) -> g (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
visit Term f v a -> Maybe (g (Term f v a))
f Term f v a
e
  Tm f (Term f v a)
body -> a -> f (Term f v a) -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) (f (Term f v a) -> Term f v a)
-> g (f (Term f v a)) -> g (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term f v a -> g (Term f v a))
-> f (Term f v a) -> g (f (Term f v a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
visit Term f v a -> Maybe (g (Term f v a))
f) f (Term f v a)
body

-- | Apply an effectful function to an ABT tree top down, sequencing the results.
visit' ::
  (Traversable f, Monad g, Ord v) =>
  (f (Term f v a) -> g (f (Term f v a))) ->
  Term f v a ->
  g (Term f v a)
visit' :: forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Monad g, Ord v) =>
(f (Term f v a) -> g (f (Term f v a)))
-> Term f v a -> g (Term f v a)
visit' f (Term f v a) -> g (f (Term f v a))
f Term f v a
t = case Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
t of
  Var v
_ -> Term f v a -> g (Term f v a)
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term f v a
t
  Cycle Term f v a
body -> a -> Term f v a -> Term f v a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) (Term f v a -> Term f v a) -> g (Term f v a) -> g (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (f (Term f v a) -> g (f (Term f v a)))
-> Term f v a -> g (Term f v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Monad g, Ord v) =>
(f (Term f v a) -> g (f (Term f v a)))
-> Term f v a -> g (Term f v a)
visit' f (Term f v a) -> g (f (Term f v a))
f Term f v a
body
  Abs v
x Term f v a
e -> a -> v -> Term f v a -> Term f v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) v
x (Term f v a -> Term f v a) -> g (Term f v a) -> g (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (f (Term f v a) -> g (f (Term f v a)))
-> Term f v a -> g (Term f v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Monad g, Ord v) =>
(f (Term f v a) -> g (f (Term f v a)))
-> Term f v a -> g (Term f v a)
visit' f (Term f v a) -> g (f (Term f v a))
f Term f v a
e
  Tm f (Term f v a)
body -> f (Term f v a) -> g (f (Term f v a))
f f (Term f v a)
body g (f (Term f v a))
-> (f (Term f v a) -> g (Term f v a)) -> g (Term f v a)
forall a b. g a -> (a -> g b) -> g b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((f (Term f v a) -> Term f v a)
-> g (f (Term f v a)) -> g (Term f v a)
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> f (Term f v a) -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t)) (g (f (Term f v a)) -> g (Term f v a))
-> (f (Term f v a) -> g (f (Term f v a)))
-> f (Term f v a)
-> g (Term f v a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term f v a -> g (Term f v a))
-> f (Term f v a) -> g (f (Term f v a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((f (Term f v a) -> g (f (Term f v a)))
-> Term f v a -> g (Term f v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Monad g, Ord v) =>
(f (Term f v a) -> g (f (Term f v a)))
-> Term f v a -> g (Term f v a)
visit' f (Term f v a) -> g (f (Term f v a))
f))

-- | Apply an effectful function to an ABT tree top down, sequencing the results.
visit_ ::
  (Traversable f, Applicative g, Ord v) =>
  (f (Term f v a) -> g ()) ->
  Term f v a ->
  g (Term f v a)
visit_ :: forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(f (Term f v a) -> g ()) -> Term f v a -> g (Term f v a)
visit_ f (Term f v a) -> g ()
f Term f v a
t = case Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
t of
  Var v
_ -> Term f v a -> g (Term f v a)
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term f v a
t
  Cycle Term f v a
body -> a -> Term f v a -> Term f v a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) (Term f v a -> Term f v a) -> g (Term f v a) -> g (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (f (Term f v a) -> g ()) -> Term f v a -> g (Term f v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(f (Term f v a) -> g ()) -> Term f v a -> g (Term f v a)
visit_ f (Term f v a) -> g ()
f Term f v a
body
  Abs v
x Term f v a
e -> a -> v -> Term f v a -> Term f v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) v
x (Term f v a -> Term f v a) -> g (Term f v a) -> g (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (f (Term f v a) -> g ()) -> Term f v a -> g (Term f v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(f (Term f v a) -> g ()) -> Term f v a -> g (Term f v a)
visit_ f (Term f v a) -> g ()
f Term f v a
e
  Tm f (Term f v a)
body -> f (Term f v a) -> g ()
f f (Term f v a)
body g () -> g (Term f v a) -> g (Term f v a)
forall a b. g a -> g b -> g b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (a -> f (Term f v a) -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) (f (Term f v a) -> Term f v a)
-> g (f (Term f v a)) -> g (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term f v a -> g (Term f v a))
-> f (Term f v a) -> g (f (Term f v a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((f (Term f v a) -> g ()) -> Term f v a -> g (Term f v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(f (Term f v a) -> g ()) -> Term f v a -> g (Term f v a)
visit_ f (Term f v a) -> g ()
f) f (Term f v a)
body)

-- | `visit` specialized to the `Identity` effect.
visitPure ::
  (Traversable f, Ord v) =>
  (Term f v a -> Maybe (Term f v a)) ->
  Term f v a ->
  Term f v a
visitPure :: forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
visitPure Term f v a -> Maybe (Term f v a)
f = Identity (Term f v a) -> Term f v a
forall a. Identity a -> a
runIdentity (Identity (Term f v a) -> Term f v a)
-> (Term f v a -> Identity (Term f v a))
-> Term f v a
-> Term f v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term f v a -> Maybe (Identity (Term f v a)))
-> Term f v a -> Identity (Term f v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
visit ((Term f v a -> Identity (Term f v a))
-> Maybe (Term f v a) -> Maybe (Identity (Term f v a))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term f v a -> Identity (Term f v a)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term f v a) -> Maybe (Identity (Term f v a)))
-> (Term f v a -> Maybe (Term f v a))
-> Term f v a
-> Maybe (Identity (Term f v a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f v a -> Maybe (Term f v a)
f)

foreachSubterm ::
  (Traversable f, Applicative g) =>
  (Term f v a -> g b) ->
  Term f v a ->
  g [b]
foreachSubterm :: forall (f :: * -> *) (g :: * -> *) v a b.
(Traversable f, Applicative g) =>
(Term f v a -> g b) -> Term f v a -> g [b]
foreachSubterm Term f v a -> g b
f Term f v a
e = case Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
e of
  Var v
_ -> b -> [b]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> [b]) -> g b -> g [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f v a -> g b
f Term f v a
e
  Cycle Term f v a
body -> (:) (b -> [b] -> [b]) -> g b -> g ([b] -> [b])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f v a -> g b
f Term f v a
e g ([b] -> [b]) -> g [b] -> g [b]
forall a b. g (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term f v a -> g b) -> Term f v a -> g [b]
forall (f :: * -> *) (g :: * -> *) v a b.
(Traversable f, Applicative g) =>
(Term f v a -> g b) -> Term f v a -> g [b]
foreachSubterm Term f v a -> g b
f Term f v a
body
  Abs v
_ Term f v a
body -> (:) (b -> [b] -> [b]) -> g b -> g ([b] -> [b])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f v a -> g b
f Term f v a
e g ([b] -> [b]) -> g [b] -> g [b]
forall a b. g (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term f v a -> g b) -> Term f v a -> g [b]
forall (f :: * -> *) (g :: * -> *) v a b.
(Traversable f, Applicative g) =>
(Term f v a -> g b) -> Term f v a -> g [b]
foreachSubterm Term f v a -> g b
f Term f v a
body
  Tm f (Term f v a)
body ->
    (:)
      (b -> [b] -> [b]) -> g b -> g ([b] -> [b])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f v a -> g b
f Term f v a
e
      g ([b] -> [b]) -> g [b] -> g [b]
forall a b. g (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([[b]] -> [b]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ([[b]] -> [b]) -> (f [b] -> [[b]]) -> f [b] -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f [b] -> [[b]]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList (f [b] -> [b]) -> g (f [b]) -> g [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term f v a -> g [b]) -> f (Term f v a) -> g (f [b])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((Term f v a -> g b) -> Term f v a -> g [b]
forall (f :: * -> *) (g :: * -> *) v a b.
(Traversable f, Applicative g) =>
(Term f v a -> g b) -> Term f v a -> g [b]
foreachSubterm Term f v a -> g b
f) f (Term f v a)
body)

subterms :: (Ord v, Traversable f) => Term f v a -> [Term f v a]
subterms :: forall v (f :: * -> *) a.
(Ord v, Traversable f) =>
Term f v a -> [Term f v a]
subterms Term f v a
t = Identity [Term f v a] -> [Term f v a]
forall a. Identity a -> a
runIdentity (Identity [Term f v a] -> [Term f v a])
-> Identity [Term f v a] -> [Term f v a]
forall a b. (a -> b) -> a -> b
$ (Term f v a -> Identity (Term f v a))
-> Term f v a -> Identity [Term f v a]
forall (f :: * -> *) (g :: * -> *) v a b.
(Traversable f, Applicative g) =>
(Term f v a -> g b) -> Term f v a -> g [b]
foreachSubterm Term f v a -> Identity (Term f v a)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term f v a
t

-- * Patterns

pattern Var' :: v -> Term f v a
pattern $mVar' :: forall {r} {v} {f :: * -> *} {a}.
Term f v a -> (v -> r) -> ((# #) -> r) -> r
Var' v <- Term _ _ (Var v)

pattern Cycle' :: [v] -> Term f v a -> Term f v a
pattern $mCycle' :: forall {r} {v} {f :: * -> *} {a}.
Term f v a -> ([v] -> Term f v a -> r) -> ((# #) -> r) -> r
Cycle' vs t <- Term _ _ (Cycle (AbsN' vs t))

pattern AbsN' :: [v] -> Term f v a -> Term f v a
pattern $mAbsN' :: forall {r} {v} {f :: * -> *} {a}.
Term f v a -> ([v] -> Term f v a -> r) -> ((# #) -> r) -> r
AbsN' vs body <- (unabs -> (vs, body))

{-# COMPLETE AbsN' #-}

pattern Tm' :: f (Term f v a) -> Term f v a
pattern $mTm' :: forall {r} {f :: * -> *} {v} {a}.
Term f v a -> (f (Term f v a) -> r) -> ((# #) -> r) -> r
Tm' f <- Term _ _ (Tm f)

unabs :: Term f v a -> ([v], Term f v a)
unabs :: forall (f :: * -> *) v a. Term f v a -> ([v], Term f v a)
unabs (Term Set v
_ a
_ (Abs v
hd Term f v a
body)) =
  let ([v]
tl, Term f v a
body') = Term f v a -> ([v], Term f v a)
forall (f :: * -> *) v a. Term f v a -> ([v], Term f v a)
unabs Term f v a
body in (v
hd v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
tl, Term f v a
body')
unabs Term f v a
t = ([], Term f v a
t)

-- | Produce a variable which is free in both terms
freshInBoth :: (Var v) => Term f v a -> Term f v a -> v -> v
freshInBoth :: forall v (f :: * -> *) a.
Var v =>
Term f v a -> Term f v a -> v -> v
freshInBoth Term f v a
t1 Term f v a
t2 = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn (Set v -> v -> v) -> Set v -> v -> v
forall a b. (a -> b) -> a -> b
$ Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
t1) (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
t2)

substsInheritAnnotation ::
  (Foldable f, Functor f, Var v) =>
  [(v, Term f v b)] ->
  Term f v a ->
  Term f v a
substsInheritAnnotation :: forall (f :: * -> *) v b a.
(Foldable f, Functor f, Var v) =>
[(v, Term f v b)] -> Term f v a -> Term f v a
substsInheritAnnotation [(v, Term f v b)]
replacements Term f v a
body =
  ((v, Term f v b) -> Term f v a -> Term f v a)
-> Term f v a -> [(v, Term f v b)] -> Term f v a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((v -> Term f v b -> Term f v a -> Term f v a)
-> (v, Term f v b) -> Term f v a -> Term f v a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry v -> Term f v b -> Term f v a -> Term f v a
forall (f :: * -> *) v b a.
(Foldable f, Functor f, Var v) =>
v -> Term f v b -> Term f v a -> Term f v a
substInheritAnnotation) Term f v a
body ([(v, Term f v b)] -> [(v, Term f v b)]
forall a. [a] -> [a]
reverse [(v, Term f v b)]
replacements)

-- Like `subst`, but the annotation of the replacement is inherited from
-- the previous annotation at each replacement point.
substInheritAnnotation ::
  (Foldable f, Functor f, Var v) =>
  v ->
  Term f v b ->
  Term f v a ->
  Term f v a
substInheritAnnotation :: forall (f :: * -> *) v b a.
(Foldable f, Functor f, Var v) =>
v -> Term f v b -> Term f v a -> Term f v a
substInheritAnnotation v
v Term f v b
r =
  (a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
(a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
subst' (\a
ann -> a -> b -> a
forall a b. a -> b -> a
const a
ann (b -> a) -> Term f v b -> Term f v a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f v b
r) v
v (Term f v b -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v b
r)

-- Slightly generalized version of `subst`, the replacement action is handled
-- by the function `replace`, which is given the annotation `a` at the point
-- of replacement. `r` should be the set of free variables contained in the
-- term returned by `replace`. See `substInheritAnnotation` for an example usage.
subst' :: (Foldable f, Functor f, Var v) => (a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
subst' :: forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
(a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
subst' a -> Term f v a
replace v
v Set v
r t2 :: Term f v a
t2@(Term Set v
fvs a
ann ABT f v (Term f v a)
body)
  | v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember v
v Set v
fvs = Term f v a
t2 -- subtrees not containing the var can be skipped
  | Bool
otherwise = case ABT f v (Term f v a)
body of
      Var v
v'
        | v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v' -> a -> Term f v a
replace a
ann -- var match; perform replacement
        | Bool
otherwise -> Term f v a
t2 -- var did not match one being substituted; ignore
      Cycle Term f v a
body -> a -> Term f v a -> Term f v a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle a
ann ((a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
(a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
subst' a -> Term f v a
replace v
v Set v
r Term f v a
body)
      Abs v
x Term f v a
_ | v
x v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v -> Term f v a
t2 -- x shadows v; ignore subtree
      Abs v
x Term f v a
e -> a -> v -> Term f v a -> Term f v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs a
ann v
x' Term f v a
e'
        where
          x' :: v
x' = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn (Set v
fvs Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set v
r) v
x
          -- rename x to something that cannot be captured by `r`
          e' :: Term f v a
e' =
            if v
x v -> v -> Bool
forall a. Eq a => a -> a -> Bool
/= v
x'
              then (a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
(a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
subst' a -> Term f v a
replace v
v Set v
r (v -> v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
x v
x' Term f v a
e)
              else (a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
(a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
subst' a -> Term f v a
replace v
v Set v
r Term f v a
e
      Tm f (Term f v a)
body -> a -> f (Term f v a) -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm a
ann ((Term f v a -> Term f v a) -> f (Term f v a) -> f (Term f v a)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
(a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
subst' a -> Term f v a
replace v
v Set v
r) f (Term f v a)
body)

-- | renames `old` to `new` in the given term, ignoring subtrees that bind `old`
rename :: (Foldable f, Functor f, Var v) => v -> v -> Term f v a -> Term f v a
rename :: forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
old v
new t0 :: Term f v a
t0@(Term Set v
fvs a
ann ABT f v (Term f v a)
t) =
  if v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember v
old Set v
fvs
    then Term f v a
t0
    else case ABT f v (Term f v a)
t of
      Var v
v -> if v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
old then a -> v -> Term f v a
forall a v (f :: * -> *). a -> v -> Term f v a
var a
ann v
new else Term f v a
t0
      Cycle Term f v a
body -> a -> Term f v a -> Term f v a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle a
ann (v -> v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
old v
new Term f v a
body)
      Abs v
v Term f v a
body ->
        -- v shadows old, so skip this subtree
        if v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
old
          then a -> v -> Term f v a -> Term f v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs a
ann v
v Term f v a
body
          else -- the rename would capture new, freshen this Abs
          -- to make that no longer true, then proceed with
          -- renaming `old` to `new`

            if v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
new
              then
                let v' :: v
v' = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn ([v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList [v
new, v
old] Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
body) v
v
                 in a -> v -> Term f v a -> Term f v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs a
ann v
v' (v -> v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
old v
new (v -> v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
v v
v' Term f v a
body))
              else -- nothing special, just rename inside body of Abs
                a -> v -> Term f v a -> Term f v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs a
ann v
v (v -> v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
old v
new Term f v a
body)
      Tm f (Term f v a)
v -> a -> f (Term f v a) -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm a
ann ((Term f v a -> Term f v a) -> f (Term f v a) -> f (Term f v a)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> v -> Term f v a -> Term f v a
rename v
old v
new) f (Term f v a)
v)

allVars :: (Foldable f) => Term f v a -> [v]
allVars :: forall (f :: * -> *) v a. Foldable f => Term f v a -> [v]
allVars Term f v a
t = case Term f v a -> ABT f v (Term f v a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f v a
t of
  Var v
v -> [v
v]
  Cycle Term f v a
body -> Term f v a -> [v]
forall (f :: * -> *) v a. Foldable f => Term f v a -> [v]
allVars Term f v a
body
  Abs v
v Term f v a
body -> v
v v -> [v] -> [v]
forall a. a -> [a] -> [a]
: Term f v a -> [v]
forall (f :: * -> *) v a. Foldable f => Term f v a -> [v]
allVars Term f v a
body
  Tm f (Term f v a)
v -> f (Term f v a) -> [Term f v a]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList f (Term f v a)
v [Term f v a] -> (Term f v a -> [v]) -> [v]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term f v a -> [v]
forall (f :: * -> *) v a. Foldable f => Term f v a -> [v]
allVars

-- | Freshens the given variable wrt. the set of used variables
-- tracked by state. Adds the result to the set of used variables.
freshenS :: (Var v, MonadState (Set v) m) => v -> m v
freshenS :: forall v (m :: * -> *). (Var v, MonadState (Set v) m) => v -> m v
freshenS = Lens' (Set v) (Set v) -> v -> m v
forall v s (m :: * -> *).
(Var v, MonadState s m) =>
Lens' s (Set v) -> v -> m v
freshenS' (Set v -> f (Set v)) -> Set v -> f (Set v)
forall a. a -> a
Lens' (Set v) (Set v)
id

-- | A more general version of `freshenS` that uses a lens
-- to focus on used variables inside state.
freshenS' :: (Var v, MonadState s m) => Lens' s (Set v) -> v -> m v
freshenS' :: forall v s (m :: * -> *).
(Var v, MonadState s m) =>
Lens' s (Set v) -> v -> m v
freshenS' Lens' s (Set v)
uvLens v
v = do
  Set v
usedVars <- Getting (Set v) s (Set v) -> m (Set v)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (Set v) s (Set v)
Lens' s (Set v)
uvLens
  let v' :: v
v' = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn Set v
usedVars v
v
  (Set v -> Identity (Set v)) -> s -> Identity s
Lens' s (Set v)
uvLens ((Set v -> Identity (Set v)) -> s -> Identity s) -> Set v -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= v -> Set v -> Set v
forall a. Ord a => a -> Set a -> Set a
Set.insert v
v' Set v
usedVars
  pure v
v'