Safe Haskell	None
Language	Haskell2010

Unison.ABT

Contents

Types
Combinators & Traversals
Optics
Safe Term constructors & Patterns
Algorithms

Description

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

Synopsis

data ABT (f :: Type -> Type) v r
- = Var v
- | Cycle r
- | Abs v r
- | Tm (f r)
data Term (f :: Type -> Type) v a = Term {
- freeVars :: Set v
- annotation :: a
- out :: ABT f v (Term f v a)
}
data Term' (f :: Type -> Type) v a x = Term' {
- freeVars' :: Set v
- annotation' :: a
- out' :: ABT f v x
}
class Ord v => Var v where
- freshIn :: Set v -> v -> v
data V v
- = Free v
- | Bound v
data Subst (f :: Type -> Type) v a = Subst {
- freshen :: forall (m :: Type -> Type) v'. Monad m => (v -> m v') -> m v'
- bind :: Term f v a -> Term f v a
- bindInheritAnnotation :: forall b. Term f v b -> Term f v a
- variable :: v
}
fresh :: forall v (f :: Type -> Type) a. Var v => Term f v a -> v -> v
unvar :: V v -> v
freshenS :: (Var v, MonadState (Set v) m) => v -> m v
freshInBoth :: forall v (f :: Type -> Type) a. Var v => Term f v a -> Term f v a -> v -> v
freshenBothWrt :: forall v (f :: Type -> Type) 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)
freshenWrt :: forall v (f :: Type -> Type) a. (Var v, Traversable f) => (v -> v) -> Term f v a -> [Term f v a] -> [Term f v a]
visit :: forall (f :: Type -> Type) g v a. (Traversable f, Applicative g, Ord v) => (Term f v a -> Maybe (g (Term f v a))) -> Term f v a -> g (Term f v a)
visit' :: (Traversable f, Monad g, Ord v) => (f (Term f v a) -> g (f (Term f v a))) -> Term f v a -> g (Term f v a)
visit_ :: (Traversable f, Applicative g, Ord v) => (f (Term f v a) -> g ()) -> Term f v a -> g (Term f v a)
visitPure :: forall (f :: Type -> Type) v a. (Traversable f, Ord v) => (Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
changeVars :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => Map v v -> Term f v a -> Term f v a
allVars :: forall (f :: Type -> Type) v a. Foldable f => Term f v a -> [v]
numberedFreeVars :: forall v (f :: Type -> Type) a. (Ord v, Foldable f) => Term f v a -> Map v Int
subterms :: forall v (f :: Type -> Type) a. (Ord v, Traversable f) => Term f v a -> [Term f v a]
annotateBound :: forall v (f :: Type -> Type) a. (Ord v, Foldable f, Functor f) => Term f v a -> Term f v (a, Set v)
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
rebuildMaybeUp :: forall v (f :: Type -> Type) 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)
rebuildUp' :: forall v (f :: Type -> Type) a. (Ord v, Foldable f, Functor f) => (Term f v a -> Term f v a) -> Term f v a -> Term f v a
reannotateUp :: forall v (f :: Type -> Type) b a. (Ord v, Foldable f, Functor f, Monoid b) => (Term f v a -> b) -> Term f v a -> Term f v (a, b)
rewriteDown :: forall (f :: Type -> Type) v a. (Traversable f, Ord v) => (Term f v a -> Term f v a) -> Term f v a -> Term f v a
transform :: (Ord v, Foldable g, Functor g) => (forall a1. f a1 -> g a1) -> Term f v a -> Term g v a
transformM :: (Ord v, Monad m, Traversable g) => (forall a1. f a1 -> m (g a1)) -> Term f v a -> m (Term g v a)
foreachSubterm :: forall (f :: Type -> Type) g v a b. (Traversable f, Applicative g) => (Term f v a -> g b) -> Term f v a -> g [b]
freeVarOccurrences :: forall (f :: Type -> Type) v a. (Traversable f, Ord v) => Set v -> Term f v a -> [(v, a)]
isFreeIn :: forall v (f :: Type -> Type) a. Ord v => v -> Term f v a -> Bool
occurrences :: forall (f :: Type -> Type) v a. (Foldable f, Var v) => v -> Term f v a -> Int
extraMap :: Functor g => (forall k. f k -> g k) -> Term f v a -> Term g v a
vmap :: forall (f :: Type -> Type) v' v a. (Functor f, Foldable f, Ord v') => (v -> v') -> Term f v a -> Term f v' a
vmapM :: forall m (f :: Type -> Type) v2 v a. (Applicative m, Traversable f, Foldable f, Ord v2) => (v -> m v2) -> Term f v a -> m (Term f v2 a)
amap :: forall (f :: Type -> Type) v a a2. (Functor f, Foldable f, Ord v) => (a -> a2) -> Term f v a -> Term f v a2
rename :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => v -> v -> Term f v a -> Term f v a
renames :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => Map v v -> Term f v a -> Term f v a
subst :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => v -> Term f v a -> Term f v a -> Term f v a
substs :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => [(v, Term f v a)] -> Term f v a -> Term f v a
substInheritAnnotation :: forall (f :: Type -> Type) v b a. (Foldable f, Functor f, Var v) => v -> Term f v b -> Term f v a -> Term f v a
substsInheritAnnotation :: forall (f :: Type -> Type) v b a. (Foldable f, Functor f, Var v) => [(v, Term f v b)] -> Term f v a -> Term f v a
find :: forall v (f :: Type -> Type) a x. (Ord v, Foldable f, Functor f) => (Term f v a -> FindAction x) -> Term f v a -> [x]
find' :: forall v (f :: Type -> Type) a. (Ord v, Foldable f, Functor f) => (Term f v a -> Bool) -> Term f v a -> [Term f v a]
data FindAction x
- = Found x
- | Prune
- | Continue
containsExpression :: forall (f :: Type -> Type) v a. (Var v, forall a1. Eq a1 => Eq (f a1), Traversable f) => Term f v a -> Term f v a -> Bool
rewriteExpression :: forall (f :: Type -> Type) v a. (Var v, Show v, forall a1. Eq a1 => Eq (f a1), forall a1. Show a1 => Show (f a1), Traversable f) => Term f v a -> Term f v a -> Term f v a -> Maybe (Term f v a)
baseFunctor_ :: Applicative m => (f (Term f v a) -> m (f (Term f v a))) -> Term f v a -> m (Term f v a)
rewriteDown_ :: forall (f :: Type -> Type) 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)
annotate :: forall a (f :: Type -> Type) v. a -> Term f v a -> Term f v a
annotatedVar :: forall a v (f :: Type -> Type). a -> v -> Term f v a
var :: forall v (f :: Type -> Type). v -> Term f v ()
tm :: (Foldable f, Ord v) => f (Term f v ()) -> Term f v ()
tm' :: (Foldable f, Ord v) => a -> f (Term f v a) -> Term f v a
abs :: forall v (f :: Type -> Type). Ord v => v -> Term f v () -> Term f v ()
absChain :: forall v (f :: Type -> Type). Ord v => [v] -> Term f v () -> Term f v ()
absChain' :: forall v a (f :: Type -> Type). Ord v => [(a, v)] -> Term f v a -> Term f v a
abs' :: forall v a (f :: Type -> Type). Ord v => a -> v -> Term f v a -> Term f v a
absr :: forall (f :: Type -> Type) v. (Functor f, Foldable f, Var v) => v -> Term f (V v) () -> Term f (V v) ()
unabs :: forall (f :: Type -> Type) v a. Term f v a -> ([v], Term f v a)
unabsA :: forall (f :: Type -> Type) v a. Term f v a -> ([(a, v)], Term f v a)
dropAbs :: forall (f :: Type -> Type) v a. Int -> Term f v a -> Term f v a
cycle :: forall (f :: Type -> Type) v. Term f v () -> Term f v ()
cycle' :: forall a (f :: Type -> Type) v. a -> Term f v a -> Term f v a
cycler :: forall (f :: Type -> Type) v. (Functor f, Foldable f, Var v) => [v] -> Term f (V v) () -> Term f (V v) ()
pattern Abs' :: (Foldable f, Functor f, Var v) => a -> Subst f v a -> Term f v a
pattern Abs'' :: v -> Term f v a -> Term f v a
pattern AbsN' :: [v] -> Term f v a -> Term f v a
pattern AbsNA' :: [(a, v)] -> Term f v a -> Term f v a
pattern Var' :: v -> Term f v a
pattern Cycle' :: [v] -> f (Term f v a) -> Term f v a
pattern Cycle'' :: Term f v a -> Term f v a
pattern CycleA' :: a -> [(a, v)] -> Term f v a -> Term f v a
pattern Tm' :: f (Term f v a) -> Term f v a
components :: forall v (f :: Type -> Type) a. Var v => [(v, Term f v a)] -> [[(v, Term f v a)]]
orderedComponents :: forall v (f :: Type -> Type) a. Var v => [(v, Term f v a)] -> [[(v, Term f v a)]]

