Safe Haskell	None
Language	Haskell2010

U.Core.ABT

Contents

Traversals
Patterns

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
}
amap :: forall (f :: Type -> Type) a a' v. Functor f => (a -> a') -> Term f v a -> Term f 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)
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)
abs :: forall v a (f :: Type -> Type). Ord v => a -> v -> Term f v a -> Term f v a
var :: forall a v (f :: Type -> Type). a -> v -> Term f v a
cycle :: forall a (f :: Type -> Type) v. a -> Term f v a -> Term f v a
tm :: (Foldable f, Ord v) => a -> f (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
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]
subterms :: forall v (f :: Type -> Type) a. (Ord v, Traversable f) => Term f v a -> [Term f v a]
pattern Var' :: v -> Term f v a
pattern Cycle' :: [v] -> Term f v a -> Term f v a
pattern AbsN' :: [v] -> Term f v a -> Term f v a
pattern Tm' :: f (Term f v a) -> Term f v a
unabs :: forall (f :: Type -> Type) v a. Term f v a -> ([v], Term f v a)
freshInBoth :: forall v (f :: Type -> Type) a. Var v => Term f v a -> Term f v a -> v -> v
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
substsMapInheritAnnotation :: forall (f :: Type -> Type) v a b. (Foldable f, Functor f, Var v) => Map v (Term f v b) -> 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
subst' :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => (a -> Term f v a) -> v -> Set v -> Term f v a -> Term f v a
rename :: forall (f :: Type -> Type) v a. (Foldable f, Functor f, Var v) => v -> v -> Term f v a -> Term f v a
allVars :: forall (f :: Type -> Type) v a. Foldable f => Term f v a -> [v]
freshenS :: (Var v, MonadState (Set v) m) => v -> m v
freshenS' :: (Var v, MonadState s m) => Lens' s (Set v) -> v -> m v

Documentation

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

Constructors

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

Instances

Instances details

Functor f => Functor (ABT f v) Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Constructors

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

Instances

Instances details

Functor f => Functor (Term' f v a) Source #
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) Source #
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 #

amap :: forall (f :: Type -> Type) a a' v. Functor f => (a -> a') -> Term f v a -> Term f 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 Source #

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

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

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

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

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

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

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

Traversals

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

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

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

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

visit specialized to the Identity effect.

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

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

Patterns

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

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

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

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

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

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

Produce a variable which is free in both terms

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

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.

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

Substitutes every variable in the map at once, avoiding capture; the annotation of each replacement is inherited from the variable it replaces. This is subst' with a map of variables in place of its one variable: the key set in place of v, and the free variables of all the replacements in place of r. The key set travels with the map because every node tests its free variables against it, and keysSet is linear.

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

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

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

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

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

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

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

freshenS' :: (Var v, MonadState s m) => Lens' s (Set v) -> v -> m v Source #

A more general version of freshenS that uses a lens to focus on used variables inside state.