Help: Notation for Turing Machines from transition table

Stream: new members

[Thomas Vigouroux]

Hi,
I would like to implement an notation for Turing machine that mimics this notation: https://wiki.bbchallenge.org/wiki/Turing_machine#Standard_text_format

I don't know if this is possible or if anyone had experience implementing similar notations. I am fine learning how to handle elaboration and stuff like that by the way, but would greatly appreciate any guidance.

My formalisation of Turing machines is there by the way: https://git.sr.ht/~vigoux/busybeaver/tree/master/item/Busybeaver/Basic.lean#L69

[Martin Dvořák]

Are you interested in parsing
image.png
to a docs#TuringMachine term?

Or do you also want to use the notation
image.png
for describing the computation?

[Thomas Vigouroux]

I'd say both

[Martin Dvořák]

Regarding the latter notation, would writing something like ⟨[0, 0, 0], A, 0, [0, 0, 0]⟩ be good enough?
Or do you actually want to require single-character identifiers, no delimiters, and so on?

[Thomas Vigouroux]

For this I already have a notation actually, which resembles this

[Thomas Vigouroux]

And I think it is fine writing them like this

[Thomas Vigouroux]

Or at least, we can postpone such considerations to later

[Thomas Vigouroux]

Thanks for your time by the way !

[Thomas Vigouroux]

I am trying to have this working but I am stuck, here is my current implementation:

/-
Parsing machines in standard format for convenience.
-/
import Busybeaver.Basic

open Lean Elab

declare_syntax_cat dir

syntax "L": dir
syntax "R": dir

def elabDir : Syntax → MetaM Expr
  -- `mkAppM` creates an `Expr.app`, given the function `Name` and the args
  -- `mkNatLit` creates an `Expr` from a `Nat`
  | `(dir | L) => Meta.mkAppM ``Turing.Dir.left #[]
  | `(dir | R) => Meta.mkAppM ``Turing.Dir.right #[]
  | _ => throwUnsupportedSyntax

declare_syntax_cat symbol
syntax num : symbol

declare_syntax_cat label
syntax "A" : label
syntax "B" : label
syntax "C" : label
syntax "D" : label
syntax "E" : label
syntax "F" : label

declare_syntax_cat stmt
syntax symbol dir label: stmt
syntax "...": stmt

def elabStmt : Syntax → MetaM Expr
  -- `mkAppM` creates an `Expr.app`, given the function `Name` and the args
  -- `mkNatLit` creates an `Expr` from a `Nat`
  | `(stmt | ...) => Meta.mkAppM ``TM.Stmt.halt #[]
  | `(stmt | $S:symbol $D:dir $L:label ) => do dbg_trace "stmt"; throwUnsupportedSyntax
  | _ => throwUnsupportedSyntax

elab "test_elab " l:stmt : term => elabStmt l

#reduce test_elab ...