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

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-24 06:18:01 -07:00
parent afabe15a26
commit 0ab38742db
10 changed files with 967 additions and 968 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

868
src/Lean/Expr.lean
View file

File diff suppressed because it is too large Load diff

28
src/Lean/InternalExceptionId.lean
View file

@ -7,30 +7,30 @@ Authors: Leonardo de Moura
namespace Lean
structure InternalExceptionId :=
(idx : Nat := 0)
(idx : Nat := 0)
instance : Inhabited InternalExceptionId := ⟨{}⟩
instance : HasBeq InternalExceptionId :=
⟨fun id₁ id₂ => id₁.idx == id₂.idx⟩
⟨fun id₁ id₂ => id₁.idx == id₂.idx⟩
builtin_initialize internalExceptionsRef : IO.Ref (Array Name) ← IO.mkRef #[]
def registerInternalExceptionId (name : Name) : IO InternalExceptionId := do
let exs ← internalExceptionsRef.get
if exs.contains name then throw $ IO.userError s!"invalid internal exception id, '{name}' has already been used"
let nextIdx := exs.size
internalExceptionsRef.modify fun a => a.push name
pure { idx := nextIdx }
let exs ← internalExceptionsRef.get
if exs.contains name then throw $ IO.userError s!"invalid internal exception id, '{name}' has already been used"
let nextIdx := exs.size
internalExceptionsRef.modify fun a => a.push name
pure { idx := nextIdx }
def InternalExceptionId.toString (id : InternalExceptionId) : String :=
s!"internal exception #{id.idx}"
s!"internal exception #{id.idx}"
def InternalExceptionId.getName (id : InternalExceptionId) : IO Name := do
let exs ← internalExceptionsRef.get
let i := id.idx;
if h : i < exs.size then
pure $ exs.get ⟨i, h⟩
else
throw $ IO.userError "invalid internal exception id"
let exs ← internalExceptionsRef.get
let i := id.idx;
if h : i < exs.size then
pure $ exs.get ⟨i, h⟩
else
throw $ IO.userError "invalid internal exception id"
end Lean

180
src/Lean/KeyedDeclsAttribute.lean
View file

@ -29,140 +29,140 @@ abbrev Key := Name
Important: `mkConst valueTypeName` and `γ` must be definitionally equal. -/
structure Def (γ : Type) :=
(builtinName : Name) -- Builtin attribute name (e.g., `builtinTermElab)
(name : Name) -- Attribute name (e.g., `termElab)
(descr : String) -- Attribute description
(valueTypeName : Name)
-- Convert `Syntax` into a `Key`, the default implementation expects an identifier.
(evalKey : Bool → Syntax → AttrM Key :=
fun builtin arg => match attrParamSyntaxToIdentifier arg with
| some id => pure id
| none => throwError "invalid attribute argument, expected identifier")
(builtinName : Name) -- Builtin attribute name (e.g., `builtinTermElab)
(name : Name) -- Attribute name (e.g., `termElab)
(descr : String) -- Attribute description
(valueTypeName : Name)
-- Convert `Syntax` into a `Key`, the default implementation expects an identifier.
(evalKey : Bool → Syntax → AttrM Key :=
fun builtin arg => match attrParamSyntaxToIdentifier arg with
| some id => pure id
| none => throwError "invalid attribute argument, expected identifier")
instance {γ} : Inhabited (Def γ) :=
⟨{ builtinName := arbitrary _, name := arbitrary _, descr := arbitrary _, valueTypeName := arbitrary _ }⟩
⟨{ builtinName := arbitrary _, name := arbitrary _, descr := arbitrary _, valueTypeName := arbitrary _ }⟩
structure OLeanEntry :=
(key : Key)
(decl : Name) -- Name of a declaration stored in the environment which has type `mkConst Def.valueTypeName`.
(key : Key)
(decl : Name) -- Name of a declaration stored in the environment which has type `mkConst Def.valueTypeName`.
structure AttributeEntry (γ : Type) extends OLeanEntry :=
/- Recall that we cannot store `γ` into .olean files because it is a closure.
Given `OLeanEntry.decl`, we convert it into a `γ` by using the unsafe function `evalConstCheck`. -/
(value : γ)
/- Recall that we cannot store `γ` into .olean files because it is a closure.
Given `OLeanEntry.decl`, we convert it into a `γ` by using the unsafe function `evalConstCheck`. -/
(value : γ)
abbrev Table (γ : Type) := SMap Key (List γ)
structure ExtensionState (γ : Type) :=
(newEntries : List OLeanEntry := [])
(table : Table γ := {})
(newEntries : List OLeanEntry := [])
(table : Table γ := {})
abbrev Extension (γ : Type) := PersistentEnvExtension OLeanEntry (AttributeEntry γ) (ExtensionState γ)
end KeyedDeclsAttribute
structure KeyedDeclsAttribute (γ : Type) :=
(defn : KeyedDeclsAttribute.Def γ)
-- imported/builtin instances
(tableRef : IO.Ref (KeyedDeclsAttribute.Table γ))
-- instances from current module
(ext : KeyedDeclsAttribute.Extension γ)
(defn : KeyedDeclsAttribute.Def γ)
-- imported/builtin instances
(tableRef : IO.Ref (KeyedDeclsAttribute.Table γ))
-- instances from current module
(ext : KeyedDeclsAttribute.Extension γ)
namespace KeyedDeclsAttribute
def Table.insert {γ : Type} (table : Table γ) (k : Key) (v : γ) : Table γ :=
match table.find? k with
| some vs => SMap.insert table k (v::vs)
| none => SMap.insert table k [v]
match table.find? k with
| some vs => SMap.insert table k (v::vs)
| none => SMap.insert table k [v]
instance {γ} : Inhabited (ExtensionState γ) := ⟨{}⟩
instance {γ} : Inhabited (KeyedDeclsAttribute γ) :=
⟨{ defn := arbitrary _, tableRef := arbitrary _, ext := arbitrary _ }⟩
⟨{ defn := arbitrary _, tableRef := arbitrary _, ext := arbitrary _ }⟩
private def mkInitial {γ} (tableRef : IO.Ref (Table γ)) : IO (ExtensionState γ) := do
let table ← tableRef.get
pure { table := table }
let table ← tableRef.get
pure { table := table }
private unsafe def addImported {γ} (df : Def γ) (tableRef : IO.Ref (Table γ)) (es : Array (Array OLeanEntry)) : ImportM (ExtensionState γ) := do
let ctx ← read
let table ← tableRef.get
let table ← es.foldlM
(fun table entries =>
entries.foldlM
(fun (table : Table γ) entry =>
match ctx.env.evalConstCheck γ ctx.opts df.valueTypeName entry.decl with
| Except.ok f => pure $ table.insert entry.key f
| Except.error ex => throw (IO.userError ex))
table)
table
pure { table := table }
let ctx ← read
let table ← tableRef.get
let table ← es.foldlM
(fun table entries =>
entries.foldlM
(fun (table : Table γ) entry =>
match ctx.env.evalConstCheck γ ctx.opts df.valueTypeName entry.decl with
| Except.ok f => pure $ table.insert entry.key f
| Except.error ex => throw (IO.userError ex))
table)
table
pure { table := table }
private def addExtensionEntry {γ} (s : ExtensionState γ) (e : AttributeEntry γ) : ExtensionState γ :=
{ table := s.table.insert e.key e.value, newEntries := e.toOLeanEntry :: s.newEntries }
{ table := s.table.insert e.key e.value, newEntries := e.toOLeanEntry :: s.newEntries }
def addBuiltin {γ} (attr : KeyedDeclsAttribute γ) (key : Key) (val : γ) : IO Unit :=
attr.tableRef.modify $ fun m => m.insert key val
attr.tableRef.modify $ fun m => m.insert key val
/--
def _regBuiltin$(declName) : IO Unit :=
@addBuiltin $(mkConst valueTypeName) $(mkConst attrDeclName) $(key) $(mkConst declName)
-/
def declareBuiltin {γ} (df : Def γ) (attrDeclName : Name) (env : Environment) (key : Key) (declName : Name) : IO Environment :=
let name := `_regBuiltin ++ declName
let type := mkApp (mkConst `IO) (mkConst `Unit)
let val := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, mkConst declName]
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false }
match env.addAndCompile {} decl with
-- TODO: pretty print error
| Except.error e => do
let msg ← (e.toMessageData {}).toString
throw (IO.userError s!"failed to emit registration code for builtin '{declName}': {msg}")
| Except.ok env => IO.ofExcept (setBuiltinInitAttr env name)
let name := `_regBuiltin ++ declName
let type := mkApp (mkConst `IO) (mkConst `Unit)
let val := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, mkConst declName]
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false }
match env.addAndCompile {} decl with
-- TODO: pretty print error
| Except.error e => do
let msg ← (e.toMessageData {}).toString
throw (IO.userError s!"failed to emit registration code for builtin '{declName}': {msg}")
| Except.ok env => IO.ofExcept (setBuiltinInitAttr env name)
/- TODO: add support for scoped attributes -/
protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDeclsAttribute γ) := do
let tableRef ← IO.mkRef ({} : Table γ)
let ext : Extension γ ← registerPersistentEnvExtension {
name := df.name,
mkInitial := mkInitial tableRef,
addImportedFn := addImported df tableRef,
addEntryFn := addExtensionEntry,
exportEntriesFn := fun s => s.newEntries.reverse.toArray,
statsFn := fun s => f!"number of local entries: {s.newEntries.length}"
}
registerBuiltinAttribute {
name := df.builtinName,
descr := "(builtin) " ++ df.descr,
add := fun declName arg persistent => do
unless persistent do throwError! "invalid attribute '{df.builtinName}', must be persistent"
let key ← df.evalKey true arg
let decl ← getConstInfo declName
match decl.type with
| Expr.const c _ _ =>
if c != df.valueTypeName then throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected"
else
let env ← getEnv
let env ← liftIO $ declareBuiltin df attrDeclName env key declName
setEnv env
| _ => throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected",
applicationTime := AttributeApplicationTime.afterCompilation
}
registerBuiltinAttribute {
name := df.name,
descr := df.descr,
add := fun constName arg persistent => do
let key ← df.evalKey false arg
let val ← evalConstCheck γ df.valueTypeName constName
let env ← getEnv
setEnv $ ext.addEntry env { key := key, decl := constName, value := val },
applicationTime := AttributeApplicationTime.afterCompilation
}
pure { defn := df, tableRef := tableRef, ext := ext }
let tableRef ← IO.mkRef ({} : Table γ)
let ext : Extension γ ← registerPersistentEnvExtension {
name := df.name,
mkInitial := mkInitial tableRef,
addImportedFn := addImported df tableRef,
addEntryFn := addExtensionEntry,
exportEntriesFn := fun s => s.newEntries.reverse.toArray,
statsFn := fun s => f!"number of local entries: {s.newEntries.length}"
}
registerBuiltinAttribute {
name := df.builtinName,
descr := "(builtin) " ++ df.descr,
add := fun declName arg persistent => do
unless persistent do throwError! "invalid attribute '{df.builtinName}', must be persistent"
let key ← df.evalKey true arg
let decl ← getConstInfo declName
match decl.type with
| Expr.const c _ _ =>
if c != df.valueTypeName then throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected"
else
let env ← getEnv
let env ← liftIO $ declareBuiltin df attrDeclName env key declName
setEnv env
| _ => throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected",
applicationTime := AttributeApplicationTime.afterCompilation
}
registerBuiltinAttribute {
name := df.name,
descr := df.descr,
add := fun constName arg persistent => do
let key ← df.evalKey false arg
let val ← evalConstCheck γ df.valueTypeName constName
let env ← getEnv
setEnv $ ext.addEntry env { key := key, decl := constName, value := val },
applicationTime := AttributeApplicationTime.afterCompilation
}
pure { defn := df, tableRef := tableRef, ext := ext }
/-- Retrieve values tagged with `[attr key]` or `[builtinAttr key]`. -/
def getValues {γ} (attr : KeyedDeclsAttribute γ) (env : Environment) (key : Name) : List γ :=
(attr.ext.getState env).table.findD key []
(attr.ext.getState env).table.findD key []
end KeyedDeclsAttribute

