From 844c99336a42830a418bf86f630f770e62b29c36 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 3 Apr 2024 22:29:58 -0700 Subject: [PATCH] Intermediate commit: add while loops and start trying to formalize them. --- Language.agda | 246 +++++++++++++++++++++++++++++++++++--------------- 1 file changed, 172 insertions(+), 74 deletions(-) diff --git a/Language.agda b/Language.agda index a9bc644..ceb9b8a 100644 --- a/Language.agda +++ b/Language.agda @@ -1,8 +1,9 @@ module Language where open import Data.Nat using (ℕ; suc; pred) +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 using (_×_; Σ; _,_; proj₁; proj₂) open import Data.Vec using (Vec; foldr; lookup; _∷_) open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) @@ -23,8 +24,60 @@ data Expr : Set where `_ : String → Expr #_ : ℕ → Expr +data BasicStmt : Set where + _←_ : String → Expr → BasicStmt + noop : BasicStmt + data Stmt : Set where - _←_ : String → Expr → Stmt + ⟨_⟩ : 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) ⇒ˢ ρ open import Lattice.MapSet _≟ˢ_ renaming @@ -47,9 +100,9 @@ data _∈ᵉ_ : String → Expr → Set where in⁻₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ - e₂) here : ∀ {k : String} → k ∈ᵉ (` k) -data _∈ᵗ_ : String → Stmt → Set where - in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵗ (k ← e) - in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵗ (k' ← e) +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 @@ -58,84 +111,91 @@ private 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 ∈ˢ (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 + -- ∈⇒∈-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 (x ← e) = (singletonˢ x) ⊔ˢ (Expr-vars e) + 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 ∈ˢ (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) + -- ∈⇒∈-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) → + -- 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') + -- ∈⇒∈-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. @@ -160,6 +220,44 @@ private 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 @@ -192,8 +290,8 @@ record Program : Set where 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} + -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ∈ˡ vars + -- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s} _≟_ : IsDecidable (_≡_ {_} {State}) _≟_ = _≟ᶠ_