feat(library/init/lean): use Environment in the new frontend

library/init/lean/declaration.lean

@@ -26,11 +26,11 @@ other regular definitions used in a definition. When creating declarations using
 we can specify the definitional depth manually.
 
 Remark: the hint only affects performance. None of the hints prevent the kernel from unfolding a
-Declaration during Type checking.
+declaration during Type checking.
 
 Remark: the ReducibilityHints are not related to the attributes: reducible/irrelevance/semireducible.
 These attributes are used by the Elaborator. The ReducibilityHints are used by the kernel (and Elaborator).
-Moreover, the ReducibilityHints cannot be changed after a Declaration is added to the kernel. -/
+Moreover, the ReducibilityHints cannot be changed after a declaration is added to the kernel. -/
 inductive ReducibilityHints
 | opaque   : ReducibilityHints
 | «abbrev» : ReducibilityHints
@@ -49,7 +49,7 @@ structure DefinitionVal extends ConstantVal :=
 structure TheoremVal extends ConstantVal :=
 (value : Task Expr)
 
-/- Value for an opaque constant Declaration `constant x : t := e` -/
+/- Value for an opaque constant declaration `constant x : t := e` -/
 structure OpaqueVal extends ConstantVal :=
 (value : Expr)
 
@@ -82,7 +82,7 @@ inductive Declaration
 structure InductiveVal extends ConstantVal :=
 (nparams : Nat)       -- Number of parameters
 (nindices : Nat)      -- Number of indices
-(all : List Name)     -- List of all (including this one) inductive datatypes in the mutual Declaration containing this one
+(all : List Name)     -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
 (ctors : List Name)   -- List of all constructors for this inductive datatype
 (isRec : Bool)        -- `true` Iff it is recursive
 (isUnsafe : Bool)
@@ -90,7 +90,7 @@ structure InductiveVal extends ConstantVal :=
 
 structure ConstructorVal extends ConstantVal :=
 (induct  : Name)  -- Inductive Type this Constructor is a member of
-(cidx    : Nat)   -- Constructor index (i.e., Position in the inductive Declaration)
+(cidx    : Nat)   -- Constructor index (i.e., Position in the inductive declaration)
 (nparams : Nat)   -- Number of parameters in inductive datatype `induct`
 (nfields : Nat)   -- Number of fields (i.e., arity - nparams)
 (isUnsafe : Bool)
@@ -102,7 +102,7 @@ structure RecursorRule :=
 (rhs : Expr)    -- Right hand side of the reduction rule
 
 structure RecursorVal extends ConstantVal :=
-(all : List Name)            -- List of all inductive datatypes in the mutual Declaration that generated this recursor
+(all : List Name)            -- List of all inductive datatypes in the mutual declaration that generated this recursor
 (nparams : Nat)              -- Number of parameters
 (nindices : Nat)             -- Number of indices
 (nmotives : Nat)             -- Number of motives

library/init/lean/elaborator.lean

@@ -10,13 +10,9 @@ import init.lean.parser.module
 import init.lean.expander
 import init.lean.expr
 import init.lean.options
+import init.lean.environment
 
 namespace Lean
--- TODO(Sebastian): should probably be meta together with the whole Elaborator
-constant environment : Type := Unit
-
-@[extern "lean_environment_contains"]
-constant environment.contains (env : @& environment) (n : @& Name) : Bool := false
 -- deprecated Constructor
 @[extern "lean_expr_local"]
 constant Expr.local (n : Name) (pp : Name) (ty : Expr) (bi : BinderInfo) : Expr := default Expr
@@ -35,7 +31,7 @@ structure SectionVar :=
 
 /-- Simplified State of the Lean 3 Parser. Maps are replaced with lists for easier interop. -/
 structure OldElaboratorState :=
-(env : environment)
+(env : Environment)
 (ngen : NameGenerator)
 (univs : List (Name × Level))
 (vars : List (Name × SectionVar))
