Add parse_theorem and parse_definition

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

examples/ex3.lean

@@ -0,0 +1,12 @@
+Definition xor (x y : Bool) : Bool := (not x) = y
+Infixr 50 ⊕ xor
+Show xor true false
+Eval xor true true
+Eval xor true false
+Variable a : Bool
+Show a ⊕ a ⊕ a
+Check Subst
+Theorem EM2 (a : Bool) : a \/ (not a) :=
+   Case (fun x : Bool, x \/ (not x)) Trivial Trivial a
+Check EM2
+Check EM2 a

src/frontend/parser.cpp

@@ -80,6 +80,7 @@ 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; }
 
     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; }
@@ -87,6 +88,7 @@ struct parser_fn {
     void check_comma_next(char const * msg) { check_next(scanner::token::Comma, msg); }
     void check_lparen_next(char const * msg) { check_next(scanner::token::LeftParen, msg); }
     void check_rparen_next(char const * msg) { check_next(scanner::token::RightParen, msg); }
+    void check_assign_next(char const * msg) { check_next(scanner::token::Assign, msg); }
     void check_name(name const & op, char const * msg) { if(!curr_is_identifier() || curr_name() != op) throw parser_error(msg); }
     void check_name_next(name const & op, char const * msg) { check_name(op, msg); next(); }
 
@@ -315,13 +317,8 @@ struct parser_fn {
         }
     }
 
-    expr parse_abstraction(bool is_lambda) {
+    expr mk_abstraction(bool is_lambda, buffer<std::pair<name, expr>> const & bindings, expr const & body) {
-        next();
+        expr result = body;
-        local_decls::mk_scope scope(m_local_decls);
-        buffer<std::pair<name, expr>> bindings;
-        parse_bindings(bindings);
-        check_comma_next("invalid abstraction, ',' expected");
-        expr result = parse_expr();
         unsigned i = bindings.size();
         while (i > 0) {
             --i;
@@ -333,6 +330,16 @@ struct parser_fn {
         return result;
     }
 
+    expr parse_abstraction(bool is_lambda) {
+        next();
+        local_decls::mk_scope scope(m_local_decls);
+        buffer<std::pair<name, expr>> bindings;
+        parse_bindings(bindings);
+        check_comma_next("invalid abstraction, ',' expected");
+        expr result = parse_expr();
+        return mk_abstraction(is_lambda, bindings, result);
+    }
+
     expr parse_lambda() {
         return parse_abstraction(true);
     }
@@ -426,11 +433,38 @@ struct parser_fn {
         return e;
     }
 
-    void parse_definition() {
+    void parse_def_core(bool is_definition) {
         next();
+        expr type, val;
         name id = check_identifier_next("invalid definition, identifier expected");
-        check_colon_next("invalid definition, ':' expected");
+        if (curr_is_colon()) {
-        // TODO
+            next();
+            type = elaborate(parse_expr());
+            check_assign_next("invalid definition, ':=' expected");
+            val  = elaborate(parse_expr());
+        } else {
+            local_decls::mk_scope scope(m_local_decls);
+            buffer<std::pair<name, expr>> bindings;
+            parse_bindings(bindings);
+            check_colon_next("invalid definition, ':' expected");
+            expr type_body = parse_expr();
+            check_assign_next("invalid definition, ':=' expected");
+            expr val_body  = parse_expr();
+            type = elaborate(mk_abstraction(false, bindings, type_body));
+            val  = elaborate(mk_abstraction(true, bindings, val_body));
+        }
+        if (is_definition)
+            m_frontend.add_definition(id, type, val);
+        else
+            m_frontend.add_theorem(id, type, val);
+    }
+
+    void parse_definition() {
+        parse_def_core(true);
+    }
+
+    void parse_theorem() {
+        parse_def_core(false);
     }
 
     void parse_variable() {
@@ -441,10 +475,6 @@ struct parser_fn {
         m_frontend.add_var(id, type);
     }
 
-    void parse_theorem() {
-        // TODO
-    }
-
     void parse_axiom() {
         next();
         name id = check_identifier_next("invalid axiom, identifier expected");