Copyright | (c) 2014 Edwin Westbrook Nicolas Frisby and Paul Brauner |
---|---|

License | BSD3 |

Maintainer | westbrook@kestrel.edu |

Stability | experimental |

Portability | GHC |

Safe Haskell | None |

Language | Haskell98 |

This module defines the typeclass

, which allows
pattern-matching on the bodies of multi-bindings when their bodies
have type a. To ensure adequacy, the actual machinery of how this
works is hidden from the user, but, for any given (G)ADT `NuMatching`

a`a`

, the
user can use the Template Haskell function `mkNuMatching`

to
create a `NuMatching`

instance for `a`

.

- class NuMatching a where
- mkNuMatching :: Q Type -> Q [Dec]
- class NuMatchingList args where
- class NuMatching1 f where
- data MbTypeRepr a
- isoMbTypeRepr :: NuMatching b => (a -> b) -> (b -> a) -> MbTypeRepr a
- data NuMatchingObj a = NuMatching a => NuMatchingObj ()

# Documentation

class NuMatching a where Source #

Instances of the

class allow pattern-matching on
multi-bindings whose bodies have type `NuMatching`

a`a`

, i.e., on multi-bindings
of type

. The structure of this class is mostly hidden
from the user; see `Mb`

ctx a`mkNuMatching`

to see how to create instances
of the `NuMatching`

class.

nuMatchingProof :: MbTypeRepr a Source #

NuMatching Bool Source # | |

NuMatching Char Source # | |

NuMatching Int Source # | |

NuMatching Integer Source # | |

NuMatching () Source # | |

NuMatching a => NuMatching [a] Source # | |

NuMatching a => NuMatching (Maybe a) Source # | |

NuMatching (Name a) Source # | |

NuMatching (Closed a) Source # | |

NuMatching (Term a0) Source # | |

NuMatching (Decls a0) Source # | |

NuMatching (Decl a0) Source # | |

NuMatching (DTerm a0) Source # | |

(NuMatching a, NuMatching b) => NuMatching (a -> b) Source # | |

(NuMatching a, NuMatching b) => NuMatching (Either a b) Source # | |

(NuMatching a, NuMatching b) => NuMatching (a, b) Source # | |

(NuMatching1 f, NuMatchingList ctx) => NuMatching (MapRList f ctx) Source # | |

NuMatching (Member c a) Source # | |

NuMatching a => NuMatching (Mb ctx a) Source # | |

(NuMatching a, NuMatching b, NuMatching c) => NuMatching (a, b, c) Source # | |

(NuMatching a, NuMatching b, NuMatching c, NuMatching d) => NuMatching (a, b, c, d) Source # | |

mkNuMatching :: Q Type -> Q [Dec] Source #

Template Haskell function for creating NuMatching instances for (G)ADTs.
Typical usage is to include the following line in the source file for
(G)ADT `T`

(here assumed to have two type arguments):

$(mkNuMatching [t| forall a b . T a b |])

The `mkNuMatching`

call here will create an instance declaration for

. It is also possible to include a context in the
forall type; for example, if we define the `NuMatching`

(T a b)`ID`

data type as follows:

data ID a = ID a

then we can create a `NuMatching`

instance for it like this:

$( mkNuMatching [t| NuMatching a => ID a |])

Note that, when a context is included, the Haskell parser will add
the `forall a`

for you.

class NuMatchingList args where Source #

nuMatchingListProof :: MapRList NuMatchingObj args Source #

NuMatchingList (RNil *) Source # | |

(NuMatchingList args, NuMatching a) => NuMatchingList ((:>) * args a) Source # | |

class NuMatching1 f where Source #

nuMatchingProof1 :: NuMatching a => NuMatchingObj (f a) Source #

data MbTypeRepr a Source #

This type states that it is possible to replace free names with
fresh names in an object of type `a`

. This type essentially just
captures a representation of the type a as either a Name type, a
multi-binding, a function type, or a (G)ADT. In order to be sure
that only the "right" proofs are used for (G)ADTs, however, this
type is hidden from the user, and can only be constructed with
`mkNuMatching`

.

isoMbTypeRepr :: NuMatching b => (a -> b) -> (b -> a) -> MbTypeRepr a Source #

Build an `MbTypeRepr`

for type `a`

by using an isomorphism with an
already-representable type `b`

. This is useful for building `NuMatching`

instances for, e.g., `Integral`

types, by mapping to and from `Integer`

,
without having to define instances for each one in this module.

data NuMatchingObj a Source #

NuMatching a => NuMatchingObj () |