feat(library/init/lean/elaborator): convertForall skeleton

library/init/lean/elaborator/basic.lean

@@ -39,6 +39,7 @@ structure ElabScope :=
 (univs       : List Name := [])
 (lctx        : LocalContext := {})
 (nextInstIdx : Nat := 1)
+(inPattern   : Bool := false)
 
 namespace ElabScope
 
@@ -432,6 +433,9 @@ modifyGet $ fun s =>
     (a, { scopes := h :: t, .. s })
   | _ => (default _, s)
 
+def localContext : Elab LocalContext :=
+do scope ← getScope; pure scope.lctx
+
 def mkLocalDecl (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : Elab LocalDecl :=
 do
 idx ← mkFreshName;
@@ -439,6 +443,12 @@ modifyGetScope $ fun scope =>
    let (decl, lctx) := scope.lctx.mkLocalDecl idx userName type bi;
    (decl, { lctx := lctx, .. scope })
 
+def mkLambda (xs : Array Expr) (b : Expr) : Elab Expr :=
+do lctx ← localContext; pure $ lctx.mkLambda xs b
+
+def mkForall (xs : Array Expr) (b : Expr) : Elab Expr :=
+do lctx ← localContext; pure $ lctx.mkForall xs b
+
 def anonymousInstNamePrefix := `_inst
 
 def mkAnonymousInstName : Elab Name :=
@@ -489,6 +499,14 @@ a ← x;
 modify $ fun s => { scopes := s.scopes.tail, .. s};
 pure a
 
+@[inline] def withInPattern {α} (x : Elab α) : Elab α :=
+withNewScope $ do
+  modifyScope $ fun scope => { inPattern := true, .. scope };
+  x
+
+def inPattern : Elab Bool :=
+do scope ← getScope; pure $ scope.inPattern
+
 /- Remark: in an ideal world where performance doesn't matter, we would define `Elab` as
    ```
    ExceptT ElabException (StateT ElabException IO)

library/init/lean/elaborator/preterm.lean

@@ -56,6 +56,9 @@ private def dummy : Expr := Expr.const `Prop []
 def mkAsIs (e : Expr) : PreTerm :=
 e.mkAnnotation `as_is
 
+def mkAsPattern (id : Name) (e : PreTerm) : PreTerm :=
+(Expr.app (Expr.fvar id) e).mkAnnotation `as_pattern
+
 def mkPreTypeAscription (p : PreTerm) (expectedType : Expr) : PreTerm :=
 Expr.app (Expr.app (Expr.const `typedExpr []) expectedType) p
 
@@ -138,23 +141,38 @@ fun n => do
 private def mkLocal (decl : LocalDecl) : PreTerm :=
 Expr.local decl.name decl.userName decl.type decl.binderInfo
 
