feat(library/init/lean/parser): declarations and binders

library/init/lean/parser/basic.lean

@@ -48,6 +48,7 @@ structure parser_config :=
 def parser_t (m : Type → Type) [monad m] := reader_t parser_config $ state_t parser_state $ parsec_t syntax m
 abbreviation basic_parser_m := parser_t id
 abbreviation basic_parser := basic_parser_m syntax
+abbreviation monad_basic_read := has_monad_lift_t basic_parser_m
 
  -- an arbitrary `parser` type; parsers are usually some monad stack based on `basic_parser_m` returning `syntax`
 variable {ρ : Type}
@@ -125,5 +126,16 @@ def parse.view : syntax → option parse.view_ty
 | (syntax.node ⟨none, [root, eoi]⟩) := some ⟨root, eoi⟩
 | _ := none
 
+
+/- Monad stacks used in multiple files -/
+
+@[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_read]
+def command_parser_m := rec_t unit syntax basic_parser_m
+abbreviation command_parser := command_parser_m syntax
+
+@[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_read]
+def term_parser_m := rec_t nat syntax command_parser_m
+abbreviation term_parser := term_parser_m syntax
+
 end «parser»
 end lean

library/init/lean/parser/combinators.lean

@@ -10,6 +10,9 @@ import init.lean.parser.basic
 
 namespace lean
 namespace parser
