Skip to content

Instantly share code, notes, and snippets.

@noughtmare

noughtmare/Gram5.hs

Last active August 18, 2024 09:59
Show Gist options
  • Save noughtmare/e02da0ae9dba74acf0f57cfc73ee1d3b to your computer and use it in GitHub Desktop.
Save noughtmare/e02da0ae9dba74acf0f57cfc73ee1d3b to your computer and use it in GitHub Desktop.
Download ZIP
Data dependent parsing with explicit variables
Raw
Gram5.hs
{- cabal:
build-depends: base, recover-rtti, tasty-bench, tasty-bench-fit
-}
{-# LANGUAGE GHC2021, GADTs, DataKinds, LambdaCase, TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
-- DATA-DEPENDENT PARSING WITH VARIABLES
import Prelude hiding (Monad (..))
import Data.Char (intToDigit)
import Data.Kind (Type)
-- import Debug.RecoverRTTI
-- import Test.Tasty.Bench.Fit
-- import Test.Tasty.Bench
import Data.Type.Equality
import Data.Bifunctor
type Var :: [k] -> k -> Type
data Var ctx a where
Here :: Var (a : ctx) a
There :: Var ctx a -> Var (b : ctx) a
deriving instance Show (Var ctx a)
type Exp :: [Type] -> Type -> Type
data Exp ctx a where
ENil :: a -> Exp ctx a
ECons :: forall ctx a x. Var ctx x -> Exp ctx (x -> a) -> Exp ctx a
deriving instance Functor (Exp ctx)
instance Applicative (Exp ctx) where
pure = ENil
ENil f <*> x = fmap f x
ECons x xs <*> y = ECons x (flip <$> xs <*> y)
ehere :: Exp (x : vs) x
ehere = ECons Here (ENil id)
ethere :: Exp vs a -> Exp (x : vs) a
ethere (ENil x) = ENil x
ethere (ECons v x) = ECons (There v) (ethere x)
instance Show (Exp ctx a) where
-- show (ENil x) = "ENil (" ++ anythingToString x ++ ")"
show ENil{} = "ENil{}"
show (ECons v xs) = "ECons (" ++ show v ++ ") (" ++ show xs ++ ")"
type CFG :: [(Type,Type)] -> [Type] -> Type -> Type
data CFG nts vs a where
Fail :: CFG nts vs a
Or :: CFG nts vs a -> CFG nts vs a -> CFG nts vs a
Done :: Exp vs a -> CFG nts vs a
Seq :: CFG nts vs a -> (CFG nts (a : vs) b) -> CFG nts vs b
Char :: Char -> CFG nts vs ()
Var :: Var nts '(x, a) -> Exp vs x -> CFG nts vs a
Fix :: CFG ('(x,a):nts) (x:vs) a -> Exp vs x -> CFG nts vs a
Guard :: Exp vs Bool -> CFG nts vs ()
Let :: CFG nts (x : vs) y -> CFG ('(x,y):nts) vs a -> CFG nts vs a
data Thin xs ys where
EndDrop :: Thin xs '[]
EndId :: Thin xs xs
Keep :: Thin xs ys -> Thin (x : xs) (x : ys)
Drop :: Thin xs ys -> Thin (x : xs) ys
data CombineThin xs ys zs = forall xs'. CombineThin (Thin xs xs') (Thin xs' ys) (Thin xs' zs)
combineThin :: Thin xs ys -> Thin xs zs -> CombineThin xs ys zs
combineThin EndDrop t = CombineThin t EndDrop EndId
combineThin t EndDrop = CombineThin t EndId EndDrop
combineThin EndId t = CombineThin EndId EndId t
combineThin t EndId = CombineThin EndId t EndId
combineThin (Keep t) (Keep t') =
case combineThin t t' of
CombineThin x y z -> CombineThin (Keep x) (Keep y) (Keep z)
combineThin (Keep t) (Drop t') =
case combineThin t t' of
CombineThin x y z -> CombineThin (Keep x) (Keep y) (Drop z)
combineThin (Drop t) (Keep t') =
case combineThin t t' of
CombineThin x y z -> CombineThin (Keep x) (Drop y) (Keep z)
combineThin (Drop t) (Drop t') =
case combineThin t t' of
CombineThin x y z -> CombineThin (Drop x) y z
data Unused nts vs a = forall nts'. Unused (CFG nts' vs a) (Thin nts nts')
combine
:: (forall nts'. CFG nts' vsa a -> CFG nts' vsb b -> CFG nts' vsc c)
-> Unused nts vsa a -> Unused nts vsb b -> Unused nts vsc c
combine f (Unused x t) (Unused y t') =
case combineThin t t' of
CombineThin tt tx ty -> Unused (f (wkNts (apThin tx) x) (wkNts (apThin ty) y)) tt
varToThin :: Var nts a -> Thin nts '[a]
varToThin Here = Keep EndDrop
varToThin (There v) = Drop (varToThin v)
unused :: CFG nts vs a -> Unused nts vs a
unused Fail = Unused Fail EndDrop
unused (Or x y) = combine Or (unused x) (unused y)
unused (Done x) = Unused (Done x) EndDrop
unused (Seq x y) = combine Seq (unused x) (unused y)
unused (Char c) = Unused (Char c) EndDrop
unused (Var v e) = Unused (Var Here e) (varToThin v)
unused (Guard e) = Unused (Guard e) EndDrop
unused (Fix p e) =
case unused p of
Unused p' EndDrop -> Unused (Fix (wkNts There p') e) EndDrop
Unused p' EndId -> Unused (Fix p' e) EndId
Unused p' (Drop t) -> Unused (Fix (wkNts There p') e) t
Unused p' (Keep t) -> Unused (Fix p' e) t
unused (Let p q) =
case (unused p, unused q) of
(Unused p' tp, Unused q' EndDrop) -> Unused (Let p' (wkNts (\case) q')) tp
(Unused p' tp, Unused q' EndId) -> Unused (Let (wkNts (apThin tp) p') q') EndId
(Unused p' tp, Unused q' (Drop tq)) ->
case combineThin tp tq of
CombineThin tt tp' tq' ->
Unused
(Let
(wkNts (apThin tp') p')
(wkNts (There . apThin tq') q'))
tt
(Unused p' tp, Unused q' (Keep tq)) ->
case combineThin tp tq of
CombineThin tt tp' tq' ->
Unused
(Let
(wkNts (apThin tp') p')
(wkNts (\case Here -> Here; There v -> There $ apThin tq' v) q'))
tt
eqVar :: Var vs a -> Var vs b -> Maybe (a :~: b)
eqVar Here Here = Just Refl
eqVar (There v) (There w) = eqVar v w
eqVar _ _ = Nothing
-- this optimization improves dotsl
simplifyE :: Exp vs a -> Exp vs a
simplifyE (ECons v (ECons w xs)) | Just Refl <- eqVar v w = ECons v (fmap (\f x -> f x x) xs)
simplifyE x = x
apThin :: Thin xs ys -> Var ys a -> Var xs a
apThin EndDrop x = case x of {}
apThin EndId x = x
apThin (Drop t) x = There (apThin t x)
apThin (Keep t) (There x) = There (apThin t x)
apThin (Keep _) Here = Here
simplify :: CFG nts vs a -> CFG nts vs a
simplify (Seq a b) =
case (simplify a, simplify b) of
(Fail, _) -> Fail
(_, Fail) -> Fail
(Done x, y) -> apEG y x
(a', b') -> Seq a' b'
simplify (Or a b) =
case (simplify a, simplify b) of
(Fail, x) -> x
(x, Fail) -> x
(a', b') -> Or a' b'
simplify (Fix x e) =
-- this optimization improves dotsr
case unused x of
Unused x' EndDrop -> apEG (wkNts (\case) (simplify x')) (simplifyE e)
Unused x' (Drop t) -> apEG (wkNts (apThin t) (simplify x')) (simplifyE e)
_ -> Fix (simplify x) (simplifyE e)
simplify (Guard e) = case simplifyE e of
ENil b -> if b then Done (ENil ()) else Fail
e' -> Guard e'
simplify (Done e) = Done (simplifyE e)
-- simplify (Let (Let p q) r) = Let p (Let (_ q) (_ r))
simplify (Let p q) =
case unused (simplify q) of
Unused q' EndDrop -> wkNts (\case) q'
Unused q' (Drop t) -> wkNts (apThin t) q'
_ -> Let (simplify p) (simplify q)
simplify (Char c) = Char c
simplify Fail = Fail
simplify (Var v e) = Var v (simplifyE e)
instance Show (CFG nts vs a) where
show Fail = "Fail"
show (Or x y) = "Or (" ++ show x ++ ") (" ++ show y ++ ")"
show (Done e) = "Done (" ++ show e ++ ")"
show (Seq x y) = "Seq (" ++ show x ++ ") (" ++ show y ++ ")"
show (Char c) = "Char " ++ show c
show (Fix p e) = "Fix (" ++ show p ++ ") (" ++ show e ++ ")"
show (Var v e) = "Var (" ++ show v ++ ") (" ++ show e ++ ")"
show (Guard e) = "Guard (" ++ show e ++ ")"
show (Let p q) = "Let (" ++ show p ++ ") (" ++ show q ++ ")"
substE :: (forall x. Var vs x -> Exp vs' x) -> Exp vs a -> Exp vs' a
substE _ (ENil x) = ENil x
substE f (ECons v xs) = substE f xs <*> f v
substVs :: (forall x. Var vs x -> Exp vs' x) -> CFG nts vs a -> CFG nts vs' a
substVs _ Fail = Fail
substVs f (Or p q) = Or (substVs f p) (substVs f q)
substVs f (Done x) = Done (substE f x)
substVs f (Seq p q) = Seq (substVs f p) (substVs (\case Here -> ECons Here (ENil id); There v -> wkE There $ f v) q)
substVs _ (Char c) = Char c
substVs f (Var v e) = Var v (substE f e)
substVs f (Fix p e) = Fix (substVs (\case Here -> ECons Here (ENil id); There v -> wkE There (f v)) p) (substE f e)
substVs f (Guard e) = Guard (substE f e)
substVs f (Let p q) = Let (substVs (\case Here -> ehere; There v -> ethere (f v)) p) (substVs f q)
wkVs :: (forall x. Var vs x -> Var vs' x) -> CFG nts vs a -> CFG nts vs' a
wkVs f = substVs (\v -> ECons (f v) (ENil id))
substNts :: (forall x y. Var nts '(x,y) -> CFG nts' (x:vs) y) -> CFG nts vs a -> CFG nts' vs a
substNts _ Fail = Fail
substNts f (Or p q) = Or (substNts f p) (substNts f q)
substNts _ (Done x) = Done x
substNts f (Seq p q) = Seq (substNts f p) (substNts (wkVs (\case Here -> Here; There v -> There (There v)) . f) q)
substNts _ (Char c) = Char c
substNts f (Var v e) = apEG (f v) e
substNts f (Fix p e) = Fix (substNts (\case Here -> Var Here (ECons Here (ENil id)); There v -> wkNts There $ wkVs (\case Here -> Here; There v' -> There (There v')) $ f v) p) e
substNts _ (Guard e) = Guard e
substNts f (Let p q) = Let (substNts (wkVs (\case Here -> Here; There v -> There (There v)) . f) p) (substNts (\case Here -> Var Here ehere; There v -> wkNts There (f v)) q)
wkNts :: (forall x y. Var nts '(x,y) -> Var nts' '(x,y)) -> CFG nts vs a -> CFG nts' vs a
wkNts f = substNts ((\v -> Var v (ECons Here (ENil id))) . f)
apEE :: Exp (a : vs) b -> Exp vs a -> Exp vs b
apEE (ENil x) _ = ENil x
apEE (ECons Here xs) e = flip ($) <$> e <*> apEE xs e
apEE (ECons (There v) xs) e = ECons v (apEE xs e)
apEG :: CFG nts (a : vs) b -> Exp vs a -> CFG nts vs b
apEG p e = substVs (\case Here -> e; There v -> ECons v (ENil id)) p
both :: (a -> b) -> (a, a) -> (b, b)
both f (x, y) = (f x, f y)
both1 :: (forall x. f x -> g x) -> (f a, f b) -> (g a, g b)
both1 f (x, y) = (f x, f y)
wkE :: (forall x. Var vs x -> Var vs' x) -> Exp vs a -> Exp vs' a
wkE _ (ENil x) = ENil x
wkE f (ECons v xs) = ECons (f v) (wkE f xs)
nullable :: (forall x y. Var nts '(x, y) -> [(Exp (x:vs) Bool, Exp (x:vs) y)]) -> CFG nts vs a -> [(Exp vs Bool, Exp vs a)]
nullable _ Fail = []
nullable ev (Or p q) = nullable ev p ++ nullable ev q
nullable _ (Done x) = [(ENil True, x)]
nullable ev (Seq p q) = do
(xg,xe) <- nullable ev p
(yg,ye) <- nullable ev (apEG q xe)
pure (liftA2 (&&) xg yg, ye)
nullable _ (Char _) = []
nullable _ (Guard e) = [(e, ENil ())]
nullable ev (Var v e) = map (\(x,y) -> (apEE x e, apEE y e)) (ev v)
nullable ev (Fix x e) = map (both1 (`apEE` e)) $ nullable (\case Here -> []; There v -> map (both1 (wkE (\case Here -> Here; There v' -> There (There v')))) $ ev v) x
nullable ev (Let p q) =
let x = nullable (map (both1 (wkE (\case Here -> Here; There v -> There (There v)))) . ev) p
in nullable (\case Here -> x; There v -> ev v) q
nullable0 :: CFG '[] '[] a -> [a]
nullable0 x = do
(ENil b, ENil xe) <- nullable (\case) x
[xe | b]
derivative :: CFG nts vs a
-> (forall x y. Var nts '(x,y) -> ([(Exp (x:vs) Bool, Exp (x:vs) y)],Var nts '(x,y)))
-> Char -> CFG nts vs a
-- derivative cfg _ c | traceShow ("derivative", cfg, c) False = undefined
derivative Fail _ _ = Fail
derivative (Or p q) nts c = Or (derivative p nts c) (derivative q nts c)
derivative (Done _) _ _ = Fail
derivative (Seq p q) nts c = Or
(foldr Or Fail [Seq (Guard xg) (wkVs There $ derivative (apEG q xe) nts c) | (xg,xe) <- nullable (fst . nts) p])
(Seq (derivative p nts c) q)
derivative (Char c') _ c = if c == c' then Done (ENil ()) else Fail
derivative (Var v x) nts _ = Var (snd (nts v)) x
derivative (Fix @x p x) nts c =
Let
(Fix (wkVs (\case Here -> Here; There v -> There (There v)) p) (ECons Here (ENil id)))
-- substNts (\case Here -> Fix (wkVs (\case Here -> Here; There v -> There (There v)) p) (ECons Here (ENil id)); There v -> Var v ehere) $
(Fix
(derivative
(wkNts There p)
(\case
Here -> error "impossible"
There Here ->
(nullable (map (both1 (wkE (\case Here -> Here; There v -> There (There (There v))))) . fst . nts) (Fix (wkVs (\case Here -> Here; There v -> There (There (There v))) p) (ECons Here (ENil id)))
, Here
)
There (There v) -> let (a,b) = nts v in (map (both1 (wkE (\case Here -> Here; There v' -> There (There v')))) a, There (There b))
)
c)
x)
derivative (Guard _) _ _ = Fail
derivative (Let p q) nts c =
Let p $
Let
(wkNts There $ derivative
p
(first (map (both1 (wkE (\case
Here -> Here
There v -> There (There v))))) . nts)
c) $
derivative
(wkNts There q)
(\case
Here -> error "impossible"
There Here ->
(nullable (map (both1 (wkE (\case
Here -> Here
There v -> There (There v)))) . fst . nts) p
,Here)
There (There v) -> fmap (There . There) (nts v))
c
derivative0 :: CFG '[] '[] a -> Char -> CFG '[] '[] a
derivative0 g = derivative g (\case)
parse :: CFG '[] '[] a -> String -> [a]
parse s [] = nullable0 s
parse s (x:xs) = parse (simplify (derivative0 s x)) xs
digit :: CFG nts vs Int
digit = foldr Or Fail [Seq (Char (intToDigit x)) (Done (ENil x)) | x <- [0..9]]
dotsr :: Int -> CFG nts vs ()
dotsr n = Fix (Or
(Seq (Char '.') (Var Here (ECons (There Here) (ENil (subtract 1)))))
(Guard (ECons Here (ENil (== 0))))
) (ENil n)
dotsl :: Int -> CFG nts vs ()
dotsl n = Fix (Or
(Seq (Guard (ECons Here (ENil (> 0)))) (Seq (Var Here (ECons (There Here) (ENil (subtract 1)))) (Char '.')))
(Guard (ECons Here (ENil (== 0))))
) (ENil n)
data X = X | Add X X deriving Show
type (<=) :: forall k. [k] -> [k] -> Type
type vs <= vs' = forall x. Var vs x -> Var vs' x
fix :: (forall nts' vs'. nts <= nts' -> Var nts' '(x,a) -> vs <= vs' -> Var vs' x -> CFG nts' vs' a) -> Exp vs x -> CFG nts vs a
fix f = Fix (f There Here There Here)
infixr 4 >>=
(>>=) :: CFG nts vs a -> (forall vs'. vs <= vs' -> Var vs' a -> CFG nts vs' b) -> CFG nts vs b
m >>= k = Seq m (k There Here)
return :: Var vs a -> CFG nts vs a
return v = Done (ECons v (ENil id))
evar :: Var vs a -> Exp vs a
evar v = ECons v (ENil id)
infixr 4 >>
(>>) :: CFG nts vs a -> CFG nts vs b -> CFG nts vs b
m >> k = Seq m (wkVs There k)
infixr 3 <|>
(<|>) :: CFG nts vs a -> CFG nts vs a -> CFG nts vs a
(<|>) = Or
ex :: CFG nts vs X
ex = fix (\_ p _ b -> Char 'x' >>
Done (pure X)
<|> Guard (evar b) >>
Var p (pure False) >>= \_ x ->
Char '+' >>
Var p (pure True) >>= \e y ->
Done (Add <$> evar (e x) <*> evar y))
(pure True)
-- main :: IO ()
-- main = defaultMain $
-- [ bench (show k) $ nf (\n -> parse (dotsr n) (replicate n '.')) k
-- | k <- [10,20..80]
-- ]
-- main = do
-- putStrLn "Start"
-- mapM_ print =<< fits (mkFitConfig (\n -> parse (dotsl (fromIntegral n)) (replicate (fromIntegral n) '.')) (10, 100))
@noughtmare
Copy link
Author

noughtmare commented Aug 17, 2024 •
edited
Loading

These are the pretty printed steps of parsing the ex grammar on the string "x+x+...":

Fix
   (Or
      (Seq (Char 'x') (Done (ENil (X))))
      (Seq
         (Guard (ECons (Here) (ENil (<Fun>))))
         (Seq
            (Var (Here) (ENil (False)))
            (Seq
               (Char '+')
               (Seq
                  (Var (Here) (ENil (True)))
                  (Done
                     (ECons
                        (There (There Here))
                        (ECons (Here) (ENil (<Fun>))))))))))
   (ENil (True))

 Let
   (Fix
      (Or
         (Seq (Char 'x') (Done (ENil (X))))
         (Seq
            (Guard (ECons (Here) (ENil (<Fun>))))
            (Seq
               (Var (Here) (ENil (False)))
               (Seq
                  (Char '+')
                  (Seq
                     (Var (Here) (ENil (True)))
                     (Done
                        (ECons
                           (Here)
                           (ECons (There (There Here)) (ENil (<Fun>))))))))))
      (ECons (Here) (ENil (<Fun>))))
   (Fix
      (Or
         (Done (ENil (X)))
         (Seq
            (Guard (ECons (Here) (ENil (<Fun>))))
            (Seq
               (Var (Here) (ENil (False)))
               (Seq
                  (Char '+')
                  (Seq
                     (Var (There Here) (ENil (True)))
                     (Done
                        (ECons
                           (There (There Here))
                           (ECons (Here) (ENil (<Fun>))))))))))
      (ENil (True)))

 Let
   (Fix
      (Or
         (Seq (Char 'x') (Done (ENil (X))))
         (Seq
            (Guard (ECons (Here) (ENil (<Fun>))))
            (Seq
               (Var (Here) (ENil (False)))
               (Seq
                  (Char '+')
                  (Seq
                     (Var (Here) (ENil (True)))
                     (Done
                        (ECons
                           (Here)
                           (ECons (There (There Here)) (ENil (<Fun>))))))))))
      (ECons (Here) (ENil (<Fun>))))
   (Fix
      (Seq
         (Guard (ECons (Here) (ENil (<Fun>))))
         (Or
            (Seq
               (Var (There Here) (ENil (True)))
               (Done (ECons (Here) (ENil (<Fun>)))))
            (Seq
               (Var (Here) (ENil (False)))
               (Seq
                  (Char '+')
                  (Seq
                     (Var (There Here) (ENil (True)))
                     (Done
                        (ECons
                           (There (There Here))
                           (ECons (Here) (ENil (<Fun>))))))))))
      (ENil (True)))

 Let
   (Fix
      (Or
         (Seq (Char 'x') (Done (ENil (X))))
         (Seq
            (Guard (ECons (Here) (ENil (<Fun>))))
            (Seq
               (Var (Here) (ENil (False)))
               (Seq
                  (Char '+')
                  (Seq
                     (Var (Here) (ENil (True)))
                     (Done
                        (ECons
                           (Here)
                           (ECons (There (There Here)) (ENil (<Fun>))))))))))
      (ECons (Here) (ENil (<Fun>))))
   (Let
      (Let
         (Fix
            (Or
               (Seq (Char 'x') (Done (ENil (X))))
               (Seq
                  (Guard (ECons (Here) (ENil (<Fun>))))
                  (Seq
                     (Var (Here) (ENil (False)))
                     (Seq
                        (Char '+')
                        (Seq
                           (Var (Here) (ENil (True)))
                           (Done
                              (ECons
                                 (There (There Here))
                                 (ECons (Here) (ENil (<Fun>))))))))))
            (ECons (Here) (ENil (<Fun>))))
         (Fix
            (Or
               (Done (ENil (X)))
               (Seq
                  (Guard (ECons (Here) (ENil (<Fun>))))
                  (Seq
                     (Var (Here) (ENil (False)))
                     (Seq
                        (Char '+')
                        (Seq
                           (Var (There Here) (ENil (True)))
                           (Done
                              (ECons
                                 (Here)
                                 (ECons
                                    (There (There Here)) (ENil (<Fun>))))))))))
            (ECons (Here) (ENil (<Fun>)))))
      (Fix
         (Seq
            (Guard (ECons (Here) (ENil (<Fun>))))
            (Or
               (Seq
                  (Var (There Here) (ENil (True)))
                  (Done (ECons (Here) (ENil (<Fun>)))))
               (Seq
                  (Var (Here) (ENil (False)))
                  (Seq
                     (Char '+')
                     (Seq
                        (Var (There (There Here)) (ENil (True)))
                        (Done
                           (ECons
                              (There (There Here))
                              (ECons (Here) (ENil (<Fun>))))))))))
         (ENil (True))))

 Let
   (Fix
      (Or
         (Seq (Char 'x') (Done (ENil (X))))
         (Seq
            (Guard (ECons (Here) (ENil (<Fun>))))
            (Seq
               (Var (Here) (ENil (False)))
               (Seq
                  (Char '+')
                  (Seq
                     (Var (Here) (ENil (True)))
                     (Done
                        (ECons
                           (Here)
                           (ECons (There (There Here)) (ENil (<Fun>))))))))))
      (ECons (Here) (ENil (<Fun>))))
   (Let
      (Let
         (Fix
            (Or
               (Seq (Char 'x') (Done (ENil (X))))
               (Seq
                  (Guard (ECons (Here) (ENil (<Fun>))))
                  (Seq
                     (Var (Here) (ENil (False)))
                     (Seq
                        (Char '+')
                        (Seq
                           (Var (Here) (ENil (True)))
                           (Done
                              (ECons
                                 (There (There Here))
                                 (ECons (Here) (ENil (<Fun>))))))))))
            (ECons (Here) (ENil (<Fun>))))
         (Fix
            (Seq
               (Guard (ECons (Here) (ENil (<Fun>))))
               (Or
                  (Seq
                     (Var (There Here) (ENil (True)))
                     (Done (ECons (Here) (ENil (<Fun>)))))
                  (Seq
                     (Var (Here) (ENil (False)))
                     (Seq
                        (Char '+')
                        (Seq
                           (Var (There Here) (ENil (True)))
                           (Done
                              (ECons
                                 (Here)
                                 (ECons
                                    (There (There Here)) (ENil (<Fun>))))))))))
            (ECons (Here) (ENil (<Fun>)))))
      (Fix
         (Seq
            (Guard (ECons (Here) (ENil (<Fun>))))
            (Or
               (Seq
                  (Var (There Here) (ENil (True)))
                  (Done (ECons (Here) (ENil (<Fun>)))))
               (Seq
                  (Var (Here) (ENil (False)))
                  (Seq
                     (Char '+')
                     (Seq
                        (Var (There (There Here)) (ENil (True)))
                        (Done
                           (ECons
                              (There (There Here))
                              (ECons (Here) (ENil (<Fun>))))))))))
         (ENil (True))))

@noughtmare
Copy link
Author

noughtmare commented Aug 18, 2024 •
edited
Loading

Perhaps this representation is a bit easier to read:

x =
  Fix
    ( Or
        (do Char 'x'; Done ([]))
        (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
    )
    ([])

x =
  Let
    ( Fix
        ( Or
            (do Char 'x'; Done ([]))
            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
        )
        ([0])
    )
    ( Fix
        ( Or
            (Done ([]))
            (do Guard ([0]); Var (0) ([]); Char '+'; Var (1) ([]); Done ([2, 0]))
        )
        ([])
    )

x =
  Let
    ( Fix
        ( Or
            (do Char 'x'; Done ([]))
            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
        )
        ([0])
    )
    ( Fix
        ( do
            Guard ([0])
            Or
              (do Var (1) ([]); Done ([0]))
              (do Var (0) ([]); Char '+'; Var (1) ([]); Done ([2, 0]))
        )
        ([])
    )

x =
  Let
    ( Fix
        ( Or
            (do Char 'x'; Done ([]))
            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
        )
        ([0])
    )
    ( Let
        ( Let
            ( Fix
                ( Or
                    (do Char 'x'; Done ([]))
                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
                )
                ([0])
            )
            ( Fix
                ( Or
                    (Done ([]))
                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (1) ([]); Done ([0, 2]))
                )
                ([0])
            )
        )
        ( Fix
            ( do
                Guard ([0])
                Or
                  (do Var (1) ([]); Done ([0]))
                  (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([2, 0]))
            )
            ([])
        )
    )

x =
  Let
    ( Fix
        ( Or
            (do Char 'x'; Done ([]))
            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
        )
        ([0])
    )
    ( Let
        ( Let
            ( Fix
                ( Or
                    (do Char 'x'; Done ([]))
                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
                )
                ([0])
            )
            ( Fix
                ( do
                    Guard ([0])
                    Or
                      (do Var (1) ([]); Done ([0]))
                      (do Var (0) ([]); Char '+'; Var (1) ([]); Done ([0, 2]))
                )
                ([0])
            )
        )
        ( Fix
            ( do
                Guard ([0])
                Or
                  (do Var (1) ([]); Done ([0]))
                  (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([2, 0]))
            )
            ([])
        )
    )

x =
  Let
    ( Fix
        ( Or
            (do Char 'x'; Done ([]))
            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
        )
        ([0])
    )
    ( Let
        ( Let
            ( Fix
                ( Or
                    (do Char 'x'; Done ([]))
                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
                )
                ([0])
            )
            ( Let
                ( Let
                    ( Fix
                        ( Or
                            (do Char 'x'; Done ([]))
                            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
                        )
                        ([0])
                    )
                    ( Fix
                        ( Or
                            (Done ([]))
                            (do Guard ([0]); Var (0) ([]); Char '+'; Var (1) ([]); Done ([2, 0]))
                        )
                        ([0])
                    )
                )
                ( Fix
                    ( do
                        Guard ([0])
                        Or
                          (do Var (1) ([]); Done ([0]))
                          (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([0, 2]))
                    )
                    ([0])
                )
            )
        )
        ( Fix
            ( do
                Guard ([0])
                Or
                  (do Var (1) ([]); Done ([0]))
                  (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([2, 0]))
            )
            ([])
        )
    )

x =
  Let
    ( Fix
        ( Or
            (do Char 'x'; Done ([]))
            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
        )
        ([0])
    )
    ( Let
        ( Let
            ( Fix
                ( Or
                    (do Char 'x'; Done ([]))
                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
                )
                ([0])
            )
            ( Let
                ( Let
                    ( Fix
                        ( Or
                            (do Char 'x'; Done ([]))
                            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
                        )
                        ([0])
                    )
                    ( Fix
                        ( do
                            Guard ([0])
                            Or
                              (do Var (1) ([]); Done ([0]))
                              (do Var (0) ([]); Char '+'; Var (1) ([]); Done ([2, 0]))
                        )
                        ([0])
                    )
                )
                ( Fix
                    ( do
                        Guard ([0])
                        Or
                          (do Var (1) ([]); Done ([0]))
                          (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([0, 2]))
                    )
                    ([0])
                )
            )
        )
        ( Fix
            ( do
                Guard ([0])
                Or
                  (do Var (1) ([]); Done ([0]))
                  (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([2, 0]))
            )
            ([])
        )
    )

x =
  Let
    ( Fix
        ( Or
            (do Char 'x'; Done ([]))
            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
        )
        ([0])
    )
    ( Let
        ( Let
            ( Fix
                ( Or
                    (do Char 'x'; Done ([]))
                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
                )
                ([0])
            )
            ( Let
                ( Let
                    ( Fix
                        ( Or
                            (do Char 'x'; Done ([]))
                            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
                        )
                        ([0])
                    )
                    ( Let
                        ( Let
                            ( Fix
                                ( Or
                                    (do Char 'x'; Done ([]))
                                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
                                )
                                ([0])
                            )
                            ( Fix
                                ( Or
                                    (Done ([]))
                                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (1) ([]); Done ([0, 2]))
                                )
                                ([0])
                            )
                        )
                        ( Fix
                            ( do
                                Guard ([0])
                                Or
                                  (do Var (1) ([]); Done ([0]))
                                  (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([2, 0]))
                            )
                            ([0])
                        )
                    )
                )
                ( Fix
                    ( do
                        Guard ([0])
                        Or
                          (do Var (1) ([]); Done ([0]))
                          (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([0, 2]))
                    )
                    ([0])
                )
            )
        )
        ( Fix
            ( do
                Guard ([0])
                Or
                  (do Var (1) ([]); Done ([0]))
                  (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([2, 0]))
            )
            ([])
        )
    )

x =
  Let
    ( Fix
        ( Or
            (do Char 'x'; Done ([]))
            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
        )
        ([0])
    )
    ( Let
        ( Let
            ( Fix
                ( Or
                    (do Char 'x'; Done ([]))
                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
                )
                ([0])
            )
            ( Let
                ( Let
                    ( Fix
                        ( Or
                            (do Char 'x'; Done ([]))
                            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
                        )
                        ([0])
                    )
                    ( Let
                        ( Let
                            ( Fix
                                ( Or
                                    (do Char 'x'; Done ([]))
                                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
                                )
                                ([0])
                            )
                            ( Fix
                                ( do
                                    Guard ([0])
                                    Or
                                      (do Var (1) ([]); Done ([0]))
                                      (do Var (0) ([]); Char '+'; Var (1) ([]); Done ([0, 2]))
                                )
                                ([0])
                            )
                        )
                        ( Fix
                            ( do
                                Guard ([0])
                                Or
                                  (do Var (1) ([]); Done ([0]))
                                  (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([2, 0]))
                            )
                            ([0])
                        )
                    )
                )
                ( Fix
                    ( do
                        Guard ([0])
                        Or
                          (do Var (1) ([]); Done ([0]))
                          (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([0, 2]))
                    )
                    ([0])
                )
            )
        )
        ( Fix
            ( do
                Guard ([0])
                Or
                  (do Var (1) ([]); Done ([0]))
                  (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([2, 0]))
            )
            ([])
        )
    )

x =
  Let
    ( Fix
        ( Or
            (do Char 'x'; Done ([]))
            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
        )
        ([0])
    )
    ( Let
        ( Let
            ( Fix
                ( Or
                    (do Char 'x'; Done ([]))
                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
                )
                ([0])
            )
            ( Let
                ( Let
                    ( Fix
                        ( Or
                            (do Char 'x'; Done ([]))
                            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
                        )
                        ([0])
                    )
                    ( Let
                        ( Let
                            ( Fix
                                ( Or
                                    (do Char 'x'; Done ([]))
                                    (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([2, 0]))
                                )
                                ([0])
                            )
                            ( Let
                                ( Let
                                    ( Fix
                                        ( Or
                                            (do Char 'x'; Done ([]))
                                            (do Guard ([0]); Var (0) ([]); Char '+'; Var (0) ([]); Done ([0, 2]))
                                        )
                                        ([0])
                                    )
                                    ( Fix
                                        ( Or
                                            (Done ([]))
                                            (do Guard ([0]); Var (0) ([]); Char '+'; Var (1) ([]); Done ([2, 0]))
                                        )
                                        ([0])
                                    )
                                )
                                ( Fix
                                    ( do
                                        Guard ([0])
                                        Or
                                          (do Var (1) ([]); Done ([0]))
                                          (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([0, 2]))
                                    )
                                    ([0])
                                )
                            )
                        )
                        ( Fix
                            ( do
                                Guard ([0])
                                Or
                                  (do Var (1) ([]); Done ([0]))
                                  (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([2, 0]))
                            )
                            ([0])
                        )
                    )
                )
                ( Fix
                    ( do
                        Guard ([0])
                        Or
                          (do Var (1) ([]); Done ([0]))
                          (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([0, 2]))
                    )
                    ([0])
                )
            )
        )
        ( Fix
            ( do
                Guard ([0])
                Or
                  (do Var (1) ([]); Done ([0]))
                  (do Var (0) ([]); Char '+'; Var (2) ([]); Done ([2, 0]))
            )
            ([])
        )
    )

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment