{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

-- | Based on: http://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html
module Unison.ABT
  ( -- * Types
    ABT (..),
    Term (..),
    Term' (..),
    Var (..),
    V (..),
    Subst (..),

    -- * Combinators & Traversals
    fresh,
    unvar,
    freshenS,
    freshInBoth,
    freshenBothWrt,
    freshenWrt,
    visit,
    visit',
    visit_,
    visitPure,
    changeVars,
    allVars,
    numberedFreeVars,
    subterms,
    annotateBound,
    rebuildUp,
    rebuildMaybeUp,
    rebuildUp',
    reannotateUp,
    rewriteDown,
    transform,
    transformM,
    foreachSubterm,
    freeVarOccurrences,
    isFreeIn,
    occurrences,
    extraMap,
    vmap,
    vmapM,
    amap,
    rename,
    renames,
    subst,
    substs,
    substInheritAnnotation,
    substsInheritAnnotation,
    find,
    find',
    FindAction (..),
    containsExpression,
    rewriteExpression,

    -- * Optics
    baseFunctor_,
    rewriteDown_,

    -- * Safe Term constructors & Patterns
    annotate,
    annotatedVar,
    var,
    tm,
    tm',
    abs,
    absChain,
    absChain',
    abs',
    absr,
    unabs,
    unabsA,
    dropAbs,
    cycle,
    cycle',
    cycler,
    pattern Abs',
    pattern Abs'',
    pattern AbsN',
    pattern AbsNA',
    pattern Var',
    pattern Cycle',
    pattern Cycle'',
    pattern CycleA',
    pattern Tm',

    -- * Algorithms
    components,
    orderedComponents,
  )
where

import Control.Lens (Lens', lens, (%%~))
import Control.Monad.State (MonadState, evalState, get, put, runState)
import Data.Foldable qualified as Foldable
import Data.List hiding (cycle, find)
import Data.Map qualified as Map
import Data.Set qualified as Set
import U.Core.ABT
  ( ABT (..),
    Term (..),
    Term' (..),
    allVars,
    foreachSubterm,
    freshInBoth,
    freshenS,
    rename,
    subst',
    substInheritAnnotation,
    substsInheritAnnotation,
    subterms,
    transform,
    transformM,
    unabs,
    visit,
    visit',
    visitPure,
    visit_,
    vmap,
    vmapM,
    pattern AbsN',
    pattern Tm',
    pattern Var',
  )
import U.Core.ABT qualified
import U.Core.ABT.Var (Var (freshIn))
import Unison.Prelude
import Unison.Util.Components qualified as Components
import Prelude hiding (abs, cycle)

abt_ :: Lens' (Term f v a) (ABT f v (Term f v a))
abt_ :: forall (f :: * -> *) v a (f :: * -> *).
Functor f =>
(ABT f v (Term f v a) -> f (ABT f v (Term f v a)))
-> Term f v a -> f (Term f v a)
abt_ = (Term f v a -> ABT f v (Term f v a))
-> (Term f v a -> ABT f v (Term f v a) -> Term f v a)
-> Lens
     (Term f v a)
     (Term f v a)
     (ABT f v (Term f v a))
     (ABT f v (Term f v a))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens 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 -> ABT f v (Term f v a) -> Term f v a
forall {f :: * -> *} {v} {a} {f :: * -> *}.
Term f v a -> ABT f v (Term f v a) -> Term f v a
setter
  where
    setter :: Term f v a -> ABT f v (Term f v a) -> Term f v a
setter (Term Set v
fv a
a ABT f v (Term f v 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
fv a
a ABT f v (Term f v a)
abt

-- a.k.a. baseFunctor_ :: Traversal' (Term f v a) (f _)
baseFunctor_ ::
  (Applicative m) =>
  (f (Term f v a) -> m (f (Term f v a))) ->
  Term f v a ->
  m (Term f v a)
baseFunctor_ :: forall (m :: * -> *) (f :: * -> *) v a.
Applicative m =>
(f (Term f v a) -> m (f (Term f v a)))
-> Term f v a -> m (Term f v a)
baseFunctor_ f (Term f v a) -> m (f (Term f v a))
f Term f v a
t =
  Term f v a
t
    Term f v a -> (Term f v a -> m (Term f v a)) -> m (Term f v a)
forall a b. a -> (a -> b) -> b
& (ABT f v (Term f v a) -> m (ABT f v (Term f v a)))
-> Term f v a -> m (Term f v a)
forall (f :: * -> *) v a (f :: * -> *).
Functor f =>
(ABT f v (Term f v a) -> f (ABT f v (Term f v a)))
-> Term f v a -> f (Term f v a)
abt_ ((ABT f v (Term f v a) -> m (ABT f v (Term f v a)))
 -> Term f v a -> m (Term f v a))
-> (ABT f v (Term f v a) -> m (ABT f v (Term f v a)))
-> Term f v a
-> m (Term f v a)
forall {k} (f :: k -> *) s (t :: k) a (b :: k).
LensLike f s t a b -> LensLike f s t a b
%%~ \case
      Tm f (Term f v a)
fx -> 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) -> ABT f v (Term f v a))
-> m (f (Term f v a)) -> m (ABT f v (Term f v a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Term f v a) -> m (f (Term f v a))
f (f (Term f v a)
fx)
      ABT f v (Term f v a)
x -> ABT f v (Term f v a) -> m (ABT f v (Term f v a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ABT f v (Term f v a)
x

-- deriving instance (Data a, Data v, Typeable f, Data (f (Term f v a)), Ord v) => Data (Term f v a)

data V v = Free v | Bound v deriving (V v -> V v -> Bool
(V v -> V v -> Bool) -> (V v -> V v -> Bool) -> Eq (V v)
forall v. Eq v => V v -> V v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v. Eq v => V v -> V v -> Bool
== :: V v -> V v -> Bool
$c/= :: forall v. Eq v => V v -> V v -> Bool
/= :: V v -> V v -> Bool
Eq, Eq (V v)
Eq (V v) =>
(V v -> V v -> Ordering)
-> (V v -> V v -> Bool)
-> (V v -> V v -> Bool)
-> (V v -> V v -> Bool)
-> (V v -> V v -> Bool)
-> (V v -> V v -> V v)
-> (V v -> V v -> V v)
-> Ord (V v)
V v -> V v -> Bool
V v -> V v -> Ordering
V v -> V v -> V v
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v. Ord v => Eq (V v)
forall v. Ord v => V v -> V v -> Bool
forall v. Ord v => V v -> V v -> Ordering
forall v. Ord v => V v -> V v -> V v
$ccompare :: forall v. Ord v => V v -> V v -> Ordering
compare :: V v -> V v -> Ordering
$c< :: forall v. Ord v => V v -> V v -> Bool
< :: V v -> V v -> Bool
$c<= :: forall v. Ord v => V v -> V v -> Bool
<= :: V v -> V v -> Bool
$c> :: forall v. Ord v => V v -> V v -> Bool
> :: V v -> V v -> Bool
$c>= :: forall v. Ord v => V v -> V v -> Bool
>= :: V v -> V v -> Bool
$cmax :: forall v. Ord v => V v -> V v -> V v
max :: V v -> V v -> V v
$cmin :: forall v. Ord v => V v -> V v -> V v
min :: V v -> V v -> V v
Ord, Int -> V v -> ShowS
[V v] -> ShowS
V v -> String
(Int -> V v -> ShowS)
-> (V v -> String) -> ([V v] -> ShowS) -> Show (V v)
forall v. Show v => Int -> V v -> ShowS
forall v. Show v => [V v] -> ShowS
forall v. Show v => V v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> V v -> ShowS
showsPrec :: Int -> V v -> ShowS
$cshow :: forall v. Show v => V v -> String
show :: V v -> String
$cshowList :: forall v. Show v => [V v] -> ShowS
showList :: [V v] -> ShowS
Show, (forall a b. (a -> b) -> V a -> V b)
-> (forall a b. a -> V b -> V a) -> Functor V
forall a b. a -> V b -> V a
forall a b. (a -> b) -> V a -> V b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> V a -> V b
fmap :: forall a b. (a -> b) -> V a -> V b
$c<$ :: forall a b. a -> V b -> V a
<$ :: forall a b. a -> V b -> V a
Functor)

unvar :: V v -> v
unvar :: forall v. V v -> v
unvar (Free v
v) = v
v
unvar (Bound v
v) = v
v

instance (Var v) => Var (V v) where
  freshIn :: Set (V v) -> V v -> V v
freshIn Set (V v)
s V v
v = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn ((V v -> v) -> Set (V v) -> Set v
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map V v -> v
forall v. V v -> v
unvar Set (V v)
s) (v -> v) -> V v -> V v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> V v
v

wrap :: (Functor f, Foldable f, Var v) => v -> Term f (V v) a -> (V v, Term f (V v) a)
wrap :: forall (f :: * -> *) v a.
(Functor f, Foldable f, Var v) =>
v -> Term f (V v) a -> (V v, Term f (V v) a)
wrap v
v Term f (V v) a
t =
  if V v -> Set (V v) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (v -> V v
forall v. v -> V v
Free v
v) (Term f (V v) a -> Set (V v)
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f (V v) a
t)
    then let v' :: V v
v' = Term f (V v) a -> V v -> V v
forall v (f :: * -> *) a. Var v => Term f v a -> v -> v
fresh Term f (V v) a
t (v -> V v
forall v. v -> V v
Bound v
v) in (V v
v', V v -> V v -> Term f (V v) a -> Term f (V 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
forall v. v -> V v
Bound v
v) V v
v' Term f (V v) a
t)
    else (v -> V v
forall v. v -> V v
Bound v
v, Term f (V v) a
t)

wrap' ::
  (Functor f, Foldable f, Var v) =>
  v ->
  Term f (V v) a ->
  (V v -> Term f (V v) a -> c) ->
  c
wrap' :: forall (f :: * -> *) v a c.
(Functor f, Foldable f, Var v) =>
v -> Term f (V v) a -> (V v -> Term f (V v) a -> c) -> c
wrap' v
v Term f (V v) a
t V v -> Term f (V v) a -> c
f = (V v -> Term f (V v) a -> c) -> (V v, Term f (V v) a) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry V v -> Term f (V v) a -> c
f (v -> Term f (V v) a -> (V v, Term f (V v) a)
forall (f :: * -> *) v a.
(Functor f, Foldable f, Var v) =>
v -> Term f (V v) a -> (V v, Term f (V v) a)
wrap v
v Term f (V v) a
t)

-- Annotate the tree with the set of bound variables at each node.
annotateBound :: (Ord v, Foldable f, Functor f) => Term f v a -> Term f v (a, Set v)
annotateBound :: forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
Term f v a -> Term f v (a, Set v)
annotateBound = Set v -> Term f v a -> Term f v (a, Set v)
forall {a} {f :: * -> *} {a}.
(Ord a, Foldable f, Functor f) =>
Set a -> Term f a a -> Term f a (a, Set a)
go Set v
forall a. Set a
Set.empty
  where
    go :: Set a -> Term f a a -> Term f a (a, Set a)
go Set a
bound Term f a a
t =
      let a :: (a, Set a)
a = (Term f a a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f a a
t, Set a
bound)
       in case Term f a a -> ABT f a (Term f a a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term f a a
t of
            Var a
v -> (a, Set a) -> a -> Term f a (a, Set a)
forall a v (f :: * -> *). a -> v -> Term f v a
annotatedVar (a, Set a)
a a
v
            Cycle Term f a a
body -> (a, Set a) -> Term f a (a, Set a) -> Term f a (a, Set a)
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle' (a, Set a)
a (Set a -> Term f a a -> Term f a (a, Set a)
go Set a
bound Term f a a
body)
            Abs a
x Term f a a
body -> (a, Set a) -> a -> Term f a (a, Set a) -> Term f a (a, Set a)
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs' (a, Set a)
a a
x (Set a -> Term f a a -> Term f a (a, Set a)
go (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
x Set a
bound) Term f a a
body)
            Tm f (Term f a a)
body -> (a, Set a) -> f (Term f a (a, Set a)) -> Term f a (a, Set a)
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm' (a, Set a)
a (Set a -> Term f a a -> Term f a (a, Set a)
go Set a
bound (Term f a a -> Term f a (a, Set a))
-> f (Term f a a) -> f (Term f a (a, Set a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Term f a a)
body)

-- | `True` if `v` is a member of the set of free variables of `t`
isFreeIn :: (Ord v) => v -> Term f v a -> Bool
isFreeIn :: forall v (f :: * -> *) a. Ord v => v -> Term f v a -> Bool
isFreeIn v
v Term f v a
t = v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
v (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
t)

-- | Replace the annotation with the given argument.
annotate :: a -> Term f v a -> Term f v a
annotate :: forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
annotate a
a (Term Set v
fvs a
_ ABT f v (Term f v a)
out) = 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
fvs a
a ABT f v (Term f v a)
out

amap :: (Functor f, Foldable f, Ord v) => (a -> a2) -> Term f v a -> Term f v a2
amap :: forall (f :: * -> *) v a a2.
(Functor f, Foldable f, Ord v) =>
(a -> a2) -> Term f v a -> Term f v a2
amap = (Term f v a -> a -> a2) -> Term f v a -> Term f v a2
forall (f :: * -> *) v a a2.
(Functor f, Foldable f, Ord v) =>
(Term f v a -> a -> a2) -> Term f v a -> Term f v a2
amap' ((Term f v a -> a -> a2) -> Term f v a -> Term f v a2)
-> ((a -> a2) -> Term f v a -> a -> a2)
-> (a -> a2)
-> Term f v a
-> Term f v a2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a2) -> Term f v a -> a -> a2
forall a b. a -> b -> a
const

amap' :: (Functor f, Foldable f, Ord v) => (Term f v a -> a -> a2) -> Term f v a -> Term f v a2
amap' :: forall (f :: * -> *) v a a2.
(Functor f, Foldable f, Ord v) =>
(Term f v a -> a -> a2) -> Term f v a -> Term f v a2
amap' Term f v a -> a -> a2
f t :: Term f v a
t@(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 -> a2 -> v -> Term f v a2
forall a v (f :: * -> *). a -> v -> Term f v a
annotatedVar (Term f v a -> a -> a2
f Term f v a
t a
a) v
v
  Tm f (Term f v a)
fa -> a2 -> f (Term f v a2) -> Term f v a2
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm' (Term f v a -> a -> a2
f Term f v a
t a
a) ((Term f v a -> Term f v a2) -> f (Term f v a) -> f (Term f v a2)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term f v a -> a -> a2) -> Term f v a -> Term f v a2
forall (f :: * -> *) v a a2.
(Functor f, Foldable f, Ord v) =>
(Term f v a -> a -> a2) -> Term f v a -> Term f v a2
amap' Term f v a -> a -> a2
f) f (Term f v a)
fa)
  Cycle Term f v a
r -> a2 -> Term f v a2 -> Term f v a2
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle' (Term f v a -> a -> a2
f Term f v a
t a
a) ((Term f v a -> a -> a2) -> Term f v a -> Term f v a2
forall (f :: * -> *) v a a2.
(Functor f, Foldable f, Ord v) =>
(Term f v a -> a -> a2) -> Term f v a -> Term f v a2
amap' Term f v a -> a -> a2
f Term f v a
r)
  Abs v
v Term f v a
body -> a2 -> v -> Term f v a2 -> Term f v a2
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs' (Term f v a -> a -> a2
f Term f v a
t a
a) v
v ((Term f v a -> a -> a2) -> Term f v a -> Term f v a2
forall (f :: * -> *) v a a2.
(Functor f, Foldable f, Ord v) =>
(Term f v a -> a -> a2) -> Term f v a -> Term f v a2
amap' Term f v a -> a -> a2
f Term f v a
body)

extraMap :: (Functor g) => (forall k. f k -> g k) -> Term f v a -> Term g v a
extraMap :: forall (g :: * -> *) (f :: * -> *) v a.
Functor g =>
(forall k. f k -> g k) -> Term f v a -> Term g v a
extraMap forall k. f k -> g k
p (Term Set v
fvs a
a ABT f v (Term f v a)
sub) = Set v -> a -> ABT g v (Term g v a) -> Term g v a
forall (f :: * -> *) v a.
Set v -> a -> ABT f v (Term f v a) -> Term f v a
Term Set v
fvs a
a ((forall k. f k -> g k)
-> ABT f v (Term f v a) -> ABT g v (Term g v a)
forall (g :: * -> *) (f :: * -> *) v a.
Functor g =>
(forall k. f k -> g k)
-> ABT f v (Term f v a) -> ABT g v (Term g v a)
go f k -> g k
forall k. f k -> g k
p ABT f v (Term f v a)
sub)
  where
    go :: (Functor g) => (forall k. f k -> g k) -> ABT f v (Term f v a) -> ABT g v (Term g v a)
    go :: forall (g :: * -> *) (f :: * -> *) v a.
Functor g =>
(forall k. f k -> g k)
-> ABT f v (Term f v a) -> ABT g v (Term g v a)
go forall k. f k -> g k
p = \case
      Var v
v -> v -> ABT g v (Term g v a)
forall (f :: * -> *) v r. v -> ABT f v r
Var v
v
      Cycle Term f v a
r -> Term g v a -> ABT g v (Term g v a)
forall (f :: * -> *) v r. r -> ABT f v r
Cycle ((forall k. f k -> g k) -> Term f v a -> Term g v a
forall (g :: * -> *) (f :: * -> *) v a.
Functor g =>
(forall k. f k -> g k) -> Term f v a -> Term g v a
extraMap f k -> g k
forall k. f k -> g k
p Term f v a
r)
      Abs v
v Term f v a
r -> v -> Term g v a -> ABT g v (Term g v a)
forall (f :: * -> *) v r. v -> r -> ABT f v r
Abs v
v ((forall k. f k -> g k) -> Term f v a -> Term g v a
forall (g :: * -> *) (f :: * -> *) v a.
Functor g =>
(forall k. f k -> g k) -> Term f v a -> Term g v a
extraMap f k -> g k
forall k. f k -> g k
p Term f v a
r)
      Tm f (Term f v a)
x -> g (Term g v a) -> ABT g v (Term g v a)
forall (f :: * -> *) v r. f r -> ABT f v r
Tm ((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 k. f k -> g k) -> Term f v a -> Term g v a
forall (g :: * -> *) (f :: * -> *) v a.
Functor g =>
(forall k. f k -> g k) -> Term f v a -> Term g v a
extraMap f k -> g k
forall k. f k -> g k
p) (f (Term f v a) -> g (Term f v a)
forall k. f k -> g k
p f (Term f v a)
x))

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

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

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

