How to evaluate a DSL using the elaborator?

Stream: general

[Andrej Bauer]

I would like to define a small domain-specific language (DSL) and use it during elaboration to define complex objects. The catch is that not every expression in this DSL leads to a well-defined object, and the compilation itself is more than just macro expansion.

I can illustrate what I'd like to do with the following small example. Suppose we defined a type of expressions made of numerals, variables and addition:

mport Mathlib.Control.Basic

/-- An inductive type of expressions with variables ranging over type `V`. -/
inductive Expr where
  /-- Numeric constant -/
| num : Nat → Expr
  /-- Variable -/
| var : String → Expr
  /-- Addition -/
| plus : Expr → Expr → Expr

Such an expression is said to be closed if it does not contain any variables. A closed expression may be evaluated to a number. Here is a function which does so, or reports a variable that was encountered:

/-- Evaluate a closed expression and either return
    `inr n` where `n` is its value, or `inl x` is variable
    `x` is encoutnered. -/
def eval_closed : Expr → Sum String Nat
| .num k => return k
| .var x => .inl x
| .plus e₁ e₂ =>
  do
    let n₁ ← eval_closed e₁
    let n₂ ← eval_closed e₂
    return (n₁ + n₂)

#eval eval_closed (.plus (.num 4) (.num 5)) -- .inr 9

#eval eval_closed (.plus (.num 4) (.var "x")) -- .inl "x"

I would like to use the above function, or something like it, to introduce special notation ⟦ e ⟧ where e denotes an expression, such that either ⟦ e ⟧ evaluates/elaborates to a numeral value, or the user sees an error message "cannot compile e as variable x appears in it".

-- imaginary examples
#check ⟦ plus (num 3) (num 5) ⟧ -- this is elaborated to 8
#check ⟦ pus (num 3) (var "x") ⟧ -- this reports an error: "x occurs"

Naively one would expect the above function eval_closed to be useful, but I suspect it's not "meta-level" enough.

From what I understand this is a job for macros and the elaborator. I am ok with introducing additional syntax for expressions, or even a syntax category, so that we can control what may appear within ⟦ - ⟧.

If I am going wrong about it, I'd be glad to hear how to do it right.

[Mario Carneiro]

open Lean hiding Expr
open Qq
elab "⟦" x:term "⟧" : term => do
  let e ← unsafe Elab.Term.evalTerm Expr q(Expr) x
  match eval_closed e with
  | .inr n => return q($n)
  | .inl x => throwError "{x} occurs"

open Expr
#check ⟦ plus (num 3) (num 5) ⟧ -- this is elaborated to 8
#check ⟦ plus (num 3) (var "x") ⟧ -- this reports an error: "x occurs"

[Andrej Bauer]

Thanks!

[Notification Bot]

Andrej Bauer has marked this topic as resolved.

[Notification Bot]

Andrej Bauer has marked this topic as unresolved.

[Andrej Bauer]

Hmm, does Elab.Term.evalTerm think that its first argument must come from Type? Is there an analogous function that allows me to evaluate to a type? The following seems problematic:

elab "⟦" A:term "|" e:term "⟧" : term => do
  let A ← unsafe Lean.Elab.Term.evalTerm Type A --
  ...

I get:

application type mismatch
  @Lean.Elab.Term.evalTerm Type
argument
  Type
has type
  Type 1 : Type 2
but is expected to have type
  Type : Type 1

[Andrej Bauer]

More generally, is there a place where I can read about the interaction between the elaborator and type classes? It looks like I need some type class instances to evalute my expression.

[Kyle Miller]

Instead of evalTerm (which uses the compiler and ir evaluator for its evaluation strategy), you could also use whnf and friends as an evaluation strategy — just thought I'd mention it. It's a bit awkward though, since the expression matching code feels much more ad hoc.

[Andrej Bauer]

