~vigoux/busybeaver-devel

This thread contains a patchset. You're looking at the original emails, but you may wish to use the patch review UI. Review patch
1

[PATCH busybeaver] feat: add space time diagram command

Details
Message ID
<20240913081512.17648-1-me@vigoux.eu>
DKIM signature
pass
Download raw message
Patch: +240 -1
Use SVG to generate the diagram.

The new subcommand is:
```
explore <machine> <length> <outfile>
```

We could add another feature to "truncate" the diagram up to a certain
length.

Signed-off-by: Thomas Vigouroux <me@vigoux.eu>
---
 Busybeaver/SpaceTimeDiagram.lean | 214 +++++++++++++++++++++++++++++++
 Main.lean                        |  27 +++-
 2 files changed, 240 insertions(+), 1 deletion(-)
 create mode 100644 Busybeaver/SpaceTimeDiagram.lean

diff --git a/Busybeaver/SpaceTimeDiagram.lean b/Busybeaver/SpaceTimeDiagram.lean
new file mode 100644
index 000000000000..d1876bd994b7
--- /dev/null
+++ b/Busybeaver/SpaceTimeDiagram.lean
@@ -0,0 +1,214 @@
import Busybeaver.Basic
import Lean.Data.AssocList
import Busybeaver.Parse

/-!
Generates a time diagram for a TM as an SVG.
-/

namespace SVG

inductive Size where
| pixels : ℤ → Size

instance: OfNat Size n where
  ofNat := .pixels n

instance: Coe ℤ Size where
  coe := .pixels

instance: Coe ℕ Size where
  coe n := .pixels ↑n

instance: ToString Size where
  toString := λ
  | .pixels n => toString n

inductive Kind where
| rect (width height: Size) (x y: Size)

instance: ToString Kind where
  toString := λ
  | .rect width height x y => s!"rect width=\"{width}\" height=\"{height}\" x=\"{x}\" y=\"{y}\""

inductive Color where
| rgb : UInt8 → UInt8 → UInt8 → Color
| hsl : Fin 361 → Fin 101 → Fin 101 → Color

instance: ToString Color where
  toString := λ
  | .rgb r g b => s!"rgb({r} {g} {b})"
  | .hsl h s l => s!"hsl({h}deg {s}% {l}%)"

structure Elem where
  kind : Kind
  fill? : Option Color
  modifiers : List (String × String)

instance: ToString Elem where
  toString e :=
  "<" ++ toString e.kind ++
    (if let .some c := e.fill? then
      " fill=\""  ++ toString c ++ "\""
    else
      "")
  ++ e.modifiers.foldl (λ acc ⟨k, v⟩ ↦ s!"{acc} {k}=\"{v}\"") "" ++ "/>"

structure Doc where
  width : Size
  height : Size
  elems: List Elem

instance: ToString Doc where
  toString doc :=
    s!"<svg width=\"{doc.width}\" height=\"{doc.height}\" xmlns=\"http://www.w3.org/2000/svg\">{String.join (doc.elems.map toString)}</svg>"

def Doc.writeTo (doc: Doc) (stream: IO.FS.Stream) := stream.putStr (toString doc)


declare_syntax_cat svg
declare_syntax_cat svg_elem
declare_syntax_cat svg_color
declare_syntax_cat svg_attrib

syntax str : svg_attrib
syntax num : svg_attrib
syntax "{{" term "}}" : svg_attrib

syntax "rgb(" term "," term "," term ")" : svg_color
syntax "hsl(" term "," term "," term ")" : svg_color
syntax "{{" term "}}" : svg_color

syntax "<svg width=" svg_attrib " height=" svg_attrib ">" svg_elem* "</svg>" : term
syntax "<rect width=" svg_attrib " height=" svg_attrib " x=" svg_attrib " y=" svg_attrib (" fill=" svg_color)? "/>" : svg_elem

syntax "se[[" svg_elem "]]" : term
syntax "sa[[" svg_attrib "]]" : term
syntax "sc[[" svg_color "]]" : term

macro_rules
| `(term| <svg width=$w height=$h>$[$el:svg_elem]*</svg>) => `(term| Doc.mk sa[[$w]] sa[[$h]] [$[ se[[$el]] ],*])

