chore: move to new frontend
This commit is contained in:
Leonardo de Moura
parent
d3a22397b4
commit
b7658ef91f
3 changed files with 160 additions and 174 deletions
|
|
@ -4,28 +4,27 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura, Sebastian Ullrich
|
||||
-/
|
||||
import Lean.Meta.ExprDefEq
|
||||
|
||||
namespace Lean
|
||||
namespace Meta
|
||||
new_frontend
|
||||
namespace Lean.Meta
|
||||
|
||||
def forallTelescopeCompatibleAux {α} (k : Array Expr → Expr → Expr → MetaM α) : Nat → Expr → Expr → Array Expr → MetaM α
|
||||
| 0, type₁, type₂, xs => k xs type₁ type₂
|
||||
| i+1, type₁, type₂, xs => do
|
||||
type₁ ← whnf type₁;
|
||||
type₂ ← whnf type₂;
|
||||
let type₁ ← whnf type₁
|
||||
let type₂ ← whnf type₂
|
||||
match type₁, type₂ with
|
||||
| Expr.forallE n₁ d₁ b₁ c₁, Expr.forallE n₂ d₂ b₂ c₂ => do
|
||||
unless (n₁ == n₂) $
|
||||
throwError ("parameter name mismatch '" ++ n₁ ++ "', expected '" ++ n₂ ++ "'");
|
||||
unlessM (isDefEq d₁ d₂) $
|
||||
throwError ("type mismatch at parameter '" ++ n₁ ++ "'" ++ indentExpr d₁ ++ Format.line ++ "expected type" ++ indentExpr d₂);
|
||||
unless (c₁.binderInfo == c₂.binderInfo) $
|
||||
throwError ("binder annotation mismatch at parameter '" ++ n₁ ++ "'");
|
||||
| Expr.forallE n₁ d₁ b₁ c₁, Expr.forallE n₂ d₂ b₂ c₂ =>
|
||||
unless n₁ == n₂ do
|
||||
throwError! "parameter name mismatch '{n₁}', expected '{n₂}'"
|
||||
unless (← isDefEq d₁ d₂) do
|
||||
throwError! "type mismatch at parameter '{n₁}'{indentExpr d₁}\nexpected type{indentExpr d₂}"
|
||||
unless c₁.binderInfo == c₂.binderInfo do
|
||||
throwError! "binder annotation mismatch at parameter '{n₁}'"
|
||||
withLocalDecl n₁ c₁.binderInfo d₁ fun x =>
|
||||
let type₁ := b₁.instantiate1 x;
|
||||
let type₂ := b₂.instantiate1 x;
|
||||
forallTelescopeCompatibleAux i type₁ type₂ (xs.push x)
|
||||
| _, _ => throwError ("unexpected number of parameters")
|
||||
let type₁ := b₁.instantiate1 x
|
||||
let type₂ := b₂.instantiate1 x
|
||||
forallTelescopeCompatibleAux k i type₁ type₂ (xs.push x)
|
||||
| _, _ => throwError "unexpected number of parameters"
|
||||
|
||||
/-- Given two forall-expressions `type₁` and `type₂`, ensure the first `numParams` parameters are compatible, and
|
||||
then execute `k` with the parameters and remaining types. -/
|
||||
|
|
@ -38,19 +37,19 @@ namespace Elab
|
|||
|
||||
def expandOptDeclSig (stx : Syntax) : Syntax × Option Syntax :=
|
||||
-- many Term.bracketedBinder >> Term.optType
|
||||
let binders := stx.getArg 0;
|
||||
let optType := stx.getArg 1; -- optional (parser! " : " >> termParser)
|
||||
let binders := stx[0]
|
||||
let optType := stx[1] -- optional (parser! " : " >> termParser)
|
||||
if optType.isNone then
|
||||
(binders, none)
|
||||
else
|
||||
let typeSpec := optType.getArg 0;
|
||||
(binders, some $ typeSpec.getArg 1)
|
||||
let typeSpec := optType[0]
|
||||
(binders, some typeSpec[1])
|
||||
|
||||
def expandDeclSig (stx : Syntax) : Syntax × Syntax :=
|
||||
-- many Term.bracketedBinder >> Term.typeSpec
|
||||
let binders := stx.getArg 0;
|
||||
let typeSpec := stx.getArg 1;
|
||||
(binders, typeSpec.getArg 1)
|
||||
let binders := stx[0]
|
||||
let typeSpec := stx[1]
|
||||
(binders, typeSpec[1])
|
||||
|
||||
def mkFreshInstanceName (env : Environment) (nextIdx : Nat) : Name :=
|
||||
(env.mainModule ++ `_instance).appendIndexAfter nextIdx
|
||||
|
|
@ -73,11 +72,11 @@ match name with
|
|||
Remark: `explicitParams` are in reverse declaration order. That is, the head is the last declared parameter. -/
|
||||
def sortDeclLevelParams (scopeParams : List Name) (allUserParams : List Name) (usedParams : Array Name) : Except String (List Name) :=
|
||||
match allUserParams.find? $ fun u => !usedParams.contains u && !scopeParams.elem u with
|
||||
| some u => throw ("unused universe parameter '" ++ toString u ++ "'")
|
||||
| some u => throw s!"unused universe parameter '{u}'"
|
||||
| none =>
|
||||
let result := allUserParams.foldl (fun result levelName => if usedParams.elem levelName then levelName :: result else result) [];
|
||||
let remaining := usedParams.filter (fun levelParam => !allUserParams.elem levelParam);
|
||||
let remaining := remaining.qsort Name.lt;
|
||||
let result := allUserParams.foldl (fun result levelName => if usedParams.elem levelName then levelName :: result else result) []
|
||||
let remaining := usedParams.filter (fun levelParam => !allUserParams.elem levelParam)
|
||||
let remaining := remaining.qsort Name.lt
|
||||
pure $ result ++ remaining.toList
|
||||
|
||||
end Elab
|
||||
|
|
|
|||
|
|
@ -9,21 +9,19 @@ import Lean.Elab.DefView
|
|||
import Lean.Elab.Inductive
|
||||
import Lean.Elab.Structure
|
||||
import Lean.Elab.MutualDef
|
||||
|
||||
namespace Lean
|
||||
namespace Elab
|
||||
namespace Command
|
||||
new_frontend
|
||||
namespace Lean.Elab.Command
|
||||
|
||||
open Meta
|
||||
|
||||
/- Auxiliary function for `expandDeclNamespace?` -/
|
||||
def expandDeclIdNamespace? (declId : Syntax) : Option (Name × Syntax) :=
|
||||
let (id, optUnivDeclStx) := expandDeclIdCore declId;
|
||||
let scpView := extractMacroScopes id;
|
||||
let (id, optUnivDeclStx) := expandDeclIdCore declId
|
||||
let scpView := extractMacroScopes id
|
||||
match scpView.name with
|
||||
| Name.str Name.anonymous s _ => none
|
||||
| Name.str pre s _ =>
|
||||
let nameNew := { scpView with name := mkNameSimple s }.review;
|
||||
let nameNew := { scpView with name := mkNameSimple s }.review
|
||||
if declId.isIdent then
|
||||
some (pre, mkIdentFrom declId nameNew)
|
||||
else
|
||||
|
|
@ -34,8 +32,8 @@ match scpView.name with
|
|||
def expandDeclNamespace? (stx : Syntax) : Option (Name × Syntax) :=
|
||||
if !stx.isOfKind `Lean.Parser.Command.declaration then none
|
||||
else
|
||||
let decl := stx.getArg 1;
|
||||
let k := decl.getKind;
|
||||
let decl := stx[1]
|
||||
let k := decl.getKind
|
||||
if k == `Lean.Parser.Command.abbrev ||
|
||||
k == `Lean.Parser.Command.def ||
|
||||
k == `Lean.Parser.Command.theorem ||
|
||||
|
|
@ -43,17 +41,17 @@ else
|
|||
k == `Lean.Parser.Command.axiom ||
|
||||
k == `Lean.Parser.Command.inductive ||
|
||||
k == `Lean.Parser.Command.structure then
|
||||
match expandDeclIdNamespace? (decl.getArg 1) with
|
||||
match expandDeclIdNamespace? decl[1] with
|
||||
| some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 1 declId))
|
||||
| none => none
|
||||
else if k == `Lean.Parser.Command.instance then
|
||||
let optDeclId := decl.getArg 1;
|
||||
let optDeclId := decl[1]
|
||||
if optDeclId.isNone then none
|
||||
else match expandDeclIdNamespace? (optDeclId.getArg 0) with
|
||||
else match expandDeclIdNamespace? optDeclId[0] with
|
||||
| some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 1 (optDeclId.setArg 0 declId)))
|
||||
| none => none
|
||||
else if k == `Lean.Parser.Command.classInductive then
|
||||
match expandDeclIdNamespace? (decl.getArg 2) with
|
||||
match expandDeclIdNamespace? decl[2] with
|
||||
| some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 2 declId))
|
||||
| none => none
|
||||
else
|
||||
|
|
@ -61,31 +59,31 @@ else
|
|||
|
||||
def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
|
||||
-- parser! "axiom " >> declId >> declSig
|
||||
let declId := stx.getArg 1;
|
||||
let (binders, typeStx) := expandDeclSig (stx.getArg 2);
|
||||
scopeLevelNames ← getLevelNames;
|
||||
⟨name, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers;
|
||||
runTermElabM declName $ fun vars => Term.withLevelNames allUserLevelNames $ Term.elabBinders binders.getArgs fun xs => do
|
||||
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration;
|
||||
type ← Term.elabType typeStx;
|
||||
Term.synthesizeSyntheticMVarsNoPostponing;
|
||||
type ← instantiateMVars type;
|
||||
type ← mkForallFVars xs type;
|
||||
(type, _) ← mkForallUsedOnly vars type;
|
||||
(type, _) ← Term.levelMVarToParam type;
|
||||
let usedParams := (collectLevelParams {} type).params;
|
||||
let declId := stx[1]
|
||||
let (binders, typeStx) := expandDeclSig stx[2]
|
||||
let scopeLevelNames ← getLevelNames
|
||||
let ⟨name, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
|
||||
runTermElabM declName fun vars => Term.withLevelNames allUserLevelNames $ Term.elabBinders binders.getArgs fun xs => do
|
||||
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
|
||||
let type ← Term.elabType typeStx
|
||||
Term.synthesizeSyntheticMVarsNoPostponing
|
||||
let type ← instantiateMVars type
|
||||
let type ← mkForallFVars xs type
|
||||
let (type, _) ← mkForallUsedOnly vars type
|
||||
let (type, _) ← Term.levelMVarToParam type
|
||||
let usedParams := collectLevelParams {} type $.params
|
||||
match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with
|
||||
| Except.error msg => throwErrorAt stx msg
|
||||
| Except.ok levelParams => do
|
||||
| Except.ok levelParams =>
|
||||
let decl := Declaration.axiomDecl {
|
||||
name := declName,
|
||||
lparams := levelParams,
|
||||
type := type,
|
||||
isUnsafe := modifiers.isUnsafe
|
||||
};
|
||||
Term.ensureNoUnassignedMVars decl;
|
||||
addDecl decl;
|
||||
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
}
|
||||
Term.ensureNoUnassignedMVars decl
|
||||
addDecl decl
|
||||
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterTypeChecking
|
||||
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
|
||||
|
||||
/-
|
||||
|
|
@ -95,25 +93,24 @@ parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
|
|||
Remark: numTokens == 1 for regular `inductive` and 2 for `class inductive`.
|
||||
-/
|
||||
private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (numTokens := 1) : CommandElabM InductiveView := do
|
||||
checkValidInductiveModifier modifiers;
|
||||
let (binders, type?) := expandOptDeclSig (decl.getArg (numTokens + 1));
|
||||
let declId := decl.getArg numTokens;
|
||||
⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers;
|
||||
ctors ← (decl.getArg (numTokens + 2)).getArgs.mapM fun ctor => withRef ctor do {
|
||||
checkValidInductiveModifier modifiers
|
||||
let (binders, type?) := expandOptDeclSig decl[numTokens + 1]
|
||||
let declId := decl[numTokens]
|
||||
let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
|
||||
let ctors ← decl[numTokens + 2].getArgs.mapM fun ctor => withRef ctor do
|
||||
-- def ctor := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
|
||||
ctorModifiers ← elabModifiers (ctor.getArg 1);
|
||||
when (ctorModifiers.isPrivate && modifiers.isPrivate) $
|
||||
throwError "invalid 'private' constructor in a 'private' inductive datatype";
|
||||
when (ctorModifiers.isProtected && modifiers.isPrivate) $
|
||||
throwError "invalid 'protected' constructor in a 'private' inductive datatype";
|
||||
checkValidCtorModifier ctorModifiers;
|
||||
let ctorName := ctor.getIdAt 2;
|
||||
let ctorName := declName ++ ctorName;
|
||||
ctorName ← withRef (ctor.getArg 2) $ applyVisibility ctorModifiers.visibility ctorName;
|
||||
let inferMod := !(ctor.getArg 3).isNone;
|
||||
let (binders, type?) := expandOptDeclSig (ctor.getArg 4);
|
||||
let ctorModifiers ← elabModifiers ctor[1]
|
||||
if ctorModifiers.isPrivate && modifiers.isPrivate then
|
||||
throwError "invalid 'private' constructor in a 'private' inductive datatype"
|
||||
if ctorModifiers.isProtected && modifiers.isPrivate then
|
||||
throwError "invalid 'protected' constructor in a 'private' inductive datatype"
|
||||
checkValidCtorModifier ctorModifiers
|
||||
let ctorName := ctor.getIdAt 2
|
||||
let ctorName := declName ++ ctorName
|
||||
let ctorName ← withRef ctor[2] $ applyVisibility ctorModifiers.visibility ctorName
|
||||
let inferMod := !ctor[3].isNone
|
||||
let (binders, type?) := expandOptDeclSig ctor[4]
|
||||
pure { ref := ctor, modifiers := ctorModifiers, declName := ctorName, inferMod := inferMod, binders := binders, type? := type? : CtorView }
|
||||
};
|
||||
pure {
|
||||
ref := decl,
|
||||
modifiers := modifiers,
|
||||
|
|
@ -129,60 +126,59 @@ private def classInductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) :
|
|||
inductiveSyntaxToView modifiers decl 2
|
||||
|
||||
def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
|
||||
v ← inductiveSyntaxToView modifiers stx;
|
||||
let v ← inductiveSyntaxToView modifiers stx
|
||||
elabInductiveViews #[v]
|
||||
|
||||
def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
|
||||
let modifiers := modifiers.addAttribute { name := `class };
|
||||
v ← classInductiveSyntaxToView modifiers stx;
|
||||
let modifiers := modifiers.addAttribute { name := `class }
|
||||
let v ← classInductiveSyntaxToView modifiers stx
|
||||
elabInductiveViews #[v]
|
||||
|
||||
@[builtinCommandElab declaration]
|
||||
def elabDeclaration : CommandElab :=
|
||||
fun stx => match expandDeclNamespace? stx with
|
||||
| some (ns, newStx) => do
|
||||
let ns := mkIdentFrom stx ns;
|
||||
newStx ← `(namespace $ns:ident $newStx end $ns:ident);
|
||||
let ns := mkIdentFrom stx ns
|
||||
let newStx ← `(namespace $ns:ident $newStx end $ns:ident)
|
||||
withMacroExpansion stx newStx $ elabCommand newStx
|
||||
| none => do
|
||||
modifiers ← elabModifiers (stx.getArg 0);
|
||||
let decl := stx.getArg 1;
|
||||
let declKind := decl.getKind;
|
||||
if declKind == `Lean.Parser.Command.axiom then
|
||||
let modifiers ← elabModifiers stx[0]
|
||||
let decl := stx[1]
|
||||
let declKind := decl.getKind
|
||||
if declKind == `Lean.Parser.Command.«axiom» then
|
||||
elabAxiom modifiers decl
|
||||
else if declKind == `Lean.Parser.Command.inductive then
|
||||
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
|
||||
else if declKind == `Lean.Parser.Command.«structure» then
|
||||
elabStructure modifiers decl
|
||||
else if isDefLike decl then do
|
||||
else if isDefLike decl then
|
||||
elabMutualDef #[stx]
|
||||
else
|
||||
throwError "unexpected declaration"
|
||||
|
||||
/- Return true if all elements of the mutual-block are inductive declarations. -/
|
||||
private def isMutualInductive (stx : Syntax) : Bool :=
|
||||
(stx.getArg 1).getArgs.all $ fun elem =>
|
||||
let decl := elem.getArg 1;
|
||||
let declKind := decl.getKind;
|
||||
stx[1].getArgs.all fun elem =>
|
||||
let decl := elem[1]
|
||||
let declKind := decl.getKind
|
||||
declKind == `Lean.Parser.Command.inductive
|
||||
|
||||
private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
|
||||
views ← elems.mapM $ fun stx => do {
|
||||
modifiers ← elabModifiers (stx.getArg 0);
|
||||
inductiveSyntaxToView modifiers (stx.getArg 1)
|
||||
};
|
||||
let views ← elems.mapM fun stx => do
|
||||
let modifiers ← elabModifiers stx[0]
|
||||
inductiveSyntaxToView modifiers stx[1]
|
||||
elabInductiveViews views
|
||||
|
||||
/- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/
|
||||
private def isMutualDef (stx : Syntax) : Bool :=
|
||||
(stx.getArg 1).getArgs.all $ fun elem =>
|
||||
let decl := elem.getArg 1;
|
||||
stx[1].getArgs.all fun elem =>
|
||||
let decl := elem[1]
|
||||
isDefLike decl
|
||||
|
||||
private def isMutualPreambleCommand (stx : Syntax) : Bool :=
|
||||
let k := stx.getKind;
|
||||
let k := stx.getKind
|
||||
k == `Lean.Parser.Command.variable ||
|
||||
k == `Lean.Parser.Command.variables ||
|
||||
k == `Lean.Parser.Command.universe ||
|
||||
|
|
@ -191,53 +187,48 @@ k == `Lean.Parser.Command.check ||
|
|||
k == `Lean.Parser.Command.set_option ||
|
||||
k == `Lean.Parser.Command.open
|
||||
|
||||
private partial def splitMutualPreamble (elems : Array Syntax) : Nat → Option (Array Syntax × Array Syntax)
|
||||
| i =>
|
||||
private partial def splitMutualPreamble (elems : Array Syntax) : Option (Array Syntax × Array Syntax) :=
|
||||
let rec loop (i : Nat) : Option (Array Syntax × Array Syntax) :=
|
||||
if h : i < elems.size then
|
||||
let elem := elems.get ⟨i, h⟩;
|
||||
let elem := elems.get ⟨i, h⟩
|
||||
if isMutualPreambleCommand elem then
|
||||
splitMutualPreamble (i+1)
|
||||
loop (i+1)
|
||||
else if i == 0 then
|
||||
none -- `mutual` block does not contain any preamble commands
|
||||
else
|
||||
some (elems.extract 0 i, elems.extract i elems.size)
|
||||
some (elems[0:i], elems[i:elems.size])
|
||||
else
|
||||
none -- a `mutual` block containing only preamble commands is not a valid `mutual` block
|
||||
loop 0
|
||||
|
||||
@[builtinMacro Lean.Parser.Command.mutual] def expandMutualNamespace : Macro :=
|
||||
fun stx => do
|
||||
let elems := (stx.getArg 1).getArgs;
|
||||
(ns?, elems) ← elems.foldlM
|
||||
(fun (acc : Option Name × Array Syntax) (elem : Syntax) =>
|
||||
let (ns?, elems) := acc;
|
||||
match ns?, expandDeclNamespace? elem with
|
||||
| _, none => pure (ns?, elems.push elem)
|
||||
| none, some (ns, elem) => pure (some ns, elems.push elem)
|
||||
| some nsCurr, some (nsNew, elem) =>
|
||||
if nsCurr == nsNew then
|
||||
pure (ns?, elems.push elem)
|
||||
else
|
||||
Macro.throwError elem
|
||||
("conflicting namespaces in mutual declaration, using namespace '" ++ toString nsNew ++ "', but used '" ++ toString nsCurr ++ "' in previous declaration"))
|
||||
(none, #[]);
|
||||
let ns? := none
|
||||
let elemsNew := #[]
|
||||
for elem in stx[1].getArgs do
|
||||
match ns?, expandDeclNamespace? elem with
|
||||
| _, none => elemsNew := elemsNew.push elem
|
||||
| none, some (ns, elem) => ns? := some ns; elemsNew := elemsNew.push elem
|
||||
| some nsCurr, some (nsNew, elem) =>
|
||||
if nsCurr == nsNew then
|
||||
elemsNew := elemsNew.push elem
|
||||
else
|
||||
Macro.throwError elem s!"conflicting namespaces in mutual declaration, using namespace '{nsNew}', but used '{nsCurr}' in previous declaration"
|
||||
match ns? with
|
||||
| some ns =>
|
||||
let ns := mkIdentFrom stx ns;
|
||||
let stxNew := stx.setArg 1 (mkNullNode elems);
|
||||
let ns := mkIdentFrom stx ns
|
||||
let stxNew := stx.setArg 1 (mkNullNode elemsNew)
|
||||
`(namespace $ns:ident $stxNew end $ns:ident)
|
||||
| none => Macro.throwUnsupported
|
||||
|
||||
@[builtinMacro Lean.Parser.Command.mutual] def expandMutualElement : Macro :=
|
||||
fun stx => do
|
||||
let elems := (stx.getArg 1).getArgs;
|
||||
(elemsNew, modified) ← elems.foldlM
|
||||
(fun (acc : Array Syntax × Bool) elem => do
|
||||
let (elemsNew, modified) := acc;
|
||||
elem? ← expandMacro? elem;
|
||||
match elem? with
|
||||
| some elemNew => pure (elemsNew.push elemNew, true)
|
||||
| none => pure (elemsNew.push elem, modified))
|
||||
(#[], false);
|
||||
let elemsNew := #[]
|
||||
let modified := false
|
||||
for elem in stx[1].getArgs do
|
||||
match (← expandMacro? elem) with
|
||||
| some elemNew => elemsNew := elemsNew.push elemNew; modified := true
|
||||
| none => elemsNew := elemsNew.push elem
|
||||
if modified then
|
||||
pure $ stx.setArg 1 (mkNullNode elemsNew)
|
||||
else
|
||||
|
|
@ -245,45 +236,44 @@ fun stx => do
|
|||
|
||||
@[builtinMacro Lean.Parser.Command.mutual] def expandMutualPreamble : Macro :=
|
||||
fun stx =>
|
||||
match splitMutualPreamble (stx.getArg 1).getArgs 0 with
|
||||
match splitMutualPreamble stx[1].getArgs with
|
||||
| none => Macro.throwUnsupported
|
||||
| some (preamble, rest) => do
|
||||
secCmd ← `(section);
|
||||
let newMutual := stx.setArg 1 (mkNullNode rest);
|
||||
endCmd ← `(end);
|
||||
let secCmd ← `(section)
|
||||
let newMutual := stx.setArg 1 (mkNullNode rest)
|
||||
let endCmd ← `(end)
|
||||
pure $ mkNullNode (#[secCmd] ++ preamble ++ #[newMutual] ++ #[endCmd])
|
||||
|
||||
@[builtinCommandElab «mutual»]
|
||||
def elabMutual : CommandElab :=
|
||||
fun stx => do
|
||||
if isMutualInductive stx then
|
||||
elabMutualInductive (stx.getArg 1).getArgs
|
||||
elabMutualInductive stx[1].getArgs
|
||||
else if isMutualDef stx then
|
||||
elabMutualDef (stx.getArg 1).getArgs
|
||||
elabMutualDef stx[1].getArgs
|
||||
else
|
||||
throwError "invalid mutual block"
|
||||
|
||||
/- parser! optional "local " >> "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "]" >> many1 ident -/
|
||||
@[builtinCommandElab «attribute»] def elabAttr : CommandElab :=
|
||||
fun stx => do
|
||||
let persistent := (stx.getArg 0).isNone;
|
||||
attrs ← elabAttrs (stx.getArg 3);
|
||||
let idents := (stx.getArg 5).getArgs;
|
||||
idents.forM fun ident => withRef ident $ liftTermElabM none do
|
||||
declName ← resolveGlobalConstNoOverload ident.getId;
|
||||
let persistent := stx[0].isNone
|
||||
let attrs ← elabAttrs stx[3]
|
||||
let idents := stx[5].getArgs
|
||||
for ident in idents do withRef ident $ liftTermElabM none do
|
||||
let declName ← resolveGlobalConstNoOverload ident.getId
|
||||
Term.applyAttributes declName attrs persistent
|
||||
|
||||
@[builtinMacro Lean.Parser.Command.«initialize»] def expandInitialize : Macro :=
|
||||
fun stx =>
|
||||
let optHeader := stx.getArg 1;
|
||||
let doSeq := stx.getArg 2;
|
||||
let optHeader := stx[1]
|
||||
let doSeq := stx[2]
|
||||
if optHeader.isNone then
|
||||
`(@[init]def initFn : IO Unit := do $doSeq)
|
||||
else
|
||||
let id := optHeader.getArg 0;
|
||||
let type := (optHeader.getArg 1).getArg 1;
|
||||
`(def initFn : IO $type := do $doSeq @[init initFn]constant $id : $type)
|
||||
let id := optHeader[0]
|
||||
let type := optHeader[1][1]
|
||||
`(def initFn : IO $type := do $doSeq
|
||||
@[init initFn]constant $id : $type)
|
||||
|
||||
end Command
|
||||
end Elab
|
||||
end Lean
|
||||
end Lean.Elab.Command
|
||||
|
|
|
|||
|
|
@ -4,47 +4,44 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura, Sebastian Ullrich
|
||||
-/
|
||||
import Lean.Parser.Module
|
||||
|
||||
namespace Lean
|
||||
namespace Elab
|
||||
new_frontend
|
||||
namespace Lean.Elab
|
||||
|
||||
def headerToImports (header : Syntax) : List Import :=
|
||||
let header := header.asNode;
|
||||
let imports := if (header.getArg 0).isNone then [{ module := `Init : Import }] else [];
|
||||
imports ++ (header.getArg 1).getArgs.toList.map (fun stx =>
|
||||
let imports := if header[0].isNone then [{ module := `Init : Import }] else []
|
||||
imports ++ header[1].getArgs.toList.map fun stx =>
|
||||
-- `stx` is of the form `(Module.import "import" "runtime"? id)
|
||||
let runtime := !(stx.getArg 1).isNone;
|
||||
let id := stx.getIdAt 2;
|
||||
{ module := id, runtimeOnly := runtime })
|
||||
let runtime := !stx[1].isNone
|
||||
let id := stx[2].getId
|
||||
{ module := id, runtimeOnly := runtime }
|
||||
|
||||
def processHeader (header : Syntax) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) :=
|
||||
catch
|
||||
(do env ← importModules (headerToImports header) trustLevel;
|
||||
pure (env, messages))
|
||||
(fun e => do
|
||||
env ← mkEmptyEnvironment;
|
||||
let spos := header.getPos.getD 0;
|
||||
let pos := inputCtx.fileMap.toPosition spos;
|
||||
pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos }))
|
||||
def processHeader (header : Syntax) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) := do
|
||||
try
|
||||
let env ← importModules (headerToImports header) trustLevel
|
||||
pure (env, messages)
|
||||
catch e =>
|
||||
let env ← mkEmptyEnvironment
|
||||
let spos := header.getPos.getD 0
|
||||
let pos := inputCtx.fileMap.toPosition spos
|
||||
pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
|
||||
|
||||
def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) := do
|
||||
env ← mkEmptyEnvironment;
|
||||
let fileName := fileName.getD "<input>";
|
||||
let inputCtx := Parser.mkInputContext input fileName;
|
||||
let env ← mkEmptyEnvironment
|
||||
let fileName := fileName.getD "<input>"
|
||||
let inputCtx := Parser.mkInputContext input fileName
|
||||
match Parser.parseHeader env inputCtx with
|
||||
| (header, parserState, messages) => do
|
||||
| (header, parserState, messages) =>
|
||||
pure (headerToImports header, inputCtx.fileMap.toPosition parserState.pos, messages)
|
||||
|
||||
@[export lean_parse_imports]
|
||||
def parseImportsExport (input : String) (fileName : Option String) : IO (List Import × Position × List Message) := do
|
||||
(imports, pos, log) ← parseImports input fileName;
|
||||
let (imports, pos, log) ← parseImports input fileName
|
||||
pure (imports, pos, log.toList)
|
||||
|
||||
@[export lean_print_deps]
|
||||
def printDeps (deps : List Import) : IO Unit :=
|
||||
deps.forM $ fun dep => do
|
||||
fname ← findOLean dep.module;
|
||||
def printDeps (deps : List Import) : IO Unit := do
|
||||
for dep in deps do
|
||||
let fname ← findOLean dep.module;
|
||||
IO.println fname
|
||||
|
||||
end Elab
|
||||
end Lean
|
||||
end Lean.Elab
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue