From 34aee3bf93c516fc35cd1437d71598b779ec8608 Mon Sep 17 00:00:00 2001 From: James Eversole Date: Wed, 8 Jul 2026 10:27:42 -0500 Subject: [PATCH] Explicit local bindings for let/where --- src/Check/Core.hs | 20 ++++++++++++++++++++ src/Check/IO.hs | 5 +++++ src/Eval.hs | 6 ++++++ src/Parser.hs | 4 ++-- src/Research.hs | 5 +++++ test/Spec.hs | 26 ++++++++++++++++++++++---- 6 files changed, 60 insertions(+), 6 deletions(-) diff --git a/src/Check/Core.hs b/src/Check/Core.hs index 187c7da..c452976 100644 --- a/src/Check/Core.hs +++ b/src/Check/Core.hs @@ -165,6 +165,9 @@ definitionUnsafeBaseReason localNames allowedExternalFacts bound ast = case ast TStem _ -> Just "uses raw t directly" TFork _ _ -> Just "uses raw t directly" SLambda args body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound args) body + SLet name val body -> + definitionUnsafeBaseReason localNames allowedExternalFacts bound val + <|> definitionUnsafeBaseReason localNames allowedExternalFacts (Set.insert name bound) body SEmpty -> Nothing SImport _ _ -> Nothing @@ -187,6 +190,7 @@ astFreeRefs candidates ast = case ast of TStem inner -> astFreeRefs candidates inner TFork left right -> astFreeRefs candidates left ++ astFreeRefs candidates right SLambda args body -> astFreeRefs (foldr Set.delete candidates args) body + SLet name val body -> astFreeRefs candidates val ++ astFreeRefs (Set.delete name candidates) body SEmpty -> [] SImport _ _ -> [] @@ -584,6 +588,14 @@ lowerExprKnownAgainst expr expected = case (expr, viewExprAsType expected) of (SApp (SApp (SVar "err" _) value) rest, Just (VTResult errView _)) -> lowerUnshadowedConstructor "err" expr expected $ lowerResultConstructor expected (viewTypeToExpr errView) value rest + (SLet name value body, _) -> do + (valueSym, valueNodes, _) <- lowerExprKnown value + recordDebugName valueSym name + bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected) + let (bodySym, bodyNodes, bodyKnown) = bodyResult + pure (bodySym, valueNodes ++ bodyNodes, bodyKnown) + -- Hand-written immediately-applied lambda (not compiler output; let/where + -- now emit SLet). Kept for source that relies on alias semantics. (SApp (SLambda [name] body) value, _) -> do (valueSym, valueNodes, _) <- lowerExprKnown value bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected) @@ -658,6 +670,14 @@ lowerExprKnown TLeaf = do lowerExprKnown (SList items) = do (sym, nodes, view, _) <- lowerListLiteral items pure (sym, nodes, Just view) +lowerExprKnown (SLet name value body) = do + (valueSym, valueNodes, _) <- lowerExprKnown value + recordDebugName valueSym name + bodyResult <- withLocalAlias name valueSym (lowerExprKnown body) + let (bodySym, bodyNodes, bodyKnown) = bodyResult + pure (bodySym, valueNodes ++ bodyNodes, bodyKnown) +-- Hand-written immediately-applied lambda (not compiler output; let/where +-- now emit SLet). Kept for source that relies on alias semantics. lowerExprKnown (SApp (SLambda [name] body) value) = do (valueSym, valueNodes, known) <- lowerExprKnown value bodyResult <- withLocalAlias name valueSym (lowerExprKnown body) diff --git a/src/Check/IO.hs b/src/Check/IO.hs index 43479df..2005667 100644 --- a/src/Check/IO.hs +++ b/src/Check/IO.hs @@ -105,6 +105,7 @@ instrumentIOContinuations asts = mapM transformTop asts SApp (SVar "io" h) action -> SApp (SVar "io" h) <$> transformIOAction action SApp f a -> SApp <$> transformExpr f <*> transformExpr a SLambda params body -> SLambda params <$> transformExpr body + SLet name val body -> SLet name <$> transformExpr val <*> transformExpr body TStem x -> TStem <$> transformExpr x TFork x y -> TFork <$> transformExpr x <*> transformExpr y _ -> pure expr @@ -118,6 +119,7 @@ instrumentIOContinuations asts = mapM transformTop asts SApp <$> (SApp (SVar "bind" h) <$> transformIOAction left) <*> (SLambda params <$> transformIOAction body) SApp f a -> SApp <$> transformIOAction f <*> transformIOAction a SLambda params body -> SLambda params <$> transformIOAction body + SLet name val body -> SLet name <$> transformIOAction val <*> transformIOAction body _ -> transformExpr action checkedPureActionFor value = @@ -183,6 +185,7 @@ mentionsContractedName contracts expr = case expr of SVar name _ -> Map.member name contracts SApp f a -> mentionsContractedName contracts f || mentionsContractedName contracts a SLambda _ body -> mentionsContractedName contracts body + SLet _ val body -> mentionsContractedName contracts val || mentionsContractedName contracts body SList items -> any (mentionsContractedName contracts) items TStem x -> mentionsContractedName contracts x TFork x y -> mentionsContractedName contracts x || mentionsContractedName contracts y @@ -372,6 +375,7 @@ substAst subst expr = case expr of SVar name Nothing -> Map.findWithDefault expr name subst SApp f a -> SApp (substAst subst f) (substAst subst a) SLambda params body -> SLambda params (substAst (foldr Map.delete subst params) body) + SLet name val body -> SLet name (substAst subst val) (substAst (Map.delete name subst) body) SList items -> SList (map (substAst subst) items) TStem x -> TStem (substAst subst x) TFork x y -> TFork (substAst subst x) (substAst subst y) @@ -397,6 +401,7 @@ astSource expr = case expr of SList items -> "[" ++ unwords (map (parens . astSource) items) ++ "]" SApp f a -> parens (astSource f) ++ " " ++ parens (astSource a) SLambda params body -> parens (unwords params ++ " : " ++ astSource body) + SLet name val body -> parens ("let " ++ name ++ " = " ++ astSource val ++ " in " ++ astSource body) TLeaf -> "t" TStem x -> "(t " ++ astSource x ++ ")" TFork x y -> "(t " ++ astSource x ++ " " ++ astSource y ++ ")" diff --git a/src/Eval.hs b/src/Eval.hs index ee2e58a..fb3e64c 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -75,6 +75,7 @@ evalTricu env x = go env (reorderDefs env (map recoverParams x)) evalASTSync :: Env -> TricuAST -> T evalASTSync env term = case term of SLambda _ _ -> evalASTSync env (elimLambda term) + SLet name val body -> evalASTSync env (SApp (SLambda [name] body) val) SVar name Nothing -> case Map.lookup name env of Just v -> v Nothing -> errorWithoutStackTrace $ "Variable " ++ name ++ " not defined" @@ -108,6 +109,7 @@ annotatedBinders (DefPhantom _ : rest) = annotatedBinders rest elimLambda :: TricuAST -> TricuAST elimLambda = go where + go (SLet name val body) = go (SApp (SLambda [name] body) val) go term | etaReduction term = go (etaReduceResult term) | triagePattern term = _TRI @@ -190,6 +192,8 @@ freeVars (SVar v Nothing) = Set.singleton v freeVars (SVar v (Just _)) = Set.singleton v freeVars (SApp t u) = Set.union (freeVars t) (freeVars u) freeVars (SLambda vs body) = Set.difference (freeVars body) (Set.fromList vs) +freeVars (SLet name val body) = + Set.union (freeVars val) (Set.delete name (freeVars body)) freeVars (SDef _ params body) = Set.difference (freeVars body) (Set.fromList params) freeVars (SDefAnn _ args _ body) = Set.difference (freeVars body) (Set.fromList (annotatedBinders args)) freeVars (TStem t) = freeVars t @@ -297,6 +301,7 @@ findVarNames ast = case ast of SVar name _ -> [name] SApp a b -> findVarNames a ++ findVarNames b SLambda args body -> findVarNames body \\ args + SLet name val body -> findVarNames val ++ (findVarNames body \\ [name]) SDef name args body -> name : (findVarNames body \\ args) SDefAnn name args _ body -> name : (findVarNames body \\ annotatedBinders args) _ -> [] @@ -317,6 +322,7 @@ toDB env = \case SInt n -> BInt n SList xs -> BList (map (toDB env) xs) SEmpty -> BEmpty + SLet name val body -> toDB env (SApp (SLambda [name] body) val) SDef{} -> error "toDB: unexpected SDef at this stage" SDefAnn{} -> error "toDB: unexpected SDefAnn at this stage" SImport _ _ -> BEmpty diff --git a/src/Parser.hs b/src/Parser.hs index 45e8991..56f0a93 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -496,7 +496,7 @@ whereChainP parseBody = do Nothing -> pure body Just (name, args, value) -> let boundValue = foldr (\p acc -> SLambda [p] acc) value args - in pure (SApp (SLambda [name] body) boundValue) + in pure (SLet name boundValue body) whereBindingP :: TokParser (String, [String], TricuAST) whereBindingP = do @@ -524,7 +524,7 @@ letP = do bodyIndent <- skipNestedNewlinesGetIndent body <- exprAtIndentP bodyIndent let boundValue = foldr (\p acc -> SLambda [p] acc) value args - pure (SApp (SLambda [name] body) boundValue) + pure (SLet name boundValue body) data DoStmt = DoBind String TricuAST diff --git a/src/Research.hs b/src/Research.hs index 742d9a8..68501d3 100644 --- a/src/Research.hs +++ b/src/Research.hs @@ -84,6 +84,11 @@ data TricuAST | TStem TricuAST | TFork TricuAST TricuAST | SLambda [String] TricuAST + -- Non-recursive local binding: `name = boundValue` scoped over `body`. + -- Produced by let/where desugaring. `boundValue` already folds any binding + -- arguments into nested SLambda. Semantically equal to + -- SApp (SLambda [name] body) boundValue + | SLet String TricuAST TricuAST | SEmpty | SImport String String deriving (Show, Eq, Ord) diff --git a/test/Spec.hs b/test/Spec.hs index 843f94a..b6b6ec2 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -336,7 +336,7 @@ parser = testGroup "Parser Tests" , testCase "Parse let expression" $ do let input = "let x = t t in x" - expect = SApp (SLambda ["x"] (SVar "x" Nothing)) (SApp TLeaf TLeaf) + expect = SLet "x" (SApp TLeaf TLeaf) (SVar "x" Nothing) parseSingle input @?= expect , testCase "Evaluate let expression" $ do @@ -344,18 +344,36 @@ parser = testGroup "Parser Tests" , testCase "Parse let function binding" $ do let input = "let f x = x in f t" - expect = SApp (SLambda ["f"] (SApp (SVar "f" Nothing) TLeaf)) - (SLambda ["x"] (SVar "x" Nothing)) + expect = SLet "f" (SLambda ["x"] (SVar "x" Nothing)) + (SApp (SVar "f" Nothing) TLeaf) parseSingle input @?= expect , testCase "Parse where expression" $ do let input = "x where x = t t" - expect = SApp (SLambda ["x"] (SVar "x" Nothing)) (SApp TLeaf TLeaf) + expect = SLet "x" (SApp TLeaf TLeaf) (SVar "x" Nothing) parseSingle input @?= expect , testCase "Evaluate where expression" $ do tricuTestString "x where x = 1" @?= "Fork (Stem Leaf) Leaf" + , testCase "Parse where binding with arguments (SLet)" $ do + let input = "f 3 where f x = x" + expect = SLet "f" (SLambda ["x"] (SVar "x" Nothing)) + (SApp (SVar "f" Nothing) (SInt 3)) + parseSingle input @?= expect + + , testCase "Evaluate where binding with arguments matches applied lambda" $ do + tricuTestString "f (t t) where f x = t x x" + @?= tricuTestString "(f : f (t t)) (x : t x x)" + + , testCase "Evaluate nested let bindings" $ do + tricuTestString "let a = t t in let b = t in t a b" + @?= tricuTestString "t (t t) t" + + , testCase "Inner let binding shadows outer binding" $ do + tricuTestString "let x = t in let x = t t in x" + @?= tricuTestString "t t" + , testCase "Parse indented multiline definition body" $ do let input = "x =\n t\n t" expect = SDef "x" [] (SApp TLeaf TLeaf)