module PrettyPrinter.GraphViz.Simulation where

open import Data.Nat
open import Data.Bool renaming (Bool to 𝔹; _β‰Ÿ_ to _β‰Ÿα΅‡_)
open import Data.List
open import Data.Product using (_Γ—_; βˆƒ-syntax; proj₁; projβ‚‚) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary.Decidable using (isYes)
open import Agda.Builtin.String
open import Text.Printf

open import Common.Utils using (magic-num)
open import Common.Types
open import CC.MultiStep
open import PrettyPrinter.GraphViz.MultiStep renaming (pprint to pprint-β† )


print-sim-edges : List (β„• Γ— β„•) β†’ (last-n : β„•) β†’ String
print-sim-edges [] last = ""
print-sim-edges (⟨ n , m ⟩ ∷ rest) last =
  let l_node = printf "left%u"  n
      r_node = printf "right%u" m in
  primStringAppend
  (if isYes (n β‰Ÿ last)
    then (printf "  %s -> %s;\n" l_node r_node)
    else (printf "  %s -> %s; { rank=\"same\"; %s; %s; }\n" l_node r_node l_node r_node))
  (print-sim-edges rest n)

print-sim-diagram : βˆ€ {M₁ M₁′ Mβ‚‚ Mβ‚‚β€² μ₁ μ₁′ ΞΌβ‚‚ ΞΌβ‚‚β€²}
  β†’ M₁  ∣ μ₁  ∣ low β€”β†  Mβ‚‚  ∣ ΞΌβ‚‚   {- reduction seq on the left   -}
  β†’ M₁′ ∣ μ₁′ ∣ low β€”β†  Mβ‚‚β€² ∣ ΞΌβ‚‚β€²  {- reduction seq on the right  -}
  β†’ List (β„• Γ— β„•)                    {- edges between two subgraphs -}
    ---------------
  β†’ String
print-sim-diagram M₁↠Mβ‚‚ M₁′↠Mβ‚‚β€² s =
  printf
  -- NOTE: use the `splines` option to draw straight lines
  -- - see https://graphviz.org/docs/attrs/splines/
  "digraph {
  splines=line;
  node[shape=plaintext];
  subgraph left {
    rankdir=\"TB\";
%s
  }
  subgraph right {
    rankdir=\"TB\";
%s
  }
  edge[style=dotted, constraint=false, arrowhead=none, minlen=3];
%s
}\n" (pprint-β†  "left" M₁↠Mβ‚‚) (pprint-β†  "right" M₁′↠Mβ‚‚β€²) (print-sim-edges s magic-num)