From 04f9eb0b4f72c37cd3fbb2c94580a6146fb228e5 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 1 Jun 2017 10:17:51 +0200 Subject: [PATCH] refactor(library/init/meta/expr): pure Lean implementation of reflected --- library/init/meta/expr.lean | 63 +++++++++---------- src/library/vm/vm_expr.cpp | 10 --- tests/lean/reflect_type_defeq.lean | 2 + .../lean/reflect_type_defeq.lean.expected.out | 6 ++ 4 files changed, 38 insertions(+), 43 deletions(-) create mode 100644 tests/lean/reflect_type_defeq.lean create mode 100644 tests/lean/reflect_type_defeq.lean.expected.out diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 8c6b369830..b0543505e9 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import init.meta.level init.category.monad +universes u v structure pos := (line : nat) @@ -47,39 +48,6 @@ meta inductive expr (elaborated : bool := tt) | macro : macro_def → list expr → expr variable {elab : bool} -/-- Internal representation for reflected_core -/ -meta constant {u} reflected_core : Sort u -meta constant reflected_core.to_expr : reflected_core → expr -meta constant reflected_core.subst : reflected_core → reflected_core → reflected_core -/-- (reflected a) is a special opaque container for a closed `expr` representing `a`. - It can only be obtained via type class inference, which will use the representation - of `a` in the calling context. Local constants in the representation are replaced - by nested inference of `reflected` instances. - - The quotation expression `(a) (outside of patterns) is equivalent to `reflect a` - and thus can be used as an explicit way of inferring an instance of `reflected a`. -/ -meta def {u} reflected {α : Sort u} : α → Sort (max 1 u) := -λ _, reflected_core - -@[inline] meta def {u} reflected.to_expr {α : Sort u} {a : α} : reflected a → expr := -reflected_core.to_expr - -@[inline] meta def {v u} reflected.subst {α : Sort u} {β : α → Sort v} {f : Π a : α, β a} {a : α} : - reflected f → reflected a → reflected (f a) := -reflected_core.subst - -meta constant expr.reflect (e : expr elab) : reflected e -meta constant string.reflect (s : string) : reflected s - -attribute [class] reflected -attribute [instance] expr.reflect string.reflect - -universes u - -@[inline] meta instance {α : Sort u} (a : α) : has_coe (reflected a) expr := -⟨reflected.to_expr⟩ - -meta def reflect {α : Sort u} (a : α) [h : reflected a] : reflected a := h meta instance : inhabited expr := ⟨expr.sort level.zero⟩ @@ -160,6 +128,35 @@ meta constant expr.collect_univ_params : expr → list name /-- `occurs e t` returns `tt` iff `e` occurs in `t` -/ meta constant expr.occurs : expr → expr → bool +/-- (reflected a) is a special opaque container for a closed `expr` representing `a`. + It can only be obtained via type class inference, which will use the representation + of `a` in the calling context. Local constants in the representation are replaced + by nested inference of `reflected` instances. + + The quotation expression `(a) (outside of patterns) is equivalent to `reflect a` + and thus can be used as an explicit way of inferring an instance of `reflected a`. -/ +meta def reflected {α : Sort u} : α → Type := +λ _, expr + +@[inline] meta def reflected.to_expr {α : Sort u} {a : α} : reflected a → expr := +id + +@[inline] meta def reflected.subst {α : Sort v} {β : α → Sort u} {f : Π a : α, β a} {a : α} : + reflected f → reflected a → reflected (f a) := +expr.subst + +meta constant expr.reflect (e : expr elab) : reflected e +meta constant string.reflect (s : string) : reflected s + +attribute [class] reflected +attribute [instance] expr.reflect string.reflect +attribute [irreducible] reflected reflected.subst reflected.to_expr + +@[inline] meta instance {α : Sort u} (a : α) : has_coe (reflected a) expr := +⟨reflected.to_expr⟩ + +meta def reflect {α : Sort u} (a : α) [h : reflected a] : reflected a := h + namespace expr open decidable diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index a7a50b2d34..2e79c9c0a8 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -448,14 +448,6 @@ vm_obj expr_is_annotation(vm_obj const &, vm_obj const & _e) { } } -vm_obj reflected_to_expr(vm_obj const & r) { - return r; -} - -vm_obj reflected_subst(vm_obj const & e1, vm_obj const & e2) { - return expr_subst(mk_vm_unit(), e1, e2); -} - vm_obj reflect_expr(vm_obj const & elab, vm_obj const & e) { if (to_bool(elab)) return to_obj(mk_expr_quote(to_expr(e))); @@ -511,8 +503,6 @@ void initialize_vm_expr() { DECLARE_VM_BUILTIN(name({"expr", "collect_univ_params"}), expr_collect_univ_params); DECLARE_VM_CASES_BUILTIN(name({"expr", "cases_on"}), expr_cases_on); - DECLARE_VM_BUILTIN(name({"reflected_core", "to_expr"}), reflected_to_expr); - DECLARE_VM_BUILTIN(name({"reflected_core", "subst"}), reflected_subst); DECLARE_VM_BUILTIN(name("string", "reflect"), reflect_string); DECLARE_VM_BUILTIN(name("expr", "reflect"), reflect_expr); diff --git a/tests/lean/reflect_type_defeq.lean b/tests/lean/reflect_type_defeq.lean new file mode 100644 index 0000000000..d54c97ce1a --- /dev/null +++ b/tests/lean/reflect_type_defeq.lean @@ -0,0 +1,2 @@ +meta def foo (x : reflected (3 : ℕ)) : reflected ([10] : list ℕ) := +x -- ERROR \ No newline at end of file diff --git a/tests/lean/reflect_type_defeq.lean.expected.out b/tests/lean/reflect_type_defeq.lean.expected.out new file mode 100644 index 0000000000..dfe7146985 --- /dev/null +++ b/tests/lean/reflect_type_defeq.lean.expected.out @@ -0,0 +1,6 @@ +reflect_type_defeq.lean:2:0: error: equation type mismatch, expression + x +has type + reflected 3 +but is expected to have type + reflected [10]