Types

data ABT (f :: Type -> Type) v r #

Constructors

Var v
Cycle r
Abs v r
Tm (f r)

Instances

Instances details

Functor f => Functor (ABT f v)

Instance details

Defined in U.Core.ABT

Methods

fmap :: (a -> b) -> ABT f v a -> ABT f v b #

(<$) :: a -> ABT f v b -> ABT f v a #

Foldable f => Foldable (ABT f v)

Instance details

Defined in U.Core.ABT

Methods

fold :: Monoid m => ABT f v m -> m #

foldMap :: Monoid m => (a -> m) -> ABT f v a -> m #

foldMap' :: Monoid m => (a -> m) -> ABT f v a -> m #

foldr :: (a -> b -> b) -> b -> ABT f v a -> b #

foldr' :: (a -> b -> b) -> b -> ABT f v a -> b #

foldl :: (b -> a -> b) -> b -> ABT f v a -> b #

foldl' :: (b -> a -> b) -> b -> ABT f v a -> b #

foldr1 :: (a -> a -> a) -> ABT f v a -> a #

foldl1 :: (a -> a -> a) -> ABT f v a -> a #

toList :: ABT f v a -> [a] #

null :: ABT f v a -> Bool #

length :: ABT f v a -> Int #

elem :: Eq a => a -> ABT f v a -> Bool #

