Replace custom Call/Procedure formatters with DDM printer (#997)

Fixes #994

Removes the custom `ToFormat` instances for `CmdExt` (call statements)
and `Procedure` in Core, replacing them with DDM-based pretty-printer
functions so the DDM formatter is the sole formatter for these types.

To break the circular dependency that prevented removing the old
instances, `ASTtoCST.lean` is split into `FormatCore.lean`
(expression/statement/procedure formatting) and `ASTtoCST.lean`
(program-level conversion only). `Program.lean` imports
`FormatCore.lean`, making DDM formatting available to all downstream
code.

Additional fixes included along the way:
- **Grammar:** Removes trailing `\n` from statement format strings and
uses `NewlineSepBy Statement` for blocks, eliminating extra blank lines.
Closing `}` is placed on its own line. Adds `:0` precedence annotation
to `while_statement` body to prevent spurious `({...})` wrapping.
- **Call formatting:** Empty-LHS calls now emit `call_unit_statement`
(`call foo(1, 2);`) instead of `call_statement` which would produce
`call := foo(1, 2);`.
- **Lambda support:** Adds a `lambda` construct to the CoreDDM grammar
and implements conversion of Lambda `.abs` expressions into DDM `lambda
d :: body` syntax, reusing `prettyName` as the bound variable name.
- **Extra-arg formatting:** When a declared function is applied to more
arguments than it declares (e.g. a function returning a function type
via `funMacro`), the formatter now renders the declared args with the
function's syntax and wraps extra args in call syntax. Uses
`Array.take`/`Array.drop` directly instead of `Array→List→Array`
round-trips.
- **Deduplication:** Extracts `mkTypeArgsAnn` helper to eliminate
repeated type-args conversion patterns. `extractFromExpr` now recurses
into `.abs` bodies.

Tested: all existing tests pass, new lambda formatting tests added.

Author: MikaelMayer

Examples/expected/DoubleTwice.callElim.core.st

@@ -5,7 +5,7 @@ spec {
   ensures [double_correct]: result == n * 2;
   } {
   result := n + n;
-  };
+};
 procedure TestProc (x : int) returns (output : int)
 spec {
   ensures [testProc_result]: output == x * 4;
@@ -18,4 +18,4 @@ spec {
   var tmp_output_1 : int := output;
   havoc output;
   assume [callElimAssume_double_correct_2]: output == tmp_arg_0 * 2;
-  };
+};

Examples/expected/DoubleTwice.inlineProcedures.core.st

@@ -5,7 +5,7 @@ spec {
   ensures [double_correct]: result == n * 2;
   } {
   result := n + n;
-  };
+};
 procedure TestProc (x : int) returns (output : int)
 spec {
   ensures [testProc_result]: output == x * 4;
@@ -15,11 +15,11 @@ spec {
     var Double_result_4 : int;
     Double_result_4 := Double_n_3 + Double_n_3;
     output := Double_result_4;
-    }
+  }
   Double$inlined: {
     var Double_n_0 : int := output;
     var Double_result_1 : int;
     Double_result_1 := Double_n_0 + Double_n_0;
     output := Double_result_1;
-    }
-  };
+  }
+};

Examples/expected/DoubleTwice.inlineProcedures.filterProcedures.core.st

@@ -9,11 +9,11 @@ spec {
     var Double_result_4 : int;
     Double_result_4 := Double_n_3 + Double_n_3;
     output := Double_result_4;
-    }
+  }
   Double$inlined: {
     var Double_n_0 : int := output;
     var Double_result_1 : int;
     Double_result_1 := Double_n_0 + Double_n_0;
     output := Double_result_1;
-    }
-  };
+  }
+};

Examples/expected/IrrelevantAxioms.removeIrrelevantAxioms.core.st

@@ -11,4 +11,4 @@ spec {
   ensures [result_positive]: result > 0;
   } {
   result := f(x);
-  };
+};

Examples/expected/LoopSimple.loopElim.core.st

@@ -14,18 +14,18 @@ spec {
       assert [entry_invariant_0_1]: i * (i - 1) div 2 == sum;
       assume [assume_entry_invariant_0_0]: i <= n;
       assume [assume_entry_invariant_0_1]: i * (i - 1) div 2 == sum;
-      }
+    }
     if (i < n) {
       arbitrary_iter_facts_0: {
         loop_havoc_0: {
           havoc sum;
           havoc i;
-          }
+        }
         arbitrary_iter_assumes_0: {
           assume [assume_guard_0]: i < n;
           assume [assume_invariant_0_0]: i <= n;
           assume [assume_invariant_0_1]: i * (i - 1) div 2 == sum;
-          }
+        }
         var $__loop_measure_0 : int;
         assume [assume_measure_0]: $__loop_measure_0 == n - i;
         assert [measure_lb_0]: !($__loop_measure_0 < 0);
@@ -34,17 +34,17 @@ spec {
         assert [arbitrary_iter_maintain_invariant_0_0]: i <= n;
         assert [arbitrary_iter_maintain_invariant_0_1]: i * (i - 1) div 2 == sum;
         assert [measure_decrease_0]: n - i < $__loop_measure_0;
-        }
+      }
       loop_havoc_0: {
         havoc sum;
         havoc i;
-        }
+      }
       assume [not_guard_0]: !(i < n);
       assume [invariant_0_0]: i <= n;
       assume [invariant_0_1]: i * (i - 1) div 2 == sum;
