diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,12 @@
+Copyright (C) 2024 Andreas Abel
+
+Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
diff --git a/src/ColorOption.hs b/src/ColorOption.hs
new file mode 100644
--- /dev/null
+++ b/src/ColorOption.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+
+{- Originally written by chatgpt.com 2024-12-10 from the following prompt:
+
+> Please write me an options parser in Haskell using the optparse-applicative package that can parse the option given as follows:
+
+> ... from https://www.gnu.org/software/gettext/manual/html_node/The-_002d_002dcolor-option.html
+
+Cut down to my purposes.
+
+-}
+
+module ColorOption where
+
+import Options.Applicative
+  ( Parser, ReadM, eitherReader, help, long, metavar, option, value
+  )
+
+-- | Values of the GNU option @--color@.
+
+data ColorOption = Always | Never | Auto
+  deriving (Eq)
+
+-- | Parser for the option @--color@.
+
+colorOption :: Parser ColorOption
+colorOption =
+  option readColorOption
+    $  long "color"
+    <> metavar "when"
+    <> value Auto
+    <> help "Specify when colorized output should be generated. Options: always, never, auto. Default: auto."
+
+-- | Read string input into 'ColorOption'.
+
+readColorOption :: ReadM ColorOption
+readColorOption = eitherReader $ \case
+  "always" -> Right Always
+  "yes"    -> Right Always
+  "never"  -> Right Never
+  "no"     -> Right Never
+  "auto"   -> Right Auto
+  "tty"    -> Right Auto
+  invalid  -> Left $ "Invalid color option: " ++ invalid
diff --git a/src/Lam/Abs.hs b/src/Lam/Abs.hs
new file mode 100644
--- /dev/null
+++ b/src/Lam/Abs.hs
@@ -0,0 +1,27 @@
+-- File generated by the BNF Converter (bnfc 2.9.6).
+
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+-- | The abstract syntax of language Lam.
+
+module Lam.Abs where
+
+import Prelude (String)
+import qualified Prelude as C (Eq, Ord, Show, Read)
+import qualified Data.String
+
+data Exp = EId Ident | EApp Exp Exp | EAbs Lambda Ident Arrow Exp
+  deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Ty = TId Ident | TArr Ty Arrow Ty
+  deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+newtype Ident = Ident String
+  deriving (C.Eq, C.Ord, C.Show, C.Read, Data.String.IsString)
+
+newtype Lambda = Lambda String
+  deriving (C.Eq, C.Ord, C.Show, C.Read, Data.String.IsString)
+
+newtype Arrow = Arrow String
+  deriving (C.Eq, C.Ord, C.Show, C.Read, Data.String.IsString)
+
diff --git a/src/Lam/Lex.hs b/src/Lam/Lex.hs
new file mode 100644
--- /dev/null
+++ b/src/Lam/Lex.hs
@@ -0,0 +1,493 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+{-# OPTIONS_GHC -fno-warn-unused-binds #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE MagicHash #-}
+{-# LINE 4 "Lam/Lex.x" #-}
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+{-# OPTIONS_GHC -w #-}
+
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lam.Lex where
+
+import Prelude
+
+import qualified Data.Bits
+import Data.Char     (ord)
+import Data.Function (on)
+import Data.Word     (Word8)
+#include "ghcconfig.h"
+import qualified Data.Array
+import Data.Array.Base (unsafeAt)
+import GHC.Exts (Addr#,Int#,Int(I#),(*#),(+#),(-#),(==#),(>=#),indexCharOffAddr#,indexInt16OffAddr#,indexInt32OffAddr#,int2Word#,narrow16Int#,narrow32Int#,negateInt#,or#,ord#,uncheckedShiftL#,word2Int#)
+import qualified GHC.Exts
+alex_tab_size :: Int
+alex_tab_size = 8
+alex_base :: AlexAddr
+alex_base = AlexA#
+  "\xf8\xff\xff\xff\x4b\xff\xff\xff\x9a\x00\x00\x00\xc9\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xf3\xff\xff\xff\x7b\xff\xff\xff\x88\xff\xff\xff"#
+
+alex_table :: AlexAddr
+alex_table = AlexA#
+  "\x00\x00\x07\x00\x07\x00\x07\x00\x07\x00\x07\x00\x05\x00\x04\x00\x07\x00\x07\x00\x07\x00\x07\x00\x07\x00\x04\x00\x09\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x07\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x07\x00\x06\x00\x06\x00\x00\x00\x00\x00\x00\x00\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x00\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x00\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0a\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02\x00\x00\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#
+
+alex_check :: AlexAddr
+alex_check = AlexA#
+  "\xff\xff\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\xbb\x00\x3e\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x92\x00\x86\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\x28\x00\x29\x00\xff\xff\xff\xff\xff\xff\x2d\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\x5c\x00\xff\xff\xff\xff\xff\xff\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\xff\xff\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xff\xff\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xc3\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x27\x00\xff\xff\xff\xff\xff\xff\xff\xff\xce\x00\xff\xff\xff\xff\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xe2\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xc3\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#
+
+alex_deflt :: AlexAddr
+alex_deflt = AlexA#
+  "\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#
+
+alex_accept = Data.Array.listArray (0 :: Int, 10)
+  [ AlexAccNone
+  , AlexAccNone
+  , AlexAcc 3
+  , AlexAccNone
+  , AlexAcc 2
+  , AlexAcc 1
+  , AlexAcc 0
+  , AlexAccSkip
+  , AlexAccNone
+  , AlexAccNone
+  , AlexAccNone
+  ]
+
+alex_actions = Data.Array.array (0 :: Int, 4)
+  [ (3,alex_action_4)
+  , (2,alex_action_3)
+  , (1,alex_action_2)
+  , (0,alex_action_1)
+  ]
+
+alex_action_1 = tok (eitherResIdent TV)
+alex_action_2 = tok (eitherResIdent T_Lambda)
+alex_action_3 = tok (eitherResIdent T_Arrow)
+alex_action_4 = tok (eitherResIdent TV)
+
+#define ALEX_GHC 1
+#define ALEX_NOPRED 1
+-- -----------------------------------------------------------------------------
+-- ALEX TEMPLATE
+--
+-- This code is in the PUBLIC DOMAIN; you may copy it freely and use
+-- it for any purpose whatsoever.
+
+-- -----------------------------------------------------------------------------
+-- INTERNALS and main scanner engine
+
+#ifdef ALEX_GHC
+#  define ILIT(n) n#
+#  define IBOX(n) (I# (n))
+#  define FAST_INT Int#
+-- Do not remove this comment. Required to fix CPP parsing when using GCC and a clang-compiled alex.
+#  if __GLASGOW_HASKELL__ > 706
+#    define GTE(n,m) (GHC.Exts.tagToEnum# (n >=# m))
+#    define EQ(n,m) (GHC.Exts.tagToEnum# (n ==# m))
+#  else
+#    define GTE(n,m) (n >=# m)
+#    define EQ(n,m) (n ==# m)
+#  endif
+#  define PLUS(n,m) (n +# m)
+#  define MINUS(n,m) (n -# m)
+#  define TIMES(n,m) (n *# m)
+#  define NEGATE(n) (negateInt# (n))
+#  define IF_GHC(x) (x)
+#else
+#  define ILIT(n) (n)
+#  define IBOX(n) (n)
+#  define FAST_INT Int
+#  define GTE(n,m) (n >= m)
+#  define EQ(n,m) (n == m)
+#  define PLUS(n,m) (n + m)
+#  define MINUS(n,m) (n - m)
+#  define TIMES(n,m) (n * m)
+#  define NEGATE(n) (negate (n))
+#  define IF_GHC(x)
+#endif
+
+#ifdef ALEX_GHC
+data AlexAddr = AlexA# Addr#
+-- Do not remove this comment. Required to fix CPP parsing when using GCC and a clang-compiled alex.
+
+{-# INLINE alexIndexInt16OffAddr #-}
+alexIndexInt16OffAddr :: AlexAddr -> Int# -> Int#
+alexIndexInt16OffAddr (AlexA# arr) off =
+#ifdef WORDS_BIGENDIAN
+  narrow16Int# i
+  where
+        i    = word2Int# ((high `uncheckedShiftL#` 8#) `or#` low)
+        high = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))
+        low  = int2Word# (ord# (indexCharOffAddr# arr off'))
+        off' = off *# 2#
+#else
+#if __GLASGOW_HASKELL__ >= 901
+  GHC.Exts.int16ToInt#
+#endif
+    (indexInt16OffAddr# arr off)
+#endif
+#else
+alexIndexInt16OffAddr = (Data.Array.!)
+#endif
+
+#ifdef ALEX_GHC
+{-# INLINE alexIndexInt32OffAddr #-}
+alexIndexInt32OffAddr :: AlexAddr -> Int# -> Int#
+alexIndexInt32OffAddr (AlexA# arr) off =
+#ifdef WORDS_BIGENDIAN
+  narrow32Int# i
+  where
+   i    = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#`
+                     (b2 `uncheckedShiftL#` 16#) `or#`
+                     (b1 `uncheckedShiftL#` 8#) `or#` b0)
+   b3   = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#)))
+   b2   = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#)))
+   b1   = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))
+   b0   = int2Word# (ord# (indexCharOffAddr# arr off'))
+   off' = off *# 4#
+#else
+#if __GLASGOW_HASKELL__ >= 901
+  GHC.Exts.int32ToInt#
+#endif
+    (indexInt32OffAddr# arr off)
+#endif
+#else
+alexIndexInt32OffAddr = (Data.Array.!)
+#endif
+
+#ifdef ALEX_GHC
+-- GHC >= 503, unsafeAt is available from Data.Array.Base.
+quickIndex = unsafeAt
+#else
+quickIndex = (Data.Array.!)
+#endif
+
+-- -----------------------------------------------------------------------------
+-- Main lexing routines
+
+data AlexReturn a
+  = AlexEOF
+  | AlexError  !AlexInput
+  | AlexSkip   !AlexInput !Int
+  | AlexToken  !AlexInput !Int a
+
+-- alexScan :: AlexInput -> StartCode -> AlexReturn a
+alexScan input__ IBOX(sc)
+  = alexScanUser undefined input__ IBOX(sc)
+
+alexScanUser user__ input__ IBOX(sc)
+  = case alex_scan_tkn user__ input__ ILIT(0) input__ sc AlexNone of
+  (AlexNone, input__') ->
+    case alexGetByte input__ of
+      Nothing ->
+#ifdef ALEX_DEBUG
+                                   Debug.Trace.trace ("End of input.") $
+#endif
+                                   AlexEOF
+      Just _ ->
+#ifdef ALEX_DEBUG
+                                   Debug.Trace.trace ("Error.") $
+#endif
+                                   AlexError input__'
+
+  (AlexLastSkip input__'' len, _) ->
+#ifdef ALEX_DEBUG
+    Debug.Trace.trace ("Skipping.") $
+#endif
+    AlexSkip input__'' len
+
+  (AlexLastAcc k input__''' len, _) ->
+#ifdef ALEX_DEBUG
+    Debug.Trace.trace ("Accept.") $
+#endif
+    AlexToken input__''' len ((Data.Array.!) alex_actions k)
+
+
+-- Push the input through the DFA, remembering the most recent accepting
+-- state it encountered.
+
+alex_scan_tkn user__ orig_input len input__ s last_acc =
+  input__ `seq` -- strict in the input
+  let
+  new_acc = (check_accs (alex_accept `quickIndex` IBOX(s)))
+  in
+  new_acc `seq`
+  case alexGetByte input__ of
+     Nothing -> (new_acc, input__)
+     Just (c, new_input) ->
+#ifdef ALEX_DEBUG
+      Debug.Trace.trace ("State: " ++ show IBOX(s) ++ ", char: " ++ show c ++ " " ++ (show . chr . fromIntegral) c) $
+#endif
+      case fromIntegral c of { IBOX(ord_c) ->
+        let
+                base   = alexIndexInt32OffAddr alex_base s
+                offset = PLUS(base,ord_c)
+
+                new_s = if GTE(offset,ILIT(0))
+                          && let check  = alexIndexInt16OffAddr alex_check offset
+                             in  EQ(check,ord_c)
+                          then alexIndexInt16OffAddr alex_table offset
+                          else alexIndexInt16OffAddr alex_deflt s
+        in
+        case new_s of
+            ILIT(-1) -> (new_acc, input__)
+                -- on an error, we want to keep the input *before* the
+                -- character that failed, not after.
+            _ -> alex_scan_tkn user__ orig_input
+#ifdef ALEX_LATIN1
+                   PLUS(len,ILIT(1))
+                   -- issue 119: in the latin1 encoding, *each* byte is one character
+#else
+                   (if c < 0x80 || c >= 0xC0 then PLUS(len,ILIT(1)) else len)
+                   -- note that the length is increased ONLY if this is the 1st byte in a char encoding)
+#endif
+                   new_input new_s new_acc
+      }
+  where
+        check_accs (AlexAccNone) = last_acc
+        check_accs (AlexAcc a  ) = AlexLastAcc a input__ IBOX(len)
+        check_accs (AlexAccSkip) = AlexLastSkip  input__ IBOX(len)
+#ifndef ALEX_NOPRED
+        check_accs (AlexAccPred a predx rest)
+           | predx user__ orig_input IBOX(len) input__
+           = AlexLastAcc a input__ IBOX(len)
+           | otherwise
+           = check_accs rest
+        check_accs (AlexAccSkipPred predx rest)
+           | predx user__ orig_input IBOX(len) input__
+           = AlexLastSkip input__ IBOX(len)
+           | otherwise
+           = check_accs rest
+#endif
+
+data AlexLastAcc
+  = AlexNone
+  | AlexLastAcc !Int !AlexInput !Int
+  | AlexLastSkip     !AlexInput !Int
+
+data AlexAcc user
+  = AlexAccNone
+  | AlexAcc Int
+  | AlexAccSkip
+#ifndef ALEX_NOPRED
+  | AlexAccPred Int (AlexAccPred user) (AlexAcc user)
+  | AlexAccSkipPred (AlexAccPred user) (AlexAcc user)
+
+type AlexAccPred user = user -> AlexInput -> Int -> AlexInput -> Bool
+
+-- -----------------------------------------------------------------------------
+-- Predicates on a rule
+
+alexAndPred p1 p2 user__ in1 len in2
+  = p1 user__ in1 len in2 && p2 user__ in1 len in2
+
+--alexPrevCharIsPred :: Char -> AlexAccPred _
+alexPrevCharIs c _ input__ _ _ = c == alexInputPrevChar input__
+
+alexPrevCharMatches f _ input__ _ _ = f (alexInputPrevChar input__)
+
+--alexPrevCharIsOneOfPred :: Array Char Bool -> AlexAccPred _
+alexPrevCharIsOneOf arr _ input__ _ _ = arr Data.Array.! alexInputPrevChar input__
+
+--alexRightContext :: Int -> AlexAccPred _
+alexRightContext IBOX(sc) user__ _ _ input__ =
+     case alex_scan_tkn user__ input__ ILIT(0) input__ sc AlexNone of
+          (AlexNone, _) -> False
+          _ -> True
+        -- TODO: there's no need to find the longest
+        -- match when checking the right context, just
+        -- the first match will do.
+#endif
+{-# LINE 54 "Lam/Lex.x" #-}
+-- | Create a token with position.
+tok :: (String -> Tok) -> (Posn -> String -> Token)
+tok f p = PT p . f
+
+-- | Token without position.
+data Tok
+  = TK {-# UNPACK #-} !TokSymbol  -- ^ Reserved word or symbol.
+  | TL !String                    -- ^ String literal.
+  | TI !String                    -- ^ Integer literal.
+  | TV !String                    -- ^ Identifier.
+  | TD !String                    -- ^ Float literal.
+  | TC !String                    -- ^ Character literal.
+  | T_Lambda !String
+  | T_Arrow !String
+  deriving (Eq, Show, Ord)
+
+-- | Smart constructor for 'Tok' for the sake of backwards compatibility.
+pattern TS :: String -> Int -> Tok
+pattern TS t i = TK (TokSymbol t i)
+
+-- | Keyword or symbol tokens have a unique ID.
+data TokSymbol = TokSymbol
+  { tsText :: String
+      -- ^ Keyword or symbol text.
+  , tsID   :: !Int
+      -- ^ Unique ID.
+  } deriving (Show)
+
+-- | Keyword/symbol equality is determined by the unique ID.
+instance Eq  TokSymbol where (==)    = (==)    `on` tsID
+
+-- | Keyword/symbol ordering is determined by the unique ID.
+instance Ord TokSymbol where compare = compare `on` tsID
+
+-- | Token with position.
+data Token
+  = PT  Posn Tok
+  | Err Posn
+  deriving (Eq, Show, Ord)
+
+-- | Pretty print a position.
+printPosn :: Posn -> String
+printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c
+
+-- | Pretty print the position of the first token in the list.
+tokenPos :: [Token] -> String
+tokenPos (t:_) = printPosn (tokenPosn t)
+tokenPos []    = "end of file"
+
+-- | Get the position of a token.
+tokenPosn :: Token -> Posn
+tokenPosn (PT p _) = p
+tokenPosn (Err p)  = p
+
+-- | Get line and column of a token.
+tokenLineCol :: Token -> (Int, Int)
+tokenLineCol = posLineCol . tokenPosn
+
+-- | Get line and column of a position.
+posLineCol :: Posn -> (Int, Int)
+posLineCol (Pn _ l c) = (l,c)
+
+-- | Convert a token into "position token" form.
+mkPosToken :: Token -> ((Int, Int), String)
+mkPosToken t = (tokenLineCol t, tokenText t)
+
+-- | Convert a token to its text.
+tokenText :: Token -> String
+tokenText t = case t of
+  PT _ (TS s _) -> s
+  PT _ (TL s)   -> show s
+  PT _ (TI s)   -> s
+  PT _ (TV s)   -> s
+  PT _ (TD s)   -> s
+  PT _ (TC s)   -> s
+  Err _         -> "#error"
+  PT _ (T_Lambda s) -> s
+  PT _ (T_Arrow s) -> s
+
+-- | Convert a token to a string.
+prToken :: Token -> String
+prToken t = tokenText t
+
+-- | Finite map from text to token organized as binary search tree.
+data BTree
+  = N -- ^ Nil (leaf).
+  | B String Tok BTree BTree
+      -- ^ Binary node.
+  deriving (Show)
+
+-- | Convert potential keyword into token or use fallback conversion.
+eitherResIdent :: (String -> Tok) -> String -> Tok
+eitherResIdent tv s = treeFind resWords
+  where
+  treeFind N = tv s
+  treeFind (B a t left right) =
+    case compare s a of
+      LT -> treeFind left
+      GT -> treeFind right
+      EQ -> t
+
+-- | The keywords and symbols of the language organized as binary search tree.
+resWords :: BTree
+resWords = b ")" 2 (b "(" 1 N N) N
+  where
+  b s n = B bs (TS bs n)
+    where
+    bs = s
+
+-- | Unquote string literal.
+unescapeInitTail :: String -> String
+unescapeInitTail = id . unesc . tail . id
+  where
+  unesc s = case s of
+    '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs
+    '\\':'n':cs  -> '\n' : unesc cs
+    '\\':'t':cs  -> '\t' : unesc cs
+    '\\':'r':cs  -> '\r' : unesc cs
+    '\\':'f':cs  -> '\f' : unesc cs
+    '"':[]       -> []
+    c:cs         -> c : unesc cs
+    _            -> []
+
+-------------------------------------------------------------------
+-- Alex wrapper code.
+-- A modified "posn" wrapper.
+-------------------------------------------------------------------
+
+data Posn = Pn !Int !Int !Int
+  deriving (Eq, Show, Ord)
+
+alexStartPos :: Posn
+alexStartPos = Pn 0 1 1
+
+alexMove :: Posn -> Char -> Posn
+alexMove (Pn a l c) '\t' = Pn (a+1)  l     (((c+7) `div` 8)*8+1)
+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1)   1
+alexMove (Pn a l c) _    = Pn (a+1)  l     (c+1)
+
+type Byte = Word8
+
+type AlexInput = (Posn,     -- current position,
+                  Char,     -- previous char
+                  [Byte],   -- pending bytes on the current char
+                  String)   -- current input string
+
+tokens :: String -> [Token]
+tokens str = go (alexStartPos, '\n', [], str)
+    where
+      go :: AlexInput -> [Token]
+      go inp@(pos, _, _, str) =
+               case alexScan inp 0 of
+                AlexEOF                   -> []
+                AlexError (pos, _, _, _)  -> [Err pos]
+                AlexSkip  inp' len        -> go inp'
+                AlexToken inp' len act    -> act pos (take len str) : (go inp')
+
+alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)
+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))
+alexGetByte (p, _, [], s) =
+  case s of
+    []  -> Nothing
+    (c:s) ->
+             let p'     = alexMove p c
+                 (b:bs) = utf8Encode c
+              in p' `seq` Just (b, (p', c, bs, s))
+
+alexInputPrevChar :: AlexInput -> Char
+alexInputPrevChar (p, c, bs, s) = c
+
+-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
+utf8Encode :: Char -> [Word8]
+utf8Encode = map fromIntegral . go . ord
+  where
+  go oc
+   | oc <= 0x7f       = [oc]
+
+   | oc <= 0x7ff      = [ 0xc0 + (oc `Data.Bits.shiftR` 6)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+
+   | oc <= 0xffff     = [ 0xe0 + (oc `Data.Bits.shiftR` 12)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+   | otherwise        = [ 0xf0 + (oc `Data.Bits.shiftR` 18)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
diff --git a/src/Lam/Lex.x b/src/Lam/Lex.x
new file mode 100644
--- /dev/null
+++ b/src/Lam/Lex.x
@@ -0,0 +1,245 @@
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6).
+
+-- Lexer definition for use with Alex 3
+{
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+{-# OPTIONS_GHC -w #-}
+
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lam.Lex where
+
+import Prelude
+
+import qualified Data.Bits
+import Data.Char     (ord)
+import Data.Function (on)
+import Data.Word     (Word8)
+}
+
+-- Predefined character classes
+
+$c = [A-Z\192-\221] # [\215]  -- capital isolatin1 letter (215 = \times) FIXME
+$s = [a-z\222-\255] # [\247]  -- small   isolatin1 letter (247 = \div  ) FIXME
+$l = [$c $s]         -- letter
+$d = [0-9]           -- digit
+$i = [$l $d _ ']     -- identifier character
+$u = [. \n]          -- universal: any character
+
+-- Symbols and non-identifier-like reserved words
+
+@rsyms = \( | \)
+
+:-
+
+-- Whitespace (skipped)
+$white+ ;
+
+-- Symbols
+@rsyms
+    { tok (eitherResIdent TV) }
+
+-- token Lambda
+[\\ λ]
+    { tok (eitherResIdent T_Lambda) }
+
+-- token Arrow
+\→ | \- \>
+    { tok (eitherResIdent T_Arrow) }
+
+-- Keywords and Ident
+$l $i*
+    { tok (eitherResIdent TV) }
+
+{
+-- | Create a token with position.
+tok :: (String -> Tok) -> (Posn -> String -> Token)
+tok f p = PT p . f
+
+-- | Token without position.
+data Tok
+  = TK {-# UNPACK #-} !TokSymbol  -- ^ Reserved word or symbol.
+  | TL !String                    -- ^ String literal.
+  | TI !String                    -- ^ Integer literal.
+  | TV !String                    -- ^ Identifier.
+  | TD !String                    -- ^ Float literal.
+  | TC !String                    -- ^ Character literal.
+  | T_Lambda !String
+  | T_Arrow !String
+  deriving (Eq, Show, Ord)
+
+-- | Smart constructor for 'Tok' for the sake of backwards compatibility.
+pattern TS :: String -> Int -> Tok
+pattern TS t i = TK (TokSymbol t i)
+
+-- | Keyword or symbol tokens have a unique ID.
+data TokSymbol = TokSymbol
+  { tsText :: String
+      -- ^ Keyword or symbol text.
+  , tsID   :: !Int
+      -- ^ Unique ID.
+  } deriving (Show)
+
+-- | Keyword/symbol equality is determined by the unique ID.
+instance Eq  TokSymbol where (==)    = (==)    `on` tsID
+
+-- | Keyword/symbol ordering is determined by the unique ID.
+instance Ord TokSymbol where compare = compare `on` tsID
+
+-- | Token with position.
+data Token
+  = PT  Posn Tok
+  | Err Posn
+  deriving (Eq, Show, Ord)
+
+-- | Pretty print a position.
+printPosn :: Posn -> String
+printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c
+
+-- | Pretty print the position of the first token in the list.
+tokenPos :: [Token] -> String
+tokenPos (t:_) = printPosn (tokenPosn t)
+tokenPos []    = "end of file"
+
+-- | Get the position of a token.
+tokenPosn :: Token -> Posn
+tokenPosn (PT p _) = p
+tokenPosn (Err p)  = p
+
+-- | Get line and column of a token.
+tokenLineCol :: Token -> (Int, Int)
+tokenLineCol = posLineCol . tokenPosn
+
+-- | Get line and column of a position.
+posLineCol :: Posn -> (Int, Int)
+posLineCol (Pn _ l c) = (l,c)
+
+-- | Convert a token into "position token" form.
+mkPosToken :: Token -> ((Int, Int), String)
+mkPosToken t = (tokenLineCol t, tokenText t)
+
+-- | Convert a token to its text.
+tokenText :: Token -> String
+tokenText t = case t of
+  PT _ (TS s _) -> s
+  PT _ (TL s)   -> show s
+  PT _ (TI s)   -> s
+  PT _ (TV s)   -> s
+  PT _ (TD s)   -> s
+  PT _ (TC s)   -> s
+  Err _         -> "#error"
+  PT _ (T_Lambda s) -> s
+  PT _ (T_Arrow s) -> s
+
+-- | Convert a token to a string.
+prToken :: Token -> String
+prToken t = tokenText t
+
+-- | Finite map from text to token organized as binary search tree.
+data BTree
+  = N -- ^ Nil (leaf).
+  | B String Tok BTree BTree
+      -- ^ Binary node.
+  deriving (Show)
+
+-- | Convert potential keyword into token or use fallback conversion.
+eitherResIdent :: (String -> Tok) -> String -> Tok
+eitherResIdent tv s = treeFind resWords
+  where
+  treeFind N = tv s
+  treeFind (B a t left right) =
+    case compare s a of
+      LT -> treeFind left
+      GT -> treeFind right
+      EQ -> t
+
+-- | The keywords and symbols of the language organized as binary search tree.
+resWords :: BTree
+resWords = b ")" 2 (b "(" 1 N N) N
+  where
+  b s n = B bs (TS bs n)
+    where
+    bs = s
+
+-- | Unquote string literal.
+unescapeInitTail :: String -> String
+unescapeInitTail = id . unesc . tail . id
+  where
+  unesc s = case s of
+    '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs
+    '\\':'n':cs  -> '\n' : unesc cs
+    '\\':'t':cs  -> '\t' : unesc cs
+    '\\':'r':cs  -> '\r' : unesc cs
+    '\\':'f':cs  -> '\f' : unesc cs
+    '"':[]       -> []
+    c:cs         -> c : unesc cs
+    _            -> []
+
+-------------------------------------------------------------------
+-- Alex wrapper code.
+-- A modified "posn" wrapper.
+-------------------------------------------------------------------
+
+data Posn = Pn !Int !Int !Int
+  deriving (Eq, Show, Ord)
+
+alexStartPos :: Posn
+alexStartPos = Pn 0 1 1
+
+alexMove :: Posn -> Char -> Posn
+alexMove (Pn a l c) '\t' = Pn (a+1)  l     (((c+7) `div` 8)*8+1)
+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1)   1
+alexMove (Pn a l c) _    = Pn (a+1)  l     (c+1)
+
+type Byte = Word8
+
+type AlexInput = (Posn,     -- current position,
+                  Char,     -- previous char
+                  [Byte],   -- pending bytes on the current char
+                  String)   -- current input string
+
+tokens :: String -> [Token]
+tokens str = go (alexStartPos, '\n', [], str)
+    where
+      go :: AlexInput -> [Token]
+      go inp@(pos, _, _, str) =
+               case alexScan inp 0 of
+                AlexEOF                   -> []
+                AlexError (pos, _, _, _)  -> [Err pos]
+                AlexSkip  inp' len        -> go inp'
+                AlexToken inp' len act    -> act pos (take len str) : (go inp')
+
+alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)
+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))
+alexGetByte (p, _, [], s) =
+  case s of
+    []  -> Nothing
+    (c:s) ->
+             let p'     = alexMove p c
+                 (b:bs) = utf8Encode c
+              in p' `seq` Just (b, (p', c, bs, s))
+
+alexInputPrevChar :: AlexInput -> Char
+alexInputPrevChar (p, c, bs, s) = c
+
+-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
+utf8Encode :: Char -> [Word8]
+utf8Encode = map fromIntegral . go . ord
+  where
+  go oc
+   | oc <= 0x7f       = [oc]
+
+   | oc <= 0x7ff      = [ 0xc0 + (oc `Data.Bits.shiftR` 6)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+
+   | oc <= 0xffff     = [ 0xe0 + (oc `Data.Bits.shiftR` 12)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+   | otherwise        = [ 0xf0 + (oc `Data.Bits.shiftR` 18)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+}
diff --git a/src/Lam/Par.hs b/src/Lam/Par.hs
new file mode 100644
--- /dev/null
+++ b/src/Lam/Par.hs
@@ -0,0 +1,851 @@
+{-# OPTIONS_GHC -w #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE NoStrictData #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE PartialTypeSignatures #-}
+#endif
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lam.Par
+  ( happyError
+  , myLexer
+  , pExp
+  ) where
+
+import Prelude
+
+import qualified Lam.Abs
+import Lam.Lex
+import qualified Data.Function as Happy_Prelude
+import qualified Data.Bool as Happy_Prelude
+import qualified Data.Function as Happy_Prelude
+import qualified Data.Maybe as Happy_Prelude
+import qualified Data.Int as Happy_Prelude
+import qualified Data.String as Happy_Prelude
+import qualified Data.List as Happy_Prelude
+import qualified Control.Monad as Happy_Prelude
+import qualified Text.Show as Happy_Prelude
+import qualified GHC.Num as Happy_Prelude
+import qualified GHC.Err as Happy_Prelude
+import qualified Data.Array as Happy_Data_Array
+import qualified Data.Bits as Bits
+import qualified GHC.Exts as Happy_GHC_Exts
+import Control.Applicative(Applicative(..))
+import Control.Monad (ap)
+
+-- parser produced by Happy Version 2.1.2
+
+newtype HappyAbsSyn  = HappyAbsSyn HappyAny
+#if __GLASGOW_HASKELL__ >= 607
+type HappyAny = Happy_GHC_Exts.Any
+#else
+type HappyAny = forall a . a
+#endif
+newtype HappyWrap5 = HappyWrap5 (Lam.Abs.Ident)
+happyIn5 :: (Lam.Abs.Ident) -> (HappyAbsSyn )
+happyIn5 x = Happy_GHC_Exts.unsafeCoerce# (HappyWrap5 x)
+{-# INLINE happyIn5 #-}
+happyOut5 :: (HappyAbsSyn ) -> HappyWrap5
+happyOut5 x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyOut5 #-}
+newtype HappyWrap6 = HappyWrap6 (Lam.Abs.Lambda)
+happyIn6 :: (Lam.Abs.Lambda) -> (HappyAbsSyn )
+happyIn6 x = Happy_GHC_Exts.unsafeCoerce# (HappyWrap6 x)
+{-# INLINE happyIn6 #-}
+happyOut6 :: (HappyAbsSyn ) -> HappyWrap6
+happyOut6 x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyOut6 #-}
+newtype HappyWrap7 = HappyWrap7 (Lam.Abs.Arrow)
+happyIn7 :: (Lam.Abs.Arrow) -> (HappyAbsSyn )
+happyIn7 x = Happy_GHC_Exts.unsafeCoerce# (HappyWrap7 x)
+{-# INLINE happyIn7 #-}
+happyOut7 :: (HappyAbsSyn ) -> HappyWrap7
+happyOut7 x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyOut7 #-}
+newtype HappyWrap8 = HappyWrap8 (Lam.Abs.Exp)
+happyIn8 :: (Lam.Abs.Exp) -> (HappyAbsSyn )
+happyIn8 x = Happy_GHC_Exts.unsafeCoerce# (HappyWrap8 x)
+{-# INLINE happyIn8 #-}
+happyOut8 :: (HappyAbsSyn ) -> HappyWrap8
+happyOut8 x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyOut8 #-}
+newtype HappyWrap9 = HappyWrap9 (Lam.Abs.Exp)
+happyIn9 :: (Lam.Abs.Exp) -> (HappyAbsSyn )
+happyIn9 x = Happy_GHC_Exts.unsafeCoerce# (HappyWrap9 x)
+{-# INLINE happyIn9 #-}
+happyOut9 :: (HappyAbsSyn ) -> HappyWrap9
+happyOut9 x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyOut9 #-}
+newtype HappyWrap10 = HappyWrap10 (Lam.Abs.Exp)
+happyIn10 :: (Lam.Abs.Exp) -> (HappyAbsSyn )
+happyIn10 x = Happy_GHC_Exts.unsafeCoerce# (HappyWrap10 x)
+{-# INLINE happyIn10 #-}
+happyOut10 :: (HappyAbsSyn ) -> HappyWrap10
+happyOut10 x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyOut10 #-}
+newtype HappyWrap11 = HappyWrap11 (Lam.Abs.Exp)
+happyIn11 :: (Lam.Abs.Exp) -> (HappyAbsSyn )
+happyIn11 x = Happy_GHC_Exts.unsafeCoerce# (HappyWrap11 x)
+{-# INLINE happyIn11 #-}
+happyOut11 :: (HappyAbsSyn ) -> HappyWrap11
+happyOut11 x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyOut11 #-}
+newtype HappyWrap12 = HappyWrap12 (Lam.Abs.Ty)
+happyIn12 :: (Lam.Abs.Ty) -> (HappyAbsSyn )
+happyIn12 x = Happy_GHC_Exts.unsafeCoerce# (HappyWrap12 x)
+{-# INLINE happyIn12 #-}
+happyOut12 :: (HappyAbsSyn ) -> HappyWrap12
+happyOut12 x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyOut12 #-}
+newtype HappyWrap13 = HappyWrap13 (Lam.Abs.Ty)
+happyIn13 :: (Lam.Abs.Ty) -> (HappyAbsSyn )
+happyIn13 x = Happy_GHC_Exts.unsafeCoerce# (HappyWrap13 x)
+{-# INLINE happyIn13 #-}
+happyOut13 :: (HappyAbsSyn ) -> HappyWrap13
+happyOut13 x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyOut13 #-}
+happyInTok :: (Token) -> (HappyAbsSyn )
+happyInTok x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyInTok #-}
+happyOutTok :: (HappyAbsSyn ) -> (Token)
+happyOutTok x = Happy_GHC_Exts.unsafeCoerce# x
+{-# INLINE happyOutTok #-}
+
+
+{-# NOINLINE happyTokenStrings #-}
+happyTokenStrings = ["'('","')'","L_Ident","L_Lambda","L_Arrow","%eof"]
+
+happyActOffsets :: HappyAddr
+happyActOffsets = HappyA# "\x14\x00\x00\x00\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\x00\x00\x00\x00\x19\x00\x00\x00\x03\x00\x00\x00\x00\x00\x00\x00\x14\x00\x00\x00\x00\x00\x00\x00\x0e\x00\x00\x00\x00\x00\x00\x00\x16\x00\x00\x00\x14\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#
+
+happyGotoOffsets :: HappyAddr
+happyGotoOffsets = HappyA# "\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x1e\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x1d\x00\x00\x00\x0f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#
+
+happyDefActions :: HappyAddr
+happyDefActions = HappyA# "\x00\x00\x00\x00\x00\x00\x00\x00\xfe\xff\xff\xff\xfb\xff\xff\xff\x00\x00\x00\x00\xf8\xff\xff\xff\xf5\xff\xff\xff\x00\x00\x00\x00\xf6\xff\xff\xff\x00\x00\x00\x00\xfd\xff\xff\xff\x00\x00\x00\x00\xf9\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\xfc\xff\xff\xff\xfa\xff\xff\xff\xf7\xff\xff\xff"#
+
+happyCheck :: HappyAddr
+happyCheck = HappyA# "\xff\xff\xff\xff\x00\x00\x00\x00\x01\x00\x00\x00\x04\x00\x00\x00\x03\x00\x00\x00\x04\x00\x00\x00\x05\x00\x00\x00\x06\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x07\x00\x00\x00\x03\x00\x00\x00\x04\x00\x00\x00\x05\x00\x00\x00\x06\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x03\x00\x00\x00\x03\x00\x00\x00\x04\x00\x00\x00\x05\x00\x00\x00\x06\x00\x00\x00\x02\x00\x00\x00\x00\x00\x00\x00\x04\x00\x00\x00\x05\x00\x00\x00\x03\x00\x00\x00\x02\x00\x00\x00\x06\x00\x00\x00\x04\x00\x00\x00\x00\x00\x00\x00\x02\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#
+
+happyTable :: HappyAddr
+happyTable = HappyA# "\x00\x00\x00\x00\x03\x00\x00\x00\x04\x00\x00\x00\x03\x00\x00\x00\x05\x00\x00\x00\x06\x00\x00\x00\x07\x00\x00\x00\x08\x00\x00\x00\x03\x00\x00\x00\x04\x00\x00\x00\xff\xff\xff\xff\x05\x00\x00\x00\x06\x00\x00\x00\x0b\x00\x00\x00\x08\x00\x00\x00\x03\x00\x00\x00\x04\x00\x00\x00\x11\x00\x00\x00\x05\x00\x00\x00\x06\x00\x00\x00\x11\x00\x00\x00\x08\x00\x00\x00\x0a\x00\x00\x00\x03\x00\x00\x00\x03\x00\x00\x00\x0b\x00\x00\x00\x0c\x00\x00\x00\x0a\x00\x00\x00\x10\x00\x00\x00\x03\x00\x00\x00\x0d\x00\x00\x00\x0e\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#
+
+happyReduceArr = Happy_Data_Array.array (1, 14) [
+        (1 , happyReduce_1),
+        (2 , happyReduce_2),
+        (3 , happyReduce_3),
+        (4 , happyReduce_4),
+        (5 , happyReduce_5),
+        (6 , happyReduce_6),
+        (7 , happyReduce_7),
+        (8 , happyReduce_8),
+        (9 , happyReduce_9),
+        (10 , happyReduce_10),
+        (11 , happyReduce_11),
+        (12 , happyReduce_12),
+        (13 , happyReduce_13),
+        (14 , happyReduce_14)
+        ]
+
+happyRuleArr :: HappyAddr
+happyRuleArr = HappyA# "\x00\x00\x00\x00\x01\x00\x00\x00\x01\x00\x00\x00\x01\x00\x00\x00\x02\x00\x00\x00\x01\x00\x00\x00\x03\x00\x00\x00\x01\x00\x00\x00\x03\x00\x00\x00\x03\x00\x00\x00\x04\x00\x00\x00\x02\x00\x00\x00\x04\x00\x00\x00\x01\x00\x00\x00\x05\x00\x00\x00\x04\x00\x00\x00\x05\x00\x00\x00\x01\x00\x00\x00\x06\x00\x00\x00\x01\x00\x00\x00\x07\x00\x00\x00\x01\x00\x00\x00\x07\x00\x00\x00\x03\x00\x00\x00\x08\x00\x00\x00\x03\x00\x00\x00\x08\x00\x00\x00\x01\x00\x00\x00"#
+
+happyCatchStates :: [Happy_Prelude.Int]
+happyCatchStates = []
+
+happy_n_terms = 8 :: Happy_Prelude.Int
+happy_n_nonterms = 9 :: Happy_Prelude.Int
+
+happy_n_starts = 1 :: Happy_Prelude.Int
+
+happyReduce_1 = happySpecReduce_1  0# happyReduction_1
+happyReduction_1 happy_x_1
+         =  case happyOutTok happy_x_1 of { (PT _ (TV happy_var_1)) -> 
+        happyIn5
+                 (Lam.Abs.Ident happy_var_1
+        )}
+
+happyReduce_2 = happySpecReduce_1  1# happyReduction_2
+happyReduction_2 happy_x_1
+         =  case happyOutTok happy_x_1 of { (PT _ (T_Lambda happy_var_1)) -> 
+        happyIn6
+                 (Lam.Abs.Lambda happy_var_1
+        )}
+
+happyReduce_3 = happySpecReduce_1  2# happyReduction_3
+happyReduction_3 happy_x_1
+         =  case happyOutTok happy_x_1 of { (PT _ (T_Arrow happy_var_1)) -> 
+        happyIn7
+                 (Lam.Abs.Arrow happy_var_1
+        )}
+
+happyReduce_4 = happySpecReduce_1  3# happyReduction_4
+happyReduction_4 happy_x_1
+         =  case happyOut5 happy_x_1 of { (HappyWrap5 happy_var_1) -> 
+        happyIn8
+                 (Lam.Abs.EId happy_var_1
+        )}
+
+happyReduce_5 = happySpecReduce_3  3# happyReduction_5
+happyReduction_5 happy_x_3
+        happy_x_2
+        happy_x_1
+         =  case happyOut10 happy_x_2 of { (HappyWrap10 happy_var_2) -> 
+        happyIn8
+                 (happy_var_2
+        )}
+
+happyReduce_6 = happySpecReduce_2  4# happyReduction_6
+happyReduction_6 happy_x_2
+        happy_x_1
+         =  case happyOut9 happy_x_1 of { (HappyWrap9 happy_var_1) -> 
+        case happyOut8 happy_x_2 of { (HappyWrap8 happy_var_2) -> 
+        happyIn9
+                 (Lam.Abs.EApp happy_var_1 happy_var_2
+        )}}
+
+happyReduce_7 = happySpecReduce_1  4# happyReduction_7
+happyReduction_7 happy_x_1
+         =  case happyOut8 happy_x_1 of { (HappyWrap8 happy_var_1) -> 
+        happyIn9
+                 (happy_var_1
+        )}
+
+happyReduce_8 = happyReduce 4# 5# happyReduction_8
+happyReduction_8 (happy_x_4 `HappyStk`
+        happy_x_3 `HappyStk`
+        happy_x_2 `HappyStk`
+        happy_x_1 `HappyStk`
+        happyRest)
+         = case happyOut6 happy_x_1 of { (HappyWrap6 happy_var_1) -> 
+        case happyOut5 happy_x_2 of { (HappyWrap5 happy_var_2) -> 
+        case happyOut7 happy_x_3 of { (HappyWrap7 happy_var_3) -> 
+        case happyOut10 happy_x_4 of { (HappyWrap10 happy_var_4) -> 
+        happyIn10
+                 (Lam.Abs.EAbs happy_var_1 happy_var_2 happy_var_3 happy_var_4
+        ) `HappyStk` happyRest}}}}
+
+happyReduce_9 = happySpecReduce_1  5# happyReduction_9
+happyReduction_9 happy_x_1
+         =  case happyOut11 happy_x_1 of { (HappyWrap11 happy_var_1) -> 
+        happyIn10
+                 (happy_var_1
+        )}
+
+happyReduce_10 = happySpecReduce_1  6# happyReduction_10
+happyReduction_10 happy_x_1
+         =  case happyOut9 happy_x_1 of { (HappyWrap9 happy_var_1) -> 
+        happyIn11
+                 (happy_var_1
+        )}
+
+happyReduce_11 = happySpecReduce_1  7# happyReduction_11
+happyReduction_11 happy_x_1
+         =  case happyOut5 happy_x_1 of { (HappyWrap5 happy_var_1) -> 
+        happyIn12
+                 (Lam.Abs.TId happy_var_1
+        )}
+
+happyReduce_12 = happySpecReduce_3  7# happyReduction_12
+happyReduction_12 happy_x_3
+        happy_x_2
+        happy_x_1
+         =  case happyOut13 happy_x_2 of { (HappyWrap13 happy_var_2) -> 
+        happyIn12
+                 (happy_var_2
+        )}
+
+happyReduce_13 = happySpecReduce_3  8# happyReduction_13
+happyReduction_13 happy_x_3
+        happy_x_2
+        happy_x_1
+         =  case happyOut12 happy_x_1 of { (HappyWrap12 happy_var_1) -> 
+        case happyOut7 happy_x_2 of { (HappyWrap7 happy_var_2) -> 
+        case happyOut13 happy_x_3 of { (HappyWrap13 happy_var_3) -> 
+        happyIn13
+                 (Lam.Abs.TArr happy_var_1 happy_var_2 happy_var_3
+        )}}}
+
+happyReduce_14 = happySpecReduce_1  8# happyReduction_14
+happyReduction_14 happy_x_1
+         =  case happyOut12 happy_x_1 of { (HappyWrap12 happy_var_1) -> 
+        happyIn13
+                 (happy_var_1
+        )}
+
+happyTerminalToTok term = case term of {
+        PT _ (TS _ 1) -> 2#;
+        PT _ (TS _ 2) -> 3#;
+        PT _ (TV happy_dollar_dollar) -> 4#;
+        PT _ (T_Lambda happy_dollar_dollar) -> 5#;
+        PT _ (T_Arrow happy_dollar_dollar) -> 6#;
+        _ -> -1#;
+        }
+{-# NOINLINE happyTerminalToTok #-}
+
+happyLex kend  _kmore []       = kend notHappyAtAll []
+happyLex _kend kmore  (tk:tks) = kmore (happyTerminalToTok tk) tk tks
+{-# INLINE happyLex #-}
+
+happyNewToken action sts stk = happyLex (\tk -> happyDoAction 7# notHappyAtAll action sts stk) (\i tk -> happyDoAction i tk action sts stk)
+
+happyReport 7# tk explist resume tks = happyReport' tks explist resume
+happyReport _ tk explist resume tks = happyReport' (tk:tks) explist (\tks -> resume (Happy_Prelude.tail tks))
+
+
+happyThen :: () => (Err a) -> (a -> (Err b)) -> (Err b)
+happyThen = ((>>=))
+happyReturn :: () => a -> (Err a)
+happyReturn = (return)
+happyThen1 m k tks = ((>>=)) m (\a -> k a tks)
+happyFmap1 f m tks = happyThen (m tks) (\a -> happyReturn (f a))
+happyReturn1 :: () => a -> b -> (Err a)
+happyReturn1 = \a tks -> (return) a
+happyReport' :: () => [(Token)] -> [Happy_Prelude.String] -> ([(Token)] -> (Err a)) -> (Err a)
+happyReport' = (\tokens expected resume -> happyError tokens)
+
+happyAbort :: () => [(Token)] -> (Err a)
+happyAbort = Happy_Prelude.error "Called abort handler in non-resumptive parser"
+
+pExp tks = happySomeParser where
+ happySomeParser = happyThen (happyParse 0# tks) (\x -> happyReturn (let {(HappyWrap10 x') = happyOut10 x} in x'))
+
+happySeq = happyDontSeq
+
+
+type Err = Either String
+
+happyError :: [Token] -> Err a
+happyError ts = Left $
+  "syntax error at " ++ tokenPos ts ++
+  case ts of
+    []      -> []
+    [Err _] -> " due to lexer error"
+    t:_     -> " before `" ++ (prToken t) ++ "'"
+
+myLexer :: String -> [Token]
+myLexer = tokens
+#define HAPPY_COERCE 1
+-- $Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp $
+
+#if !defined(__GLASGOW_HASKELL__)
+#  error This code isn't being built with GHC.
+#endif
+
+-- Get WORDS_BIGENDIAN (if defined)
+#include "MachDeps.h"
+
+-- Do not remove this comment. Required to fix CPP parsing when using GCC and a clang-compiled alex.
+#define LT(n,m) ((Happy_GHC_Exts.tagToEnum# (n Happy_GHC_Exts.<# m)) :: Happy_Prelude.Bool)
+#define GTE(n,m) ((Happy_GHC_Exts.tagToEnum# (n Happy_GHC_Exts.>=# m)) :: Happy_Prelude.Bool)
+#define EQ(n,m) ((Happy_GHC_Exts.tagToEnum# (n Happy_GHC_Exts.==# m)) :: Happy_Prelude.Bool)
+#define PLUS(n,m) (n Happy_GHC_Exts.+# m)
+#define MINUS(n,m) (n Happy_GHC_Exts.-# m)
+#define TIMES(n,m) (n Happy_GHC_Exts.*# m)
+#define NEGATE(n) (Happy_GHC_Exts.negateInt# (n))
+
+type Happy_Int = Happy_GHC_Exts.Int#
+data Happy_IntList = HappyCons Happy_Int Happy_IntList
+
+#define INVALID_TOK -1#
+#define ERROR_TOK 0#
+#define CATCH_TOK 1#
+
+#if defined(HAPPY_COERCE)
+#  define GET_ERROR_TOKEN(x)  (case Happy_GHC_Exts.unsafeCoerce# x of { (Happy_GHC_Exts.I# i) -> i })
+#  define MK_ERROR_TOKEN(i)   (Happy_GHC_Exts.unsafeCoerce# (Happy_GHC_Exts.I# i))
+#  define MK_TOKEN(x)         (happyInTok (x))
+#else
+#  define GET_ERROR_TOKEN(x)  (case x of { HappyErrorToken (Happy_GHC_Exts.I# i) -> i })
+#  define MK_ERROR_TOKEN(i)   (HappyErrorToken (Happy_GHC_Exts.I# i))
+#  define MK_TOKEN(x)         (HappyTerminal (x))
+#endif
+
+#if defined(HAPPY_DEBUG)
+#  define DEBUG_TRACE(s)    (happyTrace (s)) Happy_Prelude.$
+happyTrace string expr = Happy_System_IO_Unsafe.unsafePerformIO Happy_Prelude.$ do
+    Happy_System_IO.hPutStr Happy_System_IO.stderr string
+    Happy_Prelude.return expr
+#else
+#  define DEBUG_TRACE(s)    {- nothing -}
+#endif
+
+infixr 9 `HappyStk`
+data HappyStk a = HappyStk a (HappyStk a)
+
+-----------------------------------------------------------------------------
+-- starting the parse
+
+happyParse start_state = happyNewToken start_state notHappyAtAll notHappyAtAll
+
+-----------------------------------------------------------------------------
+-- Accepting the parse
+
+-- If the current token is ERROR_TOK, it means we've just accepted a partial
+-- parse (a %partial parser).  We must ignore the saved token on the top of
+-- the stack in this case.
+happyAccept ERROR_TOK tk st sts (_ `HappyStk` ans `HappyStk` _) =
+        happyReturn1 ans
+happyAccept j tk st sts (HappyStk ans _) =
+        (happyTcHack j (happyTcHack st)) (happyReturn1 ans)
+
+-----------------------------------------------------------------------------
+-- Arrays only: do the next action
+
+happyDoAction i tk st =
+  DEBUG_TRACE("state: " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# st) Happy_Prelude.++
+              ",\ttoken: " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# i) Happy_Prelude.++
+              ",\taction: ")
+  case happyDecodeAction (happyNextAction i st) of
+    HappyFail             -> DEBUG_TRACE("failing.\n")
+                             happyFail i tk st
+    HappyAccept           -> DEBUG_TRACE("accept.\n")
+                             happyAccept i tk st
+    HappyReduce rule      -> DEBUG_TRACE("reduce (rule " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# rule) Happy_Prelude.++ ")")
+                             (happyReduceArr Happy_Data_Array.! (Happy_GHC_Exts.I# rule)) i tk st
+    HappyShift  new_state -> DEBUG_TRACE("shift, enter state " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# new_state) Happy_Prelude.++ "\n")
+                             happyShift new_state i tk st
+
+{-# INLINE happyNextAction #-}
+happyNextAction i st = case happyIndexActionTable i st of
+  Happy_Prelude.Just (Happy_GHC_Exts.I# act) -> act
+  Happy_Prelude.Nothing                      -> happyIndexOffAddr happyDefActions st
+
+{-# INLINE happyIndexActionTable #-}
+happyIndexActionTable i st
+  | GTE(i, 0#), GTE(off, 0#), EQ(happyIndexOffAddr happyCheck off, i)
+  -- i >= 0:   Guard against INVALID_TOK (do the default action, which ultimately errors)
+  -- off >= 0: Otherwise it's a default action
+  -- equality check: Ensure that the entry in the compressed array is owned by st
+  = Happy_Prelude.Just (Happy_GHC_Exts.I# (happyIndexOffAddr happyTable off))
+  | Happy_Prelude.otherwise
+  = Happy_Prelude.Nothing
+  where
+    off = PLUS(happyIndexOffAddr happyActOffsets st, i)
+
+data HappyAction
+  = HappyFail
+  | HappyAccept
+  | HappyReduce Happy_Int -- rule number
+  | HappyShift Happy_Int  -- new state
+  deriving Happy_Prelude.Show
+
+{-# INLINE happyDecodeAction #-}
+happyDecodeAction :: Happy_Int -> HappyAction
+happyDecodeAction  0#                        = HappyFail
+happyDecodeAction -1#                        = HappyAccept
+happyDecodeAction action | LT(action, 0#)    = HappyReduce NEGATE(PLUS(action, 1#))
+                         | Happy_Prelude.otherwise = HappyShift MINUS(action, 1#)
+
+{-# INLINE happyIndexGotoTable #-}
+happyIndexGotoTable nt st = happyIndexOffAddr happyTable off
+  where
+    off = PLUS(happyIndexOffAddr happyGotoOffsets st, nt)
+
+{-# INLINE happyIndexOffAddr #-}
+happyIndexOffAddr :: HappyAddr -> Happy_Int -> Happy_Int
+happyIndexOffAddr (HappyA# arr) off =
+#if __GLASGOW_HASKELL__ >= 901
+  Happy_GHC_Exts.int32ToInt# -- qualified import because it doesn't exist on older GHC's
+#endif
+#ifdef WORDS_BIGENDIAN
+  -- The CI of `alex` tests this code path
+  (Happy_GHC_Exts.word32ToInt32# (Happy_GHC_Exts.wordToWord32# (Happy_GHC_Exts.byteSwap32# (Happy_GHC_Exts.word32ToWord# (Happy_GHC_Exts.int32ToWord32#
+#endif
+  (Happy_GHC_Exts.indexInt32OffAddr# arr off)
+#ifdef WORDS_BIGENDIAN
+  )))))
+#endif
+
+happyIndexRuleArr :: Happy_Int -> (# Happy_Int, Happy_Int #)
+happyIndexRuleArr r = (# nt, len #)
+  where
+    !(Happy_GHC_Exts.I# n_starts) = happy_n_starts
+    offs = TIMES(MINUS(r,n_starts),2#)
+    nt = happyIndexOffAddr happyRuleArr offs
+    len = happyIndexOffAddr happyRuleArr PLUS(offs,1#)
+
+data HappyAddr = HappyA# Happy_GHC_Exts.Addr#
+
+-----------------------------------------------------------------------------
+-- Shifting a token
+
+happyShift new_state ERROR_TOK tk st sts stk@(x `HappyStk` _) =
+     -- See "Error Fixup" below
+     let i = GET_ERROR_TOKEN(x) in
+     DEBUG_TRACE("shifting the error token")
+     happyDoAction i tk new_state (HappyCons st sts) stk
+
+happyShift new_state i tk st sts stk =
+     happyNewToken new_state (HappyCons st sts) (MK_TOKEN(tk) `HappyStk` stk)
+
+-- happyReduce is specialised for the common cases.
+
+happySpecReduce_0 nt fn j tk st sts stk
+     = happySeq fn (happyGoto nt j tk st (HappyCons st sts) (fn `HappyStk` stk))
+
+happySpecReduce_1 nt fn j tk old_st sts@(HappyCons st _) (v1 `HappyStk` stk')
+     = let r = fn v1 in
+       happyTcHack old_st (happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk')))
+
+happySpecReduce_2 nt fn j tk old_st
+  (HappyCons _ sts@(HappyCons st _))
+  (v1 `HappyStk` v2 `HappyStk` stk')
+     = let r = fn v1 v2 in
+       happyTcHack old_st (happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk')))
+
+happySpecReduce_3 nt fn j tk old_st
+  (HappyCons _ (HappyCons _ sts@(HappyCons st _)))
+  (v1 `HappyStk` v2 `HappyStk` v3 `HappyStk` stk')
+     = let r = fn v1 v2 v3 in
+       happyTcHack old_st (happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk')))
+
+happyReduce k nt fn j tk st sts stk
+     = case happyDrop MINUS(k,(1# :: Happy_Int)) sts of
+         sts1@(HappyCons st1 _) ->
+                let r = fn stk in -- it doesn't hurt to always seq here...
+                st `happyTcHack` happyDoSeq r (happyGoto nt j tk st1 sts1 r)
+
+happyMonadReduce k nt fn j tk st sts stk =
+      case happyDrop k (HappyCons st sts) of
+        sts1@(HappyCons st1 _) ->
+          let drop_stk = happyDropStk k stk in
+          j `happyTcHack` happyThen1 (fn stk tk)
+                                     (\r -> happyGoto nt j tk st1 sts1 (r `HappyStk` drop_stk))
+
+happyMonad2Reduce k nt fn j tk st sts stk =
+      case happyDrop k (HappyCons st sts) of
+        sts1@(HappyCons st1 _) ->
+          let drop_stk = happyDropStk k stk
+              off = happyIndexOffAddr happyGotoOffsets st1
+              off_i = PLUS(off, nt)
+              new_state = happyIndexOffAddr happyTable off_i
+          in
+            j `happyTcHack` happyThen1 (fn stk tk)
+                                       (\r -> happyNewToken new_state sts1 (r `HappyStk` drop_stk))
+
+happyDrop 0# l               = l
+happyDrop n  (HappyCons _ t) = happyDrop MINUS(n,(1# :: Happy_Int)) t
+
+happyDropStk 0# l                 = l
+happyDropStk n  (x `HappyStk` xs) = happyDropStk MINUS(n,(1#::Happy_Int)) xs
+
+-----------------------------------------------------------------------------
+-- Moving to a new state after a reduction
+
+happyGoto nt j tk st =
+   DEBUG_TRACE(", goto state " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# new_state) Happy_Prelude.++ "\n")
+   happyDoAction j tk new_state
+  where new_state = happyIndexGotoTable nt st
+
+{- Note [Error recovery]
+~~~~~~~~~~~~~~~~~~~~~~~~
+When there is no applicable action for the current lookahead token `tk`,
+happy enters error recovery mode. Depending on whether the grammar file
+declares the two action form `%error { abort } { report }` for
+    Resumptive Error Handling,
+it works in one (not resumptive) or two phases (resumptive):
+
+ 1. Fixup mode:
+    Try to see if there is an action for the error token ERROR_TOK. If there
+    is, do *not* emit an error and pretend instead that an `error` token was
+    inserted.
+    When there is no ERROR_TOK action, report an error.
+
+    In non-resumptive error handling, calling the single error handler
+    (e.g. `happyError`) will throw an exception and abort the parser.
+    However, in resumptive error handling we enter *error resumption mode*.
+
+ 2. Error resumption mode:
+    After reporting the error (with `report`), happy will attempt to find
+    a good state stack to resume parsing in.
+    For each candidate stack, it discards input until one of the candidates
+    resumes (i.e. shifts the current input).
+    If no candidate resumes before the end of input, resumption failed and
+    calls the `abort` function, to much the same effect as in non-resumptive
+    error handling.
+
+    Candidate stacks are declared by the grammar author using the special
+    `catch` terminal and called "catch frames".
+    This mechanism is described in detail in Note [happyResume].
+
+The `catch` resumption mechanism (2) is what usually is associated with
+`error` in `bison` or `menhir`. Since `error` is used for the Fixup mechanism
+(1) above, we call the corresponding token `catch`.
+Furthermore, in constrast to `bison`, our implementation of `catch`
+non-deterministically considers multiple catch frames on the stack for
+resumption (See Note [Multiple catch frames]).
+
+Note [happyResume]
+~~~~~~~~~~~~~~~~~~
+`happyResume` implements the resumption mechanism from Note [Error recovery].
+It is best understood by example. Consider
+
+Exp :: { String }
+Exp : '1'                { "1" }
+    | catch              { "catch" }
+    | Exp '+' Exp %shift { $1 Happy_Prelude.++ " + " Happy_Prelude.++ $3 } -- %shift: associate 1 + 1 + 1 to the right
+    | '(' Exp ')'        { "(" Happy_Prelude.++ $2 Happy_Prelude.++ ")" }
+
+The idea of the use of `catch` here is that upon encountering a parse error
+during expression parsing, we can gracefully degrade using the `catch` rule,
+still producing a partial syntax tree and keep on parsing to find further
+syntax errors.
+
+Let's trace the parser state for input 11+1, which will error out after shifting 1.
+After shifting, we have the following item stack (growing downwards and omitting
+transitive closure items):
+
+  State 0: %start_parseExp -> . Exp
+  State 5: Exp -> '1' .
+
+(Stack as a list of state numbers: [5,0].)
+As Note [Error recovery] describes, we will first try Fixup mode.
+That fails because no production can shift the `error` token.
+Next we try Error resumption mode. This works as follows:
+
+  1. Pop off the item stack until we find an item that can shift the `catch`
+     token. (Implemented in `pop_items`.)
+       * State 5 cannot shift catch. Pop.
+       * State 0 can shift catch, which would transition into
+          State 4: Exp -> catch .
+     So record the *stack* `[4,0]` after doing the shift transition.
+     We call this a *catch frame*, where the top is a *catch state*,
+     corresponding to an item in which we just shifted a `catch` token.
+     There can be multiple such catch stacks, see Note [Multiple catch frames].
+
+  2. Discard tokens from the input until the lookahead can be shifted in one
+     of the catch stacks. (Implemented in `discard_input_until_exp` and
+     `some_catch_state_shifts`.)
+       * We cannot shift the current lookahead '1' in state 4, so we discard
+       * We *can* shift the next lookahead '+' in state 4, but only after
+         reducing, which pops State 4 and goes to State 3:
+           State 3: %start_parseExp -> Exp .
+                    Exp -> Exp . '+' Exp
+         Here we can shift '+'.
+     As you can see, to implement this machinery we need to simulate
+     the operation of the LALR automaton, especially reduction
+     (`happySimulateReduce`).
+
+Note [Multiple catch frames]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For fewer spurious error messages, it can be beneficial to trace multiple catch
+items. Consider
+
+Exp : '1'
+    | catch
+    | Exp '+' Exp %shift
+    | '(' Exp ')'
+
+Let's trace the parser state for input (;+1, which will error out after shifting (.
+After shifting, we have the following item stack (growing downwards):
+
+  State 0: %start_parseExp -> . Exp
+  State 6: Exp -> '(' . Exp ')'
+
+Upon error, we want to find items in the stack which can shift a catch token.
+Note that both State 0 and State 6 can shift a catch token, transitioning into
+  State 4: Exp -> catch .
+Hence we record the catch frames `[4,6,0]` and `[4,0]` for possible resumption.
+
+Which catch frame do we pick for resumption?
+Note that resuming catch frame `[4,0]` will parse as "catch+1", whereas
+resuming the innermost frame `[4,6,0]` corresponds to parsing "(catch+1".
+The latter would keep discarding input until the closing ')' is found.
+So we will discard + and 1, leading to a spurious syntax error at the end of
+input, aborting the parse and never producing a partial syntax tree. Bad!
+
+It is far preferable to resume with catch frame `[4,0]`, where we can resume
+successfully on input +, so that is what we do.
+
+In general, we pick the catch frame for resumption that discards the least
+amount of input for a successful shift, preferring the topmost such catch frame.
+-}
+
+-- happyFail :: Happy_Int -> Token -> Happy_Int -> _
+-- This function triggers Note [Error recovery].
+-- If the current token is ERROR_TOK, phase (1) has failed and we might try
+-- phase (2).
+happyFail ERROR_TOK = happyFixupFailed
+happyFail i         = happyTryFixup i
+
+-- Enter Error Fixup (see Note [Error recovery]):
+-- generate an error token, save the old token and carry on.
+-- When a `happyShift` accepts the error token, we will pop off the error token
+-- to resume parsing with the current lookahead `i`.
+happyTryFixup i tk action sts stk =
+  DEBUG_TRACE("entering `error` fixup.\n")
+  happyDoAction ERROR_TOK tk action sts (MK_ERROR_TOKEN(i) `HappyStk` stk)
+  -- NB: `happyShift` will simply pop the error token and carry on with
+  --     `tk`. Hence we don't change `tk` in the call here
+
+-- See Note [Error recovery], phase (2).
+-- Enter resumption mode after reporting the error by calling `happyResume`.
+happyFixupFailed tk st sts (x `HappyStk` stk) =
+  let i = GET_ERROR_TOKEN(x) in
+  DEBUG_TRACE("`error` fixup failed.\n")
+  let resume   = happyResume i tk st sts stk
+      expected = happyExpectedTokens st sts in
+  happyReport i tk expected resume
+
+-- happyResume :: Happy_Int -> Token -> Happy_Int -> _
+-- See Note [happyResume]
+happyResume i tk st sts stk = pop_items [] st sts stk
+  where
+    !(Happy_GHC_Exts.I# n_starts) = happy_n_starts   -- this is to test whether we have a start token
+    !(Happy_GHC_Exts.I# eof_i) = happy_n_terms Happy_Prelude.- 1   -- this is the token number of the EOF token
+    happy_list_to_list :: Happy_IntList -> [Happy_Prelude.Int]
+    happy_list_to_list (HappyCons st sts)
+      | LT(st, n_starts)
+      = [(Happy_GHC_Exts.I# st)]
+      | Happy_Prelude.otherwise
+      = (Happy_GHC_Exts.I# st) : happy_list_to_list sts
+
+    -- See (1) of Note [happyResume]
+    pop_items catch_frames st sts stk
+      | LT(st, n_starts)
+      = DEBUG_TRACE("reached start state " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# st) Happy_Prelude.++ ", ")
+        if Happy_Prelude.null catch_frames_new
+          then DEBUG_TRACE("no resumption.\n")
+               happyAbort
+          else DEBUG_TRACE("now discard input, trying to anchor in states " Happy_Prelude.++ Happy_Prelude.show (Happy_Prelude.map (happy_list_to_list . Happy_Prelude.fst) (Happy_Prelude.reverse catch_frames_new)) Happy_Prelude.++ ".\n")
+               discard_input_until_exp i tk (Happy_Prelude.reverse catch_frames_new)
+      | (HappyCons st1 sts1) <- sts, _ `HappyStk` stk1 <- stk
+      = pop_items catch_frames_new st1 sts1 stk1
+      where
+        !catch_frames_new
+          | HappyShift new_state <- happyDecodeAction (happyNextAction CATCH_TOK st)
+          , DEBUG_TRACE("can shift catch token in state " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# st) Happy_Prelude.++ ", into state " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# new_state) Happy_Prelude.++ "\n")
+            Happy_Prelude.null (Happy_Prelude.filter (\(HappyCons _ (HappyCons h _),_) -> EQ(st,h)) catch_frames)
+          = (HappyCons new_state (HappyCons st sts), MK_ERROR_TOKEN(i) `HappyStk` stk):catch_frames -- MK_ERROR_TOKEN(i) is just some dummy that should not be accessed by user code
+          | Happy_Prelude.otherwise
+          = DEBUG_TRACE("already shifted or can't shift catch in " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# st) Happy_Prelude.++ "\n")
+            catch_frames
+
+    -- See (2) of Note [happyResume]
+    discard_input_until_exp i tk catch_frames
+      | Happy_Prelude.Just (HappyCons st (HappyCons catch_st sts), catch_frame) <- some_catch_state_shifts i catch_frames
+      = DEBUG_TRACE("found expected token in state " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# st) Happy_Prelude.++ " after shifting from " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# catch_st) Happy_Prelude.++ ": " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# i) Happy_Prelude.++ "\n")
+        happyDoAction i tk st (HappyCons catch_st sts) catch_frame
+      | EQ(i,eof_i) -- is i EOF?
+      = DEBUG_TRACE("reached EOF, cannot resume. abort parse :(\n")
+        happyAbort
+      | Happy_Prelude.otherwise
+      = DEBUG_TRACE("discard token " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# i) Happy_Prelude.++ "\n")
+        happyLex (\eof_tk -> discard_input_until_exp eof_i eof_tk catch_frames) -- eof
+                 (\i tk   -> discard_input_until_exp i tk catch_frames)         -- not eof
+
+    some_catch_state_shifts _ [] = DEBUG_TRACE("no catch state could shift.\n") Happy_Prelude.Nothing
+    some_catch_state_shifts i catch_frames@(((HappyCons st sts),_):_) = try_head i st sts catch_frames
+      where
+        try_head i st sts catch_frames = -- PRECONDITION: head catch_frames = (HappyCons st sts)
+          DEBUG_TRACE("trying token " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# i) Happy_Prelude.++ " in state " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# st) Happy_Prelude.++ ": ")
+          case happyDecodeAction (happyNextAction i st) of
+            HappyFail     -> DEBUG_TRACE("fail.\n")   some_catch_state_shifts i (Happy_Prelude.tail catch_frames)
+            HappyAccept   -> DEBUG_TRACE("accept.\n") Happy_Prelude.Just (Happy_Prelude.head catch_frames)
+            HappyShift _  -> DEBUG_TRACE("shift.\n")  Happy_Prelude.Just (Happy_Prelude.head catch_frames)
+            HappyReduce r -> case happySimulateReduce r st sts of
+              (HappyCons st1 sts1) -> try_head i st1 sts1 catch_frames
+
+happySimulateReduce r st sts =
+  DEBUG_TRACE("simulate reduction of rule " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# r) Happy_Prelude.++ ", ")
+  let (# nt, len #) = happyIndexRuleArr r in
+  DEBUG_TRACE("nt " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# nt) Happy_Prelude.++ ", len: " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# len) Happy_Prelude.++ ", new_st ")
+  let !(sts1@(HappyCons st1 _)) = happyDrop len (HappyCons st sts)
+      new_st = happyIndexGotoTable nt st1 in
+  DEBUG_TRACE(Happy_Prelude.show (Happy_GHC_Exts.I# new_st) Happy_Prelude.++ ".\n")
+  (HappyCons new_st sts1)
+
+happyTokenToString :: Happy_Prelude.Int -> Happy_Prelude.String
+happyTokenToString i = happyTokenStrings Happy_Prelude.!! (i Happy_Prelude.- 2) -- 2: errorTok, catchTok
+
+happyExpectedTokens :: Happy_Int -> Happy_IntList -> [Happy_Prelude.String]
+-- Upon a parse error, we want to suggest tokens that are expected in that
+-- situation. This function computes such tokens.
+-- It works by examining the top of the state stack.
+-- For every token number that does a shift transition, record that token number.
+-- For every token number that does a reduce transition, simulate that reduction
+-- on the state state stack and repeat.
+-- The recorded token numbers are then formatted with 'happyTokenToString' and
+-- returned.
+happyExpectedTokens st sts =
+  DEBUG_TRACE("constructing expected tokens.\n")
+  Happy_Prelude.map happyTokenToString (search_shifts st sts [])
+  where
+    search_shifts st sts shifts = Happy_Prelude.foldr (add_action st sts) shifts (distinct_actions st)
+    add_action st sts (Happy_GHC_Exts.I# i, Happy_GHC_Exts.I# act) shifts =
+      DEBUG_TRACE("found action in state " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# st) Happy_Prelude.++ ", input " Happy_Prelude.++ Happy_Prelude.show (Happy_GHC_Exts.I# i) Happy_Prelude.++ ", " Happy_Prelude.++ Happy_Prelude.show (happyDecodeAction act) Happy_Prelude.++ "\n")
+      case happyDecodeAction act of
+        HappyFail     -> shifts
+        HappyAccept   -> shifts -- This would always be %eof or error... Not helpful
+        HappyShift _  -> Happy_Prelude.insert (Happy_GHC_Exts.I# i) shifts
+        HappyReduce r -> case happySimulateReduce r st sts of
+          (HappyCons st1 sts1) -> search_shifts st1 sts1 shifts
+    distinct_actions st
+      -- The (token number, action) pairs of all actions in the given state
+      = ((-1), (Happy_GHC_Exts.I# (happyIndexOffAddr happyDefActions st)))
+      : [ (i, act) | i <- [begin_i..happy_n_terms], act <- get_act row_off i ]
+      where
+        row_off = happyIndexOffAddr happyActOffsets st
+        begin_i = 2 -- +2: errorTok,catchTok
+    get_act off (Happy_GHC_Exts.I# i) -- happyIndexActionTable with cached row offset
+      | let off_i = PLUS(off,i)
+      , GTE(off_i,0#)
+      , EQ(happyIndexOffAddr happyCheck off_i,i)
+      = [(Happy_GHC_Exts.I# (happyIndexOffAddr happyTable off_i))]
+      | Happy_Prelude.otherwise
+      = []
+
+-- Internal happy errors:
+
+notHappyAtAll :: a
+notHappyAtAll = Happy_Prelude.error "Internal Happy parser panic. This is not supposed to happen! Please open a bug report at https://github.com/haskell/happy/issues.\n"
+
+-----------------------------------------------------------------------------
+-- Hack to get the typechecker to accept our action functions
+
+happyTcHack :: Happy_Int -> a -> a
+happyTcHack x y = y
+{-# INLINE happyTcHack #-}
+
+-----------------------------------------------------------------------------
+-- Seq-ing.  If the --strict flag is given, then Happy emits
+--      happySeq = happyDoSeq
+-- otherwise it emits
+--      happySeq = happyDontSeq
+
+happyDoSeq, happyDontSeq :: a -> b -> b
+happyDoSeq   a b = a `Happy_GHC_Exts.seq` b
+happyDontSeq a b = b
+
+-----------------------------------------------------------------------------
+-- Don't inline any functions from the template.  GHC has a nasty habit
+-- of deciding to inline happyGoto everywhere, which increases the size of
+-- the generated parser quite a bit.
+
+{-# NOINLINE happyDoAction #-}
+{-# NOINLINE happyTable #-}
+{-# NOINLINE happyCheck #-}
+{-# NOINLINE happyActOffsets #-}
+{-# NOINLINE happyGotoOffsets #-}
+{-# NOINLINE happyDefActions #-}
+
+{-# NOINLINE happyShift #-}
+{-# NOINLINE happySpecReduce_0 #-}
+{-# NOINLINE happySpecReduce_1 #-}
+{-# NOINLINE happySpecReduce_2 #-}
+{-# NOINLINE happySpecReduce_3 #-}
+{-# NOINLINE happyReduce #-}
+{-# NOINLINE happyMonadReduce #-}
+{-# NOINLINE happyGoto #-}
+{-# NOINLINE happyFail #-}
+
+-- end of Happy Template.
diff --git a/src/Lam/Par.y b/src/Lam/Par.y
new file mode 100644
--- /dev/null
+++ b/src/Lam/Par.y
@@ -0,0 +1,78 @@
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6).
+
+-- Parser definition for use with Happy
+{
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lam.Par
+  ( happyError
+  , myLexer
+  , pExp
+  ) where
+
+import Prelude
+
+import qualified Lam.Abs
+import Lam.Lex
+
+}
+
+%name pExp Exp
+-- no lexer declaration
+%monad { Err } { (>>=) } { return }
+%tokentype {Token}
+%token
+  '('      { PT _ (TS _ 1)      }
+  ')'      { PT _ (TS _ 2)      }
+  L_Ident  { PT _ (TV $$)       }
+  L_Lambda { PT _ (T_Lambda $$) }
+  L_Arrow  { PT _ (T_Arrow $$)  }
+
+%%
+
+Ident :: { Lam.Abs.Ident }
+Ident  : L_Ident { Lam.Abs.Ident $1 }
+
+Lambda :: { Lam.Abs.Lambda }
+Lambda  : L_Lambda { Lam.Abs.Lambda $1 }
+
+Arrow :: { Lam.Abs.Arrow }
+Arrow  : L_Arrow { Lam.Abs.Arrow $1 }
+
+Exp3 :: { Lam.Abs.Exp }
+Exp3 : Ident { Lam.Abs.EId $1 } | '(' Exp ')' { $2 }
+
+Exp2 :: { Lam.Abs.Exp }
+Exp2 : Exp2 Exp3 { Lam.Abs.EApp $1 $2 } | Exp3 { $1 }
+
+Exp :: { Lam.Abs.Exp }
+Exp
+  : Lambda Ident Arrow Exp { Lam.Abs.EAbs $1 $2 $3 $4 } | Exp1 { $1 }
+
+Exp1 :: { Lam.Abs.Exp }
+Exp1 : Exp2 { $1 }
+
+Ty1 :: { Lam.Abs.Ty }
+Ty1 : Ident { Lam.Abs.TId $1 } | '(' Ty ')' { $2 }
+
+Ty :: { Lam.Abs.Ty }
+Ty : Ty1 Arrow Ty { Lam.Abs.TArr $1 $2 $3 } | Ty1 { $1 }
+
+{
+
+type Err = Either String
+
+happyError :: [Token] -> Err a
+happyError ts = Left $
+  "syntax error at " ++ tokenPos ts ++
+  case ts of
+    []      -> []
+    [Err _] -> " due to lexer error"
+    t:_     -> " before `" ++ (prToken t) ++ "'"
+
+myLexer :: String -> [Token]
+myLexer = tokens
+
+}
+
diff --git a/src/Lam/Print.hs b/src/Lam/Print.hs
new file mode 100644
--- /dev/null
+++ b/src/Lam/Print.hs
@@ -0,0 +1,155 @@
+-- File generated by the BNF Converter (bnfc 2.9.6).
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+#if __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE OverlappingInstances #-}
+#endif
+
+-- | Pretty-printer for Lam.
+
+module Lam.Print where
+
+import Prelude
+  ( ($), (.)
+  , Bool(..), (==), (<)
+  , Int, Integer, Double, (+), (-), (*)
+  , String, (++)
+  , ShowS, showChar, showString
+  , all, elem, foldr, id, map, null, replicate, shows, span
+  )
+import Data.Char ( Char, isSpace )
+import qualified Lam.Abs
+
+-- | The top-level printing method.
+
+printTree :: Print a => a -> String
+printTree = render . prt 0
+
+type Doc = [ShowS] -> [ShowS]
+
+doc :: ShowS -> Doc
+doc = (:)
+
+render :: Doc -> String
+render d = rend 0 False (map ($ "") $ d []) ""
+  where
+  rend
+    :: Int        -- ^ Indentation level.
+    -> Bool       -- ^ Pending indentation to be output before next character?
+    -> [String]
+    -> ShowS
+  rend i p = \case
+      "["      :ts -> char '[' . rend i False ts
+      "("      :ts -> char '(' . rend i False ts
+      "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
+      "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
+      "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
+      [";"]        -> char ';'
+      ";"      :ts -> char ';' . new i ts
+      t  : ts@(s:_) | closingOrPunctuation s
+                   -> pending . showString t . rend i False ts
+      t        :ts -> pending . space t      . rend i False ts
+      []           -> id
+    where
+    -- Output character after pending indentation.
+    char :: Char -> ShowS
+    char c = pending . showChar c
+
+    -- Output pending indentation.
+    pending :: ShowS
+    pending = if p then indent i else id
+
+  -- Indentation (spaces) for given indentation level.
+  indent :: Int -> ShowS
+  indent i = replicateS (2*i) (showChar ' ')
+
+  -- Continue rendering in new line with new indentation.
+  new :: Int -> [String] -> ShowS
+  new j ts = showChar '\n' . rend j True ts
+
+  -- Make sure we are on a fresh line.
+  onNewLine :: Int -> Bool -> ShowS
+  onNewLine i p = (if p then id else showChar '\n') . indent i
+
+  -- Separate given string from following text by a space (if needed).
+  space :: String -> ShowS
+  space t s =
+    case (all isSpace t, null spc, null rest) of
+      (True , _   , True ) -> []             -- remove trailing space
+      (False, _   , True ) -> t              -- remove trailing space
+      (False, True, False) -> t ++ ' ' : s   -- add space if none
+      _                    -> t ++ s
+    where
+      (spc, rest) = span isSpace s
+
+  closingOrPunctuation :: String -> Bool
+  closingOrPunctuation [c] = c `elem` closerOrPunct
+  closingOrPunctuation _   = False
+
+  closerOrPunct :: String
+  closerOrPunct = ")],;"
+
+parenth :: Doc -> Doc
+parenth ss = doc (showChar '(') . ss . doc (showChar ')')
+
+concatS :: [ShowS] -> ShowS
+concatS = foldr (.) id
+
+concatD :: [Doc] -> Doc
+concatD = foldr (.) id
+
+replicateS :: Int -> ShowS -> ShowS
+replicateS n f = concatS (replicate n f)
+
+-- | The printer class does the job.
+
+class Print a where
+  prt :: Int -> a -> Doc
+
+instance {-# OVERLAPPABLE #-} Print a => Print [a] where
+  prt i = concatD . map (prt i)
+
+instance Print Char where
+  prt _ c = doc (showChar '\'' . mkEsc '\'' c . showChar '\'')
+
+instance Print String where
+  prt _ = printString
+
+printString :: String -> Doc
+printString s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"')
+
+mkEsc :: Char -> Char -> ShowS
+mkEsc q = \case
+  s | s == q -> showChar '\\' . showChar s
+  '\\' -> showString "\\\\"
+  '\n' -> showString "\\n"
+  '\t' -> showString "\\t"
+  s -> showChar s
+
+prPrec :: Int -> Int -> Doc -> Doc
+prPrec i j = if j < i then parenth else id
+
+instance Print Integer where
+  prt _ x = doc (shows x)
+
+instance Print Double where
+  prt _ x = doc (shows x)
+
+instance Print Lam.Abs.Ident where
+  prt _ (Lam.Abs.Ident i) = doc $ showString i
+instance Print Lam.Abs.Lambda where
+  prt _ (Lam.Abs.Lambda i) = doc $ showString i
+instance Print Lam.Abs.Arrow where
+  prt _ (Lam.Abs.Arrow i) = doc $ showString i
+instance Print Lam.Abs.Exp where
+  prt i = \case
+    Lam.Abs.EId id_ -> prPrec i 3 (concatD [prt 0 id_])
+    Lam.Abs.EApp exp1 exp2 -> prPrec i 2 (concatD [prt 2 exp1, prt 3 exp2])
+    Lam.Abs.EAbs lambda id_ arrow exp -> prPrec i 0 (concatD [prt 0 lambda, prt 0 id_, prt 0 arrow, prt 0 exp])
+
+instance Print Lam.Abs.Ty where
+  prt i = \case
+    Lam.Abs.TId id_ -> prPrec i 1 (concatD [prt 0 id_])
+    Lam.Abs.TArr ty1 arrow ty2 -> prPrec i 0 (concatD [prt 1 ty1, prt 0 arrow, prt 0 ty2])
diff --git a/src/License.hs b/src/License.hs
new file mode 100644
--- /dev/null
+++ b/src/License.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module License where
+
+import Data.String.QQ
+
+copyright :: String
+copyright = head (lines license)
+
+license :: String
+license = [s|
+Copyright (C) 2024 Andreas Abel
+
+Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+|]
diff --git a/src/Main.hs b/src/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Main.hs
@@ -0,0 +1,520 @@
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Redundant <&>" #-}
+
+-- | Visualization of constraint-based type inference.
+
+module Main where
+
+import Control.Monad
+import Control.Monad.Except
+import Control.Monad.State
+-- import Control.Monad.TransMaybe
+
+import Data.Function ( on )
+import Data.Functor  ( (<&>) )
+import Data.IntMap   ( IntMap )
+import Data.IntMap   qualified as IntMap
+import Data.Map      ( Map )
+import Data.Map      qualified as Map
+import Data.Maybe
+import Data.Set      ( Set )
+import Data.Set      qualified as Set
+
+import Prettyprinter ( (<+>), annotate, brackets, colon, indent, line, punctuate, vsep )
+import Prettyprinter qualified as P
+import Prettyprinter.Util ( putDocW )
+import Prettyprinter.Internal ( Doc(Empty) )
+import Prettyprinter.Render.Terminal as C
+
+import System.Console.ANSI ( clearScreen, setCursorPosition )
+import System.Exit   ( exitFailure)
+import System.IO     ( hFlush, readFile, stdout )
+
+import Lam.Abs       qualified as A
+import Lam.Abs       ( Ident(..), Exp(..) )
+import Lam.Par       ( pExp, myLexer )
+import Lam.Print     ( Print, printTree )
+
+import Options
+
+-- | State of the type inference problem.
+
+data St = St
+  { stDerivation          :: Derivation
+      -- ^ The problem tree.
+  , stConstraints         :: Constraints
+      -- ^ The collected unsolved constraints.
+  , stSolution            :: Maybe Solution
+      -- ^ A solve meta to be added to the substitution.
+  , stSubstitution        :: Substitution
+      -- ^ The solved constraints.
+  , stMetas               :: MetaVariables
+      -- ^ The collection of allocated metas
+  , stMetaSupply          :: MetaSupply
+      -- ^ A supply of identifiers for meta-variables.
+  , stAction              :: Maybe Action
+      -- ^ Last action taken on derivation.
+  }
+
+-- | Collection of meta variables indexed by their suggested name.
+--   For each name suggestion, we collect the take name suffixes.
+
+type MetaVariables = Map Ident (IntMap Suffix)
+type Suffix        = Int
+
+-- | Supply of available UIDs for metas.
+
+type MetaSupply = [MetaID]
+type MetaID     = Int
+
+-- | A type meta variable.
+
+data Meta = Meta
+  { metaID     :: MetaID
+      -- ^ UID of the meta
+  , metaName   :: Ident
+      -- ^ Suggestion for the name.
+  , metaSuffix :: Suffix
+      -- ^ Suffix for disambiguation of name.
+  }
+
+instance Eq Meta where (==) = (==) `on` metaID
+instance Ord Meta where compare = compare `on` metaID
+
+data Ty
+  = TyMeta Meta
+  | TyFun  Ty Ty
+  deriving (Eq, Ord)
+
+-- | Derivations are fully-annotated lambda-terms with holes.
+
+data Derivation
+  = DLeaf Exp Ty (Maybe TypeError)
+      -- ^ Unsolved ('Nothing') or error ('Just') leaf in the derivation tree.
+  | DVar Ident Ty
+      -- ^ Solved leaf in the derivation tree.
+  | DAbs Ident Ty Exp Ty Derivation
+      -- ^ Lambda abstraction with type of domain and range.
+  | DApp Exp Exp Ty Derivation Derivation
+      -- ^ Application.
+  | DRoot Exp Ty Derivation
+      -- ^ The original problem.
+
+data Action
+  = Check String
+  | Simplify Equation -- ^ Equation between function types
+  | Trivial Meta      -- ^ Reflexive equation.
+  | Solve Meta Ty
+  | Substitute Meta Ty
+  | Fail
+  | Done
+
+data PostAction a = PostAction a Action
+data WithAction a = WithAction Action a
+type TypeError = String
+
+newtype Constraints = Constraints { theConstraints :: [Equation] }
+
+data Equation = Equation Ty Ty
+  deriving (Eq, Ord)
+
+-- | An equation in solved form.
+data Solution = Solution Meta Ty
+
+type Substitution = Map Meta Ty
+
+-- | Typing context.
+type Context = Map Ident Ty
+
+type M = State St
+
+main :: IO ()
+main = do
+
+  -- Parse options.
+  opts@Options{..} <- options
+  let
+    strategy = if optJ then strategyJ else strategyC
+    batch = optBatch || isNothing optFile
+    clear = unless optNoColors do
+      clearScreen
+      setCursorPosition 0 0
+    wait = do
+      hFlush stdout
+      getLine
+    next = do
+      wait
+      clear
+    render :: forall a. Pretty a => a -> IO ()
+    render = (if optNoColors then putDocW 80 else C.putDoc) . pretty
+
+
+  -- Read expression from file or stdin.
+  input <- case optFile of
+    Nothing -> getContents
+    Just f  -> readFile f
+
+  -- Parse expression.
+  e <- case pExp (myLexer input) of
+    Left err -> do
+      putStrLn err
+      exitFailure
+    Right e -> pure e
+
+  let
+    st = initSt e
+    tr = evalState (trampolin strategy) st
+    ss = st : map (\ (WithAction _ s) -> s) tr
+
+  -- In the batch mode, we need to output the initial state here,
+  -- as we won't do it during the loop.
+  if batch then do
+    render st
+    putStrLn ""
+  else do
+    clear
+    putStrLn "(Press ENTER to step)"
+
+  -- Loop over triples (current state, action, subsequent state).
+  forM_ (zip ss tr) \ (s0, WithAction a s) -> do
+    if
+      -- In the batch mode, we display the action and the subsequent state.
+      | batch -> do
+          render $ WithAction a s
+
+      -- In the --slide mode, we display the current state with the next action.
+      | optSlide -> do
+          next
+          render $ PostAction s0 a
+
+      -- In default mode, we display current state, and after the ok from the user,
+      -- the action and the next state.
+      | otherwise -> do
+          next
+          render s0
+          wait
+          render $ WithAction a s
+
+  -- In the --slide mode, we have not displayed the final state yet.
+  when optSlide do
+    let WithAction _ s = last tr
+    next
+    render $ PostAction s Done
+    putStrLn ""
+
+-- | Initial type inference problem.
+
+initSt :: Exp -> St
+initSt e = St
+  { stDerivation   = DRoot e t $ DLeaf e t Nothing
+  , stConstraints  = Constraints []
+  , stSolution     = Nothing
+  , stSubstitution = Map.empty
+  , stMetas        = addMeta m Map.empty
+  , stMetaSupply   = [1..]
+  , stAction       = Nothing
+  }
+  where
+    x   = Ident "?"
+    mid = 0
+    suf = 0
+    m   = Meta{ metaID = mid, metaName = x, metaSuffix = suf }
+    t   = TyMeta m
+
+-- | Algorithm C: first collect all constraints, then solve them.
+
+strategyC :: M (Maybe Action)
+strategyC = foldl1 orElse $
+  [ stepDerivation
+  , stepSolution
+  , stepConstraints
+  ]
+
+-- | Algorithm J: solve a constraint as soon as it arises.
+
+strategyJ :: M (Maybe Action)
+strategyJ = foldl1 orElse
+  [ stepSolution
+  , stepConstraints
+  , stepDerivation
+  ]
+
+-- | Combination of tactics.
+
+orElse :: Monad m => m (Maybe Action) -> m (Maybe Action) -> m (Maybe Action)
+orElse c1 c2 = do
+  c1 >>= \case
+    Nothing -> c2
+    Just Fail -> return $ Nothing
+    Just a  -> return $ Just a
+
+-- | Try to make progress in the derivation.
+
+stepDerivation :: M (Maybe Action)
+stepDerivation = do
+  putAction Nothing
+  d <- gets stDerivation
+  putDerivation =<< loop Map.empty d
+  gets stAction
+  where
+    loop :: Context -> Derivation -> M Derivation
+    loop cxt d = gets stAction >>= \case
+      Just{}  -> return d
+      Nothing -> case d of
+        DRoot e t d        -> DRoot e t <$> loop cxt d
+        d@DVar{}           -> pure d
+        DAbs x t1 e t2 d   -> DAbs x t1 e t2 <$> loop (Map.insert x t1 cxt) d
+        DApp e1 e2 t d1 d2 -> DApp e1 e2 t <$> loop cxt d1 <*> loop cxt d2
+        DLeaf e t Just{}   -> pure d
+        DLeaf e t Nothing  -> do
+          case e of
+            EId x -> do
+              checkAction "variable"
+              case Map.lookup x cxt of
+                Nothing -> pure $ DLeaf e t $ Just $ "unbound variable"
+                Just t1 -> DVar x t <$ subType t1 t
+            EAbs _lam x _arr body -> do
+              checkAction "abstraction"
+              (t1, t2) <- splitFunType (Just x) t
+              pure $ DAbs x t1 body t2 $ DLeaf body t2 Nothing
+            EApp e1 e2 -> do
+              checkAction "application"
+              dom <- TyMeta <$> newMeta Nothing
+              pure $ DApp e1 e2 t (DLeaf e1 (TyFun dom t) Nothing) (DLeaf e2 dom Nothing)
+    checkAction = putAction . Just . Check
+
+splitFunType :: Maybe Ident -> Ty -> M (Ty, Ty)
+splitFunType x = \case
+  TyFun t1 t2 -> return (t1, t2)
+  t@TyMeta{}  -> do
+    t1 <- TyMeta <$> newMeta x
+    t2 <- TyMeta <$> newMeta Nothing
+    (t1, t2) <$ equate t (TyFun t1 t2) -- subType (TyFun t1 t2) t
+
+-- | Try to apply the last solution.
+
+stepSolution :: M (Maybe Action)
+stepSolution = do
+  gets stSolution >>= \case
+    Nothing -> return Nothing
+    Just (Solution x t)
+      | occurs x t -> return $ Just Fail
+      | otherwise -> Just (Substitute x t) <$
+          modify \ st -> st
+            { stSolution     = Nothing
+            , stDerivation   = substitute x t (stDerivation st)
+            , stConstraints  = substitute x t (stConstraints st)
+            , stSubstitution = substitute x t (stSubstitution st)
+            }
+
+class Substitute a where
+  substitute :: Meta -> Ty -> a -> a
+
+instance Substitute Ty where
+  substitute x t0 = \case
+    TyMeta y -> if x == y then t0 else TyMeta y
+    TyFun t1 t2 -> TyFun (substitute x t0 t1) (substitute x t0 t2)
+
+instance Substitute Equation where
+  substitute x t0 (Equation t1 t2) = Equation (substitute x t0 t1) (substitute x t0 t2)
+
+instance Substitute a => Substitute [a] where
+  substitute x t0 = fmap $ substitute x t0
+
+instance Substitute a => Substitute (Map k a) where
+  substitute x t0 = fmap $ substitute x t0
+
+instance Substitute Constraints where
+  substitute x t0 = Constraints . substitute x t0 . theConstraints
+
+instance Substitute Derivation where
+  substitute x0 t0 = \case
+    DRoot e t d        -> DRoot e (substitute x0 t0 t) (substitute x0 t0 d)
+    DLeaf e t err      -> DLeaf e (substitute x0 t0 t) err
+    DAbs x t1 e t2 d   -> DAbs x  (substitute x0 t0 t1) e (substitute x0 t0 t2) (substitute x0 t0 d)
+    DApp e1 e2 t d1 d2 -> DApp e1 e2 (substitute x0 t0 t) (substitute x0 t0 d1) (substitute x0 t0 d2)
+    DVar x t           -> DVar x     (substitute x0 t0 t)
+
+
+-- | Try to make progress with the constraints
+
+stepConstraints :: M (Maybe Action)
+stepConstraints = do
+  gets (theConstraints . stConstraints) >>= \case
+    [] -> return Nothing
+    Equation t1 t2 : cs -> do
+      modify \ st -> st{ stConstraints = Constraints cs }
+      unify t1 t2
+
+unify :: Ty -> Ty -> M (Maybe Action)
+unify t1 t2 = case (t1, t2) of
+  (TyFun dom1 rng1, TyFun dom2 rng2) -> do
+    equate rng1 rng2
+    equate dom1 dom2
+    return $ Just $ Simplify $ Equation t1 t2
+  (TyFun{}, TyMeta m) -> solve m t1
+  (TyMeta m, TyFun{}) -> solve m t2
+  (TyMeta m1, TyMeta m2) ->
+    -- Heuristics: keep older metas
+    case (compare `on` metaID) m1 m2 of
+      LT -> solve m2 t1
+      EQ -> return $ Just $ Trivial m1
+      GT -> solve m1 t2
+
+solve :: Meta -> Ty -> M (Maybe Action)
+solve m t = do
+  modify \ st -> st{ stSolution = Just $ Solution m t }
+  return $ Just $ Solve m t
+
+occurs :: Meta -> Ty -> Bool
+occurs x = \case
+  TyMeta y -> x == y
+  TyFun t1 t2 -> occurs x t1 || occurs x t2
+
+-- | From the current state, unfold with the given modifier until no more action is produced.
+--   (Classic trampolin.)
+
+trampolin :: M (Maybe Action) -> M [WithAction St]
+trampolin step = loop
+  where
+    loop = step >>= \case
+      Nothing -> return []
+      Just a  -> do
+        st <- get
+        (WithAction a st :) <$> loop
+
+-- * State manipulation
+
+equate :: Ty -> Ty -> M ()
+equate t1 t2 = modify \ st -> st{ stConstraints = addConstraint (Equation t1 t2) (stConstraints st) }
+
+subType :: Ty -> Ty -> M ()
+subType t1 t2 = modify \ st -> st{ stConstraints = addConstraint (Equation t1 t2) (stConstraints st) }
+
+putAction :: Maybe Action -> M ()
+putAction a = modify \ st -> st{ stAction = a }
+
+putDerivation :: Derivation -> M ()
+putDerivation a = modify \ st -> st{ stDerivation = a }
+
+newMeta :: Maybe Ident -> M Meta
+newMeta mx = do
+  let x = fromMaybe (Ident "?") mx
+  st <- get
+  case stMetaSupply st of
+    i:is -> do
+      let
+        metas = stMetas st
+        -- Get next available suffix for x
+        suf = case Map.lookup x metas of
+          Nothing -> 0
+          Just ss -> maximum ss + 1
+        m = Meta i x suf
+      m <$ put st{ stMetaSupply = is, stMetas = addMeta m metas }
+
+-- * Auxiliary functions
+
+addMeta :: Meta -> MetaVariables -> MetaVariables
+addMeta (Meta i x suf) = Map.insertWith IntMap.union x (IntMap.singleton i suf)
+
+addConstraint :: Equation -> Constraints -> Constraints
+addConstraint e (Constraints cs) = Constraints $ e : cs
+
+-- * Pretty printing
+
+-- | Colored documents.
+
+type CDoc = Doc AnsiStyle
+
+annotateExp :: CDoc -> CDoc
+annotateExp = annotate $ colorDull Magenta
+
+annotateTy :: CDoc -> CDoc
+annotateTy = annotate $ colorDull Green
+
+annotateMeta :: CDoc -> CDoc
+annotateMeta = annotate $ color Yellow
+
+class Pretty a where
+  pretty :: a -> CDoc
+
+instance Pretty String where
+  pretty = P.pretty
+
+instance Pretty a => Pretty (Maybe a) where
+  pretty = maybe mempty pretty
+
+instance Pretty St where
+  pretty St{ stDerivation = d, stSolution = ms, stConstraints = cs } =
+    ruleSep [ pretty d, pretty ms, pretty cs ]
+
+ruleSep :: [CDoc] -> CDoc
+ruleSep = vsep . punctuate (line <> pretty (replicate 12 '─')) . filter (not . isEmpty)
+
+isEmpty :: Doc ann -> Bool
+isEmpty = \case
+  Empty -> True
+  _ -> False
+
+instance Pretty Derivation where
+  pretty = \case
+    DRoot e t d        -> ("¿" <+> judgement e t) $$ pretty d
+    DVar x t           -> checkMark (judgement x t)
+    DAbs x t1 e t2 d   -> checkMark (brackets (judgement x t1) <+> judgement e t2) $$ indent 2 (pretty d)
+    DApp e1 e2 t d1 d2 -> checkMark (judgement (EApp e1 e2) t) $$ indent 2 (pretty d1 $$ pretty d2)
+    DLeaf e t Nothing  -> "•" <+> judgement e t
+    DLeaf e t (Just err) -> "✗" <+> judgement e t <+> brackets (pretty err)
+
+instance Pretty Constraints where
+  pretty = vsep . map pretty . theConstraints
+
+instance Pretty Equation where
+  pretty (Equation t1 t2) = pretty t1 <+> "≟" <+> pretty t2
+
+instance Pretty Solution where
+  pretty (Solution x t) = pretty x <+> "=" <+> pretty t <+>
+    (if occurs x t then "✗ recursive" else "✓")
+
+instance Pretty Action where
+  pretty = \case
+    Check s        -> "checking" <+> pretty s
+    Simplify eq    -> "simplify" <+> pretty eq
+    Solve x t      -> "occurs check" <+> pretty x <+> "=" <+> pretty t
+    Substitute x t -> "substitute" <+> pretty x <+> ":=" <+> pretty t
+    Trivial x      -> "discard trivial equation" <+> pretty x <+> "=" <+> pretty x
+    Done           -> "done"
+
+instance Pretty a => Pretty (WithAction a) where
+  pretty (WithAction a d) = line <> "==>" <+> pretty a <> line <> line <> pretty d <> line
+
+instance Pretty a => Pretty (PostAction a) where
+  pretty (PostAction d a) = line <> pretty d <> line <> line <> "==>" <+> pretty a <> line
+
+instance Pretty Ident where
+  pretty = pretty . printTree
+
+instance Pretty Exp where
+  pretty = annotateExp . pretty . printTree
+
+instance Pretty Ty where
+  pretty = annotateTy . pretty . printTree . tyA
+
+instance Pretty Meta where
+  pretty = annotateMeta . pretty . metaString
+
+($$) :: Doc ann -> Doc ann -> Doc ann
+d1 $$ d2 = d1 <> line <> d2
+
+checkMark :: Doc ann -> Doc ann
+checkMark = ("✓" <+>)
+
+judgement :: (Pretty a, Pretty b) => a -> b -> CDoc
+judgement x t = annotateExp (pretty x) <+> colon <+> annotateTy (pretty t)
+
+tyA :: Ty -> A.Ty
+tyA = \case
+  TyFun t1 t2 -> A.TArr (tyA t1) (A.Arrow "→") (tyA t2)
+  TyMeta m    -> A.TId $ Ident $ metaString m
+
+metaString :: Meta -> String
+metaString (Meta _ (Ident x) suf) = x ++ show suf
diff --git a/src/Options.hs b/src/Options.hs
new file mode 100644
--- /dev/null
+++ b/src/Options.hs
@@ -0,0 +1,159 @@
+module Options where
+
+import Data.List
+  ( intercalate )
+import Data.Version
+  ( Version(versionBranch) )
+
+import Options.Applicative
+  ( Parser, (<**>)
+  , action, execParser, footerDoc, headerDoc, help, helper, hidden
+  , info, infoOption, long, metavar, optional, short, strArgument, switch, value
+  )
+import Options.Applicative.Help.Pretty
+  ( pretty, nest, vcat )
+
+import System.IO
+  ( stdout )
+import System.Console.ANSI
+  ( hSupportsANSI )
+
+import ColorOption
+import License
+import qualified Paths_visualize_type_inference as Paths
+
+-- | Program options.
+
+data Options = Options
+  { optBatch      :: Bool
+      -- ^ Run in batch mode (rather than interactively step-by-step).
+  , optJ          :: Bool
+      -- ^ Algorithm J (immediate substitution) rather than C (constraint collection).
+  , optColor      :: ColorOption
+      -- ^ GNU @--color@ option.
+  , optFile       :: Maybe FilePath
+      -- ^ The file with the input (optional).
+  , optNoColors   :: Bool
+      -- ^ Turn off colors?  (Default: no.)
+  , optSlide      :: Bool
+      -- ^ Slide mode?  Less intermediate steps.  (Default: no.)
+  }
+
+
+self :: String
+self = "visualize-type-inference"
+
+homepage :: String
+homepage = concat [ "https://github.com/teach-plt/", self ]
+
+-- | The program version obtained from the cabal file.
+
+version :: String
+version = intercalate "." $ map show $ versionBranch Paths.version
+
+-- | Option parsing and handling
+
+options :: IO Options
+options = do
+  opts <- execParser $ info parser infoMod
+  case optColor opts of
+    Always -> return opts
+    Never  -> return opts{ optNoColors = True }
+    Auto   -> hSupportsANSI stdout >>= \case
+      True  -> return opts
+      False -> return opts{ optNoColors = True }
+  where
+  parser = programOptions <**>
+    (versionOption <*> numericVersionOption <*> licenseOption <*> helper)
+  infoMod = headerDoc header <> footerDoc footer
+
+  versionOption =
+    infoOption versionLong
+      $  long "version"
+      <> short 'V'
+      <> help "Show version info."
+      <> hidden
+  versionText = unwords [ self, "version", version ]
+  versionLong = intercalate "\n" $
+    [ versionText
+    , copyright
+    , "This is free software under the BSD-3-clause license."
+    ]
+
+  numericVersionOption =
+    infoOption version
+      $  long "numeric-version"
+      <> help "Show just version number."
+      <> hidden
+      -- Newline at the end:
+      -- <> helpDoc (Just $ text "Show just version number." <$$> text "")
+
+  licenseOption =
+    infoOption license
+      $  long "license"
+      -- <> long "licence"
+      <> help "Show the license text."
+      <> hidden
+
+  -- Obs: match the order with Options.Options!
+  programOptions = pure Options
+    <*> oBatch
+    <*> oJ
+    <*> colorOption
+    <*> oFile
+    <*> pure False  -- by default, use colors
+    <*> oSlide
+
+  oBatch =
+    switch
+      $  long "batch"
+      <> short 'b'
+      <> help "Run in batch mode (rather than interactively step-by-step)."
+
+  oSlide =
+    switch
+      $  long "slide"
+      <> short 's'
+      <> help "Run in slide mode: interactive, omitting repetition of state."
+
+  oJ =
+    switch
+      $  short 'J'
+      <> help "Algorithm J: solve and substitute eagerly."
+
+  -- oVerbose =
+  --   switch
+  --     $  long "verbose"
+  --     <> short 'v'
+  --     <> help "Comment on what is happening."
+
+  oNoColors =
+    switch
+      $  long "no-colors"
+      <> help "Disable colorized output.  Automatic if terminal does not support colors."
+
+  oFile :: Parser (Maybe FilePath)
+  oFile = optional $
+    strArgument
+      $  metavar "FILE"
+      <> action "file"
+      <> help "The text file containing the lambda-term for type inference."
+
+  -- Note: @header@ does not respect line breaks, so we need @headerDoc@.
+  header = Just $ vcat
+    [ pretty $ unwords [ versionText, homepage ]
+    , ""
+    , "Visualize type inference for the simply-typed lambda-calculus"
+    , "based on type meta variables and unification."
+    ]
+  footer = Just $ vcat
+    [ "By default, constraints are collected first and then solved one-by-one."
+    , "With option -J, each new constraint is solved right away."
+    , ""
+    , "Type inference is performed on a single term in Haskell syntax read from FILE."
+    , "If no FILE is given, the term is read from standard input and processed in batch mode."
+    , ""
+    , "Example terms:"
+    , nest 2 $ "\\ f -> \\ g -> \\ x -> f (g x)"
+    , nest 2 $ "λ x → x x"
+    ]
diff --git a/visualize-type-inference.cabal b/visualize-type-inference.cabal
new file mode 100644
--- /dev/null
+++ b/visualize-type-inference.cabal
@@ -0,0 +1,68 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.38.1.
+--
+-- see: https://github.com/sol/hpack
+
+name:           visualize-type-inference
+version:        0.0.1.0
+synopsis:       Simulate simple constraint-based type inference
+description:    Constraint-based inference for simple types is traced step-by-step, both for the original algorithm J that eagerly applies substitutions gained from unification, and a more modern conception that separates constraint generation from constraint solving.
+category:       Teaching
+homepage:       https://github.com/teach-plt/visualize-type-inference#readme
+bug-reports:    https://github.com/teach-plt/visualize-type-inference/issues
+author:         Andreas Abel
+maintainer:     Andreas Abel
+copyright:      Andreas Abel, 2024
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+tested-with:
+    GHC == 9.12.2
+  , GHC == 9.10.3
+  , GHC == 9.8.4
+  , GHC == 9.6.7
+  , GHC == 9.4.8
+  , GHC == 9.2.8
+
+source-repository head
+  type: git
+  location: https://github.com/teach-plt/visualize-type-inference
+
+executable visualize-type-inference
+  main-is: Main.hs
+  other-modules:
+      ColorOption
+      Lam.Abs
+      Lam.Lex
+      Lam.Par
+      Lam.Print
+      License
+      Options
+      Paths_visualize_type_inference
+  hs-source-dirs:
+      src
+  default-extensions:
+      BlockArguments
+      FlexibleInstances
+      ImportQualifiedPost
+      LambdaCase
+      MultiWayIf
+      OverloadedStrings
+      RecordWildCards
+      ScopedTypeVariables
+      TypeSynonymInstances
+  build-tools:
+      alex
+    , happy
+  build-depends:
+      ansi-terminal
+    , array
+    , base >=4.15 && <5
+    , containers
+    , mtl
+    , optparse-applicative
+    , prettyprinter
+    , prettyprinter-ansi-terminal
+    , string-qq
+  default-language: Haskell2010
