Fix trailing whitespace

Author: andrewmwells-amazon

Strata/DL/Call/CallCapable.lean

@@ -20,43 +20,43 @@ languages that support calls.
 class CallCapable (Stmt : Type) where
   -- Create a simple function call (no return value)
   simpleCall : String → List Heap.HExpr → Stmt
-  
+
   -- Create a function call with return values
   call : List String → String → List Heap.HExpr → Stmt
-  
+
   -- Inspection methods for analyses
   getCallInfo : Stmt → Option (List String × String × List Heap.HExpr)  -- (lhs, funcName, args)
-  
+
   -- Check if this statement is a call
   isCall : Stmt → Bool
-  
+
   -- Extract the underlying imperative statement if possible
   asImperativeStmt : Stmt → Option (Imperative.Stmt (Imperative.Cmd Heap.HExpr))
 
 -- Default implementation for Call dialect statements
 instance : CallCapable (CallStatement Heap.HExpr) where
-  simpleCall funcName args := 
+  simpleCall funcName args :=
     CallStatement.simpleCall funcName args
-    
-  call lhs funcName args := 
+
+  call lhs funcName args :=
     CallStatement.call lhs funcName args
-    
+
   getCallInfo stmt := match stmt with
     | .cmd (.directCall lhs funcName args) => some (lhs, funcName, args)
     | _ => none
-    
+
   isCall stmt := match stmt with
     | .cmd (.directCall _ _ _) => true
     | _ => false
-    
+
   asImperativeStmt stmt := match stmt with
     | .cmd (.imperativeCmd cmd) => some (.cmd cmd)
-    | .ite cond thenb elseb => 
+    | .ite cond thenb elseb =>
       -- Convert blocks by filtering out calls (for now)
       let thenStmts := thenb.ss.filterMap (fun s => match s with
         | .cmd (.imperativeCmd cmd) => some (.cmd cmd)
         | _ => none)
-      let elseStmts := elseb.ss.filterMap (fun s => match s with  
+      let elseStmts := elseb.ss.filterMap (fun s => match s with
         | .cmd (.imperativeCmd cmd) => some (.cmd cmd)
         | _ => none)
       some (.ite cond ⟨thenStmts⟩ ⟨elseStmts⟩)

Strata/DL/Call/CallEval.lean

@@ -19,7 +19,7 @@ specific dialect that uses Call (e.g., Heap dialect).
 class CallEvaluator (State : Type) (P : Imperative.PureExpr) where
   -- Evaluate a direct function call
   evalDirectCall : (lhs : List String) → (funcName : String) → (args : List P.Expr) → State → State
-  
+
   -- Evaluate an imperative command (delegate to the base dialect)
   evalImperativeCmd : Imperative.Cmd P → State → State
 

Strata/DL/DataFlow.lean

@@ -18,7 +18,7 @@ namespace DataFlow
 -- DataLocation abstracts storage locations across different dialects
 inductive DataLocation where
   | variable : String → DataLocation                    -- Variable: x
-  | heapField : String → Nat → DataLocation           -- Heap field: obj[5]  
+  | heapField : String → Nat → DataLocation           -- Heap field: obj[5]
   | dynamicField : String → String → DataLocation     -- Dynamic field: obj[key]
   | functionParam : String → Nat → DataLocation       -- Function parameter: func.param[0]
   | functionResult : String → DataLocation            -- Function return value: func.result

Strata/DL/Generic/TranslationContext.lean

@@ -58,7 +58,7 @@ def TranslationContext.addFunction {S T : Type} (ctx : TranslationContext S T) (
   { ctx with functions := func :: ctx.functions }
 
 -- Empty context
-def TranslationContext.empty {S T : Type} : TranslationContext S T := 
+def TranslationContext.empty {S T : Type} : TranslationContext S T :=
   { functions := [] }
 
 end Generic