-- 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.Map qualified as Map
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)

-- | Substitutes the replacements in order, with `substInheritAnnotation`'s
-- semantics for each: the result is what substituting them one at a time,
-- first to last, gives. So a variable free in a replacement is replaced by
-- the substitutions after it in the list, and of two replacements for the
-- same variable the first takes the term's occurrences and the second
-- reaches only the occurrences inside the first's replacement. The term is
-- traversed once, not once per replacement: with thousands of replacements,
-- as when the names of a wide expression are bound, one traversal per
-- replacement rebuilt the path to each occurrence (and its free-variable
-- sets) thousands of times over.
--
-- The one-at-a-time result is reproduced up to the names of binders: a
-- binder is renamed when it could capture a variable free in any
-- replacement, where the one-at-a-time form renames it only for the
-- replacements that reach its body, and the fresh name need not be the
-- same. The two results are alpha-equivalent.
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 =
  Map v (Term f v b) -> Term f v a -> Term f v a
forall (f :: * -> *) v a b.
(Foldable f, Functor f, Var v) =>
Map v (Term f v b) -> Term f v a -> Term f v a
substsMapInheritAnnotation (((v, Term f v b) -> Map v (Term f v b) -> Map v (Term f v b))
-> Map v (Term f v b) -> [(v, Term f v b)] -> Map v (Term f v b)
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) -> Map v (Term f v b) -> Map v (Term f v b)
forall {k} {f :: * -> *} {a}.
(Foldable f, Functor f, Var k) =>
(k, Term f k a) -> Map k (Term f k a) -> Map k (Term f k a)
compose Map v (Term f v b)
forall k a. Map k a
Map.empty [(v, Term f v b)]
replacements) Term f v a
body
  where
    -- The simultaneous substitution that equals substituting `(v, r)` and
    -- then the (already composed) substitutions after it.
    compose :: (k, Term f k a) -> Map k (Term f k a) -> Map k (Term f k a)
compose (k
v, Term f k a
r) Map k (Term f k a)
later = k -> Term f k a -> Map k (Term f k a) -> Map k (Term f k a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
v (Map k (Term f k a) -> Term f k a -> Term f k a
forall (f :: * -> *) v a b.
(Foldable f, Functor f, Var v) =>
Map v (Term f v b) -> Term f v a -> Term f v a
substsMapInheritAnnotation Map k (Term f k a)
later Term f k a
r) Map k (Term f k a)
later

-- | Substitutes every variable in the map at once, avoiding capture; the
-- annotation of each replacement is inherited from the variable it replaces.
-- This is `subst'` with a map of variables in place of its one variable: the
-- key set in place of `v`, and the free variables of all the replacements in
-- place of `r`. The key set travels with the map because every node tests
-- its free variables against it, and `Map.keysSet` is linear.
substsMapInheritAnnotation ::
  forall f v a b.
  (Foldable f, Functor f, Var v) =>
  Map v (Term f v b) ->
  Term f v a ->
  Term f v a
substsMapInheritAnnotation :: forall (f :: * -> *) v a b.
(Foldable f, Functor f, Var v) =>
Map v (Term f v b) -> Term f v a -> Term f v a
substsMapInheritAnnotation Map v (Term f v b)
m0 = Map v (Term f v b) -> Set v -> Term f v a -> Term f v a
go Map v (Term f v b)
m0 (Map v (Term f v b) -> Set v
forall k a. Map k a -> Set k
Map.keysSet Map v (Term f v b)
m0)
  where
    -- the variables a replacement can bring in, which a binder must not capture
    r :: Set v
r = (Term f v b -> Set v) -> Map v (Term f v b) -> Set v
forall m a. Monoid m => (a -> m) -> Map v a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term f v b -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Map v (Term f v b)
m0
    go :: Map v (Term f v b) -> Set v -> Term f v a -> Term f v a
    go :: Map v (Term f v b) -> Set v -> Term f v a -> Term f v a
go Map v (Term f v b)
m Set v
keys t :: Term f v a
t@(Term Set v
fvs a
ann ABT f v (Term f v a)
body)
      -- subtrees containing none of the vars can be skipped. The term's
      -- free variables come first: a term with none decides this without
      -- forcing the keys, so composing a closed replacement into a map of
      -- thousands costs nothing.
      | Set v -> Set v -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set v
fvs Set v
keys = Term f v a
t
      | Bool
otherwise = case ABT f v (Term f v a)
body of
          Var v
v -> Term f v a
-> (Term f v b -> Term f v a) -> Maybe (Term f v b) -> Term f v a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Term f v a
t ((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 :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> b -> a
forall a b. a -> b -> a
const a
ann)) (v -> Map v (Term f v b) -> Maybe (Term f v b)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v (Term f v b)
m) -- var match; perform replacement
          Cycle Term f v a
e -> 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 (Map v (Term f v b) -> Set v -> Term f v a -> Term f v a
go Map v (Term f v b)
m Set v
keys Term f v a
e)
          Abs v
x Term f v a
e
            | Set v -> Set v -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
e) Set v
keys' -> Term f v a
t -- x shadows every var reaching here; ignore subtree
            | v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
x Set v
r -> 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' (Map v (Term f v b) -> Set v -> Term f v a -> Term f v a
go Map v (Term f v b)
m' Set v
keys' (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)) -- x would capture; rename it
            | Bool
otherwise -> 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 (Map v (Term f v b) -> Set v -> Term f v a -> Term f v a
go Map v (Term f v b)
m' Set v
keys' Term f v a
e)
            where
              (Map v (Term f v b)
m', Set v
keys') = (v -> Map v (Term f v b) -> Map v (Term f v b)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete v
x Map v (Term f v b)
m, v -> Set v -> Set v
forall a. Ord a => a -> Set a -> Set a
Set.delete v
x Set v
keys) -- x shadows x, if it was a key
              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
          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 (Map v (Term f v b) -> Set v -> Term f v a -> Term f v a
go Map v (Term f v b)
m Set v
keys) f (Term f v a)
body)

-- 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'