@@ -121,7 +117,7 @@ structure ElaboratorState :=
 (messages : MessageLog := MessageLog.empty)
 (parserCfg : ModuleParserConfig)
 (expanderCfg : Expander.ExpanderConfig)
-(env : environment)
+(env : Environment)
 (ngen : NameGenerator)
 (nextInstIdx : Nat := 0)
 
@@ -455,17 +451,17 @@ Expr.lit $ Literal.natVal $ match mod with
 | some $ inferModifier.View.relaxed _ := 1
 | some $ inferModifier.View.strict _  := 2
 
-def Declaration.elaborate : Elaborator :=
+def declaration.elaborate : Elaborator :=
 λ stx, locally $ do
-  let Decl := view «Declaration» stx,
-  match Decl.inner with
-  | Declaration.inner.View.«axiom» c@{sig := {params := bracketedBinders.View.simple [], type := type}, ..} := do
+  let decl := view «declaration» stx,
+  match decl.inner with
+  | declaration.inner.View.«axiom» c@{sig := {params := bracketedBinders.View.simple [], type := type}, ..} := do
     let mdata := MData.empty.setName `command `«axiom», -- CommentTo(Kha): It was `constant` here
-    mods ← declModifiersToPexpr Decl.modifiers,
+    mods ← declModifiersToPexpr decl.modifiers,
     let id := identUnivParamsToPexpr c.Name,
     type ← toPexpr type.type,
     oldElabCommand stx $ Expr.mdata mdata $ Expr.mkCapp `_ [mods, id, type]
-  | Declaration.inner.View.defLike dl := do
+  | declaration.inner.View.defLike dl := do
       -- The numeric literals below should reflect the enum values
       -- enum class declCmdKind { Theorem, Definition, OpaqueConst, Example, Instance, Var, Abbreviation };
       let kind := match dl.kind with
@@ -474,27 +470,27 @@ def Declaration.elaborate : Elaborator :=
       | defLike.kind.View.«constant» _ := 2
       | defLike.kind.View.abbreviation _ := 6
       | defLike.kind.View.«abbrev» _ := 6,
-      elabDefLike stx Decl.modifiers dl kind
+      elabDefLike stx decl.modifiers dl kind
 
   -- these are almost macros for `def`, Except the Elaborator handles them specially at a few places
   -- based on the kind
-  | Declaration.inner.View.example ex :=
-    elabDefLike stx Decl.modifiers {
+  | declaration.inner.View.example ex :=
+    elabDefLike stx decl.modifiers {
       kind := defLike.kind.View.def,
       Name := {id := Name.anonymous},
       sig := {..ex.sig},
       ..ex} 3
-  | Declaration.inner.View.instance i :=
-    elabDefLike stx Decl.modifiers {
+  | declaration.inner.View.instance i :=
+    elabDefLike stx decl.modifiers {
       kind := defLike.kind.View.def,
       Name := i.Name.getOrElse {id := Name.anonymous},
       sig := {..i.sig},
       ..i} 4
 
-  | Declaration.inner.View.inductive ind@{«class» := none, sig := {params := bracketedBinders.View.simple bbs}, ..} := do
+  | declaration.inner.View.inductive ind@{«class» := none, sig := {params := bracketedBinders.View.simple bbs}, ..} := do
     let mdata := MData.empty.setName `command `inductives,
-    mods ← declModifiersToPexpr Decl.modifiers,
-    attrs ← attrsToPexpr (match Decl.modifiers.attrs with
+    mods ← declModifiersToPexpr decl.modifiers,
+    attrs ← attrsToPexpr (match decl.modifiers.attrs with
       | some attrs := attrs.attrs
       | none       := []),
     let mutAttrs := Expr.mkCapp `_ [attrs],
