eval_expr and universes

Stream: metaprogramming / tactics

[Eric Wieser]

Is it possible to use eval_expr in a universe-polymorphic way? The non-working pseudocode is:

/-- Evaluate `ex` and reflect back its value -/
meta def reflect_eval (ex : expr) : tactic expr :=
do
  et ← infer_type ex,
  expr.sort l ← infer_type et,
  -- `Type` isn't universe polymorphic; how to use `l`?
  -- note that we have to call `interaction_monad_bind` manually as `>>=` doesn't allow universe polymorphism
  interaction_monad_bind (eval_expr Type et) $ λ t, do
    let inst1 : reflected Type t := sorry,
    x ← @eval_expr t inst1 ex,
    let inst2 : reflected t x := sorry,
    pure (@reflect _ x inst2)

With the intent that reflect_eval `(1 + 1) = `(2) (but in a way that knows about any computable definition)

[Mario Carneiro]

where is the has_reflect instance supposed to come from?

[Eric Wieser]

I was hoping that I could ask instance search to look for one

[Eric Wieser]

(edited above to be non-pseudocode, but have sorrys instead)

[Eric Wieser]

Obviously the instance wouldn't be available in all cases, but it feels like it ought to be possible if et is `(nat)

[Mario Carneiro]

Ha!

open tactic

meta def eval' (α : Sort*) [has_reflect α] [reflected _ α] (e : expr) : tactic expr :=
  do a ← eval_expr α e, pure (reflect a)

/-- Evaluate `ex` and reflect back its value -/
meta def reflect_eval (ex : expr) : tactic expr :=
do
  t ← infer_type ex,
  inst ← mk_app ``has_reflect [t] >>= mk_instance,
  f ← eval_expr (expr → expr → tactic expr) ((expr.const ``eval' []).mk_app [t, inst]),
  f t ex

#eval reflect_eval `(1 + 1) >>= tactic.trace