diff --git a/examples/Main.hs b/examples/Main.hs
index 11a866c..5385c9f 100644
--- a/examples/Main.hs
+++ b/examples/Main.hs
@@ -1,35 +1,90 @@
 {-# LANGUAGE TemplateHaskellQuotes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
 
 import Gigaparsec
 
 import Control.Applicative ( Alternative((<|>)) )
 import Data.Char ( intToDigit )
 import Data.Foldable ( asum, traverse_ )
+import Data.GADT.Compare
+import Data.Type.Equality
 
-digit :: Int -> Parser Int
-digit b = asum [i <$ char (intToDigit i) | i <- [0..b - 1]]
+data E a where
+  E :: E Int
+  N :: Int -> E Int
+  D :: Int -> E Int
+  NDots :: E ()
+  NDotsGo :: Int -> E ()
+deriving instance Eq (E a)
+deriving instance Ord (E a)
+instance GEq E where
+  geq E E = Just Refl
+  geq (N x) (N y) | x == y = Just Refl
+  geq (D x) (D y) | x == y = Just Refl
+  geq NDots NDots = Just Refl
+  geq (NDotsGo x) (NDotsGo y) | x == y = Just Refl
+  geq _ _ = Nothing
+instance GCompare E where
+  gcompare E E = GEQ
+  gcompare (N x) (N y) =
+    case compare x y of
+      LT -> GLT
+      EQ -> GEQ
+      GT -> GGT
+  gcompare (D x) (D y) =
+    case compare x y of
+      LT -> GLT
+      EQ -> GEQ
+      GT -> GGT
+  gcompare NDots NDots = GEQ
+  gcompare (NDotsGo x) (NDotsGo y) =
+    case compare x y of
+      LT -> GLT
+      EQ -> GEQ
+      GT -> GGT
+  gcompare E _ = GLT
+  gcompare _ E = GGT
+  gcompare N{} _ = GLT
+  gcompare _ N{} = GGT
+  gcompare D{} _ = GLT
+  gcompare _ D{} = GGT
+  gcompare NDots _ = GLT
+  gcompare _ NDots = GGT
 
-number :: Int -> Parser Int
-number b = 'number
-  ::= (\x y -> b * x + y) <$> number b <*> digit b
-  <|> digit b
+digit :: Int -> RHS E Int
+digit b = asum [i <$ t (intToDigit i) | i <- [0..b - 1]]
 
-expr :: Parser Int
-expr = 'expr
-  ::= (*) <$> expr <* char '*' <*> expr
-  <|> (+) <$> expr <* char '+' <*> expr 
+number :: Int -> RHS E Int
+number b = (\x y -> b * x + y) <$> nt (N b) <*> nt (D b)
+  <|> nt (D b)
+
+expr :: RHS E Int
+expr = (*) <$> nt E <* t '*' <*> nt E
+  <|> (+) <$> nt E <* t '+' <*> nt E 
   <|> number 10
 
-ndots :: Parser ()
-ndots = number 10 >>= go where
-  go 0 = pure ()
-  go n = char '.' *> go (n - 1)
+ndots :: RHS E ()
+ndots = nt (N 10) >>= nt . NDotsGo
+
+ndotsGo :: Int -> RHS E ()
+ndotsGo 0 = pure ()
+ndotsGo n = t '.' *> nt (NDotsGo (n - 1))
+
+mkE :: E a -> CFG E a
+mkE e = CFG e $ \case
+  E -> expr
+  N b -> number b
+  D b -> digit b
+  NDots -> ndots
+  NDotsGo n -> ndotsGo n
 
 main :: IO ()
 main = do
   -- simple left-recursive
   putStrLn "Should succeed:"
-  traverse_ (\x -> print (x, parse (number 2) x))
+  traverse_ (\x -> print (x, parse (mkE (N 2)) x))
     [ "0"
     , "1"
     , "00"
@@ -40,7 +95,7 @@ main = do
     , "11111"
     ]
   putStrLn "Should fail:"
-  traverse_ (\x -> print (x, parse (number 2) x))
+  traverse_ (\x -> print (x, parse (mkE (N 2)) x))
     [ ""
     , "X"
     , "01X00"
@@ -50,7 +105,7 @@ main = do
 
   -- more complicated left-recursive
   putStrLn "Should succeed:"
-  traverse_ (\x -> print (x, parse expr x))
+  traverse_ (\x -> print (x, parse (mkE E) x))
     [ "1+1" 
     , "1+2+3"
 --    , "1+2+3+4+5+6+7+8+9"
@@ -59,15 +114,71 @@ main = do
 
   -- monadic
   putStrLn "Should succeed:"
-  traverse_ (\x -> print (x, parse ndots x))
+  traverse_ (\x -> print (x, parse (mkE NDots) x))
     [ "5....."
     , "3..."
     , "10.........."
     ]
   putStrLn "Should fail:"
-  traverse_ (\x -> print (x, parse ndots x))
+  traverse_ (\x -> print (x, parse (mkE NDots) x))
     [ "5...."
     , "5......"
     , "3....."
     , "10........"
-    ]
\ No newline at end of file
+    ]
+
+
+-- data E a where E :: E Int
+
+-- deriving instance Eq (E a)
+-- deriving instance Ord (E a)
+-- instance GEq E where
+--   geq E E = Just Refl
+-- instance GCompare E where
+--   gcompare E E = GEQ
+-- deriving instance Show (E a)
+
+example :: CFG E Int
+example = CFG E $ \E -> nt E *> t '+' *> nt E <|> 0 <$ t 'a'
+
+-- >>> parseCFG example "a+a+a+a+a+a"
+-- (G {getG = Rel (fromList [(Comm "E" 0,[(Slot,0,<Cont>),(Slot,0,<Cont>)]),(Comm "E" 2,[(Slot,2,<Cont>),(Slot,0,<Cont>)]),(Comm "E" 4,[(Slot,2,<Cont>),(Slot,4,<Cont>),(Slot,0,<Cont>)]),(Comm "E" 6,[(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,4,<Cont>),(Slot,6,<Cont>),(Slot,0,<Cont>)]),(Comm "E" 8,[(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,4,<Cont>),(Slot,6,<Cont>),(Slot,8,<Cont>),(Slot,0,<Cont>)]),(Comm "E" 10,[(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,4,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,4,<Cont>),(Slot,0,<Cont>),(Slot,6,<Cont>),(Slot,8,<Cont>),(Slot,10,<Cont>),(Slot,0,<Cont>)])])},P {getP = Rel (fromList [(Comm "E" 0,[11,11,11,11,9,11,11,11,11,9,11,11,11,9,7,11,11,9,11,11,11,11,9,11,11,9,7,5,11,11,11,9,11,11,11,9,7,11,11,9,11,11,11,11,9,11,11,11,9,7,11,11,9,11,11,11,9,11,11,11,9,7,5,3,1]),(Comm "E" 2,[11,11,11,11,9,11,11,11,9,11,11,9,7,11,11,11,9,11,11,9,7,5,3]),(Comm "E" 4,[11,11,11,9,11,11,9,7,5]),(Comm "E" 6,[11,11,9,7]),(Comm "E" 8,[11,9]),(Comm "E" 10,[11])])},True)
+
+-- data N a where N :: N Int
+-- deriving instance Eq (N a)
+-- deriving instance Ord (N a)
+-- deriving instance Show (N a)
+-- instance GEq N where
+--   geq N N = Just Refl
+-- instance GCompare N where
+--   gcompare N N = GEQ
+-- instance GShow N where
+--   gshowsPrec _ N = showString "N"
+
+example3 :: CFG E Int
+example3 = CFG E $ \E -> (+ 1) <$ t 'a' <*> nt E <|> pure 0
+
+example4 :: CFG E Int
+example4 = CFG E $ \E -> (+ 1) <$> nt E <* t 'a' <|> pure 0
+
+-- Turns out example3 takes quadratic space, I hope this can be fixed
+
+-- >>> parse example3 "aaaa"
+-- [4]
+
+-- >>> parse example4 "aaaa"
+-- [4]
+
+-- main :: IO ()
+-- -- main = print (parseCFG example "a+a+a")
+-- 
+-- main = do
+--   print $ parseCFG example3 (Text.pack "aaaa")
+--   print $ parseCFG example4 (Text.pack "aaaa")
+-- --  result <-
+-- --    fits $
+-- --      mkFitConfig
+-- --        (\n -> (\(T3 _ _ b) -> b) $ parseCFG example4 (Text.replicate (fromIntegral n) (Text.pack "a")))
+-- --        (1000, 1000000)
+-- --  mapM_ print result
+-- 
diff --git a/experiments/Experiment4.hs b/experiments/Experiment4.hs
deleted file mode 100644
index 56612a0..0000000
--- a/experiments/Experiment4.hs
+++ /dev/null
@@ -1,225 +0,0 @@
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE LambdaCase #-}
-{-# OPTIONS_GHC -Wall #-}
-
-import Data.Map.Strict (Map)
--- import Data.Set (Set)
-import Control.Applicative
-import Control.Monad
-import Data.Map.Strict qualified as Map
--- import GHC.Base (Any)
--- import Debug.Trace
-import Test.Tasty.Bench.Fit
-import Data.Text qualified as Text
-import Data.Text (Text)
-import Data.Some
-import Data.Functor.Identity
-import Data.GADT.Show
-import Data.Bifunctor
-import Unsafe.Coerce (unsafeCoerce)
-import Data.GADT.Compare
-import Data.Type.Equality
-
-data RHS f a = Pure a | T Char (RHS f a) | forall x. NT (f x) (x -> RHS f a) | Or (RHS f a) (RHS f a) | Fail
-deriving instance Functor (RHS f)
-
-instance Applicative (RHS f) where
-  pure = Pure
-  (<*>) = ap
-
-instance Alternative (RHS f) where
-  (<|>) = Or
-  empty = Fail
-
-instance Monad (RHS f) where
-  Pure x >>= k = k x
-  T c k >>= k' = T c (k >>= k')
-  NT f k >>= k' = NT f (k >=> k')
-  Or p q >>= k = Or (p >>= k) (q >>= k)
-  Fail >>= _ = Fail
-
-data CFG f a = CFG (f a) (forall x. f x -> RHS f x)
-
-data T3 a b c = T3 !a !b !c deriving Show
-
-data Comm f = Comm !(Some f) !Int deriving (Eq, Ord, Show)
-
-newtype Cont f a = Cont { getCont :: Text -> Descr -> a -> Command f }
-instance Show (Cont f a) where
-  show _ = "<Cont>"
-
-data Descr = Descr Slot !Int !Int
-data Slot = Slot -- String [Symbol] [Symbol]
-  deriving Show
-
-newtype Rel a b = Rel (Map a [b]) deriving Show
-
-rel :: Ord a => Rel a b -> a -> [b]
-rel (Rel m) x = Map.findWithDefault [] x m
-
-relMay :: Ord a => Rel a b -> a -> Maybe [b]
-relMay (Rel m) x = Map.lookup x m
-
-initRel :: Ord a => a -> Rel a b -> Rel a b
-initRel x (Rel m) = Rel (Map.insertWith (++) x [] m)
-
-addRel :: Ord a => a -> b -> Rel a b -> Rel a b
-addRel x y (Rel m) = Rel (Map.insertWith (++) x [y] m)
-
-instance GShow Identity where
-  gshowsPrec _ _ = showString "<Identity>"
-instance GShow (Cont f) where
-  gshowsPrec _ _ = showString "<Cont>"
-
--- newtype U = U (Set Descr)
-newtype G f = G { getG :: Rel (Comm f) (Slot, Int, Some (Cont f)) } deriving Show
-newtype P f = P { getP :: Rel (Comm f) (Int, Some Identity) } deriving Show
-
-newtype Command f = Command { getCommand :: forall x. T3 (G f) (P f) (Maybe x) -> T3 (G f) (P f) (Maybe x) }
-
-newtype M f a = M { getM :: Text -> Descr -> Cont f a -> Command f }
-
-extents :: GCompare f => f a -> M f (Maybe [(Int, a)])
-extents nt = M $ \inp dsc@(Descr _ _ i) (Cont k) ->
-  Command $ \(T3 g p b) -> -- trace ("extents " ++ show (nt, i)) $
-  getCommand
-    (k inp dsc (
-      let res = relMay (getP p) (Comm (Some nt) i)
-      in fmap (map (second (\(Some (Identity x)) -> unsafeCoerce x))) res))
-    (T3 g (P (initRel (Comm (Some nt) i) (getP p))) b)
-
-addExtent :: GCompare f => f a -> a -> M f ()
-addExtent nt x = M $ \inp dsc@(Descr _ l i) (Cont k) ->
-  Command $ \(T3 g p b) -> -- trace ("addExtent " ++ show (nt, l, i)) $
-  getCommand (k inp dsc ()) (T3 g (P (addRel (Comm (Some nt) l) (i, Some (Identity x)) (getP p))) b)
-
-resume :: GCompare f => f a -> a -> M f a
-resume nt x = M $ \inp (Descr Slot l r) _ ->
-  Command $ \(T3 g p b) ->
-    let cnts = rel (getG g) (Comm (Some nt) l) in -- trace ("resume " ++ show (nt, l, cnts)) $
-    foldr (\(s, l', Some (Cont k)) go -> go . getCommand (unsafeCoerce k inp (Descr s l' r) x))
-      id cnts (T3 g p b)
-
-addCont :: GCompare f => f a -> M f c -> M f c
-addCont nt m = M $ \inp dsc@(Descr s l i) k ->
-  Command $ \(T3 g p b) -> -- trace ("addCont " ++ show (nt, i)) $
-    getCommand (getM m inp dsc k) (T3 (G (addRel (Comm (Some nt) i) (s, l, Some k) (getG g))) p b)
-
-match :: Char -> M f ()
-match c = M $ \inp (Descr (Slot {- nt alpha beta -}) l i) (Cont k) ->
-  case Text.uncons inp of
-    Just (x,inp') | c == x -> k inp' (Descr (Slot {- nt alpha beta -}) l (i + 1)) ()
-    _ -> Command id
-
-skip :: Int -> M f ()
-skip r = M $ \inp (Descr s l i) (Cont k) -> k (Text.drop (r - i) inp) (Descr s l r) ()
-
-descend :: M f ()
-descend = M $ \inp (Descr Slot _ i) (Cont k) -> k inp (Descr Slot i i) ()
-
--- traceI :: String -> M ()
--- traceI msg = M $ \inp dsc@(Descr _ _ i) k -> trace (show i ++ ": " ++ msg) getCont k inp dsc ()
-
-instance Functor (M f) where
-  fmap f (M p) = M $ \inp dsc (Cont k) ->
-    p inp dsc $ Cont $ \inp' dsc' x ->
-      k inp' dsc' (f x)
-instance Applicative (M f) where
-  pure x = M $ \inp dsc (Cont k) -> k inp dsc x
-  (<*>) = ap
-instance Alternative (M f) where
-  empty = M $ \_ _ _ -> Command id
-  M p <|> M q = M $ \inp dsc k -> Command (getCommand (q inp dsc k) . getCommand (p inp dsc k))
-instance Monad (M f) where
-  M p >>= k = M $ \inp dsc k' ->
-    p inp dsc $ Cont $ \inp' dsc' x ->
-      getM (k x) inp' dsc' k'
-
-parseCFG :: forall f a. GCompare f => CFG f a -> Text -> T3 (G f) (P f) (Maybe a)
-parseCFG (CFG nt0 prods) inp0 =
-  getCommand
-    (getM (parseRHS (NT nt0 pure)) inp0 (Descr Slot 0 0) final)
-    (T3 (G (Rel mempty)) (P (Rel mempty)) Nothing) where
-
-  final :: Cont f a
-  final = Cont $ \inp _ x -> Command $ \(T3 p g b) -> (T3 p g (b <|> unsafeCoerce x <$ guard (Text.null inp)))
-
-  parseRHS :: RHS f x -> M f x
-  parseRHS (Pure x) = pure x
-  parseRHS (T c k) = parseT c *> parseRHS k
-  parseRHS (NT f k) = parseNT f >>= parseRHS . k
-  parseRHS (Or p q) = parseRHS p <|> parseRHS q
-  parseRHS Fail = empty
-
-  parseNT :: f x -> M f x
-  parseNT nt = addCont nt $
-    extents nt >>= \case
-      Nothing -> do
-        descend
-        x <- parseRHS (prods nt)
-        addExtent nt x
-        resume nt x
-      Just rs -> asum (map (\(r, x) -> x <$ skip r) rs)
-
-  parseT :: Char -> M f ()
-  parseT = match
-
-t :: Char -> RHS f ()
-t c = T c (pure ())
-
-nt :: f a -> RHS f a
-nt f = NT f pure
-
-data E a where E :: E Int
-
-deriving instance Eq (E a)
-deriving instance Ord (E a)
-instance GEq E where
-  geq E E = Just Refl
-instance GCompare E where
-  gcompare E E = GEQ
-deriving instance Show (E a)
-
-example :: CFG E Int
-example = CFG E $ \E -> nt E *> t '+' *> nt E <|> 0 <$ t 'a'
-
--- >>> parseCFG example "a+a+a+a+a+a"
--- (G {getG = Rel (fromList [(Comm "E" 0,[(Slot,0,<Cont>),(Slot,0,<Cont>)]),(Comm "E" 2,[(Slot,2,<Cont>),(Slot,0,<Cont>)]),(Comm "E" 4,[(Slot,2,<Cont>),(Slot,4,<Cont>),(Slot,0,<Cont>)]),(Comm "E" 6,[(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,4,<Cont>),(Slot,6,<Cont>),(Slot,0,<Cont>)]),(Comm "E" 8,[(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,4,<Cont>),(Slot,6,<Cont>),(Slot,8,<Cont>),(Slot,0,<Cont>)]),(Comm "E" 10,[(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,2,<Cont>),(Slot,0,<Cont>),(Slot,4,<Cont>),(Slot,0,<Cont>),(Slot,0,<Cont>),(Slot,4,<Cont>),(Slot,0,<Cont>),(Slot,6,<Cont>),(Slot,8,<Cont>),(Slot,10,<Cont>),(Slot,0,<Cont>)])])},P {getP = Rel (fromList [(Comm "E" 0,[11,11,11,11,9,11,11,11,11,9,11,11,11,9,7,11,11,9,11,11,11,11,9,11,11,9,7,5,11,11,11,9,11,11,11,9,7,11,11,9,11,11,11,11,9,11,11,11,9,7,11,11,9,11,11,11,9,11,11,11,9,7,5,3,1]),(Comm "E" 2,[11,11,11,11,9,11,11,11,9,11,11,9,7,11,11,11,9,11,11,9,7,5,3]),(Comm "E" 4,[11,11,11,9,11,11,9,7,5]),(Comm "E" 6,[11,11,9,7]),(Comm "E" 8,[11,9]),(Comm "E" 10,[11])])},True)
-
-data N a where N :: N Int
-deriving instance Eq (N a)
-deriving instance Ord (N a)
-deriving instance Show (N a)
-instance GEq N where
-  geq N N = Just Refl
-instance GCompare N where
-  gcompare N N = GEQ
-instance GShow N where
-  gshowsPrec _ N = showString "N"
-
-example3 :: CFG N Int
-example3 = CFG N $ \N -> (+ 1) <$ t 'a' <*> nt N <|> pure 0
-
-example4 :: CFG N Int
-example4 = CFG N $ \N -> (+ 1) <$> nt N <* t 'a' <|> pure 0
-
--- >>> parseCFG example3 (Text.pack "aaaa")
--- T3 (G {getG = Rel (fromList [(Comm (Some N) 0,[(Slot,0,Some <Cont>)]),(Comm (Some N) 1,[(Slot,0,Some <Cont>)]),(Comm (Some N) 2,[(Slot,1,Some <Cont>)]),(Comm (Some N) 3,[(Slot,2,Some <Cont>)]),(Comm (Some N) 4,[(Slot,3,Some <Cont>)])])})
---    (P {getP = Rel (fromList [(Comm (Some N) 0,[(0,Some <Identity>),(1,Some <Identity>),(2,Some <Identity>),(3,Some <Identity>),(4,Some <Identity>)]),(Comm (Some N) 1,[(1,Some <Identity>),(2,Some <Identity>),(3,Some <Identity>),(4,Some <Identity>)]),(Comm (Some N) 2,[(2,Some <Identity>),(3,Some <Identity>),(4,Some <Identity>)]),(Comm (Some N) 3,[(3,Some <Identity>),(4,Some <Identity>)]),(Comm (Some N) 4,[(4,Some <Identity>)])])})
---    (Just 4)
-
--- >>> parseCFG example4 (Text.pack "aaaa")
--- T3 (G {getG = Rel (fromList [(Comm (Some N) 0,[(Slot,0,Some <Cont>),(Slot,0,Some <Cont>)])])})
---    (P {getP = Rel (fromList [(Comm (Some N) 0,[(4,Some <Identity>),(3,Some <Identity>),(2,Some <Identity>),(1,Some <Identity>),(0,Some <Identity>)])])})
---    (Just 4)
-
-main :: IO ()
--- main = print (parseCFG example "a+a+a")
-
-main = do
-  result <-
-    fits $
-      mkFitConfig
-        (\n -> (\(T3 _ _ b) -> b) $ parseCFG example4 (Text.replicate (fromIntegral n) (Text.pack "a")))
-        (1000, 1000000)
-  mapM_ print result
diff --git a/gigaparsec.cabal b/gigaparsec.cabal
index 37e828d..1a30458 100644
--- a/gigaparsec.cabal
+++ b/gigaparsec.cabal
@@ -25,7 +25,7 @@ source-repository head
     location: https://github.com/noughtmare/gigaparsec
 
 common common
-    build-depends:    base >= 4.14 && <5
+    build-depends:    base >= 4.14 && <5, containers, text, some
     ghc-options:      -Wall
     default-language: GHC2021
 
@@ -33,7 +33,6 @@ library
     import:           common
     exposed-modules:  Gigaparsec, Gigaparsec.Core
     hs-source-dirs:   src
-    build-depends:    mtl, template-haskell
 
 executable gpc-examples
     import:           common
@@ -53,9 +52,9 @@ executable gpc-experiment1
     main-is:          Experiment1.hs
     hs-source-dirs:   experiments
 
-executable gpc-experiment2
+library gpc-experiment2
     import:           common
-    main-is:          Experiment2.hs
+    exposed-modules:  Experiment2
     hs-source-dirs:   experiments
     build-depends:    containers, some, mtl
 
@@ -65,8 +64,8 @@ executable gpc-experiment3
     hs-source-dirs:   experiments
     build-depends:    containers, some, mtl, tasty-bench-fit, deepseq, text
 
-executable gpc-experiment4
-    import:           common
-    main-is:          Experiment4.hs
-    hs-source-dirs:   experiments
-    build-depends:    containers, some, mtl, tasty-bench-fit, deepseq, text
+-- executable gpc-experiment4
+--     import:           common
+--     main-is:          Experiment4.hs
+--     hs-source-dirs:   experiments
+--     build-depends:    containers, some, mtl, tasty-bench-fit, deepseq, text
diff --git a/src/Gigaparsec/Core.hs b/src/Gigaparsec/Core.hs
index 5aac950..edb3a05 100644
--- a/src/Gigaparsec/Core.hs
+++ b/src/Gigaparsec/Core.hs
@@ -1,108 +1,210 @@
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# OPTIONS_GHC -Wall #-}
 
-module Gigaparsec.Core where
+module Gigaparsec.Core (CFG (CFG), RHS, Result, t, nt, parse, emptyk') where
 
-import Control.Monad.State
+import Data.Map.Strict (Map)
+-- import Data.Set (Set)
 import Control.Applicative
-import Data.Type.Equality ( type (:~:)(Refl) )
-import Data.Bifunctor (first)
-import Unsafe.Coerce ( unsafeCoerce )
-import qualified Debug.Trace
-import Language.Haskell.TH (Name)
-
-traceShow _ = id
-
-type Id a = Name
-newtype Parser a = Parser { alts :: [P a] } deriving Functor
-data P a = T Char (Parser a) | forall b. NT (Id b) (Parser b) (b -> Parser a) | Success a
-deriving instance Functor P
-
-char :: Char -> Parser ()
-char c = Parser [T c (pure ())]
-
-pattern (::=) :: Name -> Parser a -> Parser a
-pattern name ::= p <- (error "'::=' cannot be used in a pattern." -> (name, p)) where
-  (::=) = \name p -> Parser [NT name p (\x -> Parser [Success x])]
-infix 1 ::= -- tighter than $ but looser than <|>
-
-instance Applicative Parser where
-  pure x = Parser [Success x]
-  Parser ps <*> q0 = asum $ fmap (`seqP` q0) ps where
-    seqP (T c p) q = Parser [T c (p <*> q)]
-    seqP (NT n p p') q = Parser [NT n p (\x -> p' x <*> q)]
-    seqP (Success f) q = f <$> q
-
-instance Alternative Parser where
-  empty = Parser []
-  Parser ps <|> Parser qs = Parser (ps <> qs)
-
-instance Monad Parser where
-  Parser xs >>= k0 = Parser (xs >>= go (alts . k0)) where
-    go :: (a -> [P b]) -> P a -> [P b]
-    go k (Success x) = k x
-    go k (T c p) = [T c (Parser (concatMap (go k) (alts p)))]
-    go k (NT n p q) = [NT n p (Parser . concatMap (go k) . alts . q)]
-
-data SelfCont a = forall b. SelfCont (Stack b a) (a -> Parser b)
-
-data Stack a b where
-  SNil :: Stack a a
-  SCons :: Id a -> Int -> [SelfCont a] -> (a -> Parser b) -> Stack b c -> Stack a c
-
-eqId :: Id a -> Id b -> Maybe (a :~: b)
-eqId x y
-  | x == y = Just (unsafeCoerce Refl)
-  | otherwise = Nothing
-
-unwind :: forall a b c. Id b -> Int -> Stack a c -> Maybe (Stack a b, Stack b c)
-unwind _ _ SNil = Nothing
-unwind n i (SCons n' i' dcs k s) =
-  case eqId @a @b n n' of
-    Just Refl | i == i' -> Just (SNil, SCons n' i' dcs k s)
-    _ -> first (SCons n' i' dcs k) <$> unwind n i s
-
-appendStack :: Stack a b -> Stack b c -> Stack a c
-appendStack SNil x = x
-appendStack (SCons n i ks k stack') stack'' = SCons n i ks k (appendStack stack' stack'')
-
-update :: ([SelfCont a] -> [SelfCont a]) -> Stack a b -> Stack a b
-update f (SCons n i q q' s) = SCons n i (f q) q' s
-update _ SNil = error "Cannot update SNil"
-
-parse :: forall a. Parser a -> String -> [a]
-parse p0 xs0 = evalState (parse' 0 xs0 p0) SNil where
-  parse' :: Int -> String -> Parser b -> State (Stack b c) [c]
-  parse' i xs = fmap concat . traverse (go i xs) . alts
-
-  go :: forall b c. Int -> String -> P b -> State (Stack b c) [c]
-  go i (:){} (T c _) | traceShow ("t/match", c, i) False = undefined
-  go i (x:xs) (T c p) | x == c = parse' (i + 1) xs p
-  go i [] (T c _) | traceShow ("t/fail", c, i) False = undefined
-  go _ _ T{} = pure []
-
-  go i xs (NT n p p') = state $ \s -> 
-    -- Find out if the current (n, i) combination is already on the stack
-    case unwind n i s of
-      -- If not, push a new empty continuation on the initial stack (stack0) and continue running
-      Nothing | traceShow ("nt/nothing", n, i) False -> undefined
-      Nothing -> let (x, s') = runState (parse' i xs p) (SCons n i [] p' s) in (x, maybe undefined snd (unwind n i s'))
-      -- If so, add the p' as a new continuation, fail the current branch, and do update the stack
-      Just{} | traceShow ("nt/just", n, i) False -> undefined
-      Just (stack0, stack1) -> 
-        ([], appendStack stack0 (update (SelfCont stack0 p' :) stack1))
-
-  go i xs (Success x) = state $ \stack ->
-    case stack of
-      -- If there's something on the stack we can either:
-      -- use it to continue parsing, or ignore it and pop it from the stack
-      SCons{} | traceShow ("success/scons", i) False -> undefined
-      SCons _ _ ks p' stack' -> 
-        ( evalState (parse' i xs (p' x)) stack'
-          ++ concat [evalState (parse' i xs (p x)) (appendStack s stack) | SelfCont s p <- ks]
-        , stack)
-      -- If there's nothing on the stack then we succeed iff there is also no remaining input
-      SNil | traceShow ("success/snil", i) False -> undefined
-      SNil -> ([x | null xs], stack)
+import Control.Monad
+import Data.Map.Strict qualified as Map
+-- import GHC.Base (Any)
+import Debug.Trace
+import Data.Text qualified as Text
+import Data.Text (Text)
+
+import Data.Some
+import Data.GADT.Compare
+
+import Data.Functor.Identity
+import Data.Bifunctor
+import Unsafe.Coerce (unsafeCoerce)
+import Data.GADT.Show
+import Data.Type.Equality
+
+data RHS f a = Pure a | T Char (RHS f a) | forall x. NT (f x) (x -> RHS f a) | Or (RHS f a) (RHS f a) | Fail
+deriving instance Functor (RHS f)
+
+instance Applicative (RHS f) where
+  pure = Pure
+  (<*>) = ap
+
+instance Alternative (RHS f) where
+  (<|>) = Or
+  empty = Fail
+
+instance Monad (RHS f) where
+  Pure x >>= k = k x
+  T c k >>= k' = T c (k >>= k')
+  NT f k >>= k' = NT f (k >=> k')
+  Or p q >>= k = Or (p >>= k) (q >>= k)
+  Fail >>= _ = Fail
+
+data CFG f a = CFG (f a) (forall x. f x -> RHS f x)
+
+data T3 a b c = T3 !a !b !c deriving Show
+
+data Comm f = Comm !(Some f) !Int deriving (Eq, Ord, Show)
+
+newtype Cont f a = Cont { getCont :: Text -> Descr -> a -> Command f }
+-- instance Show (Cont f a) where
+--   show _ = "<Cont>"
+
+data Descr = Descr Slot !Int !Int
+data Slot = Slot -- String [Symbol] [Symbol]
+  deriving Show
+
+newtype Rel a b = Rel (Map a [b]) deriving Show
+
+rel :: Ord a => Rel a b -> a -> [b]
+rel (Rel m) x = Map.findWithDefault [] x m
+
+relMay :: Ord a => Rel a b -> a -> Maybe [b]
+relMay (Rel m) x = Map.lookup x m
+
+initRel :: Ord a => a -> Rel a b -> Rel a b
+initRel x (Rel m) = Rel (Map.insertWith (++) x [] m)
+
+addRel :: Ord a => a -> b -> Rel a b -> Rel a b
+addRel x y (Rel m) = Rel (Map.insertWith (++) x [y] m)
+
+relSize :: Rel a b -> Int
+relSize (Rel m) = Map.size m
+
+-- instance GShow Identity where
+--   gshowsPrec _ _ = showString "<Identity>"
+-- instance GShow (Cont f) where
+--   gshowsPrec _ _ = showString "<Cont>"
+
+-- newtype U = U (Set Descr)
+newtype G f = G { getG :: Rel (Comm f) (Slot, Int, Some (Cont f)) } -- deriving Show
+newtype P f = P { getP :: Rel (Comm f) (Int, Some Identity) } -- deriving Show
+
+newtype Command f = Command { getCommand :: forall x. T3 (G f) (P f) (Result x) -> T3 (G f) (P f) (Result x) }
+
+newtype M f a = M { getM :: Text -> Descr -> Cont f a -> Command f }
+
+extents :: (GCompare f) => f a -> M f (Maybe [(Int, a)])
+extents nt = M $ \inp dsc@(Descr _ _ i) (Cont k) ->
+  Command $ \(T3 g p b) -> trace ("extents " ++ show i) $
+  getCommand
+    (k inp dsc (
+      let res = relMay (getP p) (Comm (Some nt) i)
+      in fmap (map (second (\(Some (Identity x)) -> unsafeCoerce x))) res))
+    (T3 g (P (initRel (Comm (Some nt) i) (getP p))) b)
+
+addExtent :: GCompare f => f a -> a -> M f ()
+addExtent nt x = M $ \inp dsc@(Descr _ l i) (Cont k) ->
+  Command $ \(T3 g p b) -> -- trace ("addExtent " ++ show (nt, l, i)) $
+  getCommand (k inp dsc ()) (T3 g (P (addRel (Comm (Some nt) l) (i, Some (Identity x)) (getP p))) b)
+
+resume :: GCompare f => f a -> a -> M f a
+resume nt x = M $ \inp (Descr Slot l r) _ ->
+  Command $ \(T3 g p b) -> 
+    -- if l == r then trace ("resume " ++ show (l, r)) $ T3 g p b else
+    let cnts = rel (getG g) (Comm (Some nt) l) in
+    foldr (\(s, l', Some (Cont k)) go -> go . getCommand (unsafeCoerce k inp (Descr s l' r) x))
+      id cnts (T3 g p b)
+
+addCont :: GCompare f => f a -> M f c -> M f c
+addCont nt m = M $ \inp dsc@(Descr s l i) k ->
+  Command $ \(T3 g p b) -> -- trace ("addCont " ++ show (nt, i)) $
+    getCommand (getM m inp dsc k) (T3 (G (addRel (Comm (Some nt) i) (s, l, Some k) (getG g))) p b)
+
+match :: Char -> M f ()
+match c = M $ \inp (Descr (Slot {- nt alpha beta -}) l i) (Cont k) ->
+  case Text.uncons inp of
+    Just (x,inp') | c == x -> k inp' (Descr (Slot {- nt alpha beta -}) l (i + 1)) ()
+    _ -> Command id
+
+skip :: Int -> M f ()
+skip r = M $ \inp (Descr s l i) (Cont k) -> k (Text.drop (r - i) inp) (Descr s l r) ()
+
+descend :: M f ()
+descend = M $ \inp (Descr Slot _ i) (Cont k) -> k inp (Descr Slot i i) ()
+
+traceI :: String -> M f ()
+traceI msg = M $ \inp dsc@(Descr _ _ i) k -> trace (show i ++ ": " ++ msg) getCont k inp dsc ()
+
+instance Functor (M f) where
+  fmap f (M p) = M $ \inp dsc (Cont k) ->
+    p inp dsc $ Cont $ \inp' dsc' x ->
+      k inp' dsc' (f x)
+instance Applicative (M f) where
+  pure x = M $ \inp dsc (Cont k) -> k inp dsc x
+  (<*>) = ap
+instance Alternative (M f) where
+  empty = M $ \_ _ _ -> Command id
+  M p <|> M q = M $ \inp dsc k -> Command (getCommand (q inp dsc k) . getCommand (p inp dsc k))
+instance Monad (M f) where
+  M p >>= k = M $ \inp dsc k' ->
+    p inp dsc $ Cont $ \inp' dsc' x ->
+      getM (k x) inp' dsc' k'
+
+-- must have Alternative instance
+type Result = []
+
+parse :: forall f a. GCompare f => CFG f a -> Text -> Result a
+parse (CFG nt0 prods) inp0 = res where
+
+  T3 _ _ res =
+    getCommand
+      (getM (parseRHS (NT nt0 pure)) inp0 (Descr Slot 0 0) finish)
+      (T3 (G (Rel mempty)) (P (Rel mempty)) empty)
+
+  finish :: Cont f a
+  finish = Cont $ \inp _ x -> Command $ \(T3 p g b) -> (T3 p g (b <|> unsafeCoerce x <$ guard (Text.null inp)))
+
+  parseRHS :: RHS f x -> M f x
+  parseRHS (Pure x) = pure x
+  parseRHS (T c k) = parseT c *> parseRHS k
+  parseRHS (NT f k) = parseNT f >>= parseRHS . k
+  parseRHS (Or p q) = parseRHS p <|> parseRHS q
+  parseRHS Fail = empty
+
+  parseNT :: f x -> M f x
+  parseNT nt = 
+    -- if we ever finish parsing nt then resume after this point
+    addCont nt $
+      -- check if we have already finished parsing this
+      extents nt >>= \case
+        -- if not,
+        Nothing -> do
+          traceI "Nothing"
+          -- descend into nt
+          descend
+          traceI "Nothing descend"
+          -- parse its right hand side
+          x <- parseRHS (prods nt)
+          traceI "Nothing parseRHS"
+          -- remember that we've parsed it (and to what point int the input)
+          addExtent nt x
+          error "Nothing addExtent"
+          -- resume parsing the stored continuations
+          x' <- resume nt x
+          traceI "Nothing resume"
+          pure x'
+        -- if so,
+        Just rs -> do
+          traceI "Just"
+          -- for all successes, skip forward and continue parsing
+          asum (map (\(r, x) -> x <$ skip r) rs)
+
+  parseT :: Char -> M f ()
+  parseT = match
+
+t :: Char -> RHS f ()
+t c = T c (pure ())
+
+nt :: f a -> RHS f a
+nt f = NT f pure
+
+data E a where E :: E ()
+deriving instance Eq (E a)
+deriving instance Ord (E a)
+instance GEq E where geq E E = Just Refl
+instance GCompare E where gcompare E E = GEQ
+
+emptyk' :: CFG E ()
+emptyk' = CFG E $ \E -> nt E <|> pure ()
diff --git a/tests/test.hs b/tests/test.hs
index 1b568aa..cb80a19 100644
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -1,4 +1,7 @@
 {-# LANGUAGE TemplateHaskellQuotes #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
 import Test.Tasty
 -- import Test.Tasty.SmallCheck as SC
 -- import Test.Tasty.QuickCheck as QC
@@ -8,44 +11,102 @@ import Gigaparsec
 import Data.Foldable (traverse_)
 import Control.Applicative (Alternative((<|>)), asum)
 import Data.Char (intToDigit)
+import Data.GADT.Compare
+import Data.Type.Equality
+import Data.List (sort)
 
 main :: IO ()
 main = defaultMain tests
 
-digit :: Int -> Parser Int
-digit b = asum [i <$ char (intToDigit i) | i <- [0..b - 1]]
+data E a where
+  E :: E Int
+  N :: Int -> E Int
+  D :: Int -> E Int
+  NDots :: E ()
+  NDotsGo :: Int -> E ()
+deriving instance Eq (E a)
+deriving instance Ord (E a)
+instance GEq E where
+  geq E E = Just Refl
+  geq (N x) (N y) | x == y = Just Refl
+  geq (D x) (D y) | x == y = Just Refl
+  geq NDots NDots = Just Refl
+  geq (NDotsGo x) (NDotsGo y) | x == y = Just Refl
+  geq _ _ = Nothing
+instance GCompare E where
+  gcompare E E = GEQ
+  gcompare (N x) (N y) =
+    case compare x y of
+      LT -> GLT
+      EQ -> GEQ
+      GT -> GGT
+  gcompare (D x) (D y) =
+    case compare x y of
+      LT -> GLT
+      EQ -> GEQ
+      GT -> GGT
+  gcompare NDots NDots = GEQ
+  gcompare (NDotsGo x) (NDotsGo y) =
+    case compare x y of
+      LT -> GLT
+      EQ -> GEQ
+      GT -> GGT
+  gcompare E _ = GLT
+  gcompare _ E = GGT
+  gcompare N{} _ = GLT
+  gcompare _ N{} = GGT
+  gcompare D{} _ = GLT
+  gcompare _ D{} = GGT
+  gcompare NDots _ = GLT
+  gcompare _ NDots = GGT
 
-number :: Int -> Parser Int
-number b = 'number
-  ::= (\x y -> b * x + y) <$> number b <*> digit b
-  <|> digit b
+digit :: Int -> RHS E Int
+digit b = asum [i <$ t (intToDigit i) | i <- [0..b - 1]]
 
-expr :: Parser Int
-expr = 'expr
-  ::= (*) <$> expr <* char '*' <*> expr
-  <|> (+) <$> expr <* char '+' <*> expr 
+number :: Int -> RHS E Int
+number b = (\x y -> b * x + y) <$> nt (N b) <*> nt (D b)
+  <|> nt (D b)
+
+expr :: RHS E Int
+expr = (*) <$> nt E <* t '*' <*> nt E
+  <|> (+) <$> nt E <* t '+' <*> nt E 
   <|> number 10
 
-expr2 :: Parser Int
-expr2 = 'expr2
-  ::= number 10
-  <|> (+) <$> expr2 <* char '+' <*> expr2
+expr2 :: RHS E Int
+expr2 = nt (N 10)
+  <|> (+) <$> nt E <* t '+' <*> nt E
+
+ndots :: RHS E ()
+ndots = nt (N 10) >>= nt . NDotsGo
+
+ndotsGo :: Int -> RHS E ()
+ndotsGo 0 = pure ()
+ndotsGo n = t '.' *> nt (NDotsGo (n - 1))
+
+mkE :: E a -> CFG E a
+mkE = mkE' False
+
+mkE2 :: E a -> CFG E a
+mkE2 = mkE' True
 
-ndots :: Parser ()
-ndots = number 10 >>= go where
-  go 0 = pure ()
-  go n = char '.' *> go (n - 1)
+mkE' :: Bool -> E a -> CFG E a
+mkE' e2 e = CFG e $ \case
+  E -> if e2 then expr2 else expr
+  N b -> number b
+  D b -> digit b
+  NDots -> ndots
+  NDotsGo n -> ndotsGo n
 
 tests :: TestTree
 tests = testGroup "Tests" [unitTests]
 
-emptyk :: Parser ()
-emptyk = 'emptyk ::= emptyk <|> pure ()
+emptyk :: CFG E Int
+emptyk = CFG E $ \E -> nt E <|> pure 0
 
 unitTests :: TestTree
 unitTests = testGroup "Unit tests"
   [ testCase "base 2 number positive" $
-    traverse_ (\(x, y) -> parse (number 2) x @?= [y])
+    traverse_ (\(x, y) -> parse (mkE (N 2)) x @?= [y])
       [ ("0",     0)
       , ("1",     1)
       , ("00",    0)
@@ -56,7 +117,7 @@ unitTests = testGroup "Unit tests"
       , ("11111", 31)
       ]
   , testCase "base 2 number negative" $
-    traverse_ (\x -> parse (number 2) x @?= [])
+    traverse_ (\x -> parse (mkE (N 2)) x @?= [])
       [ ""
       , "X"
       , "01X00"
@@ -64,25 +125,25 @@ unitTests = testGroup "Unit tests"
       , "X1101"
       ]
   , testCase "expression positive" $
-    traverse_ (\(x, y) -> parse expr x @?= y)
+    traverse_ (\(x, y) -> sort (parse (mkE E) x) @?= y)
       [ ("1+1", [2])
       , ("1+2+3", [6,6])
-      , ("1+2*3", [9,7])
+      , ("1+2*3", [7,9])
       ]
   , testCase "expr2 positive" $
-    traverse_ (\(x, y) -> parse expr2 x @?= y)
+    traverse_ (\(x, y) -> parse (mkE2 E) x @?= y)
       [ ("1+2", [3])
       , ("1+2+3", [6,6])
-      , ("1+2+3+4", [10,10,10,10])
+      , ("1+2+3+4", [10,10,10,10,10])
       ]
   , testCase "ndots positive" $
-    traverse_ (\x -> parse ndots x @?= [()])
+    traverse_ (\x -> parse (mkE NDots) x @?= [()])
       [ "5....."
       , "3..."
       , "10.........."
       ]
   , testCase "ndots negative" $
-    traverse_ (\x -> parse ndots x @?= [])
+    traverse_ (\x -> parse (mkE NDots) x @?= [])
       [ "5...."
       , "5......"
       , "3....."
@@ -90,5 +151,5 @@ unitTests = testGroup "Unit tests"
       ]
   , localOption (Timeout 1000000 "1s") $
     testCase "emptyk positive" $ 
-      parse emptyk "" @?= [()]
+      parse emptyk "" @?= [0]
   ]