-      }
     }
+  }
   assert [sum_assert]: n * (n - 1) div 2 == sum;
   assert [neg_cond]: i == n;
   r := sum;
-  };
+};

Examples/expected/SafeBvOps.callElim.core.st

@@ -15,4 +15,4 @@ procedure safe_bv_ops (x : bv32, y : bv32) returns (r : bv32)
   e := x safesdiv y;
   f := x safesmod y;
   r := a;
-  };
+};

Examples/expected/TwoLoops.loopElim.core.st

@@ -11,49 +11,49 @@ procedure TwoLoops () returns ()
     first_iter_asserts_0: {
       assert [entry_invariant_0_0]: 0 <= i && i <= N;
       assume [assume_entry_invariant_0_0]: 0 <= i && i <= N;
-      }
+    }
     if (i < N) {
       arbitrary_iter_facts_0: {
         loop_havoc_0: {
           havoc i;
-          }
+        }
         arbitrary_iter_assumes_0: {
           assume [assume_guard_0]: i < N;
           assume [assume_invariant_0_0]: 0 <= i && i <= N;
-          }
+        }
         i := i + 1;
         assert [arbitrary_iter_maintain_invariant_0_0]: 0 <= i && i <= N;
-        }
+      }
       loop_havoc_0: {
         havoc i;
-        }
+      }
       assume [not_guard_0]: !(i < N);
       assume [invariant_0_0]: 0 <= i && i <= N;
-      }
     }
+  }
   j := 0;
   loop_1: {
     first_iter_asserts_1: {
       assert [entry_invariant_1_0]: 0 <= j && j <= N;
       assume [assume_entry_invariant_1_0]: 0 <= j && j <= N;
-      }
+    }
     if (j < N) {
       arbitrary_iter_facts_1: {
         loop_havoc_1: {
           havoc j;
-          }
+        }
         arbitrary_iter_assumes_1: {
           assume [assume_guard_1]: j < N;
           assume [assume_invariant_1_0]: 0 <= j && j <= N;
-          }
+        }
         j := j + 1;
         assert [arbitrary_iter_maintain_invariant_1_0]: 0 <= j && j <= N;
-        }
+      }
       loop_havoc_1: {
         havoc j;
-        }
+      }
       assume [not_guard_1]: !(j < N);
       assume [invariant_1_0]: 0 <= j && j <= N;
-      }
     }
-  };
+  }
+};

Strata/DDM/Format.lean

@@ -374,7 +374,28 @@ private partial def ExprF.mformatM (e : ExprF α) (rargs : Array (ArgF α)  := #
         let args := rargs.reverse
         let bindings := op.argDecls
         let .isTrue bsize := decEq args.size bindings.size
-              | return panic! "Mismatch betweeen binding and arg size"
+              | do
+                -- When a function is applied to more arguments than it declares
+                -- (e.g. a function returning a function type via funMacro),
+                -- format it with its declared args, then apply the remaining
+                -- args with call syntax.
+                let declArgCount := bindings.size
+                if rargs.size > declArgCount then
+                  let fnArgs := args.take declArgCount
+                  let extraArgs := args.drop declArgCount
+                  let .isTrue bsize' := decEq fnArgs.size bindings.size
+                        | return panic! "Mismatch betweeen binding and arg size" -- nopanic:ok
+                  let argResults ← do
+                        match formatArguments (← read) (← get) bindings ⟨fnArgs, bsize'⟩ with
+                        | .ok r => pure r
+                        | .error e => return panic! e -- nopanic:ok
+                  let fnFmt := ppOp (← read).opts op.syntaxDef (Prod.fst <$> argResults)
+                  let extraFmts := (← extraArgs.mapM (·.mformatM)) |>.map (·.format)
+                  let extraFmts := Format.joinSep extraFmts.toList f!", "
+                  return .mk f!"({fnFmt.format})({extraFmts})" callPrec
+                else
+                  -- Fewer args than expected: format as name(args)
+                  ppArgs f.fullName
         let argResults ← do
               match formatArguments (← read) (← get) bindings ⟨args, bsize⟩ with
               | .ok r => pure r

Strata/Languages/Core/Core.lean

@@ -111,17 +111,6 @@ def typeCheckAndEval (options : VerifyOptions) (program : Program)
       dbg_trace f!"{formatProofObligations E.deferred}"
   return (pEs, stats)
 
-instance instCoreProgramString : ToString (Program) where
-  toString p := toString (Core.formatProgram p)
-
-instance instCoreProgramFormat : Std.ToFormat Program where
-  format := Core.formatProgram
-
-/-- Format a single `Core.Expression.Expr` using the DDM pretty-printer.
-    This instance shadows the generic `ToFormat (LExpr T)` from `LExpr.lean`. -/
-instance instCoreExprFormat : Std.ToFormat Expression.Expr where
-  format e := Core.formatExprs [e]
-
 end -- public section
 
 end Core