Safe Haskell	Safe-Inferred
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 v a = Subst {
- freshen :: forall m 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 :: 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 :: (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 :: (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 :: (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 :: (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 :: (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 :: (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' :: (Ord v, Foldable f, Functor f) => (Term f v a -> Term f v a) -> Term f v a -> Term f v a
reannotateUp :: (Ord v, Foldable f, Functor f, Monoid b) => (Term f v a -> b) -> Term f v a -> Term f v (a, b)
rewriteDown :: (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 :: (Traversable f, Ord v) => Set v -> Term f v a -> [(v, a)]
isFreeIn :: Ord v => v -> Term f v a -> Bool
occurrences :: (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 :: (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 :: (Foldable f, Functor f, Var v) => Map v v -> Term f v a -> Term f v a
subst :: (Foldable f, Functor f, Var v) => v -> Term f v a -> Term f v a -> Term f v a
substs :: (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 :: (Ord v, Foldable f, Functor f) => (Term f v a -> FindAction x) -> Term f v a -> [x]
find' :: (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 v a. (Var v, forall a. Eq a => Eq (f a), Traversable f) => Term f v a -> Term f v a -> Bool
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)
baseFunctor_ :: Applicative m => (f (Term f v a) -> m (f (Term f v a))) -> Term f v a -> m (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)
annotate :: a -> Term f v a -> Term f v a
annotatedVar :: a -> v -> Term f v a
var :: 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 :: Ord v => v -> Term f v () -> Term f v ()
absChain :: Ord v => [v] -> Term f v () -> Term f v ()
absChain' :: Ord v => [(a, v)] -> Term f v a -> Term f v a
abs' :: Ord v => a -> v -> Term f v a -> Term f v a
absr :: (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 :: Term f v a -> ([(a, v)], Term f v a)
dropAbs :: Int -> Term f v a -> Term f v a
cycle :: Term f v () -> Term f v ()
cycle' :: a -> Term f v a -> Term f v a
cycler :: (Functor f, Foldable f, Var v) => [v] -> Term f (V v) () -> Term f (V v) ()
pattern Abs' :: (Foldable f, Functor f, Var v) => 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 :: Var v => [(v, Term f v a)] -> [[(v, Term f v a)]]
orderedComponents :: 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

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) #
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 #
Generic (ABT f v r)
Instance details Defined in U.Core.ABT Associated Types type Rep (ABT f v r) :: Type -> Type # 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-7TTEaGpY3e79hYDTKjX5dL" '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

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) #
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 #
Generic (Term f v a)
Instance details Defined in U.Core.ABT Associated Types type Rep (Term f v a) :: Type -> Type # 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-7TTEaGpY3e79hYDTKjX5dL" '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 v a Source #

Constructors

Subst
Fields freshen :: forall m 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 :: 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 :: (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 :: (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 :: (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 :: (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 :: (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 :: (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' :: (Ord v, Foldable f, Functor f) => (Term f v a -> Term f v a) -> Term f v a -> Term f v a Source #

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

rewriteDown :: (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 :: (Traversable f, Ord v) => Set v -> Term f v a -> [(v, a)] Source #

isFreeIn :: Ord v => v -> Term f v a -> Bool Source #

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

occurrences :: (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 :: (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 :: (Foldable f, Functor f, Var v) => Map v v -> Term f v a -> Term f v a Source #

subst :: (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 :: (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 #

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

find' :: (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 v a. (Var v, forall a. Eq a => Eq (f a), 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 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) 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_ :: (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 :: a -> Term f v a -> Term f v a Source #

Replace the annotation with the given argument.

annotatedVar :: a -> v -> Term f v a Source #

var :: 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 :: Ord v => v -> Term f v () -> Term f v () Source #

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

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

abs' :: Ord v => a -> v -> Term f v a -> Term f v a Source #

absr :: (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 :: Term f v a -> ([(a, v)], Term f v a) Source #

dropAbs :: Int -> Term f v a -> Term f v a Source #

cycle :: Term f v () -> Term f v () Source #

cycle' :: a -> Term f v a -> Term f v a Source #

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

pattern Abs' :: (Foldable f, Functor f, Var v) => 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 :: Var v => [(v, Term f v a)] -> [[(v, Term f v a)]] Source #

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