Lean.MonadEnv

source

def Lean.setEnv {m : Type → Type} [inst : Lean.MonadEnv m] (env : Lean.Environment) :

m Unit

Equations

Lean.setEnv env = Lean.modifyEnv fun x => env

source

def Lean.isInductive {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) :

m Bool

Equations

Lean.isInductive declName = do let a ← Lean.getEnv match Lean.Environment.find? a declName with | some (Lean.ConstantInfo.inductInfo x) => pure true | x => pure false

source

def Lean.isRecCore (env : Lean.Environment) (declName : Lean.Name) :

Bool

Equations

Lean.isRecCore env declName = match Lean.Environment.find? env declName with | some (Lean.ConstantInfo.recInfo x) => true | x => false

source

def Lean.isRec {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) :

m Bool

Equations

Lean.isRec declName = do let a ← Lean.getEnv pure (Lean.isRecCore a declName)

source

@[inline]

def Lean.withoutModifyingEnv {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : MonadFinally m] {α : Type} (x : m α) :

m α

Equations

Lean.withoutModifyingEnv x = do let env ← Lean.getEnv tryFinally x (Lean.setEnv env)

source

@[inline]

def Lean.matchConst {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadEnv m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.ConstantInfo → List Lean.Level → m α) :

m α

Equations

Lean.matchConst e failK k = match e with | Lean.Expr.const constName us x => do let a ← Lean.getEnv match Lean.Environment.find? a constName with | some cinfo => k cinfo us | none => failK () | x => failK ()

source

@[inline]

def Lean.matchConstInduct {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadEnv m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.InductiveVal → List Lean.Level → m α) :

m α

Equations

Lean.matchConstInduct e failK k = Lean.matchConst e failK fun cinfo us => match cinfo with | Lean.ConstantInfo.inductInfo val => k val us | x => failK ()

source

@[inline]

def Lean.matchConstCtor {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadEnv m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.ConstructorVal → List Lean.Level → m α) :

m α

Equations

Lean.matchConstCtor e failK k = Lean.matchConst e failK fun cinfo us => match cinfo with | Lean.ConstantInfo.ctorInfo val => k val us | x => failK ()

source

@[inline]

def Lean.matchConstRec {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadEnv m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.RecursorVal → List Lean.Level → m α) :

m α

Equations

Lean.matchConstRec e failK k = Lean.matchConst e failK fun cinfo us => match cinfo with | Lean.ConstantInfo.recInfo val => k val us | x => failK ()

source