maximum :: Ord a => ABT f v a -> a #

minimum :: Ord a => ABT f v a -> a #

sum :: Num a => ABT f v a -> a #

product :: Num a => ABT f v a -> a #

Traversable f => Traversable (ABT f v)

Instance details

Defined in U.Core.ABT

Methods

traverse :: Applicative f0 => (a -> f0 b) -> ABT f v a -> f0 (ABT f v b) #

sequenceA :: Applicative f0 => ABT f v (f0 a) -> f0 (ABT f v a) #

mapM :: Monad m => (a -> m b) -> ABT f v a -> m (ABT f v b) #

sequence :: Monad m => ABT f v (m a) -> m (ABT f v a) #

Generic (ABT f v r)

Instance details

Defined in U.Core.ABT

Associated Types

type Rep (ABT f v r)

Instance details

Defined in U.Core.ABT

type Rep (ABT f v r) = D1 ('MetaData "ABT" "U.Core.ABT" "unison-core-0.0.0-CxlIGAiBveKilYzQr8iK1" 'False) ((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 v)) :+: C1 ('MetaCons "Cycle" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 r))) :+: (C1 ('MetaCons "Abs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 v) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 r)) :+: C1 ('MetaCons "Tm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (f r)))))

Methods

from :: ABT f v r -> Rep (ABT f v r) x #