pattern Abs' :: (Foldable f, Functor f, Var v) => Subst f v a -> Term f v a
pattern $mAbs' :: forall {r} {f :: * -> *} {v} {a}.
(Foldable f, Functor f, Var v) =>
Term f v a -> (Subst f v a -> r) -> ((# #) -> r) -> r
Abs' subst <- (unabs1 -> Just subst)

pattern CycleA' :: a -> [(a, v)] -> Term f v a -> Term f v a
pattern $mCycleA' :: forall {r} {a} {v} {f :: * -> *}.
Term f v a
-> (a -> [(a, v)] -> Term f v a -> r) -> ((# #) -> r) -> r
CycleA' a avs t <- Term _ a (Cycle (AbsNA' avs t))

pattern AbsNA' :: [(a, v)] -> Term f v a -> Term f v a
pattern $mAbsNA' :: forall {r} {a} {v} {f :: * -> *}.
Term f v a -> ([(a, v)] -> Term f v a -> r) -> ((# #) -> r) -> r
AbsNA' avs body <- (unabsA -> (avs, body))

{-# COMPLETE Var', Cycle', Abs'', Tm' #-}

dropAbs :: Int -> Term f v a -> Term f v a
dropAbs :: forall (f :: * -> *) v a. Int -> Term f v a -> Term f v a
dropAbs Int
z Term f v a
tm | Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = Term f v a
tm
dropAbs Int
n (Term Set v
_ a
_ (Abs v
_ Term f v a
body)) = Int -> Term f v a -> Term f v a
forall (f :: * -> *) v a. Int -> Term f v a -> Term f v a
dropAbs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term f v a
body
dropAbs Int
_ Term f v a
tm = Term f v a
tm

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

var :: v -> Term f v ()
var :: forall v (f :: * -> *). v -> Term f v ()
var = () -> v -> Term f v ()
forall a v (f :: * -> *). a -> v -> Term f v a
annotatedVar ()

annotatedVar :: a -> v -> Term f v a
annotatedVar :: forall a v (f :: * -> *). a -> v -> Term f v a
annotatedVar = a -> v -> Term f v a
forall a v (f :: * -> *). a -> v -> Term f v a
U.Core.ABT.var

abs :: (Ord v) => v -> Term f v () -> Term f v ()
abs :: forall v (f :: * -> *). Ord v => v -> Term f v () -> Term f v ()
abs = () -> v -> Term f v () -> Term f v ()
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs' ()

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 -> 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
U.Core.ABT.abs

absr :: (Functor f, Foldable f, Var v) => v -> Term f (V v) () -> Term f (V v) ()
absr :: forall (f :: * -> *) v.
(Functor f, Foldable f, Var v) =>
v -> Term f (V v) () -> Term f (V v) ()
absr = () -> v -> Term f (V v) () -> Term f (V v) ()
forall (f :: * -> *) v a.
(Functor f, Foldable f, Var v) =>
a -> v -> Term f (V v) a -> Term f (V v) a
absr' ()

-- | Rebuild an `abs`, renaming `v` to avoid capturing any `Free v` in `body`.
absr' :: (Functor f, Foldable f, Var v) => a -> v -> Term f (V v) a -> Term f (V v) a
absr' :: forall (f :: * -> *) v a.
(Functor f, Foldable f, Var v) =>
a -> v -> Term f (V v) a -> Term f (V v) a
absr' a
a v
v Term f (V v) a
body = v
-> Term f (V v) a
-> (V v -> Term f (V v) a -> Term f (V v) a)
-> Term f (V v) a
forall (f :: * -> *) v a c.
(Functor f, Foldable f, Var v) =>
v -> Term f (V v) a -> (V v -> Term f (V v) a -> c) -> c
wrap' v
v Term f (V v) a
body ((V v -> Term f (V v) a -> Term f (V v) a) -> Term f (V v) a)
-> (V v -> Term f (V v) a -> Term f (V v) a) -> Term f (V v) a
forall a b. (a -> b) -> a -> b
$ \V v
v Term f (V v) a
body -> a -> V v -> Term f (V v) a -> Term f (V v) a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
abs' a
a V v
v Term f (V v) a
body

absChain :: (Ord v) => [v] -> Term f v () -> Term f v ()
absChain :: forall v (f :: * -> *). Ord v => [v] -> Term f v () -> Term f v ()
absChain [v]
vs Term f v ()
t = (v -> Term f v () -> Term f v ())
-> Term f v () -> [v] -> Term f v ()
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 () -> Term f v ()
forall v (f :: * -> *). Ord v => v -> Term f v () -> Term f v ()
abs Term f v ()
t [v]
vs

absChain' :: (Ord v) => [(a, v)] -> Term f v a -> Term f v a
absChain' :: forall v a (f :: * -> *).
Ord v =>
[(a, v)] -> Term f v a -> Term f v a
absChain' [(a, v)]
vs Term f v a
t = ((a, v) -> Term f v a -> Term f v a)
-> Term f v a -> [(a, v)] -> 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 (\(a
a, v
v) Term f v a
t -> 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 Term f v a
t) Term f v a
t [(a, v)]
vs

tm :: (Foldable f, Ord v) => f (Term f v ()) -> Term f v ()
tm :: forall (f :: * -> *) v.
(Foldable f, Ord v) =>
f (Term f v ()) -> Term f v ()
tm = () -> f (Term f v ()) -> Term f v ()
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
tm' ()

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 -> 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
U.Core.ABT.tm

cycle :: Term f v () -> Term f v ()
cycle :: forall (f :: * -> *) v. Term f v () -> Term f v ()
cycle = () -> Term f v () -> Term f v ()
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle' ()

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 -> Term f v a -> Term f v a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
U.Core.ABT.cycle

cycler' :: (Functor f, Foldable f, Var v) => a -> [v] -> Term f (V v) a -> Term f (V v) a
cycler' :: forall (f :: * -> *) v a.
(Functor f, Foldable f, Var v) =>
a -> [v] -> Term f (V v) a -> Term f (V v) a
cycler' a
a [v]
vs Term f (V v) a
t = a -> Term f (V v) a -> Term f (V v) a
forall a (f :: * -> *) v. a -> Term f v a -> Term f v a
cycle' a
a (Term f (V v) a -> Term f (V v) a)
-> Term f (V v) a -> Term f (V v) a
forall a b. (a -> b) -> a -> b
$ (v -> Term f (V v) a -> Term f (V v) a)
-> Term f (V v) a -> [v] -> Term f (V 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 (a -> v -> Term f (V v) a -> Term f (V v) a
forall (f :: * -> *) v a.
(Functor f, Foldable f, Var v) =>
a -> v -> Term f (V v) a -> Term f (V v) a
absr' a
a) Term f (V v) a
t [v]
vs

cycler :: (Functor f, Foldable f, Var v) => [v] -> Term f (V v) () -> Term f (V v) ()
cycler :: forall (f :: * -> *) v.
(Functor f, Foldable f, Var v) =>
[v] -> Term f (V v) () -> Term f (V v) ()
cycler = () -> [v] -> Term f (V v) () -> Term f (V v) ()
forall (f :: * -> *) v a.
(Functor f, Foldable f, Var v) =>
a -> [v] -> Term f (V v) a -> Term f (V v) a
cycler' ()

renames ::
  (Foldable f, Functor f, Var v) =>
  Map v v ->
  Term f v a ->
  Term f v a
renames :: forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames Map v v
rn0 t0 :: Term f v a
t0@(Term Set v
fvs a
ann ABT f v (Term f v a)
t)
  | Map v v -> Bool
forall k a. Map k a -> Bool
Map.null Map v v
rn = Term f v a
t0
  | Var v
v <- ABT f v (Term f v a)
t,
    Just v
u <- v -> Map v v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v v
rn =
      a -> v -> Term f v a
forall a v (f :: * -> *). a -> v -> Term f v a
annotatedVar a
ann v
u
  | Cycle Term f v a
body <- ABT f v (Term f v a)
t =
      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 v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames Map v v
rn Term f v a
body)
  | Abs v
v Term f v a
t <- ABT f v (Term f v a)
t,
    -- rename iterated variables all at once to avoid a capture issue
    AbsNA' ([(a, v)] -> ([a], [v])
forall a b. [(a, b)] -> ([a], [b])
unzip -> ([a]
as, [v]
vs)) Term f v a
body <- Term f v a
t,
    (Map v v
rn, [v]
us) <- Set v -> Map v v -> [v] -> (Map v v, [v])
forall {b}. Var b => Set b -> Map b b -> [b] -> (Map b b, [b])
mangle (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
body) Map v v
rn (v
v v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
vs),
    Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map v v -> Bool
forall k a. Map k a -> Bool
Map.null Map v v
rn =
      [(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
absChain' ([a] -> [v] -> [(a, v)]
forall a b. [a] -> [b] -> [(a, b)]
zip (a
ann a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
as) [v]
us) (Map v v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames Map v v
rn Term f v a
body)
  | Tm f (Term f v a)
body <- ABT f v (Term f v a)
t =
      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 (Map v v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames Map v v
rn (Term f v a -> Term f v a) -> f (Term f v a) -> f (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Term f v a)
body)
  | Bool
otherwise = Term f v a
t0
  where
    rn :: Map v v
rn = Map v v -> Set v -> Map v v
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map v v
rn0 Set v
fvs
    mangle :: Set b -> Map b b -> [b] -> (Map b b, [b])
mangle Set b
fvs Map b b
m [b]
vs =
      let avs :: Set b
avs = [b] -> Set b
forall a. Ord a => [a] -> Set a
Set.fromList [b]
vs Set b -> Set b -> Set b
forall a. Semigroup a => a -> a -> a
<> Set b
fvs
       in (Map b b -> b -> (Map b b, b)) -> Map b b -> [b] -> (Map b b, [b])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL (Set b -> Map b b -> b -> (Map b b, b)
forall {b}. Var b => Set b -> Map b b -> b -> (Map b b, b)
mangle1 Set b
avs) Map b b
m [b]
vs
    mangle1 :: Set b -> Map b b -> b -> (Map b b, b)
mangle1 Set b
avs Map b b
m b
v
      | (b -> Bool) -> [b] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
v) [b]
vs,
        b
u <- Set b -> b -> b
forall v. Var v => Set v -> v -> v
freshIn (Set b
avs Set b -> Set b -> Set b
forall a. Semigroup a => a -> a -> a
<> [b] -> Set b
forall a. Ord a => [a] -> Set a
Set.fromList [b]
vs) b
v =
          (b -> b -> Map b b -> Map b b
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert b
v b
u Map b b
m, b
u)
      | Bool
otherwise = (b -> Map b b -> Map b b
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete b
v Map b b
m, b
v)
      where
        vs :: [b]
vs = Map b b -> [b]
forall a. Map b a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Map b b
m

-- Note: this does not do capture-avoiding renaming. It actually
-- renames bound variables using the map as well.
changeVars :: (Foldable f, Functor f, Var v) => Map v v -> Term f v a -> Term f v a
changeVars :: forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
changeVars Map v v
m 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
  Abs v
v Term f v a
body -> case v -> Map v v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v v
m of
    Maybe v
Nothing -> 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
v (Map v v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
changeVars Map v v
m Term f v a
body)
    Just v
v' -> 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
v' (Map v v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
changeVars Map v v
m Term f v a
body)
  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) (Map v v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
changeVars Map v v
m Term f v a
body)
  Var v
v -> case v -> Map v v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v v
m of
    Maybe v
Nothing -> Term f v a
t
    Just v
v -> a -> v -> Term f v a
forall a v (f :: * -> *). a -> v -> Term f v a
annotatedVar (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) v
v
  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' (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t) (Map v v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
changeVars Map v v
m (Term f v a -> Term f v a) -> f (Term f v a) -> f (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Term f v a)
v)

fresh :: (Var v) => Term f v a -> v -> v
fresh :: forall v (f :: * -> *) a. Var v => Term f v a -> v -> v
fresh Term f v a
t = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
t)