def Lean.hasConst {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (constName : Lean.Name) :

m Bool

Equations

Lean.hasConst constName = do let a ← Lean.getEnv pure (Lean.Environment.contains a constName)

source

def Lean.mkAuxName {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (baseName : Lean.Name) (idx : Nat) :

m Lean.Name

Equations

Lean.mkAuxName baseName idx = do let a ← Lean.getEnv pure (Lean.mkAuxNameAux a baseName idx)

source

def Lean.getConstInfo {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (constName : Lean.Name) :

m Lean.ConstantInfo

Equations

Lean.getConstInfo constName = do let a ← Lean.getEnv match Lean.Environment.find? a constName with | some info => pure info | none => Lean.throwError (Lean.toMessageData "unknown constant '" ++ Lean.toMessageData (Lean.mkConst constName) ++ Lean.toMessageData "'")

source

def Lean.mkConstWithLevelParams {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (constName : Lean.Name) :

m Lean.Expr

Equations

Lean.mkConstWithLevelParams constName = do let info ← Lean.getConstInfo constName pure (Lean.mkConst constName (List.map Lean.mkLevelParam (Lean.ConstantInfo.levelParams info)))

source

def Lean.getConstInfoInduct {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (constName : Lean.Name) :

m Lean.InductiveVal

Equations

Lean.getConstInfoInduct constName = do let a ← Lean.getConstInfo constName match a with | Lean.ConstantInfo.inductInfo v => pure v | x => Lean.throwError (Lean.toMessageData "'" ++ Lean.toMessageData (Lean.mkConst constName) ++ Lean.toMessageData "' is not a inductive type")

source

def Lean.getConstInfoCtor {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (constName : Lean.Name) :

m Lean.ConstructorVal

Equations

Lean.getConstInfoCtor constName = do let a ← Lean.getConstInfo constName match a with | Lean.ConstantInfo.ctorInfo v => pure v | x => Lean.throwError (Lean.toMessageData "'" ++ Lean.toMessageData (Lean.mkConst constName) ++ Lean.toMessageData "' is not a constructor")

source

def Lean.getConstInfoRec {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (constName : Lean.Name) :

m Lean.RecursorVal

Equations

Lean.getConstInfoRec constName = do let a ← Lean.getConstInfo constName match a with | Lean.ConstantInfo.recInfo v => pure v | x => Lean.throwError (Lean.toMessageData "'" ++ Lean.toMessageData (Lean.mkConst constName) ++ Lean.toMessageData "' is not a recursor")

source

@[inline]

def Lean.matchConstStruct {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (e : Lean.Expr) (failK : Unit → m α) (k : Lean.InductiveVal → List Lean.Level → Lean.ConstructorVal → m α) :

m α

Equations

Lean.matchConstStruct e failK k = Lean.matchConstInduct e failK fun ival us => if (ival.isRec || ival.numIndices != 0) = true then failK () else match ival.ctors with | [ctor] => do let a ← Lean.getConstInfo ctor match a with | Lean.ConstantInfo.ctorInfo cval => k ival us cval | x => failK () | x => failK ()

source

def Lean.addDecl {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (decl : Lean.Declaration) :

m Unit

Equations

Lean.addDecl decl = do let a ← Lean.getEnv match Lean.Environment.addDecl a decl with | Except.ok env => Lean.setEnv env | Except.error ex => Lean.throwKernelException ex

source

def Lean.compileDecl {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (decl : Lean.Declaration) :

m Unit

Equations

Lean.compileDecl decl = do let a ← Lean.getEnv let a_1 ← Lean.getOptions match Lean.Environment.compileDecl a a_1 decl with | Except.ok env => Lean.setEnv env | Except.error (Lean.KernelException.other msg) => do Lean.checkUnsupported decl Lean.throwError (Function.comp Lean.MessageData.ofFormat Lean.format msg) | Except.error ex => Lean.throwKernelException ex

source

def Lean.addAndCompile {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (decl : Lean.Declaration) :

m Unit

Equations

Lean.addAndCompile decl = do Lean.addDecl decl Lean.compileDecl decl

source

unsafe def Lean.evalConst {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (α : Type) (constName : Lean.Name) :

m α

Equations

Lean.evalConst α constName = do let a ← Lean.getEnv let a_1 ← Lean.getOptions Lean.ofExcept (Lean.Environment.evalConst α a a_1 constName)

source

unsafe def Lean.evalConstCheck {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (α : Type) (typeName : Lean.Name) (constName : Lean.Name) :

m α

Equations

Lean.evalConstCheck α typeName constName = do let a ← Lean.getEnv let a_1 ← Lean.getOptions Lean.ofExcept (Lean.Environment.evalConstCheck α a a_1 typeName constName)

source

def Lean.findModuleOf? {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (declName : Lean.Name) :

m (Option Lean.Name)

Equations

Lean.findModuleOf? declName = do discard (Lean.getConstInfo declName) let a ← Lean.getEnv match Lean.Environment.getModuleIdxFor? a declName with | none => pure none | some modIdx => do let a ← Lean.getEnv pure (some (Array.getOp (Lean.Environment.allImportedModuleNames a) modIdx))

source

def Lean.isEnumType {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (declName : Lean.Name) :

m Bool

Equations

Lean.isEnumType declName = do let a ← Lean.getConstInfo declName match a with | Lean.ConstantInfo.inductInfo info => if (!Lean.Expr.isProp info.toConstantVal.type && List.length info.all == 1 && info.numIndices == 0 && info.numParams == 0 && !List.isEmpty info.ctors && !info.isRec && !info.isNested && !info.isUnsafe) = true then List.allM (fun ctorName => do let discr ← Lean.getConstInfo ctorName match discr with | Lean.ConstantInfo.ctorInfo info => pure (info.numFields == 0) | x => pure false) info.ctors else pure false | x => pure false