feat: add builtin notation

src/Init/Core.lean

@@ -353,9 +353,6 @@ class HasEmptyc   (α : Type u) := (emptyc : α)
 class HasPow (α : Type u) (β : Type v) :=
 (pow : α → β → α)
 
-export HasAndthen (andthen)
-export HasPow (pow)
-
 infix `+`        := HasAdd.add
 infix `*`        := HasMul.mul
 infix `-`        := HasSub.sub
@@ -382,8 +379,6 @@ infix `↔`        := Iff
 infixr `<|>`     := HasOrelse.orelse
 infixr `>>`      := HasAndthen.andthen
 
-export HasAppend (append)
-
 @[reducible] def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop := HasLessEq.LessEq b a
 @[reducible] def Greater {α : Type u} [HasLess α] (a b : α) : Prop     := HasLess.Less b a
 

src/Init/Data/DList.lean

@@ -21,7 +21,7 @@ variables {α : Type u}
 open List
 
 def ofList (l : List α) : DList α :=
-⟨append l, fun t => (appendNil l).symm ▸ rfl⟩
+⟨HasAppend.append l, fun t => (appendNil l).symm ▸ rfl⟩
 
 def empty : DList α :=
 ⟨id, fun t => rfl⟩

src/Init/Lean/Elab.lean

@@ -10,3 +10,4 @@ import Init.Lean.Elab.ElabStrategyAttrs
 import Init.Lean.Elab.Command
 import Init.Lean.Elab.Term
 import Init.Lean.Elab.Frontend
+import Init.Lean.Elab.BuiltinNotation