to :: Rep (ABT f v r) x -> ABT f v r #

(Show v, Show r, Show (f r)) => Show (ABT f v r)

Instance details

Defined in U.Core.ABT

Methods

showsPrec :: Int -> ABT f v r -> ShowS #

show :: ABT f v r -> String #

showList :: [ABT f v r] -> ShowS #

(Eq v, Eq r, Eq (f r)) => Eq (ABT f v r)

Instance details

Defined in U.Core.ABT

Methods

(==) :: ABT f v r -> ABT f v r -> Bool #

(/=) :: ABT f v r -> ABT f v r -> Bool #

type Rep (ABT f v r)

Instance details

Defined in U.Core.ABT

type Rep (ABT f v r) = D1 ('MetaData "ABT" "U.Core.ABT" "unison-core-0.0.0-CxlIGAiBveKilYzQr8iK1" 'False) ((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 v)) :+: C1 ('MetaCons "Cycle" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 r))) :+: (C1 ('MetaCons "Abs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 v) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 r)) :+: C1 ('MetaCons "Tm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (f r)))))

data Term (f :: Type -> Type) v a #

At each level in the tree, we store the set of free variables and a value of type a. Variables are of type v.

Constructors

Term
Fields freeVars :: Set v annotation :: a out :: ABT f v (Term f v a)

Instances

Instances details

Functor f => Functor (Term f v)

Instance details

Defined in U.Core.ABT

Methods

fmap :: (a -> b) -> Term f v a -> Term f v b #

(<$) :: a -> Term f v b -> Term f v a #

Foldable f => Foldable (Term f v)

Instance details

Defined in U.Core.ABT

Methods

fold :: Monoid m => Term f v m -> m #

foldMap :: Monoid m => (a -> m) -> Term f v a -> m #

foldMap' :: Monoid m => (a -> m) -> Term f v a -> m #

foldr :: (a -> b -> b) -> b -> Term f v a -> b #

foldr' :: (a -> b -> b) -> b -> Term f v a -> b #

foldl :: (b -> a -> b) -> b -> Term f v a -> b #

foldl' :: (b -> a -> b) -> b -> Term f v a -> b #

foldr1 :: (a -> a -> a) -> Term f v a -> a #

foldl1 :: (a -> a -> a) -> Term f v a -> a #

toList :: Term f v a -> [a] #

null :: Term f v a -> Bool #

length :: Term f v a -> Int #

elem :: Eq a => a -> Term f v a -> Bool #

maximum :: Ord a => Term f v a -> a #

minimum :: Ord a => Term f v a -> a #

sum :: Num a => Term f v a -> a #

product :: Num a => Term f v a -> a #

Traversable f => Traversable (Term f v)

Instance details

Defined in U.Core.ABT

Methods

traverse :: Applicative f0 => (a -> f0 b) -> Term f v a -> f0 (Term f v b) #

sequenceA :: Applicative f0 => Term f v (f0 a) -> f0 (Term f v a) #

mapM :: Monad m => (a -> m b) -> Term f v a -> m (Term f v b) #

sequence :: Monad m => Term f v (m a) -> m (Term f v a) #

Generic (Term f v a)

Instance details

Defined in U.Core.ABT

Associated Types

type Rep (Term f v a)

Instance details

Defined in U.Core.ABT

