agda-spa/Language.agda
Danila Fedorin 3e2719d45f Turn old proof into a hole to clean up later.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-04-08 22:45:04 -07:00

513 lines
24 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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₃) (↑ˡ-assoc (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₂ = {!!} -- λ e∈g₁ → e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁)
}
where
↑ˡ-assoc : {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₂))
↑ˡ-assoc refl refl r zero = refl
↑ˡ-assoc {(suc s₁)} {s₂} {s₃} {n₁} {n₂} refl refl r (suc idx')
rewrite ↑ˡ-assoc 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∈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
; g₁[]≡g₂[] = λ idx
begin
lookup ns idx
≡⟨ cong (lookup ns) (↑ˡ-identityʳ (sym (+-comm 0 s)) idx)
lookup ns (castᶠ (sym (+-comm 0 s)) (idx ↑ˡ 0))
≡⟨ sym (lookup-cast₁ (+-comm 0 s) _ _)
lookup (cast (+-comm 0 s) ns) (idx ↑ˡ 0)
; e∈g₁⇒e∈g₂ = {!!}
}
)
where
↑ˡ-identityʳ : {s} (p : s +ⁿ 0 s) (idx : Fin s)
idx castᶠ p (idx ↑ˡ 0)
↑ˡ-identityʳ p zero = refl
↑ˡ-identityʳ {suc s'} p (suc f')
rewrite sym (↑ˡ-identityʳ (+-comm s' 0) f') = refl
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') []
})