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.Relation.Unary.All using (All; []; _∷_) 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ˢ ) 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' indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique indices 0 = ([] , Utils.empty) indices (suc n') = let (inds' , unids') = indices n' in ( zero ∷ List.map suc inds' , push (z≢mapsfs inds') (Unique-map suc suc-injective unids') ) indices-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (indices n)) indices-complete (suc n') zero = RelAny.here refl indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f')) record Program : Set where field rootStmt : Stmt graph : Graph graph = buildCfg rootStmt State : Set State = Graph.Index graph initialState : State initialState = proj₁ (buildCfg-input rootStmt) finalState : State finalState = proj₁ (buildCfg-output rootStmt) 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 = proj₁ (indices (Graph.size graph)) states-complete : ∀ (s : State) → s ListMem.∈ states states-complete = indices-complete (Graph.size graph) states-Unique : Unique states states-Unique = proj₂ (indices (Graph.size 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 idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges graph)) states