module Language.Graphs where

open import Language.Base using (Expr; Stmt; BasicStmt; ⟨_⟩; _then_; if_then_else_; while_repeat_)

open import Data.Fin as Fin using (Fin; suc; zero)
open import Data.Fin.Properties as FinProp using (suc-injective)
open import Data.List as List using (List; []; _∷_)
open import Data.List.Membership.Propositional as ListMem using ()
open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
open import Data.Nat as Nat using (ℕ; suc)
open import Data.Nat.Properties using (+-assoc; +-comm)
open import Data.Product using (_×_; Σ; _,_)
open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_)
open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)

open import Lattice
open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct)

record Graph : Set where
    constructor MkGraph
    field
        size : ℕ

    Index : Set
    Index = Fin size

    Edge : Set
    Edge = Index × Index

    field
        nodes : Vec (List BasicStmt) size
        edges : List Edge
        inputs : List Index
        outputs : List Index

_↑ˡ_ : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n Nat.+ m) × Fin (n Nat.+ m))
_↑ˡ_ (idx₁ , idx₂) m = (idx₁ Fin.↑ˡ m , idx₂ Fin.↑ˡ m)

_↑ʳ_ : ∀ {m} n → (Fin m × Fin m) → Fin (n Nat.+ m) × Fin (n Nat.+ m)
_↑ʳ_ n (idx₁ , idx₂) = (n Fin.↑ʳ idx₁ , n Fin.↑ʳ idx₂)

_↑ˡⁱ_ : ∀ {n} → List (Fin n) → ∀ m → List (Fin (n Nat.+ m))
_↑ˡⁱ_ l m = List.map (Fin._↑ˡ m) l

_↑ʳⁱ_ : ∀ {m} n → List (Fin m) → List (Fin (n Nat.+ m))
_↑ʳⁱ_ n l = List.map (n Fin.↑ʳ_) l

_↑ˡᵉ_ : ∀ {n} → List (Fin n × Fin n) → ∀ m → List (Fin (n Nat.+ m) × Fin (n Nat.+ m))
_↑ˡᵉ_ l m = List.map (_↑ˡ m) l

_↑ʳᵉ_ : ∀ {m} n → List (Fin m × Fin m) → List (Fin (n Nat.+ m) × Fin (n Nat.+ m))
_↑ʳᵉ_ n l = List.map (n ↑ʳ_) l

infixr 5 _∙_
_∙_ : Graph → Graph → Graph
_∙_ g₁ g₂ = record
    { size = Graph.size g₁ Nat.+ Graph.size g₂
    ; nodes = Graph.nodes g₁ ++ Graph.nodes g₂
    ; edges = (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) List.++
              (Graph.size g₁ ↑ʳᵉ Graph.edges g₂)
    ; inputs = (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂) List.++
               (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂)
    ; outputs = (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂) List.++
                (Graph.size g₁ ↑ʳⁱ Graph.outputs g₂)
    }

infixr 5 _↦_
_↦_ : Graph → Graph → Graph
_↦_ g₁ g₂ = record
    { size = Graph.size g₁ Nat.+ Graph.size g₂
    ; nodes = Graph.nodes g₁ ++ Graph.nodes g₂
    ; edges = (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) List.++
              (Graph.size g₁ ↑ʳᵉ Graph.edges g₂) List.++
              (List.cartesianProduct (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂)
                                     (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂))
    ; inputs = Graph.inputs g₁ ↑ˡⁱ Graph.size g₂
    ; outputs = Graph.size g₁ ↑ʳⁱ Graph.outputs g₂
    }

loop : Graph → Graph
loop g = record
    { size = 2 Nat.+ Graph.size g
    ; nodes = [] ∷ [] ∷ Graph.nodes g
    ; edges = (2 ↑ʳᵉ Graph.edges g) List.++
              List.map (zero ,_) (2 ↑ʳⁱ Graph.inputs g) List.++
              List.map (_, suc zero) (2 ↑ʳⁱ Graph.outputs g) List.++
              ((suc zero , zero) ∷ (zero , suc zero) ∷ [])
    ; inputs = zero ∷ []
    ; outputs = (suc zero) ∷ []
    }

infixr 5 _skipto_
_skipto_ : Graph → Graph → Graph
_skipto_ g₁ g₂ = record (g₁ ∙ g₂)
    { edges = Graph.edges (g₁ ∙ g₂) List.++
              (List.cartesianProduct (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂)
                                     (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂))
    ; inputs = Graph.inputs g₁ ↑ˡⁱ Graph.size g₂
    ; outputs = Graph.size g₁ ↑ʳⁱ Graph.inputs g₂
    }

_[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
_[_] g idx = lookup (Graph.nodes g) idx

singleton : List BasicStmt → Graph
singleton bss = record
    { size = 1
    ; nodes = bss ∷ []
    ; edges = []
    ; inputs = zero ∷ []
    ; outputs = zero ∷ []
    }

buildCfg : Stmt → Graph
buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ [])
buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton []
buildCfg (while _ repeat s) = loop (buildCfg s)