-private def processBinder (b : Syntax Expr) : Elab (List PreTerm) :=
+private def processBinder (b : Syntax Expr) : Elab (Array PreTerm) :=
 match b.getKind with
 | `Lean.Parser.Term.simpleBinder   => do
    let args := (b.getArg 0).getArgs;
-   args.mfoldl (fun r arg => do
+   args.mmap $ fun arg => do
      let id := arg.getId;
      hole ← mkHoleFor arg;
      decl ← mkLocalDecl id hole;
-     pure (mkLocal decl :: r))
-     []
-| `Lean.Parser.Term.explicitBinder => do runIO (IO.println $ ">> explicit " ++ (toString b)); pure []
-| `Lean.Parser.Term.implicitBinder => do runIO (IO.println $ ">> implict " ++ (toString b)); pure []
-| `Lean.Parser.Term.instBinder     => do runIO (IO.println $ ">> inst " ++ (toString b)); pure []
+     pure (mkLocal decl)
+| `Lean.Parser.Term.explicitBinder =>
+   let ids     := (b.getArg 1).getArgs;
+   let optType := b.getArg 2;
+   let optDef  := b.getArg 3;
+   ids.mmap $ fun idStx => do
+     let id := idStx.getId;
+     type ← if optType.getNumArgs == 0 then mkHoleFor idStx else toPreTerm (optType.getArg 1);
+     type ← if optDef.getNumArgs == 0 then pure type else
+       let defInfo := optDef.getArg 0;
+       match defInfo.getKind with
+       | `Lean.Parser.Term.binderDefault => do
+          defVal ← toPreTerm (defInfo.getArg 1);
+          pure $ Expr.app (Expr.app (Expr.const `optParam []) type) defVal
+       | `Lean.Parser.Term.binderTactic => logErrorAndThrow optDef "old elaborator does not support tactics in parameters"
+       | _ => throw "unknown binder default value annotation";
+     decl ← mkLocalDecl id type;
+     pure (mkLocal decl)
+| `Lean.Parser.Term.implicitBinder => do runIO (IO.println $ ">> implict " ++ (toString b)); pure Array.empty
+| `Lean.Parser.Term.instBinder     => do runIO (IO.println $ ">> inst " ++ (toString b)); pure Array.empty
 | _ => throw "unknown binder kind"
 
-private def processBinders (bs : Array (Syntax Expr)) : Elab (List PreTerm) :=
-bs.mfoldl (fun r s => do xs ← processBinder s; pure (r ++ xs)) []
+private def processBinders (bs : Array (Syntax Expr)) : Elab (Array PreTerm) :=
+bs.mfoldl (fun r s => do xs ← processBinder s; pure (r ++ xs)) Array.empty
 
 @[builtinPreTermElab «forall»] def convertForall : PreTermElab :=
 fun n => do
@@ -162,21 +180,8 @@ fun n => do
   let body    := n.getArg 3;
   withNewScope $ do
     xs   ← processBinders binders.getArgs;
-    runIO (IO.println (xs.map Expr.dbgToString));
     body ← toPreTerm body;
-    -- TODO
-    pure $ Expr.sort (Level.zero)
---  dom ← toPreTerm $ n.getArg 0;
---  rng ← toPreTerm $ n.getArg 2;
---  pure $ Expr.pi id BinderInfo.default dom rng
-
--- TODO: delete... arrow should be expanded at term.lean
-@[builtinPreTermElab «arrow»] def convertArrow : PreTermElab :=
-fun n => do
-  id ← mkFreshName;
-  dom ← toPreTerm $ n.getArg 0;
-  rng ← toPreTerm $ n.getArg 2;
-  pure $ Expr.pi id BinderInfo.default dom rng
+    mkForall xs body
 
 @[builtinPreTermElab «hole»] def convertHole : PreTermElab :=
 fun _ => pure $ Expr.mvar Name.anonymous
@@ -184,6 +189,17 @@ fun _ => pure $ Expr.mvar Name.anonymous
 @[builtinPreTermElab «sorry»] def convertSorry : PreTermElab :=
 fun _ => pure $ Expr.app (Expr.const `sorryAx []) (Expr.mvar Name.anonymous)
 
+@[builtinPreTermElab «id»] def convertId : PreTermElab :=
+fun n => do
+  let id := n.getIdAt 0;
+  -- TODO add support for `explicitUniv` and `namedPattern`
+  lctx ← localContext;
+  match lctx.findFromUserName id with
+  | some decl => pure $ mkLocal decl
+  | none =>
+    -- TODO global name resolution
+    logErrorAndThrow n.val ("unknown identifier '" ++ toString id ++ "'")
+
 def oldElaborate (stx : Syntax Expr) (expectedType : Option Expr := none) : Elab Expr :=
 do
   p ← toPreTerm stx;

library/init/lean/elaborator/term.lean

@@ -49,15 +49,20 @@ fun stx _ => do
   let openBkt  := stx.getArg 0;
   let args     := stx.getArg 1;
   let closeBkt := stx.getArg 2;
-  let consId   := openBkt.mkIdent `List.cons;
-  let nilId    := closeBkt.mkIdent `List.nil;
+  let consId   := mkIdentFrom openBkt `List.cons;
+  let nilId    := mkIdentFrom closeBkt `List.nil;
   pure $ args.foldSepArgs (fun arg r => mkAppStx consId [arg, r]) nilId
 
+def mkExplicitBinder {α} (n : Syntax α) (type : Syntax α) : Syntax α :=
+mkNode `Lean.Parser.Term.explicitBinder [mkAtom "(", mkNullNode [n], mkNullNode [mkAtom ":", type], mkNullNode [], mkAtom ")"]
+
 @[builtinTermElab arrow] def elabArrow : TermElab :=
 fun stx _ => do
-  id ← mkFreshName;
-  runIO (IO.println stx.val);
-  pure $ Syntax.other $ Expr.sort (Level.zero)
+  n ← mkFreshName;
+  let id  := mkIdentFrom stx.val n;
+  let dom := stx.getArg 0;
+  let rng := stx.getArg 2;
+  pure $ mkNode `Lean.Parser.Term.forall [mkAtom "forall", mkNullNode [mkExplicitBinder id dom], mkAtom ",", rng]
 
 end Elab
 end Lean

library/init/lean/syntax.lean

@@ -329,7 +329,7 @@ end SyntaxNode
 /- Helper functions for creating Syntax objects using C++ -/
 
 @[export lean_mk_syntax_atom]
-def mkSimpleAtom (val : String) : Syntax :=
+def mkSimpleAtomCore (val : String) : Syntax :=
 Syntax.atom none val
 
 @[export lean_mk_syntax_ident]
@@ -340,6 +340,20 @@ Syntax.ident none (toString val).toSubstring val []
 def mkListNode (args : Array Syntax) : Syntax :=
 Syntax.node nullKind args
 
+def mkAtom {α} (val : String) : Syntax α :=
+Syntax.atom none val
+
+@[inline] def mkNode {α} (k : SyntaxNodeKind) (args : List (Syntax α)) : Syntax α :=
+Syntax.node k args.toArray
+
+@[inline] def mkNullNode {α} (args : List (Syntax α)) : Syntax α :=
+Syntax.node nullKind args.toArray
+
+def mkOptionalNode {α} (arg : Option (Syntax α)) : Syntax α :=
+match arg with
+| some arg => Syntax.node nullKind (Array.singleton arg)
+| none     => Syntax.node nullKind Array.empty
+
 /- Helper functions for creating string and numeric literals -/
 
 def mkLit (kind : SyntaxNodeKind) (val : String) (info : Option SourceInfo := none) : Syntax :=
@@ -457,10 +471,15 @@ match stx.isNatLit with
 | some val => val
 | none     => 0
 
+end Syntax
+
 /-- Create an identifier using `SourceInfo` from `src` -/
-def mkIdent {α} (src : Syntax α) (val : Name) : Syntax α :=
+def mkIdentFrom {α} (src : Syntax α) (val : Name) : Syntax α :=
 let info := src.getHeadInfo;
 Syntax.ident info (toString val).toSubstring val []
 
-end Syntax
+def mkAtomFrom {α} (src : Syntax α) (val : String) : Syntax α :=
+let info := src.getHeadInfo;
+Syntax.atom info val
+
 end Lean