Embedded DSL with access to (mutable) variables

Stream: new members

[dxo]

I'm trying to write a little embedded DSL that expands into monadic Lean4 code to help me play around with designs for a new language. I would like the code in the DSL blocks to be able to read from (and modify) mutable variables declared in the outer scope. I think I'm pretty close to a working solution, but I'm getting some error messages that I don't understand. What am I doing wrong here?

import Lean
open Lean

-- Syntax --

declare_syntax_cat statement
declare_syntax_cat literal

syntax num : literal
syntax ident ":=" literal : statement
syntax "assembly {" statement "}" : term

-- Semantics --

-- This seems extremely suspect...
instance : Coe Syntax (TSyntax `term) where
  coe s := ⟨s⟩

macro_rules
  | `(literal | $n:num) => `(pure $n)
  -- Is the quoting here correct?
  | `(statement | $i:ident := $l:literal) => `($i "←" $l)
  | `(assembly { $s:statement}) => `($s)

-- Test Case --

#check do
  let mut x : Nat := 0
  /-
  the `assembly` block below should expand into the following:
    x ← pure 10

  currently gives the following error:
    function expected at
      x
    term has type
      Nat
  -/
  assembly { x := 10 }
  return x

[dxo]

I believe I've made a little bit of progress, or at least have managed to uncover an even more confusing error... Does anyone have any insight?

import Lean
open Lean

-- Syntax --

declare_syntax_cat statement
declare_syntax_cat literal

syntax num : literal
syntax ident ":=" literal : statement
syntax "assembly {" statement "}" : doElem

-- Semantics --

macro_rules
  | `(literal | $n:num) => `(pure $n)
  | `(statement | $i:ident := $l:literal) => `(doElem | `($i) ← `(literal | $l))
  | `(doElem | assembly { $s:statement }) => `(statement | $s)

-- Test Case --

#check do
  let mut x : Nat := 0
  /-
  the `assembly` block below should expand into the following:
    x ← pure 10

  Currently gives the following error:

  ▶ 43:14-44:21: error:
  non-exhaustive 'match' (syntax)

  ▶ 43:14-44:21: error:
  application type mismatch
    Syntax.matchesIdent __discr✝
  argument
    __discr✝
  has type
    ?m.7189 __discr✝¹ (TSyntax `term) : Type
  but is expected to have type
    Syntax : Type
  -/
  assembly { x := 10 }
  return x