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 (∈-filter⁺)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as RelAny using ()
open import Data.Nat as Nat using (ℕ; suc)
open import Data.Nat.Properties using (+-assoc; +-comm)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Product.Properties as ProdProp 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 Relation.Nullary using (¬_)

open import Lattice
open import Utils using (Unique; push; Unique-map; 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 ∷ []
    }

wrap : Graph → Graph
wrap g = singleton [] ↦ g ↦ singleton []

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)

private
    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
    z≢sf f ()

    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
    z≢mapsfs [] = []
    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'

    finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
    finValues 0 = ([] , Utils.empty)
    finValues (suc n') =
        let
            (inds' , unids') = finValues n'
        in
            ( zero ∷ List.map suc inds'
            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
            )

    finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n))
    finValues-complete (suc n') zero = RelAny.here refl
    finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))

module _ (g : Graph) where
    open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size g}) (FinProp._≟_ {Graph.size g})) using (_∈?_)

    indices : List (Graph.Index g)
    indices = proj₁ (finValues (Graph.size g))

    indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices
    indices-complete = finValues-complete (Graph.size g)

    indices-Unique : Unique indices
    indices-Unique = proj₂ (finValues (Graph.size g))

    predecessors : (Graph.Index g) → List (Graph.Index g)
    predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices

    edge⇒predecessor : ∀ {idx₁ idx₂ : Graph.Index g} → (idx₁ , idx₂) ListMem.∈ (Graph.edges g) →
                    idx₁ ListMem.∈ (predecessors idx₂)
    edge⇒predecessor {idx₁} {idx₂} idx₁,idx₂∈es =
        ∈-filter⁺ (λ idx' → (idx' , idx₂) ∈? (Graph.edges g))
                  (indices-complete idx₁) idx₁,idx₂∈es