|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +// |
| 4 | +// Ast.res — Abstract Syntax Tree for typed-wasm (.twasm) programs. |
| 5 | +// |
| 6 | +// This module defines the typed AST that the parser produces from tokenised |
| 7 | +// source text. The AST mirrors the grammar in spec/grammar.ebnf. |
| 8 | +// |
| 9 | +// Every node carries a source location (loc) for error reporting. |
| 10 | + |
| 11 | +/// Source location. |
| 12 | +type loc = Lexer.loc |
| 13 | + |
| 14 | +/// Located AST node. |
| 15 | +type located<'a> = { |
| 16 | + node: 'a, |
| 17 | + loc: loc, |
| 18 | +} |
| 19 | + |
| 20 | +// ============================================================================ |
| 21 | +// Top-Level Declarations |
| 22 | +// ============================================================================ |
| 23 | + |
| 24 | +/// A typed-wasm module: a list of top-level declarations. |
| 25 | +type rec module_ = { |
| 26 | + declarations: array<located<declaration>>, |
| 27 | +} |
| 28 | + |
| 29 | +/// Top-level declaration. |
| 30 | +and declaration = |
| 31 | + | RegionDecl(regionDecl) |
| 32 | + | ImportRegionDecl(importRegionDecl) |
| 33 | + | ExportRegionDecl(exportRegionDecl) |
| 34 | + | FunctionDecl(functionDecl) |
| 35 | + | MemoryDecl(memoryDecl) |
| 36 | + | InvariantDecl(invariantDecl) |
| 37 | + |
| 38 | +// ============================================================================ |
| 39 | +// Region Declarations (Section 2 of grammar) |
| 40 | +// ============================================================================ |
| 41 | + |
| 42 | +/// A region declaration: `region Name[count] { fields; align N; invariant { ... } }` |
| 43 | +and regionDecl = { |
| 44 | + name: string, |
| 45 | + instanceCount: option<located<expr>>, |
| 46 | + fields: array<located<fieldDecl>>, |
| 47 | + alignment: option<int>, |
| 48 | + invariants: array<located<invariantExpr>>, |
| 49 | +} |
| 50 | + |
| 51 | +/// A field within a region: `name: type where constraints;` |
| 52 | +and fieldDecl = { |
| 53 | + name: string, |
| 54 | + fieldType: located<fieldType>, |
| 55 | + constraints: array<located<constraintExpr>>, |
| 56 | +} |
| 57 | + |
| 58 | +/// Field types. |
| 59 | +and fieldType = |
| 60 | + | Primitive(primitiveType) |
| 61 | + | RegionRef(string) // @RegionName — embedded region |
| 62 | + | PointerType(pointerKind, located<fieldType>) // ptr<T>, ref<T>, unique<T> |
| 63 | + | OptionalType(located<fieldType>) // opt<T> |
| 64 | + | ArrayFieldType(located<fieldType>, located<expr>) // T[N] |
| 65 | + | UnionType(array<located<variantDecl>>) |
| 66 | + |
| 67 | +/// WASM primitive types. |
| 68 | +and primitiveType = |
| 69 | + | I8 |
| 70 | + | I16 |
| 71 | + | I32 |
| 72 | + | I64 |
| 73 | + | U8 |
| 74 | + | U16 |
| 75 | + | U32 |
| 76 | + | U64 |
| 77 | + | F32 |
| 78 | + | F64 |
| 79 | + | Bool |
| 80 | + |
| 81 | +/// Pointer kinds. |
| 82 | +and pointerKind = |
| 83 | + | PtrOwning // ptr<T> — owning, must free |
| 84 | + | RefBorrow // ref<T> — borrowing, no free |
| 85 | + | UniqueExcl // unique<T> — exclusive owning |
| 86 | + |
| 87 | +/// Union variant. |
| 88 | +and variantDecl = { |
| 89 | + tag: string, |
| 90 | + variantType: located<fieldType>, |
| 91 | +} |
| 92 | + |
| 93 | +/// Field constraint expressions. |
| 94 | +and constraintExpr = |
| 95 | + | RangeConstraint(located<expr>, string, located<expr>) // lo <= field <= hi |
| 96 | + | PredicateConstraint(string, array<located<expr>>) |
| 97 | + | AlignConstraint(int) |
| 98 | + |
| 99 | +/// Region-level invariant expressions. |
| 100 | +and invariantExpr = { |
| 101 | + name: string, |
| 102 | + proposition: located<expr>, |
| 103 | +} |
| 104 | + |
| 105 | +// ============================================================================ |
| 106 | +// Import / Export (Section 3 of grammar) |
| 107 | +// ============================================================================ |
| 108 | + |
| 109 | +/// Import a region from another module. |
| 110 | +and importRegionDecl = { |
| 111 | + regionName: string, |
| 112 | + moduleName: string, |
| 113 | + expectedFields: array<located<fieldDecl>>, |
| 114 | +} |
| 115 | + |
| 116 | +/// Export a region from this module. |
| 117 | +and exportRegionDecl = { |
| 118 | + regionName: string, |
| 119 | +} |
| 120 | + |
| 121 | +// ============================================================================ |
| 122 | +// Functions (Section 4 of grammar) |
| 123 | +// ============================================================================ |
| 124 | + |
| 125 | +/// Function declaration. |
| 126 | +and functionDecl = { |
| 127 | + name: string, |
| 128 | + params: array<located<param>>, |
| 129 | + returnType: option<located<fieldType>>, |
| 130 | + effects: option<array<located<effect>>>, |
| 131 | + lifetimeConstraints: array<located<lifetimeConstraint>>, |
| 132 | + body: array<located<statement>>, |
| 133 | +} |
| 134 | + |
| 135 | +/// Function parameter. |
| 136 | +and param = { |
| 137 | + name: string, |
| 138 | + paramType: located<paramType>, |
| 139 | +} |
| 140 | + |
| 141 | +/// Parameter types: either a field type or a region handle type. |
| 142 | +and paramType = |
| 143 | + | FieldParam(fieldType) |
| 144 | + | RegionHandleParam(handleMode, string) // ®ion<Name>, &mut region<Name>, own region<Name> |
| 145 | + |
| 146 | +/// Handle modes for region parameters. |
| 147 | +and handleMode = |
| 148 | + | SharedBorrow // & |
| 149 | + | MutableBorrow // &mut |
| 150 | + | Owning // own |
| 151 | + |
| 152 | +/// Memory effects. |
| 153 | +and effect = |
| 154 | + | ReadEffect |
| 155 | + | WriteEffect |
| 156 | + | AllocEffect |
| 157 | + | FreeEffect |
| 158 | + | ReadRegionEffect(string) |
| 159 | + | WriteRegionEffect(string) |
| 160 | + |
| 161 | +/// Lifetime constraints. |
| 162 | +and lifetimeConstraint = { |
| 163 | + name: string, // lifetime name without the ' |
| 164 | + bound: lifetimeBound, |
| 165 | +} |
| 166 | + |
| 167 | +/// Lifetime bounds. |
| 168 | +and lifetimeBound = |
| 169 | + | StaticLifetime |
| 170 | + | FnLifetime |
| 171 | + | NamedLifetime(string) |
| 172 | + | OutlivesLifetime(string, string) // 'a >= 'b |
| 173 | + |
| 174 | +// ============================================================================ |
| 175 | +// Statements (Section 5 of grammar) |
| 176 | +// ============================================================================ |
| 177 | + |
| 178 | +/// Statements within function bodies. |
| 179 | +and statement = |
| 180 | + | RegionGetStmt(regionGetStmt) |
| 181 | + | RegionSetStmt(regionSetStmt) |
| 182 | + | RegionScanStmt(regionScanStmt) |
| 183 | + | RegionAllocStmt(regionAllocStmt) |
| 184 | + | RegionFreeStmt(string) |
| 185 | + | LetStmt(letStmt) |
| 186 | + | IfStmt(ifStmt) |
| 187 | + | WhileStmt(whileStmt) |
| 188 | + | ReturnStmt(option<located<expr>>) |
| 189 | + | StaticAssertStmt(located<expr>) |
| 190 | + | ProofStmt(proofStmt) |
| 191 | + | ExprStmt(located<expr>) |
| 192 | + |
| 193 | +/// region.get $target .field.path -> binding |
| 194 | +and regionGetStmt = { |
| 195 | + target: regionTarget, |
| 196 | + fieldPath: array<fieldPathSegment>, |
| 197 | + binding: option<string>, |
| 198 | +} |
| 199 | + |
| 200 | +/// region.set $target .field.path, value |
| 201 | +and regionSetStmt = { |
| 202 | + target: regionTarget, |
| 203 | + fieldPath: array<fieldPathSegment>, |
| 204 | + value: located<expr>, |
| 205 | +} |
| 206 | + |
| 207 | +/// region.scan $target where pred -> |binding| { body } |
| 208 | +and regionScanStmt = { |
| 209 | + target: regionTarget, |
| 210 | + predicate: option<located<expr>>, |
| 211 | + bindingName: option<string>, |
| 212 | + body: array<located<statement>>, |
| 213 | +} |
| 214 | + |
| 215 | +/// region.alloc RegionName { field = val, ... } -> binding |
| 216 | +and regionAllocStmt = { |
| 217 | + regionName: string, |
| 218 | + initializers: array<(string, located<expr>)>, |
| 219 | + binding: string, |
| 220 | +} |
| 221 | + |
| 222 | +/// Region target: $name or $name[index] |
| 223 | +and regionTarget = { |
| 224 | + name: string, |
| 225 | + index: option<located<expr>>, |
| 226 | +} |
| 227 | + |
| 228 | +/// Field path segments: .field or [index] |
| 229 | +and fieldPathSegment = |
| 230 | + | FieldAccess(string) |
| 231 | + | IndexAccess(located<expr>) |
| 232 | + |
| 233 | +/// let [mut] name [: type] = expr; |
| 234 | +and letStmt = { |
| 235 | + isMutable: bool, |
| 236 | + name: string, |
| 237 | + typeAnnotation: option<located<fieldType>>, |
| 238 | + initializer: located<expr>, |
| 239 | +} |
| 240 | + |
| 241 | +/// if expr { stmts } [else { stmts }] |
| 242 | +and ifStmt = { |
| 243 | + condition: located<expr>, |
| 244 | + thenBranch: array<located<statement>>, |
| 245 | + elseBranch: option<array<located<statement>>>, |
| 246 | +} |
| 247 | + |
| 248 | +/// while expr { stmts } |
| 249 | +and whileStmt = { |
| 250 | + condition: located<expr>, |
| 251 | + body: array<located<statement>>, |
| 252 | +} |
| 253 | + |
| 254 | +/// proof name { steps } |
| 255 | +and proofStmt = { |
| 256 | + name: string, |
| 257 | + steps: array<located<proofStep>>, |
| 258 | +} |
| 259 | + |
| 260 | +/// Individual proof step. |
| 261 | +and proofStep = |
| 262 | + | GivenStep(located<expr>) |
| 263 | + | ShowStep(located<expr>) |
| 264 | + | ByStep(proofTactic) |
| 265 | + |
| 266 | +/// Proof tactics. |
| 267 | +and proofTactic = |
| 268 | + | BoundsCheck |
| 269 | + | Linearity |
| 270 | + | Lifetime |
| 271 | + | AliasFreedom |
| 272 | + | EffectPurity |
| 273 | + | Induction(string) |
| 274 | + | Rewrite(string) |
| 275 | + |
| 276 | +// ============================================================================ |
| 277 | +// Expressions (Section 6 of grammar) |
| 278 | +// ============================================================================ |
| 279 | + |
| 280 | +/// Expressions. |
| 281 | +and expr = |
| 282 | + | IntLit(int) |
| 283 | + | FloatLit(float) |
| 284 | + | StringLit(string) |
| 285 | + | BoolLit(bool) |
| 286 | + | NullLit |
| 287 | + | Identifier(string) |
| 288 | + | RegionVar(string) // $name |
| 289 | + | BinOp(located<expr>, binOp, located<expr>) |
| 290 | + | UnaryOp(unaryOp, located<expr>) |
| 291 | + | SizeofExpr(string) // sizeof(RegionName) |
| 292 | + | OffsetofExpr(string, string) // offsetof(Region.field) |
| 293 | + | TypeofExpr(located<expr>) |
| 294 | + | IsValidExpr(string) // is_valid($name) |
| 295 | + | IsNullExpr(located<expr>) |
| 296 | + | CastExpr(located<fieldType>, located<expr>) // cast<Type>(expr) |
| 297 | + | ParenExpr(located<expr>) |
| 298 | + | CallExpr(string, array<located<expr>>) |
| 299 | + |
| 300 | +/// Binary operators. |
| 301 | +and binOp = |
| 302 | + | Add |
| 303 | + | Sub |
| 304 | + | Mul |
| 305 | + | Div |
| 306 | + | Mod |
| 307 | + | Eq |
| 308 | + | NotEq |
| 309 | + | Lt |
| 310 | + | Gt |
| 311 | + | LtEq |
| 312 | + | GtEq |
| 313 | + | And |
| 314 | + | Or |
| 315 | + | BitAnd |
| 316 | + | BitOr |
| 317 | + | BitXor |
| 318 | + | Shl |
| 319 | + | Shr |
| 320 | + |
| 321 | +/// Unary operators. |
| 322 | +and unaryOp = |
| 323 | + | Neg |
| 324 | + | Not |
| 325 | + | BitNot |
| 326 | + |
| 327 | +// ============================================================================ |
| 328 | +// Memory Declaration (Section 7 of grammar) |
| 329 | +// ============================================================================ |
| 330 | + |
| 331 | +/// Memory declaration. |
| 332 | +and memoryDecl = { |
| 333 | + name: string, |
| 334 | + initialPages: int, |
| 335 | + maximumPages: option<int>, |
| 336 | + isShared: bool, |
| 337 | + placements: array<located<regionPlacement>>, |
| 338 | +} |
| 339 | + |
| 340 | +/// Region placement: `place RegionName at offset;` |
| 341 | +and regionPlacement = { |
| 342 | + regionName: string, |
| 343 | + offset: located<expr>, |
| 344 | +} |
| 345 | + |
| 346 | +// ============================================================================ |
| 347 | +// Global Invariant (Section 8 of grammar) |
| 348 | +// ============================================================================ |
| 349 | + |
| 350 | +/// Cross-region invariant declaration. |
| 351 | +and invariantDecl = { |
| 352 | + name: string, |
| 353 | + regions: array<string>, |
| 354 | + proposition: located<expr>, |
| 355 | + proofTactic: option<proofTactic>, |
| 356 | +} |
0 commit comments