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

chore: move to new frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-13 13:23:35 -07:00
parent 7e9052be24
commit d10b95d2ad
3 changed files with 93 additions and 99 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

78
src/Lean/Elab/Print.lean
View file

@ -5,39 +5,39 @@ Authors: Leonardo de Moura
-/
import Lean.Util.FoldConsts
import Lean.Elab.Command
new_frontend
namespace Lean
namespace Elab
namespace Command
private def throwUnknownId (id : Name) : CommandElabM Unit :=
throwError ("unknown identifier '" ++ toString id ++ "'")
throwError! "unknown identifier '{id}'"
private def lparamsToMessageData (lparams : List Name) : MessageData :=
match lparams with
| [] => ""
| u::us =>
let m : MessageData := ".{" ++ u;
let m := us.foldl (fun (s : MessageData) u => s ++ ", " ++ u) m;
m ++ "}"
| u::us => do
let m : MessageData := ".{" ++ u
for u in us do
m := m ++ ", " ++ u
return m ++ "}"
private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData := do
let m : MessageData := if isUnsafe then "unsafe " else "";
env ← getEnv;
let m := if isProtected env id then m ++ "protected " else m;
let m : MessageData := if isUnsafe then "unsafe " else ""
let m := if isProtected (← getEnv) id then m ++ "protected " else m
let (m, id) := match privateToUserName? id : _ → MessageData × Name with
| some id => (m ++ "private ", id)
| none => (m, id);
let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type;
| none => (m, id)
let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type
pure m
private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (isUnsafe := false) : CommandElabM Unit := do
m ← mkHeader kind id lparams type isUnsafe;
let m := m ++ " :=" ++ Format.line ++ value;
let m ← mkHeader kind id lparams type isUnsafe
let m := m ++ " :=" ++ Format.line ++ value
logInfo m
private def printAxiomLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
m ← mkHeader kind id lparams type isUnsafe;
let m ← mkHeader kind id lparams type isUnsafe
logInfo m
private def printQuot (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do
@ -45,19 +45,15 @@ printAxiomLike "Quotient primitive" id lparams type
private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr)
(ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
env ← getEnv;
m ← mkHeader "inductive" id lparams type isUnsafe;
let m := m ++ Format.line ++ "constructors:";
m ← ctors.foldlM
(fun (m : MessageData) ctor => do
cinfo ← getConstInfo ctor;
pure $ m ++ Format.line ++ ctor ++ " : " ++ cinfo.type)
m;
let m ← mkHeader "inductive" id lparams type isUnsafe
let m := m ++ Format.line ++ "constructors:"
for ctor in ctors do
let cinfo ← getConstInfo ctor
m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
logInfo m
private def printIdCore (id : Name) : CommandElabM Unit := do
env ← getEnv;
match env.find? id with
match (← getEnv).find? id with
| ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
| ConstantInfo.defnInfo { lparams := us, type := t, value := v, isUnsafe := u, .. } => printDefLike "def" id us t v u
| ConstantInfo.thmInfo { lparams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
@ -70,14 +66,14 @@ match env.find? id with
| none => throwUnknownId id
private def printId (id : Name) : CommandElabM Unit := do
cs ← resolveGlobalConst id;
let cs ← resolveGlobalConst id
cs.forM printIdCore
@[builtinCommandElab «print»] def elabPrint : CommandElab :=
fun stx =>
let numArgs := stx.getNumArgs;
let numArgs := stx.getNumArgs
if numArgs == 2 then
let arg := stx.getArg 1;
let arg := stx.getArg 1
if arg.isIdent then
printId arg.getId
else match arg.isStrLit? with
@ -89,18 +85,18 @@ fun stx =>
namespace CollectAxioms
structure State :=
(visited : NameSet := {})
(visited : NameSet := {})
(axioms : Array Name := #[])
abbrev M := ReaderT Environment $ StateM State
partial def collect : Name → M Unit
| c => do
let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM collect;
s ← get;
unless (s.visited.contains c) do
modify fun s => { s with visited := s.visited.insert c };
env ← read;
let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM collect
let s ← get
unless s.visited.contains c do
modify fun s => { s with visited := s.visited.insert c }
let env ← read
match env.find? c with
| some (ConstantInfo.axiomInfo _) => modify fun s => { s with axioms := s.axioms.push c }
| some (ConstantInfo.defnInfo v) => collectExpr v.type *> collectExpr v.value
@ -115,19 +111,17 @@ partial def collect : Name → M Unit
end CollectAxioms
private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
env ← getEnv;
let (_, s) := ((CollectAxioms.collect constName).run env).run {};
let env ← getEnv
let (_, s) := ((CollectAxioms.collect constName).run env).run {}
if s.axioms.isEmpty then
logInfo ("'" ++ constName ++ "' does not depend on any axioms")
logInfo msg!"'{constName}' does not depend on any axioms"
else
logInfo ("'" ++ constName ++ "' depends on axioms: " ++ toString s.axioms.toList)
logInfo msg!"'{constName}' depends on axioms: {s.axioms.toList}"
@[builtinCommandElab «printAxioms»] def elabPrintAxioms : CommandElab :=
fun stx => do
let id := (stx.getArg 2).getId;
cs ← resolveGlobalConst id;
let id := (stx.getArg 2).getId
let cs ← resolveGlobalConst id
cs.forM printAxiomsOf
end Command
end Elab
end Lean
end Lean.Elab.Command

14
src/Lean/Elab/StrategyAttrs.lean
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Attributes
new_frontend
namespace Lean
/-
@ -17,14 +18,11 @@ inductive ElaboratorStrategy
instance ElaboratorStrategy.inhabited : Inhabited ElaboratorStrategy :=
⟨ElaboratorStrategy.withExpectedType⟩
def mkElaboratorStrategyAttrs : IO (EnumAttributes ElaboratorStrategy) :=
registerEnumAttributes `elaboratorStrategy
[(`elabWithExpectedType, "instructs elaborator that the arguments of the function application (f ...) should be elaborated using information about the expected type", ElaboratorStrategy.withExpectedType),
(`elabSimple, "instructs elaborator that the arguments of the function application (f ...) should be elaborated from left to right, and without propagating information from the expected type to its arguments", ElaboratorStrategy.simple),
(`elabAsEliminator, "instructs elaborator that the arguments of the function application (f ...) should be elaborated as f were an eliminator", ElaboratorStrategy.asEliminator)]
@[init mkElaboratorStrategyAttrs]
constant elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy := arbitrary _
initialize elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy ←
registerEnumAttributes `elaboratorStrategy
[(`elabWithExpectedType, "instructs elaborator that the arguments of the function application (f ...) should be elaborated using information about the expected type", ElaboratorStrategy.withExpectedType),
(`elabSimple, "instructs elaborator that the arguments of the function application (f ...) should be elaborated from left to right, and without propagating information from the expected type to its arguments", ElaboratorStrategy.simple),
(`elabAsEliminator, "instructs elaborator that the arguments of the function application (f ...) should be elaborated as f were an eliminator", ElaboratorStrategy.asEliminator)]
@[export lean_get_elaborator_strategy]
def getElaboratorStrategy (env : Environment) (n : Name) : Option ElaboratorStrategy :=

