feat(library/init/lean): progress

library/init/core.lean

@@ -328,7 +328,7 @@ inductive list (T : Type u)
 | nil {} : list
 | cons (hd : T) (tl : list) : list
 
-notation h :: t  := list.cons h t
+infixr :: := list.cons
 notation `[` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) := l
 
 inductive nat
@@ -375,7 +375,7 @@ export has_andthen (andthen)
 export has_pow (pow)
 
 infix ∈        := has_mem.mem
-notation a ∉ s := ¬ has_mem.mem a s
+notation a ` ∉ ` s := ¬ has_mem.mem a s
 infix +        := has_add.add
 infix *        := has_mul.mul
 infix -        := has_sub.sub
@@ -471,7 +471,7 @@ be stronger than application.
 
 def std.prec.max_plus : nat := std.prec.max + 10
 
-notation α × β := prod α β
+infixr × := prod
 -- notation for n-ary tuples
 
 /- sizeof -/
@@ -618,9 +618,9 @@ attribute [elab_simple] bin_tree.node bin_tree.leaf
 | ff tt  := tt
 | _  _   := ff
 
-notation !x     := bnot x
-notation x || y := bor x y
-notation x && y := band x y
+prefix ! := bnot
+infix || := bor
+infix && := band
 
 /- Logical connectives an equality -/
 
@@ -687,7 +687,7 @@ theorem cast_proof_irrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast
 theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a := rfl
 
 @[reducible] def ne {α : Sort u} (a b : α) := ¬(a = b)
-notation a ≠ b := ne a b
+infix ≠ := ne
 
 theorem ne.def {α : Sort u} (a b : α) : a ≠ b = ¬ (a = b) := rfl
 
@@ -1530,10 +1530,10 @@ variables {α : Type u} {β : Type v}
 variable f : α → α → α
 variable inv : α → α
 variable one : α
-local notation a * b := f a b
+local infix * := f
 local postfix `⁻¹`:max := inv
 variable g : α → α → α
-local notation a + b := g a b
+local infix + := g
 
 def commutative        := ∀ a b, a * b = b * a
 def associative        := ∀ a b c, (a * b) * c = a * (b * c)

library/init/lean/elaborator.lean

@@ -33,6 +33,46 @@ do cfg ← read,
 
 local attribute [instance] name.has_lt_quick
 
+def prec_to_nat (prec : option precedence.view) : nat :=
+(prec <&> λ p, p.prec.to_nat).get_or_else 0
+
+def command_parser_config.register_notation_tokens (spec : notation_spec.view) (cfg : command_parser_config) :
+  except string command_parser_config :=
+do spec.rules.mfoldl (λ (cfg : command_parser_config) r, match r.symbol with
+   | notation_symbol.view.quoted {symbol := syntax.atom a, prec := prec, ..} :=
+     pure {cfg with tokens := cfg.tokens.insert a.val.trim {«prefix» := a.val.trim, lbp := prec_to_nat prec}}
+   | _ := throw "register_notation_tokens: unreachable") cfg
+
+def command_parser_config.register_notation_parser (spec : notation_spec.view) (cfg : command_parser_config) :
+  except string command_parser_config :=
+do -- build and register parser
+   let k : syntax_node_kind := {name := "notation<TODO>"},
+   ps ← spec.rules.mmap (λ r : rule.view, do
+     psym ← match r.symbol with
+     | notation_symbol.view.quoted {symbol := syntax.atom a ..} :=
+       pure (symbol a.val : term_parser)
+     | _ := throw "register_notation_parser: unreachable",
+     ptrans ← match r.transition with
+     | some (transition.view.binders b) :=
+       pure $ some $ term.binders.parser
+     | some (transition.view.arg {action := none, ..}) :=
+       pure $ some term.parser
+     | some (transition.view.arg {action := some {action := action_kind.view.prec prec}, ..}) :=
+       pure $ some $ term.parser prec.to_nat
+     | some (transition.view.arg {action := some {action := action_kind.view.scoped sc}, ..}) :=
+       pure $ some $ term.parser $ prec_to_nat sc.prec
+     | none := pure $ none
+     | _ := throw "register_notation_parser: unimplemented",
+     pure $ psym::ptrans.to_monad
+   ),
+   let ps := ps.bind id,
+   cfg ← match spec.prefix_arg with
+   | none   := pure {cfg with leading_term_parsers :=
+     parser.combinators.node k ps::cfg.leading_term_parsers}
+   | some _ := pure {cfg with trailing_term_parsers :=
+     parser.combinators.node k (read::ps.map coe)::cfg.trailing_term_parsers},
+   pure cfg
+
 def postprocess_notation_spec (spec : notation_spec.view) : notation_spec.view :=
 -- default leading tokens to `max`
 -- NOTE: should happen after copying precedences from reserved notation