type Rep (Term f v a) = D1 ('MetaData "Term" "U.Core.ABT" "unison-core-0.0.0-CxlIGAiBveKilYzQr8iK1" 'False) (C1 ('MetaCons "Term" 'PrefixI 'True) (S1 ('MetaSel ('Just "freeVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set v)) :*: (S1 ('MetaSel ('Just "annotation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "out") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ABT f v (Term f v a))))))

Methods

from :: Term f v a -> Rep (Term f v a) x #

to :: Rep (Term f v a) x -> Term f v a #

(forall a1. Show a1 => Show (f a1), Show v) => Show (Term f v a)

Instance details

Defined in U.Core.ABT

Methods

showsPrec :: Int -> Term f v a -> ShowS #

show :: Term f v a -> String #

showList :: [Term f v a] -> ShowS #

(Foldable f, Functor f, forall a1. Eq a1 => Eq (f a1), Var v) => Eq (Term f v a)

Instance details

Defined in U.Core.ABT

Methods

(==) :: Term f v a -> Term f v a -> Bool #

(/=) :: Term f v a -> Term f v a -> Bool #

(forall a1. Eq a1 => Eq (f a1), Foldable f, Functor f, forall a1. Ord a1 => Ord (f a1), Var v) => Ord (Term f v a)

Instance details

Defined in U.Core.ABT

Methods

compare :: Term f v a -> Term f v a -> Ordering #

(<) :: Term f v a -> Term f v a -> Bool #

(<=) :: Term f v a -> Term f v a -> Bool #

(>) :: Term f v a -> Term f v a -> Bool #

(>=) :: Term f v a -> Term f v a -> Bool #

max :: Term f v a -> Term f v a -> Term f v a #

min :: Term f v a -> Term f v a -> Term f v a #

Functor f => Recursive (Term f v a) (Term' f v a)

Instance details

Defined in U.Core.ABT

Methods

cata :: Algebra (Term' f v a) a0 -> Term f v a -> a0 #

project :: Term f v a -> Term' f v a (Term f v a) #

embed :: Term' f v a (Term f v a) -> Term f v a #

type Rep (Term f v a)

Instance details

Defined in U.Core.ABT

type Rep (Term f v a) = D1 ('MetaData "Term" "U.Core.ABT" "unison-core-0.0.0-CxlIGAiBveKilYzQr8iK1" 'False) (C1 ('MetaCons "Term" 'PrefixI 'True) (S1 ('MetaSel ('Just "freeVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set v)) :*: (S1 ('MetaSel ('Just "annotation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "out") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ABT f v (Term f v a))))))

data Term' (f :: Type -> Type) v a x #

Constructors

Term'
Fields freeVars' :: Set v annotation' :: a out' :: ABT f v x

Instances

Instances details

Functor f => Functor (Term' f v a)
Instance details Defined in U.Core.ABT Methods fmap :: (a0 -> b) -> Term' f v a a0 -> Term' f v a b # (<$) :: a0 -> Term' f v a b -> Term' f v a a0 #
Functor f => Recursive (Term f v a) (Term' f v a)
Instance details Defined in U.Core.ABT Methods cata :: Algebra (Term' f v a) a0 -> Term f v a -> a0 # project :: Term f v a -> Term' f v a (Term f v a) # embed :: Term' f v a (Term f v a) -> Term f v a #

class Ord v => Var v where #

A class for avoiding accidental variable capture

`Set.notMember (freshIn vs v) vs`: freshIn returns a variable not used in the Set

Methods

freshIn :: Set v -> v -> v #

Instances

Instances details

Var Symbol Source #
Instance details Defined in Unison.Symbol Methods freshIn :: Set Symbol -> Symbol -> Symbol #
Var v => Var (V v) Source #
Instance details Defined in Unison.ABT Methods freshIn :: Set (V v) -> V v -> V v #

data V v Source #

Constructors

Free v
Bound v

Instances

Instances details

Functor V Source #
Instance details Defined in Unison.ABT Methods fmap :: (a -> b) -> V a -> V b # (<$) :: a -> V b -> V a #
Show v => Show (V v) Source #
Instance details Defined in Unison.ABT Methods showsPrec :: Int -> V v -> ShowS # show :: V v -> String # showList :: [V v] -> ShowS #
Eq v => Eq (V v) Source #
Instance details Defined in Unison.ABT Methods (==) :: V v -> V v -> Bool # (/=) :: V v -> V v -> Bool #
Ord v => Ord (V v) Source #
Instance details Defined in Unison.ABT Methods compare :: 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 # max :: V v -> V v -> V v # min :: V v -> V v -> V v #
Var v => Var (V v) Source #
Instance details Defined in Unison.ABT Methods freshIn :: Set (V v) -> V v -> V v #

data Subst (f :: Type -> Type) v a Source #

Constructors

Subst
Fields freshen :: forall (m :: Type -> Type) v'. Monad m => (v -> m v') -> m v' bind :: Term f v a -> Term f v a bindInheritAnnotation :: forall b. Term f v b -> Term f v a variable :: v

Combinators & Traversals

fresh :: forall v (f :: Type -> Type) a. Var v => Term f v a -> v -> v Source #

unvar :: V v -> v Source #

freshenS :: (Var v, MonadState (Set v) m) => v -> m v #

Freshens the given variable wrt. the set of used variables tracked by state. Adds the result to the set of used variables.

freshInBoth :: forall v (f :: Type -> Type) a. Var v => Term f v a -> Term f v a -> v -> v #

Produce a variable which is free in both terms

freshenBothWrt :: forall v (f :: Type -> Type) 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) Source #

freshenWrt :: forall v (f :: Type -> Type) a. (Var v, Traversable f) => (v -> v) -> Term f v a -> [Term f v a] -> [Term f v a] Source #

visit :: forall (f :: Type -> Type) g v a. (Traversable f, Applicative g, Ord v) => (Term f v a -> Maybe (g (Term f v a))) -> Term f v a -> g (Term f v a) #

`visit f t` applies an effectful function to each subtree of t and sequences the results. When f returns Nothing, visit descends into the children of the current subtree. When f returns `Just t2`, visit replaces the current subtree with t2. Thus: `visit (const Nothing) t == pure t` and `visit (const (Just (pure t2))) t == pure t2`

visit' :: (Traversable f, Monad g, Ord v) => (f (Term f v a) -> g (f (Term f v a))) -> Term f v a -> g (Term f v a) #

Apply an effectful function to an ABT tree top down, sequencing the results.

visit_ :: (Traversable f, Applicative g, Ord v) => (f (Term f v a) -> g ()) -> Term f v a -> g (Term f v a) #

Apply an effectful function to an ABT tree top down, sequencing the results.

visitPure :: forall (f :: Type -> Type) v a. (Traversable f, Ord v) => (Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a #

visit specialized to the Identity effect.

changeVars :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => Map v v -> Term f v a -> Term f v a Source #

allVars :: forall (f :: Type -> Type) v a. Foldable f => Term f v a -> [v] #

numberedFreeVars :: forall v (f :: Type -> Type) a. (Ord v, Foldable f) => Term f v a -> Map v Int Source #

subterms :: forall v (f :: Type -> Type) a. (Ord v, Traversable f) => Term f v a -> [Term f v a] #

annotateBound :: forall v (f :: Type -> Type) a. (Ord v, Foldable f, Functor f) => Term f v a -> Term f v (a, Set v) Source #

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 Source #

rebuildMaybeUp :: forall v (f :: Type -> Type) 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) Source #

rebuildUp' :: forall v (f :: Type -> Type) a. (Ord v, Foldable f, Functor f) => (Term f v a -> Term f v a) -> Term f v a -> Term f v a Source #

reannotateUp :: forall v (f :: Type -> Type) b a. (Ord v, Foldable f, Functor f, Monoid b) => (Term f v a -> b) -> Term f v a -> Term f v (a, b) Source #

rewriteDown :: forall (f :: Type -> Type) v a. (Traversable f, Ord v) => (Term f v a -> Term f v a) -> Term f v a -> Term f v a Source #

transform :: (Ord v, Foldable g, Functor g) => (forall a1. f a1 -> g a1) -> Term f v a -> Term g v a #

transformM :: (Ord v, Monad m, Traversable g) => (forall a1. f a1 -> m (g a1)) -> Term f v a -> m (Term g v a) #

foreachSubterm :: forall (f :: Type -> Type) g v a b. (Traversable f, Applicative g) => (Term f v a -> g b) -> Term f v a -> g [b] #

freeVarOccurrences :: forall (f :: Type -> Type) v a. (Traversable f, Ord v) => Set v -> Term f v a -> [(v, a)] Source #

isFreeIn :: forall v (f :: Type -> Type) a. Ord v => v -> Term f v a -> Bool Source #

True if v is a member of the set of free variables of t

occurrences :: forall (f :: Type -> Type) v a. (Foldable f, Var v) => v -> Term f v a -> Int Source #

extraMap :: Functor g => (forall k. f k -> g k) -> Term f v a -> Term g v a Source #

vmap :: forall (f :: Type -> Type) v' v a. (Functor f, Foldable f, Ord v') => (v -> v') -> Term f v a -> Term f v' a #

vmapM :: forall m (f :: Type -> Type) v2 v a. (Applicative m, Traversable f, Foldable f, Ord v2) => (v -> m v2) -> Term f v a -> m (Term f v2 a) #

amap :: forall (f :: Type -> Type) v a a2. (Functor f, Foldable f, Ord v) => (a -> a2) -> Term f v a -> Term f v a2 Source #

rename :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => v -> v -> Term f v a -> Term f v a #

renames old to new in the given term, ignoring subtrees that bind old

renames :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => Map v v -> Term f v a -> Term f v a Source #

subst :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => v -> Term f v a -> Term f v a -> Term f v a Source #

`subst v e body` substitutes e for v in body, avoiding capture by renaming abstractions in body

substs :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => [(v, Term f v a)] -> Term f v a -> Term f v a Source #

`substs [(t1,v1), (t2,v2), ...] body` performs multiple simultaneous substitutions, avoiding capture

substInheritAnnotation :: forall (f :: Type -> Type) v b a. (Foldable f, Functor f, Var v) => v -> Term f v b -> Term f v a -> Term f v a #

substsInheritAnnotation :: forall (f :: Type -> Type) v b a. (Foldable f, Functor f, Var v) => [(v, Term f v b)] -> Term f v a -> Term f v a #

Substitutes the replacements in order, with substInheritAnnotation's semantics for each: the result is what substituting them one at a time, first to last, gives. So a variable free in a replacement is replaced by the substitutions after it in the list, and of two replacements for the same variable the first takes the term's occurrences and the second reaches only the occurrences inside the first's replacement. The term is traversed once, not once per replacement: with thousands of replacements, as when the names of a wide expression are bound, one traversal per replacement rebuilt the path to each occurrence (and its free-variable sets) thousands of times over.

The one-at-a-time result is reproduced up to the names of binders: a binder is renamed when it could capture a variable free in any replacement, where the one-at-a-time form renames it only for the replacements that reach its body, and the fresh name need not be the same. The two results are alpha-equivalent.

find :: forall v (f :: Type -> Type) a x. (Ord v, Foldable f, Functor f) => (Term f v a -> FindAction x) -> Term f v a -> [x] Source #

find' :: forall v (f :: Type -> Type) a. (Ord v, Foldable f, Functor f) => (Term f v a -> Bool) -> Term f v a -> [Term f v a] Source #

data FindAction x Source #

Constructors

Found x
Prune
Continue

Instances

Instances details

Functor FindAction Source #
Instance details Defined in Unison.ABT Methods fmap :: (a -> b) -> FindAction a -> FindAction b # (<$) :: a -> FindAction b -> FindAction a #
Show x => Show (FindAction x) Source #
Instance details Defined in Unison.ABT Methods showsPrec :: Int -> FindAction x -> ShowS # show :: FindAction x -> String # showList :: [FindAction x] -> ShowS #

containsExpression :: forall (f :: Type -> Type) v a. (Var v, forall a1. Eq a1 => Eq (f a1), Traversable f) => Term f v a -> Term f v a -> Bool Source #

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.

rewriteExpression :: forall (f :: Type -> Type) v a. (Var v, Show v, forall a1. Eq a1 => Eq (f a1), forall a1. Show a1 => Show (f a1), Traversable f) => Term f v a -> Term f v a -> Term f v a -> Maybe (Term f v a) Source #

Core logic of structured find and replace. Works for any base functor. Returns Nothing if no replacements.

Optics

baseFunctor_ :: Applicative m => (f (Term f v a) -> m (f (Term f v a))) -> Term f v a -> m (Term f v a) Source #

rewriteDown_ :: forall (f :: Type -> Type) 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) Source #

Setter' (Term f v a) (Term f v a)

Safe Term constructors & Patterns

annotate :: forall a (f :: Type -> Type) v. a -> Term f v a -> Term f v a Source #

Replace the annotation with the given argument.

annotatedVar :: forall a v (f :: Type -> Type). a -> v -> Term f v a Source #

var :: forall v (f :: Type -> Type). v -> Term f v () Source #

tm :: (Foldable f, Ord v) => f (Term f v ()) -> Term f v () Source #

tm' :: (Foldable f, Ord v) => a -> f (Term f v a) -> Term f v a Source #

abs :: forall v (f :: Type -> Type). Ord v => v -> Term f v () -> Term f v () Source #

absChain :: forall v (f :: Type -> Type). Ord v => [v] -> Term f v () -> Term f v () Source #

absChain' :: forall v a (f :: Type -> Type). Ord v => [(a, v)] -> Term f v a -> Term f v a Source #

abs' :: forall v a (f :: Type -> Type). Ord v => a -> v -> Term f v a -> Term f v a Source #

absr :: forall (f :: Type -> Type) v. (Functor f, Foldable f, Var v) => v -> Term f (V v) () -> Term f (V v) () Source #

unabs :: forall (f :: Type -> Type) v a. Term f v a -> ([v], Term f v a) #

unabsA :: forall (f :: Type -> Type) v a. Term f v a -> ([(a, v)], Term f v a) Source #

dropAbs :: forall (f :: Type -> Type) v a. Int -> Term f v a -> Term f v a Source #

cycle :: forall (f :: Type -> Type) v. Term f v () -> Term f v () Source #

cycle' :: forall a (f :: Type -> Type) v. a -> Term f v a -> Term f v a Source #

cycler :: forall (f :: Type -> Type) v. (Functor f, Foldable f, Var v) => [v] -> Term f (V v) () -> Term f (V v) () Source #

pattern Abs' :: (Foldable f, Functor f, Var v) => a -> Subst f v a -> Term f v a Source #

pattern Abs'' :: v -> Term f v a -> Term f v a Source #

pattern AbsN' :: [v] -> Term f v a -> Term f v a #

pattern AbsNA' :: [(a, v)] -> Term f v a -> Term f v a Source #

pattern Var' :: v -> Term f v a #

pattern Cycle' :: [v] -> f (Term f v a) -> Term f v a Source #

pattern Cycle'' :: Term f v a -> Term f v a Source #

pattern CycleA' :: a -> [(a, v)] -> Term f v a -> Term f v a Source #

pattern Tm' :: f (Term f v a) -> Term f v a #

Algorithms

components :: forall v (f :: Type -> Type) a. Var v => [(v, Term f v a)] -> [[(v, Term f v a)]] Source #

orderedComponents :: forall v (f :: Type -> Type) a. Var v => [(v, Term f v a)] -> [[(v, Term f v a)]] Source #