diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Eugene Smolanka, Sergey Vinokurov.
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of multiple nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,7 @@
+
+invertible-grammar
+==================
+
+Framework to build invertible parsing combinator libraries.
+
+See [`sexp-grammar`](http://github.com/esmolanka/sexp-grammar).
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/invertible-grammar.cabal b/invertible-grammar.cabal
new file mode 100644
--- /dev/null
+++ b/invertible-grammar.cabal
@@ -0,0 +1,49 @@
+name:                invertible-grammar
+version:             0.1.0
+license:             BSD3
+license-file:        LICENSE
+author:              Eugene Smolanka, Sergey Vinokurov
+maintainer:          Eugene Smolanka <esmolanka@gmail.com>
+homepage:            https://github.com/esmolanka/sexp-grammar
+category:            Language
+build-type:          Simple
+extra-source-files:  README.md
+cabal-version:       >=1.10
+synopsis:
+  Invertible parsing combinators framework
+description:
+  Grammar combinator framework to build invertible parsing libraries
+  for concrete syntax.
+tested-with:   GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3
+
+source-repository head
+  type: git
+  location: https://github.com/esmolanka/invertible-grammar
+
+library
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -Wall -fno-warn-name-shadowing -fno-warn-unused-do-bind
+  exposed-modules:
+    Data.InvertibleGrammar
+    Data.InvertibleGrammar.Base
+    Data.InvertibleGrammar.Combinators
+    Data.InvertibleGrammar.Generic
+    Data.InvertibleGrammar.TH
+
+  other-modules:
+    Control.Monad.ContextError
+    Data.InvertibleGrammar.Monad
+
+  build-depends:
+      base              >=4.7   && <5.0
+    , bifunctors        >=4.2   && <5.6
+    , containers        >=0.5.5 && <0.6
+    , mtl               >=2.1   && <2.3
+    , prettyprinter     >=1     && <1.3
+    , profunctors       >=4.4   && <5.3
+    , semigroups        >=0.16  && <0.19
+    , tagged            >=0.7   && <0.9
+    , template-haskell  >=2.9   && <2.14
+    , transformers      >=0.3   && <0.6
+    , text              >=1.2   && <1.3
diff --git a/src/Control/Monad/ContextError.hs b/src/Control/Monad/ContextError.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/ContextError.hs
@@ -0,0 +1,229 @@
+{-# LANGUAGE CPP                    #-}
+{-# LANGUAGE DeriveFunctor          #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+module Control.Monad.ContextError
+  ( ContextErrorT
+  , runContextErrorT
+  , ContextError
+  , runContextError
+  , MonadContextError (..)
+  ) where
+
+#if MIN_VERSION_mtl(2,2,0)
+import Control.Monad.Except
+#else
+import Control.Monad.Error
+#endif
+
+import Control.Applicative
+import Control.Monad.Trans.Cont as Cont (ContT, liftLocal)
+import Control.Monad.Trans.Identity (IdentityT, mapIdentityT)
+import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT)
+import Control.Monad.Trans.Reader (ReaderT, mapReaderT)
+import qualified Control.Monad.Trans.RWS.Lazy as Lazy (RWST, mapRWST)
+import qualified Control.Monad.Trans.RWS.Strict as Strict (RWST, mapRWST)
+import qualified Control.Monad.Trans.State.Lazy as Lazy (StateT, mapStateT)
+import qualified Control.Monad.Trans.State.Strict as Strict (StateT, mapStateT)
+import Control.Monad.Trans.Writer.Lazy as Lazy (WriterT, mapWriterT)
+import Control.Monad.Trans.Writer.Strict as Strict (WriterT, mapWriterT)
+
+import Control.Monad.State  (MonadState (..))
+import Control.Monad.Reader (MonadReader (..))
+import Control.Monad.Writer (MonadWriter (..))
+
+import Data.Functor.Identity
+#if !MIN_VERSION_base(4,11,0)
+import Data.Semigroup
+#endif
+
+----------------------------------------------------------------------
+-- Monad
+
+newtype ContextErrorT c e m a =
+  ContextErrorT { unContextErrorT :: forall b. c -> (e -> m b) -> (c -> a -> m b) -> m b }
+
+runContextErrorT :: (Monad m) => ContextErrorT c e m a -> c -> m (Either e a)
+runContextErrorT k c = unContextErrorT k c (return . Left) (const $ return . Right)
+
+type ContextError c e a = ContextErrorT c e Identity a
+
+runContextError :: ContextError c e a -> c -> Either e a
+runContextError k c = runIdentity $ unContextErrorT k c (return . Left) (const $ return . Right)
+
+instance Functor (ContextErrorT c e m) where
+  fmap f e = ContextErrorT $ \c err ret -> unContextErrorT e c err (\c' -> ret c' . f)
+
+instance Applicative (ContextErrorT c e m) where
+  pure a = ContextErrorT $ \c _ ret -> ret c a
+  {-# INLINE pure #-}
+
+  fe <*> ae = ContextErrorT $ \c err ret ->
+    unContextErrorT fe c err (\c' f -> unContextErrorT ae c' err (\c'' -> ret c'' . f))
+  {-# INLINE (<*>) #-}
+
+instance (Semigroup e) => Alternative (ContextErrorT c e m) where
+  -- FIXME: sane 'empty' needed!
+  empty = ContextErrorT $ \_ err _ -> err (error "empty ContextErrorT")
+  {-# INLINE empty #-}
+
+  ae <|> be = ContextErrorT $ \c err ret ->
+    unContextErrorT ae c (\e -> unContextErrorT be c (\e' -> err (e <> e')) ret) ret
+  {-# INLINE (<|>) #-}
+
+instance Monad (ContextErrorT c e m) where
+  return a = ContextErrorT $ \c _ ret -> ret c a
+  {-# INLINE return #-}
+
+  ma >>= fb =
+    ContextErrorT $ \c err ret ->
+      unContextErrorT ma c err $ \c' a ->
+        unContextErrorT (fb a) c' err ret
+  {-# INLINE (>>=) #-}
+
+instance (Semigroup e) => MonadPlus (ContextErrorT c e m) where
+  mzero = empty
+  {-# INLINE mzero #-}
+
+  mplus = (<|>)
+  {-# INLINE mplus #-}
+
+instance MonadTrans (ContextErrorT c e) where
+  lift act = ContextErrorT $ \c _ ret -> act >>= ret c
+  {-# INLINE lift #-}
+
+instance MonadState s m => MonadState s (ContextErrorT c e m) where
+  get = lift get
+  put = lift . put
+  state = lift . state
+
+instance MonadWriter w m => MonadWriter w (ContextErrorT c e m) where
+  writer = lift . writer
+  tell = lift . tell
+  listen m = ContextErrorT $ \c err ret -> do
+    (res, w) <- listen (unContextErrorT m c (return . Left) (curry (return . Right)))
+    case res of
+      Left e -> err e
+      Right (c', a) -> ret c' (a, w)
+  pass m = ContextErrorT $ \c err ret -> pass $ do
+    res <- unContextErrorT m c (return . Left) (curry (return . Right))
+    case res of
+      Right (c', (a, f)) -> liftM (\b -> (b, f)) $ ret c' a
+      Left e -> liftM (\b -> (b, id)) $ err e
+
+instance MonadReader r m => MonadReader r (ContextErrorT c e m) where
+  ask = lift ask
+  local f m = ContextErrorT $ \c err ret ->
+    local f (unContextErrorT m c err ret)
+  reader = lift . reader
+
+----------------------------------------------------------------------
+-- Monad class stuff
+
+class (Monad m) => MonadContextError c e m | m -> c e where
+  throwInContext :: (c -> e) -> m a
+  askContext     :: m c
+  localContext  :: (c -> c) -> m a -> m a
+  modifyContext   :: (c -> c) -> m ()
+
+instance Monad m =>
+         MonadContextError c e (ContextErrorT c e m) where
+  throwInContext f = ContextErrorT $ \c err _ -> err (f c)
+  askContext = ContextErrorT $ \c _ ret -> ret c c
+  localContext f m = ContextErrorT $ \c err ret ->
+    unContextErrorT m (f c) err (\_ -> ret c)
+  modifyContext f = ContextErrorT $ \c _ ret -> ret (f c) ()
+
+instance MonadContextError c e m =>
+         MonadContextError c e (ContT r m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = Cont.liftLocal askContext localContext
+    modifyContext = lift . modifyContext
+
+#if MIN_VERSION_mtl(2, 2, 0)
+
+instance MonadContextError c e m =>
+         MonadContextError c e (ExceptT e m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = mapExceptT . localContext
+    modifyContext = lift . modifyContext
+
+#else
+
+instance (Error e', MonadContextError c e m) =>
+         MonadContextError c e (ErrorT e' m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = mapErrorT . localContext
+    modifyContext = lift . modifyContext
+
+#endif
+
+instance MonadContextError c e m =>
+         MonadContextError c e (IdentityT m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = mapIdentityT . localContext
+    modifyContext = lift . modifyContext
+
+instance MonadContextError c e m =>
+         MonadContextError c e (MaybeT m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = mapMaybeT . localContext
+    modifyContext = lift . modifyContext
+
+instance MonadContextError c e m =>
+         MonadContextError c e (ReaderT r m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = mapReaderT . localContext
+    modifyContext = lift . modifyContext
+
+instance (Monoid w, MonadContextError c e m) =>
+         MonadContextError c e (Lazy.WriterT w m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = Lazy.mapWriterT . localContext
+    modifyContext = lift . modifyContext
+
+instance (Monoid w, MonadContextError c e m) =>
+         MonadContextError c e (Strict.WriterT w m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = Strict.mapWriterT . localContext
+    modifyContext = lift . modifyContext
+
+instance MonadContextError c e m =>
+         MonadContextError c e (Lazy.StateT s m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = Lazy.mapStateT . localContext
+    modifyContext = lift . modifyContext
+
+instance MonadContextError c e m =>
+         MonadContextError c e (Strict.StateT s m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = Strict.mapStateT . localContext
+    modifyContext = lift . modifyContext
+
+instance (Monoid w, MonadContextError c e m) =>
+         MonadContextError c e (Lazy.RWST r w s m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = Lazy.mapRWST . localContext
+    modifyContext = lift . modifyContext
+
+instance (Monoid w, MonadContextError c e m) =>
+         MonadContextError c e (Strict.RWST r w s m) where
+    throwInContext = lift . throwInContext
+    askContext = lift askContext
+    localContext = Strict.mapRWST . localContext
+    modifyContext = lift . modifyContext
diff --git a/src/Data/InvertibleGrammar.hs b/src/Data/InvertibleGrammar.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/InvertibleGrammar.hs
@@ -0,0 +1,18 @@
+module Data.InvertibleGrammar
+  ( -- * Base
+    Grammar, (:-), forward, backward
+    -- * Combinators
+  , module Data.InvertibleGrammar.Combinators
+    -- * Running grammars
+  , runGrammar
+  , runGrammarDoc
+  , runGrammarString
+  -- ** Error messages
+  , ErrorMessage(..)
+  , ContextError, Propagation , GrammarError
+  , Mismatch, expected, unexpected
+  ) where
+
+import Data.InvertibleGrammar.Base
+import Data.InvertibleGrammar.Combinators
+import Data.InvertibleGrammar.Monad
diff --git a/src/Data/InvertibleGrammar/Base.hs b/src/Data/InvertibleGrammar/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/InvertibleGrammar/Base.hs
@@ -0,0 +1,181 @@
+{-# LANGUAGE CPP                   #-}
+{-# LANGUAGE DeriveFoldable        #-}
+{-# LANGUAGE DeriveFunctor         #-}
+{-# LANGUAGE DeriveTraversable     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE TypeOperators         #-}
+
+module Data.InvertibleGrammar.Base
+  ( Grammar (..)
+  , (:-) (..)
+  , forward
+  , backward
+  , GrammarError (..)
+  , Mismatch
+  , expected
+  , unexpected
+  ) where
+
+import Prelude hiding ((.), id)
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+import Control.Category
+import Control.Monad
+import Data.Text (Text)
+import Data.Bifunctor
+import Data.Bifoldable
+import Data.Bitraversable
+#if !MIN_VERSION_base(4,8,0)
+import Data.Traversable
+import Data.Foldable
+#endif
+#if !MIN_VERSION_base(4,11,0)
+import Data.Semigroup
+#endif
+import Data.InvertibleGrammar.Monad
+import qualified Debug.Trace
+
+-- | \"Cons\" pair of a heterogenous list or a stack with potentially
+-- polymophic tail. E.g. @"first" :- 2 :- (3,4) :- t@
+--
+-- Isomorphic to a tuple with two elments, but is much more
+-- convenient for nested pairs.
+data h :- t = h :- t deriving (Eq, Show, Functor, Foldable, Traversable)
+infixr 5 :-
+
+instance Bifunctor (:-) where
+  bimap f g (a :- b) = f a :- g b
+
+instance Bifoldable (:-) where
+  bifoldr f g x0 (a :- b) = a `f` (b `g` x0)
+
+instance Bitraversable (:-) where
+  bitraverse f g (a :- b) = (:-) <$> f a <*> g b
+
+-- | Representation of an invertible grammar -- a grammar that can be
+-- run either "forwards" and "backwards".
+--
+-- For a grammar @Grammar p a b@, running it forwards will take a
+-- value of type @a@ and possibly produce a value of type @b@. Running
+-- it backwards will take a value of type @b@ and possibly produce an
+-- @a@. If a value cannot be produced, an error message is generated.
+--
+-- As a common example, running a 'Grammar' forwards corresponds to
+-- parsing and running backwards corresponds to prettyprinting.
+--
+-- That is, the grammar defines a partial isomorphism between two
+-- values.
+data Grammar p a b where
+  -- | Total isomorphism grammar.
+  Iso        :: (a -> b) -> (b -> a) -> Grammar p a b
+
+  -- | Partial isomorphism. Use 'Flip' to change the direction of
+  -- partiality.
+  PartialIso :: (a -> b) -> (b -> Either Mismatch a) -> Grammar p a b
+
+  -- | Flip forward and backward passes of an underlying grammar.
+  Flip       :: Grammar p a b -> Grammar p b a
+
+  -- | Grammar composition.
+  (:.:)      :: Grammar p b c -> Grammar p a b -> Grammar p a c
+
+  -- | Grammar alternation. Left operand is tried first.
+  (:<>:)     :: Grammar p a b -> Grammar p a b -> Grammar p a b
+
+  -- | Application of a grammar on 'Traversable' functor.
+  Traverse   :: (Traversable f) => Grammar p a b -> Grammar p (f a) (f b)
+
+  -- | Applicaiton of a grammar on stack head
+  -- (first component of ':-').
+  OnHead     :: Grammar p a b -> Grammar p (a :- t) (b :- t)
+
+  -- | Applicaiton of a grammar on stack tail
+  -- (second component of ':-').
+  OnTail     :: Grammar p a b -> Grammar p (h :- a) (h :- b)
+
+  -- | Application of a grammar inside a context of annotation, used
+  -- for error messages.
+  Annotate   :: Text -> Grammar p a b -> Grammar p a b
+
+  -- | Application of a grammar inside a context of a nested
+  -- structure, used for error messages. E.g. JSON arrays.
+  Dive       :: Grammar p a b -> Grammar p a b
+
+  -- | Propagate logical position inside a nested
+  -- structure. E.g. after each successfully matched element of a JSON
+  -- array.
+  Step       :: Grammar p a a
+
+  -- | Update the position of grammar monad from value on grammar's
+  -- input or output on forward or backward pass, respectively. Used
+  -- for error messages.
+  Locate     :: Grammar p p p
+
+trace :: String -> a -> a
+trace = if False then Debug.Trace.trace else flip const
+
+
+instance Category (Grammar p) where
+  id                                              = Iso id id
+
+  PartialIso f g        . Iso f' g'               = trace "p/i" $ PartialIso (f . f') (fmap g' . g)
+  Iso f g               . PartialIso f' g'        = trace "i/p" $ PartialIso (f . f') (g' . g)
+
+  Flip (PartialIso f g) . Iso f' g'               = trace "fp/i" $ Flip $ PartialIso (g' . f) (g . f')
+  Iso f g               . Flip (PartialIso f' g') = trace "i/fp" $ Flip $ PartialIso (f' . g) (fmap f . g')
+
+  PartialIso f g        . (Iso f' g'               :.: h) = trace "p/i2" $ PartialIso (f . f') (fmap g' . g) :.: h
+  Iso f g               . (PartialIso f' g'        :.: h) = trace "i/p2" $ PartialIso (f . f') (g' . g) :.: h
+
+  Flip (PartialIso f g) . (Iso f' g'               :.: h) = trace "fp/i2" $ Flip (PartialIso (g' . f) (g . f')) :.: h
+  Iso f g               . (Flip (PartialIso f' g') :.: h) = trace "i/fp2" $ Flip (PartialIso (f' . g) (fmap f . g')) :.: h
+
+  Flip g . Flip h                                 = trace "f/f" $ Flip (h . g)
+  Iso f g . Iso f' g'                             = trace "i/i" $ Iso (f . f') (g' . g)
+
+  (g :.: h)             . j                       = trace "assoc" $ g :.: (h . j)
+
+  g                     . h                       = g :.: h
+
+
+instance Semigroup (Grammar p a b) where
+  (<>) = (:<>:)
+
+-- | Run 'Grammar' forwards.
+--
+-- For @Grammar p a b@, given a value of type @a@ tries to produce a
+-- value of type @b@, otherwise reports an error with position of type
+-- @p@.
+forward :: Grammar p a b -> a -> ContextError (Propagation p) (GrammarError p) b
+forward (Iso f _)        = return . f
+forward (PartialIso f _) = return . f
+forward (Flip g)         = backward g
+forward (g :.: f)        = forward g <=< forward f
+forward (f :<>: g)       = \x -> forward f x `mplus` forward g x
+forward (Traverse g)     = traverse (forward g)
+forward (OnHead g)       = \(a :- b) -> (:- b) <$> forward g a
+forward (OnTail g)       = \(a :- b) -> (a :-) <$> forward g b
+forward (Annotate t g)   = doAnnotate t . forward g
+forward (Dive g)         = doDive . forward g
+forward Step             = \x -> doStep >> return x
+forward Locate           = \x -> doLocate x >> return x
+
+-- | Run 'Grammar' backwards.
+--
+-- For @Grammar p a b@, given a value of type @b@ tries to produce a
+-- value of type @a@, otherwise reports an error with position of type
+-- @p@.
+backward :: Grammar p a b -> b -> ContextError (Propagation p) (GrammarError p) a
+backward (Iso _ g)        = return . g
+backward (PartialIso _ g) = either doError return . g
+backward (Flip g)         = forward g
+backward (g :.: f)        = backward g >=> backward f
+backward (f :<>: g)       = \x -> backward f x `mplus` backward g x
+backward (Traverse g)     = traverse (backward g)
+backward (OnHead g)       = \(a :- b) -> (:- b) <$> backward g a
+backward (OnTail g)       = \(a :- b) -> (a :-) <$> backward g b
+backward (Annotate t g)   = doAnnotate t . backward g
+backward (Dive g)         = doDive . backward g
+backward Step             = \x -> doStep >> return x
+backward Locate           = \x -> doLocate x >> return x
diff --git a/src/Data/InvertibleGrammar/Combinators.hs b/src/Data/InvertibleGrammar/Combinators.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/InvertibleGrammar/Combinators.hs
@@ -0,0 +1,209 @@
+{-# LANGUAGE CPP                 #-}
+{-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators       #-}
+
+module Data.InvertibleGrammar.Combinators
+  ( iso
+  , osi
+  , partialIso
+  , partialOsi
+  , push
+  , pair
+  , swap
+  , cons
+  , nil
+  , insert
+  , insertMay
+  , toDefault
+  , coproduct
+  , onHead
+  , onTail
+  , traversed
+  , flipped
+  , sealed
+  , coerced
+  , annotated
+  ) where
+
+import Control.Category ((>>>))
+import Data.Coerce
+import Data.Maybe
+import Data.Void
+import Data.Text (Text)
+import Data.InvertibleGrammar.Base
+
+#if !MIN_VERSION_base(4,11,0)
+import Data.Semigroup
+#endif
+
+-- | Isomorphism on the stack head.
+iso :: (a -> b) -> (b -> a) -> Grammar p (a :- t) (b :- t)
+iso f' g' = Iso f g
+  where
+    f (a :- t) = f' a :- t
+    g (b :- t) = g' b :- t
+
+
+-- | Flipped isomorphism on the stack head.
+osi :: (b -> a) -> (a -> b) -> Grammar p (a :- t) (b :- t)
+osi f' g' = Iso g f
+  where
+    f (a :- t) = f' a :- t
+    g (b :- t) = g' b :- t
+
+-- | Partial isomorphism (for backward run) on the stack head.
+partialIso :: (a -> b) -> (b -> Either Mismatch a) -> Grammar p (a :- t) (b :- t)
+partialIso f' g' = PartialIso f g
+  where
+    f (a :- t) = f' a :- t
+    g (b :- t) = (:- t) <$> g' b
+
+
+-- | Partial isomorphism (for forward run) on the stack head.
+partialOsi :: (a -> Either Mismatch b) -> (b -> a) -> Grammar p (a :- t) (b :- t)
+partialOsi g' f' = Flip $ PartialIso f g
+  where
+    f (a :- t) = f' a :- t
+    g (b :- t) = (:- t) <$> g' b
+
+
+-- | Push an element to the stack on forward run, check if the element
+-- satisfies predicate, otherwise report a mismatch.
+push :: a -> (a -> Bool) -> (a -> Mismatch) -> Grammar p t (a :- t)
+push a p e = PartialIso f g
+  where
+    f t = a :- t
+    g (a' :- t)
+      | p a' = Right t
+      | otherwise = Left $ e a'
+
+
+-- | 2-tuple grammar. Construct on forward run, deconstruct on
+-- backward run.
+pair :: Grammar p (b :- a :- t) ((a, b) :- t)
+pair = Iso
+  (\(b :- a :- t) -> (a, b) :- t)
+  (\((a, b) :- t) -> b :- a :- t)
+
+
+-- | List cons-cell grammar. Construct on forward run, deconstruct on
+-- backward run.
+cons :: Grammar p ([a] :- a :- t) ([a] :- t)
+cons = PartialIso
+  (\(lst :- el :- t) -> (el:lst) :- t)
+  (\(lst :- t) ->
+      case lst of
+        [] -> Left (expected "list element")
+        (el:rest) -> Right (rest :- el :- t))
+
+
+-- | Empty list grammar. Construct empty list on forward run, check if
+-- list is empty on backward run.
+nil :: Grammar p t ([a] :- t)
+nil = PartialIso
+  (\t -> [] :- t)
+  (\(lst :- t) ->
+      case lst of
+        [] -> Right t
+        (_el:_rest) -> Left (expected "end of list"))
+
+
+-- | Swap two topmost stack elements.
+swap :: Grammar p (a :- b :- t) (b :- a :- t)
+swap = Iso
+  (\(a :- b :- t) -> (b :- a :- t))
+  (\(b :- a :- t) -> (a :- b :- t))
+
+
+-- | Assoc-list element grammar. Inserts an element (with static key)
+-- on forward run, look up an element on backward run.
+insert :: (Eq k) => k -> Mismatch -> Grammar p (v :- [(k, v)] :- t) ([(k, v)] :- t)
+insert k m = PartialIso
+  (\(v :- alist :- t) -> ((k, v) : alist) :- t)
+  (\(alist :- t) ->
+     case popKey k alist of
+       Nothing -> Left m
+       Just (v, alist') -> Right (v :- alist' :- t))
+
+
+-- | Optional assoc-list element grammar. Like 'insert', but does not
+-- report a mismatch on backward run. Instead takes and produces a
+-- Maybe-value.
+insertMay :: (Eq k) => k -> Grammar p (Maybe v :- [(k, v)] :- t) ([(k, v)] :- t)
+insertMay k = PartialIso
+  (\(mv :- alist :- t) ->
+      case mv of
+        Just v -> ((k, v) : alist) :- t
+        Nothing -> alist :- t)
+  (\(alist :- t) ->
+     case popKey k alist of
+       Nothing -> Right (Nothing :- alist :- t)
+       Just (v, alist') -> Right (Just v :- alist' :- t))
+
+
+popKey :: forall k v. Eq k => k -> [(k, v)] -> Maybe (v, [(k, v)])
+popKey k' = go []
+  where
+    go :: [(k, v)] -> [(k, v)] -> Maybe (v, [(k, v)])
+    go acc (x@(k, v) : xs)
+      | k == k' = Just (v, reverse acc ++ xs)
+      | otherwise = go (x:acc) xs
+    go _ [] = Nothing
+
+
+-- | Default value grammar. Replaces 'Nothing' with a default value on
+-- forward run, an replaces a default value with 'Nothing' on backward
+-- run.
+toDefault :: (Eq a) => a -> Grammar p (Maybe a :- t) (a :- t)
+toDefault def = iso
+  (fromMaybe def)
+  (\val -> if val == def then Nothing else Just val)
+
+
+-- | Run a grammar operating on the stack head in a context where
+-- there is no stack.
+sealed :: Grammar p (a :- Void) (b :- Void) -> Grammar p a b
+sealed g =
+  Iso (:- error "void") (\(a :- _) -> a) >>>
+  g >>>
+  Iso (\(a :- _) -> a) (:- error "void")
+
+
+-- | Focus a given grammar to the stack head.
+onHead :: Grammar p a b -> Grammar p (a :- t) (b :- t)
+onHead = OnHead
+
+
+-- | Focus a given grammar to the stack tail.
+onTail :: Grammar p ta tb -> Grammar p (h :- ta) (h :- tb)
+onTail = OnTail
+
+
+-- | Traverse a structure with a given grammar.
+traversed :: (Traversable f) => Grammar p a b -> Grammar p (f a) (f b)
+traversed = Traverse
+
+
+-- | Run a grammar with inputs and outputs flipped.
+flipped :: Grammar p a b -> Grammar p b a
+flipped = Flip
+
+
+-- | Run a grammar with an annotation.
+annotated :: Text -> Grammar p a b -> Grammar p a b
+annotated = Annotate
+
+
+-- | Run a grammar with the stack heads coerced to other ('Coercible')
+-- types.
+coerced
+  :: (Coercible a c, Coercible b d) =>
+     Grammar p (a :- t) (b :- t')
+  -> Grammar p (c :- t) (d :- t')
+coerced g = iso coerce coerce >>> g >>> iso coerce coerce
+
+
+-- | Join alternative grammars in parallel.
+coproduct :: [Grammar p a b] -> Grammar p a b
+coproduct = foldl1 (<>)
diff --git a/src/Data/InvertibleGrammar/Generic.hs b/src/Data/InvertibleGrammar/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/InvertibleGrammar/Generic.hs
@@ -0,0 +1,240 @@
+{-# LANGUAGE CPP                    #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE OverloadedStrings      #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+
+-- NB: UndecidableInstances needed for nested type family application. :-/
+{-# LANGUAGE UndecidableInstances   #-}
+
+module Data.InvertibleGrammar.Generic
+  ( with
+  , match
+  , Coproduct (..)
+  ) where
+
+import Prelude hiding ((.), id)
+
+import Control.Applicative
+import Control.Category ((.))
+
+import Data.Functor.Identity
+import Data.InvertibleGrammar.Base
+import Data.Monoid (First(..))
+import Data.Profunctor (Choice(..))
+import Data.Profunctor.Unsafe
+import Data.Tagged
+import Data.Text (pack)
+#if !MIN_VERSION_base(4,11,0)
+import Data.Semigroup ((<>))
+#endif
+
+import GHC.Generics
+
+-- | Provide a data constructor/stack isomorphism to a grammar working on
+-- stacks. Works for types with one data constructor. For sum types use 'match'
+-- and 'Coproduct'.
+with
+  :: forall a b s t c d f p.
+     ( Generic a
+     , MkPrismList (Rep a)
+     , MkStackPrism f
+     , Rep a ~ M1 D d (M1 C c f)
+     , StackPrismLhs f t ~ b
+     , Constructor c
+     ) =>
+     (Grammar p b (a :- t) -> Grammar p s (a :- t))
+  -> Grammar p s (a :- t)
+with g =
+  let PrismList (P prism) = mkRevPrismList
+      name = conName (undefined :: m c f e)
+  in g (PartialIso
+         (fwd prism)
+         (maybe (Left $ expected ("constructor " <> pack name)) Right . bkwd prism))
+
+-- | Combine all grammars provided in 'Coproduct' list into a single grammar.
+match
+  :: ( Generic a
+     , MkPrismList (Rep a)
+     , Match (Rep a) bs t
+     , bs ~ Coll (Rep a) t
+     ) =>
+     Coproduct p s bs a t
+  -> Grammar p s (a :- t)
+match = fst . match' mkRevPrismList
+
+-- | Heterogenous list of grammars, each one matches a data constructor of type
+-- @a@. 'With' is used to provide a data constructor/stack isomorphism to a
+-- grammar working on stacks. 'End' ends the list of matches.
+data Coproduct p s bs a t where
+
+  With
+    :: (Grammar p b (a :- t) -> Grammar p s (a :- t))
+    -> Coproduct p s bs a t
+    -> Coproduct p s (b ': bs) a t
+
+  End :: Coproduct p s '[] a t
+
+----------------------------------------------------------------------
+-- Machinery
+
+type family (:++) (as :: [k]) (bs :: [k]) :: [k] where
+  (:++) (a ': as) bs = a ': (as :++ bs)
+  (:++) '[] bs = bs
+
+type family Coll (f :: * -> *) (t :: *) :: [*] where
+  Coll (f :+: g)  t = Coll f t :++ Coll g t
+  Coll (M1 D c f) t = Coll f t
+  Coll (M1 C c f) t = '[StackPrismLhs f t]
+
+type family Trav (t :: * -> *) (l :: [*]) :: [*] where
+  Trav (f :+: g) lst = Trav g (Trav f lst)
+  Trav (M1 D c f) lst = Trav f lst
+  Trav (M1 C c f) (l ': ls) = ls
+
+class Match (f :: * -> *) bs t where
+  match' :: PrismList f a
+         -> Coproduct p s bs a t
+         -> ( Grammar p s (a :- t)
+            , Coproduct p s (Trav f bs) a t
+            )
+
+instance (Match f bs t, Trav f bs ~ '[]) => Match (M1 D c f) bs t where
+  match' (PrismList p) = match' p
+
+instance
+  ( Match f bs t
+  , Match g (Trav f bs) t
+  ) => Match (f :+: g) bs t where
+  match' (p :& q) lst =
+    let (gp, rest)  = match' p lst
+        (qp, rest') = match' q rest
+    in (gp <> qp, rest')
+
+instance (StackPrismLhs f t ~ b, Constructor c) => Match (M1 C c f) (b ': bs) t where
+  match' (P prism) (With g rest) =
+    let name = conName (undefined :: m c f e)
+        p = fwd prism
+        q = maybe (Left $ expected ("constructor " <> pack name)) Right . bkwd prism
+    in (g $ PartialIso p q, rest)
+
+-- NB. The following machinery is heavily based on
+-- https://github.com/MedeaMelana/stack-prism/blob/master/Data/StackPrism/Generic.hs
+
+-- | Derive a list of stack prisms. For more information on the shape of a
+-- 'PrismList', please see the documentation below.
+mkRevPrismList :: (Generic a, MkPrismList (Rep a)) => StackPrisms a
+mkRevPrismList = mkPrismList' to (Just . from)
+
+type StackPrism a b = forall p f. (Choice p, Applicative f) => p a (f a) -> p b (f b)
+
+-- | Construct a prism.
+stackPrism :: (a -> b) -> (b -> Maybe a) -> StackPrism a b
+stackPrism f g = dimap (\b -> maybe (Left b) Right (g b)) (either pure (fmap f)) . right'
+
+-- | Apply a prism in forward direction.
+fwd :: StackPrism a b -> a -> b
+fwd l = runIdentity #. unTagged #. l .# Tagged .# Identity
+
+-- | Apply a prism in backward direction.
+bkwd :: StackPrism a b -> b -> Maybe a
+bkwd l = getFirst #. getConst #. l (Const #. First #. Just)
+
+-- | Convenient shorthand for a 'PrismList' indexed by a type and its generic
+-- representation.
+type StackPrisms a = PrismList (Rep a) a
+
+-- | A data family that is indexed on the building blocks from representation
+-- types from @GHC.Generics@. It builds up to a list of prisms, one for each
+-- constructor in the generic representation. The list is wrapped in the unary
+-- constructor @PrismList@. Within that constructor, the prisms are separated by
+-- the right-associative binary infix constructor @:&@. Finally, the individual
+-- prisms are wrapped in the unary constructor @P@.
+--
+-- As an example, here is how to define the prisms @nil@ and @cons@ for @[a]@,
+-- which is an instance of @Generic@:
+--
+-- > nil  :: StackPrism              t  ([a] :- t)
+-- > cons :: StackPrism (a :- [a] :- t) ([a] :- t)
+-- > PrismList (P nil :& P cons) = mkPrismList :: StackPrisms [a]
+data family PrismList (f :: * -> *) (a :: *)
+
+class MkPrismList (f :: * -> *) where
+  mkPrismList' :: (f p -> a) -> (a -> Maybe (f q)) -> PrismList f a
+
+data instance PrismList (M1 D c f) a = PrismList (PrismList f a)
+
+instance MkPrismList f => MkPrismList (M1 D c f) where
+  mkPrismList' f' g' = PrismList (mkPrismList' (f' . M1) (fmap unM1 . g'))
+
+infixr :&
+data instance PrismList (f :+: g) a = PrismList f a :& PrismList g a
+
+instance (MkPrismList f, MkPrismList g) => MkPrismList (f :+: g) where
+  mkPrismList' f' g' = f f' g' :& g f' g'
+    where
+      f :: forall a p q. ((f :+: g) p -> a) -> (a -> Maybe ((f :+: g) q)) -> PrismList f a
+      f _f' _g' = mkPrismList' (\fp -> _f' (L1 fp)) (matchL _g')
+      g :: forall a p q. ((f :+: g) p -> a) -> (a -> Maybe ((f :+: g) q)) -> PrismList g a
+      g _f' _g' = mkPrismList' (\gp -> _f' (R1 gp)) (matchR _g')
+
+      matchL :: (a -> Maybe ((f :+: g) q)) -> a -> Maybe (f q)
+      matchL _g' a = case _g' a of
+        Just (L1 f'') -> Just f''
+        _ -> Nothing
+
+      matchR :: (a -> Maybe ((f :+: g) q)) -> a -> Maybe (g q)
+      matchR _g' a = case _g' a of
+        Just (R1 g'') -> Just g''
+        _ -> Nothing
+
+data instance PrismList (M1 C c f) a = P (forall t. StackPrism (StackPrismLhs f t) (a :- t))
+
+instance MkStackPrism f => MkPrismList (M1 C c f) where
+  mkPrismList' f' g' = P (stackPrism (f f') (g g'))
+    where
+      f :: forall a p t. (M1 C c f p -> a) -> StackPrismLhs f t -> a :- t
+      f _f' lhs = mapHead (_f' . M1) (mkR lhs)
+      g :: forall a p t. (a -> Maybe (M1 C c f p)) -> (a :- t) -> Maybe (StackPrismLhs f t)
+      g _g' (a :- t) = fmap (mkL . (:- t) . unM1) (_g' a)
+
+-- Deriving types and conversions for single constructors
+
+type family StackPrismLhs (f :: * -> *) (t :: *) :: *
+
+class MkStackPrism (f :: * -> *) where
+  mkR :: forall p t. StackPrismLhs f t -> (f p :- t)
+  mkL :: forall p t. (f p :- t) -> StackPrismLhs f t
+
+type instance StackPrismLhs U1 t = t
+instance MkStackPrism U1 where
+  mkR t         = U1 :- t
+  mkL (U1 :- t) = t
+
+type instance StackPrismLhs (K1 i a) t = a :- t
+instance MkStackPrism (K1 i a) where
+  mkR (h :- t) = K1 h :- t
+  mkL (K1 h :- t) = h :- t
+
+type instance StackPrismLhs (M1 i c f) t = StackPrismLhs f t
+instance MkStackPrism f => MkStackPrism (M1 i c f) where
+  mkR = mapHead M1 . mkR
+  mkL = mkL . mapHead unM1
+
+type instance StackPrismLhs (f :*: g) t = StackPrismLhs g (StackPrismLhs f t)
+instance (MkStackPrism f, MkStackPrism g) => MkStackPrism (f :*: g) where
+  mkR t = (hg :*: hf) :- tg
+    where
+      hf :- tf = mkR t
+      hg :- tg = mkR tf
+  mkL ((hf :*: hg) :- t) = mkL (hg :- mkL (hf :- t))
+
+mapHead :: (a -> b) -> (a :- t) -> (b :- t)
+mapHead f (h :- t) = f h :- t
diff --git a/src/Data/InvertibleGrammar/Monad.hs b/src/Data/InvertibleGrammar/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/InvertibleGrammar/Monad.hs
@@ -0,0 +1,205 @@
+{-# LANGUAGE CPP               #-}
+{-# LANGUAGE DeriveGeneric     #-}
+{-# LANGUAGE FlexibleContexts  #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ViewPatterns      #-}
+
+module Data.InvertibleGrammar.Monad
+  ( module Control.Monad.ContextError
+  , runGrammar
+  , runGrammarDoc
+  , runGrammarString
+  , ErrorMessage (..)
+  , doAnnotate
+  , doDive
+  , doStep
+  , doLocate
+  , doError
+  , Propagation
+  , GrammarError (..)
+  , Mismatch
+  , expected
+  , unexpected
+  ) where
+
+import Control.Arrow (left)
+import Control.Applicative
+import Control.Monad.ContextError
+
+import Data.Maybe
+import Data.Semigroup as Semi
+import Data.Set (Set)
+import qualified Data.Set as S
+import Data.Text (Text)
+import GHC.Generics
+
+import Data.Text.Prettyprint.Doc
+  ( Doc, Pretty, pretty, vsep, hsep, line, indent, fillSep, punctuate
+  , comma, colon, (<+>), layoutSmart, PageWidth(..), LayoutOptions(..)
+  )
+
+#if MIN_VERSION_prettyprinter(1,2,0)
+import Data.Text.Prettyprint.Doc.Render.String
+#else
+import Data.Text.Prettyprint.Doc (SimpleDocStream)
+import Data.Text.Prettyprint.Doc.Render.ShowS
+
+renderString :: SimpleDocStream ann -> String
+renderString stream = renderShowS stream ""
+#endif
+
+
+initPropagation :: p -> Propagation p
+initPropagation = Propagation [0] []
+
+data Propagation p = Propagation
+  { pProp :: [Int]
+  , pAnns :: [Text]
+  , pPos  :: p
+  } deriving (Show)
+
+instance Eq (Propagation p) where
+  Propagation xs _ _ == Propagation ys _ _ = xs == ys
+  {-# INLINE (==) #-}
+
+instance Ord (Propagation p) where
+  compare (Propagation as _ _) (Propagation bs _ _) =
+    reverse as `compare` reverse bs
+  {-# INLINE compare #-}
+
+-- | Data type to encode mismatches during parsing or generation, kept
+-- abstract. Use 'expected' and 'unexpected' constructors to build a
+-- mismatch report.
+data Mismatch = Mismatch
+  { mismatchExpected :: Set Text
+  , mismatchGot :: Maybe Text
+  } deriving (Show, Eq)
+
+-- | Construct a mismatch report with specified expectation. Can be
+-- appended to other expectations and 'unexpected' reports to clarify
+-- a mismatch.
+expected :: Text -> Mismatch
+expected a = Mismatch (S.singleton a) Nothing
+
+-- | Construct a mismatch report with information what occurred during
+-- the processing but was not expected.
+unexpected :: Text -> Mismatch
+unexpected a = Mismatch S.empty (Just a)
+
+instance Semigroup Mismatch where
+  m <> m' =
+    Mismatch
+      (mismatchExpected m Semi.<> mismatchExpected m')
+      (mismatchGot m <|> mismatchGot m')
+  {-# INLINE (<>) #-}
+
+instance Monoid Mismatch where
+  mempty = Mismatch mempty mempty
+  {-# INLINE mempty #-}
+  mappend = (<>)
+  {-# INLINE mappend #-}
+
+-- | Run a 'forward' or 'backward' pass of a 'Grammar'.
+runGrammar :: p -> ContextError (Propagation p) (GrammarError p) a -> Either (ErrorMessage p) a
+runGrammar initPos m =
+  case runContextError m (initPropagation initPos) of
+    Left (GrammarError p mismatch) ->
+      Left $ ErrorMessage
+        (pPos p)
+        (reverse (pAnns p))
+        (mismatchExpected mismatch)
+        (mismatchGot mismatch)
+    Right a ->
+      Right a
+
+-- | Run a 'forward' or 'backward' pass of a 'Grammar', report errors
+-- as pretty printed 'Doc' message.
+runGrammarDoc :: (Pretty p) => p -> ContextError (Propagation p) (GrammarError p) a -> Either (Doc ann) a
+runGrammarDoc initPos m =
+  left (ppError pretty) $
+    runGrammar initPos m
+
+-- | Run a 'forward' or 'backward' pass of a 'Grammar', report errors
+-- as 'String' message.
+runGrammarString :: (Show p) => p -> ContextError (Propagation p) (GrammarError p) a -> Either String a
+runGrammarString initPos m =
+  left (renderString . layoutSmart (LayoutOptions (AvailablePerLine 79 0.75)) . ppError (pretty . show)) $
+    runGrammar initPos m
+
+-- | 'Grammar' run error messages type.
+data ErrorMessage p = ErrorMessage
+  { emPosition :: p
+  , emAnnotations :: [Text]
+  , emExpected :: Set Text
+  , emGot :: Maybe Text
+  } deriving (Eq, Ord, Generic)
+
+instance (Pretty p) => Pretty (ErrorMessage p) where
+  pretty = ppError pretty
+
+ppMismatch :: Set Text -> Maybe Text -> Doc ann
+ppMismatch (S.toList -> []) Nothing =
+  "Unknown mismatch occurred"
+ppMismatch (S.toList -> []) unexpected =
+  "Unexpected:" <+> pretty unexpected
+ppMismatch (S.toList -> expected) Nothing =
+  "Expected:" <+> fillSep (punctuate comma $ map pretty expected)
+ppMismatch (S.toList -> expected) (Just got) =
+  vsep
+  [ "Expected:" <+> fillSep (punctuate comma $ map pretty expected)
+  , "But got: " <+> pretty got
+  ]
+
+ppError :: (p -> Doc ann) -> ErrorMessage p -> Doc ann
+ppError ppPosition (ErrorMessage pos annotations expected got) =
+  vsep $ catMaybes
+    [ Just $ ppPosition pos `mappend` ":" <+> "mismatch:"
+    , if null annotations
+      then Nothing
+      else Just $ indent 2 $ "In" <+> hsep (punctuate (comma <> line <> "in") $ map pretty annotations) <> colon
+    , Just $ indent 4 $ ppMismatch expected got
+    ]
+
+data GrammarError p = GrammarError (Propagation p) Mismatch
+  deriving (Show)
+
+instance Semigroup (GrammarError p) where
+  GrammarError pos m <> GrammarError pos' m'
+    | pos > pos' = GrammarError pos m
+    | pos < pos' = GrammarError pos' m'
+    | otherwise  = GrammarError pos (m <> m')
+  {-# INLINE (<>) #-}
+
+doAnnotate :: MonadContextError (Propagation p) e m => Text -> m a -> m a
+doAnnotate ann =
+  localContext $ \propagation ->
+    propagation { pAnns = ann : pAnns propagation }
+{-# INLINE doAnnotate #-}
+
+doDive :: MonadContextError (Propagation p) e m => m a -> m a
+doDive =
+  localContext $ \propagation ->
+    propagation { pProp = 0 : pProp propagation }
+{-# INLINE doDive #-}
+
+doStep :: MonadContextError (Propagation p) e m => m ()
+doStep =
+  modifyContext $ \propagation ->
+    propagation
+      { pProp = case pProp propagation of
+          (x : xs) -> succ x : xs
+          [] -> [0]
+      }
+{-# INLINE doStep #-}
+
+doLocate :: MonadContextError (Propagation p) e m => p -> m ()
+doLocate pos =
+  modifyContext $ \propagation ->
+    propagation { pPos = pos }
+{-# INLINE doLocate #-}
+
+doError :: MonadContextError (Propagation p) (GrammarError p) m => Mismatch -> m a
+doError mismatch =
+  throwInContext $ \ctx ->
+    GrammarError ctx mismatch
+{-# INLINE doError #-}
diff --git a/src/Data/InvertibleGrammar/TH.hs b/src/Data/InvertibleGrammar/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/InvertibleGrammar/TH.hs
@@ -0,0 +1,157 @@
+{-# LANGUAGE CPP             #-}
+{-# LANGUAGE LambdaCase      #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Data.InvertibleGrammar.TH where
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+#endif
+import Data.Foldable (toList)
+import Data.InvertibleGrammar.Base
+import Data.Maybe
+import Data.Text (pack)
+import Language.Haskell.TH as TH
+import Data.Set (Set)
+import qualified Data.Set as S
+#if !MIN_VERSION_base(4,11,0)
+import Data.Semigroup ((<>))
+#endif
+
+
+{- | Build a prism and the corresponding grammar that will match on the
+     given constructor and convert it to reverse sequence of :- stacks.
+
+     E.g. consider a data type:
+
+     > data FooBar a b c = Foo a b c | Bar
+
+     For constructor Foo
+
+     > fooGrammar = $(grammarFor 'Foo)
+
+     will expand into
+
+     > fooGrammar = PartialIso
+     >   (\(c :- b :- a :- t) -> Foo a b c :- t)
+     >   (\case { Foo a b c :- t -> Just $ c :- b :- a :- t; _ -> Nothing })
+
+     Note the order of elements on the stack:
+
+     > ghci> :t fooGrammar
+     > fooGrammar :: Grammar p (c :- (b :- (a :- t))) (FooBar a b c :- t)
+-}
+
+grammarFor :: Name -> ExpQ
+grammarFor constructorName = do
+#if defined(__GLASGOW_HASKELL__)
+# if __GLASGOW_HASKELL__ <= 710
+  DataConI realConstructorName _typ parentName _fixity <- reify constructorName
+# else
+  DataConI realConstructorName _typ parentName <- reify constructorName
+# endif
+#endif
+  TyConI dataDef <- reify parentName
+
+  let Just (single, constructorInfo) = do
+        (single, allConstr) <- constructors dataDef
+        constr <- findConstructor realConstructorName allConstr
+        return (single, constr)
+
+  let ts = fieldTypes constructorInfo
+  vs <- mapM (const $ newName "x") ts
+  t <- newName "t"
+
+  let matchStack []      = varP t
+      matchStack (_v:vs) = [p| $(varP _v) :- $_vs' |]
+        where
+          _vs' = matchStack vs
+      fPat  = matchStack vs
+      buildConstructor = foldr (\v acc -> appE acc (varE v)) (conE realConstructorName) vs
+      fBody = [e| $buildConstructor :- $(varE t) |]
+      fFunc = lamE [fPat] fBody
+
+  let gPat  = [p| $_matchConsructor :- $(varP t) |]
+        where
+          _matchConsructor = conP realConstructorName (map varP (reverse vs))
+      gBody = foldr (\v acc -> [e| $(varE v) :- $acc |]) (varE t) vs
+      gFunc = lamCaseE $ catMaybes
+        [ Just $ TH.match gPat (normalB [e| Right ($gBody) |]) []
+        , if single
+          then Nothing
+          else Just $ TH.match wildP (normalB [e| Left (expected $ "constructor " <> pack ( $(stringE (show constructorName))) ) |]) []
+        ]
+
+  [e| PartialIso $fFunc $gFunc |]
+
+
+{- | Build prisms and corresponding grammars for all data constructors of given
+     type. Expects grammars to zip built ones with.
+
+     > $(match ''Maybe)
+
+     Will expand into a lambda:
+
+     > (\nothingG justG -> ($(grammarFor 'Nothing) . nothingG) <>
+     >                     ($(grammarFor 'Just)    . justG))
+-}
+match :: Name -> ExpQ
+match tyName = do
+  names  <- concatMap (toList . constructorNames) <$> (extractConstructors =<< reify tyName)
+  argTys <- mapM (\_ -> newName "a") names
+  let grammars = map (\(con, arg) -> [e| $(varE arg) $(grammarFor con) |]) (zip names argTys)
+  lamE (map varP argTys) (foldr1 (\e1 e2 -> [e| $e1 <> $e2 |]) grammars)
+  where
+    extractConstructors :: Info -> Q [Con]
+    extractConstructors (TyConI dataDef) =
+      case constructors dataDef of
+        Just (_, cs) -> pure cs
+        Nothing      -> fail $ "Data type " ++ show tyName ++ " defines no constructors"
+    extractConstructors _ =
+      fail $ "Data definition expected for name " ++ show tyName
+
+----------------------------------------------------------------------
+-- Utils
+
+constructors :: Dec -> Maybe (Bool, [Con])
+#if defined(__GLASGOW_HASKELL__)
+# if __GLASGOW_HASKELL__ <= 710
+constructors (DataD _ _ _ cs _)     = Just (length cs == 1, cs)
+constructors (NewtypeD _ _ _ c _)   = Just (True, [c])
+# else
+constructors (DataD _ _ _ _ cs _)   = Just (length cs == 1, cs)
+constructors (NewtypeD _ _ _ _ c _) = Just (True, [c])
+# endif
+#endif
+constructors _                      = Nothing
+
+findConstructor :: Name -> [Con] -> Maybe Con
+findConstructor _    [] = Nothing
+findConstructor name (c:cs)
+  | name `S.member` constructorNames c = Just c
+  | otherwise                          = findConstructor name cs
+
+constructorNames :: Con -> Set Name
+constructorNames = \case
+  NormalC name _   -> S.singleton name
+  RecC name _      -> S.singleton name
+  InfixC _ name _  -> S.singleton name
+  ForallC _ _ con' -> constructorNames con'
+#if MIN_VERSION_template_haskell(2, 11, 0)
+  GadtC cs _ _     -> S.fromList cs
+  RecGadtC cs _ _  -> S.fromList cs
+#endif
+
+fieldTypes :: Con -> [Type]
+fieldTypes = \case
+  NormalC _ fieldTypes  -> map extractType fieldTypes
+  RecC _ fieldTypes     -> map extractType' fieldTypes
+  InfixC (_,a) _b (_,b) -> [a, b]
+  ForallC _ _ con'      -> fieldTypes con'
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
+  GadtC _ fs _          -> map extractType fs
+  RecGadtC _ fs _       -> map extractType' fs
+#endif
+  where
+    extractType (_, t) = t
+    extractType' (_, _, t) = t