Staring at the definition of Elab.Term.evalTerm, it seems odd that it limits the type to the lowest universe. Is this a feature or a bug?

[Andrej Bauer]

Actually, Eval.evalExpr already suffers from this feature. How deep is the rabbit hole, I wonder.

[Kyle Miller]

It's something you can get around. The main issue is that it's monadic, and bind is has a strong universe constraint, so if anything is at Type everything will be. docs#Lean.Environment.evalConst is universe polymorphic

[Andrej Bauer]

evalConst does not seem to be useful for the purposes of the problem at hand. It feels like I am doing something wrong, it can't be that hard to write a small meta-level evaluator (maybe it's just macros) that can fail.

[Kyle Miller]

To use something like evalConst, you add a new constant to the environment first with the value you want to evaluate.

[Kyle Miller]

For example, #eval adds a temporary constant like this

[Henrik Böving]

What exactly is your plan with the Type here? An element of type Type has no meaning in the Lean runtime. Do you want to work with the runtime representation of the type or with the meta one?

[Andrej Bauer]

I think we're solving the wrong problem. If you look at the top of the thread, I'd just like a little DSL that gets expanded at elaboration time, except that (a) it's recursive and (b) it can fail.

[Andrej Bauer]

I think recursiveness is not a problem.

[Andrej Bauer]

I think I should be going in the direction of Mini-project

[Kyle Miller]

I think we're solving the wrong problem.

That may be true, but I'm just responding to your questions about the Type constraints of evalTerm

[Kyle Miller]

Here's a reduction-based strategy @Andrej Bauer. It uses a recognizer for Expr that reduces to constructors. Given the examples it seems each expression will already be in whnf, but why not.

namespace DSL

/-- An inductive type of expressions with variables ranging over type `V`. -/
inductive Expr where
  /-- Numeric constant -/
| num : Nat → Expr
  /-- Variable -/
| var : String → Expr
  /-- Addition -/
| plus : Expr → Expr → Expr

def eval_closed : Expr → Except String Nat
| .num k => return k
| .var x => .error x
| .plus e₁ e₂ =>
  do
    let n₁ ← eval_closed e₁
    let n₂ ← eval_closed e₂
    return (n₁ + n₂)

open Lean.Meta

partial def ofLeanExpr? (e : Lean.Expr) : Lean.MetaM Expr := do
  match ← whnf e with
  | Lean.mkApp (.const ``Expr.num []) n =>
    let .lit (.natVal n) ← whnf n | failure
    return Expr.num n
  | Lean.mkApp (.const ``Expr.var []) (.lit (.strVal s)) =>
    return Expr.var s
  | Lean.mkApp2 (.const ``Expr.plus []) e₁ e₂ =>
    return Expr.plus (← ofLeanExpr? e₁) (← ofLeanExpr? e₂)
  | _ => failure

open Lean.Elab

elab "⟦" x:term "⟧" : term => do
  let e ← Term.elabTermAndSynthesize x (some <| .const ``Expr [])
  let some e' ← Lean.observing? (ofLeanExpr? e) | throwError "expecting a term that is recognizably an `Expr`, not{Lean.indentD e}"
  match eval_closed e' with
  | .ok n => return Lean.toExpr n
  | .error s => throwError m!"{s} occurs"

open Expr
#check ⟦ plus (num 3) (num 5) ⟧ -- 8 : Nat
#check ⟦ plus (num 3) (var "x") ⟧ -- error: x occurs

[Mario Carneiro]

Should ofLeanExpr? be a deriveable typeclass function?

[Kyle Miller]

That seems like it could be fairly useful

[Edward van de Meent]

That would be basically a function that puts terms in whnf and then unquotes?

[Edward van de Meent]

I imagine this becomes a bit hard to do in a universe-polymorphic way?

[Andrej Bauer]

