DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Remove sketch if proof since the proof is done

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-13 12:31:04 -07:00
parent b6e357787f
commit ba1c9b3ec8
1 changed files with 0 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
Language.agda
View File

@ -484,44 +484,6 @@ 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