Skip to content

Commit f4bdce0

Browse files
authored
binop except assign and conditionals (#141)
1 parent 1684a2b commit f4bdce0

File tree

47 files changed

+3023
-74
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

47 files changed

+3023
-74
lines changed

CHANGELOG.md

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,17 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
2424
- Execution functions use target's release optimization so proofs cover actual deployed code
2525
- `OptLevel` is currently metadata only; optimization passes planned for future
2626
- Add validation guards in `codegen()`: reject proof mode with non-Wasm32 targets, reject Soroban with non-det operations ([#97])
27+
- Add binary and unary expression lowering to WebAssembly codegen ([#140])
28+
- All arithmetic operators (`+`, `-`, `*`, `/`, `%`) for i32 and i64, signed and unsigned variants
29+
- All comparison operators (`==`, `!=`, `<`, `<=`, `>`, `>=`) with correct sign-sensitive dispatch
30+
- All logical operators (`&&`, `||`) lowered as bitwise `i32.and`/`i32.or` (bool operands guaranteed by type-checker)
31+
- All bitwise operators (`&`, `|`, `^`) and shift operators (`<<`, `>>`) for i32 and i64
32+
- Unary negation (`-x`) via `0 - x` idiom (no native WASM integer negate instruction)
33+
- Logical not (`!x`) via `i32.eqz`
34+
- Bitwise not (`~x`) via `x ^ -1` idiom (works for both i32 and i64)
35+
- Parenthesized expressions lowered transparently (no extra instructions emitted)
36+
- Variable definition initializers now accept any value-producing expression (not just literals/identifiers/uzumaki)
37+
- `Pow` operator (`**`) deferred — no native WASM instruction
2738
- Add function parameter lowering and function call support to WebAssembly codegen ([#136])
2839
- Function parameters mapped to WASM local indices `0..n`; body locals start at `n`
2940
- Pre-scan builds `func_name_to_idx` map for forward reference support
@@ -317,3 +328,4 @@ Initial tagged release.
317328
[#134]: https://github.com/Inferara/inference/pull/135
318329
[#136]: https://github.com/Inferara/inference/pull/136
319330
[#138]: https://github.com/Inferara/inference/pull/138
331+
[#140]: https://github.com/Inferara/inference/pull/140

core/ast/docs/nodes.md

Lines changed: 27 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -585,14 +585,14 @@ pub struct BinaryExpression {
585585
**Operators:**
586586
```rust
587587
pub enum OperatorKind {
588-
Pow, // **
588+
Pow, // ** — parsed but NOT yet lowered in WASM codegen (todo!)
589589
Add, // +
590590
Sub, // -
591591
Mul, // *
592-
Div, // / (Added in issue #86)
592+
Div, // /
593593
Mod, // %
594-
And, // &&
595-
Or, // ||
594+
And, // && — lowers to i32.and (no short-circuit)
595+
Or, // || — lowers to i32.or (no short-circuit)
596596
Eq, // ==
597597
Ne, // !=
598598
Lt, // <
@@ -602,19 +602,31 @@ pub enum OperatorKind {
602602
BitAnd, // &
603603
BitOr, // |
604604
BitXor, // ^
605-
BitNot, // ~
605+
BitNot, // design inconsistency — never produced for BinaryExpression;
606+
// the ~ token is always a PrefixUnaryExpression (UnaryOperatorKind::BitNot)
606607
Shl, // <<
607608
Shr, // >>
608609
}
609610
```
610611

612+
**Codegen notes:**
613+
614+
- `Pow` (`**`) is not yet implemented in the WASM backend. Attempting to lower a
615+
binary expression with this operator will panic with a `todo!()`.
616+
- `BitNot` should not appear in any `BinaryExpression` node. The `~` token is
617+
always parsed as a prefix unary expression and stored as
618+
`UnaryOperatorKind::BitNot`. The `OperatorKind::BitNot` variant is a design
619+
inconsistency that will be removed in a future cleanup.
620+
- `And` and `Or` lower to WebAssembly `i32.and`/`i32.or` bitwise instructions.
621+
Both operands are always evaluated — there is no short-circuit evaluation.
622+
611623
**Example source:**
612624
```inference
613625
x + y
614626
a * b + c
615-
a / b // Division operator (issue #86)
627+
a / b
616628
flag && (count > 0)
617-
x % 2 == 0 // Modulo
629+
x % 2 == 0
618630
```
619631

620632
### PrefixUnaryExpression
@@ -630,19 +642,22 @@ pub struct PrefixUnaryExpression {
630642
}
631643

632644
pub enum UnaryOperatorKind {
633-
Not, // ! - Logical negation
634-
Neg, // - - Numeric negation (Added in issue #86)
635-
BitNot, // ~ - Bitwise NOT (Added in issue #86)
645+
Not, // ! - Logical negation — lowers to i32.eqz
646+
Neg, // - - Numeric negation — lowers to (0 - expr) using i32.sub or i64.sub
647+
BitNot, // ~ - Bitwise NOT — lowers to (expr ^ -1) using i32.xor or i64.xor
636648
}
637649
```
638650

651+
Note: `~` always produces a `PrefixUnaryExpression` with `UnaryOperatorKind::BitNot`.
652+
It is never stored as `OperatorKind::BitNot` in a `BinaryExpression`.
653+
639654
**Example source:**
640655
```inference
641656
!flag // Logical NOT
642657
!(x > 0)
643-
-x // Numeric negation (issue #86)
658+
-x // Numeric negation
644659
-42
645-
~mask // Bitwise NOT (issue #86)
660+
~mask // Bitwise NOT
646661
~0xFF
647662
```
648663

core/ast/src/arena.rs

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,12 @@ pub struct Arena {
2020
}
2121

2222
impl Arena {
23+
/// Returns all `SourceFile` nodes in the arena, sorted by node ID.
24+
///
25+
/// In a single-file compilation the result contains exactly one element.
26+
/// In multi-file compilation (via `ParserContext`) it contains one entry per
27+
/// parsed file. Node ID order matches the order in which files were added to
28+
/// the builder.
2329
#[must_use]
2430
pub fn source_files(&self) -> Vec<Rc<SourceFile>> {
2531
self.list_nodes_cmp(|node| {
@@ -31,6 +37,11 @@ impl Arena {
3137
})
3238
.collect()
3339
}
40+
41+
/// Returns all `FunctionDefinition` nodes in the arena, sorted by node ID.
42+
///
43+
/// This includes both free functions and struct methods. Node ID order
44+
/// matches source order within each file.
3445
#[must_use]
3546
pub fn functions(&self) -> Vec<Rc<FunctionDefinition>> {
3647
self.list_nodes_cmp(|node| {
@@ -68,6 +79,10 @@ impl Arena {
6879
}
6980
}
7081

82+
/// Returns a clone of the node with the given ID, or `None` if not present.
83+
///
84+
/// This is an O(1) hash map lookup. Cloning an `AstNode` is cheap because
85+
/// the heavy node data is behind `Rc`.
7186
#[must_use]
7287
pub fn find_node(&self, id: u32) -> Option<AstNode> {
7388
self.nodes.get(&id).cloned()
@@ -153,6 +168,11 @@ impl Arena {
153168
}
154169
}
155170

171+
/// Returns all descendants of the node with the given ID that satisfy `comparator`.
172+
///
173+
/// Performs a depth-first traversal starting from `id`, collecting every
174+
/// node (including the root itself) for which `comparator` returns `true`.
175+
/// Returns an empty `Vec` if the starting node does not exist.
156176
pub fn get_children_cmp<F>(&self, id: u32, comparator: F) -> Vec<AstNode>
157177
where
158178
F: Fn(&AstNode) -> bool,
@@ -178,6 +198,7 @@ impl Arena {
178198
result
179199
}
180200

201+
/// Returns all `TypeDefinition` nodes in the arena, sorted by node ID.
181202
#[must_use]
182203
pub fn list_type_definitions(&self) -> Vec<Rc<TypeDefinition>> {
183204
self.list_nodes_cmp(|node| {
@@ -190,6 +211,19 @@ impl Arena {
190211
.collect()
191212
}
192213

214+
/// Returns all nodes that satisfy `fn_predicate`, sorted by node ID.
215+
///
216+
/// Unlike `get_children_cmp`, this scans the entire arena (not just a
217+
/// subtree) and always returns results in ascending node ID order. Use this
218+
/// for global queries such as "find all binary expressions".
219+
///
220+
/// # Example
221+
///
222+
/// ```ignore
223+
/// let binary_exprs = arena.filter_nodes(|node| {
224+
/// matches!(node, AstNode::Expression(Expression::Binary(_)))
225+
/// });
226+
/// ```
193227
pub fn filter_nodes<T: Fn(&AstNode) -> bool>(&self, fn_predicate: T) -> Vec<AstNode> {
194228
let mut entries: Vec<_> = self.nodes.iter().collect();
195229
entries.sort_unstable_by_key(|(id, _)| *id);

core/cli/README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -182,7 +182,7 @@ infc example.inf --codegen -v
182182
```
183183
Parsed: example.inf
184184
Analyzed: example.inf
185-
WASM generated
185+
Codegen complete
186186
V generated at: out/example.v
187187
```
188188

core/cli/src/main.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@
2727
//!
2828
//! 3. **Codegen** (`--codegen`) – Emits WebAssembly binary
2929
//! - Generates WebAssembly binary from typed AST
30-
//! - Supports non-deterministic instructions (uzumaki, forall, exists)
30+
//! - Supports non-deterministic instructions (uzumaki, forall, exists, assume, unique)
3131
//! - Optionally translates to Rocq (.v) format for formal verification
3232
//!
3333
//! ## Phase Execution

core/type-checker/src/lib.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -133,6 +133,10 @@ impl Default for TypeCheckerBuilder<TypeCheckerInitState> {
133133
}
134134

135135
impl TypeCheckerBuilder<TypeCheckerInitState> {
136+
/// Create a new builder in the initial (untyped) state.
137+
///
138+
/// Prefer [`TypeCheckerBuilder::build_typed_context`] for the common case
139+
/// where you have an arena ready to check immediately.
136140
#[must_use]
137141
pub fn new() -> Self {
138142
TypeCheckerBuilder {

core/type-checker/src/type_info.rs

Lines changed: 47 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -179,20 +179,50 @@ impl std::str::FromStr for NumberType {
179179
}
180180
}
181181

182+
/// Discriminates the semantic category of a [`TypeInfo`] value.
183+
///
184+
/// Variants mirror the type system of the Inference language.
185+
/// See the module-level documentation for the full hierarchy.
182186
#[derive(Debug, Eq, PartialEq, Clone, Hash)]
183187
pub enum TypeInfoKind {
188+
/// The unit type `unit` — the implicit return type of void functions.
184189
Unit,
190+
/// The boolean type `bool`.
185191
Bool,
192+
/// The string type `string` (UTF-8, partial support).
186193
String,
194+
/// A numeric integer type (signed or unsigned, 8–64 bit).
187195
Number(NumberType),
196+
/// A user-defined type referenced by name that has not yet been resolved
197+
/// to a struct or enum entry in the symbol table.
198+
///
199+
/// After type registration this should have been replaced by
200+
/// [`Struct`](TypeInfoKind::Struct) or [`Enum`](TypeInfoKind::Enum).
188201
Custom(String),
202+
/// A fixed-size array: element type and element count.
189203
Array(Box<TypeInfo>, u32),
204+
/// An unresolved generic type parameter (e.g. `T` in `fn foo<T>(x: T) -> T`).
205+
///
206+
/// Replaced by a concrete type after type-parameter substitution.
190207
Generic(String),
208+
/// A two-segment qualified type name (`module::Type`) from the source.
191209
QualifiedName(String),
210+
/// A single-segment qualified type reference carrying an alias prefix.
192211
Qualified(String),
212+
/// A function type. The inner string takes one of three forms depending on
213+
/// how the function was referenced:
214+
///
215+
/// - `"FunctionName"` — a free function referenced by name (from `function_definition.name()`)
216+
/// - `"ReceiverType::MethodName"` — a method or type-member access expression
217+
/// - `"Function<N, ReturnType>"` — a function-type literal from a `Type::Function` node
218+
///
219+
/// Used to annotate function-name expressions in the `TypedContext`.
193220
Function(String),
221+
/// A resolved struct type, carrying the struct's canonical name.
194222
Struct(String),
223+
/// A resolved enum type, carrying the enum's canonical name.
195224
Enum(String),
225+
/// A spec (specification) type, carrying the spec's canonical name.
196226
Spec(String),
197227
}
198228

@@ -267,11 +297,19 @@ impl TypeInfoKind {
267297
}
268298
}
269299

300+
/// The semantic type of a value expression after type checking.
301+
///
302+
/// Produced by [`TypeInfo::new`] from AST [`Type`] nodes and stored in
303+
/// [`TypedContext`](crate::typed_context::TypedContext) keyed by AST node ID.
270304
#[derive(Debug, Eq, PartialEq, Clone, Hash)]
271305
pub struct TypeInfo {
306+
/// The concrete type category (e.g. `Number(I32)`, `Struct("Point")`).
272307
pub kind: TypeInfoKind,
308+
/// Names of any unresolved generic type parameters carried by this type
309+
/// (e.g. `["T"]` for a value whose type is a generic parameter `T`).
310+
///
311+
/// After all type parameters have been substituted this will be empty.
273312
pub type_params: Vec<String>,
274-
// (Field type information could be added here if needed for struct field checking.)
275313
}
276314

277315
impl Default for TypeInfo {
@@ -299,6 +337,10 @@ impl Display for TypeInfo {
299337
}
300338

301339
impl TypeInfo {
340+
/// Construct a `bool` `TypeInfo` value.
341+
///
342+
/// Shorthand for the common case of representing a boolean result,
343+
/// for example when checking conditions or logical operator results.
302344
#[must_use]
303345
pub fn boolean() -> Self {
304346
Self {
@@ -315,6 +357,10 @@ impl TypeInfo {
315357
}
316358
}
317359

360+
/// Convert an AST [`Type`] to its semantic `TypeInfo` representation.
361+
///
362+
/// Equivalent to `TypeInfo::new_with_type_params(ty, &[])` — use this
363+
/// when there are no in-scope generic type parameters to consider.
318364
#[must_use]
319365
pub fn new(ty: &Type) -> Self {
320366
Self::new_with_type_params(ty, &[])

core/type-checker/src/typed_context.rs

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,16 @@ use inference_ast::{
9191
};
9292
use rustc_hash::FxHashMap;
9393

94+
/// Central store produced by type checking.
95+
///
96+
/// `TypedContext` combines the original parsed [`Arena`] with a map from
97+
/// AST node IDs to their inferred [`TypeInfo`] values and the populated
98+
/// [`SymbolTable`]. It is the primary output of
99+
/// [`TypeCheckerBuilder::build_typed_context`](crate::TypeCheckerBuilder::build_typed_context)
100+
/// and the primary input to subsequent compiler phases such as WASM code generation.
101+
///
102+
/// See the module-level documentation for details on which expressions receive
103+
/// type information and which are structural.
94104
#[derive(Default)]
95105
pub struct TypedContext {
96106
pub(crate) symbol_table: SymbolTable,
@@ -372,10 +382,18 @@ impl TypedContext {
372382
}
373383
}
374384

375-
/// Information about an expression missing its type after type checking.
385+
/// Describes a value expression that has no [`TypeInfo`] entry after type checking.
386+
///
387+
/// A non-empty list returned by
388+
/// [`TypedContext::find_untyped_expressions`] indicates a bug in the type
389+
/// checker: every value expression should be annotated by the time inference
390+
/// completes.
376391
#[derive(Debug)]
377392
pub struct MissingExpressionType {
393+
/// AST node ID of the untyped expression.
378394
pub id: u32,
395+
/// Human-readable name of the expression variant (e.g. `"Binary"`, `"FunctionCall"`).
379396
pub kind: String,
397+
/// Source location of the expression, for diagnostic output.
380398
pub location: Location,
381399
}

0 commit comments

Comments
 (0)