+
+@[pattern] def choice := {syntax_node_kind . name := `lean.parser.choice}
+
 namespace combinators
 open has_tokens has_view monad_parsec
 
@@ -39,10 +42,11 @@ instance node.view (k) (rs : list parser) [i : syntax_node_kind.has_view k α] :
 
 private def many1_aux (p : parser) : list syntax → nat → parser
 | as 0     := error "unreachable"
-| as (n+1) := do a ← catch p (λ msg, throw {msg with custom :=
-                       -- append `syntax.missing` to make clear that list is incomplete
-                       syntax.node ⟨none, (syntax.missing::msg.custom::as).reverse⟩}),
-              many1_aux (a::as) n <|> pure (syntax.node ⟨none, (a::as).reverse⟩)
+| as (n+1) := do
+  a ← catch p (λ msg, throw {msg with custom :=
+    -- append `syntax.missing` to make clear that list is incomplete
+    syntax.node ⟨none, (syntax.missing::msg.custom::as).reverse⟩}),
+  many1_aux (a::as) n <|> pure (syntax.node ⟨none, (a::as).reverse⟩)
 
 def many1 (r : parser) : parser :=
 do rem ← remaining, many1_aux r [] (rem+1)
@@ -66,6 +70,59 @@ instance many.tokens (r : parser) [parser.has_tokens r] : parser.has_tokens (man
 instance many.view (r : parser) [has_view r α] : parser.has_view (many r) (list α) :=
 {..many1.view r}
 
+private def sep_by_aux (p : m syntax) (sep : parser) (allow_trailing_sep : bool) : bool → list syntax → nat → parser
+| p_opt as 0     := error "unreachable"
+| p_opt as (n+1) := do
+  let p := if p_opt then some <$> p <|> pure none else some <$> p,
+  some a ← catch p (λ msg, throw {msg with custom :=
+    -- append `syntax.missing` to make clear that list is incomplete
+    syntax.node ⟨none, (syntax.missing::msg.custom::as).reverse⟩})
+    | pure (syntax.node ⟨none, as.reverse⟩),
+  -- I don't want to think about what the output on a failed separator parse should look like
+  let sep := try sep,
+  some s ← some <$> sep <|> pure none
+    | pure (syntax.node ⟨none, (a::as).reverse⟩),
+  sep_by_aux allow_trailing_sep (s::a::as) n
+
+def sep_by (p sep : parser) (allow_trailing_sep := tt) : parser :=
+do rem ← remaining, sep_by_aux p sep allow_trailing_sep tt [] (rem+1)
+
+def sep_by1 (p sep : parser) (allow_trailing_sep := tt) : parser :=
+do rem ← remaining, sep_by_aux p sep allow_trailing_sep ff [] (rem+1)
+
+instance sep_by.tokens (p sep : parser) (a) [parser.has_tokens p] [parser.has_tokens sep] :
+  parser.has_tokens (sep_by p sep a) :=
+⟨tokens p ++ tokens sep⟩
+
+private def sep_by.view_aux {α β} (p sep : parser) [parser.has_view p α] [parser.has_view sep β] :
+  list syntax → option (list (α × option β))
+| []    := some []
+| [stx] := do
+  vp ← view p stx,
+  some [(vp, none)]
+| (stx1::stx2::stxs) := do
+  vp ← view p stx1,
+  vsep ← view sep stx2,
+  vs ← sep_by.view_aux stxs,
+  some ((vp, some vsep)::vs)
+
+instance sep_by.view {α β} (p sep : parser) (a) [parser.has_view p α] [parser.has_view sep β] :
+  parser.has_view (sep_by p sep a) (list (α × option β)) :=
+{ view := λ stx, match stx with
+    | syntax.node ⟨none, stxs⟩ := sep_by.view_aux p sep stxs
+    | _ := failure,
+  review := λ as, syntax.node ⟨none, as.bind (λ a, match a with
+    | ⟨v, some vsep⟩ := [review p v, review sep vsep]
+    | ⟨v, none⟩      := [review p v])⟩ }
+
+instance sep_by1.tokens (p sep : parser) (a) [parser.has_tokens p] [parser.has_tokens sep] :
+  parser.has_tokens (sep_by1 p sep a) :=
+⟨tokens (sep_by p sep a)⟩
+
+instance sep_by1.view {α β} (p sep : parser) (a) [parser.has_view p α] [parser.has_view sep β] :
+  parser.has_view (sep_by1 p sep a) (list (α × option β)) :=
+{..sep_by.view p sep a}
+
 def optional (r : parser) : parser :=
 do r ← optional $
      -- on error, wrap in "some"
@@ -111,9 +168,20 @@ match rs with
 
 instance any_of.tokens (rs : list parser) [parser.has_tokens rs] : parser.has_tokens (any_of rs) :=
 ⟨tokens rs⟩
-
 instance any_of.view (rs : list parser) : parser.has_view (any_of rs) syntax := default _
 
+/-- Parse a list `[p1, ..., pn]` of parsers with `monad_parsec.longest_match`.
+    If the result is ambiguous, wrap it in a `choice` node.
+    Note that there is NO explicit encoding of which parser was chosen;
+    parsers should instead produce distinct node names for disambiguation. -/
+def longest_match (rs : list parser) : parser :=
+do stxs ← monad_parsec.longest_match rs,
+   pure $ syntax.node ⟨choice, stxs⟩
+
+instance longest_match.tokens (rs : list parser) [parser.has_tokens rs] : parser.has_tokens (longest_match rs) :=
+⟨tokens rs⟩
+instance longest_match.view (rs : list parser) : parser.has_view (longest_match rs) syntax := default _
+
 /-- Parse a list `[p1, ..., pn]` of parsers as `p1 <|> ... <|> pn`.
     The result will be wrapped in a node with the the index of the successful
     parser as the name. -/
@@ -172,6 +240,11 @@ instance seq_right.tokens {α : Type} (x : m α) (p : m syntax) [parser.has_toke
 instance seq_right.view {α β : Type} (x : m α) (p : m syntax) [i : parser.has_view p β] : parser.has_view (x *> p) β :=
 {..i}
 
+instance coe.tokens {β} (r : parser) [parser.has_tokens r] [has_coe_t parser β]: parser.has_tokens (coe r : β) :=
+⟨tokens r⟩
+instance coe.view {β} (r : parser) [i : parser.has_view r α] [has_coe_t parser β] : parser.has_view (coe r : β) α :=
+{..i}
+
 end combinators
 end parser
 end lean

library/init/lean/parser/command.lean

@@ -6,7 +6,7 @@ Author: Sebastian Ullrich
 Command parsers
 -/
 prelude
-import init.lean.parser.notation
+import init.lean.parser.declaration
 
 namespace lean
 namespace parser
@@ -21,9 +21,10 @@ local postfix +:10000 := combinators.many1
 @[derive parser.has_view parser.has_tokens]
 def command_parser.recurse : command_parser := recurse ()
 
+set_option class.instance_max_depth 200
+
 namespace «command»
 
-set_option class.instance_max_depth 200
 @[derive parser.has_view parser.has_tokens]
 def open_spec.parser : command_parser :=
 node! open_spec [
@@ -62,7 +63,7 @@ open «command»
 @[derive parser.has_tokens parser.has_view]
 def command.parser : command_parser :=
 any_of [open.parser, section.parser, universe.parser, notation.parser, reserve_notation.parser,
-  mixfix.parser, reserve_mixfix.parser, check.parser] <?> "command"
+  mixfix.parser, reserve_mixfix.parser, check.parser, declaration.parser] <?> "command"
 
 end parser
 

library/init/lean/parser/declaration.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sebastian Ullrich
+
+Parsers for commands that declare things
+-/
+
+prelude
+import init.lean.parser.term
+
+namespace lean
+namespace parser
+
+open combinators monad_parsec
+open parser.has_tokens parser.has_view
+
+instance term_parser_command_parser_coe : has_coe term_parser command_parser :=
+-- run `p` directly, but use the general `term.parser` for recursion
+⟨λ p, reader_t.run p $ λ rbp, term.parser rbp⟩
+
+namespace «command»
+
+local postfix `?`:10000 := optional
+local postfix *:10000 := combinators.many
+local postfix +:10000 := combinators.many1
+
+@[derive has_tokens has_view]
+def attr_instance.parser : command_parser :=
+node! attr_instance [name: ident.parser, args: term.parser*]
+
+@[derive has_tokens has_view]
+def decl_attributes.parser : command_parser :=
+-- TODO(Seabstian): custom attribute parsers
+node! decl_attribute ["@[", attrs: sep_by1 attr_instance.parser (symbol ","), "]"]
+
+set_option class.instance_max_depth 200
+@[derive has_tokens has_view]
+def decl_modifiers.parser : command_parser :=
+node! decl_modifiers [
+  visibility: node_choice! visibility {"private", "protected"}?,
+  «noncomputable»: (symbol "noncomputable")?,
+  «meta»: (symbol "meta")?,
+  attrs: decl_attributes.parser?
+]
+
+@[derive has_tokens has_view]
+def decl_sig.parser : command_parser :=
+node! decl_sig [
+  params: term.bracketed_binder.parser*,
+  type: node! decl_type [":", type: term.parser]?
+]
+
+@[derive has_tokens has_view]
+def equation.parser : command_parser :=
+node! equation ["|", lhs: term.parser, ":=", rhs: term.parser]
+
+@[derive has_tokens has_view]
+def decl_val.parser : command_parser :=
+node_choice! decl_val {
+  simple: node! simple_decl_val [":=", body: term.parser],
+  empty_match: symbol ".",
+  «match»: equation.parser+
+}
+
+@[derive has_tokens has_view]
+def declaration.parser : command_parser :=
+node! declaration [
+  modifiers: decl_modifiers.parser,
+  inner: node_choice! declaration.inner {
+    «def»: node! «def» ["def", name: ident.parser, sig: decl_sig.parser, val: decl_val.parser],
+    «abbreviation»: node! «abbreviation» ["abbreviation", name: ident.parser, sig: decl_sig.parser, val: decl_val.parser],
+    «theorem»: node! «theorem» ["theorem", name: ident.parser, sig: decl_sig.parser, val: decl_val.parser],
+    «instance»: node! «instance» ["instance", name: ident.parser?, sig: decl_sig.parser, val: decl_val.parser],
+    «example»: node! «example» ["example", sig: decl_sig.parser, val: decl_val.parser],
+  }
+]
+
+end «command»
+end parser
+end lean

library/init/lean/parser/notation.lean

@@ -6,7 +6,7 @@ Author: Sebastian Ullrich
 Notation parsers
 -/
 prelude
-import init.lean.parser.term
+import init.lean.parser.token
 
 namespace lean
 namespace parser
@@ -23,10 +23,10 @@ set_option class.instance_max_depth 100
 
 namespace notation_spec
 @[derive parser.has_tokens parser.has_view]
-def precedence.parser : command_parser :=
+def precedence.parser : term_parser :=
 node! «precedence» [":", prec: number]/-TODO <|> expr-/
 
-def quoted_symbol.parser : command_parser :=
+def quoted_symbol.parser : term_parser :=
 do (s, info) ← with_source_info $ take_until (= '`'),
    pure $ syntax.atom ⟨info, s⟩
 
@@ -34,7 +34,7 @@ instance quoted_symbol.tokens : parser.has_tokens quoted_symbol.parser := ⟨[]
 instance quoted_symbol.view : parser.has_view quoted_symbol.parser syntax := default _
 
 @[derive parser.has_tokens parser.has_view]
-def symbol_quote.parser : command_parser :=
+def symbol_quote.parser : term_parser :=
 node! notation_quoted_symbol [
   left_quote: raw $ ch '`',
   symbol: quoted_symbol.parser,
@@ -43,14 +43,14 @@ node! notation_quoted_symbol [
 
 --TODO(Sebastian): cannot be called `symbol` because of hygiene problems
 @[derive parser.has_tokens parser.has_view]
-def notation_symbol.parser : command_parser :=
+def notation_symbol.parser : term_parser :=
 node_choice! notation_symbol {
   quoted: symbol_quote.parser
   --TODO, {read := do tk ← token, /- check if reserved token-/}
 }
 
 @[derive parser.has_tokens parser.has_view]
-def action.parser : command_parser :=
+def action.parser : term_parser :=
 node! action [":", action: node_choice! action_kind {
   prec: number,
   max: symbol_or_ident "max",
@@ -63,7 +63,7 @@ node! action [":", action: node_choice! action_kind {
     notation_tk,-/}]
 
 @[derive parser.has_tokens parser.has_view]
-def transition.parser : command_parser :=
+def transition.parser : term_parser :=
 node_choice! transition {
   binder: node! binder ["binder", prec: precedence.parser?],
   binders: node! binders ["binders", prec: precedence.parser?],
@@ -71,38 +71,38 @@ node_choice! transition {
 }
 
 @[derive parser.has_tokens parser.has_view]
-def rule.parser : command_parser :=
+def rule.parser : term_parser :=
 node! rule [symbol: notation_symbol.parser, transition: transition.parser?]
 
 end notation_spec
 
 @[derive parser.has_tokens parser.has_view]
-def notation_spec.parser : command_parser :=
+def notation_spec.parser : term_parser :=
 node_choice! notation_spec {
   number_literal: number,
   rules: node! notation_spec.rules [id: ident.parser?, rules: notation_spec.rule.parser*]
 }
 
 @[derive parser.has_tokens parser.has_view]
-def notation.parser : command_parser :=
-node! «notation» ["notation", spec: notation_spec.parser, ":=", term: term.parser]
+def notation.parser : term_parser :=
+node! «notation» ["notation", spec: notation_spec.parser, ":=", term: recurse 0]
 
 @[derive parser.has_tokens parser.has_view]
-def reserve_notation.parser : command_parser :=
+def reserve_notation.parser : term_parser :=
 node! «reserve_notation» [try ["reserve", "notation"], spec: notation_spec.parser]
 
 @[derive parser.has_tokens parser.has_view]
-def mixfix.kind.parser : command_parser :=
+def mixfix.kind.parser : term_parser :=
 node_choice! mixfix.kind {"prefix", "infix", "infixl", "infixr", "postfix"}
 
 @[derive parser.has_tokens parser.has_view]
-def mixfix.parser : command_parser :=
+def mixfix.parser : term_parser :=
 node! «mixfix» [
   kind: mixfix.kind.parser,
-  symbol: notation_spec.notation_symbol.parser, ":=", term: term.parser]
+  symbol: notation_spec.notation_symbol.parser, ":=", term: recurse 0]
 
 @[derive parser.has_tokens parser.has_view]
-def reserve_mixfix.parser : command_parser :=
+def reserve_mixfix.parser : term_parser :=
 node! «reserve_mixfix» [
   try ["reserve", kind: mixfix.kind.parser],
   symbol: notation_spec.notation_symbol.parser]

library/init/lean/parser/term.lean

@@ -6,7 +6,7 @@ Author: Sebastian Ullrich
 Term-level parsers
 -/
 prelude
-import init.lean.parser.level
+import init.lean.parser.level init.lean.parser.notation
 
 namespace lean
 namespace parser
@@ -16,20 +16,12 @@ local postfix `?`:10000 := optional
 local postfix *:10000 := combinators.many
 local postfix +:10000 := combinators.many1
 
-@[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_read]
-def command_parser_m := rec_t unit syntax basic_parser_m
-abbreviation command_parser := command_parser_m syntax
-
-@[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_read]
-def term_parser_m := rec_t nat syntax command_parser_m
-abbreviation term_parser := term_parser_m syntax
 
 /-- A term parser for a suffix or infix notation that accepts a preceding term. -/
 @[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_read]
 def trailing_term_parser_m := reader_t syntax term_parser_m
 abbreviation trailing_term_parser := trailing_term_parser_m syntax
 
-
 @[derive parser.has_tokens parser.has_view]
 def ident_univ_spec.parser : basic_parser :=
 node! ident_univ_spec [".{", levels: level.parser+, "}"]
@@ -52,6 +44,66 @@ node! hole [hole: symbol "_" max_prec]
 def sort.parser : term_parser :=
 node_choice! sort {"Sort":max_prec, "Type":max_prec}
 
+set_option class.instance_max_depth 200
+
+section binder
+@[derive has_tokens has_view]
+def binder_content.parser : term_parser :=
+node! binder_content [
+  ids: (node_choice! binder_id {id: ident.parser, hole: hole.parser})+,
+  type: node! binder_content_type [":", type: recurse 0],
+  default: node_choice! binder_default {
+    val: node! binder_default_val [":=", term: recurse 0],
+    tac: node! binder_default_tac [".", term: recurse 0]
+  }?
+]
+
+/- All binders must be surrounded with some kind of bracket. (e.g., '()', '{}', '[]').
+   We use this feature when parsing examples/definitions/theorems. The goal is to avoid counter-intuitive
+   declarations such as:
+
+     example p : false := trivial
+     def main proof : false := trivial
+
+   which would be parsed as
+
+     example (p : false) : _ := trivial
+
+     def main (proof : false) : _ := trivial
+
+   where `_` in both cases is elaborated into `true`. This issue was raised by @gebner in the slack channel.
+
+
+   Remark: we still want implicit delimiters for lambda/pi expressions. That is, we want to
+   write
+
+       fun x : t, s
+   or
+       fun x, s
+
+   instead of
+
+       fun (x : t), s -/
+@[derive has_tokens has_view]
+def bracketed_binder.parser : term_parser :=
+node_choice! bracketed_binder {
+  explicit: node! explicit_binder ["(":max_prec, content: node_choice! explicit_binder_content {
+    «notation»: any_of [command.notation.parser, command.mixfix.parser],
+    other: binder_content.parser
+  }, right: symbol ")"],
+  implicit: node! implicit_binder ["{":max_prec, content: binder_content.parser, "}"],
+  strict_implicit: node! strict_implicit_binder [
+    left: any_of [symbol "{{" max_prec, symbol "⦃" max_prec],
+    content: binder_content.parser,
+    right: any_of [symbol "}}", symbol "⦄"]
+  ],
+  inst_implicit: node! inst_implicit_binder ["[":max_prec, content: longest_match [
+    node! inst_implicit_named_binder [id: ident.parser, type: recurse 0],
+    node! inst_implicit_anonymous_binder [type: recurse 0]
+  ], "]"]
+}
+end binder
+
 @[derive parser.has_tokens parser.has_view]
 def leading.parser :=
 any_of [

library/init/lean/parser/token.lean

@@ -46,7 +46,6 @@ do whitespace,
    pure ()
 | 0 := error "unreachable"
 
-abbreviation monad_basic_read := has_monad_lift_t basic_parser_m
 variables {m : Type → Type}
 local notation `parser` := m syntax
 local notation `lift` := @monad_lift basic_parser_m _ _ _