From a9f190bceeebb6afb9b5c885c5bfc00e4ed00d10 Mon Sep 17 00:00:00 2001 From: "Eric Vincent (arch)" Date: Wed, 27 May 2026 13:28:09 -0400 Subject: [PATCH 1/2] phase10: add terminal IO builtins --- CHANGELOG.md | 14 +++++++++ README.md | 3 ++ app/Main.hs | 4 +-- docs/language-spec.md | 13 ++++++-- docs/phase10-c-codegen.md | 20 +++++++++--- lithic.cabal | 2 +- src/Compiler/CGen.hs | 63 +++++++++++++++++++++++++++++++------ src/Compiler/CGenPrelude.c | 58 ++++++++++++++++++++++++++++++++++ src/Compiler/REPL.hs | 4 +-- src/Compiler/TypeChecker.hs | 21 +++++++++++-- test/Test/CGen.hs | 32 +++++++++++++++++++ test/Test/CLIEmitC.hs | 23 ++++++++++++++ test/Test/Golden.hs | 4 +-- 13 files changed, 235 insertions(+), 26 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2decc26..cbb14a4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,19 @@ # Revision history for lithic +## 0.9.19.0 -- 2026-05-27 (Phase 10 C3.7 Terminal IO Builtins) + +* Phase 10 C3.7 terminal IO builtin slice: + * Added compiler-provided builtin bindings for `print : String -> String` and `readLn : String` so REPL, golden tests, and CLI `--emit-c` paths share the same starting type environment. + * Added first-pass C runtime helpers for `lithic_builtin_print` and `lithic_builtin_readln` in the embedded C prelude. + * Lowered Core references to `readLn` and calls to `print` through the runtime helper ABI. + * Added generated C `main(void)` wrapper emission when a zero-argument Lithic `main` declaration is present. +* Test coverage: + * Added focused CGen unit coverage for generated C entrypoint emission, `print` lowering, and `readLn` lowering, including gcc compile checks. + * Added CLI `--emit-c` integration coverage for `def main = print readLn`, including generated C wrapper/helper assertions and gcc compile checks. + * Updated golden-test typing setup to use the shared builtin environment. +* Validation: + * Editor diagnostics: clean for touched source and test modules. + ## 0.9.18.0 -- 2026-05-27 (Phase 10 C3.6 Arithmetic Lowering) * Phase 10 C3.6 arithmetic lowering: diff --git a/README.md b/README.md index 23dc90a..249d721 100644 --- a/README.md +++ b/README.md @@ -32,6 +32,8 @@ Current `--emit-c` constraints: - Input must parse as a top-level declaration (bare expressions are rejected). - Current path accepts named function declarations (`f x = ...`). - Emission is monomorphism-gated; unresolved polymorphism is reported as a codegen diagnostic. +- A zero-argument Lithic declaration named `main` emits a C `main(void)` wrapper that invokes `lithic_main()`. +- First-pass terminal IO builtins are available in typed pipelines: `print : String -> String` writes a string without adding a newline, and `readLn : String` reads one line ending at carriage return or newline. Golden cases are discovered from `test/fixtures/*.lithic` and compared against matching snapshots in `test/golden/*.golden`. @@ -54,6 +56,7 @@ In the REPL: ``` Literal scrutinees are also handled directly, so `case True of True => 1` is accepted. - Primitive literals currently include `Int`, `Float`, `String`, and `Bool` (`True`/`False`). +- First-pass terminal IO builtins are available: `print : String -> String` and `readLn : String`. `print` does not append a newline; include `\n` in the string when needed. - Prefix unary minus and infix subtraction are supported (`-x`, `x - y`). - Top-level declaration parsing (used by the file/golden pipeline) supports Phase 9F first-slice single-argument equation grouping, including pattern-headed arity-1 clauses. - `where` blocks on equation-style top-level declarations are supported (Phase 9G): bindings are layout-delimited and desugar to nested `let` bindings wrapping the equation body. Example: diff --git a/app/Main.hs b/app/Main.hs index 2302787..4eaec2e 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -26,7 +26,7 @@ import Compiler.Lexer (runLexer, LexError(..)) import Compiler.Parser (parseTopLevel, ParseError(..)) import Compiler.REPL (replLoop, runTerminalBrick) import Compiler.TUI (runTUI, TUIEvent(..)) -import Compiler.TypeChecker (Env(..), TCState(..), TypeError(..), infer, zonk) +import Compiler.TypeChecker (TCState(..), TypeError(..), builtinEnv, infer, zonk) import Compiler.TypeChecker () main :: IO () @@ -75,7 +75,7 @@ runEmitC srcPath outPath = do let tcResult = runPureEff $ evalState (MkTCState 0 IM.empty) \st -> try \ex -> - runReader (MkEnv []) \env -> do + runReader builtinEnv \env -> do rawTy <- infer st env ex rhs zonk st rawTy case tcResult of diff --git a/docs/language-spec.md b/docs/language-spec.md index 3818e30..2beaa9b 100644 --- a/docs/language-spec.md +++ b/docs/language-spec.md @@ -1,8 +1,8 @@ # Lithic Language Specification (Living Core Spec) Status: Active living spec for implemented behavior. -Version: 0.7 (2026-05-18) -Scope baseline: Parser + bidirectional checker through Phase 10 C backend scaffold (literal-scrutinee coverage fix, REPL `[C]` output). +Version: 0.8 (2026-05-27) +Scope baseline: Parser + bidirectional checker through Phase 10 C backend scaffold and first-pass terminal IO builtins (`print`, `readLn`). This document is the normative source for the currently implemented Lithic surface language and static semantics. Where implementation and docs disagree, this spec is the authority to reconcile against. @@ -56,6 +56,7 @@ Normative implemented semantics (this revision): 2. Bidirectional static semantics through current `infer`/`check`/`subsumes` pipeline. 3. Case-branch exhaustiveness and redundancy coverage semantics. 4. REPL diagnostic envelope and span-locality contracts. +5. First-pass compiler-provided builtin term bindings for terminal IO. Planned/informative semantics (non-normative in this revision): 1. Evaluator operational semantics and value model. @@ -229,6 +230,13 @@ Status table for planned declaration forms: | Pattern-headed clause (single argument) | `f = expr` | Implemented (parseTopLevel only) | Included in Phase 9F first-slice clause grouping and lowered through the same lambda/case path as other arity-1 clauses. | | Pattern-headed clause (multi argument) | `f ... = expr` | Not implemented yet | Awaiting the multi-argument clause-group follow-on slice. | +Builtin term environment currently includes: + +| Name | Type | Implementation Status | Notes | +| --- | --- | --- | --- | +| `print` | `String -> String` | Implemented | First-pass terminal IO builtin. C lowering writes the string to stdout without appending a newline and returns the original string handle. | +| `readLn` | `String` | Implemented | First-pass terminal IO builtin. C lowering reads one line from stdin, stopping on carriage return or newline. | + ```text TopLevel ::= Decl | Expr @@ -406,6 +414,7 @@ Current C2.1 codegen diagnostic note: 1. Declaration codegen still requires monomorphic declaration types. 2. When a declaration type includes unresolved polymorphism at the CGen boundary, the emitted `[C]` block includes: `codegen error: program is not fully monomorphic; instantiate before code generation`. +3. A zero-argument Lithic declaration named `main` emits a generated C `main(void)` wrapper that invokes `lithic_main()`. Contract requirements: 1. Diagnostics carry precise `Span` whenever an originating token/node exists. diff --git a/docs/phase10-c-codegen.md b/docs/phase10-c-codegen.md index 8f23f4b..4abb1d8 100644 --- a/docs/phase10-c-codegen.md +++ b/docs/phase10-c-codegen.md @@ -1,11 +1,23 @@ # Phase 10 Scaffold: C Code Generation First Pass -Status: C2.2 call/case/variant/select lowering merged on main (PR #28) + C4.3 fixture-level emit/compile integration landed (2026-05-23) + C3.1 compile-time prelude template embedding and C3.2 first-pass prelude safety hardening landed + expanded C4.4 compile/link/run sanity gate (2026-05-24) + C3.3 helper-contract depth landed (2026-05-25) + C3.4 record-init failure propagation and CLI long-field fixture coverage landed (2026-05-25) + C3.5 case-expression and expression-value lowering depth landed (2026-05-26) -Branch: main (post-merge baseline) +Status: C2.2 call/case/variant/select lowering merged on main (PR #28) + C4.3 fixture-level emit/compile integration landed (2026-05-23) + C3.1 compile-time prelude template embedding and C3.2 first-pass prelude safety hardening landed + expanded C4.4 compile/link/run sanity gate (2026-05-24) + C3.3 helper-contract depth landed (2026-05-25) + C3.4 record-init failure propagation and CLI long-field fixture coverage landed (2026-05-25) + C3.5 case-expression and expression-value lowering depth landed (2026-05-26) + C3.6 arithmetic lowering landed (2026-05-27) + C3.7 first-pass terminal IO builtin lowering in progress (2026-05-27) +Branch: feat/phase10-c3-7-io-main-print-readln -Next prep checkpoint: `docs/phase10-c3-6-prep.md`. +Next prep checkpoint: C3.7 terminal IO builtin validation. -## Immediate Next Slice (C3.6 — Arithmetic Core/CGen Lowering) +## Immediate Next Slice (C3.7 — Terminal IO Builtins) + +Goal: provide the smallest end-to-end terminal IO surface through the existing +typed and C backend pipelines without introducing a general effect system yet. + +Implemented direction for this slice: + +1. Add shared builtin term bindings for `print : String -> String` and `readLn : String`. +2. Lower `print` calls and `readLn` references through explicit C prelude helpers. +3. Emit a generated C `main(void)` wrapper when a zero-argument Lithic `main` declaration is present. +4. Keep newline behavior user-controlled: `print` does not append one; source strings may include `\n`. + +## Previous Slice (C3.6 — Arithmetic Core/CGen Lowering) Goal: introduce arithmetic operators in Core and CGen so direct numeric programs can lower without relying on placeholder/unsupported paths. diff --git a/lithic.cabal b/lithic.cabal index f690a26..656b0b4 100644 --- a/lithic.cabal +++ b/lithic.cabal @@ -1,6 +1,6 @@ cabal-version: 3.4 name: lithic -version: 0.9.18.0 +version: 0.9.19.0 build-type: Simple license: NONE author: Eric Vincent (arch) diff --git a/src/Compiler/CGen.hs b/src/Compiler/CGen.hs index 1c2ef4d..4ea04fe 100644 --- a/src/Compiler/CGen.hs +++ b/src/Compiler/CGen.hs @@ -34,6 +34,27 @@ cgenProgram pairs = cPreludeChunk <> cDeclCountComment pairs <> cDeclarationSection pairs + <> cMainEntrypoint pairs + +-- | Emit a C entrypoint wrapper when a zero-arg Lithic declaration is present. +cMainEntrypoint :: Decls -> TB.Builder +cMainEntrypoint pairs = + if hasMainDecl pairs + then TB.fromText $ blks [c| + int main(void) { + (void)lithic_main(); + return 0; + } |] + else mempty + +hasMainDecl :: Decls -> Bool +hasMainDecl = any isMainDecl + where + isMainDecl (CDeclDef _ name rhs, _) | name == "main" = + case declShape rhs of + DeclConstant _ -> True + _1 -> False + isMainDecl _ = False -- | Static C prelude cPreludeChunk :: TB.Builder @@ -115,8 +136,8 @@ cgenDecl (decl, mTy) = case decl of let valTy = maybe "intptr_t" cgenCType mTy fName = cFunctionName name fBody = cgenExprValueAs valTy body - in TB.fromText $ - if isStaticCInitializer body + in TB.fromText $ + if name /= "main" && isStaticCInitializer body then blks [c| /* definition: $name */ $valTy $fName = $fBody; |] @@ -191,7 +212,9 @@ cgenFunctionBodyScoped inScope retTy = \case in blk [c| return ($retTy)$r; |] CVar _ varName -> - blk [c| return $varName; |] + case cgenBuiltinValue varName of + Just builtinExpr -> blk [c| return ($retTy)$builtinExpr; |] + Nothing -> blk [c| return $varName; |] -- Target 4: let-binding to stack-allocated local. -- Only CPVar patterns are precisely lowered; other patterns fall through @@ -219,9 +242,12 @@ cgenFunctionBodyScoped inScope retTy = \case -- Any other call target shape falls back with an explicit diagnostic marker. case fn of CVar _ fnName -> - let calleeName = cgenCallName inScope fnName - argExpr = cgenExprValue arg - in blk [c| return ($retTy)$calleeName($argExpr); |] + let argExpr = cgenExprValue arg + in case cgenBuiltinCall fnName [argExpr] of + Just builtinExpr -> blk [c| return ($retTy)$builtinExpr; |] + Nothing -> + let calleeName = cgenCallName inScope fnName + in blk [c| return ($retTy)$calleeName($argExpr); |] unsupportedFn -> let cFnTag = cgenExprTag unsupportedFn cArg = cgenExprTag arg @@ -331,15 +357,22 @@ cgenExprValue = \case CLit _ lit -> cgenLiteralValue lit - CVar _ varName -> varName + CVar _ varName -> + case cgenBuiltinValue varName of + Just builtinExpr -> builtinExpr + Nothing -> varName appExpr@(CApp _ _ _) -> let (callee, args) = collectArgs appExpr in case callee of CVar _ fnName -> - let cFnName = cFunctionName fnName - argVals = T.intercalate ", " (map cgenExprValue args) - in [c|$cFnName($argVals)|] + let argVals = map cgenExprValue args + in case cgenBuiltinCall fnName argVals of + Just builtinExpr -> builtinExpr + Nothing -> + let cFnName = cFunctionName fnName + cArgs = T.intercalate ", " argVals + in [c|$cFnName($cArgs)|] _ -> "/* unsupported-rhs:" <> cgenExprTag appExpr <> " */ (intptr_t)0" @@ -670,6 +703,16 @@ cgenRecordInitStep recTmp retTy ix (fieldName, fieldExpr) = -- ─── Utilities ──────────────────────────────────────────────────────────────── +cgenBuiltinValue :: Text -> Maybe Text +cgenBuiltinValue name = case name of + "readLn" -> Just "lithic_builtin_readln()" + _ -> Nothing + +cgenBuiltinCall :: Text -> [Text] -> Maybe Text +cgenBuiltinCall name args = case (name, args) of + ("print", [x]) -> Just [c|lithic_builtin_print((intptr_t)$x)|] + _ -> Nothing + -- | Resolve a callable C name from a surface/Core variable name. -- Names already bound in local scope are emitted unchanged; all other names are -- treated as top-level declarations and mapped via cFunctionName. diff --git a/src/Compiler/CGenPrelude.c b/src/Compiler/CGenPrelude.c index 47dbc4c..6ec3b15 100644 --- a/src/Compiler/CGenPrelude.c +++ b/src/Compiler/CGenPrelude.c @@ -361,6 +361,64 @@ static inline intptr_t lithic_record_select(intptr_t record, intptr_t field) { return (intptr_t)0; } +/* + * Builtin: print + * + * Treats the incoming intptr_t as a C string pointer, writes it to stdout, + * and returns the original handle. + */ +static inline intptr_t lithic_builtin_print(intptr_t value) { + if (value == (intptr_t)0) { + return (intptr_t)0; + } + const char *s = (const char *)(uintptr_t)value; + fputs(s, stdout); + fflush(stdout); + return value; +} + +/* + * Builtin: readLn + * + * Reads a single line from stdin, stopping on `\r` or `\n`. + * Returns a heap-allocated NUL-terminated string handle, or 0 on EOF/failure. + */ +static inline intptr_t lithic_builtin_readln(void) { + size_t cap = 128; + char *buf = (char *)malloc(cap); + if (buf == NULL) { + return (intptr_t)0; + } + + size_t len = 0; + int ch; + while ((ch = fgetc(stdin)) != EOF) { + if (ch == '\n' || ch == '\r') { + break; + } + + if (len + 1 >= cap) { + size_t nextCap = cap * 2; + char *grown = (char *)realloc(buf, nextCap); + if (grown == NULL) { + free(buf); + return (intptr_t)0; + } + buf = grown; + cap = nextCap; + } + buf[len++] = (char)ch; + } + + if (ch == EOF && len == 0) { + free(buf); + return (intptr_t)0; + } + + buf[len] = '\0'; + return (intptr_t)(uintptr_t)buf; +} + /* Marker helper used by unsupported generated paths in scaffold stages. */ static inline void lithic_unsupported_fn(intptr_t arg) { (void)arg; diff --git a/src/Compiler/REPL.hs b/src/Compiler/REPL.hs index e7f7940..3e8ae0a 100644 --- a/src/Compiler/REPL.hs +++ b/src/Compiler/REPL.hs @@ -20,7 +20,7 @@ import Compiler.AST (Decl(..), Pattern(..), TopLevel(..), Type) import Compiler.TUI (TUIEvent(..)) import Compiler.Lexer (runLexer, LexError(..)) import Compiler.Parser (ParseError(..), parseTopLevel) -import Compiler.TypeChecker (infer, generalize, Env(..), TypeError(..), TCState (..), zonk) +import Compiler.TypeChecker (infer, generalize, Env(..), TypeError(..), TCState (..), builtinEnv, zonk) import Compiler.Elaborator (elabTopLevel, ElabError(..)) import Compiler.CGen (cgenProgram) @@ -35,7 +35,7 @@ data Terminal es = MkTerminal -- Maintains persistent type environment across submissions while sharing the -- same persistent unification state handle. replLoop :: forall st es. (st :> es) => Terminal es -> State TCState st -> Eff es () -replLoop term st = go (MkEnv []) +replLoop term st = go builtinEnv where go :: Env -> Eff es () go currentEnv = do diff --git a/src/Compiler/TypeChecker.hs b/src/Compiler/TypeChecker.hs index 494910d..444c35b 100644 --- a/src/Compiler/TypeChecker.hs +++ b/src/Compiler/TypeChecker.hs @@ -37,6 +37,21 @@ data Env = MkEnv { bindings :: ![(Text, Type)] } deriving (Show, Eq, Generic) +-- | Stable span used for compiler-provided builtin bindings. +builtinSpan :: Span +builtinSpan = MkSpan 0 0 0 0 + +-- | Builtin term environment shared by REPL, tests, and CLI pipelines. +-- +-- Phase 10 temporary contracts: +-- - @print : String -> String@ +-- - @readLn : String@ +builtinEnv :: Env +builtinEnv = MkEnv + [ ("print", TArrow builtinSpan (TString builtinSpan) (TString builtinSpan)) + , ("readLn", TString builtinSpan) + ] + -- | Localized type errors utilizing parsed @Spans@ data TypeError = MkTypeError { msg :: !Text @@ -317,9 +332,9 @@ infer st env ex expr = pure recTy -- | Type-check a binary arithmetic operation. --- Both operands must have the same numeric type (Int or Float); the --- result type matches the operands. Ambiguous meta-variable operands --- are constrained by the other operand when possible. +-- Both operands must have the same numeric type (Int or Float); the result type +-- matches the operands. Ambiguous meta-variable operands are constrained by the +-- other operand when possible. inferBinArith :: forall st r ex es. (st :> es, r :> es, ex :> es) => Text -> Span -> Expr -> Expr -> State TCState st -> Reader Env r -> Exception TypeError ex -> Eff es Type diff --git a/test/Test/CGen.hs b/test/Test/CGen.hs index f6061d2..1c00ab9 100644 --- a/test/Test/CGen.hs +++ b/test/Test/CGen.hs @@ -178,6 +178,30 @@ cgenUnitTests = @? "unary negation should parenthesize its full operand expression" assertCompilesWithGcc "arithmetic-neg-compound" out + , testCase "main declaration emits C entrypoint wrapper" $ + let out = cgenProgram [(defMainPrintDecl, Just (TString sp0))] + in do + T.isInfixOf "const char* lithic_main(void)" out + @? "zero-arg Lithic main should emit a callable C helper" + T.isInfixOf "int main(void)" out + @? "zero-arg Lithic main should trigger C main wrapper emission" + T.isInfixOf "(void)lithic_main();" out + @? "C main wrapper should invoke lithic_main" + + , testCase "print builtin lowers through runtime helper and compiles" $ + let out = cgenProgram [(defMainPrintDecl, Just (TString sp0))] + in do + T.isInfixOf "lithic_builtin_print" out + @? "print builtin should lower to the runtime print helper" + assertCompilesWithGcc "builtin-print" out + + , testCase "readLn builtin lowers through runtime helper and compiles" $ + let out = cgenProgram [(defReadLnDecl, Just (TString sp0))] + in do + T.isInfixOf "lithic_builtin_readln()" out + @? "readLn builtin should lower to the runtime readLn helper" + assertCompilesWithGcc "builtin-readln" out + , testCase "declarations are emitted in input order" $ let out = cgenProgram [(defADecl, Nothing), (defBDecl, Nothing)] posA = firstIndex "/* definition: a */" out @@ -572,6 +596,14 @@ cgenUnitTests = (CVar sp0 "x") (CLit sp0 (LInt 1))))) + defMainPrintDecl = + CDeclDef sp0 "main" + (CApp sp0 (CVar sp0 "print") (CLit sp0 (LString "hello"))) + + defReadLnDecl = + CDeclDef sp0 "readInput" + (CVar sp0 "readLn") + -- Float and String literal bodies defFloatDecl = CDeclDef sp0 "pi" diff --git a/test/Test/CLIEmitC.hs b/test/Test/CLIEmitC.hs index 45c0c17..5327945 100644 --- a/test/Test/CLIEmitC.hs +++ b/test/Test/CLIEmitC.hs @@ -169,6 +169,29 @@ cliEmitCTests = assertBool "generated C should include bool case guards" (T.isInfixOf "lithic_case_scrut" out) assertCompilesWithGcc outPath + + , testCase "terminal IO builtins emit C main wrapper and helper calls" $ do + cliPath <- getCliPath + withTempLithicSource "def main = print readLn\n" \srcPath -> + withTempOutputPath \outPath -> do + (ec, stdOut, stdErr) <- runEmitC cliPath ["--emit-c", srcPath, "-o", outPath] + case ec of + ExitSuccess -> pure () + ExitFailure _ -> + assertFailure $ + unlines + [ "Expected terminal IO fixture emit-c to succeed" + , "stdout: " <> stdOut + , "stderr: " <> stdErr + ] + out <- TIO.readFile outPath + assertBool "generated C should include C main wrapper" + (T.isInfixOf "int main(void)" out) + assertBool "generated C should call print helper" + (T.isInfixOf "lithic_builtin_print" out) + assertBool "generated C should call readLn helper" + (T.isInfixOf "lithic_builtin_readln()" out) + assertCompilesWithGcc outPath ] runEmitC :: FilePath -> [String] -> IO (ExitCode, String, String) diff --git a/test/Test/Golden.hs b/test/Test/Golden.hs index e99064a..40f0a04 100644 --- a/test/Test/Golden.hs +++ b/test/Test/Golden.hs @@ -21,7 +21,7 @@ import Compiler.Elaborator (ElabError(..), elabExpr) import Compiler.Evaluator (evalCore) import Compiler.Lexer (LexError(..), runLexer) import Compiler.Parser (ParseError(..), parseTopLevel) -import Compiler.TypeChecker (Env(..), TCState(..), TypeError(..), infer, zonk) +import Compiler.TypeChecker (TCState(..), TypeError(..), builtinEnv, infer, zonk) -- | Discover all golden tests under test/fixtures and pair them with the -- matching snapshots under test/golden. @@ -81,6 +81,6 @@ renderTypedPipeline ast = runPureEff $ evalState (MkTCState 0 IM.empty) \st -> try \ex -> - runReader (MkEnv []) \env -> do + runReader builtinEnv \env -> do rawTy <- infer st env ex ast zonk st rawTy \ No newline at end of file From 432aa782a3e9a383e69bf973a057564cc5492a67 Mon Sep 17 00:00:00 2001 From: "Eric Vincent (arch)" Date: Thu, 28 May 2026 14:12:51 -0400 Subject: [PATCH 2/2] phase10: address terminal IO review findings --- CHANGELOG.md | 4 ++ README.md | 4 +- app/Main.hs | 63 ++++++++++--------- docs/language-spec.md | 6 +- docs/phase10-c-codegen.md | 10 +-- src/Compiler/CGenPrelude.c | 7 +++ src/Compiler/REPL.hs | 52 ++++++++------- src/Compiler/TypeChecker.hs | 25 +++++++- test/Test/CGen.hs | 22 ++++++- test/Test/CLIEmitC.hs | 12 ++++ .../fail-reserved-builtin-binder.lithic | 1 + .../fail-reserved-builtin-binder.golden | 1 + 12 files changed, 145 insertions(+), 62 deletions(-) create mode 100644 test/fixtures/fail-reserved-builtin-binder.lithic create mode 100644 test/golden/fail-reserved-builtin-binder.golden diff --git a/CHANGELOG.md b/CHANGELOG.md index cbb14a4..443fc41 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,9 +7,13 @@ * Added first-pass C runtime helpers for `lithic_builtin_print` and `lithic_builtin_readln` in the embedded C prelude. * Lowered Core references to `readLn` and calls to `print` through the runtime helper ABI. * Added generated C `main(void)` wrapper emission when a zero-argument Lithic `main` declaration is present. + * Documented Phase 10 runtime ABI behavior for `readLn` EOF/allocation failure and returned string lifetime. + * Reserved `print` and `readLn` as builtin names for this phase and documented the reservation until builtins lower through explicit Core nodes. + * Hardened `readLn` CRLF handling so `\r\n` is consumed as one line terminator. * Test coverage: * Added focused CGen unit coverage for generated C entrypoint emission, `print` lowering, and `readLn` lowering, including gcc compile checks. * Added CLI `--emit-c` integration coverage for `def main = print readLn`, including generated C wrapper/helper assertions and gcc compile checks. + * Added regression coverage for reserved builtin declaration rejection and CRLF `readLn` behavior across consecutive reads. * Updated golden-test typing setup to use the shared builtin environment. * Validation: * Editor diagnostics: clean for touched source and test modules. diff --git a/README.md b/README.md index 249d721..6dc1069 100644 --- a/README.md +++ b/README.md @@ -33,7 +33,7 @@ Current `--emit-c` constraints: - Current path accepts named function declarations (`f x = ...`). - Emission is monomorphism-gated; unresolved polymorphism is reported as a codegen diagnostic. - A zero-argument Lithic declaration named `main` emits a C `main(void)` wrapper that invokes `lithic_main()`. -- First-pass terminal IO builtins are available in typed pipelines: `print : String -> String` writes a string without adding a newline, and `readLn : String` reads one line ending at carriage return or newline. +- First-pass terminal IO builtins are available in typed pipelines: `print : String -> String` writes a string without adding a newline, and `readLn : String` reads one line ending at carriage return or newline. These names are reserved in this phase and cannot be rebound by user code. Golden cases are discovered from `test/fixtures/*.lithic` and compared against matching snapshots in `test/golden/*.golden`. @@ -56,7 +56,7 @@ In the REPL: ``` Literal scrutinees are also handled directly, so `case True of True => 1` is accepted. - Primitive literals currently include `Int`, `Float`, `String`, and `Bool` (`True`/`False`). -- First-pass terminal IO builtins are available: `print : String -> String` and `readLn : String`. `print` does not append a newline; include `\n` in the string when needed. +- First-pass terminal IO builtins are available: `print : String -> String` and `readLn : String`. `print` does not append a newline; include `\n` in the string when needed. The names `print` and `readLn` are reserved until builtins become explicit Core nodes. - Prefix unary minus and infix subtraction are supported (`-x`, `x - y`). - Top-level declaration parsing (used by the file/golden pipeline) supports Phase 9F first-slice single-argument equation grouping, including pattern-headed arity-1 clauses. - `where` blocks on equation-style top-level declarations are supported (Phase 9G): bindings are layout-delimited and desugar to nested `let` bindings wrapping the equation body. Example: diff --git a/app/Main.hs b/app/Main.hs index 4eaec2e..c526134 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -26,7 +26,7 @@ import Compiler.Lexer (runLexer, LexError(..)) import Compiler.Parser (parseTopLevel, ParseError(..)) import Compiler.REPL (replLoop, runTerminalBrick) import Compiler.TUI (runTUI, TUIEvent(..)) -import Compiler.TypeChecker (TCState(..), TypeError(..), builtinEnv, infer, zonk) +import Compiler.TypeChecker (TCState(..), TypeError(..), builtinEnv, isBuiltinName, infer, zonk) import Compiler.TypeChecker () main :: IO () @@ -70,34 +70,39 @@ runEmitC srcPath outPath = do exitFailure TDecl decl -> case decl of - DeclDef _ (PVar _ _name) rhs -> do - -- Typecheck the declaration in a pure Bluefin context. - let tcResult = - runPureEff $ evalState (MkTCState 0 IM.empty) \st -> - try \ex -> - runReader builtinEnv \env -> do - rawTy <- infer st env ex rhs - zonk st rawTy - case tcResult of - Left tcErr -> do - TIO.putStrLn $ "Type error: " <> tcErr.msg - exitFailure - Right monoTy -> - case elabTopLevel (TDecl decl) of - Left elabErr -> do - TIO.putStrLn $ "Elaboration error: " <> elabErr.msg - exitFailure - Right coreTop -> - case coreTop of - -- elabTopLevel on a TDecl always produces CTDecl, but - -- pattern match kept explicit for exhaustivness safety. - Compiler.AST.Core.CTDecl coreDecl -> do - let cText = cgenProgram [(coreDecl, Just monoTy)] - TIO.writeFile outPath cText - TIO.putStrLn $ "C output written to " <> T.pack outPath - Compiler.AST.Core.CTExpr _ -> do - TIO.putStrLn "Internal error: expected CTDecl, got CTExpr." - exitFailure + DeclDef _ (PVar _ name) rhs -> do + if isBuiltinName name + then do + TIO.putStrLn $ "--emit-c cannot declare reserved builtin name: " <> name + exitFailure + else do + -- Typecheck the declaration in a pure Bluefin context. + let tcResult = + runPureEff $ evalState (MkTCState 0 IM.empty) \st -> + try \ex -> + runReader builtinEnv \env -> do + rawTy <- infer st env ex rhs + zonk st rawTy + case tcResult of + Left tcErr -> do + TIO.putStrLn $ "Type error: " <> tcErr.msg + exitFailure + Right monoTy -> + case elabTopLevel (TDecl decl) of + Left elabErr -> do + TIO.putStrLn $ "Elaboration error: " <> elabErr.msg + exitFailure + Right coreTop -> + case coreTop of + -- elabTopLevel on a TDecl always produces CTDecl, but + -- pattern match kept explicit for exhaustivness safety. + Compiler.AST.Core.CTDecl coreDecl -> do + let cText = cgenProgram [(coreDecl, Just monoTy)] + TIO.writeFile outPath cText + TIO.putStrLn $ "C output written to " <> T.pack outPath + Compiler.AST.Core.CTExpr _ -> do + TIO.putStrLn "Internal error: expected CTDecl, got CTExpr." + exitFailure _ -> do TIO.putStrLn "--emit-c current supports only named function declarations (f x = ...)." exitFailure diff --git a/docs/language-spec.md b/docs/language-spec.md index 2beaa9b..73bf2a0 100644 --- a/docs/language-spec.md +++ b/docs/language-spec.md @@ -235,7 +235,9 @@ Builtin term environment currently includes: | Name | Type | Implementation Status | Notes | | --- | --- | --- | --- | | `print` | `String -> String` | Implemented | First-pass terminal IO builtin. C lowering writes the string to stdout without appending a newline and returns the original string handle. | -| `readLn` | `String` | Implemented | First-pass terminal IO builtin. C lowering reads one line from stdin, stopping on carriage return or newline. | +| `readLn` | `String` | Implemented | First-pass terminal IO builtin. C lowering reads one line from stdin, stopping on carriage return or newline. At the Phase 10 C ABI boundary, EOF before any character or allocation failure returns the sentinel handle `0`; successful reads return a heap-allocated NUL-terminated string handle. Returned strings currently follow the runtime prelude's malloc-and-leak ownership model. | + +The names `print` and `readLn` are reserved in this phase. User code cannot bind or declare these names until builtin operations are represented explicitly during elaboration/Core lowering instead of by raw-name CGen recognition. ```text TopLevel ::= Decl | Expr @@ -415,6 +417,8 @@ Current C2.1 codegen diagnostic note: 2. When a declaration type includes unresolved polymorphism at the CGen boundary, the emitted `[C]` block includes: `codegen error: program is not fully monomorphic; instantiate before code generation`. 3. A zero-argument Lithic declaration named `main` emits a generated C `main(void)` wrapper that invokes `lithic_main()`. +4. Phase 10 terminal IO builtins use the C runtime prelude's `intptr_t` handle ABI. `print` treats handle `0` as a no-op/failure sentinel and returns `0`; `readLn` returns `0` on EOF before any character or allocation failure. +5. `readLn` treats CRLF as one line terminator at the C runtime boundary by consuming an optional `\n` after `\r`. Contract requirements: 1. Diagnostics carry precise `Span` whenever an originating token/node exists. diff --git a/docs/phase10-c-codegen.md b/docs/phase10-c-codegen.md index 4abb1d8..34fc11d 100644 --- a/docs/phase10-c-codegen.md +++ b/docs/phase10-c-codegen.md @@ -1,16 +1,16 @@ # Phase 10 Scaffold: C Code Generation First Pass -Status: C2.2 call/case/variant/select lowering merged on main (PR #28) + C4.3 fixture-level emit/compile integration landed (2026-05-23) + C3.1 compile-time prelude template embedding and C3.2 first-pass prelude safety hardening landed + expanded C4.4 compile/link/run sanity gate (2026-05-24) + C3.3 helper-contract depth landed (2026-05-25) + C3.4 record-init failure propagation and CLI long-field fixture coverage landed (2026-05-25) + C3.5 case-expression and expression-value lowering depth landed (2026-05-26) + C3.6 arithmetic lowering landed (2026-05-27) + C3.7 first-pass terminal IO builtin lowering in progress (2026-05-27) -Branch: feat/phase10-c3-7-io-main-print-readln +Status: C2.2 call/case/variant/select lowering merged on main (PR #28) + C4.3 fixture-level emit/compile integration landed (2026-05-23) + C3.1 compile-time prelude template embedding and C3.2 first-pass prelude safety hardening landed + expanded C4.4 compile/link/run sanity gate (2026-05-24) + C3.3 helper-contract depth landed (2026-05-25) + C3.4 record-init failure propagation and CLI long-field fixture coverage landed (2026-05-25) + C3.5 case-expression and expression-value lowering depth landed (2026-05-26) + C3.6 arithmetic lowering landed (2026-05-27) + C3.7 first-pass terminal IO builtin lowering landed (2026-05-27) +Branch: mainline phase status, not branch-specific WIP tracking. -Next prep checkpoint: C3.7 terminal IO builtin validation. +Next prep checkpoint: reserve builtin-name semantics and IO helper edge-case hardening. -## Immediate Next Slice (C3.7 — Terminal IO Builtins) +## Landed Slice (C3.7 — Terminal IO Builtins) Goal: provide the smallest end-to-end terminal IO surface through the existing typed and C backend pipelines without introducing a general effect system yet. -Implemented direction for this slice: +Implemented behavior for this slice: 1. Add shared builtin term bindings for `print : String -> String` and `readLn : String`. 2. Lower `print` calls and `readLn` references through explicit C prelude helpers. diff --git a/src/Compiler/CGenPrelude.c b/src/Compiler/CGenPrelude.c index 6ec3b15..397a782 100644 --- a/src/Compiler/CGenPrelude.c +++ b/src/Compiler/CGenPrelude.c @@ -410,6 +410,13 @@ static inline intptr_t lithic_builtin_readln(void) { buf[len++] = (char)ch; } + if (ch == '\r') { + int next = fgetc(stdin); + if (next != '\n' && next != EOF) { + ungetc(next, stdin); + } + } + if (ch == EOF && len == 0) { free(buf); return (intptr_t)0; diff --git a/src/Compiler/REPL.hs b/src/Compiler/REPL.hs index 3e8ae0a..a56b81c 100644 --- a/src/Compiler/REPL.hs +++ b/src/Compiler/REPL.hs @@ -20,7 +20,7 @@ import Compiler.AST (Decl(..), Pattern(..), TopLevel(..), Type) import Compiler.TUI (TUIEvent(..)) import Compiler.Lexer (runLexer, LexError(..)) import Compiler.Parser (ParseError(..), parseTopLevel) -import Compiler.TypeChecker (infer, generalize, Env(..), TypeError(..), TCState (..), builtinEnv, zonk) +import Compiler.TypeChecker (infer, generalize, Env(..), TypeError(..), TCState (..), builtinEnv, isBuiltinName, zonk) import Compiler.Elaborator (elabTopLevel, ElabError(..)) import Compiler.CGen (cgenProgram) @@ -111,30 +111,40 @@ replLoop term st = go builtinEnv handleDeclSubmission env decl = case decl of DeclSig _ name _ -> do - term.output $ - "[Decl] " <> name <> " (signature accepted; persistence deferred in this slice)" - emitCodeGen (TDecl decl) Nothing - pure env + if isBuiltinName name + then do + term.output $ "Error: cannot declare reserved builtin name: " <> name + pure env + else do + term.output $ + "[Decl] " <> name <> " (signature accepted; persistence deferred in this slice)" + emitCodeGen (TDecl decl) Nothing + pure env DeclDef _ pat rhs -> case pat of PVar _ name -> do - tcResult <- try \ex -> - runReader env \envHandle -> do - rawTy <- infer st envHandle ex rhs - monoTy <- zonk st rawTy - generalize st env monoTy - - case tcResult of - Left err -> do - term.output $ "Type Error: " <> err.msg <> " at " <> T.pack (show err.span) - pure env - Right polyTy -> do - let updatedEnv = MkEnv ((name, polyTy) : env.bindings) - term.output $ "[Decl] " <> name - term.output $ "[Type] " <> T.pack (show polyTy) - emitCodeGen (TDecl decl) (Just polyTy) - pure updatedEnv + if isBuiltinName name + then do + term.output $ "Error: cannot declare reserved builtin name: " <> name + pure env + else do + tcResult <- try \ex -> + runReader env \envHandle -> do + rawTy <- infer st envHandle ex rhs + monoTy <- zonk st rawTy + generalize st env monoTy + + case tcResult of + Left err -> do + term.output $ "Type Error: " <> err.msg <> " at " <> T.pack (show err.span) + pure env + Right polyTy -> do + let updatedEnv = MkEnv ((name, polyTy) : env.bindings) + term.output $ "[Decl] " <> name + term.output $ "[Type] " <> T.pack (show polyTy) + emitCodeGen (TDecl decl) (Just polyTy) + pure updatedEnv _ -> do term.output "Error: top-level declaration currently requires a variable binder." diff --git a/src/Compiler/TypeChecker.hs b/src/Compiler/TypeChecker.hs index 444c35b..4ad7d80 100644 --- a/src/Compiler/TypeChecker.hs +++ b/src/Compiler/TypeChecker.hs @@ -52,6 +52,22 @@ builtinEnv = MkEnv , ("readLn", TString builtinSpan) ] +-- | Return True for names reserved by the compiler-provided builtin environment. +-- +-- Phase 10 reserves these names so CGen can lower builtins without ambiguity +-- until builtins become explicit Core nodes during elaboration. +isBuiltinName :: Text -> Bool +isBuiltinName name = name == "print" || name == "readLn" + +-- | Reject attempts to bind a compiler-reserved builtin name. +rejectBuiltinBinder + :: forall ex es. (ex :> es) + => Exception TypeError ex -> Span -> Text -> Eff es () +rejectBuiltinBinder ex sp name = + if isBuiltinName name + then throw ex $ MkTypeError ("Cannot bind reserved builtin name: " <> name) sp + else pure () + -- | Localized type errors utilizing parsed @Spans@ data TypeError = MkTypeError { msg :: !Text @@ -123,7 +139,9 @@ checkPattern checkPattern st ex pat expectedTy = do forcedTy <- force st expectedTy case pat of - PVar _ x -> pure [(x, forcedTy)] + PVar sp x -> do + rejectBuiltinBinder ex sp x + pure [(x, forcedTy)] PWildcard _ -> pure [] PLit sp lit -> do let litTy = case lit of @@ -239,7 +257,8 @@ infer st env ex expr = -- Let-generalization is restricted to simple variable bindings bindings <- case pat of - PVar _ name -> do + PVar sp name -> do + rejectBuiltinBinder ex sp name e <- ask env polyTy <- generalize st e zonkedValTy pure [(name, polyTy)] @@ -365,7 +384,7 @@ inferBinArith opName sp e1 e2 st env ex = do (_, NumericNonNumeric) -> throw ex $ MkTypeError ("Right operand of " <> opName <> " must be numeric.") (getSpan e2) - + -- | Check that an expression satisfies an expected type. check :: forall st env ex es. (st :> es, env :> es, ex :> es) diff --git a/test/Test/CGen.hs b/test/Test/CGen.hs index 1c00ab9..6a0598b 100644 --- a/test/Test/CGen.hs +++ b/test/Test/CGen.hs @@ -202,6 +202,20 @@ cgenUnitTests = @? "readLn builtin should lower to the runtime readLn helper" assertCompilesWithGcc "builtin-readln" out + , testCase "readLn consumes CRLF as a single line terminator" $ + let out = cgenProgram [(defReadLnDecl, Just (TString sp0))] + harness = T.unlines + [ "#include " + , "#include " + , "extern const char *lithic_readInput(void);" + , "int main(void) {" + , " const char *first = lithic_readInput();" + , " const char *second = lithic_readInput();" + , " return (first != 0 && second != 0 && strcmp(first, \"one\") == 0 && strcmp(second, \"two\") == 0) ? 0 : 1;" + , "}" + ] + in assertCompilesLinksAndRunsWithGccInput "builtin-readln-crlf" out harness "one\r\ntwo\n" + , testCase "declarations are emitted in input order" $ let out = cgenProgram [(defADecl, Nothing), (defBDecl, Nothing)] posA = firstIndex "/* definition: a */" out @@ -729,6 +743,12 @@ assertCompilesWithGcc tag cSrc = -- This provides a narrow C4.4 runtime sanity gate beyond object-only checks. assertCompilesLinksAndRunsWithGcc :: String -> T.Text -> T.Text -> IO () assertCompilesLinksAndRunsWithGcc tag cSrc harnessSrc = + assertCompilesLinksAndRunsWithGccInput tag cSrc harnessSrc "" + +-- | Compile generated C, link with a tiny harness, and execute the binary with +-- supplied stdin. +assertCompilesLinksAndRunsWithGccInput :: String -> T.Text -> T.Text -> String -> IO () +assertCompilesLinksAndRunsWithGccInput tag cSrc harnessSrc stdinText = withTempArtifact tag ".c" \cPath -> withTempArtifact (tag <> "-harness") ".c" \harnessPath -> withTempArtifact tag ".out" \exePath -> do @@ -765,7 +785,7 @@ assertCompilesLinksAndRunsWithGcc tag cSrc harnessSrc = , compileErr ]) - (runEc, runOut, runErr) <- readProcessWithExitCode exePath [] "" + (runEc, runOut, runErr) <- readProcessWithExitCode exePath [] stdinText case runEc of ExitSuccess -> pure () ExitFailure _ -> diff --git a/test/Test/CLIEmitC.hs b/test/Test/CLIEmitC.hs index 5327945..5146e0f 100644 --- a/test/Test/CLIEmitC.hs +++ b/test/Test/CLIEmitC.hs @@ -192,6 +192,18 @@ cliEmitCTests = assertBool "generated C should call readLn helper" (T.isInfixOf "lithic_builtin_readln()" out) assertCompilesWithGcc outPath + + , testCase "--emit-c rejects declarations that shadow reserved builtins" $ do + cliPath <- getCliPath + withTempLithicSource "def print = 1\n" \srcPath -> do + (ec, stdOut, stdErr) <- runEmitC cliPath ["--emit-c", srcPath] + case ec of + ExitSuccess -> + assertFailure "Expected --emit-c to reject a declaration named print" + ExitFailure _ -> do + let msg = stdOut <> stdErr + assertBool "failure should mention reserved builtin name" + ("reserved builtin name" `elemIn` msg) ] runEmitC :: FilePath -> [String] -> IO (ExitCode, String, String) diff --git a/test/fixtures/fail-reserved-builtin-binder.lithic b/test/fixtures/fail-reserved-builtin-binder.lithic new file mode 100644 index 0000000..d1c53ee --- /dev/null +++ b/test/fixtures/fail-reserved-builtin-binder.lithic @@ -0,0 +1 @@ +\print => print diff --git a/test/golden/fail-reserved-builtin-binder.golden b/test/golden/fail-reserved-builtin-binder.golden new file mode 100644 index 0000000..e9efb4b --- /dev/null +++ b/test/golden/fail-reserved-builtin-binder.golden @@ -0,0 +1 @@ +Type Error: Cannot bind reserved builtin name: print at [1,2]..[1,6]