Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,23 @@
# 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.
* 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.

## 0.9.18.0 -- 2026-05-27 (Phase 10 C3.6 Arithmetic Lowering)

* Phase 10 C3.6 arithmetic lowering:
Expand Down
3 changes: 3 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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. 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`.

Expand All @@ -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. 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:
Expand Down
63 changes: 34 additions & 29 deletions app/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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, isBuiltinName, infer, zonk)
import Compiler.TypeChecker ()

main :: IO ()
Expand Down Expand Up @@ -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 (MkEnv []) \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
Expand Down
17 changes: 15 additions & 2 deletions docs/language-spec.md
Original file line number Diff line number Diff line change
@@ -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.

Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -229,6 +230,15 @@ 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. 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

Expand Down Expand Up @@ -406,6 +416,9 @@ 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()`.
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.
Expand Down
20 changes: 16 additions & 4 deletions docs/phase10-c-codegen.md
Original file line number Diff line number Diff line change
@@ -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 landed (2026-05-27)
Branch: mainline phase status, not branch-specific WIP tracking.

Next prep checkpoint: `docs/phase10-c3-6-prep.md`.
Next prep checkpoint: reserve builtin-name semantics and IO helper edge-case hardening.

## Immediate Next Slice (C3.6 — Arithmetic Core/CGen Lowering)
## 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 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.
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.
Expand Down
2 changes: 1 addition & 1 deletion lithic.cabal
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
63 changes: 53 additions & 10 deletions src/Compiler/CGen.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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; |]
Expand Down Expand Up @@ -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; |]
Comment thread
efvincent marked this conversation as resolved.

-- Target 4: let-binding to stack-allocated local.
-- Only CPVar patterns are precisely lowered; other patterns fall through
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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"

Expand Down Expand Up @@ -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.
Expand Down
65 changes: 65 additions & 0 deletions src/Compiler/CGenPrelude.c
Original file line number Diff line number Diff line change
Expand Up @@ -361,6 +361,71 @@ 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;
}

Comment thread
efvincent marked this conversation as resolved.
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 == '\r') {
int next = fgetc(stdin);
if (next != '\n' && next != EOF) {
ungetc(next, stdin);
}
}

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;
Expand Down
Loading