quote tactic

Stream: general

[Mario Carneiro]

Here's a demo of a new quote tactic, indended for working with domain-specific languages:

import tactic.interactive

namespace tactic

meta class has_quote (α : Type*) := (f : expr → option α)

meta def quote_with (α) [has_reflect α] [has_quote α] (e : expr) : option expr :=
do a ← has_quote.f α e, pure (reflect a)

namespace interactive
open tactic interactive interactive.types lean.parser

meta def quote (q : parse texpr) : tactic unit :=
do e ← i_to_expr_strict q,
  α ← target,
  f ← i_to_expr_strict ``(quote_with %%α) >>= tactic.eval_expr' (expr → option expr),
  r ← f e | fail "conversion failed",
  tactic.exact r

end interactive
end tactic

[Mario Carneiro]

@[derive has_reflect]
inductive ring_expr : Type
| num : ℕ → ring_expr
| add : ring_expr → ring_expr → ring_expr

meta def to_ring_expr : expr → option ring_expr
| `(%%e₁ + %%e₂) := ring_expr.add <$> to_ring_expr e₁ <*> to_ring_expr e₂
| e := ring_expr.num <$> e.to_nat
meta instance : tactic.has_quote ring_expr := ⟨to_ring_expr⟩

def E : ring_expr := by quote 2 + 2
#print E

-- def E : ring_expr :=
-- ring_expr.add (ring_expr.num 2) (ring_expr.num 2)

[Mario Carneiro]

the idea is that you write a parser function for your target syntax, as a function expr -> option A, and then quote will spit out parsed values of your type

[Patrick Massot]

Do you have a more realistic use case in mind?

[Mario Carneiro]

Jesse and Floris could use this for parsing formulas in first order logic into their embedded language

[Mario Carneiro]

I'm thinking about using it for writing programs and embedding in an AST without too much notational overhead

[Mario Carneiro]

The nice thing is that it's completely non-meta after the parsing stage, just like any other proof producing tactic

[Mario Carneiro]

It's probably not that useful for regular maths, but for anything involving deep embeddings or embedded DSLs this is a very important technique

[Simon Hudon]

That kind of looks like the beginning of a compiler, am I close?

[Mario Carneiro]

it's also useful for custom lean compilers ;)

[Simon Hudon]

Who would ever want that? :P

[Mario Carneiro]

Unfortunately it's still pretty limited since the quoted expression has to be a valid expr. It's possible to relax it to pexprs, but the pattern matching for pexpr is not nearly as nice. I also haven't figured out how to support antiquoting or really anything that's not well typed by lean standards

[Simon Hudon]

What kind of expression would you like Lean to accept?

[Mario Carneiro]

by quote 2 + AQ e is one thing I'm trying for the ring_expr example, where e : ring_expr

[Mario Carneiro]

but there are plenty of things that aren't even syntactically correct lean terms that I would like to support. Probably most of this will need to wait for Sebastian's parser work

[Simon Hudon]

When you parse it, you could temporarily add functions quote and AQ of the right type and then restore the environment

[Simon Hudon]

Yeah, that can't be helped

[Mario Carneiro]

Getting AQ to have the right type is not easy. In this case it should have type ring_expr -> nat but nat isn't mentioned anywhere else

[Mario Carneiro]

Plus in cases like formula quotation we want two kinds of AQ, formula -> Prop and term -> A where A is the fictional domain of the FOL formula