module Language where open import Data.Nat using (ℕ; suc; pred; _≤_) renaming (_+_ to _+ⁿ_) open import Data.Nat.Properties using (m≤n⇒m≤n+o; ≤-reflexive; +-assoc; +-comm) open import Data.Integer using (ℤ; +_) renaming (_+_ to _+ᶻ_; _-_ to _-ᶻ_) open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) open import Data.Vec using (Vec; foldr; lookup; _∷_; []; _++_; cast) open import Data.Vec.Properties using (++-assoc; ++-identityʳ; lookup-++ˡ; lookup-cast₁) open import Data.Vec.Relation.Binary.Equality.Cast using (cast-is-id) open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ; _++_ to _++ˡ_) open import Data.List.Properties using () renaming (++-assoc to ++ˡ-assoc; map-++ to mapˡ-++ˡ; ++-identityʳ to ++ˡ-identityʳ) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.Any as RelAny using () open import Data.List.Relation.Unary.Any.Properties using (++⁺ʳ) open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁; inject≤; _↑ʳ_; _↑ˡ_) renaming (_≟_ to _≟ᶠ_; cast to castᶠ) open import Data.Fin.Properties using (suc-injective) open import Relation.Binary.PropositionalEquality as Eq using (subst; cong; _≡_; sym; trans; refl) open import Relation.Nullary using (¬_) open import Function using (_∘_) open Eq.≡-Reasoning open import Lattice open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs; _⊗_; _,_) data Expr : Set where _+_ : Expr → Expr → Expr _-_ : Expr → Expr → Expr `_ : String → Expr #_ : ℕ → Expr data BasicStmt : Set where _←_ : String → Expr → BasicStmt noop : BasicStmt data Stmt : Set where ⟨_⟩ : BasicStmt → Stmt _then_ : Stmt → Stmt → Stmt if_then_else_ : Expr → Stmt → Stmt → Stmt while_repeat_ : Expr → Stmt → Stmt module Semantics where data Value : Set where ↑ᶻ : ℤ → Value Env : Set Env = List (String × Value) data _∈_ : (String × Value) → Env → Set where here : ∀ (s : String) (v : Value) (ρ : Env) → (s , v) ∈ ((s , v) ∷ ρ) there : ∀ (s s' : String) (v v' : Value) (ρ : Env) → ¬ (s ≡ s') → (s , v) ∈ ρ → (s , v) ∈ ((s' , v') ∷ ρ) data _,_⇒ᵉ_ : Env → Expr → Value → Set where ⇒ᵉ-ℕ : ∀ (ρ : Env) (n : ℕ) → ρ , (# n) ⇒ᵉ (↑ᶻ (+ n)) ⇒ᵉ-Var : ∀ (ρ : Env) (x : String) (v : Value) → (x , v) ∈ ρ → ρ , (` x) ⇒ᵉ v ⇒ᵉ-+ : ∀ (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) → ρ , e₁ ⇒ᵉ (↑ᶻ z₁) → ρ , e₂ ⇒ᵉ (↑ᶻ z₂) → ρ , (e₁ + e₂) ⇒ᵉ (↑ᶻ (z₁ +ᶻ z₂)) ⇒ᵉ-- : ∀ (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) → ρ , e₁ ⇒ᵉ (↑ᶻ z₁) → ρ , e₂ ⇒ᵉ (↑ᶻ z₂) → ρ , (e₁ - e₂) ⇒ᵉ (↑ᶻ (z₁ -ᶻ z₂)) data _,_⇒ᵇ_ : Env → BasicStmt → Env → Set where ⇒ᵇ-noop : ∀ (ρ : Env) → ρ , noop ⇒ᵇ ρ ⇒ᵇ-← : ∀ (ρ : Env) (x : String) (e : Expr) (v : Value) → ρ , e ⇒ᵉ v → ρ , (x ← e) ⇒ᵇ ((x , v) ∷ ρ) data _,_⇒ˢ_ : Env → Stmt → Env → Set where ⇒ˢ-⟨⟩ : ∀ (ρ₁ ρ₂ : Env) (bs : BasicStmt) → ρ₁ , bs ⇒ᵇ ρ₂ → ρ₁ , ⟨ bs ⟩ ⇒ˢ ρ₂ ⇒ˢ-then : ∀ (ρ₁ ρ₂ ρ₃ : Env) (s₁ s₂ : Stmt) → ρ₁ , s₁ ⇒ˢ ρ₂ → ρ₂ , s₂ ⇒ˢ ρ₃ → ρ₁ , (s₁ then s₂) ⇒ˢ ρ₃ ⇒ˢ-if-true : ∀ (ρ₁ ρ₂ : Env) (e : Expr) (z : ℤ) (s₁ s₂ : Stmt) → ρ₁ , e ⇒ᵉ (↑ᶻ z) → ¬ z ≡ (+ 0) → ρ₁ , s₁ ⇒ˢ ρ₂ → ρ₁ , (if e then s₁ else s₂) ⇒ˢ ρ₂ ⇒ˢ-if-false : ∀ (ρ₁ ρ₂ : Env) (e : Expr) (s₁ s₂ : Stmt) → ρ₁ , e ⇒ᵉ (↑ᶻ (+ 0)) → ρ₁ , s₂ ⇒ˢ ρ₂ → ρ₁ , (if e then s₁ else s₂) ⇒ˢ ρ₂ ⇒ˢ-while-true : ∀ (ρ₁ ρ₂ ρ₃ : Env) (e : Expr) (z : ℤ) (s : Stmt) → ρ₁ , e ⇒ᵉ (↑ᶻ z) → ¬ z ≡ (+ 0) → ρ₁ , s ⇒ˢ ρ₂ → ρ₂ , (while e repeat s) ⇒ˢ ρ₃ → ρ₁ , (while e repeat s) ⇒ˢ ρ₃ ⇒ˢ-while-false : ∀ (ρ : Env) (e : Expr) (s : Stmt) → ρ , e ⇒ᵉ (↑ᶻ (+ 0)) → ρ , (while e repeat s) ⇒ˢ ρ module Graphs where open Semantics 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 ↑ˡ-Edge : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n +ⁿ m) × Fin (n +ⁿ m)) ↑ˡ-Edge (idx₁ , idx₂) m = (idx₁ ↑ˡ m , idx₂ ↑ˡ m) _[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt _[_] g idx = lookup (Graph.nodes g) idx record _⊆_ (g₁ g₂ : Graph) : Set where constructor Mk-⊆ field n : ℕ sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ +ⁿ n g₁[]≡g₂[] : ∀ (idx : Graph.Index g₁) → lookup (Graph.nodes g₁) idx ≡ lookup (cast sg₂≡sg₁+n (Graph.nodes g₂)) (idx ↑ˡ n) e∈g₁⇒e∈g₂ : ∀ (e : Graph.Edge g₁) → e ∈ˡ (Graph.edges g₁) → (↑ˡ-Edge e n) ∈ˡ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂)) ⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃ ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃} (Mk-⊆ n₁ p₁@refl g₁[]≡g₂[] e∈g₁⇒e∈g₂) (Mk-⊆ n₂ p₂@refl g₂[]≡g₃[] e∈g₂⇒e∈g₃) = record { n = n₁ +ⁿ n₂ ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂ ; g₁[]≡g₂[] = λ idx → begin lookup ns₁ idx ≡⟨ g₁[]≡g₂[] _ ⟩ lookup (cast p₁ ns₂) (idx ↑ˡ n₁) ≡⟨ lookup-cast₁ p₁ ns₂ _ ⟩ lookup ns₂ (castᶠ (sym p₁) (idx ↑ˡ n₁)) ≡⟨ g₂[]≡g₃[] _ ⟩ lookup (cast p₂ ns₃) ((castᶠ (sym p₁) (idx ↑ˡ n₁)) ↑ˡ n₂) ≡⟨ lookup-cast₁ p₂ _ _ ⟩ lookup ns₃ (castᶠ (sym p₂) (((castᶠ (sym p₁) (idx ↑ˡ n₁)) ↑ˡ n₂))) ≡⟨ cong (lookup ns₃) (flatten-casts (sym p₂) (sym p₁) (sym (+-assoc s₁ n₁ n₂)) idx) ⟩ lookup ns₃ (castᶠ (sym (+-assoc s₁ n₁ n₂)) (idx ↑ˡ (n₁ +ⁿ n₂))) ≡⟨ sym (lookup-cast₁ (+-assoc s₁ n₁ n₂) _ _) ⟩ lookup (cast (+-assoc s₁ n₁ n₂) ns₃) (idx ↑ˡ (n₁ +ⁿ n₂)) ∎ ; e∈g₁⇒e∈g₂ = {!!} } where flatten-casts : ∀ {s₁ s₂ s₃ n₁ n₂ : ℕ} (p : s₂ +ⁿ n₂ ≡ s₃) (q : s₁ +ⁿ n₁ ≡ s₂) (r : s₁ +ⁿ (n₁ +ⁿ n₂) ≡ s₃) (idx : Fin s₁) → castᶠ p ((castᶠ q (idx ↑ˡ n₁)) ↑ˡ n₂) ≡ castᶠ r (idx ↑ˡ (n₁ +ⁿ n₂)) flatten-casts refl refl r zero = refl flatten-casts {(suc s₁)} {s₂} {s₃} {n₁} {n₂} refl refl r (suc idx') rewrite flatten-casts refl refl (sym (+-assoc s₁ n₁ n₂)) idx' = refl record Relaxable (T : Graph → Set) : Set where field relax : ∀ {g₁ g₂ : Graph} → g₁ ⊆ g₂ → T g₁ → T g₂ instance IndexRelaxable : Relaxable Graph.Index IndexRelaxable = record { relax = λ { (Mk-⊆ n refl _ _) idx → idx ↑ˡ n } } EdgeRelaxable : Relaxable Graph.Edge EdgeRelaxable = record { relax = λ g₁⊆g₂ (idx₁ , idx₂) → ( Relaxable.relax IndexRelaxable g₁⊆g₂ idx₁ , Relaxable.relax IndexRelaxable g₁⊆g₂ idx₂ ) } ProdRelaxable : ∀ {P : Graph → Set} {Q : Graph → Set} → {{ PRelaxable : Relaxable P }} → {{ QRelaxable : Relaxable Q }} → Relaxable (P ⊗ Q) ProdRelaxable {{pr}} {{qr}} = record { relax = (λ { g₁⊆g₂ (p , q) → ( Relaxable.relax pr g₁⊆g₂ p , Relaxable.relax qr g₁⊆g₂ q) } ) } open Relaxable {{...}} public relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) → g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ] relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl g₁[]≡g₂[] _) idx = trans (g₁[]≡g₂[] idx) (cong (λ vec → lookup vec (idx ↑ˡ n)) (cast-is-id refl (Graph.nodes g₂))) MonotonicGraphFunction : (Graph → Set) → Set MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂) infixr 2 _⟨⊗⟩_ _⟨⊗⟩_ : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }} → MonotonicGraphFunction T₁ → MonotonicGraphFunction T₂ → MonotonicGraphFunction (T₁ ⊗ T₂) _⟨⊗⟩_ {{r}} f₁ f₂ g with (g' , (t₁ , g⊆g')) ← f₁ g with (g'' , (t₂ , g'⊆g'')) ← f₂ g' = (g'' , ((Relaxable.relax r g'⊆g'' t₁ , t₂) , ⊆-trans g⊆g' g'⊆g'')) infixl 2 _update_ _update_ : ∀ {T : Graph → Set} {{ TRelaxable : Relaxable T }} → MonotonicGraphFunction T → (∀ (g : Graph) → T g → Σ Graph (λ g' → g ⊆ g')) → MonotonicGraphFunction T _update_ {{r}} f mod g with (g' , (t , g⊆g')) ← f g with (g'' , g'⊆g'') ← mod g' t = (g'' , ((Relaxable.relax r g'⊆g'' t , ⊆-trans g⊆g' g'⊆g''))) infixl 2 _map_ _map_ : ∀ {T₁ T₂ : Graph → Set} → MonotonicGraphFunction T₁ → (∀ (g : Graph) → T₁ g → T₂ g) → MonotonicGraphFunction T₂ _map_ f fn g = let (g' , (t₁ , g⊆g')) = f g in (g' , (fn g' t₁ , g⊆g')) module Construction where pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index pushBasicBlock bss g = ( record { size = Graph.size g +ⁿ 1 ; nodes = Graph.nodes g ++ (bss ∷ []) ; edges = mapˡ (λ e → ↑ˡ-Edge e 1) (Graph.edges g) } , ( Graph.size g ↑ʳ zero , record { n = 1 ; sg₂≡sg₁+n = refl ; g₁[]≡g₂[] = λ idx → trans (sym (lookup-++ˡ (Graph.nodes g) (bss ∷ []) idx)) (sym (cong (λ vec → lookup vec (idx ↑ˡ 1)) (cast-is-id refl (Graph.nodes g ++ (bss ∷ []))))) ; e∈g₁⇒e∈g₂ = λ e e∈g₁ → x∈xs⇒fx∈fxs (λ e' → ↑ˡ-Edge e' 1) e∈g₁ } ) ) addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g') addEdges g es = ( record { size = Graph.size g ; nodes = Graph.nodes g ; edges = es ++ˡ Graph.edges g } , record { n = 0 ; sg₂≡sg₁+n = +-comm 0 (Graph.size g) ; g₁[]≡g₂[] = {!!} ; e∈g₁⇒e∈g₂ = {!!} } ) pushEmptyBlock : MonotonicGraphFunction Graph.Index pushEmptyBlock = pushBasicBlock [] buildCfg : Stmt → MonotonicGraphFunction (Graph.Index ⊗ Graph.Index) buildCfg ⟨ bs₁ ⟩ = pushBasicBlock (bs₁ ∷ []) map (λ g idx → (idx , idx)) buildCfg (s₁ then s₂) = (buildCfg s₁ ⟨⊗⟩ buildCfg s₂) update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → addEdges g ((idx₂ , idx₃) ∷ []) }) map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → (idx₁ , idx₄) }) buildCfg (if _ then s₁ else s₂) = (buildCfg s₁ ⟨⊗⟩ buildCfg s₂ ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock) update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → addEdges g ((idx , idx₁) ∷ (idx , idx₃) ∷ (idx₂ , idx') ∷ (idx₄ , idx') ∷ []) }) map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → (idx , idx') }) buildCfg (while _ repeat s) = (buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock) update (λ { g ((idx₁ , idx₂) , idx , idx') → addEdges g ((idx , idx') ∷ (idx₂ , idx) ∷ []) }) map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') }) open import Lattice.MapSet _≟ˢ_ renaming ( MapSet to StringSet ; insert to insertˢ ; to-List to to-Listˢ ; empty to emptyˢ ; singleton to singletonˢ ; _⊔_ to _⊔ˢ_ ; `_ to `ˢ_ ; _∈_ to _∈ˢ_ ; ⊔-preserves-∈k₁ to ⊔ˢ-preserves-∈k₁ ; ⊔-preserves-∈k₂ to ⊔ˢ-preserves-∈k₂ ) data _∈ᵉ_ : String → Expr → Set where in⁺₁ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₁ → k ∈ᵉ (e₁ + e₂) in⁺₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ + e₂) in⁻₁ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₁ → k ∈ᵉ (e₁ - e₂) in⁻₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ - e₂) here : ∀ {k : String} → k ∈ᵉ (` k) data _∈ᵇ_ : String → BasicStmt → Set where in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵇ (k ← e) in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵇ (k' ← e) private Expr-vars : Expr → StringSet Expr-vars (l + r) = Expr-vars l ⊔ˢ Expr-vars r Expr-vars (l - r) = Expr-vars l ⊔ˢ Expr-vars r Expr-vars (` s) = singletonˢ s Expr-vars (# _) = emptyˢ -- ∈-Expr-vars⇒∈ : ∀ {k : String} (e : Expr) → k ∈ˢ (Expr-vars e) → k ∈ᵉ e -- ∈-Expr-vars⇒∈ {k} (e₁ + e₂) k∈vs -- with Expr-Provenance k ((`ˢ (Expr-vars e₁)) ∪ (`ˢ (Expr-vars e₂))) k∈vs -- ... | in₁ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁))) -- ... | in₂ _ (single k,tt∈vs₂) = (in⁺₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂))) -- ... | bothᵘ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁))) -- ∈-Expr-vars⇒∈ {k} (e₁ - e₂) k∈vs -- with Expr-Provenance k ((`ˢ (Expr-vars e₁)) ∪ (`ˢ (Expr-vars e₂))) k∈vs -- ... | in₁ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁))) -- ... | in₂ _ (single k,tt∈vs₂) = (in⁻₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂))) -- ... | bothᵘ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁))) -- ∈-Expr-vars⇒∈ {k} (` k) (RelAny.here refl) = here -- ∈⇒∈-Expr-vars : ∀ {k : String} {e : Expr} → k ∈ᵉ e → k ∈ˢ (Expr-vars e) -- ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₁ k∈e₁) = -- ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁} -- {m₂ = Expr-vars e₂} -- (∈⇒∈-Expr-vars k∈e₁) -- ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₂ k∈e₂) = -- ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁} -- {m₂ = Expr-vars e₂} -- (∈⇒∈-Expr-vars k∈e₂) -- ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₁ k∈e₁) = -- ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁} -- {m₂ = Expr-vars e₂} -- (∈⇒∈-Expr-vars k∈e₁) -- ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₂ k∈e₂) = -- ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁} -- {m₂ = Expr-vars e₂} -- (∈⇒∈-Expr-vars k∈e₂) -- ∈⇒∈-Expr-vars here = RelAny.here refl BasicStmt-vars : BasicStmt → StringSet BasicStmt-vars (x ← e) = (singletonˢ x) ⊔ˢ (Expr-vars e) BasicStmt-vars noop = emptyˢ Stmt-vars : Stmt → StringSet Stmt-vars ⟨ bs ⟩ = BasicStmt-vars bs Stmt-vars (s₁ then s₂) = (Stmt-vars s₁) ⊔ˢ (Stmt-vars s₂) Stmt-vars (if e then s₁ else s₂) = ((Expr-vars e) ⊔ˢ (Stmt-vars s₁)) ⊔ˢ (Stmt-vars s₂) Stmt-vars (while e repeat s) = (Expr-vars e) ⊔ˢ (Stmt-vars s) -- ∈-Stmt-vars⇒∈ : ∀ {k : String} (s : Stmt) → k ∈ˢ (Stmt-vars s) → k ∈ᵇ s -- ∈-Stmt-vars⇒∈ {k} (k' ← e) k∈vs -- with Expr-Provenance k ((`ˢ (singletonˢ k')) ∪ (`ˢ (Expr-vars e))) k∈vs -- ... | in₁ (single (RelAny.here refl)) _ = in←₁ -- ... | in₂ _ (single k,tt∈vs') = in←₂ (∈-Expr-vars⇒∈ e (forget k,tt∈vs')) -- ... | bothᵘ (single (RelAny.here refl)) _ = in←₁ -- ∈⇒∈-Stmt-vars : ∀ {k : String} {s : Stmt} → k ∈ᵇ s → k ∈ˢ (Stmt-vars s) -- ∈⇒∈-Stmt-vars {k} {k ← e} in←₁ = -- ⊔ˢ-preserves-∈k₁ {m₁ = singletonˢ k} -- {m₂ = Expr-vars e} -- (RelAny.here refl) -- ∈⇒∈-Stmt-vars {k} {k' ← e} (in←₂ k∈e) = -- ⊔ˢ-preserves-∈k₂ {m₁ = singletonˢ k'} -- {m₂ = Expr-vars e} -- (∈⇒∈-Expr-vars k∈e) Stmts-vars : ∀ {n : ℕ} → Vec Stmt n → StringSet Stmts-vars = foldr (λ n → StringSet) (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ -- ∈-Stmts-vars⇒∈ : ∀ {n : ℕ} {k : String} (ss : Vec Stmt n) → -- k ∈ˢ (Stmts-vars ss) → Σ (Fin n) (λ f → k ∈ᵇ lookup ss f) -- ∈-Stmts-vars⇒∈ {suc n'} {k} (s ∷ ss') k∈vss -- with Expr-Provenance k ((`ˢ (Stmt-vars s)) ∪ (`ˢ (Stmts-vars ss'))) k∈vss -- ... | in₁ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs)) -- ... | in₂ _ (single k,tt∈vss') = -- let -- (f' , k∈s') = ∈-Stmts-vars⇒∈ ss' (forget k,tt∈vss') -- in -- (suc f' , k∈s') -- ... | bothᵘ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs)) -- ∈⇒∈-Stmts-vars : ∀ {n : ℕ} {k : String} {ss : Vec Stmt n} {f : Fin n} → -- k ∈ᵇ lookup ss f → k ∈ˢ (Stmts-vars ss) -- ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {zero} k∈s = -- ⊔ˢ-preserves-∈k₁ {m₁ = Stmt-vars s} -- {m₂ = Stmts-vars ss'} -- (∈⇒∈-Stmt-vars k∈s) -- ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {suc f'} k∈ss' = -- ⊔ˢ-preserves-∈k₂ {m₁ = Stmt-vars s} -- {m₂ = Stmts-vars ss'} -- (∈⇒∈-Stmts-vars {n} {k} {ss'} {f'} k∈ss') -- Creating a new number from a natural number can never create one -- equal to one you get from weakening the bounds on another number. z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f) z≢sf f () z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs) z≢mapsfs [] = [] z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs' indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique indices 0 = ([] , empty) indices (suc n') = let (inds' , unids') = indices n' in ( zero ∷ mapˡ suc inds' , push (z≢mapsfs inds') (Unique-map suc suc-injective unids') ) indices-complete : ∀ (n : ℕ) (f : Fin n) → f ∈ˡ (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')) -- Sketch, 'build control flow graph' -- -- Create new block, mark it as the current insertion point. -- emptyBlock : m Id -- currentBlock : m Id -- -- Create a new block, and insert the statement into it. Shold restore insertion pont. -- createBlock : Stmt → m (Id × Id) -- -- Note that the given ID is a successor / predecessor of the given -- -- insertion point. -- noteSuccessor : Id → m () -- notePredecessor : Id → m () -- noteEdge : Id → Id → m () -- -- Insert the given statment into the current insertion point. -- buildCfg : Stmt → m Cfg -- buildCfg { bs₁ } = push bs₁ -- buildCfg (s₁ ; s₂ ) = buildCfg s₁ >> buildCfg s₂ -- buildCfg (if _ then s₁ else s₂) = do -- (b₁ , b₁') ← createBlock s₁ -- noteSuccessor b₁ -- (b₂ , b₂') ← createBlock s₂ -- noteSuccessor b₂ -- b ← emptyBlock -- notePredecessor b₁' -- notePredecessor b₂' -- buildCfg (while e repeat s) = do -- (b₁, b₁') ← createBlock s -- noteSuccessor b₁ -- noteEdge b₁' b₁ -- b ← emptyBlock -- notePredecessor b₁' -- For now, just represent the program and CFG as one type, without branching. record Program : Set where field length : ℕ stmts : Vec Stmt length private vars-Set : StringSet vars-Set = Stmts-vars stmts vars : List String vars = to-Listˢ vars-Set vars-Unique : Unique vars vars-Unique = proj₂ vars-Set State : Set State = Fin length states : List State states = proj₁ (indices length) states-complete : ∀ (s : State) → s ∈ˡ states states-complete = indices-complete length states-Unique : Unique states states-Unique = proj₂ (indices length) code : State → Stmt code = lookup stmts -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ∈ˡ vars -- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s} _≟_ : IsDecidable (_≡_ {_} {State}) _≟_ = _≟ᶠ_ -- Computations for incoming and outgoing edges will have to change too -- when we support branching etc. incoming : State → List State incoming with length ... | 0 = (λ ()) ... | suc n' = (λ { zero → [] ; (suc f') → (inject₁ f') ∷ [] })