402
src/Lean/Level.lean
View file

@ -25,62 +25,62 @@ namespace Lean
def Level.Data := UInt64
instance : Inhabited Level.Data :=
inferInstanceAs (Inhabited UInt64)
inferInstanceAs (Inhabited UInt64)
def Level.Data.hash (c : Level.Data) : USize :=
c.toUInt32.toUSize
c.toUInt32.toUSize
instance : HasBeq Level.Data :=
⟨fun (a b : UInt64) => a == b⟩
⟨fun (a b : UInt64) => a == b⟩
def Level.Data.depth (c : Level.Data) : UInt32 :=
(c.shiftRight 40).toUInt32
(c.shiftRight 40).toUInt32
def Level.Data.hasMVar (c : Level.Data) : Bool :=
((c.shiftRight 32).land 1) == 1
((c.shiftRight 32).land 1) == 1
def Level.Data.hasParam (c : Level.Data) : Bool :=
((c.shiftRight 33).land 1) == 1
((c.shiftRight 33).land 1) == 1
def Level.mkData (h : USize) (depth : Nat) (hasMVar hasParam : Bool) : Level.Data :=
if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big"
else
let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40
r
if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big"
else
let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40
r
open Level
inductive Level
| zero : Data → Level
| succ : Level → Data → Level
| max : Level → Level → Data → Level
| imax : Level → Level → Data → Level
| param : Name → Data → Level
| mvar : Name → Data → Level
| zero : Data → Level
| succ : Level → Data → Level
| max : Level → Level → Data → Level
| imax : Level → Level → Data → Level
| param : Name → Data → Level
| mvar : Name → Data → Level
namespace Level
@[inline] def data : Level → Data
| zero d => d
| mvar _ d => d
| param _ d => d
| succ _ d => d
| max _ _ d => d
| imax _ _ d => d
| zero d => d
| mvar _ d => d
| param _ d => d
| succ _ d => d
| max _ _ d => d
| imax _ _ d => d
protected def hash (u : Level) : USize :=
u.data.hash
u.data.hash
instance : Hashable Level := ⟨Level.hash⟩
def depth (u : Level) : Nat :=
u.data.depth.toNat
u.data.depth.toNat
def hasMVar (u : Level) : Bool :=
u.data.hasMVar
u.data.hasMVar
def hasParam (u : Level) : Bool :=
u.data.hasParam
u.data.hasParam
@[export lean_level_hash] def hashEx : Level → USize := Level.hash
@[export lean_level_has_mvar] def hasMVarEx : Level → Bool := hasMVar
@ -90,26 +90,26 @@ u.data.hasParam
end Level
def levelZero :=
Level.zero $ mkData 2221 0 false false
Level.zero $ mkData 2221 0 false false
def mkLevelMVar (mvarId : Name) :=
Level.mvar mvarId $ mkData (mixHash 2237 $ hash mvarId) 0 true false
Level.mvar mvarId $ mkData (mixHash 2237 $ hash mvarId) 0 true false
def mkLevelParam (name : Name) :=
Level.param name $ mkData (mixHash 2239 $ hash name) 0 false true
Level.param name $ mkData (mixHash 2239 $ hash name) 0 false true
def mkLevelSucc (u : Level) :=
Level.succ u $ mkData (mixHash 2243 $ hash u) (u.depth + 1) u.hasMVar u.hasParam
Level.succ u $ mkData (mixHash 2243 $ hash u) (u.depth + 1) u.hasMVar u.hasParam
def mkLevelMax (u v : Level) :=
Level.max u v $ mkData (mixHash 2251 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
(u.hasMVar || v.hasMVar)
(u.hasParam || v.hasParam)
Level.max u v $ mkData (mixHash 2251 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
(u.hasMVar || v.hasMVar)
(u.hasParam || v.hasParam)
def mkLevelIMax (u v : Level) :=
Level.imax u v $ mkData (mixHash 2267 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
(u.hasMVar || v.hasMVar)
(u.hasParam || v.hasParam)
Level.imax u v $ mkData (mixHash 2267 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
(u.hasMVar || v.hasMVar)
(u.hasParam || v.hasParam)
def levelOne := mkLevelSucc levelZero
@ -125,79 +125,79 @@ namespace Level
instance : Inhabited Level := ⟨levelZero⟩
def isZero : Level → Bool
| zero _ => true
| _ => false
| zero _ => true
| _ => false
def isSucc : Level → Bool
| succ _ _ => true
| _ => false
| succ .. => true
| _ => false
def isMax : Level → Bool
| max _ _ _ => true
| _ => false
| max .. => true
| _ => false
def isIMax : Level → Bool
| imax _ _ _ => true
| _ => false
| imax .. => true
| _ => false
def isMaxIMax : Level → Bool
| max _ _ _ => true
| imax _ _ _ => true
| _ => false
| max .. => true
| imax .. => true
| _ => false
def isParam : Level → Bool
| param _ _ => true
| _ => false
| param .. => true
| _ => false
def isMVar : Level → Bool
| mvar _ _ => true
| _ => false
| mvar .. => true
| _ => false
def mvarId! : Level → Name
| mvar mvarId _ => mvarId
| _ => panic! "metavariable expected"
| mvar mvarId _ => mvarId
| _ => panic! "metavariable expected"
/-- If result is true, then forall assignments `A` which assigns all parameters and metavariables occuring
in `l`, `l[A] != zero` -/
def isNeverZero : Level → Bool
| zero _ => false
| param _ _ => false
| mvar _ _ => false
| succ _ _ => true
| max l₁ l₂ _ => isNeverZero l₁ || isNeverZero l₂
| imax l₁ l₂ _ => isNeverZero l₂
| zero _ => false
| param .. => false
| mvar .. => false
| succ .. => true
| max l₁ l₂ _ => isNeverZero l₁ || isNeverZero l₂
| imax l₁ l₂ _ => isNeverZero l₂
def ofNat : Nat → Level
| 0 => levelZero
| n+1 => mkLevelSucc (ofNat n)
| 0 => levelZero
| n+1 => mkLevelSucc (ofNat n)
def addOffsetAux : Nat → Level → Level
| 0, u => u
| (n+1), u => addOffsetAux n (mkLevelSucc u)
| 0, u => u
| (n+1), u => addOffsetAux n (mkLevelSucc u)
def addOffset (u : Level) (n : Nat) : Level :=
u.addOffsetAux n
u.addOffsetAux n
def isExplicit : Level → Bool
| zero _ => true
| succ u _ => !u.hasMVar && !u.hasParam && isExplicit u
| _ => false
| zero _ => true
| succ u _ => !u.hasMVar && !u.hasParam && isExplicit u
| _ => false
def getOffsetAux : Level → Nat → Nat
| succ u _, r => getOffsetAux u (r+1)
| _, r => r
| succ u _, r => getOffsetAux u (r+1)
| _, r => r
def getOffset (lvl : Level) : Nat :=
getOffsetAux lvl 0
getOffsetAux lvl 0
def getLevelOffset : Level → Level
| succ u _ => getLevelOffset u
| u => u
| succ u _ => getLevelOffset u
| u => u
def toNat (lvl : Level) : Option Nat :=
match lvl.getLevelOffset with
| zero _ => lvl.getOffset
| _ => none
match lvl.getLevelOffset with
| zero _ => lvl.getOffset
| _ => none
@[extern "lean_level_eq"]
protected constant beq (a : @& Level) (b : @& Level) : Bool := arbitrary _
@ -206,34 +206,34 @@ instance : HasBeq Level := ⟨Level.beq⟩
/-- `occurs u l` return `true` iff `u` occurs in `l`. -/
def occurs : Level → Level → Bool
| u, v@(succ v₁ _) => u == v || occurs u v₁
| u, v@(max v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂
| u, v@(imax v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂
| u, v => u == v
| u, v@(succ v₁ _) => u == v || occurs u v₁
| u, v@(max v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂
| u, v@(imax v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂
| u, v => u == v
def ctorToNat : Level → Nat
| zero _ => 0
| param _ _ => 1
| mvar _ _ => 2
| succ _ _ => 3
| max _ _ _ => 4
| imax _ _ _ => 5
| zero .. => 0
| param .. => 1
| mvar .. => 2
| succ .. => 3
| max .. => 4
| imax .. => 5
/- TODO: use well founded recursion. -/
partial def normLtAux : Level → Nat → Level → Nat → Bool
| succ l₁ _, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂
| l₁, k₁, succ l₂ _, k₂ => normLtAux l₁ k₁ l₂ (k₂+1)
| l₁@(max l₁₁ l₁₂ _), k₁, l₂@(max l₂₁ l₂₂ _), k₂ =>
if l₁ == l₂ then k₁ < k₂
else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
else normLtAux l₁₂ 0 l₂₂ 0
| l₁@(imax l₁₁ l₁₂ _), k₁, l₂@(imax l₂₁ l₂₂ _), k₂ =>
if l₁ == l₂ then k₁ < k₂
else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
else normLtAux l₁₂ 0 l₂₂ 0
| param n₁ _, k₁, param n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use Name.lt because it is lexicographical
| mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.quickLt n₁ n₂ -- metavariables are temporary, the actual order doesn't matter
| l₁, k₁, l₂, k₂ => if l₁ == l₂ then k₁ < k₂ else ctorToNat l₁ < ctorToNat l₂
| succ l₁ _, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂
| l₁, k₁, succ l₂ _, k₂ => normLtAux l₁ k₁ l₂ (k₂+1)
| l₁@(max l₁₁ l₁₂ _), k₁, l₂@(max l₂₁ l₂₂ _), k₂ =>
if l₁ == l₂ then k₁ < k₂
else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
else normLtAux l₁₂ 0 l₂₂ 0
| l₁@(imax l₁₁ l₁₂ _), k₁, l₂@(imax l₂₁ l₂₂ _), k₂ =>
if l₁ == l₂ then k₁ < k₂
else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
else normLtAux l₁₂ 0 l₂₂ 0
| param n₁ _, k₁, param n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use Name.lt because it is lexicographical
| mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.quickLt n₁ n₂ -- metavariables are temporary, the actual order doesn't matter
| l₁, k₁, l₂, k₂ => if l₁ == l₂ then k₁ < k₂ else ctorToNat l₁ < ctorToNat l₂
/--
A total order on level expressions that has the following properties
@ -241,30 +241,30 @@ partial def normLtAux : Level → Nat → Level → Nat → Bool
- `zero` is the minimal element.
This total order is used in the normalization procedure. -/
def normLt (l₁ l₂ : Level) : Bool :=
normLtAux l₁ 0 l₂ 0
normLtAux l₁ 0 l₂ 0
private def isAlreadyNormalizedCheap : Level → Bool
| zero _ => true
| param _ _ => true
| mvar _ _ => true
| succ u _ => isAlreadyNormalizedCheap u
| _ => false
| zero _ => true
| param _ _ => true
| mvar _ _ => true
| succ u _ => isAlreadyNormalizedCheap u
| _ => false
/- Auxiliary function used at `normalize` -/
private def mkIMaxAux : Level → Level → Level
| _, u@(zero _) => u
| zero _, u => u
| u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
| _, u@(zero _) => u
| zero _, u => u
| u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
/- Auxiliary function used at `normalize` -/
@[specialize] private partial def getMaxArgsAux (normalize : Level → Level) : Level → Bool → Array Level → Array Level
| max l₁ l₂ _, alreadyNormalized, lvls => getMaxArgsAux normalize l₂ alreadyNormalized (getMaxArgsAux normalize l₁ alreadyNormalized lvls)
| l, false, lvls => getMaxArgsAux normalize (normalize l) true lvls
| l, true, lvls => lvls.push l
| max l₁ l₂ _, alreadyNormalized, lvls => getMaxArgsAux normalize l₂ alreadyNormalized (getMaxArgsAux normalize l₁ alreadyNormalized lvls)
| l, false, lvls => getMaxArgsAux normalize (normalize l) true lvls
| l, true, lvls => lvls.push l
private def accMax (result : Level) (prev : Level) (offset : Nat) : Level :=
if result.isZero then prev.addOffset offset
else mkLevelMax result (prev.addOffset offset)
if result.isZero then prev.addOffset offset
else mkLevelMax result (prev.addOffset offset)
/- Auxiliary function used at `normalize`.
Remarks:
@ -275,26 +275,26 @@ else mkLevelMax result (prev.addOffset offset)
- `result` is the accumulator
-/
private partial def mkMaxAux (lvls : Array Level) (extraK : Nat) (i : Nat) (prev : Level) (prevK : Nat) (result : Level) : Level :=
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
let curr := lvl.getLevelOffset
let currK := lvl.getOffset
if curr == prev then
mkMaxAux lvls extraK (i+1) curr currK result
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
let curr := lvl.getLevelOffset
let currK := lvl.getOffset
if curr == prev then
mkMaxAux lvls extraK (i+1) curr currK result
else
mkMaxAux lvls extraK (i+1) curr currK (accMax result prev (extraK + prevK))
else
mkMaxAux lvls extraK (i+1) curr currK (accMax result prev (extraK + prevK))
else
accMax result prev (extraK + prevK)
accMax result prev (extraK + prevK)
/-
Auxiliary function for `normalize`. It assumes `lvls` has been sorted using `normLt`.
It finds the first position that is not an explicit universe. -/
private partial def skipExplicit (lvls : Array Level) (i : Nat) : Nat :=
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
if lvl.getLevelOffset.isZero then skipExplicit lvls (i+1) else i
else
i
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
if lvl.getLevelOffset.isZero then skipExplicit lvls (i+1) else i
else
i
/-
Auxiliary function for `normalize`.
@ -303,19 +303,19 @@ else
`i` starts at the first non explict level.
It assumes `lvls` has been sorted using `normLt`. -/
private partial def isExplicitSubsumedAux (lvls : Array Level) (maxExplicit : Nat) (i : Nat) : Bool :=
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
if lvl.getOffset ≥ maxExplicit then true
else isExplicitSubsumedAux lvls maxExplicit (i+1)
else
false
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
if lvl.getOffset ≥ maxExplicit then true
else isExplicitSubsumedAux lvls maxExplicit (i+1)
else
false
/- Auxiliary function for `normalize`. See `isExplicitSubsumedAux` -/
private def isExplicitSubsumed (lvls : Array Level) (firstNonExplicit : Nat) : Bool :=
if firstNonExplicit == 0 then false
else
let max := (lvls.get! (firstNonExplicit - 1)).getOffset;
isExplicitSubsumedAux lvls max firstNonExplicit
if firstNonExplicit == 0 then false
else
let max := (lvls.get! (firstNonExplicit - 1)).getOffset;
isExplicitSubsumedAux lvls max firstNonExplicit
partial def normalize (l : Level) : Level :=
if isAlreadyNormalizedCheap l then l
@ -344,74 +344,74 @@ partial def normalize (l : Level) : Level :=
/- Return true if `u` and `v` denote the same level.
Check is currently incomplete. -/
def isEquiv (u v : Level) : Bool :=
u == v || u.normalize == v.normalize
u == v || u.normalize == v.normalize
/-- Reduce (if possible) universe level by 1 -/
def dec : Level → Option Level
| zero _ => none
| param _ _ => none
| mvar _ _ => none
| succ l _ => l
| max l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂
/- Remark: `mkLevelMax` in the following line is not a typo.
If `dec l₂` succeeds, then `imax l₁ l₂` is equivalent to `max l₁ l₂`. -/
| imax l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂
| zero _ => none
| param _ _ => none
| mvar _ _ => none
| succ l _ => l
| max l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂
/- Remark: `mkLevelMax` in the following line is not a typo.
If `dec l₂` succeeds, then `imax l₁ l₂` is equivalent to `max l₁ l₂`. -/
| imax l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂
/- Level to Format -/
namespace LevelToFormat
inductive Result
| leaf : Format → Result
| num : Nat → Result
| offset : Result → Nat → Result
| maxNode : List Result → Result
| imaxNode : List Result → Result
| leaf : Format → Result
| num : Nat → Result
| offset : Result → Nat → Result
| maxNode : List Result → Result
| imaxNode : List Result → Result
def Result.succ : Result → Result
| Result.offset f k => Result.offset f (k+1)
| Result.num k => Result.num (k+1)
| f => Result.offset f 1
| Result.offset f k => Result.offset f (k+1)
| Result.num k => Result.num (k+1)
| f => Result.offset f 1
def Result.max : Result → Result → Result
| f, Result.maxNode Fs => Result.maxNode (f::Fs)
| f₁, f₂ => Result.maxNode [f₁, f₂]
| f, Result.maxNode Fs => Result.maxNode (f::Fs)
| f₁, f₂ => Result.maxNode [f₁, f₂]
def Result.imax : Result → Result → Result
| f, Result.imaxNode Fs => Result.imaxNode (f::Fs)
| f₁, f₂ => Result.imaxNode [f₁, f₂]
| f, Result.imaxNode Fs => Result.imaxNode (f::Fs)
| f₁, f₂ => Result.imaxNode [f₁, f₂]
def parenIfFalse : Format → Bool → Format
| f, true => f
| f, false => f.paren
| f, true => f
| f, false => f.paren
@[specialize] private def formatLst (fmt : Result → Format) : List Result → Format
| [] => Format.nil
| r::rs => Format.line ++ fmt r ++ formatLst fmt rs
| [] => Format.nil
| r::rs => Format.line ++ fmt r ++ formatLst fmt rs
partial def Result.format : Result → Bool → Format
| Result.leaf f, _ => f
| Result.num k, _ => toString k
| Result.offset f 0, r => format f r
| Result.offset f (k+1), r =>
let f' := format f false;
parenIfFalse (f' ++ "+" ++ fmt (k+1)) r
| Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst (fun r => format r false) fs) r
| Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst (fun r => format r false) fs) r
| Result.leaf f, _ => f
| Result.num k, _ => toString k
| Result.offset f 0, r => format f r
| Result.offset f (k+1), r =>
let f' := format f false;
parenIfFalse (f' ++ "+" ++ fmt (k+1)) r
| Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst (fun r => format r false) fs) r
| Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst (fun r => format r false) fs) r
def toResult : Level → Result
| zero _ => Result.num 0
| succ l _ => Result.succ (toResult l)
| max l₁ l₂ _ => Result.max (toResult l₁) (toResult l₂)
| imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂)
| param n _ => Result.leaf (fmt n)
| mvar n _ =>
let n := n.replacePrefix `_uniq `u;
Result.leaf ("?" ++ fmt n)
| zero _ => Result.num 0
| succ l _ => Result.succ (toResult l)
| max l₁ l₂ _ => Result.max (toResult l₁) (toResult l₂)
| imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂)
| param n _ => Result.leaf (fmt n)
| mvar n _ =>
let n := n.replacePrefix `_uniq `u;
Result.leaf ("?" ++ fmt n)
end LevelToFormat
protected def format (l : Level) : Format :=
(LevelToFormat.toResult l).format true
(LevelToFormat.toResult l).format true
instance : HasFormat Level := ⟨Level.format⟩
instance : HasToString Level := ⟨Format.pretty ∘ Level.format⟩
@ -427,47 +427,47 @@ instance : HasToString Level := ⟨Format.pretty ∘ Level.format⟩
@[extern "lean_level_update_succ"]
def updateSucc (lvl : Level) (newLvl : Level) (h : lvl.isSucc = true) : Level :=
mkLevelSucc newLvl
mkLevelSucc newLvl
@[inline] def updateSucc! (lvl : Level) (newLvl : Level) : Level :=
match lvl with
| succ lvl d => updateSucc (succ lvl d) newLvl rfl
| _ => panic! "succ level expected"
| succ lvl d => updateSucc (succ lvl d) newLvl rfl
| _ => panic! "succ level expected"
@[extern "lean_level_update_max"]
def updateMax (lvl : Level) (newLhs : Level) (newRhs : Level) (h : lvl.isMax = true) : Level :=
mkLevelMax newLhs newRhs
mkLevelMax newLhs newRhs
@[inline] def updateMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match lvl with
| max lhs rhs d => updateMax (max lhs rhs d) newLhs newRhs rfl
| _ => panic! "max level expected"
match lvl with
| max lhs rhs d => updateMax (max lhs rhs d) newLhs newRhs rfl
| _ => panic! "max level expected"
@[extern "lean_level_update_imax"]
def updateIMax (lvl : Level) (newLhs : Level) (newRhs : Level) (h : lvl.isIMax = true) : Level :=
mkLevelIMax newLhs newRhs
mkLevelIMax newLhs newRhs
@[inline] def updateIMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match lvl with
| imax lhs rhs d => updateIMax (imax lhs rhs d) newLhs newRhs rfl
| _ => panic! "imax level expected"
match lvl with
| imax lhs rhs d => updateIMax (imax lhs rhs d) newLhs newRhs rfl
| _ => panic! "imax level expected"
def mkNaryMax : List Level → Level
| [] => levelZero
| [u] => u
| u::us => mkLevelMax u (mkNaryMax us)
| [] => levelZero
| [u] => u
| u::us => mkLevelMax u (mkNaryMax us)
/- Level to Format -/
@[specialize] def instantiateParams (s : Name → Option Level) : Level → Level
| u@(zero _) => u
| u@(succ v _) => if u.hasParam then u.updateSucc! (instantiateParams s v) else u
| u@(max v₁ v₂ _) => if u.hasParam then u.updateMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(imax v₁ v₂ _) => if u.hasParam then u.updateIMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(param n _) => match s n with
| some u' => u'
| none => u
| u => u
| u@(zero _) => u
| u@(succ v _) => if u.hasParam then u.updateSucc! (instantiateParams s v) else u
| u@(max v₁ v₂ _) => if u.hasParam then u.updateMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(imax v₁ v₂ _) => if u.hasParam then u.updateIMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(param n _) => match s n with
| some u' => u'
| none => u
| u => u
end Level
@ -482,4 +482,4 @@ abbrev PLevelSet := PersistentLevelSet
end Lean
abbrev Nat.toLevel (n : Nat) : Lean.Level :=
Lean.Level.ofNat n
Lean.Level.ofNat n

42
src/Lean/Modifiers.lean
View file

@ -12,11 +12,11 @@ builtin_initialize protectedExt : TagDeclarationExtension ← mkTagDeclarationEx
@[export lean_add_protected]
def addProtected (env : Environment) (n : Name) : Environment :=
protectedExt.tag env n
protectedExt.tag env n
@[export lean_is_protected]
def isProtected (env : Environment) (n : Name) : Bool :=
protectedExt.isTagged env n
protectedExt.isTagged env n
builtin_initialize privateExt : EnvExtension Nat ← registerEnvExtension (pure 1)
@ -36,44 +36,44 @@ def privateHeader : Name := `_private
@[export lean_mk_private_prefix]
def mkUniquePrivatePrefix (env : Environment) : Environment × Name :=
let idx := privateExt.getState env
let p := mkNameNum (privateHeader ++ env.mainModule) idx
let env := privateExt.setState env (idx+1)
(env, p)
let idx := privateExt.getState env
let p := mkNameNum (privateHeader ++ env.mainModule) idx
let env := privateExt.setState env (idx+1)
(env, p)
@[export lean_mk_private_name]
def mkUniquePrivateName (env : Environment) (n : Name) : Environment × Name :=
let (env, p) := mkUniquePrivatePrefix env
(env, p ++ n)
let (env, p) := mkUniquePrivatePrefix env
(env, p ++ n)
def mkPrivateName (env : Environment) (n : Name) : Name :=
mkNameNum (privateHeader ++ env.mainModule) 0 ++ n
mkNameNum (privateHeader ++ env.mainModule) 0 ++ n
def isPrivateName : Name → Bool
| n@(Name.str p _ _) => n == privateHeader || isPrivateName p
| Name.num p _ _ => isPrivateName p
| _ => false
| n@(Name.str p _ _) => n == privateHeader || isPrivateName p
| Name.num p _ _ => isPrivateName p
| _ => false
@[export lean_is_private_name]
def isPrivateNameExport (n : Name) : Bool :=
isPrivateName n
isPrivateName n
private def privateToUserNameAux : Name → Name
| Name.str p s _ => mkNameStr (privateToUserNameAux p) s
| _ => Name.anonymous
| Name.str p s _ => mkNameStr (privateToUserNameAux p) s
| _ => Name.anonymous
@[export lean_private_to_user_name]
def privateToUserName? (n : Name) : Option Name :=
if isPrivateName n then privateToUserNameAux n
else none
if isPrivateName n then privateToUserNameAux n
else none
private def privatePrefixAux : Name → Name
| Name.str p _ _ => privatePrefixAux p
| n => n
| Name.str p _ _ => privatePrefixAux p
| n => n
@[export lean_private_prefix]
def privatePrefix (n : Name) : Option Name :=
if isPrivateName n then privatePrefixAux n
else none
if isPrivateName n then privatePrefixAux n
else none
end Lean

114
src/Lean/MonadEnv.lean
View file

@ -14,107 +14,107 @@ section Methods
variables {m : Type → Type} [MonadEnv m]
def setEnv (env : Environment) : m Unit :=
modifyEnv fun _ => env
modifyEnv fun _ => env
@[inline] def withoutModifyingEnv [Monad m] [MonadFinally m] {α : Type} (x : m α) : m α := do
let env ← getEnv
try x finally setEnv env
let env ← getEnv
try x finally setEnv env
@[inline] def matchConst [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : ConstantInfo → List Level → m α) : m α := do
match e with
| Expr.const constName us _ => do
match (← getEnv).find? constName with
| some cinfo => k cinfo us
| none => failK ()
| _ => failK ()
match e with
| Expr.const constName us _ => do
match (← getEnv).find? constName with
| some cinfo => k cinfo us
| none => failK ()
| _ => failK ()
@[inline] def matchConstInduct [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → m α) : m α :=
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.inductInfo val => k val us
| _ => failK ()
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.inductInfo val => k val us
| _ => failK ()
@[inline] def matchConstCtor [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : ConstructorVal → List Level → m α) : m α :=
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.ctorInfo val => k val us
| _ => failK ()
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.ctorInfo val => k val us
| _ => failK ()
@[inline] def matchConstRec [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : RecursorVal → List Level → m α) : m α :=
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.recInfo val => k val us
| _ => failK ()
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.recInfo val => k val us
| _ => failK ()
section
variables [Monad m]
def hasConst (constName : Name) : m Bool := do
return (← getEnv).contains constName
return (← getEnv).contains constName
private partial def mkAuxNameAux (env : Environment) (base : Name) (i : Nat) : Name :=
let candidate := base.appendIndexAfter i
if env.contains candidate then
mkAuxNameAux env base (i+1)
else
candidate
let candidate := base.appendIndexAfter i
if env.contains candidate then
mkAuxNameAux env base (i+1)
else
candidate
def mkAuxName (baseName : Name) (idx : Nat) : m Name := do
return mkAuxNameAux (← getEnv) baseName idx
return mkAuxNameAux (← getEnv) baseName idx
variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
def getConstInfo (constName : Name) : m ConstantInfo := do
match (← getEnv).find? constName with
| some info => pure info
| none => throwError! "unknown constant '{mkConst constName}'"
match (← getEnv).find? constName with
| some info => pure info
| none => throwError! "unknown constant '{mkConst constName}'"
def getConstInfoInduct (constName : Name) : m InductiveVal := do
match (← getConstInfo constName) with
| ConstantInfo.inductInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a inductive type"
match (← getConstInfo constName) with
| ConstantInfo.inductInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a inductive type"
def getConstInfoCtor (constName : Name) : m ConstructorVal := do
match (← getConstInfo constName) with
| ConstantInfo.ctorInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a constructor"
match (← getConstInfo constName) with
| ConstantInfo.ctorInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a constructor"
def getConstInfoRec (constName : Name) : m RecursorVal := do
match (← getConstInfo constName) with
| ConstantInfo.recInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a recursor"
match (← getConstInfo constName) with
| ConstantInfo.recInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a recursor"
@[inline] def matchConstStruct {α : Type} (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → ConstructorVal → m α) : m α :=
matchConstInduct e failK fun ival us => do
if ival.isRec then failK ()
else match ival.ctors with
| [ctor] =>
match (← getConstInfo ctor) with
| ConstantInfo.ctorInfo cval => k ival us cval
matchConstInduct e failK fun ival us => do
if ival.isRec then failK ()
else match ival.ctors with
| [ctor] =>
match (← getConstInfo ctor) with
| ConstantInfo.ctorInfo cval => k ival us cval
| _ => failK ()
| _ => failK ()
| _ => failK ()
def addDecl [MonadOptions m] (decl : Declaration) : m Unit := do
match (← getEnv).addDecl decl with
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
match (← getEnv).addDecl decl with
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
def compileDecl [MonadOptions m] (decl : Declaration) : m Unit := do
match (← getEnv).compileDecl (← getOptions) decl with
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
match (← getEnv).compileDecl (← getOptions) decl with
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
def addAndCompile [MonadOptions m] (decl : Declaration) : m Unit := do
addDecl decl;
compileDecl decl
addDecl decl;
compileDecl decl
variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] [MonadOptions m]
unsafe def evalConst (α) (constName : Name) : m α := do
ofExcept $ (← getEnv).evalConst α (← getOptions) constName
ofExcept $ (← getEnv).evalConst α (← getOptions) constName
unsafe def evalConstCheck (α) (typeName : Name) (constName : Name) : m α := do
ofExcept $ (← getEnv).evalConstCheck α (← getOptions) typeName constName
ofExcept $ (← getEnv).evalConstCheck α (← getOptions) typeName constName
end

50
src/Lean/PrettyPrinter.lean
View file

@ -12,51 +12,51 @@ import Lean.Parser.Module
namespace Lean
def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env }
Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env }
def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
ppCtx.runCoreM $ x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
ppCtx.runCoreM $ x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
namespace PrettyPrinter
def ppTerm (stx : Syntax) : CoreM Format := do
let opts ← getOptions
let stx := (sanitizeSyntax stx).run' { options := opts }
parenthesizeTerm stx >>= formatTerm
let opts ← getOptions
let stx := (sanitizeSyntax stx).run' { options := opts }
parenthesizeTerm stx >>= formatTerm
def ppExpr (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) : MetaM Format := do
let lctx ← getLCtx
let opts ← getOptions
let lctx := lctx.sanitizeNames.run' { options := opts }
Meta.withLCtx lctx #[] do
let stx ← delab currNamespace openDecls e
ppTerm stx
let lctx ← getLCtx
let opts ← getOptions
let lctx := lctx.sanitizeNames.run' { options := opts }
Meta.withLCtx lctx #[] do
let stx ← delab currNamespace openDecls e
ppTerm stx
@[export lean_pp_expr]
def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
Prod.fst <$> ((ppExpr Name.anonymous [] e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts } { env := env }
Prod.fst <$> ((ppExpr Name.anonymous [] e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts } { env := env }
def ppCommand (stx : Syntax) : CoreM Format :=
parenthesizeCommand stx >>= formatCommand
parenthesizeCommand stx >>= formatCommand
def ppModule (stx : Syntax) : CoreM Format := do
parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter
parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter
private partial def noContext : MessageData → MessageData
| MessageData.withContext ctx msg => noContext msg
| MessageData.withNamingContext ctx msg => MessageData.withNamingContext ctx (noContext msg)
| MessageData.nest n msg => MessageData.nest n (noContext msg)
| MessageData.group msg => MessageData.group (noContext msg)
| MessageData.compose msg₁ msg₂ => MessageData.compose (noContext msg₁) (noContext msg₂)
| MessageData.tagged tag msg => MessageData.tagged tag (noContext msg)
| MessageData.node msgs => MessageData.node (msgs.map noContext)
| msg => msg
| MessageData.withContext ctx msg => noContext msg
| MessageData.withNamingContext ctx msg => MessageData.withNamingContext ctx (noContext msg)
| MessageData.nest n msg => MessageData.nest n (noContext msg)
| MessageData.group msg => MessageData.group (noContext msg)
| MessageData.compose msg₁ msg₂ => MessageData.compose (noContext msg₁) (noContext msg₂)
| MessageData.tagged tag msg => MessageData.tagged tag (noContext msg)
| MessageData.node msgs => MessageData.node (msgs.map noContext)
| msg => msg
-- strip context (including environments with registered pretty printers) to prevent infinite recursion when pretty printing pretty printer error
private def withoutContext {m} [MonadExcept Exception m] (x : m Format) : m Format :=
tryCatch x fun
| Exception.error ref msg => throw $ Exception.error ref (noContext msg)
| ex => throw ex
tryCatch x fun
| Exception.error ref msg => throw $ Exception.error ref (noContext msg)
| ex => throw ex
builtin_initialize
ppFnsRef.set {

46
src/Lean/ProjFns.lean
View file

@ -11,19 +11,19 @@ namespace Lean
/- Given a structure `S`, Lean automatically creates an auxiliary definition (projection function)
for each field. This structure caches information about these auxiliary definitions. -/
structure ProjectionFunctionInfo :=
(ctorName : Name) -- Constructor associated with the auxiliary projection function.
(nparams : Nat) -- Number of parameters in the structure
(i : Nat) -- The field index associated with the auxiliary projection function.
(fromClass : Bool) -- `true` if the structure is a class
(ctorName : Name) -- Constructor associated with the auxiliary projection function.
(nparams : Nat) -- Number of parameters in the structure
(i : Nat) -- The field index associated with the auxiliary projection function.
(fromClass : Bool) -- `true` if the structure is a class
@[export lean_mk_projection_info]
def mkProjectionInfoEx (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo :=
{ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass }
{ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass }
@[export lean_projection_info_from_class]
def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass
def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass
instance : Inhabited ProjectionFunctionInfo :=
⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩
⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩
builtin_initialize projectionFnInfoExt : SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo) ←
registerSimplePersistentEnvExtension {
@ -35,32 +35,32 @@ builtin_initialize projectionFnInfoExt : SimplePersistentEnvExtension (Name × P
@[export lean_add_projection_info]
def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
projectionFnInfoExt.addEntry env (projName, { ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass })
projectionFnInfoExt.addEntry env (projName, { ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass })
namespace Environment
@[export lean_get_projection_info]
def getProjectionFnInfo? (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
match env.getModuleIdxFor? projName with
| some modIdx =>
match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some e => some e.2
| none => none
| none => (projectionFnInfoExt.getState env).find? projName
match env.getModuleIdxFor? projName with
| some modIdx =>
match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some e => some e.2
| none => none
| none => (projectionFnInfoExt.getState env).find? projName
def isProjectionFn (env : Environment) (n : Name) : Bool :=
match env.getModuleIdxFor? n with
| some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, arbitrary _) (fun a b => Name.quickLt a.1 b.1)
| none => (projectionFnInfoExt.getState env).contains n
match env.getModuleIdxFor? n with
| some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, arbitrary _) (fun a b => Name.quickLt a.1 b.1)
| none => (projectionFnInfoExt.getState env).contains n
/-- If `projName` is the name of a projection function, return the associated structure name -/
def getProjectionStructureName? (env : Environment) (projName : Name) : Option Name :=
match env.getProjectionFnInfo? projName with
| none => none
| some projInfo =>
match env.find? projInfo.ctorName with
| some (ConstantInfo.ctorInfo val) => some val.induct
| _ => none
match env.getProjectionFnInfo? projName with
| none => none
| some projInfo =>
match env.find? projInfo.ctorName with
| some (ConstantInfo.ctorInfo val) => some val.induct
| _ => none
end Environment
end Lean

20
src/Lean/ReducibilityAttrs.lean
View file

@ -9,7 +9,7 @@ import Lean.Attributes
namespace Lean
inductive ReducibilityStatus
| reducible | semireducible | irreducible
| reducible | semireducible | irreducible
instance : Inhabited ReducibilityStatus := ⟨ReducibilityStatus.semireducible⟩
@ -21,19 +21,19 @@ builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ←
@[export lean_get_reducibility_status]
def getReducibilityStatus (env : Environment) (n : Name) : ReducibilityStatus :=
match reducibilityAttrs.getValue env n with
| some s => s
| none => ReducibilityStatus.semireducible
match reducibilityAttrs.getValue env n with
| some s => s
| none => ReducibilityStatus.semireducible
@[export lean_set_reducibility_status]
def setReducibilityStatus (env : Environment) (n : Name) (s : ReducibilityStatus) : Environment :=
match reducibilityAttrs.setValue env n s with
| Except.ok env => env
| _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails
match reducibilityAttrs.setValue env n s with
| Except.ok env => env
| _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails
def isReducible (env : Environment) (n : Name) : Bool :=
match getReducibilityStatus env n with
| ReducibilityStatus.reducible => true
| _ => false
match getReducibilityStatus env n with
| ReducibilityStatus.reducible => true
| _ => false
end Lean

185
src/Lean/ResolveName.lean
View file

@ -18,9 +18,9 @@ abbrev AliasState := SMap Name (List Name)
abbrev AliasEntry := Name × Name
def addAliasEntry (s : AliasState) (e : AliasEntry) : AliasState :=
match s.find? e.1 with
| none => s.insert e.1 [e.2]
| some es => if es.elem e.2 then s else s.insert e.1 (e.2 :: es)
match s.find? e.1 with
| none => s.insert e.1 [e.2]
| some es => if es.elem e.2 then s else s.insert e.1 (e.2 :: es)
builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState ←
registerSimplePersistentEnvExtension {
@ -31,101 +31,101 @@ builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry Alia
/- Add alias `a` for `e` -/
@[export lean_add_alias] def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
aliasExtension.addEntry env (a, e)
aliasExtension.addEntry env (a, e)
def getAliases (env : Environment) (a : Name) : List Name :=
match aliasExtension.getState env $.find? a with
| none => []
| some es => es
match aliasExtension.getState env $.find? a with
| none => []
| some es => es
-- slower, but only used in the pretty printer
def getRevAliases (env : Environment) (e : Name) : List Name :=
(aliasExtension.getState env).fold (fun as a es => if List.contains es e then a :: as else as) []
(aliasExtension.getState env).fold (fun as a es => if List.contains es e then a :: as else as) []
/- Global name resolution -/
namespace ResolveName
/- Check whether `ns ++ id` is a valid namepace name and/or there are aliases names `ns ++ id`. -/
private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name :=
let resolvedId := ns ++ id
let resolvedIds := getAliases env resolvedId
if env.contains resolvedId && (!id.isAtomic || !isProtected env resolvedId) then
resolvedId :: resolvedIds
else
-- Check whether environment contains the private version. That is, `_private.<module_name>.ns.id`.
let resolvedIdPrv := mkPrivateName env resolvedId
if env.contains resolvedIdPrv then resolvedIdPrv :: resolvedIds
else resolvedIds
let resolvedId := ns ++ id
let resolvedIds := getAliases env resolvedId
if env.contains resolvedId && (!id.isAtomic || !isProtected env resolvedId) then
resolvedId :: resolvedIds
else
-- Check whether environment contains the private version. That is, `_private.<module_name>.ns.id`.
let resolvedIdPrv := mkPrivateName env resolvedId
if env.contains resolvedIdPrv then resolvedIdPrv :: resolvedIds
else resolvedIds
/- Check surrounding namespaces -/
private def resolveUsingNamespace (env : Environment) (id : Name) : Name → List Name
| ns@(Name.str p _ _) =>
match resolveQualifiedName env ns id with
| [] => resolveUsingNamespace env id p
| resolvedIds => resolvedIds
| _ => []
| ns@(Name.str p _ _) =>
match resolveQualifiedName env ns id with
| [] => resolveUsingNamespace env id p
| resolvedIds => resolvedIds
| _ => []
/- Check exact name -/
private def resolveExact (env : Environment) (id : Name) : Option Name :=
if id.isAtomic then none
else
let resolvedId := id.replacePrefix rootNamespace Name.anonymous
if env.contains resolvedId then some resolvedId
if id.isAtomic then none
else
-- We also allow `_root` when accessing private declarations.
-- If we change our minds, we should just replace `resolvedId` with `id`
let resolvedIdPrv := mkPrivateName env resolvedId
if env.contains resolvedIdPrv then some resolvedIdPrv
else none
let resolvedId := id.replacePrefix rootNamespace Name.anonymous
if env.contains resolvedId then some resolvedId
else
-- We also allow `_root` when accessing private declarations.
-- If we change our minds, we should just replace `resolvedId` with `id`
let resolvedIdPrv := mkPrivateName env resolvedId
if env.contains resolvedIdPrv then some resolvedIdPrv
else none
/- Check open namespaces -/
private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → List Name → List Name
| [], resolvedIds => resolvedIds
| OpenDecl.simple ns exs :: openDecls, resolvedIds =>
if exs.elem id then
| [], resolvedIds => resolvedIds
| OpenDecl.simple ns exs :: openDecls, resolvedIds =>
if exs.elem id then
resolveOpenDecls env id openDecls resolvedIds
else
let newResolvedIds := resolveQualifiedName env ns id
resolveOpenDecls env id openDecls (newResolvedIds ++ resolvedIds)
| OpenDecl.explicit openedId resolvedId :: openDecls, resolvedIds =>
let resolvedIds := if id == openedId then resolvedId :: resolvedIds else resolvedIds
resolveOpenDecls env id openDecls resolvedIds
else
let newResolvedIds := resolveQualifiedName env ns id
resolveOpenDecls env id openDecls (newResolvedIds ++ resolvedIds)
| OpenDecl.explicit openedId resolvedId :: openDecls, resolvedIds =>
let resolvedIds := if id == openedId then resolvedId :: resolvedIds else resolvedIds
resolveOpenDecls env id openDecls resolvedIds
def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List (Name × List String) :=
-- decode macro scopes from name before recursion
let extractionResult := extractMacroScopes id
let rec loop : Name → List String → List (Name × List String)
| id@(Name.str p s _), projs =>
-- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
let id := { extractionResult with name := id }.review
match resolveUsingNamespace env id ns with
| resolvedIds@(_ :: _) => resolvedIds.eraseDups.map fun id => (id, projs)
| [] =>
match resolveExact env id with
| some newId => [(newId, projs)]
| none =>
let resolvedIds := if env.contains id then [id] else []
let idPrv := mkPrivateName env id
let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds
let resolvedIds := resolveOpenDecls env id openDecls resolvedIds
let resolvedIds := getAliases env id ++ resolvedIds
match resolvedIds with
| _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs)
| [] => loop p (s::projs)
| _, _ => []
loop extractionResult.name []
-- decode macro scopes from name before recursion
let extractionResult := extractMacroScopes id
let rec loop : Name → List String → List (Name × List String)
| id@(Name.str p s _), projs =>
-- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
let id := { extractionResult with name := id }.review
match resolveUsingNamespace env id ns with
| resolvedIds@(_ :: _) => resolvedIds.eraseDups.map fun id => (id, projs)
| [] =>
match resolveExact env id with
| some newId => [(newId, projs)]
| none =>
let resolvedIds := if env.contains id then [id] else []
let idPrv := mkPrivateName env id
let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds
let resolvedIds := resolveOpenDecls env id openDecls resolvedIds
let resolvedIds := getAliases env id ++ resolvedIds
match resolvedIds with
| _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs)
| [] => loop p (s::projs)
| _, _ => []
loop extractionResult.name []
/- Namespace resolution -/
def resolveNamespaceUsingScope (env : Environment) (n : Name) : Name → Option Name
| Name.anonymous => none
| ns@(Name.str p _ _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope env n p
| _ => unreachable!
| Name.anonymous => none
| ns@(Name.str p _ _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope env n p
| _ => unreachable!
def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → Option Name
| [] => none
| OpenDecl.simple ns [] :: ds => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls env n ds
| _ :: ds => resolveNamespaceUsingOpenDecls env n ds
| [] => none
| OpenDecl.simple ns [] :: ds => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls env n ds
| _ :: ds => resolveNamespaceUsingOpenDecls env n ds
/-
Given a name `id` try to find namespace it refers to. The resolution procedure works as follows
@ -136,24 +136,25 @@ Given a name `id` try to find namespace it refers to. The resolution procedure w
We search "backwards" again. That is, we try the most recent `open` command first.
We only consider simple `open` commands. -/
def resolveNamespace? (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : Option Name :=
if env.isNamespace id then some id
else match resolveNamespaceUsingScope env id ns with
| some n => some n
| none =>
match resolveNamespaceUsingOpenDecls env id openDecls with
if env.isNamespace id then some id
else match resolveNamespaceUsingScope env id ns with
| some n => some n
| none => none
end ResolveName
| none =>
match resolveNamespaceUsingOpenDecls env id openDecls with
| some n => some n
| none => none
end ResolveName
class MonadResolveName (m : Type → Type) :=
(getCurrNamespace : m Name)
(getOpenDecls : m (List OpenDecl))
(getCurrNamespace : m Name)
(getOpenDecls : m (List OpenDecl))
export MonadResolveName (getCurrNamespace getOpenDecls)
instance (m n) [MonadResolveName m] [MonadLift m n] : MonadResolveName n :=
{ getCurrNamespace := liftM (getCurrNamespace : m _),
getOpenDecls := liftM (getOpenDecls : m _) }
instance (m n) [MonadResolveName m] [MonadLift m n] : MonadResolveName n := {
getCurrNamespace := liftM (getCurrNamespace : m _),
getOpenDecls := liftM (getOpenDecls : m _)
}
section Methods
@ -182,27 +183,27 @@ variables {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m]
- `resolveGlobalName x.z.w` => `[(Foo.x, [z, w]), (Boo.x, [z, w])]`
-/
def resolveGlobalName (id : Name) : m (List (Name × List String)) := do
return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
def resolveNamespace (id : Name) : m Name := do
match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with
| some ns => return ns
| none => throwError s!"unknown namespace '{id}'"
match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with
| some ns => return ns
| none => throwError s!"unknown namespace '{id}'"
/- Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty. -/
def resolveGlobalConst (n : Name) : m (List Name) := do
let cs ← resolveGlobalName n
let cs := cs.filter fun (_, fieldList) => fieldList.isEmpty
if cs.isEmpty then throwUnknownConstant n
return cs.map (·.1)
let cs ← resolveGlobalName n
let cs := cs.filter fun (_, fieldList) => fieldList.isEmpty
if cs.isEmpty then throwUnknownConstant n
return cs.map (·.1)
def resolveGlobalConstNoOverload (n : Name) : m Name := do
let cs ← resolveGlobalConst n
match cs with
| [c] => pure c
| _ => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}"
let cs ← resolveGlobalConst n
match cs with
| [c] => pure c
| _ => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}"
end Methods
end Lean