Intermediate commit: add while loops and start trying to formalize them.

This commit is contained in:
Danila Fedorin 2024-04-03 22:29:58 -07:00
parent 5d56a7ce2d
commit 844c99336a

View File

@ -1,8 +1,9 @@
module Language where module Language where
open import Data.Nat using (; suc; pred) 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.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.Vec using (Vec; foldr; lookup; _∷_)
open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ) open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
@ -23,8 +24,60 @@ data Expr : Set where
`_ : String Expr `_ : String Expr
#_ : Expr #_ : Expr
data BasicStmt : Set where
_←_ : String Expr BasicStmt
noop : BasicStmt
data Stmt : Set where 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 _≟ˢ_ open import Lattice.MapSet _≟ˢ_
renaming renaming
@ -47,9 +100,9 @@ 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₂)
here : {k : String} k ∈ᵉ (` k) here : {k : String} k ∈ᵉ (` k)
data _∈_ : String Stmt Set where data _∈_ : String BasicStmt Set where
in←₁ : {k : String} {e : Expr} k (k e) in←₁ : {k : String} {e : Expr} k (k e)
in←₂ : {k k' : String} {e : Expr} k ∈ᵉ e k (k' e) in←₂ : {k k' : String} {e : Expr} k ∈ᵉ e k (k' e)
private private
Expr-vars : Expr StringSet Expr-vars : Expr StringSet
@ -58,84 +111,91 @@ private
Expr-vars (` s) = singletonˢ s Expr-vars (` s) = singletonˢ s
Expr-vars (# _) = emptyˢ Expr-vars (# _) = emptyˢ
∈-Expr-vars⇒∈ : {k : String} (e : Expr) k ∈ˢ (Expr-vars e) k ∈ᵉ e -- ∈-Expr-vars⇒∈ : ∀ {k : String} (e : Expr) → k ∈ˢ (Expr-vars e) → k ∈ᵉ e
∈-Expr-vars⇒∈ {k} (e₁ + e₂) k∈vs -- ∈-Expr-vars⇒∈ {k} (e₁ + e₂) k∈vs
with Expr-Provenance k (( (Expr-vars e₁)) ( (Expr-vars 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₁)))
... | 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₁))) -- ... | bothᵘ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
∈-Expr-vars⇒∈ {k} (e₁ - e₂) k∈vs -- ∈-Expr-vars⇒∈ {k} (e₁ - e₂) k∈vs
with Expr-Provenance k (( (Expr-vars e₁)) ( (Expr-vars 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₁)))
... | 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₁))) -- ... | bothᵘ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
∈-Expr-vars⇒∈ {k} (` k) (RelAny.here refl) = here -- ∈-Expr-vars⇒∈ {k} (` k) (RelAny.here refl) = here
∈⇒∈-Expr-vars : {k : String} {e : Expr} k ∈ᵉ e k ∈ˢ (Expr-vars e) -- ∈⇒∈-Expr-vars : ∀ {k : String} {e : Expr} → k ∈ᵉ e → k ∈ˢ (Expr-vars e)
∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₁ k∈e₁) = -- ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₁ k∈e₁) =
⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁} -- ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
{m₂ = Expr-vars e₂} -- {m₂ = Expr-vars e₂}
(∈⇒∈-Expr-vars k∈e₁) -- (∈⇒∈-Expr-vars k∈e₁)
∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₂ k∈e₂) = -- ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₂ k∈e₂) =
⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁} -- ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
{m₂ = Expr-vars e₂} -- {m₂ = Expr-vars e₂}
(∈⇒∈-Expr-vars k∈e₂) -- (∈⇒∈-Expr-vars k∈e₂)
∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₁ k∈e₁) = -- ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₁ k∈e₁) =
⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁} -- ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
{m₂ = Expr-vars e₂} -- {m₂ = Expr-vars e₂}
(∈⇒∈-Expr-vars k∈e₁) -- (∈⇒∈-Expr-vars k∈e₁)
∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₂ k∈e₂) = -- ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₂ k∈e₂) =
⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁} -- ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
{m₂ = Expr-vars e₂} -- {m₂ = Expr-vars e₂}
(∈⇒∈-Expr-vars k∈e₂) -- (∈⇒∈-Expr-vars k∈e₂)
∈⇒∈-Expr-vars here = RelAny.here refl -- ∈⇒∈-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 : 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 : String} (s : Stmt) → k ∈ˢ (Stmt-vars s) → k ∈ᵇ s
∈-Stmt-vars⇒∈ {k} (k' e) k∈vs -- ∈-Stmt-vars⇒∈ {k} (k' ← e) k∈vs
with Expr-Provenance k (( (singletonˢ k')) ( (Expr-vars e))) k∈vs -- with Expr-Provenance k ((`ˢ (singletonˢ k')) (`ˢ (Expr-vars e))) k∈vs
... | in (single (RelAny.here refl)) _ = in←₁ -- ... | in₁ (single (RelAny.here refl)) _ = in←₁
... | 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 (RelAny.here refl)) _ = in←₁ -- ... | bothᵘ (single (RelAny.here refl)) _ = in←₁
∈⇒∈-Stmt-vars : {k : String} {s : Stmt} k ∈ᵗ s k ∈ˢ (Stmt-vars s) -- ∈⇒∈-Stmt-vars : ∀ {k : String} {s : Stmt} → k ∈ᵇ s → k ∈ˢ (Stmt-vars s)
∈⇒∈-Stmt-vars {k} {k e} in←₁ = -- ∈⇒∈-Stmt-vars {k} {k ← e} in←₁ =
⊔ˢ-preserves-∈k₁ {m₁ = singletonˢ k} -- ⊔ˢ-preserves-∈k₁ {m₁ = singletonˢ k}
{m₂ = Expr-vars e} -- {m₂ = Expr-vars e}
(RelAny.here refl) -- (RelAny.here refl)
∈⇒∈-Stmt-vars {k} {k' e} (in←₂ k∈e) = -- ∈⇒∈-Stmt-vars {k} {k' ← e} (in←₂ k∈e) =
⊔ˢ-preserves-∈k₂ {m₁ = singletonˢ k'} -- ⊔ˢ-preserves-∈k₂ {m₁ = singletonˢ k'}
{m₂ = Expr-vars e} -- {m₂ = Expr-vars e}
(∈⇒∈-Expr-vars k∈e) -- (∈⇒∈-Expr-vars k∈e)
Stmts-vars : {n : } Vec Stmt n StringSet Stmts-vars : {n : } Vec Stmt n StringSet
Stmts-vars = foldr (λ n StringSet) Stmts-vars = foldr (λ n StringSet)
(λ {k} stmt acc (Stmt-vars stmt) ⊔ˢ acc) emptyˢ (λ {k} stmt acc (Stmt-vars stmt) ⊔ˢ acc) emptyˢ
∈-Stmts-vars⇒∈ : {n : } {k : String} (ss : Vec Stmt n) -- ∈-Stmts-vars⇒∈ : ∀ {n : } {k : String} (ss : Vec Stmt n)
k ∈ˢ (Stmts-vars ss) Σ (Fin n) (λ f k ∈ᵗ lookup ss f) -- k ∈ˢ (Stmts-vars ss) → Σ (Fin n) (λ f → k ∈ᵇ lookup ss f)
∈-Stmts-vars⇒∈ {suc n'} {k} (s ss') k∈vss -- ∈-Stmts-vars⇒∈ {suc n'} {k} (s ∷ ss') k∈vss
with Expr-Provenance k (( (Stmt-vars s)) ( (Stmts-vars 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∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
... | in _ (single k,tt∈vss') = -- ... | in₂ _ (single k,tt∈vss') =
let -- let
(f' , k∈s') = ∈-Stmts-vars⇒∈ ss' (forget k,tt∈vss') -- (f' , k∈s') = ∈-Stmts-vars⇒∈ ss' (forget k,tt∈vss')
in -- in
(suc f' , k∈s') -- (suc f' , k∈s')
... | bothᵘ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs)) -- ... | 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} -- ∈⇒∈-Stmts-vars : ∀ {n : } {k : String} {ss : Vec Stmt n} {f : Fin n}
k ∈ᵗ lookup ss f k ∈ˢ (Stmts-vars ss) -- k ∈ᵇ lookup ss f → k ∈ˢ (Stmts-vars ss)
∈⇒∈-Stmts-vars {suc n} {k} {s ss'} {zero} k∈s = -- ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {zero} k∈s =
⊔ˢ-preserves-∈k₁ {m₁ = Stmt-vars s} -- ⊔ˢ-preserves-∈k₁ {m₁ = Stmt-vars s}
{m₂ = Stmts-vars ss'} -- {m₂ = Stmts-vars ss'}
(∈⇒∈-Stmt-vars k∈s) -- (∈⇒∈-Stmt-vars k∈s)
∈⇒∈-Stmts-vars {suc n} {k} {s ss'} {suc f'} k∈ss' = -- ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {suc f'} k∈ss' =
⊔ˢ-preserves-∈k₂ {m₁ = Stmt-vars s} -- ⊔ˢ-preserves-∈k₂ {m₁ = Stmt-vars s}
{m₂ = Stmts-vars ss'} -- {m₂ = Stmts-vars ss'}
(∈⇒∈-Stmts-vars {n} {k} {ss'} {f'} k∈ss') -- (∈⇒∈-Stmts-vars {n} {k} {ss'} {f'} k∈ss')
-- Creating a new number from a natural number can never create one -- Creating a new number from a natural number can never create one
-- equal to one you get from weakening the bounds on another number. -- 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') zero = RelAny.here refl
indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f')) 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. -- For now, just represent the program and CFG as one type, without branching.
record Program : Set where record Program : Set where
@ -192,8 +290,8 @@ record Program : Set where
code : State Stmt code : State Stmt
code = lookup stmts code = lookup stmts
vars-complete : {k : String} (s : State) k ∈ᵗ (code s) k ∈ˡ vars -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ∈ˡ vars
vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s} -- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}
_≟_ : IsDecidable (_≡_ {_} {State}) _≟_ : IsDecidable (_≡_ {_} {State})
_≟_ = _≟ᶠ_ _≟_ = _≟ᶠ_