-- Numbers the free vars by the position where they're first
-- used within the term. See usage in `Type.normalizeForallOrder`
numberedFreeVars :: (Ord v, Foldable f) => Term f v a -> Map v Int
numberedFreeVars :: forall v (f :: * -> *) a.
(Ord v, Foldable f) =>
Term f v a -> Map v Int
numberedFreeVars Term f v a
t =
  [(v, Int)] -> Map v Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(v, Int)] -> Map v Int) -> [(v, Int)] -> Map v Int
forall a b. (a -> b) -> a -> b
$ [(v, Int)] -> [(v, Int)]
forall a. [a] -> [a]
reverse ([v] -> Term f v a -> [v]
forall {a} {t :: * -> *} {a}.
(Eq a, Foldable t) =>
[a] -> Term t a a -> [a]
go [v]
forall a. Monoid a => a
mempty Term f v a
t [v] -> [Int] -> [(v, Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Int
0 ..])
  where
    go :: [a] -> Term t a a -> [a]
go [a]
bound Term t a a
t = case Term t a a -> ABT t a (Term t a a)
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term t a a
t of
      Var a
v -> if a
v a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
bound then [] else [a
v]
      Cycle Term t a a
body -> [a] -> Term t a a -> [a]
go [a]
bound Term t a a
body
      Abs a
v Term t a a
body -> [a] -> Term t a a -> [a]
go (a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
bound) Term t a a
body
      Tm t (Term t a a)
v -> t (Term t a a) -> [Term t a a]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList t (Term t a a)
v [Term t a a] -> (Term t a a -> [a]) -> [a]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [a] -> Term t a a -> [a]
go [a]
bound

-- | `subst v e body` substitutes `e` for `v` in `body`, avoiding capture by
-- renaming abstractions in `body`
subst ::
  (Foldable f, Functor f, Var v) =>
  v ->
  Term f v a ->
  Term f v a ->
  Term f v a
subst :: forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> Term f v a -> Term f v a -> Term f v a
subst v
v Term f v a
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' (Term f v a -> a -> Term f v a
forall a b. a -> b -> a
const Term f v a
r) v
v (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
r)

