feat: def-like elaboration skeleton

src/Init/Lean/Elab/Command.lean

@@ -194,24 +194,25 @@ modify $ fun s => {
   scopes := { kind := kind, header := header, currNamespace := newNamespace, .. s.scopes.head! } :: s.scopes,
   .. s }
 
-private def addScopes (kind : String) (updateNamespace : Bool) : Name → CommandElabM Unit
+private def addScopes (ref : Syntax) (kind : String) (updateNamespace : Bool) : Name → CommandElabM Unit
 | Name.anonymous => pure ()
 | Name.str p header _ => do
   addScopes p;
   currNamespace ← getCurrNamespace;
   addScope kind header (if updateNamespace then currNamespace ++ header else currNamespace)
-| _ => unreachable!
+| _ => throwError ref "invalid scope"
+
+private def addNamespace (ref : Syntax) (header : Name) : CommandElabM Unit :=
+addScopes ref "namespace" true header
 
 @[builtinCommandElab «namespace»] def elabNamespace : CommandElab :=
-fun n => do
-  let header := n.getIdAt 1;
-  addScopes "namespace" true header
+fun stx => addNamespace stx.val (stx.getIdAt 1)
 
 @[builtinCommandElab «section»] def elabSection : CommandElab :=
-fun n => do
-  let header? := (n.getArg 1).getOptionalIdent?;
+fun stx => do
+  let header? := (stx.getArg 1).getOptionalIdent?;
   match header? with
-  | some header => addScopes "section" false header
+  | some header => addScopes stx.val "section" false header
   | none        => do currNamespace ← getCurrNamespace; addScope "section" "" currNamespace
 
 def getScopes : CommandElabM (List Scope) := do
@@ -244,6 +245,12 @@ fun n => do
   | none        => unless (checkAnonymousScope scopes) $ throwError n.val "invalid 'end', name is missing"
   | some header => unless (checkEndHeader header scopes) $ throwError n.val "invalid 'end', name mismatch"
 
