From ba1c9b3ec8f19e59c91d834d6a21ea7348b29f8c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 13 Apr 2024 12:31:04 -0700 Subject: [PATCH] Remove sketch if proof since the proof is done Signed-off-by: Danila Fedorin --- Language.agda | 38 -------------------------------------- 1 file changed, 38 deletions(-) diff --git a/Language.agda b/Language.agda index 7cdf8a0..f643de8 100644 --- a/Language.agda +++ b/Language.agda @@ -484,44 +484,6 @@ 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