| `(term| se[[<rect width=$w height=$h x=$x y=$y/>]]) =>
    `(term| Elem.mk (Kind.rect sa[[$w]] sa[[$h]] sa[[$x]] sa[[$y]]) .none [])
| `(term| se[[<rect width=$w height=$h x=$x y=$y fill=$c/>]]) =>
    `(term| Elem.mk (Kind.rect sa[[$w]] sa[[$h]] sa[[$x]] sa[[$y]]) (.some sc[[$c]]) [])

| `(term| sc[[rgb($r,$g,$b)]]) => `(term| Color.rgb $r $g $b)
| `(term| sc[[hsl($h,$s,$l)]]) => `(term| Color.hsl $h $s $l)
| `(term| sc[[{{$v}}]]) => pure v

| `(term| sa[[$v:num]]) => `(term| $v)
| `(term| sa[[$v:str]]) => `(term| $v)
| `(term| sa[[{{$v}}]]) => pure v
end SVG

namespace TM.SpaceTime

private def sColor (sym: Symbol s): SVG.Color :=
  let val: ℕ := (sym * 255) / s
  let val: UInt8 := UInt8.ofNat val
  SVG.Color.rgb val val val

private def lColor (label: Label l): SVG.Color :=
  let val: ℕ := (label * 300) / l
  let val: Fin 361 := val
  SVG.Color.hsl val 82 43

def size := 10

private def symToRec (sym: Symbol s) (offset: ℤ) (depth: ℕ): SVG.Elem :=
  se[[
    <rect width={{size}} height={{size}} x={{↑(offset * size)}} y={{↑(depth * size)}} fill={{sColor sym}}/>
  ]]

abbrev Line (l s) := Config l s × Turing.Dir

def getLines (depth: ℕ) (cfg: Config l s) (M: Machine l s): List <| Line l s := match depth with
| 0 => []
| n + 1 => match hM: M cfg.state cfg.tape.head with
  | .halt => []
  | .next _ dir _ =>
    let ncfg : Config l s := M.step cfg |>.get (by simp [Option.isSome, Machine.step, hM])
    (cfg, dir) :: getLines n ncfg M

def getBounds (left cur right: ℤ): List (Line l s) → ℤ × ℤ
| [] => (left, right)
| (_, dir) :: rest => match dir with
  | .left => getBounds (min (cur - 1) left) (cur - 1) right rest
  | .right => getBounds left (cur + 1) (max (cur + 1) right) rest

lemma getBounds.leftNeg {L: List <| Line l s}: (getBounds le cu ri L).1 ≤ le :=
by induction le, cu, ri, L using getBounds.induct with simp [getBounds]
| case2 left cur right _ rest IH => {
  simp at IH
  exact IH.2
}
| case3 left cur right _ rest IH => {
  simp at IH
  exact IH
}

lemma getBounds.rightPos {L: List <| Line l s}: ri ≤ (getBounds le cu ri L).2 :=
by induction le, cu, ri, L using getBounds.induct with simp [getBounds]
| case2 left cur right _ rest IH => {
  simp at IH
  exact IH
}
| case3 left cur right _ rest IH => {
  simp at IH
  exact IH.2
}

/--
Turns the given ListBlank into a list of length target
-/
unsafe def unquotAndPad (target: ℕ) (hT: Turing.ListBlank (Symbol s)): List (Symbol s) :=
  let unq := Quot.unquot hT
  unq ++ List.replicate (target - unq.length) default