100
src/Lean/Elab/Util.lean
View file

@ -7,6 +7,7 @@ import Lean.Util.Trace
import Lean.Parser.Extension
import Lean.KeyedDeclsAttribute
import Lean.Elab.Exception
new_frontend
namespace Lean
@ -16,12 +17,13 @@ match stx.unsetTrailing.reprint with -- TODO use syntax pretty printer
| none => format stx
def MacroScopesView.format (view : MacroScopesView) (mainModule : Name) : Format :=
format $
if view.scopes.isEmpty then view.name
fmt $
if view.scopes.isEmpty then
view.name
else if view.mainModule == mainModule then
view.scopes.foldl mkNameNum (view.name ++ view.imported)
view.scopes.foldl mkNameNum (view.name ++ view.imported)
else
view.scopes.foldl mkNameNum (view.name ++ view.imported ++ view.mainModule)
view.scopes.foldl mkNameNum (view.name ++ view.imported ++ view.mainModule)
namespace Elab
@ -35,51 +37,49 @@ def getBetterRef (ref : Syntax) (macroStack : MacroStack) : Syntax :=
match ref.getPos with
| some _ => ref
| none =>
match macroStack.find? $ fun (elem : MacroStackElem) => elem.before.getPos != none with
match macroStack.find? (·.before.getPos != none) with
| some elem => elem.before
| none => ref
def ppMacroStackDefault := false
@[init] def ppMacroStackOption : IO Unit :=
registerOption `pp.macroStack { defValue := ppMacroStackDefault, group := "pp", descr := "dispaly macro expansion stack" }
def getMacroStackOption (o : Options) : Bool:= o.get `pp.macroStack ppMacroStackDefault
def setMacroStackOption (o : Options) (flag : Bool) : Options := o.setBool `pp.macroStack flag
initialize
registerOption `pp.macroStack { defValue := ppMacroStackDefault, group := "pp", descr := "dispaly macro expansion stack" }
def addMacroStack {m} [Monad m] [MonadOptions m] (msgData : MessageData) (macroStack : MacroStack) : m MessageData := do
options ← getOptions;
if !getMacroStackOption options then pure msgData else
if !getMacroStackOption (← getOptions) then pure msgData else
match macroStack with
| [] => pure msgData
| stack@(top::_) =>
let msgData := msgData ++ Format.line ++ "with resulting expansion" ++ MessageData.nest 2 (Format.line ++ top.after);
let msgData := msgData ++ Format.line ++ "with resulting expansion" ++ MessageData.nest 2 (Format.line ++ top.after)
pure $ stack.foldl
(fun (msgData : MessageData) (elem : MacroStackElem) =>
msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ elem.before))
msgData
def checkSyntaxNodeKind (k : Name) : AttrM Name := do
env ← getEnv;
if Parser.isValidSyntaxNodeKind env k then pure k
if Parser.isValidSyntaxNodeKind (← getEnv) k then pure k
else throwError "failed"
namespace OldFrontend -- TODO: delete
private def checkSyntaxNodeKindAtNamespacesAux (k : Name) : List Name → AttrM Name
| [] => throwError "failed"
| n::ns => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux ns
| n::ns => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux k ns
def checkSyntaxNodeKindAtNamespaces (k : Name) : AttrM Name := do
env ← getEnv;
let env ← getEnv
checkSyntaxNodeKindAtNamespacesAux k (Lean.TODELETE.getNamespaces env)
end OldFrontend
def checkSyntaxNodeKindAtNamespacesAux (k : Name) : Name → AttrM Name
| n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux p
| n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux k p
| _ => throwError "failed"
def checkSyntaxNodeKindAtNamespaces (k : Name) : AttrM Name := do
ctx ← read;
let ctx ← read
checkSyntaxNodeKindAtNamespacesAux k ctx.currNamespace
def syntaxNodeKindOfAttrParam (defaultParserNamespace : Name) (arg : Syntax) : AttrM SyntaxNodeKind :=
@ -93,8 +93,8 @@ match attrParamSyntaxToIdentifier arg with
<|>
checkSyntaxNodeKind (defaultParserNamespace ++ k)
<|>
throwError ("invalid syntax node kind '" ++ toString k ++ "'")
| none => throwError ("syntax node kind is missing")
throwError! "invalid syntax node kind '{k}'"
| none => throwError "syntax node kind is missing"
private unsafe def evalSyntaxConstantUnsafe (env : Environment) (constName : Name) : ExceptT String Id Syntax :=
env.evalConstCheck Syntax `Lean.Syntax constName
@ -107,31 +107,34 @@ private constant evalConstant (γ : Type) (env : Environment) (typeName : Name)
unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (parserNamespace : Name) (typeName : Name) (kind : String)
: IO (KeyedDeclsAttribute γ) :=
KeyedDeclsAttribute.init {
builtinName := attrBuiltinName,
name := attrName,
descr := kind ++ " elaborator",
builtinName := attrBuiltinName,
name := attrName,
descr := kind ++ " elaborator",
valueTypeName := typeName,
evalKey := fun _ arg => syntaxNodeKindOfAttrParam parserNamespace arg,
evalKey := fun _ arg => syntaxNodeKindOfAttrParam parserNamespace arg,
} attrDeclName
unsafe def mkMacroAttribute : IO (KeyedDeclsAttribute Macro) :=
unsafe def mkMacroAttributeUnsafe : IO (KeyedDeclsAttribute Macro) :=
mkElabAttribute Macro `Lean.Elab.macroAttribute `builtinMacro `macro Name.anonymous `Lean.Macro "macro"
@[init mkMacroAttribute] constant macroAttribute : KeyedDeclsAttribute Macro := arbitrary _
@[implementedBy mkMacroAttributeUnsafe]
constant mkMacroAttribute : IO (KeyedDeclsAttribute Macro) := arbitrary _
initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute
private def expandMacroFns (stx : Syntax) : List Macro → MacroM Syntax
| [] => throw Macro.Exception.unsupportedSyntax
| m::ms =>
| m::ms => do
try
m stx
catch
(m stx)
(fun ex =>
match ex with
| Macro.Exception.unsupportedSyntax => expandMacroFns ms
| ex => throw ex)
| Macro.Exception.unsupportedSyntax => expandMacroFns stx ms
| ex => throw ex
def getMacros (env : Environment) : Macro :=
fun stx =>
let k := stx.getKind;
let table := (macroAttribute.ext.getState env).table;
let k := stx.getKind
let table := (macroAttribute.ext.getState env).table
match table.find? k with
| some macroFns => expandMacroFns stx macroFns
| none => throw Macro.Exception.unsupportedSyntax
@ -147,32 +150,31 @@ instance monadMacroAdapterTrans (m n) [MonadMacroAdapter m] [MonadLift m n] : Mo
setNextMacroScope := fun s => liftM (MonadMacroAdapter.setNextMacroScope s : m _) }
private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syntax) := do
try
let newStx ← getMacros env stx
pure (some newStx)
catch
(do newStx ← getMacros env stx; pure (some newStx))
(fun ex => match ex with
| Macro.Exception.unsupportedSyntax => pure none
| _ => throw ex)
| Macro.Exception.unsupportedSyntax => pure none
| ex => throw ex
@[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m]
[MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (x : MacroM α) : m α := do
scp ← MonadMacroAdapter.getCurrMacroScope;
env ← getEnv;
next ← MonadMacroAdapter.getNextMacroScope;
currRecDepth ← MonadRecDepth.getRecDepth;
maxRecDepth ← MonadRecDepth.getMaxRecDepth;
match x { macroEnv := Macro.mkMacroEnv (expandMacro? env),
currMacroScope := scp, mainModule := env.mainModule, currRecDepth := currRecDepth, maxRecDepth := maxRecDepth } next with
let env ← getEnv
match x { macroEnv := Macro.mkMacroEnv (expandMacro? env),
currMacroScope := ← MonadMacroAdapter.getCurrMacroScope,
mainModule := env.mainModule,
currRecDepth := ← MonadRecDepth.getRecDepth,
maxRecDepth := ← MonadRecDepth.getMaxRecDepth } (← MonadMacroAdapter.getNextMacroScope) with
| EStateM.Result.error Macro.Exception.unsupportedSyntax _ => throwUnsupportedSyntax
| EStateM.Result.error (Macro.Exception.error ref msg) _ => throwErrorAt ref msg
| EStateM.Result.ok a nextMacroScope => do MonadMacroAdapter.setNextMacroScope nextMacroScope; pure a
| EStateM.Result.ok a nextMacroScope => MonadMacroAdapter.setNextMacroScope nextMacroScope; pure a
@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m]
[MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (x : Macro) (stx : Syntax) : m Syntax :=
liftMacroM (x stx)
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab;
registerTraceClass `Elab.step
initialize
registerTraceClass `Elab
registerTraceClass `Elab.step
end Elab
end Lean
end Lean.Elab