library/init/lean/expander.lean

@@ -37,11 +37,11 @@ instance coe_name_ident : has_coe name parser.ident.view :=
 instance coe_ident_term_ident : has_coe parser.ident.view term.ident.view :=
 ⟨λ id, {id := id}⟩
 
-instance coe_term_ident_binder_id : has_coe term.ident.view binder_id.view :=
-⟨binder_id.view.id⟩
+instance coe_term_ident_binder_id : has_coe term.ident.view binder_ident.view :=
+⟨binder_ident.view.id⟩
 
-instance coe_binders {α : Type} [has_coe_t α binder_id.view] : has_coe (list α) term.binders.view :=
-⟨λ ids, binders.view.unbracketed {ids := ids.map coe}⟩
+instance coe_binders {α : Type} [has_coe_t α binder_ident.view] : has_coe (list α) term.binders.view :=
+⟨λ ids, {leading_ids := ids.map coe}⟩
 
 def mixfix_to_notation_spec (k : mixfix.kind.view) (sym : notation_symbol.view) : transform_m notation_spec.view :=
 let prec := match sym with

library/init/lean/parser/command.lean

@@ -40,9 +40,29 @@ node! open_spec [
 def open.parser : command_parser :=
 node! «open» ["open", spec: open_spec.parser]
 
+@[derive parser.has_tokens]
+def export.parser : command_parser :=
+node! «export» ["export", spec: open_spec.parser]
+
 @[derive parser.has_tokens]
 def section.parser : command_parser :=
-node! «section» ["section", name: ident.parser?, commands: command.parser*, "end", end_name: ident.parser?]
+node! «section» ["section", name: ident.parser?]
+
+@[derive parser.has_tokens]
+def namespace.parser : command_parser :=
+node! «namespace» ["namespace", name: ident.parser]
+
+@[derive parser.has_tokens]
+def variable.parser : command_parser :=
+node! «variable» ["variable", binder: term.bracketed_binder.parser]
+
+@[derive parser.has_tokens]
+def variables.parser : command_parser :=
+node! «variables» ["variables", binders: term.bracketed_binder.parser+]
+
+@[derive parser.has_tokens]
+def end.parser : command_parser :=
+node! «end» ["end", name: ident.parser?]
 
 @[derive parser.has_tokens]
 def universe.parser : command_parser :=
@@ -58,10 +78,22 @@ any_of [
 def check.parser : command_parser :=
 node! check ["#check", term: term.parser]
 
+@[derive parser.has_tokens parser.has_view]
+def attribute.parser : command_parser :=
+node! «attribute» [
+  «local»: (symbol "local ")?,
+  "attribute ",
+  "[",
+  attrs: sep_by1 attr_instance.parser (symbol ", "),
+  "] ",
+  ids: ident.parser*
+]
+
 @[derive has_tokens]
 def builtin_command_parsers : list command_parser := [
   open.parser, section.parser, universe.parser, notation.parser, reserve_notation.parser,
-  mixfix.parser, reserve_mixfix.parser, check.parser, declaration.parser]
+  mixfix.parser, reserve_mixfix.parser, check.parser, declaration.parser, attribute.parser,
+  export.parser, namespace.parser, end.parser, variable.parser, variables.parser]
 end «command»
 
 def command_parser.run (commands : list command_parser) (p : command_parser)

library/init/lean/parser/declaration.lean

@@ -40,7 +40,7 @@ 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
+-- TODO(Sebastian): custom attribute parsers
 node! decl_attribute ["@[", attrs: sep_by1 attr_instance.parser (symbol ","), "]"]
 
 set_option class.instance_max_depth 300
@@ -115,17 +115,18 @@ def declaration.parser : command_parser :=
 node! declaration [
   modifiers: decl_modifiers.parser,
   inner: node_choice! declaration.inner {
-    «def»: node! «def» ["def",
+    «def_like»: node! «def_like» [
+      kind: node_choice! def_like.kind {"def", "abbreviation", "theorem"},
       old_univ_params: node! old_univ_params ["{", ids: ident.parser+, "}"]?,
       name: term.ident.parser, sig: decl_sig.parser, val: decl_val.parser],
-    «abbreviation»: node! «abbreviation» ["abbreviation", name: term.ident.parser, sig: decl_sig.parser, val: decl_val.parser],
-    «theorem»: node! «theorem» ["theorem", name: term.ident.parser, sig: decl_sig.parser, val: decl_val.parser],
     «instance»: node! «instance» ["instance", name: term.ident.parser?, sig: decl_sig.parser, val: decl_val.parser],
     «example»: node! «example» ["example", sig: decl_sig.parser, val: decl_val.parser],
     «constant»: node! «constant» ["constant", name: term.ident.parser, sig: decl_sig.parser],
     «axiom»: node! «axiom» ["axiom", name: term.ident.parser, sig: decl_sig.parser],
 
-    «inductive»: node! «inductive» ["inductive", name: term.ident.parser, sig: decl_sig.parser,
+    «inductive»: node! «inductive» [try [«class»: (symbol "class")?, "inductive"],
+      name: term.ident.parser,
+      sig: decl_sig.parser,
       local_notation: notation_like.parser?,
       intro_rules: intro_rule.parser*],
     «structure»: structure.parser,

library/init/lean/parser/notation.lean

@@ -77,7 +77,15 @@ node! action [":", action: node_choice! action_kind {
   prec: number.parser,
   max: symbol_or_ident "max",
   prev: symbol_or_ident "prev",
-  scoped: symbol_or_ident "scoped"
+  scoped: node! scoped_action [
+    "(",
+    scoped: symbol_or_ident "scoped",
+    prec: precedence.parser?,
+    id: ident.parser,
+    ", ",
+    term: term.parser,
+    ")",
+  ],
   /-TODO seq [
     "(",
     any_of ["foldl", "foldr"],
@@ -87,8 +95,8 @@ node! action [":", action: node_choice! action_kind {
 @[derive parser.has_tokens parser.has_view]
 def transition.parser : term_parser :=
 node_choice! transition {
-  binder: node! binder ["binder", prec: precedence.parser?],
-  binders: node! binders ["binders", prec: precedence.parser?],
+  binder: node! binder [binder: symbol_or_ident "binder", prec: precedence.parser?],
+  binders: node! binders [binders: symbol_or_ident "binders", prec: precedence.parser?],
   arg: node! argument [id: ident.parser, action: action.parser?]
 }
 
@@ -131,37 +139,5 @@ node! «reserve_mixfix» [
   symbol: notation_spec.notation_symbol.parser]
 
 end «command»
-open «command»
-open command.notation_spec
-
-def command_parser_config.register_notation_tokens (spec : notation_spec.view) (cfg : command_parser_config) :
-  except string command_parser_config :=
-do spec.rules.mfoldl (λ (cfg : command_parser_config) r, match r.symbol with
-   | notation_symbol.view.quoted {symbol := syntax.atom a, prec := some prec, ..} :=
-     pure {cfg with tokens := cfg.tokens.insert a.val.trim {«prefix» := a.val.trim, lbp := prec.prec.to_nat}}
-   | _ := throw "register_notation: unreachable") cfg
-
-def command_parser_config.register_notation_parser (spec : notation_spec.view) (cfg : command_parser_config) :
-  except string command_parser_config :=
-do -- build and register parser
-   let k : syntax_node_kind := {name := "notation<TODO>"},
-   ps ← spec.rules.mmap (λ r : rule.view, do
-     psym ← match r.symbol with
-     | notation_symbol.view.quoted {symbol := syntax.atom a ..} :=
-       pure (symbol a.val : term_parser)
-     | _ := throw "register_notation: unreachable",
-     ptrans ← match r.transition with
-     | some (transition.view.arg {action := some {action := action_kind.view.prec prec}, ..}) :=
-       pure $ some $ term.parser prec.to_nat
-     | none := pure $ none
-     | _ := throw "register_notation: unimplemented",
-     pure $ psym::ptrans.to_monad
-   ),
-   let ps := ps.bind id,
-   cfg ← match spec.prefix_arg with
-   | none   := pure {cfg with leading_term_parsers := node k ps::cfg.leading_term_parsers}
-   | some _ := pure {cfg with trailing_term_parsers := node k (read::ps.map coe)::cfg.trailing_term_parsers},
-   pure cfg
-
 end parser
 end lean

library/init/lean/parser/term.lean

@@ -34,9 +34,18 @@ instance : has_view get_leading syntax := default _
 
 @[derive parser.has_tokens parser.has_view]
 def paren.parser : term_parser :=
-/- Do not allow trailing comma. Looks a bit weird and would clash with
-   adding support for tuple sections (https://downloads.haskell.org/~ghc/8.2.1/docs/html/users_guide/glasgow_exts.html#tuple-sections). -/
-node! «paren» ["(":max_prec, elems: sep_by (term.parser 0) (symbol ",") ff, ")"]
+node! «paren» ["(":max_prec,
+  content: node! paren_content [
+    term: term.parser,
+    special: node_choice! paren_special {
+      /- Do not allow trailing comma. Looks a bit weird and would clash with
+      adding support for tuple sections (https://downloads.haskell.org/~ghc/8.2.1/docs/html/users_guide/glasgow_exts.html#tuple-sections). -/
+      tuple: node! tuple [", ", tail: sep_by (term.parser 0) (symbol ", ") ff],
+      typed: node! typed [" : ", type: term.parser],
+    }?,
+  ]?,
+  ")"
+]
 
 @[derive parser.has_tokens parser.has_view]
 def hole.parser : term_parser :=
@@ -47,10 +56,14 @@ def sort.parser : term_parser :=
 node_choice! sort {"Sort":max_prec, "Type":max_prec}
 
 section binder
+@[derive has_tokens has_view]
+def binder_ident.parser : term_parser :=
+node_choice! binder_ident {id: ident.parser, hole: hole.parser}
+
 @[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})+,
+  ids: binder_ident.parser+,
   type: node! binder_content_type [":", type: term.parser 0]?,
   default: node_choice! binder_default {
     val: node! binder_default_val [":=", term: term.parser 0],
@@ -58,6 +71,10 @@ node! binder_content [
   }?
 ]
 
+@[derive parser.has_tokens parser.has_view]
+def anonymous_constructor.parser : term_parser :=
+node! anonymous_constructor ["⟨":max_prec, args: sep_by (term.parser 0) (symbol ","), "⟩"]
+
 /- 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:
@@ -98,17 +115,25 @@ node_choice! bracketed_binder {
     right: unicode_symbol "⦄" "}}",
   ],
   inst_implicit: node! inst_implicit_binder ["[":max_prec, content: longest_match [
-    node! inst_implicit_named_binder [id: ident.parser, type: term.parser 0],
+    node! inst_implicit_named_binder [id: ident.parser, " : ", type: term.parser 0],
     node! inst_implicit_anonymous_binder [type: term.parser 0]
-  ], "]"]
+  ], "]"],
+  anonymous_constructor: anonymous_constructor.parser,
 }
 
 @[derive has_tokens has_view]
 def binders.parser : term_parser :=
-node_choice! binders {
-  bracketed: bracketed_binder.parser+,
-  unbracketed: binder_content.parser,
-}
+node! binders [
+  leading_ids: binder_ident.parser*,
+  remainder: node_choice! binders_remainder {
+    type: node! binders_types [":", type: term.parser 0],
+    -- we allow mixing like in `a (b : β) c`, but not `a : α (b : β) c : γ`
+    mixed: node_choice! mixed_binder {
+      bracketed: bracketed_binder.parser,
+      id: ident.parser,
+    }+,
+  }?
+]
 
 end binder
 
@@ -121,19 +146,27 @@ node! lambda [
   body: term.parser 0
 ]
 
+@[derive parser.has_tokens parser.has_view]
+def assume.parser : term_parser :=
+node! «assume» [
+  "assume ":max_prec,
+  binders: node_choice! assume_binders {
+    anonymous: node! assume_anonymous [": ", type: term.parser],
+    binders: binders.parser
+  },
+  ", ",
+  body: term.parser 0
+]
+
 @[derive parser.has_tokens parser.has_view]
 def pi.parser : term_parser :=
 node! pi [
-  op: unicode_symbol "Π" "Pi" max_prec,
+  op: any_of [unicode_symbol "Π" "Pi" max_prec, unicode_symbol "∀" "forall" max_prec],
   binders: binders.parser,
   ",",
   range: term.parser 0
 ]
 
-@[derive parser.has_tokens parser.has_view]
-def anonymous_constructor.parser : term_parser :=
-node! anonymous_constructor ["⟨":max_prec, args: sep_by (term.parser 0) (symbol ","), "⟩"]
-
 @[derive parser.has_tokens parser.has_view]
 def explicit_ident.parser : term_parser :=
 node! explicit [
@@ -144,6 +177,59 @@ node! explicit [
   id: term.ident.parser
 ]
 
+@[derive parser.has_tokens parser.has_view]
+def from.parser : term_parser :=
+node! «from» ["from ", proof: term.parser]
+
+@[derive parser.has_tokens parser.has_view]
+def have.parser : term_parser :=
+node! «have» [
+  "have ",
+  id: (try node! have_id [id: ident.parser, " : "])?,
+  prop: term.parser,
+  proof: node_choice! have_proof {
+    term: node! have_term [" := ", term: term.parser],
+    «from»: node! have_from [", ", «from»: from.parser],
+  },
+  ", ",
+  body: term.parser,
+]
+
+@[derive parser.has_tokens parser.has_view]
+def show.parser : term_parser :=
+node! «show» [
+  "show ",
+  prop: term.parser,
+  ", ",
+  «from»: from.parser,
+]
+
+@[derive parser.has_tokens parser.has_view]
+def match.parser : term_parser :=
+node! «match» [
+  "match ",
+  scrutinees: sep_by1 term.parser (symbol ", ") ff,
+  type: node! match_type [" : ", type: term.parser]?,
+  " with ",
+  opt_bar: (symbol " | ")?,
+  equations: sep_by1
+    node! «match_equation» [
+      lhs: sep_by1 term.parser (symbol ", ") ff, ":=", rhs: term.parser]
+    (symbol " | ") ff,
+]
+
+@[derive parser.has_tokens parser.has_view]
+def if.parser : term_parser :=
+node! «if» [
+  "if ",
+  id: (try node! if_id [id: ident.parser, " : "])?,
+  prop: term.parser,
+  " then ",
+  then_branch: term.parser,
+  " else ",
+  else_branch: term.parser,
+]
+
 -- TODO(Sebastian): replace with attribute
 @[derive has_tokens]
 def builtin_leading_parsers : list term_parser := [
@@ -155,7 +241,12 @@ def builtin_leading_parsers : list term_parser := [
   lambda.parser,
   pi.parser,
   anonymous_constructor.parser,
-  explicit_ident.parser
+  explicit_ident.parser,
+  have.parser,
+  show.parser,
+  assume.parser,
+  match.parser,
+  if.parser
 ]
 
 @[derive parser.has_tokens parser.has_view]

library/init/lean/parser/token.lean

@@ -40,7 +40,7 @@ do r ← remaining,
 private def whitespace_aux : nat → basic_parser_m unit
 | (n+1) :=
 do whitespace,
-   str "--" *> take_while' (= '\n') *> whitespace_aux n <|>
+   str "--" *> take_while' (≠ '\n') *> whitespace_aux n <|>
    -- a "/--" doc comment is an actual token, not whitespace
    try (str "/-" *> not_followed_by (str "-")) *> finish_comment_block *> whitespace_aux n <|>
    pure ()
@@ -181,14 +181,14 @@ lift $ try $ do {
 } <?> repr sym
 
 instance symbol.tokens (sym lbp) : parser.has_tokens (symbol sym lbp : parser) :=
-⟨[⟨sym, lbp, none⟩]⟩
+⟨[⟨sym.trim, lbp, none⟩]⟩
 instance symbol.view (sym lbp) : parser.has_view (symbol sym lbp : parser) (option syntax_atom) :=
 { view := λ stx, match stx with
   | syntax.atom atom := some atom
   | _                := none,
   review := λ a, (syntax.atom <$> a).get_or_else syntax.missing }
 instance symbol.view_default (sym lbp) : parser.has_view_default (symbol sym lbp : parser) _
-  (some {info := none, val := sym}) := ⟨⟩
+  (some {info := none, val := sym.trim}) := ⟨⟩
 
 def number.parser : parser :=
 lift $ try $ do {

tests/lean/parser1.lean

@@ -87,9 +87,10 @@ universes u v
   pure cmd'.reprint
 
 -- slowly progressing...
+--set_option profiler true
 #eval (do {
   s ← io.fs.read_file "../../library/init/core.lean",
-  let s := (s.mk_iterator.nextn 7000).prev_to_string,
+  let s := (s.mk_iterator.nextn 50000).prev_to_string,
   parser_cfg ← monad_except.lift_except $ mk_config,
   let cfg : elaborator_config := {filename := "foo"},
   let st : elaborator_state := {parser_cfg := {..parser_cfg}},
@@ -112,13 +113,13 @@ universes u v
         --io.println cmd',
         match ((elaborate cmd').run cfg).run st with
         | except.ok ((), st) := pure (sum.inl (k, st, out :: outs))
-        | except.error e := throw e.text
+        | except.error e := io.println e.text *> pure (sum.inl (k, st, out :: outs))
       }
-      | except.error e := throw e.text
+      | except.error e := io.println e.text *> pure (sum.inl (k, st, out :: outs))
     },
-  check_reprint outs s,
+  check_reprint outs s/-,
   let stx := syntax.node ⟨none, outs.map (λ r, r.cmd)⟩,
   let stx := stx.update_leading s,
   io.println "result:",
-  io.println (to_string stx)
+  io.println (to_string stx)-/
 } : except_t string io unit)