From d0a578c3dbcb10de471671cfaa8eb3499826d3ff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 18 Jan 2017 18:12:08 -0800
Subject: [PATCH] feat(library/init/meta/environment): add is_projection

---
 library/init/meta/environment.lean | 14 ++++++++++++++
 src/library/vm/vm_environment.cpp  | 20 +++++++++++++++++++-
 2 files changed, 33 insertions(+), 1 deletion(-)

diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean
index 24a608d371..58e1474800 100644
--- a/library/init/meta/environment.lean
+++ b/library/init/meta/environment.lean
@@ -9,6 +9,19 @@ import init.meta.declaration init.meta.exceptional
 meta constant environment : Type
 
 namespace environment
+/--
+Information for a projection declaration
+- `cname`    is the name of the constructor associated with the projection.
+- `nparams`  is the number of constructor parameters
+- `idx`      is the parameter being projected by this projection
+- `is_class` is tt iff this is a class projection.
+-/
+structure projection_info :=
+(cname : name)
+(nparams : nat)
+(idx : nat)
+(is_class : bool)
+
 /- Create a standard environment using the given trust level -/
 meta constant mk_std          : nat → environment
 /- Return the trust level of the given environment -/
@@ -48,6 +61,7 @@ meta constant inductive_num_indices : environment → name → nat
 meta constant inductive_dep_elim : environment → name → bool
 /- Return tt iff the given name is a generalized inductive datatype -/
 meta constant is_ginductive : environment → name → bool
+meta constant is_projection : environment → name → option projection_info
 /- Fold over declarations in the environment -/
 meta constant fold {α :Type} : environment → α → (declaration → α → α) → α
 /- (relation_info env n) returns some value if n is marked as a relation in the given environment.
diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp
index 7362472b48..6efe049960 100644
--- a/src/library/vm/vm_environment.cpp
+++ b/src/library/vm/vm_environment.cpp
@@ -7,11 +7,12 @@ Author: Leonardo de Moura
 #include <string>
 #include "kernel/type_checker.h"
 #include "kernel/inductive/inductive.h"
-#include "library/inductive_compiler/ginductive.h"
 #include "library/standard_kernel.h"
 #include "library/module.h"
+#include "library/projection.h"
 #include "library/util.h"
 #include "library/relation_manager.h"
+#include "library/inductive_compiler/ginductive.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_option.h"
@@ -208,6 +209,22 @@ vm_obj environment_decl_pos_info(vm_obj const & env, vm_obj const & n) {
     }
 }
 
+/*
+structure projection_info :=
+(cname : name)
+(nparams : nat)
+(idx : nat)
+(is_class : bool)
+*/
+vm_obj environment_is_projection(vm_obj const & env, vm_obj const & n) {
+    if (auto info = get_projection_info(to_env(env), to_name(n))) {
+        return mk_vm_some(mk_vm_constructor(0, to_obj(info->m_constructor), mk_vm_nat(info->m_nparams),
+                                            mk_vm_nat(info->m_i), mk_vm_bool(info->m_inst_implicit)));
+    } else {
+        return mk_vm_none();
+    }
+}
+
 void initialize_vm_environment() {
     DECLARE_VM_BUILTIN(name({"environment", "mk_std"}),                environment_mk_std);
     DECLARE_VM_BUILTIN(name({"environment", "trust_lvl"}),             environment_trust_lvl);
@@ -226,6 +243,7 @@ void initialize_vm_environment() {
     DECLARE_VM_BUILTIN(name({"environment", "inductive_num_indices"}), environment_inductive_num_indices);
     DECLARE_VM_BUILTIN(name({"environment", "inductive_dep_elim"}),    environment_inductive_dep_elim);
     DECLARE_VM_BUILTIN(name({"environment", "is_ginductive"}),         environment_is_ginductive);
+    DECLARE_VM_BUILTIN(name({"environment", "is_projection"}),         environment_is_projection);
     DECLARE_VM_BUILTIN(name({"environment", "relation_info"}),         environment_relation_info);
     DECLARE_VM_BUILTIN(name({"environment", "refl_for"}),              environment_refl_for);
     DECLARE_VM_BUILTIN(name({"environment", "symm_for"}),              environment_symm_for);