Add parsing for let ... in ... statement.

kami-language · Aug 10, 2024 · b6031b9 · b6031b9
1 parent 0138fd6
commit b6031b9
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/src/Parser/Definition.hs b/src/Parser/Definition.hs
@@ -103,6 +103,7 @@ basetermParser = choice
     , try $ string "tt" >> return TT
     , try $ between (string "(") (string ")") termParser'
     , try $ between (string "{") (string "}") (Mod Box <$> termParser') -- mod for box modality
+    , try $ string "let" >> white' >> LetIn <$> argParser <* white' <* string "=" <* white' <*> termParser' <* spaces <* string "in" <* white' <*> termParser'
 
     , try $ string "fst" >> white' >> Fst <$> basetermParser
     , try $ string "snd" >> white' >> Snd <$> basetermParser

diff --git a/test/examples/globalize-sum.kami b/test/examples/globalize-sum.kami
@@ -6,8 +6,10 @@ aa : Unit
 aa = tt
 
 gl : ((Unit + Unit) @ 0) -> ((Unit @ 0) + (Unit @ 0))
-gl x = (\(y : {(Unit @ 0) + (Unit @ 0)} @ 0) -> y) (gl0 x)
+gl x = let y = gl0 x
+       in y
 
+// (\(y : {(Unit @ 0) + (Unit @ 0)} @ 0) -> y) (gl0 x)
 // gl0 x
 // gl0 (xs @ 0) = either xs (\x -> {left (x @ 0)}) g @ 0
 // gl0 (left xleft @ 0) = {left (x @ 0)} @ 0