Thanks for these examples, that's great. In my particular case, Expr is parameterized by a type A. Everything is also universe-polymorphic, but that's not a real obstacle, I suppose, as in most examples we'll have A : Type. (Also, eval_closed needs an instance of PCA A.) Let me see if I can adapt your examples to the situation – thanks again.

[Andrej Bauer]

BTW, there's a kludge that I can resort to. The carrier sets I work with are inhabited, so I could just interpret any variable I see with a default value. Kind of what programming languages did in the 1960s and 70s, where variables had default initial values. It was a lot of fun to debug.

[Andrej Bauer]

At the risk of asking too many questions, here's what I think might be the last one. In a macro, when I parse an ident, how do I convert to a string or Name or some such entity?

  declare_syntax_cat combinator

  -- syntax:10 "≪" ident "≫" combinator:10 : combinator
  syntax:90 "var" ident : combinator
  syntax:90 "S" : combinator
  syntax:90 "K" : combinator
  syntax:40 combinator:40 "⬝" combinator:35 : combinator
  syntax "[pca:" combinator "]" : term

  macro_rules
  | `([pca: var $x:ident]) => `(Expr.var x.toString) -- <==== What should stand here for x.toString?
  | `([pca: K]) => `(Expr.K)
  | `([pca: S]) => `(Expr.S)
  | `([pca: $a:combinator ⬝ $b:combinator]) => `(Expr.app [pca: $a] [pca: $b])

[Adam Topaz]

x.getId will get you the name. You can make it a string from there

[Adam Topaz]

docs#Lean.TSyntax.getId

[Andrej Bauer]

The bit that confuses is me how to quote/unqoute this stuff. Here's a MWE:

declare_syntax_cat cow
syntax "moo" ident : cow
syntax "[bovine:" cow "]" : term

macro_rules
| `([bovine: moo $x]) => `($x.getId) -- STRUGGLING HERE

#check [bovine: moo x] -- Should produce x as a name or a string

[Kevin Buzzard]

At the risk of asking too many questions

I don't know if you've noticed how many new posts there are on this Zulip if you ignore it for a 24 hour period, but the long and short of it is that I don't think you should worry about asking lots of questions. I believe that me perpetually asking questions (some of them quite stupid) in 2017/18, and sometimes getting really insightful answers, was what accelerated my learning of the language (and I had essentially no programming experience before that). Remember also that you're not the only person who's learning from these conversations.

[Adam Topaz]

Oh I see. You can surely make an elaborator and use toExpr. I don’t know off the top of my head how to do this in a macro and I’m away from my computer at the moment.

[Shreyas Srinivas]

Andrej Bauer said:

The bit that confuses is me how to quote/unqoute this stuff. Here's a MWE:

declare_syntax_cat cow
syntax "moo" ident : cow
syntax "[bovine:" cow "]" : term

macro_rules
| `([bovine: moo $x]) => `($x.getId) -- STRUGGLING HERE

#check [bovine: moo x] -- Should produce x as a name or a string

In these cases I try Lean.quote. It is another matter that I find the whole quotation and anti quotation syntax in lean horrendously confusing and resort to the kind of trial and error method that I already unlearnt in undergrad as a hack.

[Shreyas Srinivas]

@loogle Lean.quote

[loogle]

:exclamation: unknown identifier 'Lean.quote'
Did you mean "Lean.quote"?

[Shreyas Srinivas]

@loogle Lean.Quote.quote

[loogle]

:search: Lean.Quote.quote

[Mario Carneiro]

like so:

macro_rules
| `([bovine: moo $x]) => `($(Lean.quote x.getId))

[Mario Carneiro]

(the quotation isn't really necessary here but maybe it generalizes better to if you want to do other things)

[Kyle Miller]

Answering the earlier form of the question:

macro_rules
  | `([pca: var $x:ident]) => `(Expr.var $(quote x.getId.toString))

You can also consider letting Expr.var take a Name; having hierarchical names can be convenient, and it gives you access to the hygienic name system.