module Language where

open import Language.Base public
open import Language.Semantics public
open import Language.Traces public
open import Language.Graphs public
open import Language.Properties public

open import Data.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.Any as RelAny using ()
open import Data.Nat using (ℕ; suc)
open import Data.Product using (_,_; Σ; proj₁; proj₂)
open import Data.Product.Properties as ProdProp using ()
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (¬_)

open import Lattice
open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs)
open import Lattice.MapSet _≟ˢ_ using ()
    renaming
        ( MapSet to StringSet
        ; to-List to to-Listˢ
        )

record Program : Set where
    field
        rootStmt : Stmt

    graph : Graph
    graph = wrap (buildCfg rootStmt)

    State : Set
    State = Graph.Index graph

    initialState : State
    initialState = proj₁ (wrap-input (buildCfg rootStmt))

    finalState : State
    finalState = proj₁ (wrap-output (buildCfg rootStmt))

    trace : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → Trace {graph} initialState finalState [] ρ
    trace {ρ} ∅,s⇒ρ
        with MkEndToEndTrace idx₁ (RelAny.here refl) idx₂ (RelAny.here refl) tr
             ← EndToEndTrace-wrap (buildCfg-sufficient ∅,s⇒ρ) = tr

    private
        vars-Set : StringSet
        vars-Set = Stmt-vars rootStmt

    vars : List String
    vars = to-Listˢ vars-Set

    vars-Unique : Unique vars
    vars-Unique = proj₂ vars-Set

    states : List State
    states = indices graph

    states-complete : ∀ (s : State) → s ListMem.∈ states
    states-complete = indices-complete graph

    states-Unique : Unique states
    states-Unique = indices-Unique graph

    code : State → List BasicStmt
    code st = graph [ st ]

    -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ListMem.∈ vars
    -- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}

    _≟_ : IsDecidable (_≡_ {_} {State})
    _≟_ = FinProp._≟_

    _≟ᵉ_ : IsDecidable (_≡_ {_} {Graph.Edge graph})
    _≟ᵉ_ = ProdProp.≡-dec _≟_ _≟_

    open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_)

    incoming : State → List State
    incoming = predecessors graph

    initialState-pred-∅ : incoming initialState ≡ []
    initialState-pred-∅ =
        wrap-preds-∅ (buildCfg rootStmt) initialState (RelAny.here refl)

    edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) →
                    s₁ ListMem.∈ (incoming s₂)
    edge⇒incoming = edge⇒predecessor graph