agda-spa/lean/Spa/Language.lean

import Spa.Language.Base
import Spa.Language.Semantics
import Spa.Language.Graphs
import Spa.Language.Traces
import Spa.Language.Properties
import Mathlib.Data.Finset.Sort
import Mathlib.Data.String.Basic

namespace Spa

structure Program where
  rootStmt : Stmt

namespace Program

variable (p : Program)

def cfg : Graph := Graph.wrap p.rootStmt.cfg

abbrev State : Type := p.cfg.Index

def initialState : p.State := p.rootStmt.cfg.wrapInput

def finalState : p.State := p.rootStmt.cfg.wrapOutput

theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
    Trace p.cfg p.initialState p.finalState [] ρ := by
  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₂
  exact tr

def vars : List String := p.rootStmt.vars.sort (· ≤ ·)

theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _

def states : List p.State := p.cfg.indices

theorem states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s

theorem states_nodup : p.states.Nodup := p.cfg.nodup_indices

def code (st : p.State) : List BasicStmt := p.cfg.nodes st

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 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.cfg.edges) : s₁ ∈ p.incoming s₂ :=
  p.cfg.mem_predecessors_of_edge h

end Program

end Spa