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
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-1VWfQyRJkVMKYBxkNy6zmW" '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-1VWfQyRJkVMKYBxkNy6zmW" '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-1VWfQyRJkVMKYBxkNy6zmW" '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-1VWfQyRJkVMKYBxkNy6zmW" '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 #

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.