issues codegening to do notation

Stream: general

[Frederick Pu]

im trying to generate a TSyntax doSeqItem however im getting the following error:

import Lean

open Lean

def mwe (x : TSyntax `term) : MetaM (TSyntax `Lean.Parser.Term.doSeqItem) := do
  `(Lean.Parser.Term.doSeqItem| let mut x ← $x)
/-
Application type mismatch: The argument
  x
has type
  TSyntax `term
but is expected to have type
  TSyntax `doElem
in the application
  x.raw
-/

there is

@[builtin_doElem_parser] def doExpr := leading_parser notFollowedByRedefinedTermToken >> termParser >> notFollowedBy (symbol ":=" <|> leftArrow) "unexpected token after 'expr' in 'do' block"

so i dont understand what the issue is

[Floris van Doorn]

You have to give Lean a hint that it should parse $x as a term:

import Lean

open Lean

def mwe (x : TSyntax `term) : MetaM (TSyntax `Lean.Parser.Term.doSeqItem) := do
  `(Lean.Parser.Term.doSeqItem| let mut x ← $x:term)

[Frederick Pu]

thx!

[Frederick Pu]

i thought cause it was TSyntax term that that would be obvious lol

[Floris van Doorn]

I'm not sure whether `(...) looks at the expected type.
I've been bitten by the same issue before!

[Frederick Pu]

also do you see any reason why this code gen pretty prints to a metavariable instead of a do block?

import Lean
import Init
import Std.Data.HashMap.Basic
import Pullback.CImp.Syntax

open Lean
open Std

namespace CImp

abbrev ImpM := EStateM String (HashMap String Value)

def Expr.toTerm: Expr → MetaM (TSyntax `term)
  | Expr.const v => do return (quote v.toNat)
  | Expr.var x => do
    let mut q := 0
    `($(mkIdent x):ident)
  | Expr.add e₁ e₂ => do
    let v₁ ← Expr.toTerm e₁
    let v₂ ← Expr.toTerm e₂
    `($v₁ + $v₂)
  | Expr.lt e₁ e₂ => do
    let v₁ ← Expr.toTerm e₁
    let v₂ ← Expr.toTerm e₂
    `(if $v₁ < $v₂ then 1 else 0)
  | _ => `(0)
  -- | Expr.deref e => do
  --   let e' ← Expr.toTerm e
  --   -- note: the below is a valid term since it only requires the Bind typeclass instance and doesnt need do notation to work
  --   `(← Memory.read $e')

#check HashSet

def Stmt.toDoSeqItem : Stmt → StateT (HashSet Name) MetaM (TSyntaxArray `Lean.Parser.Term.doSeqItem)
  | .assign n e => do
    let xId := mkIdent n
    let eSyn ← Expr.toTerm e
    if !((← get).contains n) then
      modify (fun x => x.insert n)
      pure #[← `(Lean.Parser.Term.doSeqItem| let mut $xId ← $eSyn:term)]
    else
      pure #[← `(Lean.Parser.Term.doSeqItem| $xId:ident ← $eSyn:term)]
  -- | .assignPtr ptr e => do
  --   let ptr' ← Expr.toTerm ptr
  --   let e' ← Expr.toTerm e
  --   pure #[← `(Lean.Parser.Term.doSeqItem| Memory.write $ptr' $e')]
  | .seq s₁ s₂ => do
    return (← toDoSeqItem s₁) ++ (← toDoSeqItem s₂)
  | .while c b => do
    let cSyn ← Expr.toTerm c
    let bSyn ← toDoSeqItem b
    let bSyn ← `(Lean.Parser.Term.doSeqItem| while $cSyn do $bSyn*)
    pure #[bSyn]
  | .IfThenElse c t e => do
    let cSyn ← Expr.toTerm c
    let tSyn ← toDoSeqItem t
    let eSyn ← toDoSeqItem e
    pure #[← `(Lean.Parser.Term.doSeqItem| if $cSyn then do $tSyn* else do $eSyn*)]
  | _ => pure #[]

-- Example use
def testStmt : Stmt :=
  stmt{
    while (x < 10) {
      x := x + 1;
    }
  }

#eval (do
  let (x, _) ← (Stmt.toDoSeqItem testStmt).run {};
  let nihee ← Lean.Elab.Term.elabTerm (← `(do $x*)) none
  IO.println "bruhh"
  IO.println (← Lean.Meta.ppExpr nihee).pretty
  : Lean.Elab.Term.TermElabM Unit)

[Frederick Pu]

any tips for bugging something like this?

[Frederick Pu]

hmm it seems to be from trying to elaboratoe the expr for x + 1 in a context where is x is not yet defined:

#eval (do
  let x ← Expr.toTerm (expr{x + 0})
  let nihe ← Lean.Elab.Term.elabTerm (x) none
  IO.println (← Lean.Meta.ppExpr nihe).pretty
: Lean.Elab.Term.TermElabM Unit)
-- Unknown identifier `x`

[Frederick Pu]

i think elabAndSynthesize is prob a better choice too:

#eval (do
  let (x, _) ← (Stmt.toDoSeqItem testStmt).run {};
  IO.println (← `(do $x*)).raw
  let nihee ← Lean.Elab.Term.elabTermAndSynthesize (← `(do $x*)) none
  IO.println "bruhh"
  IO.println (← Lean.Meta.ppExpr nihee).pretty
  : Lean.Elab.Term.TermElabM Unit)

[Frederick Pu]

im guessing i need to give it like Q(Id Unit) for the expected type or smth

[Robin Arnez]

You can also use Lean.logInfo nihee instead of the IO.println stuff you've done here. That alsso gives you hover information on the expression

[Frederick Pu]

finally works now lol:

(Term.do
 "do"
 (Term.doSeqIndent
  [(Term.doSeqItem (Term.doLetArrow "let" ["mut"] (Term.doIdDecl `x [] "←" (Term.doExpr (num "1")))) [])
   (Term.doSeqItem
    (Lean.doElemWhile_Do_
     "while"
     («term_<_» `x "<" (num "0"))
     "do"
     (Term.doSeqIndent
      [(Term.doSeqItem
        (Term.doReassignArrow (Term.doIdDecl `x [] "←" (Term.doExpr («term_+_» `x "+" (num "1")))))
        [])]))
    [])]))
bruhh
do
  let x ← 1
  let r ←
    forIn Loop.mk x fun x r =>
        let x := r;
        if x < 0 then do
          let r ← x + 1
          let x : Nat := r
          pure PUnit.unit
          pure (ForInStep.yield x)
        else pure (ForInStep.done x)
  let x : Nat := r
  pure PUnit.unit

[Frederick Pu]

this case for exprToTerm was returning a Nat before which was bad for some reason

| Expr.lt e₁ e₂ => do
    let v₁ ← Expr.toTerm e₁
    let v₂ ← Expr.toTerm e₂
    `($v₁ < $v₂)