-- | `substs [(t1,v1), (t2,v2), ...] body` performs multiple simultaneous
-- substitutions, avoiding capture
substs ::
  (Foldable f, Functor f, Var v) =>
  [(v, Term f v a)] ->
  Term f v a ->
  Term f v a
substs :: forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
[(v, Term f v a)] -> Term f v a -> Term f v a
substs [(v, Term f v a)]
replacements Term f v a
body = ((v, Term f v a) -> Term f v a -> Term f v a)
-> Term f v a -> [(v, Term f v a)] -> 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 a -> Term f v a -> Term f v a)
-> (v, Term f v a) -> Term f v a -> Term f v a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry v -> Term f v a -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> Term f v a -> Term f v a -> Term f v a
subst) Term f v a
body ([(v, Term f v a)] -> [(v, Term f v a)]
forall a. [a] -> [a]
reverse [(v, Term f v a)]
replacements)

-- Count the number times the given variable appears free in the term
occurrences :: (Foldable f, Var v) => v -> Term f v a -> Int
occurrences :: forall (f :: * -> *) v a.
(Foldable f, Var v) =>
v -> Term f v a -> Int
occurrences v
v Term f v a
t | Bool -> Bool
not (v
v v -> Term f v a -> Bool
forall v (f :: * -> *) a. Ord v => v -> Term f v a -> Bool
`isFreeIn` Term f v a
t) = Int
0
occurrences v
v 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
v2 -> if v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2 then Int
1 else Int
0
  Cycle Term f v a
t -> v -> Term f v a -> Int
forall (f :: * -> *) v a.
(Foldable f, Var v) =>
v -> Term f v a -> Int
occurrences v
v Term f v a
t
  Abs v
v2 Term f v a
t -> if v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2 then Int
0 else v -> Term f v a -> Int
forall (f :: * -> *) v a.
(Foldable f, Var v) =>
v -> Term f v a -> Int
occurrences v
v Term f v a
t
  Tm f (Term f v a)
t -> (Int -> Term f v a -> Int) -> Int -> [Term f v a] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Int
s Term f v a
t -> Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ v -> Term f v a -> Int
forall (f :: * -> *) v a.
(Foldable f, Var v) =>
v -> Term f v a -> Int
occurrences v
v Term f v a
t) Int
0 ([Term f v a] -> Int) -> [Term f v a] -> Int
forall a b. (a -> b) -> a -> b
$ 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

rebuildUp ::
  (Ord v, Foldable f, Functor f) =>
  (f (Term f v a) -> f (Term f v a)) ->
  Term f v a ->
  Term f v a
rebuildUp :: forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(f (Term f v a) -> f (Term f v a)) -> Term f v a -> Term f v a
rebuildUp f (Term f v a) -> f (Term f v a)
f (Term Set v
_ a
ann ABT f v (Term f v a)
body) = case ABT f v (Term f v a)
body of
  Var v
v -> a -> v -> Term f v a
forall a v (f :: * -> *). a -> v -> Term f v a
annotatedVar a
ann v
v
  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 ((f (Term f v a) -> f (Term f v a)) -> Term f v a -> Term f v a
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(f (Term f v a) -> f (Term f v a)) -> Term f v a -> Term f v a
rebuildUp f (Term f v a) -> 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' a
ann v
x ((f (Term f v a) -> f (Term f v a)) -> Term f v a -> Term f v a
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(f (Term f v a) -> f (Term f v a)) -> Term f v a -> Term f v a
rebuildUp f (Term f v a) -> f (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' a
ann (f (Term f v a) -> f (Term f v a)
f (f (Term f v a) -> f (Term f v a))
-> f (Term f v a) -> f (Term f v a)
forall a b. (a -> b) -> a -> b
$ (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 ((f (Term f v a) -> f (Term f v a)) -> Term f v a -> Term f v a
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(f (Term f v a) -> f (Term f v a)) -> Term f v a -> Term f v a
rebuildUp f (Term f v a) -> f (Term f v a)
f) f (Term f v a)
body)

rebuildUp' ::
  (Ord v, Foldable f, Functor f) =>
  (Term f v a -> Term f v a) ->
  Term f v a ->
  Term f v a
rebuildUp' :: forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> Term f v a) -> Term f v a -> Term f v a
rebuildUp' Term f v a -> Term f v a
f (Term Set v
_ a
ann ABT f v (Term f v a)
body) = case ABT f v (Term f v a)
body of
  Var v
v -> Term f v a -> Term f v a
f (a -> v -> Term f v a
forall a v (f :: * -> *). a -> v -> Term f v a
annotatedVar a
ann v
v)
  Cycle Term f v a
body -> Term f v a -> Term f v a
f (Term f v a -> Term f v a) -> Term f v a -> Term f v a
forall a b. (a -> b) -> a -> b
$ 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 ((Term f v a -> Term f v a) -> Term f v a -> Term f v a
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> Term f v a) -> Term f v a -> Term f v a
rebuildUp' Term f v a -> Term f v a
f Term f v a
body)
  Abs v
x Term f v a
e -> Term f v a -> Term f v a
f (Term f v a -> Term f v a) -> Term f v a -> Term f v a
forall a b. (a -> b) -> a -> b
$ 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 -> Term f v a) -> Term f v a -> Term f v a
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> Term f v a) -> Term f v a -> Term f v a
rebuildUp' Term f v a -> Term f v a
f Term f v a
e)
  Tm f (Term f v a)
body -> Term f v a -> Term f v a
f (Term f v a -> Term f v a) -> Term f v a -> Term f v a
forall a b. (a -> b) -> a -> 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' 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 ((Term f v a -> Term f v a) -> Term f v a -> Term f v a
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> Term f v a) -> Term f v a -> Term f v a
rebuildUp' Term f v a -> Term f v a
f) f (Term f v a)
body)

rebuildMaybeUp ::
  (Ord v, Foldable f, Functor f) =>
  (Term f v a -> Maybe (Term f v a)) ->
  Term f v a ->
  Maybe (Term f v a)
rebuildMaybeUp :: forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> Maybe (Term f v a))
-> Term f v a -> Maybe (Term f v a)
rebuildMaybeUp Term f v a -> Maybe (Term f v a)
f tm :: Term f v a
tm@(Term Set v
_ a
ann ABT f v (Term f v a)
body) = Term f v a -> Maybe (Term f v a)
f (Term f v a -> Maybe (Term f v a))
-> Term f v a -> Maybe (Term f v a)
forall a b. (a -> b) -> a -> b
$ case ABT f v (Term f v a)
body of
  Var v
_ -> Term f v a
tm
  Cycle Term f v a
body -> Term f v a -> Maybe (Term f v a) -> Term f v a
forall a. a -> Maybe a -> a
fromMaybe Term f v a
tm (Maybe (Term f v a) -> Term f v a)
-> Maybe (Term f v a) -> Term f v a
forall a b. (a -> b) -> a -> b
$ (Term f v a -> Term f v a)
-> Maybe (Term f v a) -> Maybe (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 (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) ((Term f v a -> Maybe (Term f v a))
-> Term f v a -> Maybe (Term f v a)
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> Maybe (Term f v a))
-> Term f v a -> Maybe (Term f v a)
rebuildMaybeUp Term f v a -> Maybe (Term f v a)
f Term f v a
body)
  Abs v
x Term f v a
e -> Term f v a -> Maybe (Term f v a) -> Term f v a
forall a. a -> Maybe a -> a
fromMaybe Term f v a
tm (Maybe (Term f v a) -> Term f v a)
-> Maybe (Term f v a) -> Term f v a
forall a b. (a -> b) -> a -> b
$ (Term f v a -> Term f v a)
-> Maybe (Term f v a) -> Maybe (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 (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 -> Maybe (Term f v a))
-> Term f v a -> Maybe (Term f v a)
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> Maybe (Term f v a))
-> Term f v a -> Maybe (Term f v a)
rebuildMaybeUp Term f v a -> Maybe (Term f v a)
f Term f v a
e)
  Tm f (Term f v a)
body ->
    if ((Term f v a, Maybe (Term f v a)) -> Bool)
-> f (Term f v a, Maybe (Term f v a)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe (Term f v a) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (Term f v a) -> Bool)
-> ((Term f v a, Maybe (Term f v a)) -> Maybe (Term f v a))
-> (Term f v a, Maybe (Term f v a))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term f v a, Maybe (Term f v a)) -> Maybe (Term f v a)
forall a b. (a, b) -> b
snd) f (Term f v a, Maybe (Term f v a))
body'
      then Term f v a
tm
      else 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, Maybe (Term f v a)) -> Term f v a)
