hobbits-1.3.1: A library for canonically representing terms with binding
Copyright(c) 2014 Edwin Westbrook Nicolas Frisby and Paul Brauner
LicenseBSD3
Maintainerwestbrook@kestrel.edu
Stabilityexperimental
PortabilityGHC
Safe HaskellNone
LanguageHaskell2010

Data.Binding.Hobbits.NuMatching

Description

This module defines the typeclass NuMatching a, 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 a, the user can use the Template Haskell function mkNuMatching to create a NuMatching instance for a.

Synopsis

Documentation

class NuMatching a where Source #

Instances of the NuMatching a class allow pattern-matching on multi-bindings whose bodies have type a, i.e., on multi-bindings of type Mb ctx a. The structure of this class is mostly hidden from the user; see mkNuMatching to see how to create instances of the NuMatching class.

Instances

Instances details
NuMatching Bool Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Char Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Double Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Float Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Int Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Integer Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Natural Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Word Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Word8 Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Word16 Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Word32 Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching Word64 Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching () Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching a => NuMatching [a] Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching a => NuMatching (Maybe a) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatchingInstances

(Integral a, NuMatching a) => NuMatching (Ratio a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Liftable

NuMatchingAny1 f => NuMatching (f a) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching a => NuMatching (Vector a) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching (Closed a) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching (SomeName k) Source # 
Instance details

Defined in Data.Binding.Hobbits.NameSet

NuMatching (Term a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

NuMatching (Decls a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

NuMatching (Decl a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

NuMatching (DTerm a) Source # 
Instance details

Defined in Data.Binding.Hobbits.Examples.LambdaLifting.Terms

(NuMatching a, NuMatching b) => NuMatching (a -> b) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

Methods

nuMatchingProof :: MbTypeRepr (a -> b) Source #

(NuMatching a, NuMatching b) => NuMatching (Either a b) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatchingInstances

(NuMatching a, NuMatching b) => NuMatching (a, b) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching (Proxy a) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatchingInstances

NuMatching (Name a) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatchingAny1 f => NuMatching (NameAndElem f) Source # 
Instance details

Defined in Data.Binding.Hobbits.NameMap

(NuMatching a, NuMatching b, NuMatching c) => NuMatching (a, b, c) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

Methods

nuMatchingProof :: MbTypeRepr (a, b, c) Source #

NuMatching (a :~: b) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatchingInstances

NuMatching a => NuMatching (Constant a b) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatchingInstances

NuMatchingAny1 f => NuMatching (RAssign f ctx) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

NuMatching a => NuMatching (Mb ctx a) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

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

Defined in Data.Binding.Hobbits.NuMatching

Methods

nuMatchingProof :: MbTypeRepr (a, b, c, d) Source #

NuMatching (Member ctx a) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatchingInstances

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 NuMatching (T a b). It is also possible to include a context in the forall type; for example, if we define the 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.

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.

unsafeMbTypeRepr :: MbTypeRepr a Source #

Builds an MbTypeRepr proof for use in a NuMatching instance. This proof is unsafe because it does no renaming of fresh names, so should only be used for types that are guaranteed not to contain any Name or Mb values.

class NuMatchingAny1 (f :: k -> Type) where Source #

Typeclass for lifting the NuMatching constraint to functors on arbitrary kinds that do not require any constraints on their input types

Instances

Instances details
NuMatchingAny1 (Name :: k -> Type) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

Methods

nuMatchingAny1Proof :: forall (a :: k0). MbTypeRepr (Name a) Source #

NuMatching a => NuMatchingAny1 (Constant a :: k -> Type) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

Methods

nuMatchingAny1Proof :: forall (a0 :: k0). MbTypeRepr (Constant a a0) Source #

NuMatchingAny1 ((:~:) a :: k -> Type) Source # 
Instance details

Defined in Data.Binding.Hobbits.NuMatching

Methods

nuMatchingAny1Proof :: forall (a0 :: k0). MbTypeRepr (a :~: a0) Source #