From de956cdc6a0815b31b27e282f9914a3b168f6254 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 13 Apr 2024 18:39:38 -0700 Subject: [PATCH] Split the Language file into modules Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 2 +- Language.agda | 507 +++------------------------------------- Language/Base.agda | 145 ++++++++++++ Language/Graphs.agda | 280 ++++++++++++++++++++++ Language/Semantics.agda | 55 +++++ 5 files changed, 508 insertions(+), 481 deletions(-) create mode 100644 Language/Base.agda create mode 100644 Language/Graphs.agda create mode 100644 Language/Semantics.agda diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index cf9aa1a..ac1c832 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -1,4 +1,4 @@ -open import Language +open import Language hiding (_[_]) open import Lattice module Analysis.Forward diff --git a/Language.agda b/Language.agda index de86158..7bc21b6 100644 --- a/Language.agda +++ b/Language.agda @@ -1,506 +1,53 @@ 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.Product.Properties using (≡-dec) -open import Data.Vec using (Vec; foldr; lookup; _∷_; []; _++_; cast) -open import Data.Vec.Properties using (++-assoc; ++-identityʳ; lookup-++ˡ; lookup-cast₁; cast-sym) -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ˡ; filter to filterᶠ; _++_ 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.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ) +open import Language.Base public +open import Language.Semantics public +open import Language.Graphs 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.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) renaming (cast-is-id to castᶠ-is-id) -open import Relation.Binary.PropositionalEquality as Eq using (subst; cong; _≡_; sym; trans; refl) +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 Relation.Nullary.Decidable.Core using (does) -open import Function using (_∘_) -open Eq.≡-Reasoning open import Lattice -open import Utils using (Unique; Unique-map; push; x∈xs⇒fx∈fxs; _⊗_; _,_) renaming (empty to emptyᵘ; proj₁ to proj₁'; proj₂ to proj₂') - -data Expr : Set where - _+_ : Expr → Expr → Expr - _-_ : Expr → Expr → Expr - `_ : String → Expr - #_ : ℕ → Expr - -data BasicStmt : Set where - _←_ : String → Expr → BasicStmt - noop : BasicStmt - -infixr 2 _then_ -infix 3 while_repeat_ -infix 3 if_then_else_ -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 - - empty : Graph - empty = record - { size = 0 - ; nodes = [] - ; edges = [] - } - - ↑ˡ-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 - newNodes : Vec (List BasicStmt) n - nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes - 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₂)) - - castᵉ : ∀ {n m : ℕ} .(p : n ≡ m) → (Fin n × Fin n) → (Fin m × Fin m) - castᵉ p (idx₁ , idx₂) = (castᶠ p idx₁ , castᶠ p idx₂) - - ↑ˡ-assoc : ∀ {s n₁ n₂} (f : Fin s) (p : s +ⁿ (n₁ +ⁿ n₂) ≡ s +ⁿ n₁ +ⁿ n₂) → - f ↑ˡ n₁ ↑ˡ n₂ ≡ castᶠ p (f ↑ˡ (n₁ +ⁿ n₂)) - ↑ˡ-assoc zero p = refl - ↑ˡ-assoc {suc s'} {n₁} {n₂} (suc f') p rewrite ↑ˡ-assoc f' (sym (+-assoc s' n₁ n₂)) = refl - - ↑ˡ-Edge-assoc : ∀ {s n₁ n₂} (e : Fin s × Fin s) (p : s +ⁿ (n₁ +ⁿ n₂) ≡ s +ⁿ n₁ +ⁿ n₂) → - ↑ˡ-Edge (↑ˡ-Edge e n₁) n₂ ≡ castᵉ p (↑ˡ-Edge e (n₁ +ⁿ n₂)) - ↑ˡ-Edge-assoc (idx₁ , idx₂) p - rewrite ↑ˡ-assoc idx₁ p - rewrite ↑ˡ-assoc idx₂ p = refl - - ↑ˡ-identityʳ : ∀ {s} (f : Fin s) (p : s +ⁿ 0 ≡ s) → - f ≡ castᶠ p (f ↑ˡ 0) - ↑ˡ-identityʳ zero p = refl - ↑ˡ-identityʳ {suc s'} (suc f') p rewrite sym (↑ˡ-identityʳ f' (+-comm s' 0)) = refl - - ↑ˡ-Edge-identityʳ : ∀ {s} (e : Fin s × Fin s) (p : s +ⁿ 0 ≡ s) → - e ≡ castᵉ p (↑ˡ-Edge e 0) - ↑ˡ-Edge-identityʳ (idx₁ , idx₂) p - rewrite sym (↑ˡ-identityʳ idx₁ p) - rewrite sym (↑ˡ-identityʳ idx₂ p) = refl - - cast∈⇒∈subst : ∀ {n m : ℕ} (p : n ≡ m) (q : m ≡ n) - (e : Fin n × Fin n) (es : List (Fin m × Fin m)) → - castᵉ p e ∈ˡ es → - e ∈ˡ subst (λ m → List (Fin m × Fin m)) q es - cast∈⇒∈subst refl refl (idx₁ , idx₂) es e∈es - rewrite castᶠ-is-id refl idx₁ - rewrite castᶠ-is-id refl idx₂ = e∈es - - ⊆-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 newNodes₁ nsg₂≡nsg₁++newNodes₁ e∈g₁⇒e∈g₂) - (Mk-⊆ n₂ p₂@refl newNodes₂ nsg₃≡nsg₂++newNodes₂ e∈g₂⇒e∈g₃) - rewrite cast-is-id refl ns₂ - rewrite cast-is-id refl ns₃ - with refl ← nsg₂≡nsg₁++newNodes₁ - with refl ← nsg₃≡nsg₂++newNodes₂ = - record - { n = n₁ +ⁿ n₂ - ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂ - ; newNodes = newNodes₁ ++ newNodes₂ - ; nsg₂≡nsg₁++newNodes = ++-assoc (+-assoc s₁ n₁ n₂) ns₁ newNodes₁ newNodes₂ - ; e∈g₁⇒e∈g₂ = λ {e} e∈g₁ → - cast∈⇒∈subst (sym (+-assoc s₁ n₁ n₂)) (+-assoc s₁ n₁ n₂) _ _ - (subst (λ e' → e' ∈ˡ es₃) - (↑ˡ-Edge-assoc e (sym (+-assoc s₁ n₁ n₂))) - (e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁))) - } - - 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 newNodes nsg₂≡nsg₁++newNodes _) idx - rewrite cast-is-id refl (Graph.nodes g₂) - with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes g₁) _ _) - - -- Tools for graph construction. The most important is a 'monotonic function': - -- one that takes a graph, and produces another graph, such that the - -- new graph includes all the information from the old one. - - MonotonicGraphFunction : (Graph → Set) → Set - MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂) - - -- Now, define some operations on monotonic functions; these are useful - -- to save the work of threading intermediate graphs in and out of operations. - - 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')) - - - -- To reason about monotonic functions and what we do, we need a way - -- to describe values they produce. A 'graph-value predicate' is - -- just a predicate for some (dependent) value. - - GraphValuePredicate : (Graph → Set) → Set₁ - GraphValuePredicate T = ∀ (g : Graph) → T g → Set - - Both : {T₁ T₂ : Graph → Set} → GraphValuePredicate T₁ → GraphValuePredicate T₂ → - GraphValuePredicate (T₁ ⊗ T₂) - Both P Q = (λ { g (t₁ , t₂) → (P g t₁ × Q g t₂) }) - - -- Since monotnic functions keep adding on to a function, proofs of - -- graph-value predicates go stale fast (they describe old values of - -- the graph). To keep propagating them through, we need them to still - -- on 'bigger graphs'. We call such predicates monotonic as well, since - -- they respect the ordering of graphs. - - MonotonicPredicate : ∀ {T : Graph → Set} {{ TRelaxable : Relaxable T }} → - GraphValuePredicate T → Set - MonotonicPredicate {T} P = ∀ (g₁ g₂ : Graph) (t₁ : T g₁) (g₁⊆g₂ : g₁ ⊆ g₂) → - P g₁ t₁ → P g₂ (relax g₁⊆g₂ t₁) - - - -- A 'map' has a certain property if its ouputs satisfy that property - -- for all inputs. - - always : ∀ {T : Graph → Set} → GraphValuePredicate T → MonotonicGraphFunction T → Set - always P m = ∀ g₁ → let (g₂ , t , _) = m g₁ in P g₂ t - - ⟨⊗⟩-reason : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }} - {P : GraphValuePredicate T₁} {Q : GraphValuePredicate T₂} - {P-Mono : MonotonicPredicate P} - {m₁ : MonotonicGraphFunction T₁} {m₂ : MonotonicGraphFunction T₂} → - always P m₁ → always Q m₂ → always (Both P Q) (m₁ ⟨⊗⟩ m₂) - ⟨⊗⟩-reason {P-Mono = P-Mono} {m₁ = m₁} {m₂ = m₂} aP aQ g - with p ← aP g - with (g' , (t₁ , g⊆g')) ← m₁ g - with q ← aQ g' - with (g'' , (t₂ , g'⊆g'')) ← m₂ g' = (P-Mono _ _ _ g'⊆g'' p , q) - - 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 - ; newNodes = (bss ∷ []) - ; nsg₂≡nsg₁++newNodes = cast-is-id refl _ - ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e → ↑ˡ-Edge e 1) e∈g₁ - } - ) - ) - - addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g') - addEdges (MkGraph s ns es) es' = - ( record - { size = s - ; nodes = ns - ; edges = es' ++ˡ es - } - , record - { n = 0 - ; sg₂≡sg₁+n = +-comm 0 s - ; newNodes = [] - ; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns) - ; e∈g₁⇒e∈g₂ = λ {e} e∈es → - cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _ - (subst (λ e' → e' ∈ˡ _) - (↑ˡ-Edge-identityʳ e (+-comm s 0)) - (∈ˡ-++⁺ʳ es' e∈es)) - } - ) - - 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₁) ∷ (idx₂ , idx) ∷ []) }) - map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') }) - -open import Lattice.MapSet _≟ˢ_ +open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs) +open import Lattice.MapSet _≟ˢ_ using () 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 : ∀ {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 = ([] , emptyᵘ) + indices 0 = ([] , Utils.empty) indices (suc n') = let (inds' , unids') = indices n' in - ( zero ∷ mapˡ suc inds' + ( zero ∷ List.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 : ∀ (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')) - --- For now, just represent the program and CFG as one type, without branching. record Program : Set where - open Graphs - field rootStmt : Stmt @@ -514,10 +61,10 @@ record Program : Set where State = Graph.Index graph initialState : State - initialState = proj₁' (proj₁ (proj₂ buildResult)) + initialState = Utils.proj₁ (proj₁ (proj₂ buildResult)) finalState : State - finalState = proj₂' (proj₁ (proj₂ buildResult)) + finalState = Utils.proj₂ (proj₁ (proj₂ buildResult)) private vars-Set : StringSet @@ -532,7 +79,7 @@ record Program : Set where states : List State states = proj₁ (indices (Graph.size graph)) - states-complete : ∀ (s : State) → s ∈ˡ states + states-complete : ∀ (s : State) → s ListMem.∈ states states-complete = indices-complete (Graph.size graph) states-Unique : Unique states @@ -541,16 +88,16 @@ record Program : Set where code : State → List BasicStmt code st = graph [ st ] - -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ∈ˡ vars + -- 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}) - _≟ᵉ_ = ≡-dec _≟_ _≟_ + _≟ᵉ_ = ProdProp.≡-dec _≟_ _≟_ - open import Data.List.Membership.DecPropositional _≟ᵉ_ using () renaming (_∈?_ to _∈ˡ?_) + open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_) incoming : State → List State - incoming idx = filterᶠ (λ idx' → (idx' , idx) ∈ˡ? (Graph.edges graph)) states + incoming idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges graph)) states diff --git a/Language/Base.agda b/Language/Base.agda new file mode 100644 index 0000000..35d3f88 --- /dev/null +++ b/Language/Base.agda @@ -0,0 +1,145 @@ +module Language.Base where + +open import Data.List as List using (List) +open import Data.Nat using (ℕ; suc) +open import Data.Product using (Σ; _,_; proj₁) +open import Data.String as String using (String) +open import Data.Vec using (Vec; foldr; lookup) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Lattice + +data Expr : Set where + _+_ : Expr → Expr → Expr + _-_ : Expr → Expr → Expr + `_ : String → Expr + #_ : ℕ → Expr + +data BasicStmt : Set where + _←_ : String → Expr → BasicStmt + noop : BasicStmt + +infixr 2 _then_ +infix 3 if_then_else_ +infix 3 while_repeat_ +data Stmt : Set where + ⟨_⟩ : BasicStmt → Stmt + _then_ : Stmt → Stmt → Stmt + if_then_else_ : Expr → Stmt → Stmt → Stmt + while_repeat_ : Expr → Stmt → Stmt + +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) + +open import Lattice.MapSet (String._≟_) + renaming + ( MapSet to StringSet + ; insert to insertˢ + ; empty to emptyˢ + ; singleton to singletonˢ + ; _⊔_ to _⊔ˢ_ + ; `_ to `ˢ_ + ; _∈_ to _∈ˢ_ + ; ⊔-preserves-∈k₁ to ⊔ˢ-preserves-∈k₁ + ; ⊔-preserves-∈k₂ to ⊔ˢ-preserves-∈k₂ + ) + +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') diff --git a/Language/Graphs.agda b/Language/Graphs.agda new file mode 100644 index 0000000..8bb07f0 --- /dev/null +++ b/Language/Graphs.agda @@ -0,0 +1,280 @@ +module Language.Graphs where + +open import Language.Base +open import Language.Semantics + +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ʳ) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst) + +open import Lattice +open import Utils using (x∈xs⇒fx∈fxs; _⊗_; _,_) + +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 + +empty : Graph +empty = record + { size = 0 + ; nodes = [] + ; edges = [] + } + +↑ˡ-Edge : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n Nat.+ m) × Fin (n Nat.+ 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₁ Nat.+ n + newNodes : Vec (List BasicStmt) n + nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes + e∈g₁⇒e∈g₂ : ∀ {e : Graph.Edge g₁} → + e ListMem.∈ (Graph.edges g₁) → + (↑ˡ-Edge e n) ListMem.∈ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂)) + +castᵉ : ∀ {n m : ℕ} .(p : n ≡ m) → (Fin n × Fin n) → (Fin m × Fin m) +castᵉ p (idx₁ , idx₂) = (Fin.cast p idx₁ , Fin.cast p idx₂) + +↑ˡ-assoc : ∀ {s n₁ n₂} (f : Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) ≡ s Nat.+ n₁ Nat.+ n₂) → + f ↑ˡ n₁ ↑ˡ n₂ ≡ Fin.cast p (f ↑ˡ (n₁ Nat.+ n₂)) +↑ˡ-assoc zero p = refl +↑ˡ-assoc {suc s'} {n₁} {n₂} (suc f') p rewrite ↑ˡ-assoc f' (sym (+-assoc s' n₁ n₂)) = refl + +↑ˡ-Edge-assoc : ∀ {s n₁ n₂} (e : Fin s × Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) ≡ s Nat.+ n₁ Nat.+ n₂) → + ↑ˡ-Edge (↑ˡ-Edge e n₁) n₂ ≡ castᵉ p (↑ˡ-Edge e (n₁ Nat.+ n₂)) +↑ˡ-Edge-assoc (idx₁ , idx₂) p + rewrite ↑ˡ-assoc idx₁ p + rewrite ↑ˡ-assoc idx₂ p = refl + +↑ˡ-identityʳ : ∀ {s} (f : Fin s) (p : s Nat.+ 0 ≡ s) → + f ≡ Fin.cast p (f ↑ˡ 0) +↑ˡ-identityʳ zero p = refl +↑ˡ-identityʳ {suc s'} (suc f') p rewrite sym (↑ˡ-identityʳ f' (+-comm s' 0)) = refl + +↑ˡ-Edge-identityʳ : ∀ {s} (e : Fin s × Fin s) (p : s Nat.+ 0 ≡ s) → + e ≡ castᵉ p (↑ˡ-Edge e 0) +↑ˡ-Edge-identityʳ (idx₁ , idx₂) p + rewrite sym (↑ˡ-identityʳ idx₁ p) + rewrite sym (↑ˡ-identityʳ idx₂ p) = refl + +cast∈⇒∈subst : ∀ {n m : ℕ} (p : n ≡ m) (q : m ≡ n) + (e : Fin n × Fin n) (es : List (Fin m × Fin m)) → + castᵉ p e ListMem.∈ es → + e ListMem.∈ subst (λ m → List (Fin m × Fin m)) q es +cast∈⇒∈subst refl refl (idx₁ , idx₂) es e∈es + rewrite FinProp.cast-is-id refl idx₁ + rewrite FinProp.cast-is-id refl idx₂ = e∈es + +⊆-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 newNodes₁ nsg₂≡nsg₁++newNodes₁ e∈g₁⇒e∈g₂) + (Mk-⊆ n₂ p₂@refl newNodes₂ nsg₃≡nsg₂++newNodes₂ e∈g₂⇒e∈g₃) + rewrite cast-is-id refl ns₂ + rewrite cast-is-id refl ns₃ + with refl ← nsg₂≡nsg₁++newNodes₁ + with refl ← nsg₃≡nsg₂++newNodes₂ = + record + { n = n₁ Nat.+ n₂ + ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂ + ; newNodes = newNodes₁ ++ newNodes₂ + ; nsg₂≡nsg₁++newNodes = ++-assoc (+-assoc s₁ n₁ n₂) ns₁ newNodes₁ newNodes₂ + ; e∈g₁⇒e∈g₂ = λ {e} e∈g₁ → + cast∈⇒∈subst (sym (+-assoc s₁ n₁ n₂)) (+-assoc s₁ n₁ n₂) _ _ + (subst (λ e' → e' ListMem.∈ es₃) + (↑ˡ-Edge-assoc e (sym (+-assoc s₁ n₁ n₂))) + (e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁))) + } + +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 newNodes nsg₂≡nsg₁++newNodes _) idx + rewrite cast-is-id refl (Graph.nodes g₂) + with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes g₁) _ _) + +-- Tools for graph construction. The most important is a 'monotonic function': +-- one that takes a graph, and produces another graph, such that the +-- new graph includes all the information from the old one. + +MonotonicGraphFunction : (Graph → Set) → Set +MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂) + +-- Now, define some operations on monotonic functions; these are useful +-- to save the work of threading intermediate graphs in and out of operations. + +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')) + + +-- To reason about monotonic functions and what we do, we need a way +-- to describe values they produce. A 'graph-value predicate' is +-- just a predicate for some (dependent) value. + +GraphValuePredicate : (Graph → Set) → Set₁ +GraphValuePredicate T = ∀ (g : Graph) → T g → Set + +Both : {T₁ T₂ : Graph → Set} → GraphValuePredicate T₁ → GraphValuePredicate T₂ → + GraphValuePredicate (T₁ ⊗ T₂) +Both P Q = (λ { g (t₁ , t₂) → (P g t₁ × Q g t₂) }) + +-- Since monotnic functions keep adding on to a function, proofs of +-- graph-value predicates go stale fast (they describe old values of +-- the graph). To keep propagating them through, we need them to still +-- on 'bigger graphs'. We call such predicates monotonic as well, since +-- they respect the ordering of graphs. + +MonotonicPredicate : ∀ {T : Graph → Set} {{ TRelaxable : Relaxable T }} → + GraphValuePredicate T → Set +MonotonicPredicate {T} P = ∀ (g₁ g₂ : Graph) (t₁ : T g₁) (g₁⊆g₂ : g₁ ⊆ g₂) → + P g₁ t₁ → P g₂ (relax g₁⊆g₂ t₁) + + +-- A 'map' has a certain property if its ouputs satisfy that property +-- for all inputs. + +always : ∀ {T : Graph → Set} → GraphValuePredicate T → MonotonicGraphFunction T → Set +always P m = ∀ g₁ → let (g₂ , t , _) = m g₁ in P g₂ t + +⟨⊗⟩-reason : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }} + {P : GraphValuePredicate T₁} {Q : GraphValuePredicate T₂} + {P-Mono : MonotonicPredicate P} + {m₁ : MonotonicGraphFunction T₁} {m₂ : MonotonicGraphFunction T₂} → + always P m₁ → always Q m₂ → always (Both P Q) (m₁ ⟨⊗⟩ m₂) +⟨⊗⟩-reason {P-Mono = P-Mono} {m₁ = m₁} {m₂ = m₂} aP aQ g + with p ← aP g + with (g' , (t₁ , g⊆g')) ← m₁ g + with q ← aQ g' + with (g'' , (t₂ , g'⊆g'')) ← m₂ g' = (P-Mono _ _ _ g'⊆g'' p , q) + +module Construction where + pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index + pushBasicBlock bss g = + ( record + { size = Graph.size g Nat.+ 1 + ; nodes = Graph.nodes g ++ (bss ∷ []) + ; edges = List.map (λ e → ↑ˡ-Edge e 1) (Graph.edges g) + } + , ( Graph.size g ↑ʳ zero + , record + { n = 1 + ; sg₂≡sg₁+n = refl + ; newNodes = (bss ∷ []) + ; nsg₂≡nsg₁++newNodes = cast-is-id refl _ + ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e → ↑ˡ-Edge e 1) e∈g₁ + } + ) + ) + + addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g') + addEdges (MkGraph s ns es) es' = + ( record + { size = s + ; nodes = ns + ; edges = es' List.++ es + } + , record + { n = 0 + ; sg₂≡sg₁+n = +-comm 0 s + ; newNodes = [] + ; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns) + ; e∈g₁⇒e∈g₂ = λ {e} e∈es → + cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _ + (subst (λ e' → e' ListMem.∈ _) + (↑ˡ-Edge-identityʳ e (+-comm s 0)) + (ListMemProp.∈-++⁺ʳ es' e∈es)) + } + ) + + 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₁) ∷ (idx₂ , idx) ∷ []) }) + map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') }) diff --git a/Language/Semantics.agda b/Language/Semantics.agda new file mode 100644 index 0000000..6ee8611 --- /dev/null +++ b/Language/Semantics.agda @@ -0,0 +1,55 @@ +module Language.Semantics where + +open import Language.Base + +open import Data.Integer using (ℤ; +_) renaming (_+_ to _+ᶻ_; _-_ to _-ᶻ_) +open import Data.Product using (_×_; _,_) +open import Data.String using (String) +open import Data.List using (List; _∷_) +open import Data.Nat using (ℕ) +open import Relation.Nullary using (¬_) +open import Relation.Binary.PropositionalEquality using (_≡_) + +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) ⇒ˢ ρ