From 4a6378aa868e9c1d49fc5ad1576616933c913004 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Thu, 14 Nov 2024 16:54:14 +0100
Subject: Basic reduction

---
 src/Language/Mili/Parser.hs | 24 ++++++++++--------------
 1 file changed, 10 insertions(+), 14 deletions(-)

(limited to 'src/Language/Mili/Parser.hs')

diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs
index a733ade..958c0a8 100644
--- a/src/Language/Mili/Parser.hs
+++ b/src/Language/Mili/Parser.hs
@@ -77,7 +77,9 @@ toLevel n = do
 
 -- | abstraction, entering increases the abstraction depth
 abs :: Parser Term
-abs = between (startSymbol "[") (symbol "]") (Abs <$> (inc *> block <* dec))
+abs = between (startSymbol "[")
+              (symbol "]")
+              (gets (Abs <$> _depth) <*> (inc *> block <* dec))
  where
   inc = modify $ \r@(PS { _depth = d }) -> r { _depth = d + 1 }
   dec = modify $ \r@(PS { _depth = d }) -> r { _depth = d - 1 }
@@ -98,28 +100,22 @@ rec :: Parser Term
 rec = do
   _  <- symbol "REC"
   _  <- spaces
-  _  <- symbol "("
-  _  <- spaces
+  _  <- startSymbol "("
   t  <- term
   _  <- spaces
-  _  <- symbol ","
-  _  <- spaces
+  _  <- startSymbol ","
   t' <- nat
   _  <- spaces
-  _  <- symbol ")"
-  _  <- spaces
-  _  <- symbol ","
-  _  <- spaces
+  _  <- startSymbol ")"
+  _  <- startSymbol ","
   u  <- term
   _  <- spaces
-  _  <- symbol ","
-  _  <- spaces
+  _  <- startSymbol ","
   v  <- term
   _  <- spaces
-  _  <- symbol ","
-  _  <- spaces
+  _  <- startSymbol ","
   w  <- term
-  pure $ Rec (t, t') u v w -- TODO
+  pure $ Rec (t, t') u v w
 
 -- | single identifier, directly parsed to corresponding term
 def :: Parser Term
-- 
cgit v1.2.3