-> f (Term f v a, Maybe (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 ((Term f v a -> Maybe (Term f v a) -> Term f v a)
-> (Term f v a, Maybe (Term f v a)) -> Term f v a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Term f v a -> Maybe (Term f v a) -> Term f v a
forall a. a -> Maybe a -> a
fromMaybe) f (Term f v a, Maybe (Term f v a))
body')
    where
      body' :: f (Term f v a, Maybe (Term f v a))
body' = (Term f v a -> (Term f v a, Maybe (Term f v a)))
-> f (Term f v a) -> f (Term f v a, Maybe (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 (\Term f v a
tm -> (Term f v a
tm, (Term f v a -> Maybe (Term f v a))
-> Term f v a -> Maybe (Term f v a)
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> Maybe (Term f v a))
-> Term f v a -> Maybe (Term f v a)
rebuildMaybeUp Term f v a -> Maybe (Term f v a)
f Term f v a
tm)) f (Term f v a)
body

freeVarOccurrences :: (Traversable f, Ord v) => Set v -> Term f v a -> [(v, a)]
freeVarOccurrences :: forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
Set v -> Term f v a -> [(v, a)]
freeVarOccurrences Set v
except Term f v a
t =
  [(v
v, a
a) | (v
v, a
a) <- Term f v (a, Set v) -> [(v, a)]
forall {v} {t :: * -> *} {b}.
(Ord v, Foldable t) =>
Term t v (b, Set v) -> [(v, b)]
go (Term f v (a, Set v) -> [(v, a)])
-> Term f v (a, Set v) -> [(v, a)]
forall a b. (a -> b) -> a -> b
$ Term f v a -> Term f v (a, Set v)
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
Term f v a -> Term f v (a, Set v)
annotateBound Term f v a
t, Bool -> Bool
not (v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
v Set v
except)]
  where
    go :: Term t v (b, Set v) -> [(v, b)]
go Term t v (b, Set v)
e = case Term t v (b, Set v) -> ABT t v (Term t v (b, Set v))
forall (f :: * -> *) v a. Term f v a -> ABT f v (Term f v a)
out Term t v (b, Set v)
e of
      Var v
v ->
        if v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
v ((b, Set v) -> Set v
forall a b. (a, b) -> b
snd ((b, Set v) -> Set v) -> (b, Set v) -> Set v
forall a b. (a -> b) -> a -> b
$ Term t v (b, Set v) -> (b, Set v)
forall (f :: * -> *) v a. Term f v a -> a
annotation Term t v (b, Set v)
e)
          then []
          else [(v
v, (b, Set v) -> b
forall a b. (a, b) -> a
fst ((b, Set v) -> b) -> (b, Set v) -> b
forall a b. (a -> b) -> a -> b
$ Term t v (b, Set v) -> (b, Set v)
forall (f :: * -> *) v a. Term f v a -> a
annotation Term t v (b, Set v)
e)]
      Cycle Term t v (b, Set v)
body -> Term t v (b, Set v) -> [(v, b)]
go Term t v (b, Set v)
body
      Abs v
_ Term t v (b, Set v)
body -> Term t v (b, Set v) -> [(v, b)]
go Term t v (b, Set v)
body
      Tm t (Term t v (b, Set v))
body -> (Term t v (b, Set v) -> [(v, b)])
-> t (Term t v (b, Set v)) -> [(v, b)]
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term t v (b, Set v) -> [(v, b)]
go t (Term t v (b, Set v))
body

-- subterms_ :: (Traversable f) => Fold (Term f v a) (Term f v a)
-- subterms_ = folding subterms

-- subTermsSetter_ :: (Traversable f, Ord v) => Setter' (Term f v a) (Term f v a)
-- subTermsSetter_ f tm = visit (Just . f) tm

rewriteDown ::
  (Traversable f, Ord v) =>
  (Term f v a -> Term f v a) ->
  Term f v a ->
  Term f v a
rewriteDown :: forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Term f v a) -> Term f v a -> Term f v a
rewriteDown Term f v a -> Term f v a
f Term f v a
tm = 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 :: * -> *) (m :: * -> *) v a.
(Traversable f, Monad m, Ord v) =>
(Term f v a -> m (Term f v a)) -> Term f v a -> m (Term f v a)
rewriteDown_ (Term f v a -> Identity (Term f v a)
forall a. a -> Identity a
Identity (Term f v a -> Identity (Term f v a))
-> (Term f v a -> Term f v a)
-> Term f v a
-> Identity (Term f v a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f v a -> Term f v a
f) Term f v a
tm

-- | Setter' (Term f v a) (Term f v a)
rewriteDown_ ::
  (Traversable f, Monad m, Ord v) =>
  (Term f v a -> m (Term f v a)) ->
  Term f v a ->
  m (Term f v a)
rewriteDown_ :: forall (f :: * -> *) (m :: * -> *) v a.
(Traversable f, Monad m, Ord v) =>
(Term f v a -> m (Term f v a)) -> Term f v a -> m (Term f v a)
rewriteDown_ Term f v a -> m (Term f v a)
f Term f v a
t = do
  Term f v a
t' <- Term f v a -> m (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
v -> Term f v a -> m (Term f v a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> v -> Term f v a
forall a v (f :: * -> *). a -> v -> Term f v a
annotatedVar (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t') v
v)
    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) -> m (Term f v a) -> m (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term f v a -> m (Term f v a)) -> Term f v a -> m (Term f v a)
forall (f :: * -> *) (m :: * -> *) v a.
(Traversable f, Monad m, Ord v) =>
(Term f v a -> m (Term f v a)) -> Term f v a -> m (Term f v a)
rewriteDown_ Term f v a -> m (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) -> m (Term f v a) -> m (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term f v a -> m (Term f v a)) -> Term f v a -> m (Term f v a)
forall (f :: * -> *) (m :: * -> *) v a.
(Traversable f, Monad m, Ord v) =>
(Term f v a -> m (Term f v a)) -> Term f v a -> m (Term f v a)
rewriteDown_ Term f v a -> m (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)
-> m (f (Term f v a)) -> m (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term f v a -> m (Term f v a))
-> f (Term f v a) -> m (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 -> m (Term f v a)) -> Term f v a -> m (Term f v a)
forall (f :: * -> *) (m :: * -> *) v a.
(Traversable f, Monad m, Ord v) =>
(Term f v a -> m (Term f v a)) -> Term f v a -> m (Term f v a)
rewriteDown_ Term f v a -> m (Term f v a)
f) f (Term f v a)
body)

data Subst f v a = Subst
  { forall (f :: * -> *) v a.
Subst f v a
-> forall (m :: * -> *) v'. Monad m => (v -> m v') -> m v'
freshen :: forall m v'. (Monad m) => (v -> m v') -> m v',
    forall (f :: * -> *) v a. Subst f v a -> Term f v a -> Term f v a
bind :: Term f v a -> Term f v a,
    forall (f :: * -> *) v a.
Subst f v a -> forall b. Term f v b -> Term f v a
bindInheritAnnotation :: forall b. Term f v b -> Term f v a,
    forall (f :: * -> *) v a. Subst f v a -> v
variable :: v
  }

unabs1 :: forall a f v. (Foldable f, Functor f, Var v) => Term f v a -> Maybe (Subst f v a)
unabs1 :: forall a (f :: * -> *) v.
(Foldable f, Functor f, Var v) =>
Term f v a -> Maybe (Subst f v a)
unabs1 (Term Set v
_ a
_ (Abs v
v Term f v a
body)) = Subst f v a -> Maybe (Subst f v a)
forall a. a -> Maybe a
Just ((forall (m :: * -> *) v'. Monad m => (v -> m v') -> m v')
-> (Term f v a -> Term f v a)
-> (forall b. Term f v b -> Term f v a)
-> v
-> Subst f v a
forall (f :: * -> *) v a.
(forall (m :: * -> *) v'. Monad m => (v -> m v') -> m v')
-> (Term f v a -> Term f v a)
-> (forall b. Term f v b -> Term f v a)
-> v
-> Subst f v a
Subst (v -> m v') -> m v'
forall t. (v -> t) -> t
forall (m :: * -> *) v'. Monad m => (v -> m v') -> m v'
freshen Term f v a -> Term f v a
bind Term f v b -> Term f v a
forall b. Term f v b -> Term f v a
bindInheritAnnotation v
v)
  where
    freshen :: (v -> t) -> t
    freshen :: forall t. (v -> t) -> t
freshen v -> t
f = v -> t
f v
v
    bind :: Term f v a -> Term f v a
    bind :: Term f v a -> Term f v a
bind Term f v a
x = v -> Term f v a -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
v -> Term f v a -> Term f v a -> Term f v a
subst v
v Term f v a
x Term f v a
body
    bindInheritAnnotation :: Term f v b -> Term f v a
    bindInheritAnnotation :: forall b. Term f v b -> Term f v a
bindInheritAnnotation Term f v b
x = 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 v
v Term f v b
x Term f v a
body
unabs1 Term f v a
_ = Maybe (Subst f v a)
forall a. Maybe a
Nothing

-- Rebuild the tree annotations upward, starting from the leaves,
-- using the Monoid to choose the annotation at intermediate nodes
reannotateUp ::
  (Ord v, Foldable f, Functor f, Monoid b) =>
  (Term f v a -> b) ->
  Term f v a ->
  Term f v (a, b)
reannotateUp :: forall v (f :: * -> *) b a.
(Ord v, Foldable f, Functor f, Monoid b) =>
(Term f v a -> b) -> Term f v a -> Term f v (a, b)
reannotateUp Term f v a -> b
g 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, b) -> v -> Term f v (a, b)
forall a v (f :: * -> *). a -> v -> Term f v a
annotatedVar (Term f v a -> a
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v a
t, Term f v a -> b
g Term f v a
t) v
v
  Cycle Term f v a
body ->
    let body' :: Term f v (a, b)
body' = (Term f v a -> b) -> Term f v a -> Term f v (a, b)
forall v (f :: * -> *) b a.
(Ord v, Foldable f, Functor f, Monoid b) =>
(Term f v a -> b) -> Term f v a -> Term f v (a, b)
reannotateUp Term f v a -> b
g Term f v a
body
     in (a, b) -> Term f v (a, b) -> Term f v (a, b)
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, (a, b) -> b
forall a b. (a, b) -> b
snd (Term f v (a, b) -> (a, b)
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v (a, b)
body')) Term f v (a, b)
body'
  Abs v
v Term f v a
body ->
    let body' :: Term f v (a, b)
body' = (Term f v a -> b) -> Term f v a -> Term f v (a, b)
forall v (f :: * -> *) b a.
(Ord v, Foldable f, Functor f, Monoid b) =>
(Term f v a -> b) -> Term f v a -> Term f v (a, b)
reannotateUp Term f v a -> b
g Term f v a
body
     in (a, b) -> v -> Term f v (a, b) -> Term f v (a, b)
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, (a, b) -> b
forall a b. (a, b) -> b
snd (Term f v (a, b) -> (a, b)
forall (f :: * -> *) v a. Term f v a -> a
annotation Term f v (a, b)
body')) v
v Term f v (a, b)
body'
  Tm f (Term f v a)
body ->
    let body' :: f (Term f v (a, b))
body' = (Term f v a -> b) -> Term f v a -> Term f v (a, b)
forall v (f :: * -> *) b a.
(Ord v, Foldable f, Functor f, Monoid b) =>
(Term f v a -> b) -> Term f v a -> Term f v (a, b)
reannotateUp Term f v a -> b
g (Term f v a -> Term f v (a, b))
-> f (Term f v a) -> f (Term f v (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Term f v a)
body
        ann :: b
ann = Term f v a -> b
g Term f v a
t b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Term f v (a, b) -> b) -> f (Term f v (a, b)) -> b
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a, b) -> b
forall a b. (a, b) -> b
snd ((a, b) -> b)
-> (Term f v (a, b) -> (a, b)) -> Term f v (a, b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f v (a, b) -> (a, b)
forall (f :: * -> *) v a. Term f v a -> a
annotation) f (Term f v (a, b))
body'
     in (a, b) -> f (Term f v (a, b)) -> Term f v (a, b)
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, b
ann) f (Term f v (a, b))
body'

-- Given a list of terms, freshen all their free variables
-- to not overlap with any variables used within `wrt`.
-- The `afterFreshen` function is applied to each freshened
-- variable. It can be the identity function or `Var.bakeId`,
-- or it can do some other tagging of freshened variables.
--
-- This is used by structural find and replace to ensure that rules
-- don't accidentally capture local variables.
freshenWrt :: (Var v, Traversable f) => (v -> v) -> Term f v a -> [Term f v a] -> [Term f v a]
freshenWrt :: forall v (f :: * -> *) a.
(Var v, Traversable f) =>
(v -> v) -> Term f v a -> [Term f v a] -> [Term f v a]
freshenWrt v -> v
afterFreshen Term f v a
wrt [Term f v a]
tms = Map v v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames Map v v
varChanges (Term f v a -> Term f v a) -> [Term f v a] -> [Term f v a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term f v a]
tms
  where
    used :: Set v
used = [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList (Term f v a -> [v]
forall (f :: * -> *) v a. Foldable f => Term f v a -> [v]
allVars Term f v a
wrt)
    varChanges :: Map v v
varChanges =
      (Map v v, Set v) -> Map v v
forall a b. (a, b) -> a
fst ((Map v v, Set v) -> Map v v) -> (Map v v, Set v) -> Map v v
forall a b. (a -> b) -> a -> b
$ ((Map v v, Set v) -> v -> (Map v v, Set v))
-> (Map v v, Set v) -> Set v -> (Map v v, Set v)
forall b a. (b -> a -> b) -> b -> Set a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Map v v, Set v) -> v -> (Map v v, Set v)
go (Map v v
forall k a. Map k a
Map.empty, Set v
used) ((Term f v a -> Set v) -> [Term f v a] -> Set v
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars [Term f v a]
tms)
      where
        go :: (Map v v, Set v) -> v -> (Map v v, Set v)
go (Map v v
m, Set v
u) v
v = let v' :: v
v' = v -> v
afterFreshen (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn Set v
u v
v in (v -> v -> Map v v -> Map v v
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert v
v v
v' Map v v
m, v -> Set v -> Set v
forall a. Ord a => a -> Set a -> Set a
Set.insert v
v' Set v
u)

freshenBothWrt :: (Var v, Traversable f) => Term f v a -> Term f v a -> Term f v a -> (Term f v a, Term f v a)
freshenBothWrt :: forall v (f :: * -> *) a.
(Var v, Traversable f) =>
Term f v a -> Term f v a -> Term f v a -> (Term f v a, Term f v a)
freshenBothWrt Term f v a
wrt Term f v a
tm1 Term f v a
tm2 = case (v -> v) -> Term f v a -> [Term f v a] -> [Term f v a]
forall v (f :: * -> *) a.
(Var v, Traversable f) =>
(v -> v) -> Term f v a -> [Term f v a] -> [Term f v a]
freshenWrt v -> v
forall a. a -> a
id Term f v a
wrt [Term f v a
tm1, Term f v a
tm2] of
  [Term f v a
tm1, Term f v a
tm2] -> (Term f v a
tm1, Term f v a
tm2)
  [Term f v a]
_ -> String -> (Term f v a, Term f v a)
forall a. HasCallStack => String -> a
error String
"freshenWrt impossible"

-- | Core logic of structured find and replace. Works for any base functor.
-- Returns `Nothing` if no replacements.
rewriteExpression ::
  forall f v a.
  (Var v, Show v, forall a. (Eq a) => Eq (f a), forall a. (Show a) => Show (f a), Traversable f) =>
  Term f v a ->
  Term f v a ->
  Term f v a ->
  Maybe (Term f v a)
rewriteExpression :: forall (f :: * -> *) v a.
(Var v, Show v, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a), Traversable f) =>
Term f v a -> Term f v a -> Term f v a -> Maybe (Term f v a)
rewriteExpression Term f v a
query0 Term f v a
replacement0 Term f v a
tm = Term f v a -> Maybe (Term f v a)
rewriteHere Term f v a
tm
  where
    (Term f v a
query, Term f v a
replacement) = Term f v a -> Term f v a -> Term f v a -> (Term f v a, Term f v a)
forall v (f :: * -> *) a.
(Var v, Traversable f) =>
Term f v a -> Term f v a -> Term f v a -> (Term f v a, Term f v a)
freshenBothWrt Term f v a
tm Term f v a
query0 Term f v a
replacement0
    env0 :: Map v (Maybe (Term f v a))
env0 = [(v, Maybe (Term f v a))] -> Map v (Maybe (Term f v a))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(v
v, Maybe (Term f v a)
forall a. Maybe a
Nothing) | v
v <- Set v -> [v]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
query)]
    vs0 :: Set v
vs0 = Map v (Maybe (Term f v a)) -> Set v
forall k a. Map k a -> Set k
Map.keysSet Map v (Maybe (Term f v a))
env0
    rewriteHere :: Term f v a -> Maybe (Term f v a)
    rewriteHere :: Term f v a -> Maybe (Term f v a)
rewriteHere Term f v a
tm =
      case State (Map v (Maybe (Term f v a))) Bool
-> Map v (Maybe (Term f v a)) -> (Bool, Map v (Maybe (Term f v a)))
forall s a. State s a -> s -> (a, s)
runState (Term f v a -> Term f v a -> State (Map v (Maybe (Term f v a))) Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (Term f v a))) m =>
Term f v a -> Term f v a -> m Bool
go Term f v a
query Term f v a
tm) Map v (Maybe (Term f v a))
env0 of
        (Bool
False, Map v (Maybe (Term f v a))
_) -> Term f v a -> Maybe (Term f v a)
descend Term f v a
tm
        (Bool
True, Map v (Maybe (Term f v a))
subs) ->
          let tm' :: Term f v a
tm' = [(v, Term f v a)] -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
[(v, Term f v a)] -> Term f v a -> Term f v a
substs [(v
k, Term f v a
v) | (v
k, Just Term f v a
v) <- Map v (Maybe (Term f v a)) -> [(v, Maybe (Term f v a))]
forall k a. Map k a -> [(k, a)]
Map.toList Map v (Maybe (Term f v a))
subs] Term f v a
replacement
           in Term f v a -> Maybe (Term f v a)
descend Term f v a
tm' Maybe (Term f v a) -> Maybe (Term f v a) -> Maybe (Term f v a)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term f v a -> Maybe (Term f v a)
forall a. a -> Maybe a
Just Term f v a
tm'
      where
        descend :: Term f v a -> Maybe (Term f v a)
        descend :: Term f v a -> Maybe (Term f v a)
descend Term f v a
tm0 = 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
tm0 of
          Abs v
v Term f v a
tm -> 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
tm0) v
v (Term f v a -> Term f v a)
-> Maybe (Term f v a) -> Maybe (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f v a -> Maybe (Term f v a)
rewriteHere Term f v a
tm
          Cycle Term f v a
tm -> 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
tm0) (Term f v a -> Term f v a)
-> Maybe (Term f v a) -> Maybe (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f v a -> Maybe (Term f v a)
rewriteHere Term f v a
tm
          Var v
_v -> Maybe (Term f v a)
forall a. Maybe a
Nothing
          Tm f (Term f v a)
f ->
            let ps :: f (Term f v a, Maybe (Term f v a))
ps = (\Term f v a
t -> (Term f v a
t, Term f v a -> Maybe (Term f v a)
rewriteHere Term f v a
t)) (Term f v a -> (Term f v a, Maybe (Term f v a)))
-> f (Term f v a) -> f (Term f v a, Maybe (Term f v a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Term f v a)
f
             in if ((Term f v a, Maybe (Term f v a)) -> Bool)
-> [(Term f v a, Maybe (Term f v a))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe (Term f v a) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (Term f v a) -> Bool)
-> ((Term f v a, Maybe (Term f v a)) -> Maybe (Term f v a))
-> (Term f v a, Maybe (Term f v a))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term f v a, Maybe (Term f v a)) -> Maybe (Term f v a)
forall a b. (a, b) -> b
snd) (f (Term f v a, Maybe (Term f v a))
-> [(Term f v a, Maybe (Term f v a))]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (Term f v a, Maybe (Term f v a))
ps)
                  then Maybe (Term f v a)
forall a. Maybe a
Nothing
                  else Term f v a -> Maybe (Term f v a)
forall a. a -> Maybe a
Just (Term f v a -> Maybe (Term f v a))
-> Term f v a -> Maybe (Term f v a)
forall a b. (a -> b) -> a -> 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
tm0) ((Term f v a -> Maybe (Term f v a) -> Term f v a)
-> (Term f v a, Maybe (Term f v a)) -> Term f v a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Term f v a -> Maybe (Term f v a) -> Term f v a
forall a. a -> Maybe a -> a
fromMaybe ((Term f v a, Maybe (Term f v a)) -> Term f v a)
-> f (Term f v a, Maybe (Term f v a)) -> f (Term f v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Term f v a, Maybe (Term f v a))
ps)
        go ::
          (MonadState (Map v (Maybe (Term f v a))) m) =>
          Term f v a ->
          Term f v a ->
          m Bool
        go :: forall (m :: * -> *).
MonadState (Map v (Maybe (Term f v a))) m =>
Term f v a -> Term f v a -> m Bool
go tm0 :: Term f v a
tm0@(Var' v
v) Term f v a
tm = do
          Map v (Maybe (Term f v a))
env <- m (Map v (Maybe (Term f v a)))
forall s (m :: * -> *). MonadState s m => m s
get
          case v -> Map v (Maybe (Term f v a)) -> Maybe (Maybe (Term f v a))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v (Maybe (Term f v a))
env of
            Just Maybe (Term f v a)
Nothing -> Map v (Maybe (Term f v a)) -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (v
-> Maybe (Term f v a)
-> Map v (Maybe (Term f v a))
-> Map v (Maybe (Term f v a))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert v
v (Term f v a -> Maybe (Term f v a)
forall a. a -> Maybe a
Just Term f v a
tm) Map v (Maybe (Term f v a))
env) m () -> m Bool -> m Bool
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
            Just (Just Term f v a
b) -> Term f v a -> Term f v a -> m Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (Term f v a))) m =>
Term f v a -> Term f v a -> m Bool
go Term f v a
b Term f v a
tm
            Maybe (Maybe (Term f v a))
Nothing -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Term f v a
tm0 Term f v a -> Term f v a -> Bool
forall a. Eq a => a -> a -> Bool
== Term f v a
tm
        go (Tm' f (Term f v a)
fq) (Tm' f (Term f v a)
tm) =
          if f (Term f v a) -> f ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void f (Term f v a)
