max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: break Declaration.lean into smaller files

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-04 13:31:25 -08:00
parent 6ca9a8c170
commit 93dbcc161a
4 changed files with 245 additions and 159 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/Init/Lean/Elab/Command.lean
View file

@ -451,6 +451,31 @@ fun stx => do
logInfo stx.val (e ++ " : " ++ type);
pure ()
@[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"
end Command
end Elab
end Lean

131
src/Init/Lean/Elab/DeclModifiers.lean Normal file
View file

@ -0,0 +1,131 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Init.Lean.Elab.Command
namespace Lean
namespace Elab
namespace Command
inductive AttributeArg
| str (val : String)
| num (val : Nat)
| id (val : Name)
instance AttributeArg.hasToString : HasToString AttributeArg :=
⟨fun arg => match arg with
| AttributeArg.str v => repr v
| AttributeArg.num v => toString v
| AttributeArg.id v => toString v⟩
structure Attribute :=
(name : Name) (args : Array AttributeArg := #[])
instance Attribute.hasFormat : HasFormat Attribute :=
⟨fun attr => Format.bracket "@[" (toString attr.name ++ (Format.prefixJoin " " attr.args.toList)) "]"⟩
inductive Visibility
| regular | «protected» | «private»
instance Visibility.hasToString : HasToString Visibility :=
⟨fun v => match v with
| Visibility.regular => "regular"
| Visibility.private => "private"
| Visibility.protected => "protected"⟩
structure Modifiers :=
(docString : Option String := none)
(visibility : Visibility := Visibility.regular)
(isNoncomputable : Bool := false)
(isPartial : Bool := false)
(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 :=
(match m.docString with
| some str => ["/--" ++ str ++ "-/"]
| none => [])
++ (match m.visibility with
| Visibility.regular => []
| Visibility.protected => ["protected"]
| Visibility.private => ["private"])
++ (if m.isNoncomputable then ["noncomputable"] else [])
++ (if m.isPartial then ["partial"] else [])
++ (if m.isUnsafe then ["unsafe"] else [])
++ m.attrs.toList.map (fun attr => fmt attr);
Format.bracket "{" (Format.joinSep components ("," ++ Format.line)) "}"⟩
instance Modifiers.hasToString : HasToString Modifiers := ⟨toString ∘ format⟩
def elabAttrArg (stx : Syntax) : CommandElabM AttributeArg := do
match stx.isStrLit? with
| some v => pure $ AttributeArg.str v
| _ =>
match stx.isNatLit? with
| some v => pure $ AttributeArg.num v
| _ =>
match stx with
| Syntax.ident _ _ v _ => pure $ AttributeArg.id v
| _ => throwError stx "unexpected attribute argument"
def elabAttr (stx : Syntax) : CommandElabM Attribute := do
-- rawIdent >> many attrArg
let nameStx := stx.getArg 0;
attrName ← match nameStx.isIdOrAtom? with
| none => throwError nameStx "identifier expected"
| some str => pure $ mkNameSimple str;
unlessM (liftIO stx (isAttribute attrName)) $
throwError stx ("unknown attribute [" ++ attrName ++ "]");
let argStxs := (stx.getArg 1).getArgs;
args ← argStxs.mapM elabAttrArg;
pure { name := attrName, args := args }
def elabAttrs (stx : Syntax) : CommandElabM (Array Attribute) :=
(stx.getArg 1).foldSepArgsM
(fun stx attrs => do
attr ← elabAttr stx;
pure $ attrs.push attr)
#[]
def elabModifiers (stx : Syntax) : CommandElabM Modifiers := do
let docCommentStx := stx.getArg 0;
let attrsStx := stx.getArg 1;
let visibilityStx := stx.getArg 2;
let noncompStx := stx.getArg 3;
let unsafeStx := stx.getArg 4;
let partialStx := stx.getArg 5;
docString ← match docCommentStx.getOptional? with
| none => pure none
| some s => match s.getArg 1 with
| Syntax.atom _ val => pure (some (val.extract 0 (val.bsize - 2)))
| _ => throwError s ("unexpected doc string " ++ toString (s.getArg 1));
visibility ← match visibilityStx.getOptional? with
| none => pure Visibility.regular
| some v =>
let kind := v.getKind;
if kind == `Lean.Parser.Command.private then pure Visibility.private
else if kind == `Lean.Parser.Command.protected then pure Visibility.protected
else throwError v "unexpected visibility modifier";
attrs ← match attrsStx.getOptional? with
| none => pure #[]
| some attrs => elabAttrs attrs;
pure {
docString := docString,
visibility := visibility,
isPartial := !partialStx.isNone,
isUnsafe := !unsafeStx.isNone,
isNoncomputable := !noncompStx.isNone,
attrs := attrs
}
end Command
end Elab
end Lean

190
src/Init/Lean/Elab/Declaration.lean
View file

@ -4,163 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Init.Lean.Elab.Command
import Init.Lean.Elab.Definition
namespace Lean
namespace Elab
namespace Command
inductive AttributeArg
| str (val : String)
| num (val : Nat)
| id (val : Name)
instance AttributeArg.hasToString : HasToString AttributeArg :=
⟨fun arg => match arg with
| AttributeArg.str v => repr v
| AttributeArg.num v => toString v
| AttributeArg.id v => toString v⟩
structure Attribute :=
(name : Name) (args : Array AttributeArg := #[])
instance Attribute.hasFormat : HasFormat Attribute :=
⟨fun attr => Format.bracket "@[" (toString attr.name ++ (Format.prefixJoin " " attr.args.toList)) "]"⟩
inductive Visibility
| regular | «protected» | «private»
instance Visibility.hasToString : HasToString Visibility :=
⟨fun v => match v with
| Visibility.regular => "regular"
| Visibility.private => "private"
| Visibility.protected => "protected"⟩
structure Modifiers :=
(docString : Option String := none)
(visibility : Visibility := Visibility.regular)
(isNoncomputable : Bool := false)
(isPartial : Bool := false)
(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 :=
(match m.docString with
| some str => ["/--" ++ str ++ "-/"]
| none => [])
++ (match m.visibility with
| Visibility.regular => []
| Visibility.protected => ["protected"]
| Visibility.private => ["private"])
++ (if m.isNoncomputable then ["noncomputable"] else [])
++ (if m.isPartial then ["partial"] else [])
++ (if m.isUnsafe then ["unsafe"] else [])
++ m.attrs.toList.map (fun attr => fmt attr);
Format.bracket "{" (Format.joinSep components ("," ++ Format.line)) "}"⟩
instance Modifiers.hasToString : HasToString Modifiers := ⟨toString ∘ format⟩
def elabAttrArg (stx : Syntax) : CommandElabM AttributeArg := do
match stx.isStrLit? with
| some v => pure $ AttributeArg.str v
| _ =>
match stx.isNatLit? with
| some v => pure $ AttributeArg.num v
| _ =>
match stx with
| Syntax.ident _ _ v _ => pure $ AttributeArg.id v
| _ => throwError stx "unexpected attribute argument"
def elabAttr (stx : Syntax) : CommandElabM Attribute := do
-- rawIdent >> many attrArg
let nameStx := stx.getArg 0;
attrName ← match nameStx.isIdOrAtom? with
| none => throwError nameStx "identifier expected"
| some str => pure $ mkNameSimple str;
unlessM (liftIO stx (isAttribute attrName)) $
throwError stx ("unknown attribute [" ++ attrName ++ "]");
let argStxs := (stx.getArg 1).getArgs;
args ← argStxs.mapM elabAttrArg;
pure { name := attrName, args := args }
def elabAttrs (stx : Syntax) : CommandElabM (Array Attribute) :=
(stx.getArg 1).foldSepArgsM
(fun stx attrs => do
attr ← elabAttr stx;
pure $ attrs.push attr)
#[]
def elabModifiers (stx : Syntax) : CommandElabM Modifiers := do
let docCommentStx := stx.getArg 0;
let attrsStx := stx.getArg 1;
let visibilityStx := stx.getArg 2;
let noncompStx := stx.getArg 3;
let unsafeStx := stx.getArg 4;
let partialStx := stx.getArg 5;
docString ← match docCommentStx.getOptional? with
| none => pure none
| some s => match s.getArg 1 with
| Syntax.atom _ val => pure (some (val.extract 0 (val.bsize - 2)))
| _ => throwError s ("unexpected doc string " ++ toString (s.getArg 1));
visibility ← match visibilityStx.getOptional? with
| none => pure Visibility.regular
| some v =>
let kind := v.getKind;
if kind == `Lean.Parser.Command.private then pure Visibility.private
else if kind == `Lean.Parser.Command.protected then pure Visibility.protected
else throwError v "unexpected visibility modifier";
attrs ← match attrsStx.getOptional? with
| none => pure #[]
| some attrs => elabAttrs attrs;
pure {
docString := docString,
visibility := visibility,
isPartial := !partialStx.isNone,
isUnsafe := !unsafeStx.isNone,
isNoncomputable := !noncompStx.isNone,
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;
@ -182,22 +31,35 @@ def elabAbbrev (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
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))
elabDefCore {
ref := stx, kind := DefKind.def, modifiers := modifiers,
declId := stx.getArg 1, binders := binders, type := type, val := 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))
elabDefCore {
ref := stx, kind := DefKind.def, modifiers := modifiers,
declId := stx.getArg 1, binders := binders, type := type,
val := 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))
elabDefCore {
ref := stx, kind := DefKind.theorem, modifiers := modifiers,
declId := stx.getArg 1, binders := binders, type := some type, val := 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?
elabDefCore {
ref := stx, kind := DefKind.opaque, modifiers := modifiers,
declId := stx.getArg 1, binders := binders, type := some type, val := (stx.getArg 3).getOptional?
}
def elabInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-- parser! "instance " >> optional declId >> declSig >> declVal
@ -206,19 +68,29 @@ 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))
elabDefCore {
ref := stx, kind := DefKind.def, modifiers := modifiers,
declId := declId, binders := binders, type := type, val := (stx.getArg 3).getOptional?
}
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
elabDefCore {
ref := stx, kind := DefKind.axiom, modifiers := modifiers,
declId := stx.getArg 1, binders := binders, type := some type, val := 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))
elabDefCore {
ref := stx, kind := DefKind.example, modifiers := modifiers,
declId := declId, binders := binders, type := some type,
val := some (stx.getArg 2)
}
def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
pure () -- TODO

58
src/Init/Lean/Elab/Definition.lean Normal file
View file

@ -0,0 +1,58 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Init.Lean.Elab.DeclModifiers
namespace Lean
namespace Elab
namespace Command
inductive DefKind
| «def» | «theorem» | «example» | «opaque» | «axiom»
structure DefViewCore :=
(kind : DefKind)
(ref : Syntax)
(modifiers : Modifiers)
(declId : Syntax)
(binders : Syntax)
(type : Option Syntax := none)
(val : Option Syntax := none)
structure DefView extends DefViewCore :=
(currNamespace : Name)
(name : Name)
(univNames : List Name)
(vars : Array Expr)
end Command
namespace Term
def elabDefTypeVal (view : Command.DefView) : TermElabM (Expr × Option Expr) := do
dbgTrace (toString view.currNamespace ++ " " ++ toString view.name ++ " " ++ toString view.univNames);
pure (arbitrary _, none)
end Term
namespace Command
def elabDefCore (view : DefViewCore) : CommandElabM Unit :=
withDeclId view.declId $ fun name univNames => do
currNamespace ← getCurrNamespace;
runTermElabM $ fun vars => do
(type, val?) ← Term.elabDefTypeVal {
currNamespace := currNamespace,
name := name,
univNames := univNames,
vars := vars,
.. view };
pure ()
end Command
end Elab
end Lean