unsafe def configToRects (offset: ℤ) (leftmax rightmax: ℕ) (depth: ℕ) (cfg: Config l s): List SVG.Elem :=

  /-
  Tricky: depdending on `offset` we need to padd correctly on left and right.

   o
  XXX|XXX -> lp = l + o, lr = r - o
  l     r

       o
  XXX|XXX -> lp = l + o, lr = r - o
  l     r
  -/
  let leftpadded : List (Symbol s) := unquotAndPad (leftmax + offset).toNat cfg.tape.left
  let rightpadded := unquotAndPad (rightmax - offset).toNat cfg.tape.right

  let left: List SVG.Elem := leftpadded.reverse |>.enum |>.map
    λ ⟨i, sym⟩ ↦ symToRec sym i depth

  let right := rightpadded |>.enum |>.map
    λ ⟨i, sym⟩ ↦ symToRec sym (leftpadded.length + i + 1) depth

  symToRec cfg.tape.head leftpadded.length depth ::
  se[[
    <rect width={{↑(size * 3 / 5)}} height={{↑(size * 3 / 5)}}
      x={{↑(leftpadded.length * size + size / 5)}} y={{↑(depth * size + size / 5)}}
      fill={{lColor cfg.state}}/>
  ]] :: left ++ right

private unsafe def toArray (leftmax rightmax: ℕ) (offset: ℤ): List (ℕ × Line l s) → List SVG.Elem
| [] => []
| (depth, cfg, dir) :: rest =>
    let noff := offset + match dir with
      | .left => -1
      | .right => 1
  configToRects offset leftmax rightmax depth cfg ++ toArray leftmax rightmax noff rest

unsafe def generate (depth: ℕ) (M: Machine l s): SVG.Doc :=
  let lines := getLines depth default M
  let (leftmax, rightmax) := getBounds 0 0 0 lines
  {
    width := ↑(size * (leftmax.natAbs + rightmax.natAbs + 1)),
    height := ↑(size * lines.length),
    elems := toArray leftmax.natAbs rightmax.natAbs 0 lines.enum
  }
diff --git a/Main.lean b/Main.lean
index 6b51f4fbdd9e..81f929ff24da 100644
--- a/Main.lean
+++ b/Main.lean
@@ -7,6 +7,7 @@ import Busybeaver.Deciders.NoHaltState
import Busybeaver.Deciders.TranslatedCyclers
import Busybeaver.Enumerate.Alg
import Busybeaver.Parse
import Busybeaver.SpaceTimeDiagram

import Lean.Data.Json

@@ -117,6 +118,29 @@ unsafe def checkCmd := `[Cli|
    machine: String; "The machine code"
]

unsafe def runExploreCmd (p: Parsed): IO UInt32 := do
  let ⟨l, s, M⟩ := p.positionalArg! "machine" |>.as! MParseRes
  let depth := p.positionalArg! "depth" |>.as! ℕ
  let output := p.positionalArg! "output" |>.as! String

  IO.println s!"Parsed machine with {l + 1} labels and {s + 1} symbols: {repr M}"

  let doc := TM.SpaceTime.generate depth M

  IO.FS.writeFile output (toString doc)

  return 0

unsafe def exploreCmd := `[Cli|
  explore VIA runExploreCmd;
  "Creates a space time diagram of the machine"

  ARGS:
    machine: String; "The machine code"
    depth: ℕ; "Depth to explore"
    output: String; "Path to write the output"
]

unsafe def computeCmd (p: Parsed): IO UInt32 := do
  let start ← IO.monoMsNow
  let l := (p.positionalArg! "nlabs" |>.as! ℕ) - 1
@@ -164,7 +188,8 @@ unsafe def mainCmd := `[Cli|
    nsyms: ℕ; "Number of symbols for the machines"

  SUBCOMMANDS:
    checkCmd
    checkCmd;
    exploreCmd
]

unsafe def main (args: List String): IO UInt32 := do
-- 
2.43.0

[busybeaver/patches/.build.yml] build success

builds.sr.ht <builds@sr.ht>
Details
Message ID
<D450FDBTTTI3.YEWGVNNV4MMB@fra01>
In-Reply-To
<20240913081512.17648-1-me@vigoux.eu> (view parent)
DKIM signature
missing
Download raw message
busybeaver/patches/.build.yml: SUCCESS in 7m51s

[feat: add space time diagram command][0] from [Thomas Vigouroux][1]

[0]: https://lists.sr.ht/~vigoux/busybeaver-devel/patches/55021
[1]: me@vigoux.eu

✓ #1327065 SUCCESS busybeaver/patches/.build.yml https://builds.sr.ht/~vigoux/job/1327065
Reply to thread Export thread (mbox)