fq f () -> f () -> Bool
forall a. Eq a => a -> a -> Bool
== f (Term f v a) -> f ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void f (Term f v a)
tm
            then (Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Bool -> Bool
forall a. a -> a
id ([Bool] -> Bool) -> m [Bool] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(Term f v a, Term f v a)]
-> ((Term f v a, Term f v a) -> m Bool) -> m [Bool]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (f (Term f v a) -> [Term f v a]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (Term f v a)
fq [Term f v a] -> [Term f v a] -> [(Term f v a, Term f v a)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` f (Term f v a) -> [Term f v a]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (Term f v a)
tm) (((Term f v a, Term f v a) -> m Bool) -> m [Bool])
-> ((Term f v a, Term f v a) -> m Bool) -> m [Bool]
forall a b. (a -> b) -> a -> b
$ \(Term f v a
fq, Term f v a
tm) -> Term f v a -> Term f v a -> m Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (Term f v a))) m =>
Term f v a -> Term f v a -> m Bool
go Term f v a
fq Term f v a
tm)
            else Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
        go (Cycle'' Term f v a
q) (Cycle'' Term f v a
tm) = Term f v a -> Term f v a -> m Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (Term f v a))) m =>
Term f v a -> Term f v a -> m Bool
go Term f v a
q Term f v a
tm
        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 -> Term f v a -> m Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (Term f v a))) m =>
Term f v a -> Term f v a -> m Bool
go Term f v a
body1 Term f v a
body2
            else
              let v3 :: v
v3 = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn Set v
vs0 (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ 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 Term f v a -> Term f v a -> m Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (Term f v a))) m =>
Term f v a -> Term f v a -> m Bool
go (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) (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 Term f v a
_ Term f v a
_ = Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

-- | Core logic of structured find. Works for any base functor.
-- Returns `True` if there's a subexpression of `tm` which matches `query0`
-- for some assignment of variables.
containsExpression :: forall f v a. (Var v, forall a. (Eq a) => Eq (f a), Traversable f) => Term f v a -> Term f v a -> Bool
containsExpression :: forall (f :: * -> *) v a.
(Var v, forall a. Eq a => Eq (f a), Traversable f) =>
Term f v a -> Term f v a -> Bool
containsExpression Term f v a
query0 Term f v a
tm = Term f v a -> Bool
matchesHere Term f v a
tm
  where
    used :: Set v
used = [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList (Term f v a -> [v]
forall (f :: * -> *) v a. Foldable f => Term f v a -> [v]
allVars Term f v a
tm)
    varChanges :: Map v v
varChanges =
      (Map v v, Set v) -> Map v v
forall a b. (a, b) -> a
fst ((Map v v, Set v) -> Map v v) -> (Map v v, Set v) -> Map v v
forall a b. (a -> b) -> a -> b
$ ((Map v v, Set v) -> v -> (Map v v, Set v))
-> (Map v v, Set v) -> Set v -> (Map v v, Set v)
forall b a. (b -> a -> b) -> b -> Set a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Map v v, Set v) -> v -> (Map v v, Set v)
forall {a}. Var a => (Map a a, Set a) -> a -> (Map a a, Set a)
go (Map v v
forall k a. Map k a
Map.empty, Set v
used) (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
query0)
      where
        go :: (Map a a, Set a) -> a -> (Map a a, Set a)
go (Map a a
m, Set a
u) a
v = let v' :: a
v' = Set a -> a -> a
forall v. Var v => Set v -> v -> v
freshIn Set a
u a
v in (a -> a -> Map a a -> Map a a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
v a
v' Map a a
m, a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
v' Set a
u)
    -- rename free vars to avoid possible capture of things in `tm`
    query :: Term f v a
query = Map v v -> Term f v a -> Term f v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames Map v v
varChanges Term f v a
query0
    env0 :: Map v (Maybe (ABT f v (Term f v a)))
env0 = [(v, Maybe (ABT f v (Term f v a)))]
-> Map v (Maybe (ABT f v (Term f v a)))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(v
v, Maybe (ABT f v (Term f v a))
forall a. Maybe a
Nothing) | v
v <- Set v -> [v]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f v a
query)]
    vs0 :: Set v
vs0 = Map v (Maybe (ABT f v (Term f v a))) -> Set v
forall k a. Map k a -> Set k
Map.keysSet Map v (Maybe (ABT f v (Term f v a)))
env0
    matchesHere :: Term f v a -> Bool
    matchesHere :: Term f v a -> Bool
matchesHere Term f v a
tm =
      State (Map v (Maybe (ABT f v (Term f v a)))) Bool
-> Map v (Maybe (ABT f v (Term f v a))) -> Bool
forall s a. State s a -> s -> a
evalState (ABT f v (Term f v a)
-> ABT f v (Term f v a)
-> State (Map v (Maybe (ABT f v (Term f v a)))) Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (ABT f v (Term f v a)))) m =>
ABT f v (Term f v a) -> ABT f v (Term f v a) -> m 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
query) (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
tm)) Map v (Maybe (ABT f v (Term f v a)))
env0 Bool -> Bool -> Bool
|| 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
tm of
        Abs v
_v Term f v a
tm -> Term f v a -> Bool
matchesHere Term f v a
tm
        Cycle Term f v a
tm -> Term f v a -> Bool
matchesHere Term f v a
tm
        Var v
_v -> Bool
False
        Tm f (Term f v a)
f -> (Term f v a -> Bool) -> [Term f v a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Term f v a -> Bool
matchesHere (f (Term f v a) -> [Term f v a]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (Term f v a)
f)
      where
        go ::
          (MonadState (Map v (Maybe (ABT f v (Term f v a)))) m) =>
          ABT f v (Term f v a) ->
          ABT f v (Term f v a) ->
          m Bool
        go :: forall (m :: * -> *).
MonadState (Map v (Maybe (ABT f v (Term f v a)))) m =>
ABT f v (Term f v a) -> ABT f v (Term f v a) -> m Bool
go tm0 :: ABT f v (Term f v a)
tm0@(Var v
v) ABT f v (Term f v a)
tm = do
          Map v (Maybe (ABT f v (Term f v a)))
env <- m (Map v (Maybe (ABT f v (Term f v a))))
forall s (m :: * -> *). MonadState s m => m s
get
          case v
-> Map v (Maybe (ABT f v (Term f v a)))
-> Maybe (Maybe (ABT f v (Term f v a)))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v (Maybe (ABT f v (Term f v a)))
env of
            Just Maybe (ABT f v (Term f v a))
Nothing -> Map v (Maybe (ABT f v (Term f v a))) -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (v
-> Maybe (ABT f v (Term f v a))
-> Map v (Maybe (ABT f v (Term f v a)))
-> Map v (Maybe (ABT f v (Term f v a)))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert v
v (ABT f v (Term f v a) -> Maybe (ABT f v (Term f v a))
forall a. a -> Maybe a
Just ABT f v (Term f v a)
tm) Map v (Maybe (ABT f v (Term f v a)))
env) m () -> m Bool -> m Bool
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
            Just (Just ABT f v (Term f v a)
b) -> ABT f v (Term f v a) -> ABT f v (Term f v a) -> m Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (ABT f v (Term f v a)))) m =>
ABT f v (Term f v a) -> ABT f v (Term f v a) -> m Bool
go ABT f v (Term f v a)
b ABT f v (Term f v a)
tm
            Maybe (Maybe (ABT f v (Term f v a)))
Nothing -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ABT f v (Term f v a)
tm0 ABT f v (Term f v a) -> ABT f v (Term f v a) -> Bool
forall a. Eq a => a -> a -> Bool
== ABT f v (Term f v a)
tm)
        go (Tm f (Term f v a)
fq) (Tm f (Term f v a)
tm) =
          if f (Term f v a) -> f ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void f (Term f v a)
fq f () -> f () -> Bool
forall a. Eq a => a -> a -> Bool
== f (Term f v a) -> f ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void f (Term f v a)
tm
            then (Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Bool -> Bool
forall a. a -> a
id ([Bool] -> Bool) -> m [Bool] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(Term f v a, Term f v a)]
-> ((Term f v a, Term f v a) -> m Bool) -> m [Bool]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (f (Term f v a) -> [Term f v a]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (Term f v a)
fq [Term f v a] -> [Term f v a] -> [(Term f v a, Term f v a)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` f (Term f v a) -> [Term f v a]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList f (Term f v a)
tm) (((Term f v a, Term f v a) -> m Bool) -> m [Bool])
-> ((Term f v a, Term f v a) -> m Bool) -> m [Bool]
forall a b. (a -> b) -> a -> b
$ \(Term f v a
fq, Term f v a
tm) -> ABT f v (Term f v a) -> ABT f v (Term f v a) -> m Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (ABT f v (Term f v a)))) m =>
ABT f v (Term f v a) -> ABT f v (Term f v a) -> m 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
fq) (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
tm))
            else Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
        go (Cycle Term f v a
q) (Cycle Term f v a
tm) = ABT f v (Term f v a) -> ABT f v (Term f v a) -> m Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (ABT f v (Term f v a)))) m =>
ABT f v (Term f v a) -> ABT f v (Term f v a) -> m 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
q) (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
tm)
        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 ABT f v (Term f v a) -> ABT f v (Term f v a) -> m Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (ABT f v (Term f v a)))) m =>
ABT f v (Term f v a) -> ABT f v (Term f v a) -> m 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
body1) (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
body2)
            else
              let v3 :: v
v3 = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn Set v
vs0 (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ 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 ABT f v (Term f v a) -> ABT f v (Term f v a) -> m Bool
forall (m :: * -> *).
MonadState (Map v (Maybe (ABT f v (Term f v a)))) m =>
ABT f v (Term f v a) -> ABT f v (Term f v a) -> m 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 -> ABT f v (Term f v a))
-> Term f v a -> ABT f v (Term f v a)
forall a b. (a -> b) -> a -> b
$ 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 -> 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 -> ABT f v (Term f v a))
-> Term f v a -> ABT f v (Term f v a)
forall a b. (a -> b) -> a -> b
$ 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 ABT f v (Term f v a)
_ ABT f v (Term f v a)
_ = Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

-- Find all subterms that match a predicate.  Prune the search for speed.
-- (Some patterns of pruning can cut the complexity of the search.)
data FindAction x = Found x | Prune | Continue
  deriving (Int -> FindAction x -> ShowS
[FindAction x] -> ShowS
FindAction x -> String
(Int -> FindAction x -> ShowS)
-> (FindAction x -> String)
-> ([FindAction x] -> ShowS)
-> Show (FindAction x)
forall x. Show x => Int -> FindAction x -> ShowS
forall x. Show x => [FindAction x] -> ShowS
forall x. Show x => FindAction x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall x. Show x => Int -> FindAction x -> ShowS
showsPrec :: Int -> FindAction x -> ShowS
$cshow :: forall x. Show x => FindAction x -> String
show :: FindAction x -> String
$cshowList :: forall x. Show x => [FindAction x] -> ShowS
showList :: [FindAction x] -> ShowS
Show, (forall a b. (a -> b) -> FindAction a -> FindAction b)
-> (forall a b. a -> FindAction b -> FindAction a)
-> Functor FindAction
forall a b. a -> FindAction b -> FindAction a
forall a b. (a -> b) -> FindAction a -> FindAction b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> FindAction a -> FindAction b
fmap :: forall a b. (a -> b) -> FindAction a -> FindAction b
$c<$ :: forall a b. a -> FindAction b -> FindAction a
<$ :: forall a b. a -> FindAction b -> FindAction a
Functor)

