Improve block formatting and diagnostic reporting

.github/workflows/ci.yml

@@ -324,6 +324,7 @@ jobs:
 
   strata-benchmarks:
     name: Run internal benchmarks of Strata
+    if: github.repository == 'strata-org/Strata'
     runs-on: ubuntu-latest
     permissions:
       id-token: write

.gitignore

@@ -12,4 +12,5 @@ vcs/*.smt2
 *.py.ion
 *.py.ion.core.st
 
-Strata.code-workspace
+Strata.code-workspace
+Build/

Strata/DDM/Format.lean

@@ -453,7 +453,7 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat
     if z : entries.size = 0 then
       pure (.atom .nil)
     else do
-      let f i q s := return s ++ "; " ++ (← entries[i].mformatM).format
+      let f i q s := return s ++ ";\n" ++ (← entries[i].mformatM).format
       let a := (← entries[0].mformatM).format
       .atom <$> entries.size.foldlM f (start := 1) a
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -9,7 +9,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: multiAssign supports field access targets, added opaque keyword.
+-- Last grammar change: block format uses indent(2) with leading spaces for vertical layout.
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -106,8 +106,8 @@ op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option ElseBran
 op assert (cond : StmtExpr, errorMessage: Option ErrorSummary) : StmtExpr => @[prec(0)] "assert " cond:0 errorMessage:0;
 op assume (cond : StmtExpr) : StmtExpr => @[prec(0)] "assume " cond:0;
 op return (value : StmtExpr) : StmtExpr => @[prec(0)] "return " value:0;
-op block (stmts : SemicolonSepBy StmtExpr) : StmtExpr => @[prec(1000)] "{ " stmts " }";
-op labelledBlock (stmts : SemicolonSepBy StmtExpr, label : Ident) : StmtExpr => @[prec(1000)] "{ " stmts " }" label;
+op block (stmts : SemicolonSepBy StmtExpr) : StmtExpr => @[prec(1000)] "{\n  " indent(2, stmts) "\n}";
+op labelledBlock (stmts : SemicolonSepBy StmtExpr, label : Ident) : StmtExpr => @[prec(1000)] "{\n  " indent(2, stmts) "\n}" label;
 op exit (label : Ident) : StmtExpr => @[prec(0)] "exit " label;
 
 // While loops

Strata/Languages/Laurel/LaurelCompilationPipeline.lean

@@ -211,8 +211,15 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
     if let some coreProgram := coreProgramOption then
       emit "CoreProgram" "core.st" coreProgram
     let mut allDiagnostics := passDiags ++ translateState.diagnostics
+
+    if translateState.coreDiagnostics.length > 0 && allDiagnostics.isEmpty then
+      -- The program was suppressed but no diagnostics explain why — report the core diagnostics
+      -- that have a known source location (those without one are not actionable for the user).
+      let locatedDiags := translateState.coreDiagnostics.filter (·.fileRange != FileRange.unknown)
+      allDiagnostics := allDiagnostics ++ locatedDiags
+
     let coreProgramOption :=
-      if translateState.coreProgramHasSuperfluousErrors then none else coreProgramOption
+      if !translateState.coreDiagnostics.isEmpty then none else coreProgramOption
     return (coreProgramOption, allDiagnostics, program, stats)
 
 /--

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -62,8 +62,11 @@ structure TranslateState where
   model : SemanticModel
   /-- Overflow check configuration -/
   overflowChecks : Core.OverflowChecks := {}
-  /-- Do not process the produces Core program, since it has superfluous errors -/
-  coreProgramHasSuperfluousErrors: Bool := false
+  /-- Diagnostics that indicate the Core program should not be processed further.
+      When non-empty, the produced Core program is suppressed. Each entry records
+      why the program was deemed invalid so that if no other diagnostics explain
+      the suppression, these can be surfaced to the user. -/
+  coreDiagnostics : List DiagnosticModel := []
 
 /-- The translation monad: state over Except, allowing both accumulated diagnostics and hard failures -/
 @[expose] abbrev TranslateM := OptionT (StateM TranslateState)
@@ -72,8 +75,9 @@ structure TranslateState where
 def emitDiagnostic (d : DiagnosticModel) : TranslateM Unit :=
   modify fun s => { s with diagnostics := s.diagnostics ++ [d] }
 
-private def invalidCoreType : TranslateM LMonoTy := do
-  modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+private def invalidCoreType (source : Option FileRange := none) (reason : String := "Type could not be translated to Core (resolution error placeholder)") : TranslateM LMonoTy := do
+  modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++
+    [diagnosticFromSource source reason DiagnosticType.StrataBug] }
   return .tcons s!"LaurelResolutionErrorPlaceholder" []
 
 /-
@@ -97,14 +101,15 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do
     | some (.datatypeDefinition dt) => return .tcons dt.name.text []
     | some (.datatypeConstructor typeName _) => return .tcons typeName.text []
     | _ => do -- resolution should have already emitted a diagnostic
-      modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+      modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++
+        [diagnosticFromSource ty.source s!"UserDefined type could not be resolved to a composite or datatype" DiagnosticType.StrataBug] }
       return .tcons "Composite" []
   | .TCore s => return .tcons s []
   | .TReal => return LMonoTy.real
-  | .Unknown => invalidCoreType
+  | .Unknown => invalidCoreType ty.source "Unknown type encountered during Core translation"
   | _ => do
     emitDiagnostic (diagnosticFromSource ty.source "cannot translate type to Core: not supported yet" DiagnosticType.StrataBug)
-    invalidCoreType
+    invalidCoreType ty.source s!"cannot translate type to Core: not supported yet"
 
 termination_by ty.val
 decreasing_by all_goals (first | (cases elementType; term_by_mem) | (cases keyType; term_by_mem) | (cases valueType; term_by_mem))
@@ -129,7 +134,7 @@ private def freshId : TranslateM Nat := do
 /-- Throw a hard diagnostic error, aborting the current translation -/
 def throwExprDiagnostic (d : DiagnosticModel): TranslateM Core.Expression.Expr := do
   emitDiagnostic d
-  modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+  modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] }
   let id ← freshId
   return LExpr.fvar () (⟨s!"DUMMY_VAR_{id}", ()⟩) none
 
@@ -345,7 +350,7 @@ private def exprAsUnusedInit (expr : StmtExprMd) (md : Imperative.MetaData Core.
 
 def throwStmtDiagnostic (d : DiagnosticModel): TranslateM (List Core.Statement) := do
   emitDiagnostic d
-  modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+  modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] }
   return []
 
 /--
@@ -493,8 +498,9 @@ def translateStmt (stmt : StmtExprMd)
       | none =>
           return [.exit (some "$body") md]
       | some _ =>
-          emitDiagnostic $ md.toDiagnostic "Return statement with value should have been eliminated by EliminateValueReturns pass" DiagnosticType.StrataBug
-          modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+          let d := md.toDiagnostic "Return statement with value should have been eliminated by EliminateValueReturns pass" DiagnosticType.StrataBug
+          emitDiagnostic d
+          modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] }
           return [.exit (some "$body") md]
   | .While cond invariants decreasesExpr body =>
       let condExpr ← translateExpr cond

StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean

@@ -58,21 +58,30 @@ private def roundtrip (input : String) : IO String := do
 
 /--
 info: procedure foo()
-{ assert true; assert false };
+  opaque
+{
+  assert true;
+  assert false
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure foo() { assert true; assert false };")
+#eval do IO.println (← roundtrip r"procedure foo() opaque { assert true; assert false };")
 
 /--
 info: procedure add(x: int, y: int): int
-{ x + y };
+  opaque
+{
+  x + y
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure add(x: int, y: int): int { x + y };")
+#eval do IO.println (← roundtrip r"procedure add(x: int, y: int): int opaque { x + y };")
 
 /--
 info: function aFunction(x: int): int
-{ x };
+{
+  x
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"function aFunction(x: int): int { x };")
@@ -90,17 +99,22 @@ composite Point {
 
 /--
 info: procedure test(x: int): int
-{ if x > 0 then x else 0 - x };
+  opaque
+{
+  if x > 0 then x else 0 - x
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure test(x: int): int { if x > 0 then x else 0 - x };")
+#eval do IO.println (← roundtrip r"procedure test(x: int): int opaque { if x > 0 then x else 0 - x };")
 
 /--
 info: procedure divide(x: int, y: int): int
   requires y != 0
   opaque
   ensures result >= 0
-{ x / y };
+{
+  x / y
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
@@ -113,11 +127,15 @@ procedure divide(x: int, y: int): int
 
 /--
 info: procedure test()
-{ assert forall(x: int) => x == x; assert exists(y: int) => y > 0 };
+  opaque
+{
+  assert forall(x: int) => x == x;
+  assert exists(y: int) => y > 0
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
-procedure test() {
+procedure test() opaque {
     assert forall(x: int) => x == x;
     assert exists(y: int) => y > 0
 };
@@ -127,15 +145,20 @@ procedure test() {
 info: composite Point { var x: int var y: int }
 
 procedure test(): int
-{ var p: Point := new Point; p#x := 5; p#x };
+  opaque
+{
+  var p: Point := new Point;
+  p#x := 5;
+  p#x
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
 composite Point {
   var x: int
   var y: int
 }
-procedure test(): int {
+procedure test(): int opaque {
     var p: Point := new Point;
     p#x := 5;
     p#x
@@ -160,25 +183,34 @@ info: composite Animal { }
 composite Dog extends Animal { }
 
 procedure test(a: Animal): bool
-{ a is Dog };
+  opaque
+{
+  a is Dog
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
 composite Animal {}
 composite Dog extends Animal {}
-procedure test(a: Animal): bool { a is Dog };
+procedure test(a: Animal): bool opaque { a is Dog };
 ")
 
 -- Additional coverage: while loops
 
 /--
 info: procedure test()
-{ var x: int := 0; while(x < 10)
-  invariant x >= 0 { x := x + 1 } };
+  opaque
+{
+  var x: int := 0;
+  while(x < 10)
+    invariant x >= 0 {
+    x := x + 1
+  }
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
-procedure test() {
+procedure test() opaque {
     var x: int := 0;
     while(x < 10)
       invariant x >= 0
@@ -203,7 +235,10 @@ procedure modify(c: Container)
   opaque
   ensures true
   modifies c
-{ c#value := c#value + 1; true };
+{
+  c#value := c#value + 1;
+  true
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
@@ -219,9 +254,12 @@ procedure modify(c: Container)
 
 /--
 info: procedure test(): int
-{ <??> };
+  opaque
+{
+  <??>
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure test(): int { <??> };")
+#eval do IO.println (← roundtrip r"procedure test(): int opaque { <??> };")
 
 end Strata.Laurel

StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean

@@ -44,15 +44,25 @@ def parseLaurelAndElim (input : String) : IO Program := do
 
 /--
 info: function nat$constraint(x: int): bool
-{ x >= 0 };
+{
+  x >= 0
+};
 procedure test(n: int)
   returns (r: int)
   requires nat$constraint(n)
   opaque
   ensures nat$constraint(r)
-{ assert r >= 0; var y: int := n; assert nat$constraint(y); return y };
+{
+  assert r >= 0;
+  var y: int := n;
+  assert nat$constraint(y);
+  return y
+};
 procedure $witness_nat()
-{ var $witness: int := 0; assert nat$constraint($witness) };
+{
+  var $witness: int := 0;
+  assert nat$constraint($witness)
+};
 -/
 #guard_msgs in
 #eval! do
@@ -76,11 +86,25 @@ procedure test(b: bool) {
 
 /--
 info: function pos$constraint(v: int): bool
-{ v > 0 };
+{
+  v > 0
+};
 procedure test(b: bool)
-{ if b then { var x: int := 1; assert pos$constraint(x) }; { var x: int := -5; x := -10 } };
+{
+  if b then {
+    var x: int := 1;
+    assert pos$constraint(x)
+  };
+  {
+    var x: int := -5;
+    x := -10
+  }
+};
 procedure $witness_pos()
-{ var $witness: int := 1; assert pos$constraint($witness) };
+{
+  var $witness: int := 1;
+  assert pos$constraint($witness)
+};
 -/
 #guard_msgs in
 #eval! do
@@ -92,19 +116,29 @@ procedure $witness_pos()
 -- The variable has no known value, only the type constraint is assumed.
 def uninitProgram : String := r"
 constrained posint = x: int where x > 0 witness 1
-procedure f() {
+procedure f() opaque {
   var x: posint;
   assert x == 1
 };
 "
 
 /--
 info: function posint$constraint(x: int): bool
-{ x > 0 };
+{
+  x > 0
+};
 procedure f()
-{ var x: int; assume posint$constraint(x); assert x == 1 };
+  opaque
+{
+  var x: int;
+  assume posint$constraint(x);
+  assert x == 1
+};
 procedure $witness_posint()
-{ var $witness: int := 1; assert posint$constraint($witness) };
+{
+  var $witness: int := 1;
+  assert posint$constraint($witness)
+};
 -/
 #guard_msgs in
 #eval! do