diff --git a/.envrc b/.envrc
new file mode 100644
--- /dev/null
+++ b/.envrc
@@ -0,0 +1,11 @@
+use_flake() {
+  watch_file flake.nix
+  watch_file flake.lock
+  watch_file default.nix
+  watch_file shell.nix
+  mkdir -p "$(direnv_layout_dir)"
+  eval "$(nix print-dev-env --option allow-import-from-derivation true -L --show-trace --profile "$(direnv_layout_dir)/flake-profile" || echo false)" &&
+  nix-store --add-root "shell.root" \
+   --indirect --realise "$(direnv_layout_dir)/flake-profile"
+}
+use flake
diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,3 @@
+## symantic-parser-0.0.0.20210101
+
+* Initial (pre-alpha) release, on the unsuspecting world at sleep.
diff --git a/Makefile b/Makefile
new file mode 100644
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,49 @@
+cabal = $(wildcard *.cabal)
+package = $(notdir ./$(cabal:.cabal=))
+version = $(shell sed -ne 's/^version: *\(.*\)/\1/p' $(cabal))
+all: build
+build:
+	cabal build
+clean c:
+	cabal clean
+repl:
+	cabal repl
+
+t:
+	cabal test -fdump-splices --test-show-details always --test-options "--color always --size-cutoff 100000"
+t/accept:
+	cabal test --test-show-details always --test-options "--accept --color always --size-cutoff 100000"
+t/prof:
+	cabal test --enable-profiling --enable-library-coverage --enable-coverage --test-show-details always
+t/repl:
+	cabal repl --enable-tests symantic-parser-test
+t/splices: t
+	shopt -s globstar; $$EDITOR dist-newstyle/build/**/t/**/*.dump-splices
+
+doc:
+	cabal haddock --haddock-css ocean --haddock-hyperlink-source
+
+tag:
+	git tag --merged | grep -Fqx "$(package)-$(version)" || \
+	git tag -f -s -m "$(package) v$(version)" $(package)-$(version)
+
+tar:
+	cabal sdist
+	cabal haddock --haddock-for-hackage --enable-doc
+upload: LANG=C
+upload: tar
+	cabal upload $(CABAL_UPLOAD_FLAGS) dist-newstyle/sdist/$(package)-$(version).tar.gz
+	cabal upload $(CABAL_UPLOAD_FLAGS) --documentation dist-newstyle/$(package)-$(version)-docs.tar.gz
+%/publish: CABAL_UPLOAD_FLAGS+=--publish
+%/publish: %
+	
+publish: upload/publish
+
+nix-build:
+	nix -L build
+nix-relock:
+	nix flake update --recreate-lock-file
+nix-repl:
+	nix -L develop --command cabal repl
+nix-shell:
+	nix -L develop
diff --git a/ReadMe.md b/ReadMe.md
new file mode 100644
--- /dev/null
+++ b/ReadMe.md
@@ -0,0 +1,19 @@
+### Main differences with respect to `ParsleyHaskell`
+
+- Tagless-final and `DefaultSignatures` are used instead of tagfull-final to handle recursion schemes, this avoids constructing and deconstructing as much tags when transforming combinators or instructions.
+  And structures/simplifies the code by avoiding to define custom traversals (`traverseCombinator`) or custom fix-point data-types (`Fix4`) and associated utilities (`cata4`) when introducing new index-types. 
+  Note that the extensibility of combinators, a great feature of tagless-final, is not really achievable when using the optimizing pass which requires a comprehensive initial encoding.
+
+- No dependency on `dependent-map` by keeping observed sharing inside `def` and `ref` combinators, instead of passing by a `DMap`. Same for join-points, where `TemplateHaskell` names are also directly used instead of passing by a `DMap`.
+
+- No dependency on GHC plugins: `lift-plugin` and `idioms-plugin`, because those are plugins hence introduce a bit of complexity in the build processes using this parser, but most importantly they are experimental and only cosmetic, since they only enable a cleaner usage of the parsing combinators, by lifting Haskell code in `pure` to integrate the `TemplateHaskell` needed. I do not understand them that much and do not feel confortable to maintain them in case their authors abandon them.
+
+- Error messages based upon the farthest input position reached (not yet implemented in `ParsleyHaskell`).
+
+- License is `GPL-3.0-or-later` not `BSD-3-Clause`.
+
+### Main goals
+
+- For me to better understand `ParsleyHaskell`, and find a manageable balance between simplicity of the codebase and features of the parser.
+
+- To support parsing tree-like data structures (like XML or HTTP routes) instead of just string-like data structures, which I've done using `megaparsec`, but it is not conceived for such input, and is less principled when it comes to optimizing, like merging alternatives.
diff --git a/ToDo.md b/ToDo.md
new file mode 100644
--- /dev/null
+++ b/ToDo.md
@@ -0,0 +1,12 @@
+- [ ] Factorize input size checks (like Parsley's piggy bank).
+
+- [ ] Golden tests using more complex grammars.
+
+- [ ] Error messages also based upon: [A Parsing Machine for Parsing Expression Grammars with Labeled Failures](https://dl.acm.org/doi/10.1145/2851613.2851750)
+
+- [ ] Consider introducing registers like in ParsleyHaskell.
+
+- [ ] Concerning the unusual `pure :: H.Haskell a -> repr a`,
+  it may be acceptable to use `H.Haskell` only internally.
+
+- [ ] Move the `Symantic.Univariant.*` modules into a separate package, maybe `symantic-base`.
diff --git a/cabal.project b/cabal.project
new file mode 100644
--- /dev/null
+++ b/cabal.project
@@ -0,0 +1,1 @@
+packages:.
diff --git a/default.nix b/default.nix
new file mode 100644
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,41 @@
+{ pkgs ? import <nixpkgs> {}
+, ghc ? "ghc901"
+, withHoogle ? false
+}:
+let
+  haskellPackages =
+    if ghc == null
+    then pkgs.haskellPackages
+    else pkgs.haskell.packages.${ghc};
+  hs = haskellPackages.extend (with pkgs.haskell.lib;
+    hself: hsuper: {
+      data-fix = doJailbreak hsuper.data-fix;
+      primitive = doJailbreak hsuper.primitive;
+      assoc = doJailbreak hsuper.assoc;
+      these = doJailbreak hsuper.these;
+      dump-core = dontCheck (unmarkBroken hsuper.dump-core);
+
+      #symantic-parser = enableExecutableProfiling (doCheck ( hself.callCabal2nix "symantic-parser" ./. {}));
+    } //
+    packageSourceOverrides {
+      symantic-parser = ./.;
+    } hself hsuper
+  );
+in hs.symantic-parser // {
+  shell = hs.shellFor {
+    packages = p: [ p.symantic-parser ];
+    nativeBuildInputs = [
+      pkgs.cabal-install
+      #hs.cabal-install
+      #hs.haskell-language-server
+      #hs.hpc
+    ];
+    buildInputs = [
+      #hs.ghcid
+      #hs.ormolu
+      #hs.hlint
+      #pkgs.nixpkgs-fmt
+    ];
+    inherit withHoogle;
+  };
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,14 @@
+{
+inputs.nixpkgs.url = "flake:nixpkgs";
+inputs.flake-utils.url = "github:numtide/flake-utils";
+outputs = inputs:
+  inputs.flake-utils.lib.eachDefaultSystem (system: let
+    pkgs = inputs.nixpkgs.legacyPackages.${system};
+    in {
+      defaultPackage = import ./default.nix { inherit pkgs; };
+      devShell = (import ./default.nix {
+        inherit pkgs;
+      }).shell;
+    }
+  );
+}
diff --git a/shell.nix b/shell.nix
new file mode 100644
--- /dev/null
+++ b/shell.nix
@@ -0,0 +1,1 @@
+(import ./. {}).shell
diff --git a/src/Symantic/Parser.hs b/src/Symantic/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Symantic.Parser
+ ( module Symantic.Parser.Grammar
+ , module Symantic.Parser.Machine
+ , module Symantic.Parser
+ ) where
+
+import Data.Either (Either(..))
+import Data.Ord (Ord)
+import Language.Haskell.TH (CodeQ)
+import Text.Show (Show)
+import qualified Language.Haskell.TH.Syntax as TH
+
+import Symantic.Parser.Grammar
+import Symantic.Parser.Machine
+
+runParser :: forall inp a.
+  Ord (InputToken inp) =>
+  Show (InputToken inp) =>
+  TH.Lift (InputToken inp) =>
+  -- InputToken inp ~ Char =>
+  Input inp =>
+  Readable Gen (InputToken inp) =>
+  Parser inp a ->
+  CodeQ (inp -> Either (ParsingError inp) a)
+runParser p = [|| \input -> $$(generate [||input||] (machine p)) ||]
diff --git a/src/Symantic/Parser/Grammar.hs b/src/Symantic/Parser/Grammar.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Grammar.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE ConstraintKinds #-} -- For Grammar
+module Symantic.Parser.Grammar
+ ( module Symantic.Parser.Grammar
+ , module Symantic.Parser.Grammar.Combinators
+ , module Symantic.Parser.Grammar.Fixity
+ , module Symantic.Parser.Grammar.Optimize
+ , module Symantic.Parser.Grammar.ObserveSharing
+ , module Symantic.Parser.Grammar.Write
+ , module Symantic.Parser.Grammar.Dump
+ , Letable(..)
+ ) where
+import Symantic.Parser.Grammar.Combinators
+import Symantic.Parser.Grammar.Dump
+import Symantic.Parser.Grammar.Fixity
+import Symantic.Parser.Grammar.ObserveSharing
+import Symantic.Parser.Grammar.Optimize
+import Symantic.Parser.Grammar.Write
+import Symantic.Univariant.Letable (Letable(..))
+
+import Data.Function ((.))
+import Data.String (String)
+import Text.Show (Show(..))
+import qualified Language.Haskell.TH.Syntax as TH
+
+-- Class 'Grammar'
+type Grammar repr =
+  ( Applicable repr
+  , Alternable repr
+  --, Satisfiable repr
+  , Letable TH.Name repr
+  , Selectable repr
+  , Matchable repr
+  , Foldable repr
+  , Lookable repr
+  )
+
+-- | A usual pipeline to interpret 'Comb'inators:
+-- 'observeSharing' then 'optimizeComb' then a polymorphic @(repr)@.
+grammar :: Grammar repr => ObserveSharing TH.Name (OptimizeComb TH.Name repr) a -> repr a
+grammar = optimizeComb . observeSharing
+
+-- | A usual pipeline to show 'Comb'inators:
+-- 'observeSharing' then 'optimizeComb' then 'dumpComb' then 'show'.
+showGrammar :: ObserveSharing TH.Name (OptimizeComb TH.Name DumpComb) a -> String
+showGrammar = show . dumpComb . optimizeComb . observeSharing
diff --git a/src/Symantic/Parser/Grammar/Combinators.hs b/src/Symantic/Parser/Grammar/Combinators.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Grammar/Combinators.hs
@@ -0,0 +1,471 @@
+-- The default type signature of type class methods are changed
+-- to introduce a Liftable constraint and the same type class but on the 'Output' repr,
+-- this setup avoids to define the method with boilerplate code when its default
+-- definition with lift* and 'trans' does what is expected by an instance
+-- of the type class. This is almost as explained in:
+-- https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE DeriveLift #-} -- For TH.Lift (ErrorItem tok)
+{-# LANGUAGE StandaloneDeriving #-} -- For Show (ErrorItem (InputToken inp))
+{-# LANGUAGE TemplateHaskell #-}
+module Symantic.Parser.Grammar.Combinators where
+
+import Data.Bool (Bool(..), not, (||))
+import Data.Char (Char)
+import Data.Either (Either(..))
+import Data.Eq (Eq(..))
+import Data.Function ((.), flip, const)
+import Data.Int (Int)
+import Data.Maybe (Maybe(..))
+import Data.Ord (Ord)
+import Data.String (String)
+import Language.Haskell.TH (CodeQ)
+import Text.Show (Show(..))
+import qualified Data.Functor as Functor
+import qualified Data.List as List
+import qualified Language.Haskell.TH.Syntax as TH
+
+import qualified Symantic.Univariant.Trans as Sym
+import qualified Symantic.Parser.Haskell as H
+
+-- * Class 'Applicable'
+-- | This is like the usual 'Functor' and 'Applicative' type classes
+-- from the @base@ package, but using @('H.Haskell' a)@ instead of just @(a)@
+-- to be able to use and pattern match on some usual terms of type @(a)@ (like
+-- 'H.id') and thus apply some optimizations.
+-- @(repr)@ , for "representation", is the usual tagless-final abstraction
+-- over the many semantics that this syntax (formed by the methods
+-- of type class like this one) will be interpreted.
+class Applicable repr where
+  -- | @(a2b '<$>' ra)@ parses like @(ra)@ but maps its returned value with @(a2b)@.
+  (<$>) :: H.Haskell (a -> b) -> repr a -> repr b
+  (<$>) f = (pure f <*>)
+
+  -- | Like '<$>' but with its arguments 'flip'-ped.
+  (<&>) :: repr a -> H.Haskell (a -> b) -> repr b
+  (<&>) = flip (<$>)
+
+  -- | @(a '<$' rb)@ parses like @(rb)@ but discards its returned value by replacing it with @(a)@.
+  (<$) :: H.Haskell a -> repr b -> repr a
+  (<$) x = (pure x <*)
+
+  -- | @(ra '$>' b)@ parses like @(ra)@ but discards its returned value by replacing it with @(b)@.
+  ($>) :: repr a -> H.Haskell b -> repr b
+  ($>) = flip (<$)
+
+  -- | @('pure' a)@ parses the empty string, always succeeding in returning @(a)@.
+  pure :: H.Haskell a -> repr a
+  default pure ::
+    Sym.Liftable repr => Applicable (Sym.Output repr) =>
+    H.Haskell a -> repr a
+  pure = Sym.lift . pure
+
+  -- | @(ra2b '<*>' ra)@ parses sequentially @(ra2b)@ and then @(ra)@,
+  -- and returns the application of the function returned by @(ra2b)@
+  -- to the value returned by @(ra)@.
+  (<*>) :: repr (a -> b) -> repr a -> repr b
+  default (<*>) ::
+    Sym.Liftable2 repr => Applicable (Sym.Output repr) =>
+    repr (a -> b) -> repr a -> repr b
+  (<*>) = Sym.lift2 (<*>)
+
+  -- | @('liftA2' a2b2c ra rb)@ parses sequentially @(ra)@ and then @(rb)@,
+  -- and returns the application of @(a2b2c)@ to the values returned by those parsers.
+  liftA2 :: H.Haskell (a -> b -> c) -> repr a -> repr b -> repr c
+  liftA2 f x = (<*>) (f <$> x)
+
+  -- | @(ra '<*' rb)@ parses sequentially @(ra)@ and then @(rb)@,
+  -- and returns like @(ra)@, discarding the return value of @(rb)@.
+  (<*) :: repr a -> repr b -> repr a
+  (<*) = liftA2 H.const
+
+  -- | @(ra '*>' rb)@ parses sequentially @(ra)@ and then @(rb)@,
+  -- and returns like @(rb)@, discarding the return value of @(ra)@.
+  (*>) :: repr a -> repr b -> repr b
+  x *> y = (H.id <$ x) <*> y
+
+  -- | Like '<*>' but with its arguments 'flip'-ped.
+  (<**>) :: repr a -> repr (a -> b) -> repr b
+  (<**>) = liftA2 (H.flip H..@ (H.$))
+  {-
+  (<**>) :: repr a -> repr (a -> b) -> repr b
+  (<**>) = liftA2 (\a f -> f a)
+  -}
+infixl 4 <$>, <&>, <$, $>, <*>, <*, *>, <**>
+
+-- * Class 'Alternable'
+class Alternable repr where
+  -- | @(rl '<|>' rr)@ parses @(rl)@ and return its return value or,
+  -- if it fails, parses @(rr)@ from where @(rl)@ has left the input stream,
+  -- and returns its return value.
+  (<|>) :: repr a -> repr a -> repr a
+  -- | @(empty)@ parses nothing, always failing to return a value.
+  empty :: repr a
+  -- | @('try' ra)@ records the input stream position,
+  -- then parses like @(ra)@ and either returns its value it it succeeds or fails
+  -- if it fails but with a reset of the input stream to the recorded position.
+  -- Generally used on the first alternative: @('try' rl '<|>' rr)@.
+  try :: repr a -> repr a
+  default (<|>) ::
+    Sym.Liftable2 repr => Alternable (Sym.Output repr) =>
+    repr a -> repr a -> repr a
+  default empty ::
+    Sym.Liftable repr => Alternable (Sym.Output repr) =>
+    repr a
+  default try ::
+    Sym.Liftable1 repr => Alternable (Sym.Output repr) =>
+    repr a -> repr a
+  (<|>) = Sym.lift2 (<|>)
+  empty = Sym.lift empty
+  try = Sym.lift1 try
+  -- | Like @('<|>')@ but with different returning types for the alternatives,
+  -- and a return value wrapped in an 'Either' accordingly.
+  (<+>) :: Applicable repr => Alternable repr => repr a -> repr b -> repr (Either a b)
+  p <+> q = H.left <$> p <|> H.right <$> q
+infixl 3 <|>, <+>
+
+optionally :: Applicable repr => Alternable repr => repr a -> H.Haskell b -> repr b
+optionally p x = p $> x <|> pure x
+
+optional :: Applicable repr => Alternable repr => repr a -> repr ()
+optional = flip optionally H.unit
+
+option :: Applicable repr => Alternable repr => H.Haskell a -> repr a -> repr a
+option x p = p <|> pure x
+
+choice :: Alternable repr => [repr a] -> repr a
+choice = List.foldr (<|>) empty
+ -- FIXME: Here hlint suggests to use Data.Foldable.asum,
+ -- but at this point there is no asum for our own (<|>)
+
+maybeP :: Applicable repr => Alternable repr => repr a -> repr (Maybe a)
+maybeP p = option H.nothing (H.just <$> p)
+
+manyTill :: Applicable repr => Alternable repr => repr a -> repr b -> repr [a]
+manyTill p end = let go = end $> H.nil <|> p <:> go in go
+
+-- * Class 'Selectable'
+class Selectable repr where
+  branch :: repr (Either a b) -> repr (a -> c) -> repr (b -> c) -> repr c
+  default branch ::
+    Sym.Liftable3 repr => Selectable (Sym.Output repr) =>
+    repr (Either a b) -> repr (a -> c) -> repr (b -> c) -> repr c
+  branch = Sym.lift3 branch
+
+-- * Class 'Matchable'
+class Matchable repr where
+  conditional ::
+    Eq a => [H.Haskell (a -> Bool)] -> [repr b] -> repr a -> repr b -> repr b
+  default conditional ::
+    Sym.Unliftable repr => Sym.Liftable2 repr => Matchable (Sym.Output repr) =>
+    Eq a => [H.Haskell (a -> Bool)] -> [repr b] -> repr a -> repr b -> repr b
+  conditional cs bs = Sym.lift2 (conditional cs (Sym.trans Functor.<$> bs))
+
+  match :: Eq a => [H.Haskell a] -> repr a -> (H.Haskell a -> repr b) -> repr b -> repr b
+  match as a a2b = conditional (H.eq Functor.<$> as) (a2b Functor.<$> as) a
+
+-- * Class 'Foldable'
+class Foldable repr where
+  chainPre :: repr (a -> a) -> repr a -> repr a
+  chainPost :: repr a -> repr (a -> a) -> repr a
+  {-
+  default chainPre ::
+    Sym.Liftable2 repr => Foldable (Sym.Output repr) =>
+    repr (a -> a) -> repr a -> repr a
+  default chainPost ::
+    Sym.Liftable2 repr => Foldable (Sym.Output repr) =>
+    repr a -> repr (a -> a) -> repr a
+  chainPre = Sym.lift2 chainPre
+  chainPost = Sym.lift2 chainPost
+  -}
+  default chainPre ::
+    Applicable repr =>
+    Alternable repr =>
+    repr (a -> a) -> repr a -> repr a
+  default chainPost ::
+    Applicable repr =>
+    Alternable repr =>
+    repr a -> repr (a -> a) -> repr a
+  chainPre op p = go <*> p
+    where go = (H..) <$> op <*> go <|> pure H.id
+  chainPost p op = p <**> go
+    where go = (H..) <$> op <*> go <|> pure H.id
+
+{-
+conditional :: Selectable repr => [(H.Haskell (a -> Bool), repr b)] -> repr a -> repr b -> repr b
+conditional cs p def = match p fs qs def
+  where (fs, qs) = List.unzip cs
+-}
+
+-- * Class 'Satisfiable'
+class Satisfiable repr tok where
+  satisfy :: [ErrorItem tok] -> H.Haskell (tok -> Bool) -> repr tok
+  default satisfy ::
+    Sym.Liftable repr => Satisfiable (Sym.Output repr) tok =>
+    [ErrorItem tok] ->
+    H.Haskell (tok -> Bool) -> repr tok
+  satisfy es = Sym.lift . satisfy es
+
+-- ** Type 'ErrorItem'
+data ErrorItem tok
+  =  ErrorItemToken tok
+  |  ErrorItemLabel String
+  |  ErrorItemEnd
+deriving instance Eq tok => Eq (ErrorItem tok)
+deriving instance Ord tok => Ord (ErrorItem tok)
+deriving instance Show tok => Show (ErrorItem tok)
+deriving instance TH.Lift tok => TH.Lift (ErrorItem tok)
+
+-- * Class 'Lookable'
+class Lookable repr where
+  look :: repr a -> repr a
+  negLook :: repr a -> repr ()
+  default look :: Sym.Liftable1 repr => Lookable (Sym.Output repr) => repr a -> repr a
+  default negLook :: Sym.Liftable1 repr => Lookable (Sym.Output repr) => repr a -> repr ()
+  look = Sym.lift1 look
+  negLook = Sym.lift1 negLook
+
+  eof :: repr ()
+  eof = Sym.lift eof
+  default eof :: Sym.Liftable repr => Lookable (Sym.Output repr) => repr ()
+  -- eof = negLook (satisfy @_ @Char [ErrorItemAny] (H.const H..@ H.bool True))
+             -- (item @_ @Char)
+
+{-# INLINE (<:>) #-}
+infixl 4 <:>
+(<:>) :: Applicable repr => repr a -> repr [a] -> repr [a]
+(<:>) = liftA2 H.cons
+
+sequence :: Applicable repr => [repr a] -> repr [a]
+sequence = List.foldr (<:>) (pure H.nil)
+
+traverse :: Applicable repr => (a -> repr b) -> [a] -> repr [b]
+traverse f = sequence . List.map f
+ -- FIXME: Here hlint suggests to use Control.Monad.mapM,
+ -- but at this point there is no mapM for our own sequence
+
+repeat :: Applicable repr => Int -> repr a -> repr [a]
+repeat n p = traverse (const p) [1..n]
+
+between :: Applicable repr => repr o -> repr c -> repr a -> repr a
+between open close p = open *> p <* close
+
+string :: Applicable repr => Satisfiable repr Char => [Char] -> repr [Char]
+string = traverse char
+
+-- oneOf :: [Char] -> repr Char
+-- oneOf cs = satisfy [] (makeQ (flip elem cs) [||\c -> $$(ofChars cs [||c||])||])
+
+noneOf :: TH.Lift tok => Eq tok => Satisfiable repr tok => [tok] -> repr tok
+noneOf cs = satisfy (ErrorItemToken Functor.<$> cs) (H.Haskell H.ValueCode{..})
+  where
+  value = H.Value (not . flip List.elem cs)
+  code = [||\c -> not $$(ofChars cs [||c||])||]
+
+ofChars :: TH.Lift tok => Eq tok => [tok] -> CodeQ tok -> CodeQ Bool
+ofChars = List.foldr (\c rest qc -> [|| c == $$qc || $$(rest qc) ||]) (const [||False||])
+
+more :: Applicable repr => Satisfiable repr Char => Lookable repr => repr ()
+more = look (void (item @_ @Char))
+
+char :: Applicable repr => Satisfiable repr Char => Char -> repr Char
+char c = satisfy [ErrorItemToken c] (H.eq (H.char c)) $> H.char c
+
+anyChar :: Satisfiable repr Char => repr Char
+anyChar = satisfy [] (H.const H..@ H.bool True)
+
+token ::
+  TH.Lift tok => Eq tok => Applicable repr =>
+  Satisfiable repr tok => tok -> repr tok
+token tok = satisfy [ErrorItemToken tok] (H.eq (H.char tok)) $> H.char tok
+
+tokens ::
+  TH.Lift tok => Eq tok => Applicable repr => Alternable repr =>
+  Satisfiable repr tok => [tok] -> repr [tok]
+tokens = try . traverse token
+
+item :: Satisfiable repr tok => repr tok
+item = satisfy [] (H.const H..@ H.bool True)
+
+-- Composite Combinators
+-- someTill :: repr a -> repr b -> repr [a]
+-- someTill p end = negLook end *> (p <:> manyTill p end)
+
+void :: Applicable repr => repr a -> repr ()
+void p = p *> unit
+
+unit :: Applicable repr => repr ()
+unit = pure H.unit
+
+{-
+constp :: Applicable repr => repr a -> repr (b -> a)
+constp = (H.const <$>)
+
+
+-- Alias Operations
+infixl 1 >>
+(>>) :: Applicable repr => repr a -> repr b -> repr b
+(>>) = (*>)
+
+-- Monoidal Operations
+
+infixl 4 <~>
+(<~>) :: Applicable repr => repr a -> repr b -> repr (a, b)
+(<~>) = liftA2 (H.runtime (,))
+
+infixl 4 <~
+(<~) :: Applicable repr => repr a -> repr b -> repr a
+(<~) = (<*)
+
+infixl 4 ~>
+(~>) :: Applicable repr => repr a -> repr b -> repr b
+(~>) = (*>)
+
+-- Lift Operations
+liftA2 ::
+ Applicable repr =>
+ H.Haskell (a -> b -> c) -> repr a -> repr b -> repr c
+liftA2 f x = (<*>) (fmap f x)
+
+liftA3 ::
+ Applicable repr =>
+ H.Haskell (a -> b -> c -> d) -> repr a -> repr b -> repr c -> repr d
+liftA3 f a b c = liftA2 f a b <*> c
+
+-}
+
+-- Parser Folds
+pfoldr ::
+ Applicable repr => Foldable repr =>
+ H.Haskell (a -> b -> b) -> H.Haskell b -> repr a -> repr b
+pfoldr f k p = chainPre (f <$> p) (pure k)
+
+pfoldr1 ::
+ Applicable repr => Foldable repr =>
+ H.Haskell (a -> b -> b) -> H.Haskell b -> repr a -> repr b
+pfoldr1 f k p = f <$> p <*> pfoldr f k p
+
+pfoldl ::
+ Applicable repr => Foldable repr =>
+ H.Haskell (b -> a -> b) -> H.Haskell b -> repr a -> repr b
+pfoldl f k p = chainPost (pure k) ((H.flip <$> pure f) <*> p)
+
+pfoldl1 ::
+ Applicable repr => Foldable repr =>
+ H.Haskell (b -> a -> b) -> H.Haskell b -> repr a -> repr b
+pfoldl1 f k p = chainPost (f <$> pure k <*> p) ((H.flip <$> pure f) <*> p)
+
+-- Chain Combinators
+chainl1' ::
+ Applicable repr => Foldable repr =>
+ H.Haskell (a -> b) -> repr a -> repr (b -> a -> b) -> repr b
+chainl1' f p op = chainPost (f <$> p) (H.flip <$> op <*> p)
+
+chainl1 ::
+ Applicable repr => Foldable repr =>
+ repr a -> repr (a -> a -> a) -> repr a
+chainl1 = chainl1' H.id
+
+{-
+chainr1' :: ParserOps rep => rep (a -> b) -> repr a -> repr (a -> b -> b) -> repr b
+chainr1' f p op = newRegister_ H.id $ \acc ->
+  let go = bind p $ \x ->
+           modify acc (H.flip (H..@) <$> (op <*> x)) *> go
+       <|> f <$> x
+  in go <**> get acc
+
+chainr1 :: repr a -> repr (a -> a -> a) -> repr a
+chainr1 = chainr1' H.id
+
+chainr :: repr a -> repr (a -> a -> a) -> H.Haskell a -> repr a
+chainr p op x = option x (chainr1 p op)
+-}
+
+chainl ::
+ Applicable repr => Alternable repr => Foldable repr =>
+ repr a -> repr (a -> a -> a) -> H.Haskell a -> repr a
+chainl p op x = option x (chainl1 p op)
+
+-- Derived Combinators
+many ::
+ Applicable repr => Foldable repr =>
+ repr a -> repr [a]
+many = pfoldr H.cons H.nil
+
+manyN ::
+ Applicable repr => Foldable repr =>
+ Int -> repr a -> repr [a]
+manyN n p = List.foldr (const (p <:>)) (many p) [1..n]
+
+some ::
+ Applicable repr => Foldable repr =>
+ repr a -> repr [a]
+some = manyN 1
+
+skipMany ::
+ Applicable repr => Foldable repr =>
+ repr a -> repr ()
+--skipMany p = let skipManyp = p *> skipManyp <|> unit in skipManyp
+skipMany = void . pfoldl H.const H.unit -- the void here will encourage the optimiser to recognise that the register is unused
+
+skipManyN ::
+ Applicable repr => Foldable repr =>
+ Int -> repr a -> repr ()
+skipManyN n p = List.foldr (const (p *>)) (skipMany p) [1..n]
+
+skipSome ::
+ Applicable repr => Foldable repr =>
+ repr a -> repr ()
+skipSome = skipManyN 1
+
+sepBy ::
+ Applicable repr => Alternable repr => Foldable repr =>
+ repr a -> repr b -> repr [a]
+sepBy p sep = option H.nil (sepBy1 p sep)
+
+sepBy1 ::
+ Applicable repr => Alternable repr => Foldable repr =>
+ repr a -> repr b -> repr [a]
+sepBy1 p sep = p <:> many (sep *> p)
+
+endBy ::
+ Applicable repr => Alternable repr => Foldable repr =>
+ repr a -> repr b -> repr [a]
+endBy p sep = many (p <* sep)
+
+endBy1 ::
+ Applicable repr => Alternable repr => Foldable repr =>
+ repr a -> repr b -> repr [a]
+endBy1 p sep = some (p <* sep)
+
+sepEndBy ::
+ Applicable repr => Alternable repr => Foldable repr =>
+ repr a -> repr b -> repr [a]
+sepEndBy p sep = option H.nil (sepEndBy1 p sep)
+
+sepEndBy1 ::
+ Applicable repr => Alternable repr => Foldable repr =>
+ repr a -> repr b -> repr [a]
+sepEndBy1 p sep =
+  let seb1 = p <**> (sep *> (H.flip H..@ H.cons <$> option H.nil seb1)
+                 <|> pure (H.flip H..@ H.cons H..@ H.nil))
+  in seb1
+
+{-
+sepEndBy1 :: repr a -> repr b -> repr [a]
+sepEndBy1 p sep = newRegister_ H.id $ \acc ->
+  let go = modify acc ((H.flip (H..)) H..@ H.cons <$> p)
+         *> (sep *> (go <|> get acc) <|> get acc)
+  in go <*> pure H.nil
+-}
+
+{-
+-- Combinators interpreters for 'Sym.Any'.
+instance Applicable repr => Applicable (Sym.Any repr)
+instance Satisfiable repr => Satisfiable (Sym.Any repr)
+instance Alternable repr => Alternable (Sym.Any repr)
+instance Selectable repr => Selectable (Sym.Any repr)
+instance Matchable repr => Matchable (Sym.Any repr)
+instance Lookable repr => Lookable (Sym.Any repr)
+instance Foldable repr => Foldable (Sym.Any repr)
+-}
diff --git a/src/Symantic/Parser/Grammar/Dump.hs b/src/Symantic/Parser/Grammar/Dump.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Grammar/Dump.hs
@@ -0,0 +1,68 @@
+module Symantic.Parser.Grammar.Dump where
+
+import Data.Function (($), (.), id)
+import Data.Semigroup (Semigroup(..))
+import Data.String (String, IsString(..))
+import Text.Show (Show(..))
+import qualified Control.Applicative as Fct
+import qualified Data.Tree as Tree
+import qualified Data.List as List
+
+import Symantic.Univariant.Letable
+import Symantic.Parser.Grammar.Combinators
+
+-- * Type 'DumpComb'
+newtype DumpComb a = DumpComb { unDumpComb :: Tree.Tree String }
+
+dumpComb :: DumpComb a -> DumpComb a
+dumpComb = id
+
+instance Show (DumpComb a) where
+  show = drawTree . unDumpComb
+    where
+    drawTree :: Tree.Tree String -> String
+    drawTree  = List.unlines . draw
+    draw :: Tree.Tree String -> [String]
+    draw (Tree.Node x ts0) = List.lines x <> drawSubTrees ts0
+      where
+      drawSubTrees [] = []
+      drawSubTrees [t] = shift "` " "  " (draw t)
+      drawSubTrees (t:ts) = shift "+ " "| " (draw t) <> drawSubTrees ts
+      shift first other = List.zipWith (<>) (first : List.repeat other)
+instance IsString (DumpComb a) where
+  fromString s = DumpComb $ Tree.Node (fromString s) []
+
+instance Show letName => Letable letName DumpComb where
+  def name x = DumpComb $
+    Tree.Node ("def "<>show name) [unDumpComb x]
+  ref rec name = DumpComb $
+    Tree.Node
+      ( (if rec then "rec " else "ref ")
+      <> show name
+      ) []
+instance Applicable DumpComb where
+  _f <$> x = DumpComb $ Tree.Node "<$>" [unDumpComb x]
+  pure a = DumpComb $ Tree.Node ("pure "<>showsPrec 10 a "") []
+  x <*> y = DumpComb $ Tree.Node "<*>" [unDumpComb x, unDumpComb y]
+instance Alternable DumpComb where
+  empty = DumpComb $ Tree.Node "empty" []
+  x <|> y = DumpComb $ Tree.Node "<|>" [unDumpComb x, unDumpComb y]
+  try x = DumpComb $ Tree.Node "try" [unDumpComb x]
+instance Satisfiable DumpComb tok where
+  satisfy _es _p = DumpComb $ Tree.Node "satisfy" []
+instance Selectable DumpComb where
+  branch lr l r = DumpComb $ Tree.Node "branch"
+    [ unDumpComb lr, unDumpComb l, unDumpComb r ]
+instance Matchable DumpComb where
+  conditional _cs bs a b = DumpComb $ Tree.Node "conditional"
+    [ Tree.Node "bs" (unDumpComb Fct.<$> bs)
+    , unDumpComb a
+    , unDumpComb b
+    ]
+instance Lookable DumpComb where
+  look x = DumpComb $ Tree.Node "look" [unDumpComb x]
+  negLook x = DumpComb $ Tree.Node "negLook" [unDumpComb x]
+  eof = DumpComb $ Tree.Node "eof" []
+instance Foldable DumpComb where
+  chainPre f x = DumpComb $ Tree.Node "chainPre" [unDumpComb f, unDumpComb x]
+  chainPost x f = DumpComb $ Tree.Node "chainPost" [unDumpComb x, unDumpComb f]
diff --git a/src/Symantic/Parser/Grammar/Fixity.hs b/src/Symantic/Parser/Grammar/Fixity.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Grammar/Fixity.hs
@@ -0,0 +1,115 @@
+module Symantic.Parser.Grammar.Fixity where
+
+import Data.Bool
+import Data.Eq (Eq(..))
+import Data.Function ((.))
+import Data.Int (Int)
+import Data.Maybe (Maybe(..))
+import Data.Ord (Ord(..))
+import Data.Semigroup
+import Data.String (String, IsString(..))
+import Text.Show (Show(..))
+
+-- * Type 'Fixity'
+data Fixity
+ =   Fixity1 Unifix
+ |   Fixity2 Infix
+ deriving (Eq, Show)
+
+-- ** Type 'Unifix'
+data Unifix
+ =   Prefix  { unifix_precedence :: Precedence }
+ |   Postfix { unifix_precedence :: Precedence }
+ deriving (Eq, Show)
+
+-- ** Type 'Infix'
+data Infix
+ =   Infix
+ {   infix_associativity :: Maybe Associativity
+ ,   infix_precedence    :: Precedence
+ } deriving (Eq, Show)
+
+infixL :: Precedence -> Infix
+infixL = Infix (Just AssocL)
+
+infixR :: Precedence -> Infix
+infixR = Infix (Just AssocR)
+
+infixB :: Side -> Precedence -> Infix
+infixB = Infix . Just . AssocB
+
+infixN :: Precedence -> Infix
+infixN = Infix Nothing
+
+infixN0 :: Infix
+infixN0 = infixN 0
+
+infixN5 :: Infix
+infixN5 = infixN 5
+
+-- | Given 'Precedence' and 'Associativity' of its parent operator,
+-- and the operand 'Side' it is in,
+-- return whether an 'Infix' operator
+-- needs to be enclosed by a 'Pair'.
+isPairNeeded :: (Infix, Side) -> Infix -> Bool
+isPairNeeded (po, lr) op =
+  infix_precedence op < infix_precedence po
+  || infix_precedence op == infix_precedence po
+  && not associate
+  where
+  associate =
+    case (lr, infix_associativity po) of
+     (_, Just AssocB{})   -> True
+     (SideL, Just AssocL) -> True
+     (SideR, Just AssocR) -> True
+     _ -> False
+
+-- | If 'isPairNeeded' is 'True',
+-- enclose the given 'IsString' by given 'Pair',
+-- otherwise returns the same 'IsString'.
+pairIfNeeded ::
+ Semigroup s => IsString s =>
+ Pair -> (Infix, Side) -> Infix ->
+ s -> s
+pairIfNeeded (o,c) po op s =
+  if isPairNeeded po op
+  then fromString o <> s <> fromString c
+  else s
+
+-- * Type 'Precedence'
+type Precedence = Int
+
+-- ** Class 'PrecedenceOf'
+class PrecedenceOf a where
+  precedence :: a -> Precedence
+instance PrecedenceOf Fixity where
+  precedence (Fixity1 uni) = precedence uni
+  precedence (Fixity2 inf) = precedence inf
+instance PrecedenceOf Unifix where
+  precedence = unifix_precedence
+instance PrecedenceOf Infix where
+  precedence = infix_precedence
+
+-- * Type 'Associativity'
+data Associativity
+ =   AssocL      -- ^ Associate to the left:  @a ¹ b ² c == (a ¹ b) ² c@
+ |   AssocR      -- ^ Associate to the right: @a ¹ b ² c == a ¹ (b ² c)@
+ |   AssocB Side -- ^ Associate to both sides, but to 'Side' when reading.
+ deriving (Eq, Show)
+
+-- ** Type 'Side'
+data Side
+ =   SideL -- ^ Left
+ |   SideR -- ^ Right
+ deriving (Eq, Show)
+
+-- ** Type 'Pair'
+type Pair = (String, String)
+pairAngle   :: Pair
+pairBrace   :: Pair
+pairBracket :: Pair
+pairParen   :: Pair
+pairAngle   = ("<",">")
+pairBrace   = ("{","}")
+pairBracket = ("[","]")
+pairParen   = ("(",")")
diff --git a/src/Symantic/Parser/Grammar/ObserveSharing.hs b/src/Symantic/Parser/Grammar/ObserveSharing.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Grammar/ObserveSharing.hs
@@ -0,0 +1,107 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Symantic.Parser.Grammar.ObserveSharing
+ ( module Symantic.Parser.Grammar.ObserveSharing
+ , ObserveSharing(..)
+ ) where
+
+import Control.Monad (mapM)
+import Control.Applicative (Applicative(..))
+import Data.Eq (Eq(..))
+import Data.Function (($), (.))
+import Data.Functor ((<$>))
+import Data.Hashable (Hashable, hashWithSalt)
+import Text.Show (Show(..))
+
+import Symantic.Univariant.Letable as Letable
+import qualified Symantic.Univariant.Trans as Sym
+import qualified Symantic.Parser.Grammar.Combinators as Comb
+import qualified Language.Haskell.TH.Syntax as TH
+
+-- | Like 'Letable.observeSharing'
+-- but type-binding @(letName)@ to 'TH.Name' to help type inference.
+observeSharing :: ObserveSharing TH.Name repr a -> repr a
+observeSharing = Letable.observeSharing
+
+instance Hashable TH.Name where
+  hashWithSalt s = hashWithSalt s . show
+
+-- Combinators semantics for the 'ObserveSharing' interpreter
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Comb.Satisfiable repr tok
+  ) => Comb.Satisfiable (ObserveSharing letName repr) tok
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Comb.Alternable repr
+  ) => Comb.Alternable (ObserveSharing letName repr)
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Comb.Applicable repr
+  ) => Comb.Applicable (ObserveSharing letName repr)
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Comb.Selectable repr
+  ) => Comb.Selectable (ObserveSharing letName repr)
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Comb.Matchable repr
+  ) => Comb.Matchable (ObserveSharing letName repr) where
+  -- Here the default definition does not fit
+  -- since there is no lift* for the type of 'conditional'
+  -- and its default definition handles does not handles 'bs'
+  -- as needed by the 'ObserveSharing' transformation.
+  conditional cs bs a b = observeSharingNode $ ObserveSharing $
+    Comb.conditional cs
+      <$> mapM unObserveSharing bs
+      <*> unObserveSharing a
+      <*> unObserveSharing b
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Comb.Foldable repr
+  {- TODO: the following constraints are for the current Foldable,
+   - they will have to be removed when Foldable will have Sym.lift2 as defaults
+   -}
+  , Comb.Applicable repr
+  , Comb.Alternable repr
+  ) => Comb.Foldable (ObserveSharing letName repr)
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  , Comb.Lookable repr
+  ) => Comb.Lookable (ObserveSharing letName repr)
+
+-- Combinators semantics for the 'CleanDefs' interpreter
+instance Comb.Applicable repr => Comb.Applicable (CleanDefs letName repr)
+instance Comb.Alternable repr => Comb.Alternable (CleanDefs letName repr)
+instance Comb.Satisfiable repr tok => Comb.Satisfiable (CleanDefs letName repr) tok
+instance Comb.Selectable repr => Comb.Selectable (CleanDefs letName repr)
+instance Comb.Matchable repr => Comb.Matchable (CleanDefs letName repr) where
+  conditional cs bs a b = CleanDefs $
+    Comb.conditional cs
+      <$> mapM unCleanDefs bs
+      <*> unCleanDefs a
+      <*> unCleanDefs b
+instance Comb.Lookable repr => Comb.Lookable (CleanDefs letName repr)
+instance Comb.Foldable repr => Comb.Foldable (CleanDefs letName repr) where
+  chainPre = Sym.lift2 Comb.chainPre
+  chainPost = Sym.lift2 Comb.chainPost
diff --git a/src/Symantic/Parser/Grammar/Optimize.hs b/src/Symantic/Parser/Grammar/Optimize.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Grammar/Optimize.hs
@@ -0,0 +1,440 @@
+{-# LANGUAGE PatternSynonyms #-} -- For aliased combinators
+{-# LANGUAGE TemplateHaskell #-} -- For optimizeCombNode
+{-# LANGUAGE ViewPatterns #-} -- For optimizeCombNode
+{-# OPTIONS_GHC -fno-warn-orphans #-} -- For MakeLetName TH.Name
+module Symantic.Parser.Grammar.Optimize where
+
+import Data.Bool (Bool(..))
+import Data.Either (Either(..), either)
+import Data.Eq (Eq(..))
+import Data.Foldable (all, foldr)
+import Data.Function ((.))
+import Data.Kind (Type)
+import qualified Data.Functor as Functor
+import qualified Data.List as List
+import qualified Language.Haskell.TH.Syntax as TH
+
+import Symantic.Parser.Grammar.Combinators as Comb
+import Symantic.Parser.Haskell (ValueCode(..), Value(..), getValue, code)
+import Symantic.Univariant.Letable
+import Symantic.Univariant.Trans
+import qualified Symantic.Parser.Haskell as H
+
+-- import Debug.Trace (trace)
+
+-- * Type 'Comb'
+-- | Pattern-matchable 'Comb'inators of the grammar.
+-- @(repr)@ is not strictly necessary since it's only a phantom type
+-- (no constructor use it as a value), but having it:
+--
+-- 1. emphasizes that those 'Comb'inators will be 'trans'formed again
+--    (eg. in 'DumpComb' or 'Instr'uctions).
+--
+-- 2. Avoid overlapping instances between
+--    @('Trans' ('Comb' repr) repr)@ and
+--    @('Trans' ('Comb' repr) ('OptimizeComb' letName repr))@
+data Comb (repr :: Type -> Type) a where
+  Pure :: H.Haskell a -> Comb repr a
+  Satisfy ::
+    Satisfiable repr tok =>
+    [ErrorItem tok] ->
+    H.Haskell (tok -> Bool) -> Comb repr tok
+  Item :: Satisfiable repr tok => Comb repr tok
+  Try :: Comb repr a -> Comb repr a
+  Look :: Comb repr a -> Comb repr a
+  NegLook :: Comb repr a -> Comb repr ()
+  Eof :: Comb repr ()
+  (:<*>) :: Comb repr (a -> b) -> Comb repr a -> Comb repr b
+  (:<|>) :: Comb repr a -> Comb repr a -> Comb repr a
+  Empty :: Comb repr a
+  Branch ::
+    Comb repr (Either a b) ->
+    Comb repr (a -> c) -> Comb repr (b -> c) -> Comb repr c
+  Match :: Eq a =>
+    [H.Haskell (a -> Bool)] ->
+    [Comb repr b] -> Comb repr a -> Comb repr b -> Comb repr b
+  ChainPre :: Comb repr (a -> a) -> Comb repr a -> Comb repr a
+  ChainPost :: Comb repr a -> Comb repr (a -> a) -> Comb repr a
+  Def :: TH.Name -> Comb repr a -> Comb repr a
+  Ref :: Bool -> TH.Name -> Comb repr a
+
+pattern (:<$>) :: H.Haskell (a -> b) -> Comb repr a -> Comb repr b
+pattern (:$>) :: Comb repr a -> H.Haskell b -> Comb repr b
+pattern (:<$) :: H.Haskell a -> Comb repr b -> Comb repr a
+pattern (:*>) :: Comb repr a -> Comb repr b -> Comb repr b
+pattern (:<*) :: Comb repr a -> Comb repr b -> Comb repr a
+pattern x :<$> p = Pure x :<*> p
+pattern p :$> x = p :*> Pure x
+pattern x :<$ p = Pure x :<* p
+pattern x :<* p = H.Const :<$> x :<*> p
+pattern p :*> x = H.Id :<$ p :<*> x
+
+infixl 3 :<|>
+infixl 4 :<*>, :<*, :*>
+infixl 4 :<$>, :<$, :$>
+
+instance Applicable (Comb repr) where
+  pure = Pure
+  (<*>) = (:<*>)
+instance Alternable (Comb repr) where
+  (<|>) = (:<|>)
+  empty = Empty
+  try = Try
+instance Selectable (Comb repr) where
+  branch = Branch
+instance Matchable (Comb repr) where
+  conditional = Match
+instance Foldable (Comb repr) where
+  chainPre = ChainPre
+  chainPost = ChainPost
+instance Satisfiable repr tok => Satisfiable (Comb repr) tok where
+  satisfy = Satisfy
+instance Lookable (Comb repr) where
+  look = Look
+  negLook = NegLook
+  eof = Eof
+instance Letable TH.Name (Comb repr) where
+  def = Def
+  ref = Ref
+instance MakeLetName TH.Name where
+  makeLetName _ = TH.qNewName "name"
+
+-- Pattern-matchable 'Comb'inators keep enough structure
+-- to have some of the symantics producing them interpreted again
+-- (eg. after being modified by 'optimizeComb').
+type instance Output (Comb repr) = repr
+instance
+  ( Applicable repr
+  , Alternable repr
+  , Selectable repr
+  , Foldable repr
+  , Lookable repr
+  , Matchable repr
+  , Letable TH.Name repr
+  ) => Trans (Comb repr) repr where
+  trans = \case
+    Pure a -> pure a
+    Satisfy es p -> satisfy es p
+    Item -> item
+    Try x -> try (trans x)
+    Look x -> look (trans x)
+    NegLook x -> negLook (trans x)
+    Eof -> eof
+    x :<*> y -> trans x <*> trans y
+    x :<|> y -> trans x <|> trans y
+    Empty -> empty
+    Branch lr l r -> branch (trans lr) (trans l) (trans r)
+    Match ps bs a b -> conditional ps (trans Functor.<$> bs) (trans a) (trans b)
+    ChainPre x y -> chainPre (trans x) (trans y)
+    ChainPost x y -> chainPost (trans x) (trans y)
+    Def n x -> def n (trans x)
+    Ref r n -> ref r n
+
+-- * Type 'OptimizeComb'
+-- Bottom-up application of 'optimizeCombNode'.
+newtype OptimizeComb letName repr a =
+        OptimizeComb { unOptimizeComb :: Comb repr a }
+
+optimizeComb ::
+  Trans (OptimizeComb TH.Name repr) repr =>
+  OptimizeComb TH.Name repr a -> repr a
+optimizeComb = trans
+instance
+  Trans (Comb repr) repr =>
+  Trans (OptimizeComb letName repr) repr where
+  trans = trans . unOptimizeComb
+
+type instance Output (OptimizeComb _letName repr) = Comb repr
+instance Trans (OptimizeComb letName repr) (Comb repr) where
+  trans = unOptimizeComb
+instance Trans (Comb repr) (OptimizeComb letName repr) where
+  trans = OptimizeComb . optimizeCombNode
+instance Trans1 (Comb repr) (OptimizeComb letName repr)
+instance Trans2 (Comb repr) (OptimizeComb letName repr)
+instance Trans3 (Comb repr) (OptimizeComb letName repr)
+
+instance
+  Letable letName (Comb repr) =>
+  Letable letName (OptimizeComb letName repr) where
+  -- Disable useless calls to 'optimizeCombNode'
+  -- because 'Def' or 'Ref' have no matching in it.
+  def n = OptimizeComb . def n . unOptimizeComb
+  ref r n = OptimizeComb (ref r n)
+instance Comb.Applicable (OptimizeComb letName repr)
+instance Comb.Alternable (OptimizeComb letName repr)
+instance Comb.Satisfiable repr tok =>
+         Comb.Satisfiable (OptimizeComb letName repr) tok
+instance Comb.Selectable (OptimizeComb letName repr)
+instance Comb.Matchable (OptimizeComb letName repr)
+instance Comb.Lookable (OptimizeComb letName repr)
+instance Comb.Foldable (OptimizeComb letName repr)
+
+optimizeCombNode :: Comb repr a -> Comb repr a
+optimizeCombNode = \case
+  -- Functor Identity Law
+  H.Id :<$> x ->
+    -- trace "Functor Identity Law" $
+    x
+  -- Functor Commutativity Law
+  x :<$ u ->
+    -- trace "Functor Commutativity Law" $
+    optimizeCombNode (u :$> x)
+  -- Functor Flip Const Law
+  H.Flip H.:@ H.Const :<$> u ->
+    -- trace "Functor Flip Const Law" $
+    optimizeCombNode (u :*> Pure H.Id)
+  -- Functor Homomorphism Law
+  f :<$> Pure x ->
+    -- trace "Functor Homomorphism Law" $
+    Pure (f H..@ x)
+
+  -- App Right Absorption Law
+  Empty :<*> _ ->
+    -- trace "App Right Absorption Law" $
+    Empty
+  _ :<*> Empty ->
+    -- In Parsley: this is only a weakening to u :*> Empty
+    -- but here :*> is an alias to :<*>
+    -- hence it would loop on itself forever.
+    -- trace "App Left Absorption Law" $
+    Empty
+  -- App Composition Law
+  u :<*> (v :<*> w) ->
+    -- trace "App Composition Law" $
+    optimizeCombNode (optimizeCombNode (optimizeCombNode ((H.:.) :<$> u) :<*> v) :<*> w)
+  -- App Interchange Law
+  u :<*> Pure x ->
+    -- trace "App Interchange Law" $
+    optimizeCombNode (H.Flip H..@ (H.:$) H..@ x :<$> u)
+  -- App Left Absorption Law
+  p :<* (_ :<$> q) ->
+    -- trace "App Left Absorption Law" $
+    p :<* q
+  -- App Right Absorption Law
+  (_ :<$> p) :*> q ->
+    -- trace "App Right Absorption Law" $
+    p :*> q
+  -- App Pure Left Identity Law
+  Pure _ :*> u ->
+    -- trace "App Pure Left Identity Law" $
+    u
+  -- App Functor Left Identity Law
+  (u :$> _) :*> v ->
+    -- trace "App Functor Left Identity Law" $
+    u :*> v
+  -- App Pure Right Identity Law
+  u :<* Pure _ ->
+    -- trace "App Pure Right Identity Law" $
+    u
+  -- App Functor Right Identity Law
+  u :<* (v :$> _) ->
+    -- trace "App Functor Right Identity Law" $
+    optimizeCombNode (u :<* v)
+  -- App Left Associativity Law
+  (u :<* v) :<* w ->
+    -- trace "App Left Associativity Law" $
+    optimizeCombNode (u :<* optimizeCombNode (v :<* w))
+
+  -- Alt Left CatchFail Law
+  p@Pure{} :<|> _ ->
+    -- trace "Alt Left CatchFail Law" $
+    p
+  -- Alt Left Neutral Law
+  Empty :<|> u ->
+    -- trace "Alt Left Neutral Law" $
+    u
+  -- All Right Neutral Law
+  u :<|> Empty ->
+    -- trace "Alt Right Neutral Law" $
+    u
+  -- Alt Associativity Law
+  (u :<|> v) :<|> w ->
+    -- trace "Alt Associativity Law" $
+    u :<|> optimizeCombNode (v :<|> w)
+
+  -- Look Pure Law
+  Look p@Pure{} ->
+    -- trace "Look Pure Law" $
+    p
+  -- Look Empty Law
+  Look p@Empty ->
+    -- trace "Look Empty Law" $
+    p
+  -- NegLook Pure Law
+  NegLook Pure{} ->
+    -- trace "NegLook Pure Law" $
+    Empty
+  -- NegLook Empty Law
+  NegLook Empty ->
+    -- trace "NegLook Dead Law" $
+    Pure H.unit
+  -- NegLook Double Negation Law
+  NegLook (NegLook p) ->
+    -- trace "NegLook Double Negation Law" $
+    optimizeCombNode (Look (Try p) :*> Pure H.unit)
+  -- NegLook Zero Consumption Law
+  NegLook (Try p) ->
+    -- trace "NegLook Zero Consumption Law" $
+    optimizeCombNode (NegLook p)
+  -- Idempotence Law
+  Look (Look p) ->
+    -- trace "Look Idempotence Law" $
+    Look p
+  -- Look Right Identity Law
+  NegLook (Look p) ->
+    -- trace "Look Right Identity Law" $
+    optimizeCombNode (NegLook p)
+  -- Look Left Identity Law
+  Look (NegLook p) ->
+    -- trace "Look Left Identity Law" $
+    NegLook p
+  -- NegLook Transparency Law
+  NegLook (Try p :<|> q) ->
+    -- trace "NegLook Transparency Law" $
+    optimizeCombNode (optimizeCombNode (NegLook p) :*> optimizeCombNode (NegLook q))
+  -- Look Distributivity Law
+  Look p :<|> Look q ->
+    -- trace "Look Distributivity Law" $
+    optimizeCombNode (Look (optimizeCombNode (Try p :<|> q)))
+  -- Look Interchange Law
+  Look (f :<$> p) ->
+    -- trace "Look Interchange Law" $
+    optimizeCombNode (f :<$> optimizeCombNode (Look p))
+  -- NegLook Idempotence Right Law
+  NegLook (_ :<$> p) ->
+    -- trace "NegLook Idempotence Law" $
+    optimizeCombNode (NegLook p)
+  -- Try Interchange Law
+  Try (f :<$> p) ->
+    -- trace "Try Interchange Law" $
+    optimizeCombNode (f :<$> optimizeCombNode (Try p))
+
+  -- Branch Absorption Law
+  Branch Empty _ _ ->
+    -- trace "Branch Absorption Law" $
+    empty
+  -- Branch Weakening Law
+  Branch b Empty Empty ->
+    -- trace "Branch Weakening Law" $
+    optimizeCombNode (b :*> Empty)
+  -- Branch Pure Left/Right Laws
+  Branch (Pure (trans -> lr)) l r ->
+    -- trace "Branch Pure Left/Right Law" $
+    case getValue lr of
+     Left v -> optimizeCombNode (l :<*> Pure (H.Haskell (ValueCode (Value v) c)))
+      where c = [|| case $$(code lr) of Left x -> x ||]
+     Right v -> optimizeCombNode (r :<*> Pure (H.Haskell (ValueCode (Value v) c)))
+      where c = [|| case $$(code lr) of Right x -> x ||]
+  -- Branch Generalised Identity Law
+  Branch b (Pure (trans -> l)) (Pure (trans -> r)) ->
+    -- trace "Branch Generalised Identity Law" $
+    optimizeCombNode (H.Haskell (ValueCode v c) :<$> b)
+    where
+    v = Value (either (getValue l) (getValue r))
+    c = [|| either $$(code l) $$(code r) ||]
+  -- Branch Interchange Law
+  Branch (x :*> y) p q ->
+    -- trace "Branch Interchange Law" $
+    optimizeCombNode (x :*> optimizeCombNode (Branch y p q))
+  -- Branch Empty Right Law
+  Branch b l Empty ->
+    -- trace " Branch Empty Right Law" $
+    Branch (Pure (H.Haskell (ValueCode v c)) :<*> b) Empty l
+    where
+    v = Value (either Right Left)
+    c = [||either Right Left||]
+  -- Branch Fusion Law
+  Branch (Branch b Empty (Pure (trans -> lr))) Empty br ->
+    -- trace "Branch Fusion Law" $
+    optimizeCombNode (Branch (optimizeCombNode (Pure (H.Haskell (ValueCode (Value v) c)) :<*> b))
+                             Empty br)
+    where
+    v Left{} = Left ()
+    v (Right r) = case getValue lr r of
+                   Left _ -> Left ()
+                   Right rr -> Right rr
+    c = [|| \case Left{} -> Left ()
+                  Right r -> case $$(code lr) r of
+                              Left _ -> Left ()
+                              Right rr -> Right rr ||]
+  -- Branch Distributivity Law
+  f :<$> Branch b l r ->
+    -- trace "Branch Distributivity Law" $
+    optimizeCombNode (Branch b (optimizeCombNode ((H..@) (H..) f :<$> l))
+                               (optimizeCombNode ((H..@) (H..) f :<$> r)))
+
+  -- Match Absorption Law
+  Match _ _ Empty d ->
+    -- trace "Match Absorption Law" $
+    d
+  -- Match Weakening Law
+  Match _ bs a Empty
+    | all (\case {Empty -> True; _ -> False}) bs ->
+      -- trace "Match Weakening Law" $
+      optimizeCombNode (a :*> Empty)
+  -- Match Pure Law
+  Match ps bs (Pure (trans -> a)) d ->
+    -- trace "Match Pure Law" $
+    foldr (\(trans -> p, b) next ->
+      if getValue p (getValue a) then b else next
+    ) d (List.zip ps bs)
+  -- Match Distributivity Law
+  f :<$> Match ps bs a d ->
+    -- trace "Match Distributivity Law" $
+    Match ps (optimizeCombNode . (f :<$>) Functor.<$> bs) a
+             (optimizeCombNode (f :<$> d))
+
+  {- Possibly useless laws to be tested
+  Empty  :*> _ -> Empty
+  Empty :<*  _ -> Empty
+  -- App Definition of *> Law
+  H.Flip H..@ H.Const :<$> p :<*> q ->
+    -- -- trace "EXTRALAW: App Definition of *> Law" $
+    p :*> q
+  -- App Definition of <* Law
+  H.Const :<$> p :<*> q ->
+    -- -- trace "EXTRALAW: App Definition of <* Law" $
+    p :<* q
+
+  -- Functor Composition Law
+  -- (a shortcut that could also have been be caught
+  -- by the Composition Law and Homomorphism Law)
+  f :<$> (g :<$> p) ->
+    -- -- trace "EXTRALAW: Functor Composition Law" $
+    optimizeCombNode ((H.:.) H..@ f H..@ g :<$> p)
+  -- Applicable Failure Weakening Law
+  u :<*  Empty ->
+    -- -- trace "EXTRALAW: App Failure Weakening Law" $
+    optimizeCombNode (u :*> Empty)
+  Try (p :$> x) ->
+    -- -- trace "EXTRALAW: Try Interchange Right Law" $
+    optimizeCombNode (optimizeCombNode (Try p) :$> x)
+  -- App Reassociation Law 1
+  (u :*> v) :<*> w ->
+    -- -- trace "EXTRALAW: App Reassociation Law 1" $
+    optimizeCombNode (u :*> optimizeCombNode (v :<*> w))
+  -- App Reassociation Law 2
+  u :<*> (v :<* w) ->
+    -- -- trace "EXTRALAW: App Reassociation Law 2" $
+    optimizeCombNode (optimizeCombNode (u :<*> v) :<* w)
+  -- App Right Associativity Law
+  u :*> (v :*> w) ->
+    -- -- trace "EXTRALAW: App Right Associativity Law" $
+    optimizeCombNode (optimizeCombNode (u :*> v) :*> w)
+  -- App Reassociation Law 3
+  u :<*> (v :$> x) ->
+    -- -- trace "EXTRALAW: App Reassociation Law 3" $
+    optimizeCombNode (optimizeCombNode (u :<*> Pure x) :<* v)
+
+  Look (p :$> x) ->
+    optimizeCombNode (optimizeCombNode (Look p) :$> x)
+  NegLook (p :$> _) -> optimizeCombNode (NegLook p)
+
+  -- NegLook Absorption Law
+  p :<*> NegLook q ->
+    -- trace "EXTRALAW: Neglook Absorption Law" $
+    optimizeCombNode (optimizeCombNode (p :<*> Pure H.unit) :<* NegLook q)
+    -- Infinite loop, because :<* expands to :<*>
+  -}
+
+  x -> x
diff --git a/src/Symantic/Parser/Grammar/Write.hs b/src/Symantic/Parser/Grammar/Write.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Grammar/Write.hs
@@ -0,0 +1,152 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Symantic.Parser.Grammar.Write where
+
+import Control.Monad (Monad(..))
+import Data.Function (($))
+import Data.Maybe (Maybe(..), fromMaybe, catMaybes)
+import Data.Monoid (Monoid(..))
+import Data.Semigroup (Semigroup(..))
+import Data.String (IsString(..))
+import Text.Show (Show(..))
+import qualified Data.Functor as Pre
+import qualified Data.List as List
+import qualified Data.Text.Lazy as TL
+import qualified Data.Text.Lazy.Builder as TLB
+
+import Symantic.Univariant.Letable
+import Symantic.Parser.Grammar.Combinators
+import Symantic.Parser.Grammar.Fixity
+
+-- * Type 'WriteComb'
+newtype WriteComb a = WriteComb { unWriteComb :: WriteCombInh -> Maybe TLB.Builder }
+
+instance IsString (WriteComb a) where
+  fromString s = WriteComb $ \_inh ->
+    if List.null s then Nothing
+    else Just (fromString s)
+
+-- ** Type 'WriteCombInh'
+data WriteCombInh
+ =   WriteCombInh
+ {   writeCombInh_indent :: TLB.Builder
+ ,   writeCombInh_op :: (Infix, Side)
+ ,   writeCombInh_pair :: Pair
+ }
+
+emptyWriteCombInh :: WriteCombInh
+emptyWriteCombInh = WriteCombInh
+ { writeCombInh_indent = "\n"
+ , writeCombInh_op = (infixN0, SideL)
+ , writeCombInh_pair = pairParen
+ }
+
+writeComb :: WriteComb a -> TL.Text
+writeComb (WriteComb r) = TLB.toLazyText $ fromMaybe "" $ r emptyWriteCombInh
+
+pairWriteCombInh ::
+ Semigroup s => IsString s =>
+ WriteCombInh -> Infix -> Maybe s -> Maybe s
+pairWriteCombInh inh op s =
+  if isPairNeeded (writeCombInh_op inh) op
+  then Just (fromString o<>" ")<>s<>Just (" "<>fromString c)
+  else s
+  where (o,c) = writeCombInh_pair inh
+
+instance Show letName => Letable letName WriteComb where
+  def name x = WriteComb $ \inh ->
+    pairWriteCombInh inh op $
+      Just "def "
+      <> Just (fromString (show name))
+      <> unWriteComb x inh
+    where
+    op = infixN 9
+  ref rec name = WriteComb $ \inh ->
+    pairWriteCombInh inh op $
+      Just (if rec then "rec " else "ref ") <>
+      Just (fromString (show name))
+    where
+    op = infixN 9
+instance Applicable WriteComb where
+  pure _ = WriteComb $ return Nothing
+  -- pure _ = "pure"
+  WriteComb x <*> WriteComb y = WriteComb $ \inh ->
+    let inh' side = inh
+         { writeCombInh_op = (op, side)
+         , writeCombInh_pair = pairParen
+         } in
+    case x (inh' SideL) of
+     Nothing -> y (inh' SideR)
+     Just xt ->
+      case y (inh' SideR) of
+       Nothing -> Just xt
+       Just yt ->
+        pairWriteCombInh inh op $
+          Just $ xt <> ", " <> yt
+    where
+    op = infixN 1
+instance Alternable WriteComb where
+  empty = "empty"
+  try x = WriteComb $ \inh ->
+    pairWriteCombInh inh op $
+      Just "try " <> unWriteComb x inh
+    where
+    op = infixN 9
+  x <|> y = WriteComb $ \inh ->
+    pairWriteCombInh inh op $
+    unWriteComb x inh
+     { writeCombInh_op = (op, SideL)
+     , writeCombInh_pair = pairParen
+     } <>
+    Just " | " <>
+    unWriteComb y inh
+     { writeCombInh_op = (op, SideR)
+     , writeCombInh_pair = pairParen
+     }
+    where op = infixB SideL 3
+instance Satisfiable WriteComb tok where
+  satisfy _es _f = "satisfy"
+instance Selectable WriteComb where
+  branch lr l r = WriteComb $ \inh ->
+    pairWriteCombInh inh op $
+      Just "branch " <>
+      unWriteComb lr inh <> Just " " <>
+      unWriteComb l inh <> Just " " <>
+      unWriteComb r inh
+    where
+    op = infixN 9
+instance Matchable WriteComb where
+  conditional _ps bs a d = WriteComb $ \inh ->
+    pairWriteCombInh inh op $
+      Just "conditional " <>
+      Just "[" <>
+      Just (mconcat (List.intersperse ", " $
+      catMaybes $ (Pre.<$> bs) $ \x ->
+        unWriteComb x inh{writeCombInh_op=(infixN 0, SideL)})) <>
+      Just "] " <>
+      unWriteComb a inh <> Just " " <>
+      unWriteComb d inh
+    where
+    op = infixN 9
+instance Lookable WriteComb where
+  look x = WriteComb $ \inh ->
+    pairWriteCombInh inh op $
+      Just "look " <> unWriteComb x inh
+    where op = infixN 9
+  negLook x = WriteComb $ \inh ->
+    pairWriteCombInh inh op $
+      Just "negLook " <> unWriteComb x inh
+    where op = infixN 9
+  eof = "eof"
+instance Foldable WriteComb where
+  chainPre f x = WriteComb $ \inh ->
+    pairWriteCombInh inh op $
+      Just "chainPre " <>
+      unWriteComb f inh <> Just " " <>
+      unWriteComb x inh
+    where op = infixN 9
+  chainPost f x = WriteComb $ \inh ->
+    pairWriteCombInh inh op $
+      Just "chainPost " <>
+      unWriteComb f inh <> Just " " <>
+      unWriteComb x inh
+    where op = infixN 9
diff --git a/src/Symantic/Parser/Haskell.hs b/src/Symantic/Parser/Haskell.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Haskell.hs
@@ -0,0 +1,215 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TemplateHaskell #-}
+-- | Haskell terms which are interesting
+-- to pattern-match when optimizing.
+module Symantic.Parser.Haskell where
+
+import Data.Bool (Bool(..))
+import Data.Either (Either(..))
+import Data.Eq (Eq)
+import Data.Maybe (Maybe(..))
+import Data.Ord (Ord(..))
+import Data.Kind (Type)
+import Text.Show (Show(..), showParen, showString)
+import qualified Data.Eq as Eq
+import qualified Data.Function as Function
+import qualified Language.Haskell.TH as TH
+import qualified Language.Haskell.TH.Syntax as TH
+
+import Symantic.Univariant.Trans
+
+-- * Type 'ValueCode'
+-- | Compile-time 'value' and corresponding 'code'
+-- (that can produce that value at runtime).
+data ValueCode a = ValueCode
+  { value :: Value a
+  , code :: TH.CodeQ a
+  }
+getValue :: ValueCode a -> a
+getValue = unValue Function.. value
+getCode :: ValueCode a -> TH.CodeQ a
+getCode = code
+
+-- ** Type 'Value'
+newtype Value a = Value { unValue :: a }
+
+-- * Class 'Haskellable'
+-- | Final encoding of some Haskell functions
+-- useful for some optimizations in 'optimizeComb'.
+class Haskellable (repr :: Type -> Type) where
+  (.) :: repr ((b->c) -> (a->b) -> a -> c)
+  ($) :: repr ((a->b) -> a -> b)
+  (.@) :: repr (a->b) -> repr a -> repr b
+  bool :: Bool -> repr Bool
+  char :: TH.Lift tok => tok -> repr tok
+  cons :: repr (a -> [a] -> [a])
+  const :: repr (a -> b -> a)
+  eq :: Eq a => repr a -> repr (a -> Bool)
+  flip :: repr ((a -> b -> c) -> b -> a -> c)
+  id :: repr (a->a)
+  nil :: repr [a]
+  unit :: repr ()
+  left :: repr (l -> Either l r)
+  right :: repr (r -> Either l r)
+  nothing :: repr (Maybe a)
+  just :: repr (a -> Maybe a)
+
+-- ** Type 'Haskellable'
+-- | Initial encoding of 'Haskellable'.
+data Haskell a where
+  Haskell :: ValueCode a -> Haskell a
+  (:.) :: Haskell ((b->c) -> (a->b) -> a -> c)
+  (:$) :: Haskell ((a->b) -> a -> b)
+  (:@) :: Haskell (a->b) -> Haskell a -> Haskell b
+  Cons :: Haskell (a -> [a] -> [a])
+  Const :: Haskell (a -> b -> a)
+  Eq :: Eq a => Haskell a -> Haskell (a -> Bool)
+  Flip :: Haskell ((a -> b -> c) -> b -> a -> c)
+  Id :: Haskell (a->a)
+  Unit :: Haskell ()
+infixr 0 $, :$
+infixr 9 ., :.
+infixl 9 .@, :@
+
+{-
+pattern (:.@) ::
+  -- Dummy constraint to get the following constraint
+  -- in scope when pattern-matching.
+  () =>
+  ((x -> y -> z) ~ ((b -> c) -> (a -> b) -> a -> c)) =>
+  Haskell x -> Haskell y -> Haskell z
+pattern (:.@) f g = (:.) :@ f :@ g
+pattern FlipApp ::
+  () =>
+  ((x -> y) ~ ((a -> b -> c) -> b -> a -> c)) =>
+  Haskell x -> Haskell y
+pattern FlipApp f = Flip :@ f
+pattern FlipConst ::
+  () =>
+  (x ~ (a -> b -> b)) =>
+  Haskell x
+pattern FlipConst = FlipApp Const
+-}
+
+instance Show (Haskell a) where
+  showsPrec p = \case
+    Haskell{} -> showString "Haskell"
+    (:$) -> showString "($)"
+    (:.) :@ f :@ g ->
+      showParen (p >= 9)
+      Function.$ showsPrec 9 f
+      Function.. showString " . "
+      Function.. showsPrec 9 g
+    (:.) -> showString "(.)"
+    Cons :@ x :@ xs ->
+      showParen (p >= 10)
+      Function.$ showsPrec 10 x
+      Function.. showString " : "
+      Function.. showsPrec 10 xs
+    Cons -> showString "cons"
+    Const -> showString "const"
+    Eq x ->
+      showParen True
+      Function.$ showString "== "
+      Function.. showsPrec 0 x
+    Flip -> showString "flip"
+    Id -> showString "id"
+    Unit -> showString "()"
+    (:@) f x ->
+      showParen (p >= 10)
+      Function.$ showsPrec 10 f
+      Function.. showString " "
+      Function.. showsPrec 10 x
+instance Trans Haskell Value where
+  trans = value Function.. trans
+instance Trans Haskell TH.CodeQ where
+  trans = code Function.. trans
+instance Trans Haskell ValueCode where
+  trans = \case
+    Haskell x -> x
+    (:.) -> (.)
+    (:$) -> ($)
+    (:@) f x -> (.@) (trans f) (trans x)
+    Cons -> cons
+    Const -> const
+    Eq x -> eq (trans x)
+    Flip -> flip
+    Id -> id
+    Unit -> unit
+instance Trans ValueCode Haskell where
+  trans = Haskell
+type instance Output Haskell = ValueCode
+
+instance Haskellable Haskell where
+  (.)     = (:.)
+  ($)     = (:$)
+  -- Small optimizations, mainly to reduce dump sizes.
+  Id .@ x = x
+  (Const :@ x) .@ _y = x
+  ((Flip :@ Const) :@ _x) .@ y = y
+  --
+  f .@ x  = f :@ x
+  cons    = Cons
+  const   = Const
+  eq      = Eq
+  flip    = Flip
+  id      = Id
+  unit    = Unit
+  bool b  = Haskell (bool b)
+  char c  = Haskell (char c)
+  nil     = Haskell nil
+  left    = Haskell left
+  right   = Haskell right
+  nothing = Haskell nothing
+  just    = Haskell just
+instance Haskellable ValueCode where
+  (.)      = ValueCode (.) (.)
+  ($)      = ValueCode ($) ($)
+  (.@) f x = ValueCode ((.@) (value f) (value x)) ((.@) (code f) (code x))
+  bool b   = ValueCode (bool b) (bool b)
+  char c   = ValueCode (char c) (char c)
+  cons     = ValueCode cons cons
+  const    = ValueCode const const
+  eq x     = ValueCode (eq (value x)) (eq (code x))
+  flip     = ValueCode flip flip
+  id       = ValueCode id id
+  nil      = ValueCode nil nil
+  unit     = ValueCode unit unit
+  left     = ValueCode left left
+  right    = ValueCode right right
+  nothing  = ValueCode nothing nothing
+  just     = ValueCode just just
+instance Haskellable Value where
+  (.)      = Value (Function..)
+  ($)      = Value (Function.$)
+  (.@) f x = Value (unValue f (unValue x))
+  bool     = Value
+  char     = Value
+  cons     = Value (:)
+  const    = Value Function.const
+  eq x     = Value (unValue x Eq.==)
+  flip     = Value Function.flip
+  id       = Value Function.id
+  nil      = Value []
+  unit     = Value ()
+  left     = Value Left
+  right    = Value Right
+  nothing  = Value Nothing
+  just     = Value Just
+instance Haskellable TH.CodeQ where
+  (.)      = [|| (Function..) ||]
+  ($)      = [|| (Function.$) ||]
+  (.@) f x = [|| $$f $$x ||]
+  bool b   = [|| b ||]
+  char c   = [|| c ||]
+  cons     = [|| (:) ||]
+  const    = [|| Function.const ||]
+  eq x     = [|| ($$x Eq.==) ||]
+  flip     = [|| \f x y -> f y x ||]
+  id       = [|| \x -> x ||]
+  nil      = [|| [] ||]
+  unit     = [|| () ||]
+  left     = [|| Left ||]
+  right    = [|| Right ||]
+  nothing  = [|| Nothing ||]
+  just     = [|| Just ||]
diff --git a/src/Symantic/Parser/Machine.hs b/src/Symantic/Parser/Machine.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Machine.hs
@@ -0,0 +1,35 @@
+module Symantic.Parser.Machine
+ ( module Symantic.Parser.Machine
+ , module Symantic.Parser.Machine.Instructions
+ , module Symantic.Parser.Machine.Dump
+ , module Symantic.Parser.Machine.Generate
+ , module Symantic.Parser.Machine.Input
+ ) where
+import Data.Function ((.))
+import Data.Ord (Ord)
+import Symantic.Parser.Machine.Input
+import Symantic.Parser.Grammar
+import Text.Show (Show)
+import qualified Language.Haskell.TH.Syntax as TH
+
+import Symantic.Parser.Machine.Instructions
+import Symantic.Parser.Machine.Dump
+import Symantic.Parser.Machine.Generate
+
+-- * Type 'Parser'
+type Parser inp =
+  ObserveSharing TH.Name
+                 (OptimizeComb TH.Name
+                               (Machine inp))
+
+machine :: forall inp repr a.
+  Ord (InputToken inp) =>
+  Show (InputToken inp) =>
+  TH.Lift (InputToken inp) =>
+  -- InputToken inp ~ Char =>
+  Executable repr =>
+  Readable repr (InputToken inp) =>
+  Grammar (Machine inp) =>
+  Parser inp a ->
+  repr inp '[] ('Succ 'Zero) a
+machine = runMachine . optimizeComb . observeSharing
diff --git a/src/Symantic/Parser/Machine/Dump.hs b/src/Symantic/Parser/Machine/Dump.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Machine/Dump.hs
@@ -0,0 +1,82 @@
+module Symantic.Parser.Machine.Dump where
+
+import Data.Function (($), (.), id)
+import Data.Functor ((<$>))
+import Data.Kind (Type)
+import Data.Semigroup (Semigroup(..))
+import Data.String (String, IsString(..))
+import Text.Show (Show(..))
+import qualified Data.Tree as Tree
+import qualified Data.List as List
+
+import Symantic.Parser.Machine.Instructions
+
+-- * Type 'DumpInstr'
+newtype DumpInstr inp (vs:: [Type]) (es::Peano) a
+  =     DumpInstr { unDumpInstr ::
+  Tree.Forest String -> Tree.Forest String }
+
+dumpInstr :: DumpInstr inp vs es a -> DumpInstr inp vs es a
+dumpInstr = id
+
+-- | Helper to dump a command.
+dumpInstrCmd :: String -> Tree.Forest String -> Tree.Tree String
+dumpInstrCmd n = Tree.Node n
+-- | Helper to dump an argument.
+dumpInstrArg :: String -> Tree.Forest String -> Tree.Tree String
+dumpInstrArg n = Tree.Node ("<"<>n<>">")
+
+instance Show (DumpInstr inp vs es a) where
+  show = drawTree . Tree.Node "" . ($ []) . unDumpInstr
+    where
+    drawTree :: Tree.Tree String -> String
+    drawTree  = List.unlines . draw
+    draw :: Tree.Tree String -> [String]
+    draw (Tree.Node x ts0) = List.lines x <> drawSubTrees ts0
+      where
+      drawSubTrees [] = []
+      drawSubTrees [t] = shift "" "  " (draw t)
+      drawSubTrees (t:ts) = shift "" "| " (draw t) <> drawSubTrees ts
+      shift first other = List.zipWith (<>) (first : List.repeat other)
+instance IsString (DumpInstr inp vs es a) where
+  fromString s = DumpInstr $ \is -> Tree.Node (fromString s) [] : is
+
+instance Stackable DumpInstr where
+  push a k = DumpInstr $ \is -> dumpInstrCmd ("push "<>showsPrec 10 a "") [] : unDumpInstr k is
+  pop k = DumpInstr $ \is -> dumpInstrCmd "pop" [] : unDumpInstr k is
+  liftI2 f k = DumpInstr $ \is -> dumpInstrCmd ("lift "<>show f) [] : unDumpInstr k is
+  swap k = DumpInstr $ \is -> dumpInstrCmd "swap" [] : unDumpInstr k is
+instance Branchable DumpInstr where
+  case_ l r = DumpInstr $ \is -> dumpInstrCmd "case"
+    [ dumpInstrArg "left" (unDumpInstr l [])
+    , dumpInstrArg "right" (unDumpInstr r [])
+    ] : is
+  choices ps bs d = DumpInstr $ \is ->
+    dumpInstrCmd ("choices "<>show ps) (
+      (dumpInstrArg "branch" . ($ []) . unDumpInstr <$> bs) <>
+      [ dumpInstrArg "default" (unDumpInstr d []) ]
+    ) : is
+instance Failable DumpInstr where
+  fail _err = DumpInstr $ \is -> dumpInstrCmd "fail" [] : is
+  popFail k = DumpInstr $ \is -> dumpInstrCmd "popFail" [] : unDumpInstr k is
+  catchFail t h = DumpInstr $ \is -> dumpInstrCmd "catchFail"
+    [ dumpInstrArg "try" (unDumpInstr t [])
+    , dumpInstrArg "handler" (unDumpInstr h [])
+    ] : is
+instance Inputable DumpInstr where
+  loadInput k = DumpInstr $ \is -> dumpInstrCmd "loadInput" [] : unDumpInstr k is
+  pushInput k = DumpInstr $ \is -> dumpInstrCmd "pushInput" [] : unDumpInstr k is
+instance Routinable DumpInstr where
+  subroutine n sub k = DumpInstr $ \is ->
+    Tree.Node (show n<>":") (unDumpInstr sub [])
+    : unDumpInstr k is
+  jump n = DumpInstr $ \is -> dumpInstrCmd ("jump "<>show n) [] : is
+  call n k = DumpInstr $ \is -> dumpInstrCmd ("call "<>show n) [] : unDumpInstr k is
+  ret = DumpInstr $ \is -> dumpInstrCmd "ret" [] : is
+instance Joinable DumpInstr where
+  defJoin n sub k = DumpInstr $ \is ->
+    Tree.Node (show n<>":") (unDumpInstr sub [])
+    : unDumpInstr k is
+  refJoin n = DumpInstr $ \is -> dumpInstrCmd ("refJoin "<>show n) [] : is
+instance Readable DumpInstr inp where
+  read _es _p k = DumpInstr $ \is -> dumpInstrCmd "read" [] : unDumpInstr k is
diff --git a/src/Symantic/Parser/Machine/Generate.hs b/src/Symantic/Parser/Machine/Generate.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Machine/Generate.hs
@@ -0,0 +1,416 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE StandaloneDeriving #-} -- For Show (ParsingError inp)
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UnboxedTuples #-} -- For nextInput
+{-# LANGUAGE UndecidableInstances #-} -- For Show (ParsingError inp)
+module Symantic.Parser.Machine.Generate where
+
+import Control.Monad (Monad(..))
+import Data.Bool (Bool)
+import Data.Char (Char)
+import Data.Either (Either(..))
+import Data.Function (($))
+-- import Data.Functor ((<$>))
+import Data.Int (Int)
+import Data.Maybe (Maybe(..))
+import Data.Ord (Ord, Ordering(..))
+import Data.Semigroup (Semigroup(..))
+import Data.Set (Set)
+import Language.Haskell.TH (CodeQ, Code(..))
+import Prelude (($!))
+import Text.Show (Show(..))
+import qualified Data.Eq as Eq
+import qualified Data.Set as Set
+import qualified Language.Haskell.TH.Syntax as TH
+
+import Symantic.Univariant.Trans
+import Symantic.Parser.Grammar.Combinators (ErrorItem(..))
+import Symantic.Parser.Machine.Input
+import Symantic.Parser.Machine.Instructions
+import qualified Symantic.Parser.Haskell as H
+
+-- * Type 'Gen'
+-- | Generate the 'CodeQ' parsing the input.
+newtype Gen inp vs es a = Gen { unGen ::
+  GenCtx inp vs es a ->
+  CodeQ (Either (ParsingError inp) a)
+}
+
+-- ** Type 'ParsingError'
+data ParsingError inp
+  =  ParsingErrorStandard
+  {  parsingErrorOffset :: Offset
+  ,  parsingErrorUnexpected :: Maybe (InputToken inp)
+  ,  parsingErrorExpecting :: Set (ErrorItem (InputToken inp))
+  }
+deriving instance Show (InputToken inp) => Show (ParsingError inp)
+
+-- ** Type 'Offset'
+type Offset = Int
+
+-- ** Type 'Cont'
+type Cont inp v a =
+  {-farthestInput-}Cursor inp ->
+  {-farthestExpecting-}[ErrorItem (InputToken inp)] ->
+  v ->
+  Cursor inp ->
+  Either (ParsingError inp) a
+
+-- ** Type 'SubRoutine'
+type SubRoutine inp v a =
+  {-ok-}Cont inp v a ->
+  Cursor inp ->
+  {-ko-}FailHandler inp a ->
+  Either (ParsingError inp) a
+
+-- ** Type 'FailHandler'
+type FailHandler inp a =
+  {-failureInput-}Cursor inp ->
+  {-farthestInput-}Cursor inp ->
+  {-farthestExpecting-}[ErrorItem (InputToken inp)] ->
+  Either (ParsingError inp) a
+
+{-
+-- *** Type 'FarthestError'
+data FarthestError inp = FarthestError
+  { farthestInput :: Cursor inp
+  , farthestExpecting :: [ErrorItem (InputToken inp)]
+  }
+-}
+
+-- | @('generate' input mach)@ generates @TemplateHaskell@ code
+-- parsing given 'input' according to given 'mach'ine.
+generate ::
+  forall inp ret.
+  Ord (InputToken inp) =>
+  Show (InputToken inp) =>
+  TH.Lift (InputToken inp) =>
+  -- InputToken inp ~ Char =>
+  Input inp =>
+  CodeQ inp ->
+  Show (Cursor inp) =>
+  Gen inp '[] ('Succ 'Zero) ret ->
+  CodeQ (Either (ParsingError inp) ret)
+generate input (Gen k) = [||
+  -- Pattern bindings containing unlifted types
+  -- should use an outermost bang pattern.
+  let !(# init, readMore, readNext #) = $$(cursorOf input) in
+  let finalRet = \_farInp _farExp v _inp -> Right v in
+  let finalFail _failInp !farInp !farExp =
+        Left ParsingErrorStandard
+        { parsingErrorOffset = offset farInp
+        , parsingErrorUnexpected =
+            if readMore farInp
+            then Just (let (# c, _ #) = readNext farInp in c)
+            else Nothing
+        , parsingErrorExpecting = Set.fromList farExp
+        } in
+  $$(k GenCtx
+    { valueStack = ValueStackEmpty
+    , failStack = FailStackCons [||finalFail||] FailStackEmpty
+    , retCode = [||finalRet||]
+    , input = [||init||]
+    , nextInput = [||readNext||]
+    , moreInput = [||readMore||]
+    -- , farthestError = [||Nothing||]
+    , farthestInput = [||init||]
+    , farthestExpecting = [|| [] ||]
+    })
+  ||]
+
+-- ** Type 'GenCtx'
+-- | This is a context only present at compile-time.
+data GenCtx inp vs (es::Peano) a =
+  ( TH.Lift (InputToken inp)
+  , Cursorable (Cursor inp)
+  , Show (InputToken inp)
+  -- , InputToken inp ~ Char
+  ) => GenCtx
+  { valueStack :: ValueStack vs
+  , failStack :: FailStack inp es a
+  , retCode :: CodeQ (Cont inp a a)
+  , input :: CodeQ (Cursor inp)
+  , moreInput :: CodeQ (Cursor inp -> Bool)
+  , nextInput :: CodeQ (Cursor inp -> (# InputToken inp, Cursor inp #))
+  , farthestInput :: CodeQ (Cursor inp)
+  , farthestExpecting :: CodeQ [ErrorItem (InputToken inp)]
+  }
+
+-- ** Type 'ValueStack'
+data ValueStack vs where
+  ValueStackEmpty :: ValueStack '[]
+  ValueStackCons ::
+    -- TODO: maybe use H.Haskell instead of CodeQ ?
+    -- as in https://github.com/j-mie6/ParsleyHaskell/popFail/3ec0986a5017866919a6404c14fe78678b7afb46
+    { valueStackHead :: CodeQ v
+    , valueStackTail :: ValueStack vs
+    } -> ValueStack (v ': vs)
+
+-- ** Type 'FailStack'
+data FailStack inp es a where
+  FailStackEmpty :: FailStack inp 'Zero a
+  FailStackCons ::
+    { failStackHead :: CodeQ (FailHandler inp a)
+    , failStackTail :: FailStack inp es a
+    } ->
+    FailStack inp ('Succ es) a
+
+instance Stackable Gen where
+  push x k = Gen $ \ctx -> unGen k ctx
+    { valueStack = ValueStackCons (liftCode x) (valueStack ctx) }
+  pop k = Gen $ \ctx -> unGen k ctx
+    { valueStack = valueStackTail (valueStack ctx) }
+  liftI2 f k = Gen $ \ctx -> unGen k ctx
+    { valueStack =
+      let ValueStackCons y (ValueStackCons x xs) = valueStack ctx in
+      ValueStackCons (liftCode2 f x y) xs
+    }
+  swap k = Gen $ \ctx -> unGen k ctx
+    { valueStack =
+        let ValueStackCons y (ValueStackCons x xs) = valueStack ctx in
+        ValueStackCons x (ValueStackCons y xs)
+    }
+instance Branchable Gen where
+  case_ kx ky = Gen $ \ctx ->
+    let ValueStackCons v vs = valueStack ctx in
+    [||
+      case $$v of
+        Left  x -> $$(unGen kx ctx{ valueStack = ValueStackCons [||x||] vs })
+        Right y -> $$(unGen ky ctx{ valueStack = ValueStackCons [||y||] vs })
+    ||]
+  choices fs ks kd = Gen $ \ctx ->
+    let ValueStackCons v vs = valueStack ctx in
+    go ctx{valueStack = vs} v fs ks
+    where
+    go ctx x (f:fs') (Gen k:ks') = [||
+      if $$(liftCode1 f x) then $$(k ctx)
+      else $$(go ctx x fs' ks')
+      ||]
+    go ctx _ _ _ = unGen kd ctx
+instance Failable Gen where
+  fail failExp = Gen $ \ctx@GenCtx{} -> [||
+    let (# farInp, farExp #) =
+          case $$compareOffset $$(farthestInput ctx) $$(input ctx) of
+            LT -> (# $$(input ctx), failExp #)
+            EQ -> (# $$(farthestInput ctx), ($$(farthestExpecting ctx) <> failExp) #)
+            GT -> (# $$(farthestInput ctx), $$(farthestExpecting ctx) #) in
+    {-
+    trace ("fail: "
+      <>" failExp="<>show @[ErrorItem Char] failExp
+      <>" farthestExpecting="<>show @[ErrorItem Char] ($$(farthestExpecting ctx))
+      <>" farExp="<>show @[ErrorItem Char] farExp) $
+    -}
+    $$(failStackHead (failStack ctx))
+      $$(input ctx) farInp farExp
+    ||]
+  popFail k = Gen $ \ctx ->
+    let FailStackCons _e es = failStack ctx in
+    unGen k ctx{failStack = es}
+  catchFail ok ko = Gen $ \ctx@GenCtx{} -> [||
+    let _ = "catchFail" in $$(unGen ok ctx
+      { failStack = FailStackCons [|| \(!failInp) (!farInp) (!farExp) ->
+          -- trace ("catchFail: " <> "farExp="<>show farExp) $
+          $$(unGen ko ctx
+            -- Push the input as it was when entering the catchFail.
+            { valueStack = ValueStackCons (input ctx) (valueStack ctx)
+            -- Move the input to the failing position.
+            , input = [||failInp||]
+            -- Set the farthestInput to the farthest computed by 'fail'
+            , farthestInput = [||farInp||]
+            , farthestExpecting = [||farExp||]
+            })
+        ||] (failStack ctx)
+      })
+    ||]
+instance Inputable Gen where
+  loadInput k = Gen $ \ctx ->
+    let ValueStackCons input vs = valueStack ctx in
+    unGen k ctx{valueStack = vs, input}
+  pushInput k = Gen $ \ctx ->
+    unGen k ctx{valueStack = ValueStackCons (input ctx) (valueStack ctx)}
+instance Routinable Gen where
+  call (LetName n) k = Gen $ \ctx -> [||
+    let _ = "call" in
+    $$(Code (TH.unsafeTExpCoerce (return (TH.VarE n))))
+      $$(suspend k ctx)
+      $$(input ctx)
+      $! $$(failStackHead (failStack ctx))
+    ||]
+  jump (LetName n) = Gen $ \ctx -> [||
+    let _ = "jump" in
+    $$(Code (TH.unsafeTExpCoerce (return (TH.VarE n))))
+      $$(retCode ctx)
+      $$(input ctx)
+      $! $$(failStackHead (failStack ctx))
+    ||]
+  ret = Gen $ \ctx -> unGen (resume (retCode ctx)) ctx
+  subroutine (LetName n) sub k = Gen $ \ctx -> Code $ TH.unsafeTExpCoerce $ do
+    body <- TH.unTypeQ $ TH.examineCode $ [|| -- buildRec in Parsley
+      -- SubRoutine
+      -- Why using $! at call site and not ! here on ko?
+      \ !ok !inp ko ->
+        $$(unGen sub ctx
+          { valueStack = ValueStackEmpty
+          , failStack = FailStackCons [||ko||] FailStackEmpty
+          , input = [||inp||]
+          , retCode = [||ok||]
+          -- , farthestInput = [|inp|]
+          -- , farthestExpecting = [|| [] ||]
+          })
+      ||]
+    let decl = TH.FunD n [TH.Clause [] (TH.NormalB body) []]
+    expr <- TH.unTypeQ (TH.examineCode (unGen k ctx))
+    return (TH.LetE [decl] expr)
+
+suspend ::
+  {-k-}Gen inp (v ': vs) es a ->
+  GenCtx inp vs es a ->
+  CodeQ (Cont inp v a)
+suspend k ctx = [||
+  let _ = "suspend" in
+  \farInp farExp v !inp ->
+    $$(unGen k ctx
+      { valueStack = ValueStackCons [||v||] (valueStack ctx)
+      , input = [||inp||]
+      , farthestInput = [||farInp||]
+      , farthestExpecting = [||farExp||]
+      }
+    )
+  ||]
+
+resume :: CodeQ (Cont inp v a) -> Gen inp (v ': vs) es a
+resume k = Gen $ \ctx -> [||
+  let _ = "resume" in
+  $$k
+    $$(farthestInput ctx)
+    $$(farthestExpecting ctx)
+    $$(valueStackHead (valueStack ctx))
+    $$(input ctx)
+  ||]
+
+instance Joinable Gen where
+  defJoin (LetName n) sub k = Gen $ \ctx -> Code $ TH.unsafeTExpCoerce $ do
+    body <- TH.unTypeQ $ TH.examineCode $ [||
+      \farInp farExp v !inp ->
+        $$(unGen sub ctx
+          { valueStack = ValueStackCons [||v||] (valueStack ctx)
+          , input = [||inp||]
+          , farthestInput = [||farInp||]
+          , farthestExpecting = [||farExp||]
+          })
+      ||]
+    let decl = TH.FunD n [TH.Clause [] (TH.NormalB body) []]
+    expr <- TH.unTypeQ (TH.examineCode (unGen k ctx))
+    return (TH.LetE [decl] expr)
+  refJoin (LetName n) =
+    resume (Code (TH.unsafeTExpCoerce (return (TH.VarE n))))
+instance Readable Gen Char where
+  read farExp p k =
+    -- TODO: piggy bank
+    maybeEmitCheck (Just 1) k
+    where
+    maybeEmitCheck Nothing ok = sat (liftCode p) ok (fail farExp)
+    maybeEmitCheck (Just n) ok = Gen $ \ctx ->
+      let FailStackCons e es = failStack ctx in
+      [||
+      let readFail = $$(e) in -- Factorize failure code
+      $$((`unGen` ctx{failStack = FailStackCons [||readFail||] es}) $ emitLengthCheck n
+        {-ok-}(sat (liftCode p) ok
+          {-ko-}(fail farExp))
+        {-ko-}(fail farExp))
+      ||]
+
+sat ::
+  forall inp vs es a.
+  -- Cursorable (Cursor inp) =>
+  -- InputToken inp ~ Char =>
+  Ord (InputToken inp) =>
+  TH.Lift (InputToken inp) =>
+  {-predicate-}CodeQ (InputToken inp -> Bool) ->
+  {-ok-}Gen inp (InputToken inp ': vs) ('Succ es) a ->
+  {-ko-}Gen inp vs ('Succ es) a ->
+  Gen inp vs ('Succ es) a
+sat p ok ko = Gen $ \ctx -> [||
+  let !(# c, cs #) = $$(nextInput ctx) $$(input ctx) in
+  if $$p c
+  then $$(unGen ok ctx
+    { valueStack = ValueStackCons [||c||] (valueStack ctx)
+    , input = [||cs||]
+    })
+  else let _ = "sat.else" in $$(unGen ko ctx)
+  ||]
+
+{-
+evalSat ::
+  -- Cursorable inp =>
+  -- HandlerOps inp =>
+  InstrPure (Char -> Bool) ->
+  Gen inp (Char ': vs) ('Succ es) a ->
+  Gen inp vs ('Succ es) a
+evalSat p k = do
+  bankrupt <- asks isBankrupt
+  hasChange <- asks hasCoin
+  if | bankrupt -> maybeEmitCheck (Just 1) <$> k
+     | hasChange -> maybeEmitCheck Nothing <$> local spendCoin k
+     | otherwise -> local breakPiggy (maybeEmitCheck . Just <$> asks coins <*> local spendCoin k)
+  where
+  maybeEmitCheck Nothing mk ctx = sat (genDefunc p) mk (raise ctx) ctx
+  maybeEmitCheck (Just n) mk ctx =
+    [|| let bad = $$(raise ctx) in $$(emitLengthCheck n (sat (genDefunc p) mk [||bad||]) [||bad||] ctx)||]
+-}
+
+emitLengthCheck ::
+  TH.Lift (InputToken inp) =>
+  Int -> Gen inp vs es a -> Gen inp vs es a -> Gen inp vs es a
+emitLengthCheck 0 ok _ko = ok
+emitLengthCheck 1 ok ko = Gen $ \ctx -> [||
+  if $$(moreInput ctx) $$(input ctx)
+  then $$(unGen ok ctx)
+  else let _ = "sat.length-check.else" in $$(unGen ko ctx)
+  ||]
+{-
+emitLengthCheck n ok ko ctx = Gen $ \ctx -> [||
+  if $$moreInput ($$shiftRight $$(input ctx) (n - 1))
+  then $$(unGen ok ctx)
+  else $$(unGen ko ctx {farthestExpecting = [||farExp||]})
+  ||]
+-}
+
+
+liftCode :: InstrPure a -> CodeQ a
+liftCode = trans
+{-# INLINE liftCode #-}
+
+liftCode1 :: InstrPure (a -> b) -> CodeQ a -> CodeQ b
+liftCode1 p a = case p of
+  InstrPureSameOffset -> [|| $$sameOffset $$a ||]
+  InstrPureHaskell h -> go a h
+  where
+  go :: CodeQ a -> H.Haskell (a -> b) -> CodeQ b
+  go qa = \case
+    (H.:$) -> [|| \x -> $$qa x ||]
+    (H.:.) -> [|| \g x -> $$qa (g x) ||]
+    H.Flip -> [|| \x y -> $$qa y x ||]
+    (H.:.) H.:@ f H.:@ g -> [|| $$(go (go qa g) f) ||]
+    H.Const -> [|| \_ -> $$qa ||]
+    H.Flip H.:@ H.Const -> H.id
+    h@(H.Flip H.:@ _f) -> [|| \x -> $$(liftCode2 (InstrPureHaskell h) qa [||x||]) ||]
+    H.Eq x -> [|| $$(trans x) Eq.== $$qa ||]
+    H.Id -> qa
+    h -> [|| $$(trans h) $$qa ||]
+
+liftCode2 :: InstrPure (a -> b -> c) -> CodeQ a -> CodeQ b -> CodeQ c
+liftCode2 p a b = case p of
+  InstrPureSameOffset -> [|| $$sameOffset $$a $$b ||]
+  InstrPureHaskell h -> go a b h
+  where
+  go :: CodeQ a -> CodeQ b -> H.Haskell (a -> b -> c) -> CodeQ c
+  go qa qb = \case
+    (H.:$) -> [|| $$qa $$qb ||]
+    (H.:.) -> [|| \x -> $$qa ($$qb x) ||]
+    H.Flip -> [|| \x -> $$qa x $$qb ||]
+    H.Flip H.:@ H.Const -> [|| $$qb ||]
+    H.Flip H.:@ f -> go qb qa f
+    H.Const -> [|| $$qa ||]
+    H.Cons -> [|| $$qa : $$qb ||]
+    h -> [|| $$(trans h) $$qa $$qb ||]
diff --git a/src/Symantic/Parser/Machine/Input.hs b/src/Symantic/Parser/Machine/Input.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Machine/Input.hs
@@ -0,0 +1,239 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UnboxedTuples #-}
+module Symantic.Parser.Machine.Input where
+
+import Data.Array.Base (UArray(..), listArray)
+-- import Data.Array.Unboxed (UArray)
+import Data.Bool
+import Data.ByteString.Internal (ByteString(..))
+import Data.Char (Char)
+import Data.Eq (Eq(..))
+import Data.Function (on)
+import Data.Int (Int)
+import Data.Kind (Type)
+import Data.Ord (Ord(..), Ordering)
+import Data.String (String)
+import Data.Text ()
+import Data.Text.Array ({-aBA, empty-})
+import Data.Text.Internal (Text(..))
+import Data.Text.Unsafe (iter, Iter(..), iter_, reverseIter_)
+import Text.Show (Show(..))
+import GHC.Exts (Int(..), Char(..){-, RuntimeRep(..)-})
+import GHC.ForeignPtr (ForeignPtr(..), ForeignPtrContents)
+import GHC.Prim ({-Int#,-} Addr#, nullAddr#, indexWideCharArray#, {-indexWord16Array#,-} readWord8OffAddr#, word2Int#, chr#, touch#, realWorld#, plusAddr#, (+#))
+import Language.Haskell.TH (CodeQ)
+import Prelude ((+), (-), error)
+import qualified Data.ByteString.Lazy.Internal as BSL
+import qualified Data.List as List
+
+-- * Class 'Cursorable'
+class Show cur => Cursorable cur where
+  offset :: cur -> Int
+  compareOffset :: CodeQ (cur -> cur -> Ordering)
+  compareOffset = [|| compare `on` offset ||]
+  lowerOffset :: CodeQ (cur -> cur -> Bool)
+  sameOffset :: CodeQ (cur -> cur -> Bool)
+  shiftRight :: CodeQ (cur -> Int -> cur)
+instance Cursorable Int where
+  offset = \inp -> inp
+  compareOffset = [|| compare @Int ||]
+  lowerOffset = [|| (<) @Int ||]
+  sameOffset = [|| (==) @Int ||]
+  shiftRight = [|| (+) @Int ||]
+instance Cursorable Text where
+  offset = \(Text _ i _) -> i
+  lowerOffset = [|| \(Text _ i _) (Text _ j _) -> i < j ||]
+  sameOffset = [|| \(Text _ i _) (Text _ j _) -> i == j ||]
+  shiftRight = [||shiftRightText||]
+
+shiftRightText :: Text -> Int -> Text
+shiftRightText (Text arr off unconsumed) i = go i off unconsumed
+  where
+    go 0 off' unconsumed' = Text arr off' unconsumed'
+    go n off' unconsumed'
+      | unconsumed' > 0 = let !d = iter_ (Text arr off' unconsumed') 0
+                          in go (n-1) (off'+d) (unconsumed'-d)
+      | otherwise = Text arr off' unconsumed'
+
+shiftLeftText :: Text -> Int -> Text
+shiftLeftText (Text arr off unconsumed) i = go i off unconsumed
+  where
+    go 0 off' unconsumed' = Text arr off' unconsumed'
+    go n off' unconsumed'
+      | off' > 0 = let !d = reverseIter_ (Text arr off' unconsumed') 0 in go (n-1) (off'+d) (unconsumed'-d)
+      | otherwise = Text arr off' unconsumed'
+
+instance Cursorable UnpackedLazyByteString where
+  offset = \(UnpackedLazyByteString i _ _ _ _ _) -> i
+  lowerOffset = [||\(UnpackedLazyByteString i _ _ _ _ _) (UnpackedLazyByteString j _ _ _ _ _) -> i <= j||]
+  sameOffset = [||\(UnpackedLazyByteString i _ _ _ _ _) (UnpackedLazyByteString j _ _ _ _ _) -> i == j||]
+  shiftRight = [||shiftRightByteString||]
+
+shiftRightByteString :: UnpackedLazyByteString -> Int -> UnpackedLazyByteString
+shiftRightByteString !(UnpackedLazyByteString i addr# final off size cs) j
+  | j < size  = UnpackedLazyByteString (i + j) addr# final (off + j) (size - j) cs
+  | otherwise = case cs of
+    BSL.Chunk (PS (ForeignPtr addr'# final') off' size') cs' -> shiftRightByteString (UnpackedLazyByteString (i + size) addr'# final' off' size' cs') (j - size)
+    BSL.Empty -> emptyUnpackedLazyByteString (i + size)
+
+shiftLeftByteString :: UnpackedLazyByteString -> Int -> UnpackedLazyByteString
+shiftLeftByteString (UnpackedLazyByteString i addr# final off size cs) j =
+  UnpackedLazyByteString (i - d) addr# final (off - d) (size + d) cs
+  where d = min off j
+
+offWith :: CodeQ (ts -> OffWith ts)
+offWith = [|| OffWith 0 ||]
+
+-- ** Type 'Text16'
+newtype Text16 = Text16 Text
+--newtype CacheText = CacheText Text
+-- ** Type 'CharList'
+newtype CharList = CharList String
+-- ** Type 'Stream'
+data Stream = {-# UNPACK #-} !Char :> Stream
+nomore :: Stream
+nomore = '\0' :> nomore
+{-
+instance Cursorable (OffWith Stream) where
+  lowerOffset = [|| \(OffWith i _) (OffWith j _) -> i < j ||]
+  sameOffset = [|| \(OffWith i _) (OffWith j _) -> i == j ||]
+  shiftRight = [|| \(OffWith o ts) i -> OffWith (o + i) (dropStream i ts) ||]
+  where
+    dropStream :: Int -> Stream -> Stream
+    dropStream 0 cs = cs
+    dropStream n (_ :> cs) = dropStream (n-1) cs
+-}
+
+-- ** Type 'OffWith'
+data OffWith ts = OffWith {-# UNPACK #-} !Int ts
+  deriving (Show)
+
+instance Cursorable (OffWith String) where
+  offset = \(OffWith i _) -> i
+  lowerOffset = [|| \(OffWith i _) (OffWith j _) -> i < j ||]
+  sameOffset = [|| \(OffWith i _) (OffWith j _) -> i == j ||]
+  shiftRight = [|| \(OffWith o ts) i -> OffWith (o + i) (List.drop i ts) ||]
+
+-- ** Type 'OffWithStreamAnd'
+data OffWithStreamAnd ts = OffWithStreamAnd {-# UNPACK #-} !Int !Stream ts
+-- ** Type 'UnpackedLazyByteString'
+data UnpackedLazyByteString = UnpackedLazyByteString
+  {-# UNPACK #-} !Int
+  !Addr#
+  ForeignPtrContents
+  {-# UNPACK #-} !Int
+  {-# UNPACK #-} !Int
+  BSL.ByteString
+instance Show UnpackedLazyByteString where
+  show (UnpackedLazyByteString _i _addr _p _off _size _cs) = "UnpackedLazyByteString" -- FIXME
+
+{-# INLINE emptyUnpackedLazyByteString #-}
+emptyUnpackedLazyByteString :: Int -> UnpackedLazyByteString
+emptyUnpackedLazyByteString i =
+  UnpackedLazyByteString i nullAddr#
+    (error "nullForeignPtr") 0 0 BSL.Empty
+
+-- * Class 'Input'
+class Cursorable (Cursor inp) => Input inp where
+  type Cursor inp :: Type
+  type InputToken inp :: Type
+  cursorOf :: CodeQ inp -> CodeQ
+    (# {-init-} Cursor inp
+    ,  {-more-} Cursor inp -> Bool
+    ,  {-next-} Cursor inp -> (# InputToken inp, Cursor inp #)
+    #)
+
+instance Input String where
+  type Cursor String = Int
+  type InputToken String = Char
+  cursorOf input = cursorOf @(UArray Int Char)
+    [|| listArray (0, List.length $$input-1) $$input ||]
+instance Input (UArray Int Char) where
+  type Cursor (UArray Int Char) = Int
+  type InputToken (UArray Int Char) = Char
+  cursorOf qinput = [||
+      let UArray _ _ size input# = $$qinput
+          next (I# i#) =
+            (# C# (indexWideCharArray# input# i#)
+            ,  I# (i# +# 1#)
+            #)
+      in (# 0, (< size), next #)
+    ||]
+instance Input Text where
+  type Cursor Text = Text
+  type InputToken Text = Char
+  cursorOf inp = [||
+      let _ = "cursorOf" in
+      let next t@(Text arr off unconsumed) =
+            let !(Iter c d) = iter t 0 in
+            (# c, Text arr (off+d) (unconsumed-d) #)
+          more (Text _ _ unconsumed) = unconsumed > 0
+      in (# $$inp, more, next #)
+    ||]
+instance Input ByteString where
+  type Cursor ByteString = Int
+  type InputToken ByteString = Char
+  cursorOf qinput = [||
+      let PS (ForeignPtr addr# final) off size = $$qinput
+          next i@(I# i#) =
+            case readWord8OffAddr# (addr# `plusAddr#` i#) 0# realWorld# of
+              (# s', x #) -> case touch# final s' of
+                _ -> (# C# (chr# (word2Int# x)), i + 1 #)
+      in (# off, (< size), next #)
+    ||]
+instance Input BSL.ByteString where
+  type Cursor BSL.ByteString = UnpackedLazyByteString
+  type InputToken BSL.ByteString = Char
+  cursorOf qinput = [||
+      let next (UnpackedLazyByteString i addr# final off@(I# off#) size cs) =
+            case readWord8OffAddr# addr# off# realWorld# of
+              (# s', x #) -> case touch# final s' of
+                _ ->
+                  (# C# (chr# (word2Int# x))
+                  , if size /= 1 then UnpackedLazyByteString (i+1) addr# final (off+1) (size-1) cs
+                    else case cs of
+                      BSL.Chunk (PS (ForeignPtr addr'# final') off' size') cs' -> UnpackedLazyByteString (i+1) addr'# final' off' size' cs'
+                      BSL.Empty -> emptyUnpackedLazyByteString (i+1)
+                  #)
+          more (UnpackedLazyByteString _ _ _ _ 0 _) = False
+          more _ = True
+          init = case $$qinput of
+            BSL.Chunk (PS (ForeignPtr addr# final) off size) cs -> UnpackedLazyByteString 0 addr# final off size cs
+            BSL.Empty -> emptyUnpackedLazyByteString 0
+      in (# init, more, next #)
+    ||]
+{-
+instance Input Text16 where
+  type Cursor Text16 = Int
+  cursorOf qinput = [||
+    let Text16 (Text arr off size) = $$qinput
+        arr# = aBA arr
+        next (I# i#) =
+          (# C# (chr# (word2Int# (indexWord16Array# arr# i#)))
+          , I# (i# +# 1#) #)
+    in (# off, (< size), next #)
+  ||]
+instance Input CharList where
+  type Cursor CharList = OffWith String
+  cursorOf qinput = [||
+    let CharList input = $$qinput
+        next (OffWith i (c:cs)) = (# c, OffWith (i+1) cs #)
+        size = List.length input
+        more (OffWith i _) = i < size
+        --more (OffWith _ []) = False
+        --more _              = True
+    in (# $$offWith input, more, next #)
+  ||]
+instance Input Stream where
+  type Cursor Stream = OffWith Stream
+  cursorOf qinput = [||
+    let next (OffWith o (c :> cs)) = (# c, OffWith (o + 1) cs #)
+    in (# $$offWith $$qinput, const True, next #)
+  ||]
+-}
+{-
+-- type instance Cursor CacheText = (Text, Stream)
+-- type instance Cursor BSL.ByteString = OffWith BSL.ByteString
+-}
diff --git a/src/Symantic/Parser/Machine/Instructions.hs b/src/Symantic/Parser/Machine/Instructions.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Parser/Machine/Instructions.hs
@@ -0,0 +1,407 @@
+{-# LANGUAGE ConstraintKinds #-} -- For Executable
+{-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
+{-# LANGUAGE PatternSynonyms #-} -- For Fmap, App, …
+{-# LANGUAGE UndecidableInstances #-} -- For Cursorable (Cursor inp)
+module Symantic.Parser.Machine.Instructions where
+
+import Data.Bool (Bool(..))
+import Data.Either (Either)
+import Data.Eq (Eq)
+import Data.Ord (Ord)
+import Data.Function (($), (.))
+import Data.Kind (Type)
+import System.IO.Unsafe (unsafePerformIO)
+import Text.Show (Show(..), showString)
+import qualified Data.Functor as Functor
+import qualified Language.Haskell.TH as TH
+import qualified Language.Haskell.TH.Syntax as TH
+import qualified Symantic.Parser.Haskell as H
+
+import Symantic.Parser.Grammar
+import Symantic.Parser.Machine.Input
+import Symantic.Univariant.Trans
+
+-- * Type 'Instr'
+-- | 'Instr'uctions for the 'Machine'.
+data Instr input valueStack (failStack::Peano) returnValue where
+  -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
+  -- and continues with the next 'Instr'uction @(k)@.
+  Push ::
+    InstrPure v ->
+    Instr inp (v ': vs) es ret ->
+    Instr inp vs es ret
+  -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
+  Pop ::
+    Instr inp vs es ret ->
+    Instr inp (v ': vs) es ret
+  -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
+  -- and pushes the result of @(f)@ applied to them.
+  LiftI2 ::
+    InstrPure (x -> y -> z) ->
+    Instr inp (z : vs) es ret ->
+    Instr inp (y : x : vs) es ret
+  -- | @('Fail')@ raises an error from the 'failStack'.
+  Fail ::
+    [ErrorItem (InputToken inp)] ->
+    Instr inp vs ('Succ es) ret
+  -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
+  -- and continues with the next 'Instr'uction @(k)@.
+  PopFail ::
+    Instr inp vs es ret ->
+    Instr inp vs ('Succ es) ret
+  -- | @('CatchFail' l r)@ tries the @(l)@ 'Instr'uction
+  -- in a new failure scope such that if @(l)@ raises a failure, it is caught,
+  -- then the input is pushed as it was before trying @(l)@ on the 'valueStack',
+  -- and the control flow goes on with the @(r)@ 'Instr'uction.
+  CatchFail ::
+    Instr inp vs ('Succ es) ret ->
+    Instr inp (Cursor inp ': vs) es ret ->
+    Instr inp vs es ret
+  -- | @('LoadInput' k)@ removes the input from the 'valueStack'
+  -- and continues with the next 'Instr'uction @(k)@ using that input.
+  LoadInput ::
+    Instr inp vs es r ->
+    Instr inp (Cursor inp : vs) es r
+  -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
+  -- and continues with the next 'Instr'uction @(k)@.
+  PushInput ::
+    Instr inp (Cursor inp ': vs) es ret ->
+    Instr inp vs es ret
+  -- | @('Case' l r)@.
+  Case ::
+    Instr inp (x ': vs) es r ->
+    Instr inp (y ': vs) es r ->
+    Instr inp (Either x y ': vs) es r
+  -- | @('Swap' k)@ pops two values on the 'valueStack',
+  -- pushes the first popped-out, then the second,
+  -- and continues with the next 'Instr'uction @(k)@.
+  Swap ::
+    Instr inp (x ': y ': vs) es r ->
+    Instr inp (y ': x ': vs) es r
+  -- | @('Choices' ps bs d)@.
+  Choices ::
+    [InstrPure (v -> Bool)] ->
+    [Instr inp vs es ret] ->
+    Instr inp vs es ret ->
+    Instr inp (v ': vs) es ret
+  -- | @('Subroutine' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
+  -- 'Call's @(n)@ and
+  -- continues with the next 'Instr'uction @(k)@.
+  Subroutine ::
+    LetName v -> Instr inp '[] ('Succ 'Zero) v ->
+    Instr inp vs ('Succ es) ret ->
+    Instr inp vs ('Succ es) ret
+  -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
+  Jump ::
+    LetName ret ->
+    Instr inp '[] ('Succ es) ret
+  -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
+  -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
+  Call ::
+    LetName v ->
+    Instr inp (v ': vs) ('Succ es) ret ->
+    Instr inp vs ('Succ es) ret
+  -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
+  Ret ::
+    Instr inp '[ret] es ret
+  -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
+  -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
+  -- otherwise 'Fail'.
+  Read ::
+    [ErrorItem (InputToken inp)] ->
+    InstrPure (InputToken inp -> Bool) ->
+    Instr inp (InputToken inp ': vs) ('Succ es) ret ->
+    Instr inp vs ('Succ es) ret
+  DefJoin ::
+    LetName v -> Instr inp (v ': vs) es ret ->
+    Instr inp vs es ret ->
+    Instr inp vs es ret
+  RefJoin ::
+    LetName v ->
+    Instr inp (v ': vs) es ret
+
+-- ** Type 'InstrPure'
+data InstrPure a where
+  InstrPureHaskell :: H.Haskell a -> InstrPure a
+  InstrPureSameOffset :: Cursorable cur => InstrPure (cur -> cur -> Bool)
+
+instance Show (InstrPure a) where
+  showsPrec p = \case
+    InstrPureHaskell x -> showsPrec p x
+    InstrPureSameOffset -> showString "InstrPureSameOffset"
+instance Trans InstrPure TH.CodeQ where
+  trans = \case
+    InstrPureHaskell x -> trans x
+    InstrPureSameOffset -> sameOffset
+
+-- ** Type 'LetName'
+newtype LetName a = LetName { unLetName :: TH.Name }
+  deriving (Eq)
+  deriving newtype Show
+
+-- * Class 'Executable'
+type Executable repr =
+  ( Stackable repr
+  , Branchable repr
+  , Failable repr
+  , Inputable repr
+  , Routinable repr
+  , Joinable repr
+  )
+
+-- ** Class 'Stackable'
+class Stackable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
+  push ::
+    InstrPure v ->
+    repr inp (v ': vs) n ret ->
+    repr inp vs n ret
+  pop ::
+    repr inp vs n ret ->
+    repr inp (v ': vs) n ret
+  liftI2 ::
+    InstrPure (x -> y -> z) ->
+    repr inp (z ': vs) es ret ->
+    repr inp (y ': x ': vs) es ret
+  swap ::
+    repr inp (x ': y ': vs) n r ->
+    repr inp (y ': x ': vs) n r
+
+-- ** Class 'Branchable'
+class Branchable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
+  case_ ::
+    repr inp (x ': vs) n r ->
+    repr inp (y ': vs) n r ->
+    repr inp (Either x y ': vs) n r
+  choices ::
+    [InstrPure (v -> Bool)] ->
+    [repr inp vs es ret] ->
+    repr inp vs es ret ->
+    repr inp (v ': vs) es ret
+
+-- ** Class 'Failable'
+class Failable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
+  fail :: [ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) ret
+  popFail ::
+    repr inp vs es ret ->
+    repr inp vs ('Succ es) ret
+  catchFail ::
+    repr inp vs ('Succ es) ret ->
+    repr inp (Cursor inp ': vs) es ret ->
+    repr inp vs es ret
+
+-- ** Class 'Inputable'
+class Inputable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
+  loadInput ::
+    repr inp vs es r ->
+    repr inp (Cursor inp ': vs) es r
+  pushInput ::
+    repr inp (Cursor inp ': vs) es ret ->
+    repr inp vs es ret
+
+-- ** Class 'Routinable'
+class Routinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
+  subroutine ::
+    LetName v -> repr inp '[] ('Succ 'Zero) v ->
+    repr inp vs ('Succ es) ret ->
+    repr inp vs ('Succ es) ret
+  call ::
+    LetName v -> repr inp (v ': vs) ('Succ es) ret ->
+    repr inp vs ('Succ es) ret
+  ret ::
+    repr inp '[ret] es ret
+  jump ::
+    LetName ret ->
+    repr inp '[] ('Succ es) ret
+
+-- ** Class 'Joinable'
+class Joinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
+  defJoin ::
+    LetName v ->
+    repr inp (v ': vs) es ret ->
+    repr inp vs es ret ->
+    repr inp vs es ret
+  refJoin ::
+    LetName v ->
+    repr inp (v ': vs) es ret
+
+-- ** Class 'Readable'
+class Readable (repr :: Type -> [Type] -> Peano -> Type -> Type) (tok::Type) where
+  read ::
+    tok ~ InputToken inp =>
+    [ErrorItem tok] ->
+    InstrPure (tok -> Bool) ->
+    repr inp (tok ': vs) ('Succ es) ret ->
+    repr inp vs ('Succ es) ret
+
+instance
+  ( Executable repr
+  , Readable repr (InputToken inp)
+  ) => Trans (Instr inp vs es) (repr inp vs es) where
+  trans = \case
+    Push x k -> push x (trans k)
+    Pop k -> pop (trans k)
+    LiftI2 f k -> liftI2 f (trans k)
+    Fail err -> fail err
+    PopFail k -> popFail (trans k)
+    CatchFail l r -> catchFail (trans l) (trans r)
+    LoadInput k -> loadInput (trans k)
+    PushInput k -> pushInput (trans k)
+    Case l r -> case_ (trans l) (trans r)
+    Swap k -> swap (trans k)
+    Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
+    Subroutine n sub k -> subroutine n (trans sub) (trans k)
+    Jump n -> jump n
+    Call n k -> call n (trans k)
+    Ret -> ret
+    Read es p k -> read es p (trans k)
+    DefJoin n sub k -> defJoin n (trans sub) (trans k)
+    RefJoin n -> refJoin n
+
+-- ** Type 'Peano'
+-- | Type-level natural numbers, using the Peano recursive encoding.
+data Peano = Zero | Succ Peano
+
+-- | @('Fmap' f k)@.
+pattern Fmap ::
+  InstrPure (x -> y) ->
+  Instr inp (y ': xs) es ret ->
+  Instr inp (x ': xs) es ret
+pattern Fmap f k = Push f (LiftI2 (InstrPureHaskell (H.Flip H.:@ (H.:$))) k)
+
+-- | @('App' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
+-- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
+pattern App ::
+  Instr inp (y : vs) es ret ->
+  Instr inp (x : (x -> y) : vs) es ret
+pattern App k = LiftI2 (InstrPureHaskell (H.:$)) k
+
+-- | @('If' ok ko)@ pops a 'Bool' from the 'valueStack'
+-- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
+-- or @(ko)@ otherwise.
+pattern If ::
+  Instr inp vs es ret ->
+  Instr inp vs es ret ->
+  Instr inp (Bool ': vs) es ret
+pattern If ok ko = Choices [InstrPureHaskell H.Id] [ok] ko
+
+-- * Type 'Machine'
+-- | Making the control-flow explicit.
+data Machine inp v = Machine { unMachine ::
+  forall vs es ret.
+  {-k-}Instr inp (v ': vs) ('Succ es) ret ->
+  Instr inp vs ('Succ es) ret
+  }
+
+runMachine ::
+  forall inp v es repr.
+  Executable repr =>
+  Readable repr (InputToken inp) =>
+  Machine inp v -> repr inp '[] ('Succ es) v
+runMachine (Machine auto) =
+  trans @(Instr inp '[] ('Succ es)) $
+  auto Ret
+
+instance Applicable (Machine inp) where
+  pure x = Machine $ Push (InstrPureHaskell x)
+  Machine f <*> Machine x = Machine $ f . x . App
+  liftA2 f (Machine x) (Machine y) = Machine $
+    x . y . LiftI2 (InstrPureHaskell f)
+  Machine x *> Machine y = Machine $ x . Pop . y
+  Machine x <* Machine y = Machine $ x . y . Pop
+instance
+  Cursorable (Cursor inp) =>
+  Alternable (Machine inp) where
+  empty = Machine $ \_k -> Fail []
+  Machine l <|> Machine r = Machine $ \k ->
+    makeJoin k $ \j ->
+    CatchFail
+      (l (PopFail j))
+      (failIfConsumed (r j))
+  try (Machine x) = Machine $ \k ->
+    CatchFail (x (PopFail k))
+      -- On exception, reset the input,
+      -- and propagate the failure.
+      (LoadInput (Fail []))
+
+-- | If no input has been consumed by the failing alternative
+-- then continue with the given continuation.
+-- Otherwise, propagate the 'Fail'ure.
+failIfConsumed ::
+  Cursorable (Cursor inp) =>
+  Instr inp vs ('Succ es) ret ->
+  Instr inp (Cursor inp : vs) ('Succ es) ret
+failIfConsumed k = PushInput (LiftI2 InstrPureSameOffset (If k (Fail [])))
+
+-- | @('makeJoin' k f)@ factorizes @(k)@ in @(f)@,
+-- by introducing a 'DefJoin' if necessary,
+-- and passing the corresponding 'RefJoin' to @(f)@,
+-- or @(k)@ as is when factorizing is useless.
+makeJoin ::
+  Instr inp (v : vs) es ret ->
+  (Instr inp (v : vs) es ret -> Instr inp vs es ret) ->
+  Instr inp vs es ret
+-- Double RefJoin Optimization:
+-- If a join-node points directly to another join-node,
+-- then reuse it
+makeJoin k@RefJoin{} = ($ k)
+-- Terminal RefJoin Optimization:
+-- If a join-node points directly to a terminal operation,
+-- then it's useless to introduce a join-point.
+makeJoin k@Ret = ($ k)
+makeJoin k =
+  let joinName = LetName $ unsafePerformIO $ TH.qNewName "join" in
+  \f -> DefJoin joinName k (f (RefJoin joinName))
+
+instance tok ~ InputToken inp => Satisfiable (Machine inp) tok where
+  satisfy es p = Machine $ Read es (InstrPureHaskell p)
+instance Selectable (Machine inp) where
+  branch (Machine lr) (Machine l) (Machine r) = Machine $ \k ->
+    makeJoin k $ \j ->
+    lr (Case (l (Swap (App j)))
+             (r (Swap (App j))))
+instance Matchable (Machine inp) where
+  conditional ps bs (Machine m) (Machine default_) = Machine $ \k ->
+    makeJoin k $ \j ->
+    m (Choices (InstrPureHaskell Functor.<$> ps)
+               ((\b -> unMachine b j) Functor.<$> bs)
+               (default_ j))
+instance
+  ( Ord (InputToken inp)
+  , Cursorable (Cursor inp)
+  ) => Lookable (Machine inp) where
+  look (Machine x) = Machine $ \k ->
+    PushInput (x (Swap (LoadInput k)))
+  eof = negLook (satisfy [{-discarded by negLook-}] (H.const H..@ H.bool True))
+        -- Set a better failure message
+        <|> (Machine $ \_k -> Fail [ErrorItemEnd])
+  negLook (Machine x) = Machine $ \k ->
+    CatchFail
+      -- On x success, discard the result,
+      -- and replace this 'CatchFail''s failure handler
+      -- by a 'Fail'ure whose 'farthestExpecting' is negated,
+      -- then a failure is raised from the input
+      -- when entering 'negLook', to avoid odd cases:
+      -- - where the failure that made (negLook x)
+      --   succeed can get the blame for the overall
+      --   failure of the grammar.
+      -- - where the overall failure of
+      --   the grammar might be blamed on something in x
+      --   that, if corrected, still makes x succeed and
+      --   (negLook x) fail.
+      (PushInput (x (Pop (PopFail (LoadInput (Fail []))))))
+      -- On x failure, reset the input,
+      -- and go on with the next 'Instr'uctions.
+      (LoadInput (Push (InstrPureHaskell H.unit) k))
+instance Letable TH.Name (Machine inp) where
+  def n v = Machine $ \k ->
+    Subroutine (LetName n) (unMachine v Ret) (Call (LetName n) k)
+  ref _isRec n = Machine $ \case
+    Ret -> Jump (LetName n)
+    k -> Call (LetName n) k
+instance Cursorable (Cursor inp) => Foldable (Machine inp) where
+  {-
+  chainPre op p = go <*> p
+    where go = (H..) <$> op <*> go <|> pure H.id
+  chainPost p op = p <**> go
+    where go = (H..) <$> op <*> go <|> pure H.id
+  -}
diff --git a/src/Symantic/Univariant/Letable.hs b/src/Symantic/Univariant/Letable.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Univariant/Letable.hs
@@ -0,0 +1,225 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ExistentialQuantification #-} -- For SharingName
+-- {-# LANGUAGE MagicHash #-} -- For unsafeCoerce#
+module Symantic.Univariant.Letable where
+
+import Control.Applicative (Applicative(..))
+import Control.Monad (Monad(..))
+import Data.Bool (Bool(..))
+import Data.Eq (Eq(..))
+import Data.Foldable (foldMap)
+import Data.Function (($), (.))
+import Data.Functor ((<$>))
+import Data.Functor.Compose (Compose(..))
+import Data.HashMap.Strict (HashMap)
+import Data.HashSet (HashSet)
+import Data.Hashable (Hashable, hashWithSalt, hash)
+import Data.Int (Int)
+import Data.Maybe (Maybe(..), isNothing)
+import Data.Monoid (Monoid(..))
+import Data.Ord (Ord(..))
+-- import GHC.Exts (Int(..))
+-- import GHC.Prim (unsafeCoerce#)
+import GHC.StableName (StableName(..), makeStableName, hashStableName, eqStableName)
+-- import Numeric (showHex)
+import Prelude ((+))
+import System.IO (IO)
+import System.IO.Unsafe (unsafePerformIO)
+-- import Text.Show (Show(..))
+import qualified Control.Monad.Trans.Class as MT
+import qualified Control.Monad.Trans.Reader as MT
+import qualified Control.Monad.Trans.State as MT
+import qualified Data.HashMap.Strict as HM
+import qualified Data.HashSet as HS
+
+import Symantic.Univariant.Trans
+
+-- import Debug.Trace (trace)
+
+-- * Class 'Letable'
+-- | This class is not for manual usage like usual symantic operators,
+-- here 'def' and 'ref' are introduced by 'observeSharing'.
+class Letable letName repr where
+  -- | @('def' letName x)@ let-binds @(letName)@ to be equal to @(x)@.
+  def :: letName -> repr a -> repr a
+  -- | @('ref' isRec letName)@ is a reference to @(letName)@.
+  -- @(isRec)@ is 'True' iif. this 'ref'erence is recursive,
+  -- ie. is reachable within its 'def'inition.
+  ref :: Bool -> letName -> repr a
+  default def ::
+    Liftable1 repr => Letable letName (Output repr) =>
+    letName -> repr a -> repr a
+  default ref ::
+    Liftable repr => Letable letName (Output repr) =>
+    Bool -> letName -> repr a
+  def n = lift1 (def n)
+  ref r n = lift (ref r n)
+
+-- * Class 'MakeLetName'
+class MakeLetName letName where
+  makeLetName :: SharingName -> IO letName
+
+-- * Type 'SharingName'
+-- | Note that the observable sharing enabled by 'StableName'
+-- is not perfect as it will not observe all the sharing explicitely done.
+--
+-- Note also that the observed sharing could be different between ghc and ghci.
+data SharingName = forall a. SharingName (StableName a)
+-- | @('makeSharingName' x)@ is like @('makeStableName' x)@ but it also forces
+-- evaluation of @(x)@ to ensure that the 'StableName' is correct first time,
+-- which avoids to produce a tree bigger than needed.
+--
+-- Note that this function uses 'unsafePerformIO' instead of returning in 'IO',
+-- this is apparently required to avoid infinite loops due to unstable 'StableName'
+-- in compiled code, and sometimes also in ghci.
+--
+-- Note that maybe [pseq should be used here](https://gitlab.haskell.org/ghc/ghc/-/issues/2916).
+makeSharingName :: a -> SharingName
+makeSharingName !x = SharingName $ unsafePerformIO $ makeStableName x
+
+instance Eq SharingName where
+  SharingName x == SharingName y = eqStableName x y
+instance Hashable SharingName where
+  hash (SharingName n) = hashStableName n
+  hashWithSalt salt (SharingName n) = hashWithSalt salt n
+{-
+instance Show SharingName where
+  showsPrec _ (SharingName n) = showHex (I# (unsafeCoerce# n))
+-}
+
+-- * Type 'ObserveSharing'
+-- | Interpreter detecting some (Haskell embedded) @let@ definitions used at
+-- least once and/or recursively, in order to replace them
+-- with the 'def' and 'ref' combinators.
+-- See [Type-safe observable sharing in Haskell](https://doi.org/10.1145/1596638.1596653)
+newtype ObserveSharing letName repr a = ObserveSharing { unObserveSharing ::
+  MT.ReaderT (HashSet SharingName)
+             (MT.State (ObserveSharingState letName))
+             (CleanDefs letName repr a) }
+
+observeSharing ::
+  Eq letName =>
+  Hashable letName =>
+  ObserveSharing letName repr a -> repr a
+observeSharing (ObserveSharing m) = do
+  let (a, st) = MT.runReaderT m mempty `MT.runState`
+        ObserveSharingState
+          { oss_refs = HM.empty
+          , oss_recs = HS.empty
+          }
+  let refs = HS.fromList $
+        (`foldMap` oss_refs st) $ (\(letName, refCount) ->
+          if refCount > 0 then [letName] else [])
+  -- trace (show refs) $
+  unCleanDefs a refs
+
+-- ** Type 'ObserveSharingState'
+data ObserveSharingState letName = ObserveSharingState
+  { oss_refs :: HashMap SharingName (letName, Int)
+  , oss_recs :: HashSet SharingName
+    -- ^ TODO: unused so far, will it be useful somewhere at a later stage?
+  }
+
+observeSharingNode ::
+  Eq letName =>
+  Hashable letName =>
+  Letable letName repr =>
+  MakeLetName letName =>
+  ObserveSharing letName repr a -> ObserveSharing letName repr a
+observeSharingNode (ObserveSharing m) = ObserveSharing $ do
+  let nodeName = makeSharingName m
+  st <- MT.lift MT.get
+  ((letName, before), preds) <- getCompose $ HM.alterF (\before ->
+    Compose $ case before of
+      Nothing -> do
+        let letName = unsafePerformIO $ makeLetName nodeName
+        return ((letName, before), Just (letName, 0))
+      Just (letName, refCount) -> do
+        return ((letName, before), Just (letName, refCount + 1))
+    ) nodeName (oss_refs st)
+  parentNames <- MT.ask
+  if nodeName `HS.member` parentNames
+  then do
+    MT.lift $ MT.put st
+      { oss_refs = preds
+      , oss_recs = HS.insert nodeName (oss_recs st)
+      }
+    return $ ref True letName
+  else do
+    MT.lift $ MT.put st{ oss_refs = preds }
+    if isNothing before
+      then MT.local (HS.insert nodeName) (def letName <$> m)
+      else return $ ref False letName
+
+type instance Output (ObserveSharing letName repr) = CleanDefs letName repr
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  ) => Trans (CleanDefs letName repr) (ObserveSharing letName repr) where
+  trans = observeSharingNode . ObserveSharing . return
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  ) => Trans1 (CleanDefs letName repr) (ObserveSharing letName repr) where
+  trans1 f x = observeSharingNode $ ObserveSharing $
+    f <$> unObserveSharing x
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  ) => Trans2 (CleanDefs letName repr) (ObserveSharing letName repr) where
+  trans2 f x y = observeSharingNode $ ObserveSharing $
+    f <$> unObserveSharing x
+      <*> unObserveSharing y
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  ) => Trans3 (CleanDefs letName repr) (ObserveSharing letName repr) where
+  trans3 f x y z = observeSharingNode $ ObserveSharing $
+    f <$> unObserveSharing x
+      <*> unObserveSharing y
+      <*> unObserveSharing z
+instance
+  ( Letable letName repr
+  , MakeLetName letName
+  , Eq letName
+  , Hashable letName
+  ) => Letable letName (ObserveSharing letName repr)
+
+-- * Type 'CleanDefs'
+-- | Remove 'def' when non-recursive or unused.
+newtype CleanDefs letName repr a = CleanDefs { unCleanDefs ::
+  HS.HashSet letName -> repr a }
+
+type instance Output (CleanDefs _letName repr) = repr
+instance Trans repr (CleanDefs letName repr) where
+  trans = CleanDefs . pure
+instance Trans1 repr (CleanDefs letName repr) where
+  trans1 f x = CleanDefs $ f <$> unCleanDefs x
+instance Trans2 repr (CleanDefs letName repr) where
+  trans2 f x y = CleanDefs $
+    f <$> unCleanDefs x
+      <*> unCleanDefs y
+instance Trans3 repr (CleanDefs letName repr) where
+  trans3 f x y z = CleanDefs $
+    f <$> unCleanDefs x
+      <*> unCleanDefs y
+      <*> unCleanDefs z
+instance
+  ( Letable letName repr
+  , Eq letName
+  , Hashable letName
+  ) => Letable letName (CleanDefs letName repr) where
+  def name x = CleanDefs $ \refs ->
+    if name `HS.member` refs
+    then -- Perserve 'def'
+      def name $ unCleanDefs x refs
+    else -- Remove 'def'
+      unCleanDefs x refs
diff --git a/src/Symantic/Univariant/Trans.hs b/src/Symantic/Univariant/Trans.hs
new file mode 100644
--- /dev/null
+++ b/src/Symantic/Univariant/Trans.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE ConstraintKinds #-} -- For type class synonyms
+{-# LANGUAGE DefaultSignatures #-} -- For adding Trans* constraints
+module Symantic.Univariant.Trans where
+
+-- TODO: move to symantic-univariant
+
+import Data.Function ((.))
+import Data.Kind (Type)
+
+-- * Type family 'Output'
+type family Output (repr :: Type -> Type) :: Type -> Type
+
+-- * Class 'Trans'
+-- | A 'trans'lation from an interpreter @(from)@ to an interpreter @(to)@.
+class Trans from to where
+  trans :: from a -> to a
+
+-- * Class 'BiTrans'
+-- | Convenient type class synonym.
+-- Note that this is not necessarily a bijective 'trans'lation, a 'trans' being not necessarily injective nor surjective.
+type BiTrans from to = (Trans from to, Trans to from)
+
+-- ** Class 'Liftable'
+-- | Convenient type class synonym for using 'Output'
+type Liftable repr = Trans (Output repr) repr
+lift :: forall repr a.
+  Liftable repr =>
+  Output repr a -> repr a
+lift = trans @(Output repr)
+{-# INLINE lift #-}
+
+unlift :: forall repr a.
+  Trans repr (Output repr) =>
+  repr a -> Output repr a
+unlift = trans @repr
+{-# INLINE unlift #-}
+
+-- ** Class 'Unliftable'
+-- | Convenient type class synonym for using 'Output'
+type Unliftable repr = Trans repr (Output repr)
+
+-- * Class 'Trans1'
+class Trans1 from to where
+  trans1 ::
+    (from a -> from b) ->
+    to a -> to b
+  default trans1 ::
+    BiTrans from to =>
+    (from a -> from b) ->
+    to a -> to b
+  trans1 f = trans . f . trans
+  {-# INLINE trans1 #-}
+
+-- ** Class 'Liftable1'
+-- | Convenient type class synonym for using 'Output'
+type Liftable1 repr = Trans1 (Output repr) repr
+lift1 :: forall repr a b.
+  Liftable1 repr =>
+  (Output repr a -> Output repr b) ->
+  repr a -> repr b
+lift1 = trans1 @(Output repr)
+{-# INLINE lift1 #-}
+
+-- * Class 'Trans2'
+class Trans2 from to where
+  trans2 ::
+    (from a -> from b -> from c) ->
+    to a -> to b -> to c
+  default trans2 ::
+    BiTrans from to =>
+    (from a -> from b -> from c) ->
+    to a -> to b -> to c
+  trans2 f a b = trans (f (trans a) (trans b))
+  {-# INLINE trans2 #-}
+
+-- ** Class 'Liftable2'
+-- | Convenient type class synonym for using 'Output'
+type Liftable2 repr = Trans2 (Output repr) repr
+lift2 :: forall repr a b c.
+  Liftable2 repr =>
+  (Output repr a -> Output repr b -> Output repr c) ->
+  repr a -> repr b -> repr c
+lift2 = trans2 @(Output repr)
+{-# INLINE lift2 #-}
+
+-- * Class 'Trans3'
+class Trans3 from to where
+  trans3 ::
+    (from a -> from b -> from c -> from d) ->
+    to a -> to b -> to c -> to d
+  default trans3 ::
+    BiTrans from to =>
+    (from a -> from b -> from c -> from d) ->
+    to a -> to b -> to c -> to d
+  trans3 f a b c = trans (f (trans a) (trans b) (trans c))
+  {-# INLINE trans3 #-}
+
+-- ** Class 'Liftable3'
+-- | Convenient type class synonym for using 'Output'
+type Liftable3 repr = Trans3 (Output repr) repr
+lift3 :: forall repr a b c d.
+  Liftable3 repr =>
+  (Output repr a -> Output repr b -> Output repr c -> Output repr d) ->
+  repr a -> repr b -> repr c -> repr d
+lift3 = trans3 @(Output repr)
+{-# INLINE lift3 #-}
+
+-- * Type 'Any'
+-- | A newtype to disambiguate the 'Trans' instance to any other interpreter when there is also one or more 'Trans's to other interpreters with a different interpretation than the generic one.
+newtype Any repr a = Any { unAny :: repr a }
+type instance Output (Any repr) = repr
+instance Trans (Any repr) repr where
+  trans = unAny
+instance Trans1 (Any repr) repr
+instance Trans2 (Any repr) repr
+instance Trans3 (Any repr) repr
+instance Trans repr (Any repr) where
+  trans = Any
+instance Trans1 repr (Any repr)
+instance Trans2 repr (Any repr)
+instance Trans3 repr (Any repr)
diff --git a/symantic-parser.cabal b/symantic-parser.cabal
new file mode 100644
--- /dev/null
+++ b/symantic-parser.cabal
@@ -0,0 +1,153 @@
+cabal-version: 2.2
+name: symantic-parser
+version: 0.0.0.20210101
+synopsis: Parser combinators statically optimized and staged via typed meta-programming
+description:
+  This is a work-in-progress experimental library to generate parsers,
+  leveraging Tagless-Final interpreters and Typed Template Haskell staging.
+  .
+  This is an alternative but less powerful/reviewed
+  implementation of [ParsleyHaskell](https://github.com/J-mie6/ParsleyHaskell).
+  See the paper by Jamie Willis, Nicolas Wu, and Matthew
+  Pickering, admirably well presented at ICFP-2020: [Staged
+  Selective Parser
+  Combinators](https://icfp20.sigplan.org/details/icfp-2020-papers/20/Staged-Selective-Parser-Combinators).
+license: GPL-3.0-or-later
+author:      Julien Moutinho <julm+symantic-parser@sourcephile.fr>
+maintainer:  Julien Moutinho <julm+symantic-parser@sourcephile.fr>
+bug-reports: Julien Moutinho <julm+symantic-parser@sourcephile.fr>
+copyright:   Julien Moutinho <julm+symantic-parser@sourcephile.fr>
+stability: experimental
+category: Parsing
+extra-doc-files:
+  ChangeLog.md
+  ReadMe.md
+  ToDo.md
+extra-source-files:
+  .envrc
+  Makefile
+  cabal.project
+  default.nix
+  flake.nix
+  shell.nix
+extra-tmp-files:
+build-type: Simple
+tested-with: GHC==9.0.0
+
+source-repository head
+  type: git
+  location: git://git.sourcephile.fr/haskell/symantic-parser
+
+flag dump-core
+  description: Dump GHC's Core in HTML
+  manual: True
+  default: False
+
+flag dump-splices
+  description: Dump code generated by Template Haskell
+  manual: True
+  default: False
+
+common boilerplate
+  default-language: Haskell2010
+  default-extensions:
+    BangPatterns,
+    DataKinds,
+    FlexibleContexts,
+    FlexibleInstances,
+    GADTs,
+    GeneralizedNewtypeDeriving,
+    LambdaCase,
+    MultiParamTypeClasses,
+    NamedFieldPuns,
+    NoImplicitPrelude,
+    RankNTypes,
+    RecordWildCards,
+    ScopedTypeVariables,
+    TypeApplications,
+    TypeFamilies,
+    TypeOperators
+  ghc-options:
+    -Wall
+    -Wincomplete-uni-patterns
+    -Wincomplete-record-updates
+    -fhide-source-paths
+    -freverse-errors
+
+library
+  import: boilerplate
+  hs-source-dirs: src
+  exposed-modules:
+    Symantic.Univariant.Letable
+    Symantic.Univariant.Trans
+    Symantic.Parser
+    Symantic.Parser.Grammar
+    Symantic.Parser.Grammar.Combinators
+    Symantic.Parser.Grammar.Dump
+    Symantic.Parser.Grammar.Fixity
+    Symantic.Parser.Grammar.ObserveSharing
+    Symantic.Parser.Grammar.Optimize
+    Symantic.Parser.Grammar.Write
+    Symantic.Parser.Haskell
+    Symantic.Parser.Machine
+    Symantic.Parser.Machine.Dump
+    Symantic.Parser.Machine.Generate
+    Symantic.Parser.Machine.Input
+    Symantic.Parser.Machine.Instructions
+  build-depends:
+    base >=4.10 && <5,
+    array,
+    bytestring,
+    containers,
+    ghc-prim,
+    hashable,
+    template-haskell >= 2.16,
+    text,
+    transformers,
+    unordered-containers
+
+test-suite symantic-parser-test
+  import: boilerplate
+  type: exitcode-stdio-1.0
+  hs-source-dirs: test
+  main-is: Main.hs
+  other-modules:
+    Golden
+    Golden.Grammar
+    -- Golden.Utils
+    -- Golden.Parsers
+    -- HUnit
+    -- QuickCheck
+  default-extensions:
+    ViewPatterns
+  ghc-options:
+  build-depends:
+    symantic-parser,
+    base >= 4.10 && < 5,
+    bytestring >= 0.10,
+    containers >= 0.5,
+    deepseq >= 1.4,
+    directory >= 1.3,
+    filepath >= 1.4,
+    hashable >= 1.2.6,
+    process >= 1.6,
+    strict >= 0.4,
+    tasty >= 0.11,
+    tasty-golden >= 2.3,
+    -- tasty-hunit,
+    template-haskell >= 2.16,
+    -- temporary >= 1.3,
+    text >= 1.2,
+    -- time >= 1.9,
+    transformers >= 0.4,
+    -- QuickCheck >= 2.0,
+    -- tasty-quickcheck,
+    unix >= 2.7,
+    unordered-containers
+  if flag(dump-core)
+    build-depends: dump-core
+    ghc-options: -fplugin=DumpCore
+  if flag(dump-splices)
+    ghc-options:
+      -ddump-splices
+      -ddump-to-file
diff --git a/test/Golden.hs b/test/Golden.hs
new file mode 100644
--- /dev/null
+++ b/test/Golden.hs
@@ -0,0 +1,141 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UnboxedTuples #-}
+module Golden where
+
+import Control.Monad (Monad(..))
+import Data.Char (Char)
+import Data.Either (Either(..))
+import Data.Function (($))
+import Data.Semigroup (Semigroup(..))
+import Data.String (String, IsString(..))
+import Data.Text (Text)
+import Data.Text.IO (readFile)
+import System.IO (IO, FilePath)
+import Test.Tasty
+import Test.Tasty.Golden
+import Text.Show (Show(..))
+import qualified Data.ByteString.Lazy as BSL
+import qualified Data.IORef as IORef
+import qualified Data.Text.Lazy as TL
+import qualified Data.Text.Lazy.Encoding as TL
+import qualified Language.Haskell.TH.Syntax as TH
+
+import qualified Symantic.Parser as P
+import qualified Symantic.Parser.Haskell as H
+import qualified Golden.Grammar as Grammar
+--import Golden.Utils
+
+goldensIO :: IO TestTree
+goldensIO = return $ testGroup "Golden"
+  [ goldensGrammar
+  -- Commented-out for the release
+  -- because resetTHNameCounter is not enough:
+  -- TH names still change between runs
+  -- with and without --accept
+  -- , goldensMachine
+  , goldensParser
+  ]
+
+goldensGrammar :: TestTree
+goldensGrammar = testGroup "Grammar"
+  [ testGroup "DumpComb" $ tests $ \name repr ->
+    let file = "test/Golden/Grammar/"<>name<>".dump" in
+    goldenVsStringDiff file diffGolden file $ do
+      resetTHNameCounter
+      return $ fromString $ show $
+        P.dumpComb $ P.observeSharing repr
+  , testGroup "OptimizeComb" $ tests $ \name repr ->
+    let file = "test/Golden/Grammar/"<>name<>".opt.dump" in
+    goldenVsStringDiff file diffGolden file $ do
+      resetTHNameCounter
+      return $ fromString $ show $
+        P.dumpComb $ P.optimizeComb $ P.observeSharing repr
+  ]
+  where
+  tests :: P.Grammar repr =>
+           P.Satisfiable repr Char =>
+           (forall a. String -> repr a -> TestTree) -> [TestTree]
+  tests test =
+    [ test "unit" $ P.unit
+    , test "unit-unit" $ P.unit P.*> P.unit
+    , test "app" $ P.pure (H.Haskell H.id) P.<*> P.unit
+    , test "many-a" $ P.many (P.char 'a')
+    , test "boom" $ Grammar.boom
+    , test "brainfuck" $ Grammar.brainfuck
+    , test "many-char-eof" $ P.many (P.char 'r') P.<* P.eof
+    , test "eof" $ P.eof
+    ]
+
+goldensMachine :: TestTree
+goldensMachine = testGroup "Machine"
+  [ testGroup "DumpInstr" $ tests $ \name repr ->
+    let file = "test/Golden/Machine/"<>name<>".dump" in
+    goldenVsStringDiff file diffGolden file $ do
+      resetTHNameCounter
+      return $ fromString $ show $
+        P.dumpInstr $ {-P.machine @() $ -}repr
+  ]
+  where
+  tests ::
+    P.Executable repr =>
+    P.Readable repr Char =>
+    (forall vs es ret. String -> repr Text vs es ret -> TestTree) -> [TestTree]
+  tests test =
+    [ test "unit" $ P.machine $ P.unit
+    , test "unit-unit" $ P.machine $ P.unit P.*> P.unit
+    , test "a-or-b" $ P.machine $ P.char 'a' P.<|> P.char 'b'
+    , test "app" $ P.machine $ P.pure (H.Haskell H.id) P.<*> P.unit
+    , test "many-a" $ P.machine $ P.many (P.char 'a')
+    , test "boom" $ P.machine $ Grammar.boom
+    , test "brainfuck" $ P.machine $ Grammar.brainfuck
+    , test "many-char-eof" $ P.machine $ P.many (P.char 'r') P.<* P.eof
+    , test "eof" $ P.machine $ P.eof
+    , test "many-char-fail" $ P.machine $ P.many (P.char 'a') P.<* P.char 'b'
+    ]
+
+goldensParser :: TestTree
+goldensParser = testGroup "Parser"
+  [ testGroup "runParser" $ tests $ \name p ->
+    let file = "test/Golden/Parser/"<>name in
+    goldenVsStringDiff (file<>".txt") diffGolden (file<>".dump") $ do
+      input :: Text <- readFile (file<>".txt")
+      return $ fromString $
+        case p input of
+          Left err -> show err
+          Right a -> show a
+  ]
+  where
+  tests :: (forall a. Show a => String -> (Text -> Either (P.ParsingError Text) a) -> TestTree) -> [TestTree]
+  tests test =
+    [ test "char" $$(P.runParser $ P.char 'a')
+    , test "string" $$(P.runParser $ P.string "ab")
+    , test "many-char" $$(P.runParser $ P.many (P.char 'a'))
+    , test "alt-right" $$(P.runParser $ P.string "aa" P.<|> P.string "ab")
+    , test "alt-right-try" $$(P.runParser $ P.try (P.string "aa") P.<|> P.string "ab")
+    , test "alt-left" $$(P.runParser $ P.string "aa" P.<|> P.string "ab")
+    , test "many-char-eof" $$(P.runParser $ P.many (P.char 'r') P.<* P.eof)
+    , test "eof" $$(P.runParser $ P.eof)
+    , test "eof-fail" $$(P.runParser $ P.eof)
+    -- , test "alt-char-fail" $$(P.runParser $ P.char 'a' P.<|> P.char 'b')
+    -- , test "alt-char-fail" $$(P.runParser $ P.some (P.char 'a') P.<|> P.string "b")
+    , test "many-char-fail" $$(P.runParser $ P.many (P.char 'a') P.<* P.char 'b')
+    -- , test "alt-char-try-fail" $$(P.runParser $ P.try (P.char 'a') P.<|> P.char 'b')
+    ]
+
+-- | Resetting 'TH.counter' makes 'makeLetName' deterministic,
+-- except when profiling is enabled, in this case those tests may fail
+-- due to a different numbering of the 'def' and 'ref' combinators.
+resetTHNameCounter :: IO ()
+resetTHNameCounter = IORef.writeIORef TH.counter 0
+
+-- * Golden testing utilities
+
+diffGolden :: FilePath -> FilePath -> [String]
+diffGolden ref new = ["diff", "-u", ref, new]
+
+unLeft :: Either String BSL.ByteString -> IO BSL.ByteString
+unLeft = \case
+  Left err -> return $ TL.encodeUtf8 $ TL.pack err
+  Right a  -> return a
diff --git a/test/Golden/Grammar.hs b/test/Golden/Grammar.hs
new file mode 100644
--- /dev/null
+++ b/test/Golden/Grammar.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Golden.Grammar where
+
+import Data.Char (Char)
+import Data.Eq (Eq)
+import Data.Int (Int)
+import Data.String (String)
+import Prelude (undefined)
+import Text.Show (Show)
+import qualified Prelude
+import qualified Language.Haskell.TH as TH
+
+import Symantic.Parser
+import qualified Symantic.Parser.Haskell as H
+
+data Expr = Var String | Num Int | Add Expr Expr deriving Show
+data Asgn = Asgn String Expr deriving Show
+
+data BrainFuckOp = RightPointer | LeftPointer | Increment | Decrement | Output | Input | Loop [BrainFuckOp] deriving (Show, Eq)
+
+{-
+cinput = m --try (string "aaa") <|> string "db" --(string "aab" <|> string "aac") --(char 'a' <|> char 'b') *> string "ab"
+  where
+    --m = match "ab" (lookAhead item) op empty
+    --op 'a' = item $> haskell "aaaaa"
+    --op 'b' = item $> haskell "bbbbb"
+    m = bf <* item
+    -- match :: Eq a => [Pure repr a] -> repr a -> (Pure repr a -> repr b) -> repr b -> repr b
+    bf = match [char '>'] item op empty
+    op (H.ValueCode '>' _) = string ">"
+-}
+
+--defuncTest = haskell Just <$> (haskell (+) <$> (item $> haskell 1) <*> (item $> haskell 8))
+
+-- manyTest = many (string "ab" $> (haskell 'c'))
+
+--nfb = negLook (char 'a') <|> void (string "ab")
+
+--skipManyInspect = skipMany (char 'a')
+
+boom :: Applicable repr => repr ()
+boom =
+  let foo = (-- newRegister_ unit (\r0 ->
+       let goo = (-- newRegister_ unit (\r1 ->
+             let hoo = {-get r0 <~> get r1 *>-} goo *> hoo in hoo
+            ) *> goo
+       in goo) *> pure H.unit
+  in foo *> foo
+
+haskell :: a -> TH.CodeQ a -> H.Haskell a
+haskell e c = H.Haskell (H.ValueCode (H.Value e) c)
+
+brainfuck :: Satisfiable repr Char => Grammar repr => repr [BrainFuckOp]
+brainfuck = whitespace *> bf
+  where
+    whitespace = skipMany (noneOf "<>+-[],.$")
+    lexeme p = p <* whitespace
+    -- match :: Eq a => [Pure repr a] -> repr a -> (Pure repr a -> repr b) -> repr b -> repr b
+    bf = many (lexeme (match ((\c -> haskell c [||c||]) Prelude.<$> "><+-.,[") (look anyChar) op empty))
+    --op :: H.Haskell Char -> repr BrainFuckOp
+    op (H.Haskell (H.ValueCode (H.Value c) _)) = case c of
+     '>' -> anyChar $> haskell RightPointer [||RightPointer||]
+     '<' -> anyChar $> haskell LeftPointer  [||LeftPointer||]
+     '+' -> anyChar $> haskell Increment    [||Increment||]
+     '-' -> anyChar $> haskell Decrement    [||Decrement||]
+     '.' -> anyChar $> haskell Output       [||Output||]
+     ',' -> anyChar $> haskell Input        [||Input||]
+     '[' -> between (lexeme anyChar) (char ']') (haskell Loop [||Loop||] <$> bf)
+     _ -> undefined
+    op _ = undefined
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,17 @@
+module Main where
+
+import System.IO (IO)
+import Data.Function (($))
+
+import Test.Tasty
+import Golden
+--import HUnit
+
+main :: IO ()
+main = do
+  goldens <- goldensIO
+  defaultMain $
+    testGroup ""
+     [ goldens
+     --, hunits
+     ]