@@ -514,7 +510,7 @@ def Declaration.elaborate : Elaborator :=
     params ← simpleBindersToPexpr bbs,
     introRules ← ind.introRules.mmap (λ (r : introRule.View), do
       ({params := bracketedBinders.View.simple [], type := some ty}) ← pure r.sig
-        | error stx "Declaration.elaborate: unexpected input",
+        | error stx "declaration.elaborate: unexpected input",
       type ← toPexpr ty.type,
       let Name := mangleIdent r.Name,
       pure $ Expr.local Name Name type BinderInfo.default),
@@ -526,9 +522,9 @@ def Declaration.elaborate : Elaborator :=
     oldElabCommand stx $ Expr.mdata mdata $
       Expr.mkCapp `_ [mods, mutAttrs, uparams, inds, params, introRules, inferKinds]
 
-  | Declaration.inner.View.structure s@{keyword := structureKw.View.structure _, sig := {params := bracketedBinders.View.simple bbs}, ..} := do
+  | declaration.inner.View.structure s@{keyword := structureKw.View.structure _, sig := {params := bracketedBinders.View.simple bbs}, ..} := do
     let mdata := MData.empty.setName `command `structure,
-    mods ← declModifiersToPexpr Decl.modifiers,
+    mods ← declModifiersToPexpr decl.modifiers,
     match s.oldUnivParams with
     | some uparams :=
       modifyCurrentScope $ λ sc, {sc with univs :=
@@ -555,7 +551,7 @@ def Declaration.elaborate : Elaborator :=
     fieldBlocks ← s.fieldBlocks.mmap (λ bl, do
       (bi, content) ← match bl with
         | structureFieldBlock.View.explicit {content := structExplicitBinderContent.View.notation _} :=
-          error stx "Declaration.elaborate: unexpected input"
+          error stx "declaration.elaborate: unexpected input"
         | structureFieldBlock.View.explicit {content := structExplicitBinderContent.View.other c} :=
           pure (BinderInfo.default, c)
         | structureFieldBlock.View.implicit {content := c} := pure (BinderInfo.implicit, c)
@@ -571,7 +567,7 @@ def Declaration.elaborate : Elaborator :=
     oldElabCommand stx $ Expr.mdata mdata $
       Expr.mkCapp `_ [mods, uparams, Name, params, parents, type, mk, infer, fieldBlocks]
   | _ :=
-    error stx "Declaration.elaborate: unexpected input"
+    error stx "declaration.elaborate: unexpected input"
 
 def variables.elaborate : Elaborator :=
 λ stx, do