src/Init/Lean/Elab/BuiltinNotation.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Elab.Term
+
+namespace Lean
+namespace Elab
+namespace Term
+
+@[builtinTermElab dollar] def elabDollar : TermElab :=
+fun stx expectedType? => do
+  -- term `$` term
+  let f := stx.getArg 0;
+  let a := stx.getArg 2;
+  elabTerm (mkAppStx f #[a]) expectedType?
+
+def elabInfix (f : Syntax) : TermElab :=
+fun stx expectedType? => do
+  -- term `op` term
+  let a := stx.getArg 0;
+  let b := stx.getArg 2;
+  elabTerm (mkAppStx f #[a, b]) expectedType?
+
+def elabInfixOp (op : Name) : TermElab :=
+fun stx expectedType? => elabInfix (mkTermId (stx.getArg 1) op) stx expectedType?
+
+@[builtinTermElab add] def elabAdd : TermElab := elabInfixOp `HasAdd.add
+@[builtinTermElab sub] def elabSub : TermElab := elabInfixOp `HasSub.sub
+@[builtinTermElab mul] def elabMul : TermElab := elabInfixOp `HasMul.mul
+@[builtinTermElab div] def elabDiv : TermElab := elabInfixOp `HasDiv.div
+@[builtinTermElab mod] def elabMod : TermElab := elabInfixOp `HasMod.mod
+@[builtinTermElab modN] def elabModN : TermElab := elabInfixOp `HasModN.modn
+@[builtinTermElab pow] def elabPow : TermElab := elabInfixOp `HasPow.pow
+
+@[builtinTermElab le] def elabLE : TermElab := elabInfixOp `HasLessEq.LessEq
+@[builtinTermElab ge] def elabGE : TermElab := elabInfixOp `GreaterEq
+@[builtinTermElab lt] def elabLT : TermElab := elabInfixOp `HasLess.Less
+@[builtinTermElab gt] def elabGT : TermElab := elabInfixOp `Greater
+@[builtinTermElab eq] def elabEq : TermElab := elabInfixOp `Eq
+@[builtinTermElab ne] def elabNe : TermElab := elabInfixOp `Ne
+@[builtinTermElab beq] def elabBEq : TermElab := elabInfixOp `HasBeq.beq
+@[builtinTermElab bne] def elabBNe : TermElab := elabInfixOp `bne
+@[builtinTermElab heq] def elabHEq : TermElab := elabInfixOp `HEq
+@[builtinTermElab equiv] def elabEquiv : TermElab := elabInfixOp `HasEquiv.Equiv
+
+@[builtinTermElab and] def elabAnd : TermElab := elabInfixOp `And
+@[builtinTermElab or] def elabOr : TermElab := elabInfixOp `Or
+@[builtinTermElab iff] def elabIff : TermElab := elabInfixOp `Iff
+
+@[builtinTermElab band] def elabBAnd : TermElab := elabInfixOp `and
+@[builtinTermElab bor] def elabBOr : TermElab := elabInfixOp `or
+
+@[builtinTermElab append] def elabAppend : TermElab := elabInfixOp `HasAppend.append
+@[builtinTermElab cons] def elabCons : TermElab := elabInfixOp `List.cons
+
+@[builtinTermElab andthen] def elabAndThen : TermElab := elabInfixOp `HasAndthen.andthen
+-- @[builtinTermElab bind] def elabBind : TermElab := elabInfixOp `HasBind.bind
+
+@[builtinTermElab seq] def elabseq : TermElab := elabInfixOp `HasSeq.seq
+@[builtinTermElab seqLeft] def elabseqLeft : TermElab := elabInfixOp `HasSeqLeft.seqLeft
+@[builtinTermElab seqRight] def elabseqRight : TermElab := elabInfixOp `HasSeqRight.seqRight
+
+@[builtinTermElab map] def elabMap : TermElab := elabInfixOp `Functor.map
+@[builtinTermElab mapRev] def elabMapRev : TermElab := elabInfixOp `Functor.mapRev
+@[builtinTermElab mapConst] def elabMapConst : TermElab := elabInfixOp `Functor.mapConst
+@[builtinTermElab mapConstRev] def elabMapConstRev : TermElab := elabInfixOp `Functor.mapConstRev
+
+@[builtinTermElab orelse] def elabOrElse : TermElab := elabInfixOp `HasOrelse.orelse
+@[builtinTermElab orM] def elabOrM : TermElab := elabInfixOp `orM
+@[builtinTermElab andM] def elabAndM : TermElab := elabInfixOp `andM
+
+/-
+@[builtinTermElab] def elabsubst : TermElab := elabInfixOp infixR " ▸ " 75
+-/
+
+end Term
+end Elab
+end Lean

src/Init/Lean/Elab/Term.lean

@@ -470,6 +470,9 @@ match expectedType? with
   condM (isDefEq eType expectedType)
     (pure e)
     (do -- TODO try `HasCoe`
+        e ← instantiateMVars e;
+        eType ← instantiateMVars eType;
+        expectedType ← instantiateMVars expectedType;
         let msg : MessageData :=
           "type mismatch" ++ indentExpr e
           ++ Format.line ++ "has type" ++ indentExpr eType
@@ -486,6 +489,7 @@ def synthesizeInstMVar (ref : Syntax) (instMVar : MVarId) : TermElabM Unit :=
 condM (isExprMVarAssigned instMVar) (pure ()) $ do
   instMVarDecl ← getMVarDecl instMVar;
   let type := instMVarDecl.type;
+  type ← instantiateMVars type;
   result ← trySynthInstance type;
   match result with
   | LOption.some val => assignExprMVar instMVar val
@@ -668,13 +672,6 @@ fun stx expectedType? => do
 @[builtinTermElab explicit] def elabExplicit : TermElab := elabApp
 @[builtinTermElab choice] def elabChoice : TermElab := elabApp
 
-@[builtinTermElab dollar] def elabDollar : TermElab :=
-fun stx expectedType? => do
-  -- term `$` term
-  let f := stx.getArg 0;
-  let a := stx.getArg 2;
-  elabTerm (mkAppStx f #[a]) expectedType?
-
 end Term
 
 @[init] private def regTraceClasses : IO Unit := do

tests/lean/run/frontend1.lean

@@ -22,6 +22,7 @@ def two := 2
 #eval run "#check [zero, one, two]"
 #eval run "#check id $ Nat.succ one"
 #eval run "#check HasAdd.add one two"
+#eval run "#check one + two > one ∧ True"
 
 #eval run
 "universe u universe v