import Spa.Language.Semantics
import Spa.Language.Graphs
import Spa.Language.Program

/-!

# Program Traces

This module defines program traces tied to Control Flow Graphs, or CFGs
(see `Spa.GGraph` and `Spa.Graph`). These traces boil town to sequences of
basic-block executions (really, `Spa.BasicStmt` executions), each of which must
have an actual basic block in the graph _and_ be connected to the previous
basic block by an edge. In this way, traces encode executions admitted
by the CFG.

While the regular `Trace` is just _any_ path through the graph, an
`EndToEndTrace` is a path from the entry node to the exit node, denoting
full program execution.

Properties about graphs and language semantics (especially,
the fact that the graph contains the proper basic block and edges
to represent any program execution according to the
language's big-step semantics `EvalStmt`) is found
in `Spa/Language/Properties.lean`.

-/

namespace Spa

/-- A partial trace through a graph `g`, starting right before
    the execution of the basic block at the first index, and
    ending right after the execution of the basic block at the last index. -/
inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Type
  | single {ρ₁ ρ₂ : Env} {idx : g.Index} :
      EvalBasicStmtOpt ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂
  | edge {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : g.Index} :
      EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
      Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃

/-- Sequence two traces together. Since the endpoint of the first trace
    is _after_ its last basic block's execution, and the beginning of
    the next trace is _before_ its first basic block's execution,
    there must be an edge to connect the two. -/
noncomputable def Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
    {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂)
    (he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) :
    Trace g idx₁ idx₄ ρ₁ ρ₃ := by
  induction tr₁ with
  | single hbs => exact Trace.edge hbs he tr₂
  | edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂)

scoped notation:65 tr₁:66 " ++< " he " >++ " tr₂:65 => Trace.concat tr₁ he tr₂

/-- A beginning-to-end trace corresponding to the CFG `g`. -/
inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Type
  | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs)
      (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs)
      (trace : Trace g idx₁ idx₂ ρ₁ ρ₂) : EndToEndTrace g ρ₁ ρ₂

inductive MyReaches {prog : Program} : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} →
    Trace prog.cfg s₁ s₂ ρ₁ ρ₂ →
    (s : prog.State) → (ρin ρout : Env) → Type
  | single_here {s₁ : prog.State} {ρ₁ ρ₂ : Env}
      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) :
      MyReaches (.single hnode) s₁ ρ₁ ρ₂
  | edge_here {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env}
      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) :
      MyReaches (.edge hnode hedge rest) s₁ ρ₁ ρ₂
  | edge_there {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env}
      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃)
      {s : prog.State} {ρin ρout : Env} :
      MyReaches rest s ρin ρout →
      MyReaches (.edge hnode hedge rest) s ρin ρout

noncomputable def MyReaches.prefix {prog : Program} {s₁ s₂ s: prog.State}
    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
    (r : MyReaches tr s ρin ρout) → Trace prog.cfg s₁ s ρ₁ ρout
  | .single_here hnode => Spa.Trace.single hnode
  | .edge_here hnode hedge hrest => Spa.Trace.single hnode
  | .edge_there hnode hedge hrest tmp' => Spa.Trace.edge hnode hedge tmp'.prefix

noncomputable def MyReaches.first {prog : Program} {s₁ s₂ s: prog.State}
    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
    (r : MyReaches tr s ρin ρout) → Σ ρ₁', MyReaches tr s₁ ρ₁ ρ₁'
  | .single_here hnode => ⟨_, .single_here hnode⟩
  | .edge_here hnode hedge hrest => ⟨_, .edge_here hnode hedge hrest⟩
  | .edge_there hnode hedge hrest tmp' => ⟨_, .edge_here hnode hedge hrest⟩

noncomputable def MyReaches.step {prog : Program} {s₁ s₂ s: prog.State}
    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
    (r : MyReaches tr s ρin ρout) → EvalBasicStmtOpt ρin (prog.code s) ρout
  | .single_here hnode => hnode
  | .edge_here hnode hedge hrest => hnode
  | .edge_there hnode hedge hrest tmp' => tmp'.step


end Spa