diff --git a/stage0/src/Init/Meta.lean b/stage0/src/Init/Meta.lean
index 1a279f6278..2ce23b8dcb 100644
--- a/stage0/src/Init/Meta.lean
+++ b/stage0/src/Init/Meta.lean
@@ -794,4 +794,5 @@ def expandInterpolatedStr (interpStr : Syntax) (type : Syntax) (toTypeFn : Synta
def getSepArgs (stx : Syntax) : Array Syntax :=
stx.getArgs.getSepElems
-end Lean.Syntax
+end Syntax
+end Lean
diff --git a/stage0/src/Lean/Elab/Command.lean b/stage0/src/Lean/Elab/Command.lean
index 6d8eeb9e7c..a46cf84e38 100644
--- a/stage0/src/Lean/Elab/Command.lean
+++ b/stage0/src/Lean/Elab/Command.lean
@@ -121,7 +121,8 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M
let ctx ← read
IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x
-instance : MonadLiftT IO CommandElabM := { monadLift := liftIO }
+instance : MonadLiftT IO CommandElabM where
+ monadLift := liftIO
def getScope : CommandElabM Scope := do pure (← get).scopes.head!
diff --git a/stage0/src/Lean/Elab/DeclUtil.lean b/stage0/src/Lean/Elab/DeclUtil.lean
index 67b6f16fdb..ce0c7ad3ec 100644
--- a/stage0/src/Lean/Elab/DeclUtil.lean
+++ b/stage0/src/Lean/Elab/DeclUtil.lean
@@ -17,7 +17,7 @@ def forallTelescopeCompatibleAux {α} (k : Array Expr → Expr → Expr → Meta
unless n₁ == n₂ do
throwError! "parameter name mismatch '{n₁}', expected '{n₂}'"
unless (← isDefEq d₁ d₂) do
- throwError! "type mismatch at parameter '{n₁}'{indentExpr d₁}\nexpected type{indentExpr d₂}"
+ throwError! "parameter '{n₁}' {← mkHasTypeButIsExpectedMsg d₁ d₂}"
unless c₁.binderInfo == c₂.binderInfo do
throwError! "binder annotation mismatch at parameter '{n₁}'"
withLocalDecl n₁ c₁.binderInfo d₁ fun x =>
diff --git a/stage0/src/Lean/Elab/Deriving.lean b/stage0/src/Lean/Elab/Deriving.lean
index bbca818a5f..de069d1c17 100644
--- a/stage0/src/Lean/Elab/Deriving.lean
+++ b/stage0/src/Lean/Elab/Deriving.lean
@@ -7,3 +7,4 @@ import Lean.Elab.Deriving.Basic
import Lean.Elab.Deriving.Util
import Lean.Elab.Deriving.Inhabited
import Lean.Elab.Deriving.BEq
+import Lean.Elab.Deriving.DecEq
diff --git a/stage0/src/Lean/Elab/Deriving/BEq.lean b/stage0/src/Lean/Elab/Deriving/BEq.lean
index ff59524da0..3f9169b031 100644
--- a/stage0/src/Lean/Elab/Deriving/BEq.lean
+++ b/stage0/src/Lean/Elab/Deriving/BEq.lean
@@ -11,44 +11,16 @@ namespace Lean.Elab.Deriving.BEq
open Lean.Parser.Term
open Meta
-structure Header where
- binders : Array Syntax
- argNames : Array Name
- target1Name : Name
- target2Name : Name
+open Binary (Header mkDiscrs)
def mkHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
- let argNames ← mkInductArgNames indVal
- let binders ← mkImplicitBinders argNames
- let targetType ← mkInductiveApp indVal argNames
- let target1Name ← mkFreshUserName `x
- let target2Name ← mkFreshUserName `y
- let binders := binders ++ (← mkInstImplicitBinders `BEq indVal argNames)
- let target1Binder ← `(explicitBinderF| ($(mkIdent target1Name) : $targetType))
- let target2Binder ← `(explicitBinderF| ($(mkIdent target2Name) : $targetType))
- let binders := binders ++ #[target1Binder, target2Binder]
- return {
- binders := binders
- argNames := argNames
- target1Name := target1Name
- target2Name := target2Name
- }
+ Binary.mkHeader ctx `BEq indVal
-def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) (argNames : Array Name) : TermElabM Syntax := do
- let discrs ← mkDiscrs
+def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
+ let discrs ← mkDiscrs header indVal
let alts ← mkAlts
`(match $[$discrs],* with $alts:matchAlt*)
where
- mkDiscr (varName : Name) : TermElabM Syntax :=
- `(Parser.Term.matchDiscr| $(mkIdent varName):term)
-
- mkDiscrs : TermElabM (Array Syntax) := do
- let mut discrs := #[]
- -- add indices
- for argName in argNames[indVal.nparams:] do
- discrs := discrs.push (← mkDiscr argName)
- return discrs ++ #[← mkDiscr header.target1Name, ← mkDiscr header.target2Name]
-
mkElseAlt : TermElabM Syntax := do
let mut patterns := #[]
-- add `_` pattern for indices
@@ -102,7 +74,7 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
let auxFunName ← ctx.auxFunNames[i]
let indVal ← ctx.typeInfos[i]
let header ← mkHeader ctx indVal
- let mut body ← mkMatch ctx header indVal auxFunName header.argNames
+ let mut body ← mkMatch ctx header indVal auxFunName
if ctx.usePartial then
let letDecls ← mkLocalInstanceLetDecls ctx `BEq header.argNames
body ← mkLet letDecls body
@@ -122,7 +94,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
end)
private def mkBEqInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
- let ctx ← mkContext declNames[0]
+ let ctx ← mkContext "beq" declNames[0]
let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq declNames)
trace[Elab.Deriving.beq]! "\n{cmds}"
return cmds
diff --git a/stage0/src/Lean/Elab/Deriving/DecEq.lean b/stage0/src/Lean/Elab/Deriving/DecEq.lean
new file mode 100644
index 0000000000..73237d8581
--- /dev/null
+++ b/stage0/src/Lean/Elab/Deriving/DecEq.lean
@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Transform
+import Lean.Meta.Inductive
+import Lean.Elab.Deriving.Basic
+import Lean.Elab.Deriving.Util
+
+namespace Lean.Elab.Deriving.DecEq
+open Lean.Parser.Term
+open Meta
+open Binary (Header mkDiscrs)
+
+def mkHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
+ Binary.mkHeader ctx `DecidableEq indVal
+
+def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) (argNames : Array Name) : TermElabM Syntax := do
+ let discrs ← mkDiscrs header indVal
+ let alts ← mkAlts
+ `(match $[$discrs],* with $alts:matchAlt*)
+where
+ mkSameCtorRhs : List (Syntax × Syntax × Bool) → TermElabM Syntax
+ | [] => `(isTrue rfl)
+ | (a, b, false) :: todo => withFreshMacroScope do
+ `(if h : $a = $b then
+ by subst h; exact $(← mkSameCtorRhs todo):term
+ else
+ isFalse (by intro n; injection n; apply h _; assumption))
+ | (a, b, true) :: todo => withFreshMacroScope do
+ `(@dite _ _ ($(mkIdent auxFunName) $a $b)
+ (fun h => by subst h; exact $(← mkSameCtorRhs todo):term)
+ (fun h => isFalse (by intro n; injection n; apply h _; assumption)))
+
+ mkAlts : TermElabM (Array Syntax) := do
+ let mut alts := #[]
+ for ctorName₁ in indVal.ctors do
+ let ctorInfo ← getConstInfoCtor ctorName₁
+ for ctorName₂ in indVal.ctors do
+ let mut patterns := #[]
+ -- add `_` pattern for indices
+ for i in [:indVal.nindices] do
+ patterns := patterns.push (← `(_))
+ if ctorName₁ == ctorName₂ then
+ let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do
+ let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
+ let mut patterns := patterns
+ let mut ctorArgs1 := #[]
+ let mut ctorArgs2 := #[]
+ -- add `_` for inductive parameters, they are inaccessible
+ for i in [:indVal.nparams] do
+ ctorArgs1 := ctorArgs1.push (← `(_))
+ ctorArgs2 := ctorArgs2.push (← `(_))
+ let mut todo := #[]
+ for i in [:ctorInfo.nfields] do
+ let x := xs[indVal.nparams + i]
+ if type.containsFVar x.fvarId! then
+ -- If resulting type depends on this field, we don't need to compare
+ ctorArgs1 := ctorArgs1.push (← `(_))
+ ctorArgs2 := ctorArgs2.push (← `(_))
+ else
+ let a := mkIdent (← mkFreshUserName `a)
+ let b := mkIdent (← mkFreshUserName `b)
+ ctorArgs1 := ctorArgs1.push a
+ ctorArgs2 := ctorArgs2.push b
+ let recField := (← inferType x).isAppOf indVal.name
+ todo := todo.push (a, b, recField)
+ patterns := patterns.push (← `(@$(mkIdent ctorName₁):ident $ctorArgs1:term*))
+ patterns := patterns.push (← `(@$(mkIdent ctorName₁):ident $ctorArgs2:term*))
+ let rhs ← mkSameCtorRhs todo.toList
+ `(matchAltExpr| | $[$patterns:term],* => $rhs:term)
+ alts := alts.push alt
+ else if (← compatibleCtors ctorName₁ ctorName₂) then
+ patterns := patterns ++ #[(← `($(mkIdent ctorName₁) ..)), (← `($(mkIdent ctorName₂) ..))]
+ let rhs ← `(isFalse (by intro h; injection h))
+ alts ← alts.push (← `(matchAltExpr| | $[$patterns:term],* => $rhs:term))
+ return alts
+
+def mkAuxFunction (ctx : Context) : TermElabM Syntax := do
+ let auxFunName ← ctx.auxFunNames[0]
+ let indVal ← ctx.typeInfos[0]
+ let header ← mkHeader ctx indVal
+ let mut body ← mkMatch ctx header indVal auxFunName header.argNames
+ let binders := header.binders
+ let type ← `(Decidable ($(mkIdent header.target1Name) = $(mkIdent header.target2Name)))
+ `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : $type:term := $body:term)
+
+def mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax) := do
+ let ctx ← mkContext "decEq" indVal.name
+ let cmds := #[← mkAuxFunction ctx] ++ (← mkInstanceCmds ctx `DecidableEq #[indVal.name] (useAnonCtor := false))
+ trace[Elab.Deriving.decEq]! "\n{cmds}"
+ return cmds
+
+open Command
+
+def mkDecEqInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+ if declNames.size != 1 then
+ return false -- mutually inductive types are not supported yet
+ else
+ let indVal ← getConstInfoInduct declNames[0]
+ if indVal.isNested then
+ return false -- nested inductive types are not supported yet
+ else
+ let cmds ← liftTermElabM none <| mkDecEqCmds indVal
+ cmds.forM elabCommand
+ return true
+
+builtin_initialize
+ registerBuiltinDerivingHandler `DecidableEq mkDecEqInstanceHandler
+ registerTraceClass `Elab.Deriving.decEq
+
+end Lean.Elab.Deriving.DecEq
diff --git a/stage0/src/Lean/Elab/Deriving/Util.lean b/stage0/src/Lean/Elab/Deriving/Util.lean
index c014489711..c90e1ee2ac 100644
--- a/stage0/src/Lean/Elab/Deriving/Util.lean
+++ b/stage0/src/Lean/Elab/Deriving/Util.lean
@@ -51,7 +51,7 @@ structure Context where
auxFunNames : Array Name
usePartial : Bool
-def mkContext (typeName : Name) : TermElabM Context := do
+def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
let indVal ← getConstInfoInduct typeName
let mut typeInfos := #[]
for typeName in indVal.all do
@@ -59,7 +59,7 @@ def mkContext (typeName : Name) : TermElabM Context := do
let mut auxFunNames := #[]
for typeName in indVal.all do
match typeName.eraseMacroScopes with
- | Name.str _ t _ => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| "beq" ++ t)
+ | Name.str _ t _ => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
| _ => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
trace[Elab.Deriving.beq]! "{auxFunNames}"
let usePartial := indVal.isNested || typeInfos.size > 1
@@ -91,7 +91,7 @@ def mkLet (letDecls : Array Syntax) (body : Syntax) : TermElabM Syntax :=
letDecls.foldrM (init := body) fun letDecl body =>
`(let $letDecl:letDecl; $body)
-def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) : TermElabM (Array Syntax) := do
+def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (useAnonCtor := true) : TermElabM (Array Syntax) := do
let mut instances := #[]
for i in [:ctx.typeInfos.size] do
let indVal := ctx.typeInfos[i]
@@ -102,10 +102,47 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) :
let binders := binders ++ (← mkInstImplicitBinders className indVal argNames)
let indType ← mkInductiveApp indVal argNames
let type ← `($(mkIdent className) $indType)
- let val ← `(⟨$(mkIdent auxFunName)⟩)
+ let val ← if useAnonCtor then `(⟨$(mkIdent auxFunName)⟩) else pure <| mkIdent auxFunName
let instCmd ← `(instance $binders:implicitBinder* : $type := $val)
trace[Meta.debug]! "\n{instCmd}"
instances := instances.push instCmd
return instances
+namespace Binary
+
+structure Header where
+ binders : Array Syntax
+ argNames : Array Name
+ target1Name : Name
+ target2Name : Name
+
+def mkHeader (ctx : Context) (className : Name) (indVal : InductiveVal) : TermElabM Header := do
+ let argNames ← mkInductArgNames indVal
+ let binders ← mkImplicitBinders argNames
+ let targetType ← mkInductiveApp indVal argNames
+ let target1Name ← mkFreshUserName `x
+ let target2Name ← mkFreshUserName `y
+ let binders := binders ++ (← mkInstImplicitBinders className indVal argNames)
+ let target1Binder ← `(explicitBinderF| ($(mkIdent target1Name) : $targetType))
+ let target2Binder ← `(explicitBinderF| ($(mkIdent target2Name) : $targetType))
+ let binders := binders ++ #[target1Binder, target2Binder]
+ return {
+ binders := binders
+ argNames := argNames
+ target1Name := target1Name
+ target2Name := target2Name
+ }
+
+def mkDiscr (varName : Name) : TermElabM Syntax :=
+ `(Parser.Term.matchDiscr| $(mkIdent varName):term)
+
+def mkDiscrs (header : Header) (indVal : InductiveVal) : TermElabM (Array Syntax) := do
+ let mut discrs := #[]
+ -- add indices
+ for argName in header.argNames[indVal.nparams:] do
+ discrs := discrs.push (← mkDiscr argName)
+ return discrs ++ #[← mkDiscr header.target1Name, ← mkDiscr header.target2Name]
+
+end Binary
+
end Lean.Elab.Deriving
diff --git a/stage0/src/Lean/Elab/Tactic/Basic.lean b/stage0/src/Lean/Elab/Tactic/Basic.lean
index 6578cbf3ab..92caeb281a 100644
--- a/stage0/src/Lean/Elab/Tactic/Basic.lean
+++ b/stage0/src/Lean/Elab/Tactic/Basic.lean
@@ -54,23 +54,22 @@ def BacktrackableState.restore (b : BacktrackableState) : TacticM Unit := do
let b ← saveBacktrackableState
try x catch ex => b.restore; h ex
-instance : MonadExcept Exception TacticM := {
- throw := throw,
+instance : MonadExcept Exception TacticM where
+ throw := throw
tryCatch := Tactic.tryCatch
-}
@[inline] protected def orElse {α} (x y : TacticM α) : TacticM α := do
try x catch _ => y
-instance {α} : OrElse (TacticM α) := ⟨Tactic.orElse⟩
+instance {α} : OrElse (TacticM α) where
+ orElse := Tactic.orElse
structure SavedState where
core : Core.State
meta : Meta.State
term : Term.State
tactic : State
-
-instance : Inhabited SavedState := ⟨⟨arbitrary, arbitrary, arbitrary, arbitrary⟩⟩
+ deriving Inhabited
def saveAllState : TacticM SavedState := do
pure { core := (← getThe Core.State), meta := (← getThe Meta.State), term := (← getThe Term.State), tactic := (← get) }
diff --git a/stage0/src/Lean/Elab/Tactic/Induction.lean b/stage0/src/Lean/Elab/Tactic/Induction.lean
index d8038d1c0b..069ce67c70 100644
--- a/stage0/src/Lean/Elab/Tactic/Induction.lean
+++ b/stage0/src/Lean/Elab/Tactic/Induction.lean
@@ -143,7 +143,7 @@ def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId)
let motiverInferredType ← inferType motive
let motiveType ← inferType (mkMVar motiveArg)
unless (← isDefEqGuarded motiverInferredType motiveType) do
- throwError! "type mismatch when assigning motive{indentExpr motive}\nhas type{indentExpr motiverInferredType}\nexpected type{indentExpr motiveType}"
+ throwError! "type mismatch when assigning motive{indentExpr motive}\n{← mkHasTypeButIsExpectedMsg motiverInferredType motiveType}"
assignExprMVar motiveArg motive
private def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM Nat := do
diff --git a/stage0/src/Lean/Elab/Term.lean b/stage0/src/Lean/Elab/Term.lean
index 0040dbdbad..11d1577e8a 100644
--- a/stage0/src/Lean/Elab/Term.lean
+++ b/stage0/src/Lean/Elab/Term.lean
@@ -212,8 +212,8 @@ def applyResult (result : TermElabResult) : TermElabM Expr :=
@[inline] def liftCoreM {α} (x : CoreM α) : TermElabM α :=
Term.liftMetaM $ liftM x
-instance : MonadLiftT MetaM TermElabM :=
- ⟨Term.liftMetaM⟩
+instance : MonadLiftT MetaM TermElabM where
+ monadLift := Term.liftMetaM
def getLevelNames : TermElabM (List Name) :=
return (← get).levelNames
@@ -223,24 +223,22 @@ def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
| some d => pure d
| none => unreachable!
-instance : AddErrorMessageContext TermElabM := {
- add := fun ref msg => do
+instance : AddErrorMessageContext TermElabM where
+ add ref msg := do
let ctx ← read
let ref := getBetterRef ref ctx.macroStack
let msg ← addMessageContext msg
let msg ← addMacroStack msg ctx.macroStack
pure (ref, msg)
-}
-instance : MonadLog TermElabM := {
- getRef := getRef,
- getFileMap := do pure (← read).fileMap,
- getFileName := do pure (← read).fileName,
- logMessage := fun msg => do
+instance : MonadLog TermElabM where
+ getRef := getRef
+ getFileMap := return (← read).fileMap
+ getFileName := return (← read).fileName
+ logMessage msg := do
let ctx ← readThe Core.Context
let msg := { msg with data := MessageData.withNamingContext { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } msg.data };
modify fun s => { s with messages := s.messages.add msg }
-}
protected def getCurrMacroScope : TermElabM MacroScope := do pure (← read).currMacroScope
protected def getMainModule : TermElabM Name := do pure (← getEnv).mainModule
@@ -249,11 +247,10 @@ protected def getMainModule : TermElabM Name := do pure (← getEnv).mainMod
let fresh ← modifyGetThe Core.State (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 }))
withReader (fun ctx => { ctx with currMacroScope := fresh }) x
-instance : MonadQuotation TermElabM := {
- getCurrMacroScope := Term.getCurrMacroScope,
- getMainModule := Term.getMainModule,
+instance : MonadQuotation TermElabM where
+ getCurrMacroScope := Term.getCurrMacroScope
+ getMainModule := Term.getMainModule
withFreshMacroScope := Term.withFreshMacroScope
-}
unsafe def mkTermElabAttributeUnsafe : IO (KeyedDeclsAttribute TermElab) :=
mkElabAttribute TermElab `Lean.Elab.Term.termElabAttribute `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term"
@@ -274,10 +271,11 @@ inductive LVal where
| fieldName (name : String)
| getOp (idx : Syntax)
-instance : ToString LVal := ⟨fun
- | LVal.fieldIdx i => toString i
- | LVal.fieldName n => n
- | LVal.getOp idx => "[" ++ toString idx ++ "]"⟩
+instance : ToString LVal where
+ toString
+ | LVal.fieldIdx i => toString i
+ | LVal.fieldName n => n
+ | LVal.getOp idx => "[" ++ toString idx ++ "]"
def getDeclName? : TermElabM (Option Name) := return (← read).declName?
def getLetRecsToLift : TermElabM (List LetRecToLift) := return (← get).letRecsToLift
@@ -301,10 +299,10 @@ def withoutErrToSorry {α} (x : TermElabM α) : TermElabM α :=
builtin_initialize
registerOption `autoBoundImplicitLocal {
- defValue := true,
- group := "",
+ defValue := true
+ group := ""
descr := "Unbound local variables in declaration headers become implicit arguments if they are a lower case or greek letter. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}"
-}
+ }
private def getAutoBoundImplicitLocalOption (opts : Options) : Bool :=
opts.get `autoBoundImplicitLocal true
@@ -482,14 +480,14 @@ def applyAttributesAt (declName : Name) (attrs : Array Attribute) (applicationTi
def applyAttributes (declName : Name) (attrs : Array Attribute) : TermElabM Unit :=
applyAttributesCore declName attrs none
-def mkTypeMismatchError (header? : Option String) (e : Expr) (eType : Expr) (expectedType : Expr) : MessageData :=
+def mkTypeMismatchError (header? : Option String) (e : Expr) (eType : Expr) (expectedType : Expr) : TermElabM MessageData := do
let header : MessageData := match header? with
- | some header => m!"{header} has type"
- | none => m!"type mismatch{indentExpr e}\nhas type"
- m!"{header}{indentExpr eType}\nbut is expected to have type{indentExpr expectedType}"
+ | some header => m!"{header} "
+ | none => m!"type mismatch{indentExpr e}\n"
+ m!"{header}{← mkHasTypeButIsExpectedMsg eType expectedType}"
def throwTypeMismatchError {α} (header? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr)
- (f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α :=
+ (f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α := do
/-
We ignore `extraMsg?` for now. In all our tests, it contained no useful information. It was
always of the form:
@@ -506,7 +504,7 @@ def throwTypeMismatchError {α} (header? : Option String) (expectedType : Expr)
| some extraMsg => Format.line ++ extraMsg;
-/
match f? with
- | none => throwError $ mkTypeMismatchError header? e eType expectedType ++ extraMsg
+ | none => throwError <| (← mkTypeMismatchError header? e eType expectedType) ++ extraMsg
| some f => Meta.throwAppTypeMismatch f e extraMsg
@[inline] def withoutMacroStackAtErr {α} (x : TermElabM α) : TermElabM α :=
@@ -893,11 +891,10 @@ private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catch
| some elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
| none => throwError! "elaboration function for '{k}' has not been implemented"
-instance : MonadMacroAdapter TermElabM := {
- getCurrMacroScope := getCurrMacroScope,
- getNextMacroScope := return (← getThe Core.State).nextMacroScope,
- setNextMacroScope := fun next => modifyThe Core.State fun s => { s with nextMacroScope := next }
-}
+instance : MonadMacroAdapter TermElabM where
+ getCurrMacroScope := getCurrMacroScope
+ getNextMacroScope := return (← getThe Core.State).nextMacroScope
+ setNextMacroScope next := modifyThe Core.State fun s => { s with nextMacroScope := next }
private def isExplicit (stx : Syntax) : Bool :=
match stx with
@@ -1332,13 +1329,13 @@ private def mkSomeContext : Context := {
let ((a, s), sCore, sMeta) ← (x.run ctx s).toIO ctxCore sCore ctxMeta sMeta
pure (a, sCore, sMeta, s)
-instance {α} [MetaEval α] : MetaEval (TermElabM α) :=
- ⟨fun env opts x _ =>
+instance {α} [MetaEval α] : MetaEval (TermElabM α) where
+ eval env opts x _ :=
let x : TermElabM α := do
try x finally
let s ← get
s.messages.forM fun msg => do IO.println (← msg.toString)
- MetaEval.eval env opts (hideUnit := true) $ x.run' mkSomeContext⟩
+ MetaEval.eval env opts (hideUnit := true) $ x.run' mkSomeContext
end Term
diff --git a/stage0/src/Lean/Meta.lean b/stage0/src/Lean/Meta.lean
index c33a5e1a9d..f7678f14d5 100644
--- a/stage0/src/Lean/Meta.lean
+++ b/stage0/src/Lean/Meta.lean
@@ -27,3 +27,4 @@ import Lean.Meta.ForEachExpr
import Lean.Meta.Transform
import Lean.Meta.PPGoal
import Lean.Meta.UnificationHint
+import Lean.Meta.Inductive
diff --git a/stage0/src/Lean/Meta/Check.lean b/stage0/src/Lean/Meta/Check.lean
index 9cbb2ac662..a10e0d7ff5 100644
--- a/stage0/src/Lean/Meta/Check.lean
+++ b/stage0/src/Lean/Meta/Check.lean
@@ -36,13 +36,94 @@ private def getFunctionDomain (f : Expr) : MetaM (Expr × BinderInfo) := do
| Expr.forallE _ d _ c => return (d, c.binderInfo)
| _ => throwFunctionExpected f
+/-
+Given to expressions `a` and `b`, this method tries to annotate terms with `pp.explicit := true` to
+expose "implicit" differences. For example, suppose `a` and `b` are of the form
+```lean
+@HashMap Nat Nat eqInst hasInst1
+@HashMap Nat Nat eqInst hasInst2
+```
+By default, the pretty printer formats both of them as `HashMap Nat Nat`.
+So, counterintuitive error messages such as
+```lean
+error: application type mismatch
+ HashMap.insert m
+argument
+ m
+has type
+ HashMap Nat Nat
+but is expected to have type
+ HashMap Nat Nat
+```
+would be produced.
+By adding `pp.explicit := true`, we can generate the more informative error
+```lean
+error: application type mismatch
+ HashMap.insert m
+argument
+ m
+has type
+ @HashMap Nat Nat eqInst hasInst1
+but is expected to have type
+ @HashMap Nat Nat eqInst hasInst2
+```
+Remark: this method implements a simple heuristic, we should extend it as we find other counterintuitive
+error messages.
+-/
+partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
+ if (← getOptions).getBool `pp.all false || (← getOptions).getBool `pp.explicit false then
+ return (a, b)
+ else
+ visit a b
+where
+ visit (a b : Expr) : MetaM (Expr × Expr) := do
+ try
+ if !a.isApp || !b.isApp then
+ return (a, b)
+ else if a.getAppNumArgs != b.getAppNumArgs then
+ return (a, b)
+ else if not (← isDefEq a.getAppFn b.getAppFn) then
+ return (a, b)
+ else
+ let fType ← inferType a.getAppFn
+ forallBoundedTelescope fType a.getAppNumArgs fun xs _ => do
+ let mut as := a.getAppArgs
+ let mut bs := b.getAppArgs
+ if (← hasExplicitDiff xs as bs) then
+ return (a, b)
+ else
+ for i in [:as.size] do
+ let (ai, bi) ← visit as[i] bs[i]
+ as := as.set! i ai
+ bs := bs.set! i bi
+ let a := mkAppN a.getAppFn as
+ let b := mkAppN b.getAppFn bs
+ return (a.setAppPPExplicit, b.setAppPPExplicit)
+ catch _ =>
+ return (a, b)
+
+ hasExplicitDiff (xs as bs : Array Expr) : MetaM Bool := do
+ for i in [:xs.size] do
+ let localDecl ← getLocalDecl xs[i].fvarId!
+ if localDecl.binderInfo.isExplicit then
+ if not (← isDefEq as[i] bs[i]) then
+ return true
+ return false
+
+/-
+ Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
+-/
+def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr) : MetaM MessageData := do
+ let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
+ m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}"
+
def throwAppTypeMismatch {α} (f a : Expr) (extraMsg : MessageData := Format.nil) : MetaM α := do
let (expectedType, binfo) ← getFunctionDomain f
let mut e := mkApp f a
unless binfo.isExplicit do
e := e.setAppPPExplicit
let aType ← inferType a
- throwError! "application type mismatch{indentExpr e}\nargument{indentExpr a}\nhas type{indentExpr aType}\nbut is expected to have type{indentExpr expectedType}{extraMsg}"
+ throwError! "application type mismatch{indentExpr e}\nargument{indentExpr a}\n{← mkHasTypeButIsExpectedMsg aType expectedType}"
def checkApp (f a : Expr) : MetaM Unit := do
let fType ← inferType f
diff --git a/stage0/src/Lean/Meta/Inductive.lean b/stage0/src/Lean/Meta/Inductive.lean
new file mode 100644
index 0000000000..2959699c99
--- /dev/null
+++ b/stage0/src/Lean/Meta/Inductive.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.ExprDefEq
+
+/- Helper methods for inductive datatypes -/
+
+namespace Lean.Meta
+
+/- Return true if the types of the given constructors are compatible. -/
+def compatibleCtors (ctorName₁ ctorName₂ : Name) : MetaM Bool := do
+ let ctorInfo₁ ← getConstInfoCtor ctorName₁
+ let ctorInfo₂ ← getConstInfoCtor ctorName₂
+ if ctorInfo₁.induct != ctorInfo₂.induct then
+ return false
+ else
+ let (_, _, ctorType₁) ← forallMetaTelescope ctorInfo₁.type
+ let (_, _, ctorType₂) ← forallMetaTelescope ctorInfo₂.type
+ isDefEq ctorType₁ ctorType₂
+
+end Lean.Meta
diff --git a/stage0/src/Lean/Meta/Match/Basic.lean b/stage0/src/Lean/Meta/Match/Basic.lean
index 1a8fdf3273..ef7aa4212f 100644
--- a/stage0/src/Lean/Meta/Match/Basic.lean
+++ b/stage0/src/Lean/Meta/Match/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
+import Lean.Meta.Check
import Lean.Meta.Match.MatcherInfo
import Lean.Meta.Match.CaseArraySizes
@@ -177,8 +178,9 @@ def checkAndReplaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : MetaM Alt :
let vType ← inferType v
unless (← isDefEqGuarded fvarDecl.type vType) do
withExistingLocalDecls alt.fvarDecls do
+ let (expectedType, givenType) ← addPPExplicitToExposeDiff vType fvarDecl.type
throwErrorAt alt.ref $
- m!"type mismatch during dependent match-elimination at pattern variable '{mkFVar fvarDecl.fvarId}' with type{indentExpr fvarDecl.type}\nexpected type{indentExpr vType}"
+ m!"type mismatch during dependent match-elimination at pattern variable '{mkFVar fvarDecl.fvarId}' with type{indentExpr givenType}\nexpected type{indentExpr expectedType}"
pure $ replaceFVarId fvarId v alt
end Alt
diff --git a/stage0/src/Lean/Meta/Tactic/Assert.lean b/stage0/src/Lean/Meta/Tactic/Assert.lean
index b77e8776bc..7ae0f44e90 100644
--- a/stage0/src/Lean/Meta/Tactic/Assert.lean
+++ b/stage0/src/Lean/Meta/Tactic/Assert.lean
@@ -27,7 +27,7 @@ def assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MV
Convert the given goal `Ctx |- target` into `Ctx |- let name : type := val; target`.
It assumes `val` has type `type` -/
def define (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := do
- withMVarContext mvarId $ do
+ withMVarContext mvarId do
checkNotAssigned mvarId `define
let tag ← getMVarTag mvarId
let target ← getMVarType mvarId
@@ -40,7 +40,7 @@ def define (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MV
Convert the given goal `Ctx |- target` into `Ctx |- (hName : type) -> hName = val -> target`.
It assumes `val` has type `type` -/
def assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do
- withMVarContext mvarId $ do
+ withMVarContext mvarId do
checkNotAssigned mvarId `assert
let tag ← getMVarTag mvarId
let target ← getMVarType mvarId
@@ -62,7 +62,7 @@ structure AssertAfterResult where
It assumes `val` has type `type`, and that `type` is well-formed after `fvarId`.
Note that `val` does not need to be well-formed after `fvarId`. That is, it may contain variables that are defined after `fvarId`. -/
def assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do
- withMVarContext mvarId $ do
+ withMVarContext mvarId do
checkNotAssigned mvarId `assertAfter
let tag ← getMVarTag mvarId
let target ← getMVarType mvarId
diff --git a/stage0/src/Lean/Meta/Tactic/Injection.lean b/stage0/src/Lean/Meta/Tactic/Injection.lean
index 096e52bf6c..5d4cf04e5a 100644
--- a/stage0/src/Lean/Meta/Tactic/Injection.lean
+++ b/stage0/src/Lean/Meta/Tactic/Injection.lean
@@ -57,12 +57,15 @@ private def heqToEq (mvarId : MVarId) (fvarId : FVarId) : MetaM (FVarId × MVarI
match type.heq? with
| none => pure (fvarId, mvarId)
| some (α, a, β, b) =>
- let pr ← mkEqOfHEq (mkFVar fvarId)
- let eq ← mkEq a b
- let mvarId ← assert mvarId decl.userName eq pr
- let mvarId ← clear mvarId fvarId
- let (fvarId, mvarId) ← intro1P mvarId
- pure (fvarId, mvarId)
+ if (← isDefEq α β) then
+ let pr ← mkEqOfHEq (mkFVar fvarId)
+ let eq ← mkEq a b
+ let mvarId ← assert mvarId decl.userName eq pr
+ let mvarId ← clear mvarId fvarId
+ let (fvarId, mvarId) ← intro1P mvarId
+ pure (fvarId, mvarId)
+ else
+ pure (fvarId, mvarId)
def injectionIntro : Nat → MVarId → Array FVarId → List Name → MetaM InjectionResult
| 0, mvarId, fvarIds, remainingNames =>
@@ -79,6 +82,8 @@ def injectionIntro : Nat → MVarId → Array FVarId → List Name → MetaM Inj
def injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) (useUnusedNames : Bool := true) : MetaM InjectionResult := do
match (← injectionCore mvarId fvarId) with
| InjectionResultCore.solved => pure InjectionResult.solved
- | InjectionResultCore.subgoal mvarId numEqs => injectionIntro numEqs mvarId #[] newNames
+ | InjectionResultCore.subgoal mvarId numEqs =>
+ trace[Meta.debug]! "before injectionIntro\n{MessageData.ofGoal mvarId}"
+ injectionIntro numEqs mvarId #[] newNames
end Lean.Meta
diff --git a/stage0/src/Lean/Meta/Tactic/Subst.lean b/stage0/src/Lean/Meta/Tactic/Subst.lean
index 715843dddc..6c07ef1f56 100644
--- a/stage0/src/Lean/Meta/Tactic/Subst.lean
+++ b/stage0/src/Lean/Meta/Tactic/Subst.lean
@@ -15,6 +15,7 @@ namespace Lean.Meta
def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : FVarSubst := {}) (clearH := true) : MetaM (FVarSubst × MVarId) :=
withMVarContext mvarId do
+ let mvarId0 := mvarId
let tag ← getMVarTag mvarId
checkNotAssigned mvarId `subst
let hFVarIdOriginal := hFVarId
@@ -40,61 +41,77 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
let a := mkFVar aFVarId
let hFVarId := twoVars[1]
let h := mkFVar hFVarId
- withMVarContext mvarId do
- let mvarDecl ← getMVarDecl mvarId
- let type := mvarDecl.type
- let hLocalDecl ← getLocalDecl hFVarId
- match (← matchEq? hLocalDecl.type) with
- | none => unreachable!
- | some (α, lhs, rhs) => do
- let b := if symm then lhs else rhs
- let mctx ← getMCtx
- let depElim := mctx.exprDependsOn mvarDecl.type hFVarId
- let cont (motive : Expr) (newType : Expr) : MetaM (FVarSubst × MVarId) := do
- let major ← if symm then pure h else mkEqSymm h
- let newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag
- let minor := newMVar
- let newVal ← if depElim then mkEqRec motive minor major else mkEqNDRec motive minor major
- assignExprMVar mvarId newVal
- let mvarId := newMVar.mvarId!
- let mvarId ←
- if clearH then
- let mvarId ← clear mvarId hFVarId
- clear mvarId aFVarId
+ /- Set skip to true if there is no local variable nor the target depend on the equality -/
+ let skip ←
+ if vars.size == 2 then
+ pure false
+ else
+ let mvarType ← getMVarType mvarId
+ let mctx ← getMCtx
+ pure (!mctx.exprDependsOn mvarType aFVarId && !mctx.exprDependsOn mvarType hFVarId)
+ if skip then
+ if clearH then
+ let mvarId ← clear mvarId0 hFVarId
+ let mvarId ← clear mvarId aFVarId
+ pure ({}, mvarId)
+ else
+ pure ({}, mvarId0)
+ else
+ withMVarContext mvarId do
+ let mvarDecl ← getMVarDecl mvarId
+ let type := mvarDecl.type
+ let hLocalDecl ← getLocalDecl hFVarId
+ match (← matchEq? hLocalDecl.type) with
+ | none => unreachable!
+ | some (α, lhs, rhs) => do
+ let b := if symm then lhs else rhs
+ let mctx ← getMCtx
+ let depElim := mctx.exprDependsOn mvarDecl.type hFVarId
+ let cont (motive : Expr) (newType : Expr) : MetaM (FVarSubst × MVarId) := do
+ let major ← if symm then pure h else mkEqSymm h
+ let newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag
+ let minor := newMVar
+ let newVal ← if depElim then mkEqRec motive minor major else mkEqNDRec motive minor major
+ assignExprMVar mvarId newVal
+ let mvarId := newMVar.mvarId!
+ let mvarId ←
+ if clearH then
+ let mvarId ← clear mvarId hFVarId
+ clear mvarId aFVarId
+ else
+ pure mvarId
+ let (newFVars, mvarId) ← introNP mvarId (vars.size - 2)
+ let fvarSubst ← newFVars.size.foldM (init := fvarSubst) fun i (fvarSubst : FVarSubst) =>
+ let var := vars[i+2]
+ let newFVar := newFVars[i]
+ pure $ fvarSubst.insert var (mkFVar newFVar)
+ let fvarSubst := fvarSubst.insert aFVarIdOriginal (if clearH then b else mkFVar aFVarId)
+ let fvarSubst := fvarSubst.insert hFVarIdOriginal (mkFVar hFVarId)
+ pure (fvarSubst, mvarId)
+ if depElim then do
+ let newType := type.replaceFVar a b
+ let reflB ← mkEqRefl b
+ let newType := newType.replaceFVar h reflB
+ if symm then
+ let motive ← mkLambdaFVars #[a, h] type
+ cont motive newType
else
- pure mvarId
- let (newFVars, mvarId) ← introNP mvarId (vars.size - 2)
- let fvarSubst ← newFVars.size.foldM (init := fvarSubst) fun i (fvarSubst : FVarSubst) =>
- let var := vars[i+2]
- let newFVar := newFVars[i]
- pure $ fvarSubst.insert var (mkFVar newFVar)
- let fvarSubst := fvarSubst.insert aFVarIdOriginal (if clearH then b else mkFVar aFVarId)
- let fvarSubst := fvarSubst.insert hFVarIdOriginal (mkFVar hFVarId)
- pure (fvarSubst, mvarId)
- if depElim then do
- let newType := type.replaceFVar a b
- let reflB ← mkEqRefl b
- let newType := newType.replaceFVar h reflB
- if symm then
- let motive ← mkLambdaFVars #[a, h] type
- cont motive newType
+ /- `type` depends on (h : a = b). So, we use the following trick to avoid a type incorrect motive.
+ 1- Create a new local (hAux : b = a)
+ 2- Create newType := type [hAux.symm / h]
+ `newType` is type correct because `h` and `hAux.symm` are definitionally equal by proof irrelevance.
+ 3- Create motive by abstracting `a` and `hAux` in `newType`. -/
+ let hAuxType ← mkEq b a
+ let motive ← withLocalDeclD `_h hAuxType fun hAux => do
+ let hAuxSymm ← mkEqSymm hAux
+ /- replace h in type with hAuxSymm -/
+ let newType := type.replaceFVar h hAuxSymm
+ mkLambdaFVars #[a, hAux] newType
+ cont motive newType
else
- /- `type` depends on (h : a = b). So, we use the following trick to avoid a type incorrect motive.
- 1- Create a new local (hAux : b = a)
- 2- Create newType := type [hAux.symm / h]
- `newType` is type correct because `h` and `hAux.symm` are definitionally equal by proof irrelevance.
- 3- Create motive by abstracting `a` and `hAux` in `newType`. -/
- let hAuxType ← mkEq b a
- let motive ← withLocalDeclD `_h hAuxType fun hAux => do
- let hAuxSymm ← mkEqSymm hAux
- /- replace h in type with hAuxSymm -/
- let newType := type.replaceFVar h hAuxSymm
- mkLambdaFVars #[a, hAux] newType
+ let motive ← mkLambdaFVars #[a] type
+ let newType := type.replaceFVar a b
cont motive newType
- else
- let motive ← mkLambdaFVars #[a] type
- let newType := type.replaceFVar a b
- cont motive newType
| _ =>
let eqMsg := if symm then "(t = x)" else "(x = t)"
throwTacticEx `subst mvarId
diff --git a/stage0/src/library/compiler/ir_interpreter.cpp b/stage0/src/library/compiler/ir_interpreter.cpp
index 5fde882707..bc4f6d8d2d 100644
--- a/stage0/src/library/compiler/ir_interpreter.cpp
+++ b/stage0/src/library/compiler/ir_interpreter.cpp
@@ -298,7 +298,7 @@ void * lookup_symbol_in_cur_exe(char const * sym) {
}
class interpreter;
-LEAN_THREAD_PTR(interpreter, g_interpreter);
+static interpreter & get_interpreter();
class interpreter {
// stack of IR variable slots
@@ -314,12 +314,10 @@ class interpreter {
frame(name const & mFn, size_t mArgBp, size_t mJpBp) : m_fn(mFn), m_arg_bp(mArgBp), m_jp_bp(mJpBp) {}
};
std::vector m_call_stack;
- environment const & m_env;
- options const & m_opts;
+ environment const * m_env;
+ options const * m_opts;
// if `false`, use IR code where possible
bool m_prefer_native;
- // if we were called within the execution of a different interpreter, restore the value of `g_interpreter` in the end
- interpreter * m_prev_interpreter;
struct constant_cache_entry {
bool m_is_scalar;
value m_val;
@@ -352,6 +350,37 @@ class interpreter {
return m_arg_stack[i];
}
+public:
+ template
+ static inline T with_interpreter(environment const & env, options const & opts, std::function const & f) {
+ interpreter & interp = get_interpreter();
+ if (interp.m_env && is_eqp(*interp.m_env, env) && interp.m_opts && is_eqp(*interp.m_opts, opts)) {
+ return f(interp);
+ } else {
+ // We changed threads or the closure was stored and called in a different context.
+ time_task t("interpretation",
+ message_builder(env, get_global_ios(), "foo", pos_info(), message_severity::INFORMATION));
+ abstract_type_context trace_ctx(opts);
+ scope_trace_env scope_trace(env, opts, trace_ctx);
+ flet fl1(interp.m_env, &env);
+ flet fl2(interp.m_opts, &opts);
+ flet fl3(interp.m_prefer_native, opts.get_bool(*g_interpreter_prefer_native, LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE));
+ if (interp.m_env) {
+ // both these caches contain data from the Environment, so we cannot reuse them when changing it
+ flet> fl4(interp.m_constant_cache, {});
+ flet> fl5(interp.m_symbol_cache, {});
+ return f(interp);
+ } else {
+ // if there is no outer interpreter, might as well leave the caches around; maybe the next call is for
+ // the same Environment
+ interp.m_constant_cache = {};
+ interp.m_symbol_cache = {};
+ return f(interp);
+ }
+ }
+ }
+
+private:
value eval_arg(arg const & a) {
// an "irrelevant" argument is type- or proof-erased; we can use an arbitrary value for it
return arg_is_irrelevant(a) ? box(0) : var(arg_var_id(a));
@@ -383,8 +412,8 @@ class interpreter {
object * mk_stub_closure(decl const & d, unsigned n, object ** args) {
unsigned cls_size = 3 + decl_params(d).size();
object * cls = alloc_closure(get_stub(cls_size), cls_size, 3 + n);
- closure_set(cls, 0, m_env.to_obj_arg());
- closure_set(cls, 1, m_opts.to_obj_arg());
+ closure_set(cls, 0, m_env->to_obj_arg());
+ closure_set(cls, 1, m_opts->to_obj_arg());
closure_set(cls, 2, d.to_obj_arg());
for (unsigned i = 0; i < n ; i++)
closure_set(cls, 3 + i, args[i]);
@@ -712,7 +741,7 @@ class interpreter {
return *e;
} else {
symbol_cache_entry e_new { get_decl(fn), nullptr, false };
- if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern || has_init_attribute(m_env, fn)) {
+ if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern || has_init_attribute(*m_env, fn)) {
string_ref mangled = name_mangle(fn, *g_mangle_prefix);
string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
// check for boxed version first
@@ -731,7 +760,7 @@ class interpreter {
/** \brief Retrieve Lean declaration from environment. */
decl get_decl(name const & fn) {
- option_ref d = find_ir_decl(m_env, fn);
+ option_ref d = find_ir_decl(*m_env, fn);
if (!d) {
throw exception(sstream() << "unknown declaration '" << fn << "'");
}
@@ -751,7 +780,7 @@ class interpreter {
return *o;
}
- if (get_regular_init_fn_name_for(m_env, fn)) {
+ if (get_regular_init_fn_name_for(*m_env, fn)) {
// We don't know whether `[init]` decls can be re-executed, so let's not.
throw exception(sstream() << "cannot evaluate `[init]` declaration '" << fn << "' in the same module");
}
@@ -838,21 +867,13 @@ class interpreter {
return r;
}
- // closure stub stub
+ // static closure stub
static object * stub_m_aux(object ** args) {
environment env(args[0]);
options opts(args[1]);
- if (g_interpreter && is_eqp(g_interpreter->m_env, env)) {
- return g_interpreter->stub_m(args);
- } else {
- // We changed threads or the closure was stored and called in a different context.
- // Create new interpreter with new stacks.
- time_task t("interpretation",
- message_builder(env, get_global_ios(), "foo", pos_info(), message_severity::INFORMATION));
- abstract_type_context trace_ctx(opts);
- scope_trace_env scope_trace(env, opts, trace_ctx);
- return interpreter(env, opts).stub_m(args);
- }
+ return with_interpreter