unison-core1-0.0.0
Safe HaskellNone
LanguageHaskell2010

Unison.ABT.Normalized

Documentation

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

Constructors

Abs v (Term f v) 
Tm (f v (Term f v)) 

Instances

Instances details
(forall a b. (Show a, Show b) => Show (f a b), Show v) => Show (ABT f v) Source # 
Instance details

Defined in Unison.ABT.Normalized

Methods

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

show :: ABT f v -> String #

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

(forall a b. (Eq a, Eq b) => Eq (f a b), Bifunctor f, Bifoldable f, Var v) => Eq (ABT f v) Source # 
Instance details

Defined in Unison.ABT.Normalized

Methods

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

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

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

Constructors

Term 

Fields

Bundled Patterns

pattern TAbs :: Var v => v -> Term f v -> Term f v 
pattern TTm :: (Var v, Bifoldable f) => f v (Term f v) -> Term f v 
pattern TAbss :: Var v => [v] -> Term f v -> Term f v 

Instances

Instances details
(forall a b. (Show a, Show b) => Show (f a b), Show v) => Show (Term f v) Source # 
Instance details

Defined in Unison.ABT.Normalized

Methods

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

show :: Term f v -> String #

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

(forall a b. (Eq a, Eq b) => Eq (f a b), Bifunctor f, Bifoldable f, Var v) => Eq (Term f v) Source # 
Instance details

Defined in Unison.ABT.Normalized

Methods

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

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

class (Bifoldable f, Bifunctor f) => Align (f :: Type -> Type -> Type) where Source #

Methods

align :: Applicative g => (vl -> vr -> g vs) -> (el -> er -> g es) -> f vl el -> f vr er -> Maybe (g (f vs es)) Source #

alpha :: forall (f :: Type -> Type -> Type) v. (Align f, Var v) => Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) () Source #

freshen :: forall v (f :: Type -> Type -> Type). (Var v, Bifunctor f, Bifoldable f) => Set v -> Term f v -> Term f v Source #

data Renaming v Source #

Constructors

RN 

Fields

isEmptyRenaming :: Renaming v -> Bool Source #

freshenBinder :: Var v => Set v -> Renaming v -> v -> (Renaming v, v) Source #

freshenBinders :: Var v => Set v -> Renaming v -> [v] -> (Renaming v, [v]) Source #

pruneRenaming :: Var v => Set v -> Renaming v -> Renaming v Source #

renameVar :: Var v => Renaming v -> v -> v Source #

mapping :: Var v => Map v v -> Renaming v Source #

avoiding :: Set v -> Renaming v Source #

mappingAndAvoiding :: Var v => Map v v -> Set v -> Renaming v Source #

renames :: forall v (f :: Type -> Type -> Type). (Var v, Bifunctor f, Bifoldable f) => Map v v -> Term f v -> Term f v Source #

renamesAvoiding :: forall v (f :: Type -> Type -> Type). (Var v, Bifunctor f, Bifoldable f) => Set v -> Map v v -> Term f v -> Term f v Source #

renamesAndFreshen0 :: forall v (f :: Type -> Type -> Type). (Var v, Bifunctor f, Bifoldable f) => Renaming v -> Term f v -> Term f v Source #

rename :: forall v (f :: Type -> Type -> Type). (Var v, Ord v, Bifunctor f, Bifoldable f) => v -> v -> Term f v -> Term f v Source #

transform :: (Var v, Bifunctor g, Bifoldable f, Bifoldable g) => (forall a b. f a b -> g a b) -> Term f v -> Term g v Source #

visit :: forall g (f :: Type -> Type -> Type) v. (Applicative g, Bifoldable f, Traversable (f v), Var v) => (Term f v -> Maybe (g (Term f v))) -> Term f v -> g (Term f v) Source #

visitPure :: forall (f :: Type -> Type -> Type) v. (Bifoldable f, Traversable (f v), Var v) => (Term f v -> Maybe (Term f v)) -> Term f v -> Term f v Source #