diff --git a/docs/specs/bytecode/ISA_CORE.md b/docs/specs/bytecode/ISA_CORE.md index c00c1141..08469e48 100644 --- a/docs/specs/bytecode/ISA_CORE.md +++ b/docs/specs/bytecode/ISA_CORE.md @@ -29,7 +29,7 @@ This document defines the minimal, stable Core ISA surface for the Prometeu Virt - Stack manipulation: - `PUSH_CONST u32` — load constant by index → _pushes `[value]`. - - `PUSH_I64 i64`, `PUSH_F64 f64`, `PUSH_BOOL u8`, `PUSH_I32 i32`, `PUSH_BOUNDED u32(<=0xFFFF)` — push literals. + - `PUSH_I64 i64`, `PUSH_F64 f64`, `PUSH_BOOL u8`, `PUSH_I32 i32` — push literals. - `POP` — pops 1. - `POP_N u32` — pops N. - `DUP` — `[x] -> [x, x]`. @@ -38,8 +38,6 @@ This document defines the minimal, stable Core ISA surface for the Prometeu Virt - Arithmetic: - `ADD`, `SUB`, `MUL`, `DIV`, `MOD` — binary numeric ops. - `NEG` — unary numeric negation. - - `BOUND_TO_INT` — `[bounded] -> [int64]`. - - `INT_TO_BOUND_CHECKED` — `[int] -> [bounded]` (traps on overflow 0..65535). - Comparison and logic: - `EQ`, `NEQ`, `LT`, `LTE`, `GT`, `GTE` — comparisons → `[bool]`. diff --git a/docs/specs/pbs/3. Core Syntax Specification.md b/docs/specs/pbs/3. Core Syntax Specification.md index 30e5dc0d..0dec603a 100644 --- a/docs/specs/pbs/3. Core Syntax Specification.md +++ b/docs/specs/pbs/3. Core Syntax Specification.md @@ -101,7 +101,6 @@ Numeric literals: - `IntLit`: decimal integer (`0`, `42`, `1000`) - `FloatLit`: decimal float with dot (`3.14`, `0.5`) -- `BoundedLit`: decimal integer with `b` suffix (`0b`, `255b`) String literals: @@ -256,6 +255,7 @@ Rules: - Struct methods have an implicit `this` receiver and do not declare `this: Self` explicitly. - `ctor` declares a named factory for the enclosing struct type. - A named `ctor` constructs its enclosing struct by initializing the fields of an implicit under-construction `this`. +- Multiple `ctor` declarations with the same name are allowed only when their parameter signatures differ. - Struct values are constructed only through `new Type(...)`. - `declare contract` bodies contain only function signatures. - A contract declaration introduces a nominal runtime-dispatchable method surface. @@ -351,15 +351,16 @@ Rules: - Top-level constants MUST use `declare const`. - `declare const` is a declaration and may be exported through `mod.barrel`. +- A `declare const` initializer MUST be a constant expression as defined by static semantics. +- `declare const` values are compile-time constants, not runtime-initialized module storage. ## 8. Type syntax ```ebnf TypeRef ::= OptionalType | TypePrimary -TypePrimary ::= SelfType | SimpleType | GenericType | NamedTupleType | GroupType | UnitType +TypePrimary ::= SelfType | SimpleType | NamedTupleType | GroupType | UnitType SelfType ::= 'Self' SimpleType ::= Identifier -GenericType ::= Identifier '<' TypeRef (',' TypeRef)* '>' NamedTupleType ::= '(' NamedTupleField (',' NamedTupleField){0,5} ')' NamedTupleField ::= Identifier ':' TypeRef GroupType ::= '(' TypeRef ')' @@ -372,6 +373,7 @@ Rules: - Named tuple arity is 1..6 in v1 core syntax. - Tuple types in PBS core are always named. - Single-slot tuple types are allowed only in type/signature surface, not as tuple literals. +- General user-defined generics are not part of PBS core v1. - `optional T` is the canonical optional-type syntax in all type positions. - `optional void` and `optional ()` are invalid. - `Self` is valid only inside struct method and `ctor` declarations and refers to the enclosing struct type. @@ -412,7 +414,7 @@ BreakStmt ::= 'break' ';' ContinueStmt ::= 'continue' ';' LValue ::= Identifier LValueSuffix* -LValueSuffix ::= '.' Identifier | '[' Expr ']' +LValueSuffix ::= '.' Identifier ``` Rules: @@ -428,6 +430,7 @@ Rules: - `for name: T from start until end step s { ... }` uses explicit step `s`. - `while` is the general-purpose loop form in v1 core. - `break` and `continue` are valid only inside loop contexts (`for`, `while`). +- General indexing syntax (`expr[index]`) is not part of PBS core v1. - `LValue` MUST NOT include function call segments. - Compound assignment is syntax sugar over read/compute/write. @@ -465,15 +468,14 @@ MulExpr ::= UnaryExpr (('*' | '/' | '%') UnaryExpr)* UnaryExpr ::= UnaryOp UnaryExpr | PostfixExpr UnaryOp ::= '!' | '-' | 'not' PostfixExpr ::= PrimaryExpr PostfixSuffix* -PostfixSuffix ::= CallSugarSuffix | MemberSuffix | IndexSuffix | PropagateSuffix +PostfixSuffix ::= CallSugarSuffix | MemberSuffix | PropagateSuffix CallSugarSuffix ::= '(' ArgList? ')' MemberSuffix ::= '.' Identifier -IndexSuffix ::= '[' Expr ']' PropagateSuffix ::= '!' ArgList ::= Expr (',' Expr)* -Literal ::= IntLit | FloatLit | BoundedLit | StringLit | BoolLit +Literal ::= IntLit | FloatLit | StringLit | BoolLit BoolLit ::= 'true' | 'false' PrimaryExpr ::= Literal | Identifier | ThisExpr | NewExpr | BindExpr | SomeExpr | NoneExpr | UnitExpr | TupleExpr | GroupExpr | Block ThisExpr ::= 'this' @@ -509,6 +511,7 @@ Rules: - `new Type.ctorName(args...)` is the canonical named-constructor surface. - Struct construction arguments are positional and follow the declared struct field order. - `as` is reserved in expressions for explicit contract-view conversion only; it does not denote a general cast surface in v1 core. +- The right operand of expression-form `as` is a simple contract identifier already visible in scope, never a qualified module path. - `this` is an implicit receiver name available only inside struct method and `ctor` bodies. - `apply` is right-associative: `f1 apply f2 apply x` parses as `f1 apply (f2 apply x)`. - `f1 apply f2 apply f3 apply params` parses as `f1 apply (f2 apply (f3 apply params))`. @@ -588,6 +591,7 @@ At minimum, deterministic diagnostics are required for: - invalid assignment targets (`LValue` violations), - top-level executable statements, - `const` used outside `declare const` or `let const`, +- non-constant `declare const` initializer, - duplicate declaration names in the same namespace/scope (as defined by semantic phase), - use of reserved syntax words as active constructs. @@ -616,6 +620,7 @@ Design goals: ### 13.2 Type Definition `optional` is a built-in prefix type constructor. +It is a special core-language form, not evidence of general generic-type support in v1. Rules: @@ -717,6 +722,7 @@ Design goals: `result` is not part of general `TypeRef`. It may appear only in a function return annotation. +It is a special core-language return form, not evidence of general generic-type support in v1. Rules: @@ -724,7 +730,7 @@ Rules: - The payload may be omitted; omitted payload is equivalent to `void`. - If present, the payload must be a valid return payload shape written after `result`. - A single-slot payload is internally modeled as a one-field tuple payload. -- `result` cannot be used for local variable annotations, parameter annotations, field types, or generic type arguments. +- `result` cannot be used for local variable annotations, parameter annotations, or field types. - In function return surface, `result` is the only effect wrapper in use for that declaration. ### 14.3 Construction Surface @@ -797,6 +803,19 @@ Rules: ## 15. Canonical examples +This section is the canonical reference example set for PBS v1 syntax. + +It consolidates the primary surface forms used by tooling and conformance for: + +- `apply` and call sugar, +- `bind` and nominal callbacks, +- overloads that differ by return shape, +- `optional`, +- `result`, +- `switch`. + +Examples in this section are intended to stay mutually consistent with the syntax and static-semantics documents. + ### 15.1 Host function declaration ```pbs diff --git a/docs/specs/pbs/4. Static Semantics Specification.md b/docs/specs/pbs/4. Static Semantics Specification.md index 636884c3..65ba0278 100644 --- a/docs/specs/pbs/4. Static Semantics Specification.md +++ b/docs/specs/pbs/4. Static Semantics Specification.md @@ -135,8 +135,45 @@ Rules: - Any return surface that combines `optional` and `result` is statically invalid. - Any payload-less `optional` type surface is statically invalid. - Any `optional void` type surface is statically invalid. +- A `declare const` declaration must include an explicit type annotation. +- A `declare const` initializer must be a constant expression. +- `declare const` dependency resolution is module-wide and must not depend on source-file processing order. +- `declare const` dependencies must form an acyclic graph. -### 3.4 Enum declarations and values +### 3.4 Constant expressions + +PBS core v1 restricts top-level constant evaluation to a deterministic compile-time subset. + +Rules: + +- A `declare const` initializer is evaluated at compile time. +- A `declare const` may depend only on previously resolved visible `declare const` declarations and enum case values. +- Cross-file constant resolution within a module is defined by dependency analysis, not source-file order. +- Constant evaluation fails if the dependency graph contains a cycle. +- The allowed constant-expression forms in v1 core are: + - scalar literals: `IntLit`, `FloatLit`, `StringLit`, `BoolLit`, + - enum case paths `EnumName.caseName`, + - a reference to another visible `declare const`, + - unary `-` applied to an integer or float constant expression, + - unary `not` or `!` applied to a boolean constant expression, + - binary arithmetic operators over numeric constant expressions, + - binary comparison operators over compatible constant expressions, + - binary boolean operators over boolean constant expressions. +- A `declare const` initializer must not use: + - callable application or call sugar, + - `host fn`, + - `new`, + - `bind(...)`, + - `some(...)` or `none`, + - tuple expressions, + - block expressions, + - `if`, `switch`, `handle`, `else` extraction, or `!` result propagation, + - method calls or member access except enum case paths. +- The initializer type must be compatible with the declared `const` type. +- A `pub const` may be imported from another module only through ordinary module import rules. +- A `declare const` does not introduce mutable runtime storage; implementations may inline, fold, or materialize it as an immutable constant as long as observable semantics remain unchanged. + +### 3.5 Enum declarations and values Rules: @@ -148,7 +185,7 @@ Rules: - The static type of `Name.case` is the enum type `Name`. - Error labels are not enum cases and must not be used where enum case values are required. -### 3.5 Structs, methods, and contracts +### 3.6 Structs, methods, and contracts Rules: @@ -166,6 +203,7 @@ Rules: - A `ctor` has no declared return annotation and is not a `fn`. - A `ctor` completes by falling off the end of its body after initializing the enclosing struct instance. - Every field of the enclosing struct must be definitely assigned on every completing `ctor` path. +- Named constructors participate in overload resolution by name plus parameter signature. - `return;` and `return expr;` are both invalid inside `ctor` bodies. - Methods declared in a struct body belong to the direct method namespace of that concrete struct type. - `receiver.method(...)` on a concrete struct receiver resolves only against methods declared directly in that struct body. @@ -178,6 +216,7 @@ Rules: - A struct value may be coerced to a contract value when exactly one visible `implements Contract for Struct ...` applies. - Contract coercion may happen by explicit `expr as ContractType` or by contextual typing in assignments, parameter passing, and returns. - `as` in expression position is reserved for explicit contract coercion only; no other cast semantics exist in v1 core. +- The contract name in `expr as ContractName` must be a simple visible identifier resolved through ordinary scope and import rules. - A contract value carries the underlying struct reference together with the selected contract implementation for runtime dispatch. - Calling `contractValue.method(...)` uses dynamic dispatch through the contract value. - Calling `structValue.contractMethod(...)` is not valid unless that method is also declared directly on the struct. @@ -219,7 +258,7 @@ fn demo() -> int { } ``` -### 3.6 Nominal callbacks +### 3.7 Nominal callbacks Rules: @@ -246,7 +285,10 @@ declare callback TickCb(dt: int) -> void; fn on_tick(dt: int) -> void { } -let cb: TickCb = on_tick; +fn install_tick() -> void { + let cb: TickCb = on_tick; + let _ = cb; +} ``` Bound example: @@ -259,7 +301,10 @@ declare struct Enemy(hp: int); fn update_enemy(self: Enemy, dt: int) -> void { } -let cb: UpdateCb = bind(enemy, update_enemy); +fn install_update(enemy: Enemy) -> void { + let cb: UpdateCb = bind(enemy, update_enemy); + let _ = cb; +} ``` Ambiguous overload example: @@ -273,10 +318,12 @@ fn tick(dt: int) -> void { fn tick(time: int) -> void { } -let cb: TickCb = tick; // error: ambiguous overloaded fn assignment +fn install_tick() -> void { + let cb: TickCb = tick; // error: ambiguous overloaded fn assignment +} ``` -### 3.7 Canonical application +### 3.8 Canonical application The canonical surface form for function application is: @@ -301,7 +348,7 @@ Rules: - Chained `apply` is nested ordinary application, not callable composition as a first-class value. - Callback values, `host fn`, service methods, struct methods, and contract-method targets use the same `apply` rules as top-level `fn`. -### 3.8 Call sugar +### 3.9 Call sugar The surface form: @@ -321,7 +368,7 @@ Rules: - When `(arg1, ..., argN)` is used as positional tuple sugar, the callee input tuple shape supplies the effective labels. - All overload resolution, diagnostics, and type checking are defined on the canonical `apply` form. -### 3.9 Result type of application +### 3.10 Result type of application Rules: @@ -339,10 +386,14 @@ fn func(a: int, b: int) -> (c: int, d: float) { return (c: a + b, d: 2.0); } -let params: (a: int, b: int) = (1, 2); -let r = func apply params; -let c = r.c; -let d = r.d; +fn demo_apply() -> int { + let params: (a: int, b: int) = (1, 2); + let r = func apply params; + let c = r.c; + let d = r.d; + let _ = d; + return c; +} ``` In the example above: @@ -360,8 +411,11 @@ fn plus_one(x: int) -> int { return x + 1; } -let r = plus_one apply 1; -if r == 2 { } +fn demo_single() -> void { + let r = plus_one apply 1; + if r == 2 { + } +} ``` In the example above: @@ -372,7 +426,7 @@ In the example above: - the value produced by `plus_one apply 1` has carrier type `int`, - `r.value` is not required and should not be used. -### 3.10 Overload resolution +### 3.11 Overload resolution Rules: @@ -386,7 +440,7 @@ Rules: - Overloads that differ only by labels are duplicates and are forbidden. - Overloads that differ only by output positional types are permitted, but uncontextualized `apply` sites may become ambiguous. -### 3.11 Member access and projection +### 3.12 Member access and projection Rules: @@ -413,7 +467,7 @@ Rules: - Access to a missing contract method is a compile-time error. - Member projection is not defined for single-slot collapsed carrier values. -### 3.12 Block expressions and function fallthrough +### 3.13 Block expressions and function fallthrough Rules: @@ -426,7 +480,7 @@ Rules: - Reaching the end of an `optional P` function yields `none`. - Reaching the end of a `result` function is a compile-time error. -### 3.13 Loop forms +### 3.14 Loop forms Rules: @@ -442,7 +496,7 @@ Rules: - `continue` inside `for` transfers control to the step update and then to the next bound check. - `break` exits the nearest enclosing loop. -### 3.14 `if` and `switch` conditional expressions +### 3.15 `if` and `switch` conditional expressions Rules: @@ -464,7 +518,7 @@ Rules: - A `switch` used as an `ExprStmt` is valid when the selected arm blocks evaluate to unit. - A `switch` expression used in a value-required position must be exhaustive, either by a wildcard arm or by another statically proven exhaustive case set. -### 3.15 `optional` construction and extraction +### 3.16 `optional` construction and extraction Rules: @@ -476,7 +530,7 @@ Rules: - The static result type of `opt else fallback` is the carrier value type for single-slot payloads and the named tuple payload shape for multi-slot payloads. - `opt else fallback` does not introduce implicit mutation or unwrapping side effects beyond normal expression evaluation. -### 3.16 `result` return flow and handling +### 3.17 `result` return flow and handling Rules: @@ -496,7 +550,7 @@ Rules: - The static result type of `handle expr { ... }` is the extracted success payload shape `P`, collapsed to its carrier value when single-slot. - On error, `handle` performs an immediate enclosing-function return with the mapped `err(...)`. -### 3.17 Required static diagnostics +### 3.18 Required static diagnostics At minimum, deterministic static diagnostics are required for: @@ -521,6 +575,8 @@ At minimum, deterministic static diagnostics are required for: - invalid enum case path, - invalid enum intrinsic member call, - invalid named constructor target, +- unresolved named constructor overload, +- ambiguous named constructor overload, - incompatible top-level `fn` assignment to callback type, - ambiguous overloaded top-level `fn` assignment to callback type, - attempted assignment of service method to callback type, @@ -550,6 +606,11 @@ At minimum, deterministic static diagnostics are required for: - invalid mixed `optional`/`result` return surface, - invalid payload-less `optional` type surface, - invalid `optional void` type surface, +- missing explicit type annotation on `declare const`, +- non-constant `declare const` initializer, +- incompatible `declare const` initializer type, +- cyclic dependency among `declare const` declarations, +- unresolved referenced `declare const` in constant evaluation, - invalid `none` usage without expected optional type, - invalid `else` extraction over non-optional operand, - fallback type mismatch in `else` extraction, diff --git a/docs/specs/pbs/TODO.md b/docs/specs/pbs/TODO.md new file mode 100644 index 00000000..64903b80 --- /dev/null +++ b/docs/specs/pbs/TODO.md @@ -0,0 +1,47 @@ +# PBS Spec Approval TODO + +Status: Draft +Purpose: checklist curto para decidir se a spec da PBS pode ser aprovada para seguir agora + +## Blockers + +- [ ] Fechar o gate de prontidao para implementacao definido no charter. + Hoje o charter exige specs adicionais antes de iniciar implementacao: dynamic semantics, memory and lifetime, host ABI binding, module/package, diagnostics, IR/lowering e conformance. + Referencia: `1. Language Charter.md`, secao "Required Spec Set Before Implementation". + +- [ ] Definir a identidade normativa de `host fn`. + A governanca exige versionamento por `(module, name, version)`, mas a sintaxe e a semantica atual tratam `host fn` apenas por nome e assinatura. + Isso precisa de contrato claro de binding, capability gating e linking. + Referencias: `2. Governance and Versioning.md`, `3. Core Syntax Specification.md`, `4. Static Semantics Specification.md`. + +- [ ] Fechar o modelo semantico de `service` ou remover `service` do core v1. + A gramatica aceita `service Identifier (':' Identifier)?`, mas a spec nao define o significado do `: Identifier`, o ciclo de vida do servico, como ele e resolvido nem como participa do runtime. + Referencias: `3. Core Syntax Specification.md`, secao de `ServiceDecl`; `4. Static Semantics Specification.md`, callable categories. + +- [X] Remover do core v1 ou especificar completamente as superficies que ja existem na gramatica mas ainda nao tem contrato suficiente. + Itens visiveis hoje: `BoundedLit`, `GenericType`, `IndexSuffix` (`[]`) e `declare const` top-level. + Se permanecerem no v1, precisam de semantica estatica/dinamica e diagnosticos claros. + Referencia: `3. Core Syntax Specification.md`. + +## Non-Blockers + +- [x] Corrigir exemplos invalidos ou inconsistentes na spec estatica. + Ha exemplos com `let` em escopo top-level para callbacks, mas top-level `let` e proibido pela sintaxe. + Isso nao bloqueia a direcao da linguagem, mas deve ser corrigido para evitar ambiguidade. + Referencias: `3. Core Syntax Specification.md`, `4. Static Semantics Specification.md`. + +- [x] Consolidar exemplos canonicos para overload por retorno, `optional`, `result`, `bind`, `apply` e `switch`. + A base conceitual esta boa; o ajuste aqui e editorial e de conformance, nao arquitetural. + +- [ ] Decidir se a implementacao pode comecar em modo faseado. + Recomendacao: permitir apenas parser/AST/binding inicial enquanto os blockers acima nao forem fechados. + Nao liberar ainda lowering, linker, host integration ou runtime behavior final. + +## Decision Rule + +Pode aprovar a PBS para seguir agora somente se a aprovacao significar: + +- seguir com parser/frontend parcial, ou +- seguir com fechamento das specs faltantes antes de runtime/lowering/linking. + +Nao aprovar como spec fechada para implementacao completa enquanto houver blockers abertos.