Turn buildCfg into a method

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

lean/Spa/Analysis/Forward.lean

@@ -94,7 +94,7 @@ theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
 
 theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
     (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁)
-    (tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) :
+    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
     ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ := by
   induction tr with
   | single hbss => exact stepTrace hjoin hbss

lean/Spa/Language.lean

@@ -15,17 +15,17 @@ namespace Program
 
 variable (p : Program)
 
-def graph : Graph := Graph.wrap (buildCfg p.rootStmt)
+def cfg : Graph := Graph.wrap p.rootStmt.cfg
 
-abbrev State : Type := p.graph.Index
+abbrev State : Type := p.cfg.Index
 
-def initialState : p.State := (buildCfg p.rootStmt).wrapInput
+def initialState : p.State := p.rootStmt.cfg.wrapInput
 
-def finalState : p.State := (buildCfg p.rootStmt).wrapOutput
+def finalState : p.State := p.rootStmt.cfg.wrapOutput
 
 theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
-    Trace p.graph p.initialState p.finalState [] ρ := by
+    Trace p.cfg p.initialState p.finalState [] ρ := by
-  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (buildCfg_sufficient h)
+  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (Stmt.cfg_sufficient h)
   rw [Graph.wrap_inputs, List.mem_singleton] at h₁
   rw [Graph.wrap_outputs, List.mem_singleton] at h₂
   subst h₁; subst h₂
@@ -35,23 +35,23 @@ def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
 
 theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
 
-def states : List p.State := p.graph.indices
+def states : List p.State := p.cfg.indices
 
-theorem states_complete (s : p.State) : s ∈ p.states := p.graph.mem_indices s
+theorem states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s
 
-theorem states_nodup : p.states.Nodup := p.graph.nodup_indices
+theorem states_nodup : p.states.Nodup := p.cfg.nodup_indices
 
-def code (st : p.State) : List BasicStmt := p.graph.nodes st
+def code (st : p.State) : List BasicStmt := p.cfg.nodes st
 
-def incoming (s : p.State) : List p.State := p.graph.predecessors s
+def incoming (s : p.State) : List p.State := p.cfg.predecessors s
 
 theorem incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
-  Graph.wrap_predecessors_eq_nil (buildCfg p.rootStmt) p.initialState
+  Graph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState
     (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
 
 theorem mem_incoming_of_edge {s₁ s₂ : p.State}
-    (h : (s₁, s₂) ∈ p.graph.edges) : s₁ ∈ p.incoming s₂ :=
+    (h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ :=
-  p.graph.mem_predecessors_of_edge h
+  p.cfg.mem_predecessors_of_edge h
 
 end Program
 

lean/Spa/Language/Graphs.lean

@@ -167,10 +167,10 @@ export GGraph (comp link loop skipto singleton wrap loop_inputs loop_outputs)
 end Graph
 
 open Graph in
-def buildCfg : Stmt → Graph
+def Stmt.cfg : Stmt → Graph
   | .basic bs => singleton [bs]
-  | .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂
+  | .andThen s₁ s₂ => s₁.cfg ⤳  s₂.cfg
-  | .ifElse _ s₁ s₂ => buildCfg s₁ ∙ buildCfg s₂
+  | .ifElse _ s₁ s₂ => s₁.cfg ∙ s₂.cfg
-  | .whileLoop _ s => loop (buildCfg s)
+  | .whileLoop _ s => loop s.cfg
 
 end Spa

lean/Spa/Language/Properties.lean

@@ -174,8 +174,8 @@ theorem EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
     (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
   (EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))
 
-theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
+theorem Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
-    (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace (buildCfg s) ρ₁ ρ₂ := by
+    (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace s.cfg ρ₁ ρ₂ := by
   induction h with
   | basic ρ₁ ρ₂ bs hbs =>
     exact EndToEndTrace.singleton (EvalBasicStmts.cons hbs EvalBasicStmts.nil)