- (<>) :: Monoid m => m -> m -> m
- rR1 :: forall ctx[a5EE] a[a1FY]. Rep a[a1FY] => R1 ctx[a5EE] (R a[a1FY])
- rR :: forall a[a1FY]. Rep a[a1FY] => R (R a[a1FY])
- data Bind a b = B a b
- newtype Embed a = Embed a
- newtype Shift a = Shift a
- data Rebind a b = R a (Bind [AnyName] b)
- data Rec a = Rec a
- rBind1 :: forall ctx[a5QY] a[a5FT] b[a5FU]. (Rep a[a5FT], Rep b[a5FU]) => ctx[a5QY] a[a5FT] -> ctx[a5QY] b[a5FU] -> R1 ctx[a5QY] (Bind a[a5FT] b[a5FU])
- rBind :: forall a[a5FT] b[a5FU]. (Rep a[a5FT], Rep b[a5FU]) => R (Bind a[a5FT] b[a5FU])
- rName1 :: forall ctx[a5QL] a[a1Ev]. Rep a[a1Ev] => ctx[a5QL] (R a[a1Ev]) -> ctx[a5QL] (String, Integer) -> R1 ctx[a5QL] (Name a[a1Ev])
- rName :: forall a[a1Ev]. Rep a[a1Ev] => R (Name a[a1Ev])
- rEmbed1 :: forall ctx[a5QD] a[a5FS]. Rep a[a5FS] => ctx[a5QD] a[a5FS] -> R1 ctx[a5QD] (Embed a[a5FS])
- rEmbed :: forall a[a5FS]. Rep a[a5FS] => R (Embed a[a5FS])
- rRebind1 :: forall ctx[a5Qq] a[a5FP] b[a5FQ]. (Rep a[a5FP], Rep b[a5FQ]) => ctx[a5Qq] a[a5FP] -> ctx[a5Qq] (Bind [AnyName] b[a5FQ]) -> R1 ctx[a5Qq] (Rebind a[a5FP] b[a5FQ])
- rRebind :: forall a[a5FP] b[a5FQ]. (Rep a[a5FP], Rep b[a5FQ]) => R (Rebind a[a5FP] b[a5FQ])
- rRec1 :: forall ctx[a5Qi] a[a5FO]. Rep a[a5FO] => ctx[a5Qi] a[a5FO] -> R1 ctx[a5Qi] (Rec a[a5FO])
- rRec :: forall a[a5FO]. Rep a[a5FO] => R (Rec a[a5FO])
- rShift1 :: forall ctx[a5Qa] a[a5FR]. Rep a[a5FR] => ctx[a5Qa] a[a5FR] -> R1 ctx[a5Qa] (Shift a[a5FR])
- rShift :: forall a[a5FR]. Rep a[a5FR] => R (Shift a[a5FR])
- bind :: (Alpha b, Alpha c) => b -> c -> Bind b c
- unsafeUnbind :: Bind a b -> (a, b)
- rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b
- reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)
- rec :: Alpha a => a -> Rec a
- unrec :: Alpha a => Rec a -> a
- aeq :: Alpha a => a -> a -> Bool
- fv :: (Rep b, Alpha a) => a -> Set (Name b)
- binders :: (Rep b, Alpha b) => b -> [AnyName]
- patfv :: (Rep a, Alpha b) => b -> Set (Name a)
- swaps :: Alpha a => Perm AnyName -> a -> a
- swapsBinders :: Alpha a => Perm AnyName -> a -> a
- swapsEmbeds :: Alpha a => Perm AnyName -> a -> a
- lfreshen :: Alpha a => LFresh m => a -> (a -> Perm AnyName -> m b) -> m b
- freshen :: (Fresh m, Alpha a) => a -> m (a, Perm AnyName)
- match :: Alpha a => a -> a -> Maybe (Perm AnyName)
- matchEmbeds :: Alpha a => a -> a -> Maybe (Perm AnyName)
- matchBinders :: Alpha a => a -> a -> Maybe (Perm AnyName)
- data AlphaCtx
- initial :: AlphaCtx
- pat :: AlphaCtx -> AlphaCtx
- term :: AlphaCtx -> AlphaCtx
- mode :: AlphaCtx -> AlphaCtx
- class Rep1 AlphaD a => Alpha a where
- aeq' :: AlphaCtx -> a -> a -> Bool
- swapall' :: AlphaCtx -> Perm AnyName -> a -> a
- swaps' :: AlphaCtx -> Perm AnyName -> a -> a
- fv' :: AlphaCtx -> a -> Set AnyName
- binders' :: AlphaCtx -> a -> [AnyName]
- match' :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)
- freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
- lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
- data AlphaD a = AlphaD {
- aeqD :: AlphaCtx -> a -> a -> Bool
- swapallD :: AlphaCtx -> Perm AnyName -> a -> a
- swapsD :: AlphaCtx -> Perm AnyName -> a -> a
- fvD :: AlphaCtx -> a -> Set AnyName
- bindersD :: AlphaCtx -> a -> [AnyName]
- matchD :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)
- freshenD :: forall m. Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
- lfreshenD :: forall b m. LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
- aeqR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Bool
- aeq1 :: MTup AlphaD l -> AlphaCtx -> l -> l -> Bool
- swapsR1 :: R1 AlphaD a -> AlphaCtx -> Perm AnyName -> a -> a
- swapallR1 :: R1 AlphaD a -> AlphaCtx -> Perm AnyName -> a -> a
- fvR1 :: R1 AlphaD a -> AlphaCtx -> a -> Set AnyName
- fv1 :: MTup AlphaD l -> AlphaCtx -> l -> Set AnyName
- bindersR1 :: R1 AlphaD a -> AlphaCtx -> a -> [AnyName]
- binders1 :: MTup AlphaD l -> AlphaCtx -> l -> [AnyName]
- matchR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)
- match1 :: MTup AlphaD l -> AlphaCtx -> l -> l -> Maybe (Perm AnyName)
- freshenR1 :: R1 AlphaD a -> Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
- freshenL :: Fresh m => MTup AlphaD l -> AlphaCtx -> l -> m (l, Perm AnyName)
- lfreshenR1 :: LFresh m => R1 AlphaD a -> AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
- lfreshenL :: LFresh m => MTup AlphaD l -> AlphaCtx -> l -> (l -> Perm AnyName -> m b) -> m b
- class Monad m => HasNext m where
- nextInteger :: m Integer
- resetNext :: Integer -> m ()
- class (Monad m, HasNext m) => Fresh m where
- unbind :: (Alpha b, Fresh m, Alpha c) => Bind b c -> m (b, c)
- unbind2 :: (Fresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))
- unbind3 :: (Fresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))
- class Monad m => LFresh m where
- lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> m (a, b)
- lunbind2 :: (LFresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))
- lunbind3 :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))
- subst :: (Alpha a, Alpha b, Subst b a) => Name b -> b -> a -> a
- substs :: (Alpha a, Alpha b, Subst b a) => [Name b] -> [b] -> a -> a
- class Rep1 (SubstD b) a => Subst b a where
- data SubstD b a = SubstD {}
- substR1 :: LFresh m => R1 (SubstD b) a -> Name b -> b -> a -> m a
- substsR1 :: LFresh m => R1 (SubstD b) a -> [Name b] -> [b] -> a -> m a
- data Exp
- rExp1 :: forall ctx[a6TR]. ctx[a6TR] (Name Exp) -> ctx[a6TR] Exp -> ctx[a6TR] (Bind (Name Exp) Exp) -> R1 ctx[a6TR] Exp
- rExp :: R Exp
- nameB :: Name Exp
- nameC :: Name Exp
- nameA :: Name Exp
- assert :: String -> Bool -> IO ()
- do_tests :: ()
- emptyNE :: Set (Name Exp)
- mkbig :: [Name Exp] -> Exp -> Exp
Documentation
Type of a binding. Morally, the type a should be in the
class Pattern
and the type b should be in the class Alpha
.
The Pattern class contains the constructor and a safe
destructor for these types.
We can Bind an a object in a b object if we
can create fresh a objects, and Names can be
swapped in b objects. Often a is Name
but that need not be the case.
B a b |
(Rep a[a5FT], Rep b[a5FU], Sat (ctx[a5QY] a[a5FT]), Sat (ctx[a5QY] b[a5FU])) => Rep1 ctx[a5QY] (Bind a[a5FT] b[a5FU]) | |
(Subst c a, Alpha a, Subst c b, Alpha b) => Subst c (Bind a b) | |
(Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) | |
(Show a, Show b) => Show (Bind a b) | |
(Rep a[a5FT], Rep b[a5FU]) => Rep (Bind a[a5FT] b[a5FU]) | |
(Alpha a, Alpha b) => Alpha (Bind a b) |
An annotation is a hole
in a pattern where variables
can be used, but not bound. For example patterns may include
type annotations, and those annotations can reference variables
without binding them.
Annotations do nothing special when they appear elsewhere in terms
Embed a |
Shift the scope of an embedded term one level outwards.
Shift a |
Rebinding is for telescopes --- i.e. to support patterns that also bind variables that appear later
(Rep a[a5FP], Rep b[a5FQ], Sat (ctx[a5Qq] a[a5FP]), Sat (ctx[a5Qq] (Bind [AnyName] b[a5FQ]))) => Rep1 ctx[a5Qq] (Rebind a[a5FP] b[a5FQ]) | |
(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b) | |
(Alpha a, Show a, Show b) => Show (Rebind a b) | |
(Rep a[a5FP], Rep b[a5FQ]) => Rep (Rebind a[a5FP] b[a5FQ]) | |
(Alpha a, Alpha b) => Alpha (Rebind a b) |
Rec
supports recursive patterns --- that is, patterns where
any variables anywhere in the pattern are bound in the pattern
itself. Useful for lectrec (and Agda's dot notation).
Rec a |
rBind1 :: forall ctx[a5QY] a[a5FT] b[a5FU]. (Rep a[a5FT], Rep b[a5FU]) => ctx[a5QY] a[a5FT] -> ctx[a5QY] b[a5FU] -> R1 ctx[a5QY] (Bind a[a5FT] b[a5FU])Source
rName1 :: forall ctx[a5QL] a[a1Ev]. Rep a[a1Ev] => ctx[a5QL] (R a[a1Ev]) -> ctx[a5QL] (String, Integer) -> R1 ctx[a5QL] (Name a[a1Ev])Source
rEmbed1 :: forall ctx[a5QD] a[a5FS]. Rep a[a5FS] => ctx[a5QD] a[a5FS] -> R1 ctx[a5QD] (Embed a[a5FS])Source
rRebind1 :: forall ctx[a5Qq] a[a5FP] b[a5FQ]. (Rep a[a5FP], Rep b[a5FQ]) => ctx[a5Qq] a[a5FP] -> ctx[a5Qq] (Bind [AnyName] b[a5FQ]) -> R1 ctx[a5Qq] (Rebind a[a5FP] b[a5FQ])Source
rRec1 :: forall ctx[a5Qi] a[a5FO]. Rep a[a5FO] => ctx[a5Qi] a[a5FO] -> R1 ctx[a5Qi] (Rec a[a5FO])Source
rShift1 :: forall ctx[a5Qa] a[a5FR]. Rep a[a5FR] => ctx[a5Qa] a[a5FR] -> R1 ctx[a5Qa] (Shift a[a5FR])Source
unsafeUnbind :: Bind a b -> (a, b)Source
A destructor for binders that does not guarantee fresh names for the binders.
reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)Source
destructor for binding patterns, the external names should have already been freshen'ed. We swap the internal names so that they use the external names
patfv :: (Rep a, Alpha b) => b -> Set (Name a)Source
Set of variables that occur freely in annotations (not binding)
swaps :: Alpha a => Perm AnyName -> a -> aSource
The method swaps applys a permutation to all free variables in the term.
swapsBinders :: Alpha a => Perm AnyName -> a -> aSource
Apply a permutation to the binding variables in a pattern. Embedded terms are left alone by the permutation.
swapsEmbeds :: Alpha a => Perm AnyName -> a -> aSource
Apply a permutation to the annotations in a pattern. Binding names are left alone by the permutation.
lfreshen :: Alpha a => LFresh m => a -> (a -> Perm AnyName -> m b) -> m bSource
Locally freshen an object
match :: Alpha a => a -> a -> Maybe (Perm AnyName)Source
Match compares two data structures and produces a permutation of their Names that will make them alpha-equivalent to eachother. (Names that appear in annotations must match exactly.) Also note that two terms are alpha-equivalent when the empty permutation is returned.
matchEmbeds :: Alpha a => a -> a -> Maybe (Perm AnyName)Source
Compare two patterns, ignoring the names of binders, and produce
a permutation of their annotations to make them alpha-equivalent
to eachother. Return Nothing
if no such renaming is possible.
class Rep1 AlphaD a => Alpha a whereSource
The Alpha class is for all terms that may contain binders
The Rep1
class constraint means that we can only
make instances of this class for types that have
generic representations. (Derive these using TH and
RepLib.)
aeq' :: AlphaCtx -> a -> a -> BoolSource
swapall' :: AlphaCtx -> Perm AnyName -> a -> aSource
swap everything, including bound and free variables, parts in annots, etc.
swaps' :: AlphaCtx -> Perm AnyName -> a -> aSource
The method swaps' applys a compound permutation
fv' :: AlphaCtx -> a -> Set AnyNameSource
calculate the free variables (aka support)
binders' :: AlphaCtx -> a -> [AnyName]Source
list the binding variables in a pattern, in order
match' :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)Source
Match' compares two data structures and produces a permutation of their free variables that will make them alpha-equivalent to eachother.
freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)Source
An object of type a can be freshened if a new copy of a can be produced where all old Names in a are replaced with new fresh Names, and the permutation reports which names were swapped by others.
lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m bSource
See lfreshen
Alpha Bool | |
Alpha Char | |
Alpha Double | |
Alpha Float | |
Alpha Int | |
Alpha Integer | |
Alpha () | |
Alpha AnyName | |
Alpha Exp | |
Alpha a => Alpha [a] | |
Rep a => Alpha (R a) | |
Alpha a => Alpha (Maybe a) | |
Rep a => Alpha (Name a) | |
(Eq a, Alpha a) => Alpha (Embed a) | |
(Alpha a, Alpha b) => Alpha (Either a b) | |
(Alpha a, Alpha b) => Alpha (a, b) | |
(Alpha a, Alpha b) => Alpha (Rebind a b) | |
(Alpha a, Alpha b) => Alpha (Bind a b) | |
(Alpha a, Alpha b, Alpha c) => Alpha (a, b, c) | |
(Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) | |
(Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e) |
AlphaD | |
|
class Monad m => HasNext m whereSource
A monad m supports the nextInteger operation if it can generate new fresh integers
unbind :: (Alpha b, Fresh m, Alpha c) => Bind b c -> m (b, c)Source
Unbind is the destructor of a binding. It ensures that the names in the binding b are fresh.
unbind2 :: (Fresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))Source
Destruct two bindings simultanously, if they match, using the same list of fresh names
unbind3 :: (Fresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))Source
class Monad m => LFresh m whereSource
Locally fresh monad This is the class of monads that support freshness in an (implicit) local scope. Names drawn are fresh for this particular scope, but not globally fresh. This class has a basic instance based on the reader monad.
lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> m (a, b)Source
Destruct a binding in the LFresh monad.
lunbind2 :: (LFresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))Source
lunbind3 :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))Source
subst :: (Alpha a, Alpha b, Subst b a) => Name b -> b -> a -> aSource
Capture-avoiding substitution, in a monad so that we can rename variables at binding locations and avoid capture
class Rep1 (SubstD b) a => Subst b a whereSource
Subst b Double | |
Subst b Float | |
Subst b Integer | |
Subst b Char | |
Subst b () | |
Subst b Bool | |
Subst b Int | |
Subst c AnyName | |
Subst Exp Exp | |
Subst c a => Subst c (Embed a) | |
Rep a => Subst b (Name a) | |
Rep a => Subst b (R a) | |
Subst c a => Subst c (Maybe a) | |
Subst c a => Subst c [a] | |
(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b) | |
(Subst c a, Alpha a, Subst c b, Alpha b) => Subst c (Bind a b) | |
(Subst c a, Subst c b) => Subst c (Either a b) | |
(Subst c a, Subst c b) => Subst c (a, b) | |
(Subst c a, Subst c b, Subst c d) => Subst c (a, b, d) | |
(Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e) | |
(Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f) |