Add scoped quotation syntax for object-language programs

Introduce [spa_e| ... ] for Expr and [spa| ... ] for Stmt, scoped to the
Spa namespace via a dedicated syntax category and macro_rules. This removes
the deeply nested .andThen / .basic (.assign ...) boilerplate when writing
programs; Main.lean's test programs are rewritten to use it.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018Yq5SmPQfNfzAEUpUXRo66

lean/Main.lean

@@ -1,26 +1,30 @@
 import Spa.Analysis.Sign
 import Spa.Analysis.Constant
+import Spa.Language.Notation
 
 namespace Spa
 
-def testCode : Stmt :=
-  .andThen (.basic (.assign "zero" (.num 0)))
-    (.andThen (.basic (.assign "pos" (.add (.var "zero") (.num 1))))
-      (.andThen (.basic (.assign "neg" (.sub (.var "zero") (.num 1))))
-        (.basic (.assign "unknown" (.add (.var "pos") (.var "neg"))))))
+def testCode : Stmt := [obj_stmt|
+  zero    := 0;
+  pos     := zero + 1;
+  neg     := zero - 1;
+  unknown := pos + neg
+]
 
-def testCodeCond₁ : Stmt :=
-  .andThen (.basic (.assign "var" (.num 1)))
-    (.ifElse (.var "var")
-      (.basic (.assign "var" (.add (.var "var") (.num 1))))
-      (.andThen (.basic (.assign "var" (.sub (.var "var") (.num 1))))
-        (.basic (.assign "var" (.num 1)))))
+def testCodeCond₁ : Stmt := [obj_stmt|
+  var := 1;
+  if var {
+    var := var + 1
+  } else {
+    var := var - 1;
+    var := 1
+  }
+]
 
-def testCodeCond₂ : Stmt :=
-  .andThen (.basic (.assign "var" (.num 1)))
-    (.ifElse (.var "var")
-      (.basic (.assign "x" (.num 1)))
-      (.basic .noop))
+def testCodeCond₂ : Stmt := [obj_stmt|
+  var := 1;
+  if var { x := 1 } else { noop }
+]
 
 def testProgram : Program := ⟨testCode⟩