// with.baba — Dev playground and implementation plan for header `with` locals
//
// This file documents the proposed `with` and `with rec` header clauses for
// local bindings inside function bodies. It contains:
// - Syntax and semantics
// - Typing rules (locals treated like globals)
// - Semicolon policy
// - Examples (untyped, typed, shadowing, with `when`, mutual recursion)
// - Error cases
// - Implementation plan (lexer, parser, interpreter, tests)
//
// NOTE: All examples are commented out so this file remains parseable until the
// feature is implemented.

// -----------------------------------------------------------------------------
// Syntax
//
// Function declaration (untyped params):
//   name : params -> with ( headerEntries ) -> body;
//
// Function declaration (typed params + return type):
//   name : (x: T, y: U) -> R -> with ( headerEntries ) -> body;
//
// Header entries inside `with ( ... )` are separated by semicolons `;` and may
// end with an optional trailing semicolon.
// Each entry is either:
//   - Type declaration (same style as global):
//       ident Type;
//   - Assignment (value):
//       ident : expression;
//
// Mutually recursive locals use `with rec` (or `with recursion`) to pre-bind:
//   name : args -> ...
//     with rec (
//       f : a -> ... g ...;
//       g : b -> ... f ...;
//     ) ->
//       body;
//
// Soft keywords:
// - `with` and `rec` are recognized only in the function-header position
//   (immediately after an arrow). Elsewhere they remain plain identifiers.

// -----------------------------------------------------------------------------
// Semantics
//
// with (non-rec):
// - Create an inner scope layered over the function call scope.
// - Process header entries left-to-right:
//   - Type decl: record `name -> Type` in the with-scope types map.
//   - Assignment: evaluate expression in the current with-scope, then
//     if a type was declared for `name`, validate using the existing runtime
//     type lattice (Int ⊂ Float ⊂ Number). Bind `name` to the result.
// - Evaluate `body` in that inner scope; discard the scope after.
// - No forward references among assignments.
// - Shadowing permitted (locals shadow params/globals).
//
// with rec (mutual recursion):
// - Pre-bind all names in the header to placeholders in the with-scope.
// - Evaluate each RHS in order and assign into the same with-scope.
// - Restrict RHS to functions (to avoid non-lazy cycles). If non-function is
//   assigned under `rec`, throw a clear error.
// - Body executes after all bindings are assigned.

// -----------------------------------------------------------------------------
// Semicolons
// - Inside `with ( ... )`: semicolons separate entries; trailing `;` allowed.
// - Between header and body: only the arrow `->`.
// - After `body`: same as today at top-level (semicolon optional/tolerated).

// -----------------------------------------------------------------------------
// Executable Examples

// 1) Basic locals (untyped)
addMul : x y ->
  with (inc : x + 1; prod : inc * y;) ->
    inc + prod;
addMulResult : addMul 2 5;

// 2) Quadratic roots (untyped)
quadraticRoots : a b c ->
  with (
    disc : b * b - 4 * a * c;
    sqrtDisc : math.sqrt disc;
    denom : 2 * a;
  ) ->
    { r1: (-b + sqrtDisc) / denom, r2: (-b - sqrtDisc) / denom };
roots : quadraticRoots 1 -3 2;

// 3) Typed params + typed locals (global-like declarations inside header)
sumNext : (x: Int, y: Int) -> Int ->
  with (
    nextX Int; nextY Int;
    nextX : x + 1;
    nextY : y + 1;
  ) ->
    nextX + nextY;
sumNextResult : sumNext 2 3;

// 4) Shadowing and ordering
shadow : x ->
  with (x : x + 1; y : x * 2) ->
    x + y;
shadowResult : shadow 3;

// 5) With + when
classify : n ->
  with (
    lo Int; hi Int;
    lo : 10; hi : 100;
  ) ->
    when n is
      0 then "zero"
      _ then when (n > hi) is
               true then "large"
               _    then when (n > lo) is
                          true then "medium"
                          _    then "small";
classify0 : classify 0;
classify50 : classify 50;
classify200 : classify 200;

// Multi-discriminant with local
bucket : x y ->
  with (t : x + y) ->
    when x t is
      0 0 then "origin"
      _ _ then "other";
bucketResult : bucket 0 0;

// 6) Result + with + when
safeDivide : x y ->
  with (zero : 0) ->
    when y is
      0 then Err "Division by zero"
      _ then Ok (x / y);

useDivide : a b ->
  with (fallback Int; fallback : 0) ->
    when (safeDivide a b) is
      Ok v  then v
      Err _ then fallback;
divOk : useDivide 10 2;
divErr : useDivide 10 0;

// 7) with rec — mutual recursion among locals
isEvenOdd : z ->
  with rec (
    isEven : n ->
      when n is
        0 then true
        _ then isOdd (n - 1);
    isOdd : n ->
      when n is
        0 then false
        _ then isEven (n - 1);
  ) ->
    { even: isEven 10, odd: isOdd 7 };
rEvenOdd : isEvenOdd 0;

// Sample I/O to visualize outputs when running this file directly
io.out addMulResult;
io.out roots;
io.out sumNextResult;
io.out shadowResult;
io.out classify0 classify50 classify200;
io.out bucketResult;
io.out divOk divErr;
io.out rEvenOdd;

// -----------------------------------------------------------------------------
// Error cases (intended)
// - Non-rec forward reference among assignments in `with`: error.
// - In `with rec`, assignment RHS must evaluate to a function: error otherwise.
// - Type mismatch for a typed local: reuse existing error messaging similar to
//   function parameter/return mismatches.

// -----------------------------------------------------------------------------
// Implementation plan
// 1) Lexer (none/minimal):
//    - Keep `with` / `rec` as IDENTIFIER tokens; treat as soft keywords in parser.
//
// 2) Parser (parser.js):
//    - After params and optional return type, detect: IDENT('with') [IDENT('rec'|'recursion')] LPAREN ... RPAREN ARROW
//    - Parse header entries list:
//        entry := IDENT TYPE ';'  |  IDENT ':' expression ';'
//        allow repeated entries and optional trailing ';'
//    - AST: augment FunctionDeclaration/CurriedFunctionDeclaration body with optional
//      WithHeader { recursive: boolean, entries: Array< TypeDecl | Assign > }
//      where TypeDecl { name, typeAnnotation }, Assign { name, expr }
//    - Ensure support both in top-level function and nested curried bodies.
//
// 3) Interpreter (interpreter.js):
//    - When invoking a function with WithHeader:
//        - Create with-scope Map layered over call-scope; maintain withTypes Map.
//        - If recursive:
//            - Pre-bind all names to undefined in with-scope.
//            - Evaluate each Assign RHS with with-scope in effect; verify RHS is Function; set binding.
//          Else:
//            - Process entries left-to-right: on TypeDecl store in withTypes; on Assign evaluate and bind.
//        - On each Assign, if a type exists in withTypes, validate via existing lattice.
//        - Evaluate body in with-scope; finally restore original scope.
//
// 4) Tests (tests/*.test.js):
//    - parser-with-header.test.js (new): parsing of with/with rec, typed locals, trailing semicolon, shadowing, disallow forward refs.
//    - interpreter-with-header.test.js (new):
//        * Basic untyped locals
//        * Typed locals pass and fail
//        * With + when interactions
//        * Shadowing behavior
//        * with rec mutual recursion (success), non-function RHS (error)
//    - Back-compat pass: ensure existing tests still green.
//
// 5) Docs:
//    - Update README and ref.txt with the new form, semicolon policy, and examples.