@@ -906,7 +902,7 @@ def elaborators : RBMap Name Elaborator Name.quickLt := RBMap.fromList [
   (variables.name, variables.elaborate),
   (include.name, include.elaborate),
   --(omit.name, omit.elaborate),
-  (Declaration.name, Declaration.elaborate),
+  (declaration.name, declaration.elaborate),
   (attribute.name, attribute.elaborate),
   (open.name, open.elaborate),
   (export.name, export.elaborate),
@@ -981,7 +977,7 @@ partial def preresolve : Syntax → ElaboratorM Syntax
   pure $ Syntax.rawNode {n with args := args}
 | stx := pure stx
 
-def mkState (cfg : ElaboratorConfig) (env : environment) (opts : Options) : ElaboratorState := {
+def mkState (cfg : ElaboratorConfig) (env : Environment) (opts : Options) : ElaboratorState := {
   parserCfg := cfg.initialParserCfg,
   expanderCfg := {transformers := Expander.builtinTransformers, ..cfg},
   env := env,

library/init/lean/environment.lean

@@ -42,6 +42,9 @@ def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
 def find (env : Environment) (n : Name) : Option ConstantInfo :=
 env.constants.find n
 
+def contains (env : Environment) (n : Name) : Bool :=
+(env.constants.find n).isSome
+
 /- Switch environment to "shared" mode. -/
 @[export lean.environment_switch_core]
 private def switch (env : Environment) : Environment :=

library/init/lean/expander.lean

@@ -51,7 +51,7 @@ instance coeNameIdent : HasCoe Name SyntaxIdent :=
 ⟨λ n, {val := n, rawVal := Substring.ofString n.toString}⟩
 
 /-- Create an identifier preresolved against a global binding. Because we cannot use Syntax quotations yet,
-    which the Expander would have preresolved against the global context at macro Declaration time,
+    which the Expander would have preresolved against the global context at macro declaration time,
     we have to do the preresolution manually instead. -/
 def globId (n : Name) : Syntax :=
 review identUnivs {
@@ -179,7 +179,7 @@ match k with
   -- `infixr tk:prec` ~> `notation a tk:prec b:(prec-1)`
   act ← match prec with
   | some prec := if prec.Term.toNat = 0
-    then error (review «precedence» prec) "invalid `infixr` Declaration, given precedence must greater than zero"
+    then error (review «precedence» prec) "invalid `infixr` declaration, given precedence must greater than zero"
     else pure $ some $ precToAction $ precedenceTerm.View.lit $ precedenceLit.View.num $ number.View.ofNat $ prec.Term.toNat - 1
   | none := pure none,
   pure {
@@ -395,23 +395,23 @@ def axiom.transform : transformer :=
       type := {type := review pi {op := Syntax.atom {val := "Π"}, binders := bindrs, range := type.type}}}}
   | _ := noExpansion
 
-def Declaration.transform : transformer :=
+def declaration.transform : transformer :=
 λ stx, do
-  let v := view «Declaration» stx,
+  let v := view «declaration» stx,
   match v.inner with
-  | Declaration.inner.View.inductive ind@{«class» := some _, ..} :=
+  | declaration.inner.View.inductive ind@{«class» := some _, ..} :=
     let attrs := v.modifiers.attrs.getOrElse {attrs := []} in
-    pure $ review «Declaration» {v with
+    pure $ review «declaration» {v with
       modifiers := {v.modifiers with attrs := some {attrs with attrs :=
         {item := {Name := "class", args := []}} :: attrs.attrs}},
-      inner := Declaration.inner.View.inductive {ind with «class» := none}
+      inner := declaration.inner.View.inductive {ind with «class» := none}
     }
-  | Declaration.inner.View.structure s@{keyword := structureKw.View.class _, ..} :=
+  | declaration.inner.View.structure s@{keyword := structureKw.View.class _, ..} :=
     let attrs := v.modifiers.attrs.getOrElse {attrs := []} in
-    pure $ review «Declaration» {v with
+    pure $ review «declaration» {v with
       modifiers := {v.modifiers with attrs := some {attrs with attrs :=
         {item := {Name := "class", args := []}} :: attrs.attrs}},
-      inner := Declaration.inner.View.structure {s with keyword := structureKw.View.structure}
+      inner := declaration.inner.View.structure {s with keyword := structureKw.View.structure}
     }
   | _ := noExpansion
 
@@ -490,7 +490,7 @@ def builtinTransformers : RBMap Name transformer Name.quickLt := RBMap.fromList
   (if.name, if.transform),
   (let.name, let.transform),
   (axiom.name, axiom.transform),
-  (Declaration.name, Declaration.transform),
+  (declaration.name, declaration.transform),
   (introRule.name, introRule.transform),
   (variable.name, variable.transform),
   (variables.name, variables.transform),

library/init/lean/frontend.lean

@@ -26,7 +26,7 @@ do t ← Parser.mkTokenTrie $
    }
 
 def runFrontend (filename input : String) (printMsg : Message → IO Unit) (collectOutputs : Bool) :
-  StateT environment IO (List Syntax) := λ env, do
+  StateT Environment IO (List Syntax) := λ env, do
   parserCfg ← ioOfExcept $ mkConfig filename input,
   -- TODO(Sebastian): `parseHeader` should be called directly by Lean.cpp
   match parseHeader parserCfg with
@@ -70,7 +70,7 @@ def runFrontend (filename input : String) (printMsg : Message → IO Unit) (coll
   }
 
 @[export lean_process_file]
-def processFile (f s : String) (json : Bool) : StateT environment IO Unit := do
+def processFile (f s : String) (json : Bool) : StateT Environment IO Unit := do
   let printMsg : Message → IO Unit := λ msg,
     if json then
       IO.println $ "{\"file_name\": \"<stdin>\", \"pos_line\": " ++ toString msg.pos.line ++

library/init/lean/parser/command.lean

@@ -102,8 +102,8 @@ node! «initQuot» ["initQuot"]
 def setOption.Parser : commandParser :=
 node! «setOption» ["setOption", opt: ident.Parser, val: nodeChoice! optionValue {
   Bool: nodeChoice! boolOptionValue {
-    True: symbolOrIdent "True",
-    False: symbolOrIdent "True",
+    True: symbolOrIdent "true",
+    False: symbolOrIdent "false",
   },
   String: stringLit.Parser,
   -- TODO(Sebastian): fractional numbers
@@ -112,22 +112,22 @@ node! «setOption» ["setOption", opt: ident.Parser, val: nodeChoice! optionValu
 
 @[derive HasTokens]
 def builtinCommandParsers : TokenMap commandParser := TokenMap.ofList [
-  ("/--", Declaration.Parser),
-  ("@[", Declaration.Parser),
-  ("private", Declaration.Parser),
-  ("protected", Declaration.Parser),
-  ("noncomputable", Declaration.Parser),
-  ("unsafe", Declaration.Parser),
-  ("def", Declaration.Parser),
-  ("abbreviation", Declaration.Parser),
-  ("abbrev", Declaration.Parser),
-  ("theorem", Declaration.Parser),
-  ("instance", Declaration.Parser),
-  ("axiom", Declaration.Parser),
-  ("constant", Declaration.Parser),
-  ("class", Declaration.Parser),
-  ("inductive", Declaration.Parser),
-  ("structure", Declaration.Parser),
+  ("/--", declaration.Parser),
+  ("@[", declaration.Parser),
+  ("private", declaration.Parser),
+  ("protected", declaration.Parser),
+  ("noncomputable", declaration.Parser),
+  ("unsafe", declaration.Parser),
+  ("def", declaration.Parser),
+  ("abbreviation", declaration.Parser),
+  ("abbrev", declaration.Parser),
+  ("theorem", declaration.Parser),
+  ("instance", declaration.Parser),
+  ("axiom", declaration.Parser),
+  ("constant", declaration.Parser),
+  ("class", declaration.Parser),
+  ("inductive", declaration.Parser),
+  ("structure", declaration.Parser),
 
   ("variable", variable.Parser),
   ("variables", variables.Parser),

library/init/lean/parser/declaration.lean

@@ -138,10 +138,10 @@ node! «structure» [
 ]
 
 @[derive HasTokens HasView]
-def Declaration.Parser : commandParser :=
-node! Declaration [
+def declaration.Parser : commandParser :=
+node! declaration [
   modifiers: declModifiers.Parser,
-  inner: nodeChoice! Declaration.inner {
+  inner: nodeChoice! declaration.inner {
     «defLike»: node! «defLike» [
       kind: nodeChoice! defLike.kind {"def", "abbreviation", "abbrev", "theorem", "constant"},
       oldUnivParams: oldUnivParams.Parser?,

library/init/lean/parser/syntax.lean

@@ -24,10 +24,10 @@ structure SourceInfo :=
 structure SyntaxAtom :=
 (info : Option SourceInfo := none) (val : String)
 
-/-- A simple wrapper that should remind you to use the static Declaration instead
+/-- A simple wrapper that should remind you to use the static declaration instead
     of hard-coding the Node Name. -/
 structure SyntaxNodeKind :=
--- should be equal to the Name of the Declaration this structure instance was bound to
+-- should be equal to the Name of the declaration this structure instance was bound to
 (name : Name)
 
 /-- Signifies ambiguous Syntax to be disambiguated by the Elaborator. Should have at least two children.