From eb9d793e79e694674e8b704f6a163c4fc2feacf6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 4 Jan 2020 08:48:00 -0800 Subject: [PATCH] feat: def-like elaboration skeleton --- src/Init/Lean/Elab/Command.lean | 28 ++++-- src/Init/Lean/Elab/Declaration.lean | 133 +++++++++++++++++++++++++++- 2 files changed, 150 insertions(+), 11 deletions(-) diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean index 613441b5bc..fb7ee559c2 100644 --- a/src/Init/Lean/Elab/Command.lean +++ b/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 } diff --git a/src/Init/Lean/Elab/Declaration.lean b/src/Init/Lean/Elab/Declaration.lean index bc61bed227..e699646ec1 100644 --- a/src/Init/Lean/Elab/Declaration.lean +++ b/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