Add parse_let

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

examples/ex4.lean

@@ -0,0 +1,15 @@
+Show (fun x : Bool, (fun y : Bool, x /\ y))
+Show let x := true,
+         y := true
+     in (let z := x /\ y,
+             f := (fun arg1 arg2 : Bool, arg1 /\ arg2 <=>
+                                         arg2 /\ arg1 <=>
+                                         arg1 \/ arg2 \/ arg2)
+         in (f x y) \/ z)
+Eval let x := true,
+         y := true,
+         z := x /\ y,
+         f := (fun arg1 arg2 : Bool, arg1 /\ arg2 <=>
+                                     arg2 /\ arg1 <=>
+                                     arg1 \/ arg2 \/ arg2)
+     in (f x y) \/ z

src/frontend/builtin_notation.cpp

@@ -21,5 +21,7 @@ void init_builtin_notation(frontend & f) {
     f.add_infixr("\u2228", 30, const_name(mk_or_fn()));
     f.add_infixr("=>", 25, const_name(mk_implies_fn()));
     f.add_infixr("\u21D2", 25, const_name(mk_implies_fn()));
+    f.add_infixr("<=>", 25, const_name(mk_iff_fn()));
+    f.add_infixr("\u21D4", 25, const_name(mk_iff_fn()));
 }
 }

src/frontend/parser.cpp

@@ -13,9 +13,10 @@ Author: Leonardo de Moura
 #include "type_check.h"
 #include "free_vars.h"
 #include "builtin_notation.h"
-#include "pp.h"
 #include "builtin.h"
 #include "arith.h"
+#include "pp.h"
+#include "printer.h"
 
 namespace lean {
 static name g_definition_kwd("Definition");
@@ -81,6 +82,8 @@ struct parser_fn {
     bool curr_is_identifier() const { return curr() == scanner::token::Id; }
     bool curr_is_lparen() const { return curr() == scanner::token::LeftParen; }
     bool curr_is_colon() const { return curr() == scanner::token::Colon; }
+    bool curr_is_comma() const { return curr() == scanner::token::Comma; }
+    bool curr_is_in() const { return curr() == scanner::token::In; }
 
     void check_identifier(char const * msg) { if (!curr_is_identifier()) throw parser_error(msg); }
     name check_identifier_next(char const * msg) { check_identifier(msg); name r = curr_name(); next(); return r; }
@@ -348,6 +351,31 @@ struct parser_fn {
         return parse_abstraction(false);
     }
 
+    expr parse_let() {
+        next();
+        local_decls::mk_scope scope(m_local_decls);
+        buffer<std::pair<name, expr>> bindings;
+        while (true) {
+            name id  = check_identifier_next("invalid let expression, identifier expected");
+            check_assign_next("invalid let expression, ':=' expected");
+            expr val = parse_expr();
+            register_binding(id);
+            bindings.push_back(mk_pair(id, val));
+            if (curr_is_in()) {
+                next();
+                expr r = parse_expr();
+                unsigned i = bindings.size();
+                while (i > 0) {
+                    --i;
+                    r = mk_let(bindings[i].first, bindings[i].second, r);
+                }
+                return r;
+            } else {
+                check_comma_next("invalid let expression, ',' or 'in' expected");
+            }
+        }
+    }
+
     expr parse_int() {
         expr r = mk_int_value(m_scanner.get_num_val().get_numerator());
         next();
@@ -374,6 +402,7 @@ struct parser_fn {
         case scanner::token::LeftParen:  return parse_lparen();
         case scanner::token::Lambda:     return parse_lambda();
         case scanner::token::Pi:         return parse_pi();
+        case scanner::token::Let:        return parse_let();
         case scanner::token::IntVal:     return parse_int();
         case scanner::token::DecimalVal: return parse_decimal();
         case scanner::token::StringVal:  return parse_string();

src/frontend/scanner.cpp

@@ -19,6 +19,8 @@ static name g_arrow_unicode("\u2192");
 static name g_lambda_name("fun");
 static name g_type_name("Type");
 static name g_pi_name("Pi");
+static name g_let_name("let");
+static name g_in_name("in");
 static name g_arrow_name("->");
 static name g_eq_name("=");
 
@@ -193,6 +195,10 @@ scanner::token scanner::read_a_symbol() {
                 return token::Pi;
             else if (m_name_val == g_type_name)
                 return token::Type;
+            else if (m_name_val == g_let_name)
+                return token::Let;
+            else if (m_name_val == g_in_name)
+                return token::In;
             else
                 return is_command(m_name_val) ? token::CommandId : token::Id;
         }
@@ -347,6 +353,8 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
     case scanner::token::Lambda:            out << g_lambda_unicode; break;
     case scanner::token::Pi:                out << g_pi_unicode; break;
     case scanner::token::Arrow:             out << g_arrow_unicode; break;
+    case scanner::token::Let:               out << "let"; break;
+    case scanner::token::In:                out << "in"; break;
     case scanner::token::Id:                out << "Id"; break;
     case scanner::token::CommandId:         out << "CId"; break;
     case scanner::token::IntVal:            out << "Int"; break;

src/frontend/scanner.h

@@ -19,7 +19,7 @@ class scanner {
 public:
     enum class token {
         LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
-        Id, CommandId, IntVal, DecimalVal, StringVal, Eq, Assign, Type, Eof
+        Let, In, Id, CommandId, IntVal, DecimalVal, StringVal, Eq, Assign, Type, Eof
     };
 protected:
     int                m_spos; // position in the current line of the stream

src/kernel/builtin.cpp

@@ -167,6 +167,7 @@ MK_BUILTIN(ite_fn, ite_fn_value);
 
 MK_CONSTANT(if_fn,      name("if"));
 MK_CONSTANT(implies_fn, name("implies"));
+MK_CONSTANT(iff_fn,     name("iff"));
 MK_CONSTANT(and_fn,     name("and"));
 MK_CONSTANT(or_fn,      name("or"));
 MK_CONSTANT(not_fn,     name("not"));
@@ -210,6 +211,9 @@ void add_basic_theory(environment & env) {
     // implies(x, y) := ite x y True
     env.add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
 
+    // iff(x, y) := x = y
+    env.add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y)));
+
     // not(x) := ite x False True
     env.add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
 

src/kernel/builtin.h

@@ -67,6 +67,14 @@ inline expr mk_implies(unsigned num_args, expr const * args) { lean_assert(num_a
 inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); }
 inline expr Implies(std::initializer_list<expr> const & l) { return mk_implies(l.size(), l.begin()); }
 
+/** \brief Return the Lean Iff operator */
+expr mk_iff_fn();
+/** \brief Return (e1 iff e2) */
+inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app(mk_iff_fn(), e1, e2); }
+inline expr mk_iff(unsigned num_args, expr const * args) { return mk_bin_rop(mk_iff_fn(), True, num_args, args); }
+inline expr Iff(expr const & e1, expr const & e2) { return mk_iff(e1, e2); }
+inline expr Iff(std::initializer_list<expr> const & l) { return mk_iff(l.size(), l.begin()); }
+
 /** \brief Return the Lean And operator */
 expr mk_and_fn();
 /** \brief Return (e1 and e2) */