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

feat(library/init/lean/elaborator/command): implement export command

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-24 14:55:27 -07:00
parent e0797bba14
commit 72ff4eb8e2
1 changed files with 19 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
library/init/lean/elaborator/command.lean
View file

@ -67,8 +67,25 @@ fun n => do
@[builtinCommandElab «export»] def elabExport : CommandElab :=
fun n => do
runIO (IO.println n.val);
pure ()
-- `n` is of the form (Command.export "export" <namespace> "(" (null <ids>*) ")")
let ns := (n.getArg 1).getIdentVal;
let ids := (n.getArg 3).getArgs;
ns ← resolveNamespace ns;
currNs ← getNamespace;
when (ns == currNs) $ throw "invalid 'export', self export";
s ← get;
let env := s.env;
aliases ← ids.mfoldl (fun (aliases : List (Name × Name)) (idStx : Syntax) => do {
let id := idStx.getIdentVal;
let declName := ns ++ id;
if env.contains declName then
pure $ (currNs ++ id, declName) :: aliases
else do
logError idStx ("unknown declaration '" ++ toString declName ++ "'");
pure aliases
})
[];
modify $ fun s => { env := aliases.foldl (fun env p => addAlias env p.1 p.2) s.env, .. s }
/- We just ignore Lean3 notation declaration commands. -/
@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()