From 037358308fceedd83432e40ba2df0acebfb67c44 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 27 Apr 2024 13:50:06 -0700 Subject: [PATCH] Fix up Graph construction --- Language/Graphs.agda | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/Language/Graphs.agda b/Language/Graphs.agda index 338f739..5fcd259 100644 --- a/Language/Graphs.agda +++ b/Language/Graphs.agda @@ -79,13 +79,19 @@ _↦_ g₁ g₂ = record } loop : Graph → Graph -loop g = record - { size = Graph.size g - ; nodes = Graph.nodes g - ; edges = Graph.edges g List.++ +loop g = record g + { edges = Graph.edges g List.++ List.cartesianProduct (Graph.outputs g) (Graph.inputs g) - ; inputs = Graph.inputs g - ; outputs = Graph.outputs g + } + +infixl 5 _skipto_ +_skipto_ : Graph → Graph → Graph +_skipto_ g₁ g₂ = record (g₁ ∙ g₂) + { edges = Graph.edges (g₁ ∙ g₂) List.++ + (List.cartesianProduct (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂) + (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂)) + ; inputs = Graph.inputs g₁ ↑ˡⁱ Graph.size g₂ + ; outputs = Graph.size g₁ ↑ʳⁱ Graph.inputs g₂ } _[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt @@ -104,4 +110,4 @@ buildCfg : Stmt → Graph buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ []) buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂ buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton [] -buildCfg (while _ repeat s) = loop (buildCfg s ↦ singleton []) +buildCfg (while _ repeat s) = (loop (singleton [] ↦ buildCfg s)) skipto (singleton [])