+@[inline] def withNamespace {α} (ref : Syntax) (ns : Name) (elab : CommandElabM α) : CommandElabM α := do
+addNamespace ref ns;
+a ← elab;
+modify $ fun s => { scopes := s.scopes.drop ns.getNumParts, .. s };
+pure a
+
 @[specialize] def modifyScope (f : Scope → Scope) : CommandElabM Unit :=
 modify $ fun s =>
   { scopes := match s.scopes with
@@ -254,11 +261,14 @@ modify $ fun s =>
 def getUniverseNames : CommandElabM (List Name) := do
 scope ← getScope; pure scope.univNames
 
+def throwAlreadyDeclaredUniverse {α} (ref : Syntax) (u : Name) : CommandElabM α :=
+throwError ref ("a universe named '" ++ toString u ++ "' has already been declared")
+
 def addUniverse (idStx : Syntax) : CommandElabM Unit := do
 let id := idStx.getId;
 univs ← getUniverseNames;
 if univs.elem id then
-  throwError idStx ("a universe named '" ++ toString id ++ "' has already been declared in this Scope")
+  throwAlreadyDeclaredUniverse idStx id
 else
   modifyScope $ fun scope => { univNames := id :: scope.univNames, .. scope }
 

src/Init/Lean/Elab/Declaration.lean

@@ -22,7 +22,7 @@ instance AttributeArg.hasToString : HasToString AttributeArg :=
  | AttributeArg.id v  => toString v⟩
 
 structure Attribute :=
-(name : Name) (args : Array AttributeArg)
+(name : Name) (args : Array AttributeArg := #[])
 
 instance Attribute.hasFormat : HasFormat Attribute :=
 ⟨fun attr => Format.bracket "@[" (toString attr.name ++ (Format.prefixJoin " " attr.args.toList)) "]"⟩
@@ -44,6 +44,9 @@ structure Modifiers :=
 (isUnsafe        : Bool := false)
 (attrs           : Array Attribute := #[])
 
+def Modifiers.addAttribute (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
+{ attrs := modifiers.attrs.push attr, .. modifiers }
+
 instance Modifiers.hasFormat : HasFormat Modifiers :=
 ⟨fun m =>
   let components : List Format :=
@@ -123,11 +126,137 @@ pure {
   attrs           := attrs
 }
 
+inductive DefKind
+| «def» | «theorem» | «example» | «opaque» | «axiom»
+
+@[inline] def withDeclId (declId : Syntax) (f : Name → List Name → CommandElabM Unit) : CommandElabM Unit := do
+-- ident >> optional (".{" >> sepBy1 ident ", " >> "}")
+let id             := declId.getIdAt 0;
+let optUnivDeclStx := declId.getArg 1;
+us ←
+  if optUnivDeclStx.isNone then
+    getUniverseNames
+  else do {
+    univs ← getUniverseNames;
+    let univIds := (optUnivDeclStx.getArg 1).getArgs.getEvenElems;
+    univIds.foldlM
+      (fun univs idStx =>
+        let id := idStx.getId;
+        if univs.elem id then
+          throwAlreadyDeclaredUniverse idStx id
+        else
+          pure (id :: univs))
+      univs
+  };
+let us  := us.reverse;
+let ref := declId;
+match id with
+| Name.str pre s _ => withNamespace ref pre (f (mkNameSimple s) us)
+| _                => throwError ref "invalid declaration name"
+
+def elabDefCore (ref : Syntax) (kind : DefKind) (modifiers : Modifiers)
+    (declId : Syntax) (binders : Syntax) (type : Option Syntax) (val : Option Syntax) : CommandElabM Unit :=
+withDeclId declId $ fun id us => do
+  ns ← getCurrNamespace;
+  dbgTrace (">> " ++ toString ns ++ " " ++ toString id ++ " " ++ toString us);
+  pure () -- TODO
+
+def expandOptDeclSig (stx : Syntax) : Syntax × Option Syntax :=
+-- many Term.bracktedBinder >> Term.optType
+let binders := stx.getArg 0;
+let optType := stx.getArg 1; -- optional (parser! " : " >> termParser)
+if optType.isNone then
+  (binders, none)
+else
+  let typeSpec := optType.getArg 0;
+  (binders, some $ typeSpec.getArg 1)
+
+def expandDeclSig (stx : Syntax) : Syntax × Syntax :=
+-- many Term.bracktedBinder >> Term.typeSpec
+let binders := stx.getArg 0;
+let typeSpec := stx.getArg 1;
+(binders, typeSpec.getArg 1)
+
+def elabAbbrev (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "abbrev " >> declId >> optDeclSig >> declVal
+let (binders, type) := expandOptDeclSig (stx.getArg 2);
+let modifiers       := modifiers.addAttribute { name := `inline };
+let modifiers       := modifiers.addAttribute { name := `reducible };
+elabDefCore stx DefKind.def modifiers (stx.getArg 1) binders type (some (stx.getArg 3))
+
+def elabDef (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "def " >> declId >> optDeclSig >> declVal
+let (binders, type) := expandOptDeclSig (stx.getArg 2);
+elabDefCore stx DefKind.def modifiers (stx.getArg 1) binders type (some (stx.getArg 3))
+
+def elabTheorem (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "theorem " >> declId >> declSig >> declVal
+let (binders, type) := expandDeclSig (stx.getArg 2);
+elabDefCore stx DefKind.theorem modifiers (stx.getArg 1) binders (some type) (some (stx.getArg 3))
+
+def elabConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "constant " >> declId >> declSig >> optional declValSimple
+let (binders, type) := expandDeclSig (stx.getArg 2);
+elabDefCore stx DefKind.opaque modifiers (stx.getArg 1) binders (some type) (stx.getArg 3).getOptional?
+
+def elabInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+-- parser! "instance " >> optional declId >> declSig >> declVal
+let (binders, type) := expandDeclSig (stx.getArg 2);
+let modifiers       := modifiers.addAttribute { name := `instance };
+declId ← match (stx.getArg 1).getOptional? with
+  | some declId => pure declId
+  | none        => throwError stx "not implemented yet";
+elabDefCore stx DefKind.def modifiers declId binders type (some (stx.getArg 3))
+
+def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "axiom " >> declId >> declSig
+let (binders, type) := expandDeclSig (stx.getArg 2);
+elabDefCore stx DefKind.axiom modifiers (stx.getArg 1) binders (some type) none
+
+def elabExample (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+-- parser! "example " >> declSig >> declVal
+let (binders, type) := expandDeclSig (stx.getArg 1);
+let id              := mkIdentFrom stx `_example;
+let declId          := Syntax.node `Lean.Parser.Command.declId #[id, mkNullNode];
+elabDefCore stx DefKind.example modifiers declId binders (some type) (some (stx.getArg 2))
+
+def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+pure () -- TODO
+
+def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+pure () -- TODO
+
+def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
+pure () -- TODO
+
 @[builtinCommandElab declaration]
 def elabDeclaration : CommandElab :=
 fun stx => do
   modifiers ← elabModifiers (stx.getArg 0);
-  throwError stx.val ("wip, modifiers: " ++ toString modifiers)
+  let decl     := stx.getArg 1;
+  let declKind := decl.getKind;
+  if declKind == `Lean.Parser.Command.abbrev then
+    elabAbbrev modifiers decl
+  else if declKind == `Lean.Parser.Command.def then
+    elabDef modifiers decl
+  else if declKind == `Lean.Parser.Command.theorem then
+    elabTheorem modifiers decl
+  else if declKind == `Lean.Parser.Command.constant then
+    elabConstant modifiers decl
+  else if declKind == `Lean.Parser.Command.instance then
+    elabInstance modifiers decl
+  else if declKind == `Lean.Parser.Command.axiom then
+    elabAxiom modifiers decl
+  else if declKind == `Lean.Parser.Command.example then
+    elabExample modifiers decl
+  else if declKind == `Lean.Parser.Command.inductive then
+    elabInductive modifiers decl
+  else if declKind == `Lean.Parser.Command.classInductive then
+    elabClassInductive modifiers decl
+  else if declKind == `Lean.Parser.Command.structure then
+    elabStructure modifiers decl
+  else
+    throwError stx.val "unexpected declaration"
 
 end Command
 end Elab