systemqfw

commit 28f3bc9cd70267578af66975c8216ca595fcc2e3
parent 4ba1eb6a4f4e8b9ca44327011c419f5eeccfcfbb
Author: Robert Russell <robert@rr3.xyz>
Date:   Wed, 28 Aug 2024 23:40:03 -0700

Lower precedence of let to make the current example work

By increasing the precedence of lets above annots (where they
should probably be, anyway), we ensure all top-level
(unparenthesized) lets aren't checked; they're only inferred.
Really, we ought to write a checking rule for lets as well, but
I can't be bothered.

Diffstat:
M
Main.hs
 | 
2
+-
M
Parser.hs
 | 
6
+++---

2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/Main.hs b/Main.hs
@@ -256,7 +256,7 @@ input :: ByteString
 input =
     ByteString.intercalate "\n" [
         "let zero : @M:* -> M -> (M -> M) -> M = \\[M] z s => z;",
-        "zero"
+        "\\[M] z s => z : @M:* -> M -> (M -> M) -> M"
     ]
 
 main :: IO ()
diff --git a/Parser.hs b/Parser.hs
@@ -165,15 +165,15 @@ pTermLet = do
     pSym "=" `cut` Err
     arg <- pTerm 1 `cut` Err
     pSym ";" `cut` Err
-    body <- pTerm 1 `cut` Err
+    body <- pTerm 0 `cut` Err
     pure $ TermLet x arg qa body
 
 pTerm :: Int -> P q (Term q)
 pTerm = \case
-    0 -> do
+    0 -> pTermLet <|> do
         t <- pTerm 1
         pTermAnnot t <|> pure t
-    1 -> pTermAbs <|> pTermLet <|> pTerm 2
+    1 -> pTermAbs <|> pTerm 2
     2 -> pTerm 3 >>= iter \t -> TermArrowApp t <$> pTerm 3
         <|> TermForallApp t <$> pDelim "[" (pType 0) "]"
     3 -> TermVar <$> pTermName