find ::
  (Ord v, Foldable f, Functor f) =>
  (Term f v a -> FindAction x) ->
  Term f v a ->
  [x]
find :: forall v (f :: * -> *) a x.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> FindAction x) -> Term f v a -> [x]
find Term f v a -> FindAction x
p Term f v a
t = case Term f v a -> FindAction x
p Term f v a
t of
  Found x
x -> x
x x -> [x] -> [x]
forall a. a -> [a] -> [a]
: [x]
go
  FindAction x
Prune -> []
  FindAction x
Continue -> [x]
go
  where
    go :: [x]
go = 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
_ -> []
      Cycle Term f v a
body -> (Term f v a -> FindAction x) -> Term f v a -> [x]
forall v (f :: * -> *) a x.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> FindAction x) -> Term f v a -> [x]
Unison.ABT.find Term f v a -> FindAction x
p Term f v a
body
      Abs v
_ Term f v a
body -> (Term f v a -> FindAction x) -> Term f v a -> [x]
forall v (f :: * -> *) a x.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> FindAction x) -> Term f v a -> [x]
Unison.ABT.find Term f v a -> FindAction x
p Term f v a
body
      Tm f (Term f v a)
body -> f [x] -> [x]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
Foldable.concat ((Term f v a -> FindAction x) -> Term f v a -> [x]
forall v (f :: * -> *) a x.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> FindAction x) -> Term f v a -> [x]
Unison.ABT.find Term f v a -> FindAction x
p (Term f v a -> [x]) -> f (Term f v a) -> f [x]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Term f v a)
body)

find' ::
  (Ord v, Foldable f, Functor f) =>
  (Term f v a -> Bool) ->
  Term f v a ->
  [Term f v a]
find' :: forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> Bool) -> Term f v a -> [Term f v a]
find' Term f v a -> Bool
p = (Term f v a -> FindAction (Term f v a))
-> Term f v a -> [Term f v a]
forall v (f :: * -> *) a x.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> FindAction x) -> Term f v a -> [x]
Unison.ABT.find (\Term f v a
t -> if Term f v a -> Bool
p Term f v a
t then Term f v a -> FindAction (Term f v a)
forall x. x -> FindAction x
Found Term f v a
t else FindAction (Term f v a)
forall x. FindAction x
Continue)

components :: (Var v) => [(v, Term f v a)] -> [[(v, Term f v a)]]
components :: forall v (f :: * -> *) a.
Var v =>
[(v, Term f v a)] -> [[(v, Term f v a)]]
components = (Term f v a -> Set v) -> [(v, Term f v a)] -> [[(v, Term f v a)]]
forall v t. Ord v => (t -> Set v) -> [(v, t)] -> [[(v, t)]]
Components.components Term f v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars

-- Converts to strongly connected components while preserving the
-- order of definitions. Satisfies `join (orderedComponents bs) == bs`.
orderedComponents' :: (Var v) => [(v, Term f v a)] -> [[(v, Term f v a)]]
orderedComponents' :: forall v (f :: * -> *) a.
Var v =>
[(v, Term f v a)] -> [[(v, Term f v a)]]
orderedComponents' [(v, Term f v a)]
tms = [(v, Term f v a)]
-> Set v -> [(v, Term f v a)] -> [[(v, Term f v a)]]
forall {a} {f :: * -> *} {a}.
Ord a =>
[(a, Term f a a)]
-> Set a -> [(a, Term f a a)] -> [[(a, Term f a a)]]
go [] Set v
forall a. Set a
Set.empty [(v, Term f v a)]
tms
  where
    go :: [(a, Term f a a)]
-> Set a -> [(a, Term f a a)] -> [[(a, Term f a a)]]
go [] Set a
_ [] = []
    go [] Set a
deps ((a, Term f a a)
hd : [(a, Term f a a)]
rem) = [(a, Term f a a)]
-> Set a -> [(a, Term f a a)] -> [[(a, Term f a a)]]
go [(a, Term f a a)
hd] (Set a
deps Set a -> Set a -> Set a
forall a. Semigroup a => a -> a -> a
<> Term f a a -> Set a
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars ((a, Term f a a) -> Term f a a
forall a b. (a, b) -> b
snd (a, Term f a a)
hd)) [(a, Term f a a)]
rem
    go [(a, Term f a a)]
cur Set a
deps [(a, Term f a a)]
rem = case ((a, Term f a a) -> Bool) -> [(a, Term f a a)] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex (a, Term f a a) -> Bool
isDep [(a, Term f a a)]
rem of
      Maybe Int
Nothing ->
        [(a, Term f a a)] -> [(a, Term f a a)]
forall a. [a] -> [a]
reverse [(a, Term f a a)]
cur
          [(a, Term f a a)] -> [[(a, Term f a a)]] -> [[(a, Term f a a)]]
forall a. a -> [a] -> [a]
: let ([(a, Term f a a)]
hd, [(a, Term f a a)]
tl) = Int -> [(a, Term f a a)] -> ([(a, Term f a a)], [(a, Term f a a)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
1 [(a, Term f a a)]
rem
             in [(a, Term f a a)]
-> Set a -> [(a, Term f a a)] -> [[(a, Term f a a)]]
go [(a, Term f a a)]
hd ([(a, Term f a a)] -> Set a
forall {a} {f :: * -> *} {a}. [(a, Term f a a)] -> Set a
depsFor [(a, Term f a a)]
hd) [(a, Term f a a)]
tl
      Just Int
i -> [(a, Term f a a)]
-> Set a -> [(a, Term f a a)] -> [[(a, Term f a a)]]
go ([(a, Term f a a)] -> [(a, Term f a a)]
forall a. [a] -> [a]
reverse [(a, Term f a a)]
newMembers [(a, Term f a a)] -> [(a, Term f a a)] -> [(a, Term f a a)]
forall a. [a] -> [a] -> [a]
++ [(a, Term f a a)]
cur) Set a
deps' (Int -> [(a, Term f a a)] -> [(a, Term f a a)]
forall a. Int -> [a] -> [a]
drop (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(a, Term f a a)]
rem)
        where
          deps' :: Set a
deps' = Set a
deps Set a -> Set a -> Set a
forall a. Semigroup a => a -> a -> a
<> [(a, Term f a a)] -> Set a
forall {a} {f :: * -> *} {a}. [(a, Term f a a)] -> Set a
depsFor [(a, Term f a a)]
newMembers
          newMembers :: [(a, Term f a a)]
newMembers = Int -> [(a, Term f a a)] -> [(a, Term f a a)]
forall a. Int -> [a] -> [a]
take (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(a, Term f a a)]
rem
      where
        depsFor :: [(a, Term f a a)] -> Set a
depsFor = ((a, Term f a a) -> Set a) -> [(a, Term f a a)] -> Set a
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Term f a a -> Set a
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars (Term f a a -> Set a)
-> ((a, Term f a a) -> Term f a a) -> (a, Term f a a) -> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Term f a a) -> Term f a a
forall a b. (a, b) -> b
snd)
        isDep :: (a, Term f a a) -> Bool
isDep (a
v, Term f a a
_) = a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
v Set a
deps

-- Like `orderedComponents'`, but further break up cycles and move
-- cyclic subcycles before other components in the same cycle.
-- Tweak suggested by @aryairani.
--
-- Example: given `[[x],[ping,r,s,pong]]`, where `ping` and `pong`
-- are mutually recursive but `r` and `s` are uninvolved, this produces:
-- `[[x], [ping,pong], [r], [s]]`.
orderedComponents :: (Var v) => [(v, Term f v a)] -> [[(v, Term f v a)]]
orderedComponents :: forall v (f :: * -> *) a.
Var v =>
[(v, Term f v a)] -> [[(v, Term f v a)]]
orderedComponents [(v, Term f v a)]
bs0 = [(v, Term f v a)] -> [[(v, Term f v a)]]
forall v (f :: * -> *) a.
Var v =>
[(v, Term f v a)] -> [[(v, Term f v a)]]
tweak ([(v, Term f v a)] -> [[(v, Term f v a)]])
-> [[(v, Term f v a)]] -> [[(v, Term f v a)]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [(v, Term f v a)] -> [[(v, Term f v a)]]
forall v (f :: * -> *) a.
Var v =>
[(v, Term f v a)] -> [[(v, Term f v a)]]
orderedComponents' [(v, Term f v a)]
bs0
  where
    tweak :: (Var v) => [(v, Term f v a)] -> [[(v, Term f v a)]]
    tweak :: forall v (f :: * -> *) a.
Var v =>
[(v, Term f v a)] -> [[(v, Term f v a)]]
tweak bs :: [(v, Term f v a)]
bs@((v, Term f v a)
_ : (v, Term f v a)
_ : [(v, Term f v a)]
_) = case ([(v, Term f v a)] -> Bool)
-> [[(v, Term f v a)]] -> [[(v, Term f v a)]]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile [(v, Term f v a)] -> Bool
forall {a} {f :: * -> *} {a}. Ord a => [(a, Term f a a)] -> Bool
isCyclic ([(v, Term f v a)] -> [[(v, Term f v a)]]
forall v (f :: * -> *) a.
Var v =>
[(v, Term f v a)] -> [[(v, Term f v a)]]
components [(v, Term f v a)]
bs) of
      [] -> [[(v, Term f v a)]
bs]
      [[(v, Term f v a)]]
cycles -> [[(v, Term f v a)]]
cycles [[(v, Term f v a)]] -> [[(v, Term f v a)]] -> [[(v, Term f v a)]]
forall a. Semigroup a => a -> a -> a
<> [(v, Term f v a)] -> [[(v, Term f v a)]]
forall v (f :: * -> *) a.
Var v =>
[(v, Term f v a)] -> [[(v, Term f v a)]]
orderedComponents [(v, Term f v a)]
rest
        where
          rest :: [(v, Term f v a)]
rest = [(v
v, Term f v a
b) | (v
v, Term f v a
b) <- [(v, Term f v a)]
bs, v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember v
v Set v
cycleVars]
          cycleVars :: Set v
cycleVars = [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList ((v, Term f v a) -> v
forall a b. (a, b) -> a
fst ((v, Term f v a) -> v) -> [(v, Term f v a)] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[(v, Term f v a)]] -> [(v, Term f v a)]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join [[(v, Term f v a)]]
cycles)
    tweak [(v, Term f v a)]
bs = [[(v, Term f v a)]
bs] -- any cycle with < 2 bindings is left alone
    isCyclic :: [(a, Term f a a)] -> Bool
isCyclic [(a
v, Term f a a
b)] = a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
v (Term f a a -> Set a
forall (f :: * -> *) v a. Term f v a -> Set v
freeVars Term f a a
b)
    isCyclic [(a, Term f a a)]
bs = [(a, Term f a a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, Term f a a)]
bs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1