Phase 10 C3.7 terminal IO builtins

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:

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:

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

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 <pattern> = 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 <pattern1> <pattern2> ... = 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.

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.

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)

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.

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;

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

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