diff --git a/Language/Graphs.agda b/Language/Graphs.agda index 31f4afc..6504d6d 100644 --- a/Language/Graphs.agda +++ b/Language/Graphs.agda @@ -84,6 +84,18 @@ loop g = record g List.cartesianProduct (Graph.outputs g) (Graph.inputs g) } +optional : Graph → Graph +optional g = record + { size = 2 Nat.+ Graph.size g + ; nodes = [] ∷ [] ∷ Graph.nodes g + ; edges = (2 ↑ʳᵉ Graph.edges g) List.++ + List.map (zero ,_) (2 ↑ʳⁱ Graph.inputs g) List.++ + List.map (_, suc zero) (2 ↑ʳⁱ Graph.outputs g) List.++ + ((zero , suc zero) ∷ []) + ; inputs = zero ∷ [] + ; outputs = (suc zero) ∷ [] + } + infixr 5 _skipto_ _skipto_ : Graph → Graph → Graph _skipto_ g₁ g₂ = record (g₁ ∙ g₂) @@ -110,4 +122,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 (singleton [] ↦ buildCfg s)) skipto (singleton []) +buildCfg (while _ repeat s) = optional (loop (buildCfg s))