From fa58d7c71e21a6d81e239f55dfe3a3605de54113 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Sat, 31 Oct 2015 14:41:40 -0700
Subject: [PATCH] feat(frontends/lean): basic support for partial explicit

---
 src/frontends/lean/builtin_exprs.cpp | 10 +++++++++-
 src/frontends/lean/pp.cpp            |  1 +
 src/library/explicit.cpp             |  1 +
 3 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 9096bf81b..26ec473d4 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -691,7 +691,15 @@ static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info con
 }
 
 static expr parse_partial_explicit_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    throw parser_error("partial explicit expressions (@) not supported yet", p.pos());
+    expr e = p.parse_expr(get_Max_prec());
+    if (is_choice(e)) {
+        buffer<expr> new_choices;
+        for (unsigned i = 0; i < get_num_choices(e); i++)
+            new_choices.push_back(p.save_pos(mk_partial_explicit(get_choice(e, i)), pos));
+        return p.save_pos(mk_choice(new_choices.size(), new_choices.data()), pos);
+    } else {
+        return p.save_pos(mk_partial_explicit(e), pos);
+    }    
 }
 
 static expr parse_consume_args_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 69dfff896..5fb3b273a 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -153,6 +153,7 @@ void finalize_pp() {
     delete g_from_fmt;
     delete g_visible_fmt;
     delete g_show_fmt;
+    delete g_partial_explicit_fmt;    
     delete g_explicit_fmt;
     delete g_tmp_prefix;
 }
diff --git a/src/library/explicit.cpp b/src/library/explicit.cpp
index 31837b8f6..defd15ad8 100644
--- a/src/library/explicit.cpp
+++ b/src/library/explicit.cpp
@@ -46,6 +46,7 @@ void initialize_explicit() {
     g_consume_args_name = new name("!");
 
     register_annotation(*g_explicit_name);
+    register_annotation(*g_partial_explicit_name);    
     register_annotation(*g_as_atomic_name);
     register_annotation(*g_as_is_name);
     register_annotation(*g_consume_args_name);