fix: flush the CoreM and MetaM caches at modifyEnv
This fix may impact performance. Note that we don't need to flush the cache if we are "adding" stuff to the environment. We only need to flush the caches if the change is not monotonic. BTW, most of the changes are monotonic. I think this is why we did not hit this bug before. We may also move all these caches to an environment extension. It is an easy way to make sure we preserve the cache when extending the environment. I tried a few benchmarks and did not notice a significant difference. cc @kha @gebner fixes #1051
This commit is contained in:
Leonardo de Moura
parent
719db55a9c
commit
3193acecfa
6 changed files with 164 additions and 134 deletions
|
|
@ -65,7 +65,7 @@ instance : MonadRef CoreM where
|
|||
|
||||
instance : MonadEnv CoreM where
|
||||
getEnv := return (← get).env
|
||||
modifyEnv f := modify fun s => { s with env := f s.env }
|
||||
modifyEnv f := modify fun s => { s with env := f s.env, cache := {} }
|
||||
|
||||
instance : MonadOptions CoreM where
|
||||
getOptions := return (← read).options
|
||||
|
|
|
|||
|
|
@ -207,6 +207,10 @@ instance : MonadMCtx MetaM where
|
|||
getMCtx := return (← get).mctx
|
||||
modifyMCtx f := modify fun s => { s with mctx := f s.mctx }
|
||||
|
||||
instance : MonadEnv MetaM where
|
||||
getEnv := return (← getThe Core.State).env
|
||||
modifyEnv f := do modifyThe Core.State fun s => { s with env := f s.env, cache := {} }; modify fun s => { s with cache := {} }
|
||||
|
||||
instance : AddMessageContext MetaM where
|
||||
addMessageContext := addMessageContextFull
|
||||
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@ a : α
|
|||
α : Type @ ⟨7, 13⟩-⟨7, 14⟩
|
||||
a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||||
Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Fam2 : some Sort.{?_uniq.272} @ ⟨7, 21⟩-⟨7, 25⟩
|
||||
[.] `Fam2 : some Sort.{?_uniq.317} @ ⟨7, 21⟩-⟨7, 25⟩
|
||||
Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
|
||||
α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
|
||||
α : Type @ ⟨7, 26⟩-⟨7, 27⟩
|
||||
|
|
@ -45,7 +45,7 @@ a : α
|
|||
?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
|
||||
?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
|
||||
Fam2.any : Fam2 ?α ?α @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabApp
|
||||
[.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.602]) ([mdata _inaccessible:1 ?_uniq.603]) @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
[.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.647]) ([mdata _inaccessible:1 ?_uniq.648]) @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
@Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabInaccessible
|
||||
?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabHole
|
||||
|
|
@ -61,7 +61,7 @@ a : α
|
|||
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
|
||||
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
|
||||
Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Fam2.nat : some Fam2 ([mdata _inaccessible:1 ?_uniq.634]) ([mdata _inaccessible:1 ?_uniq.635]) @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
[.] `Fam2.nat : some Fam2 ([mdata _inaccessible:1 ?_uniq.679]) ([mdata _inaccessible:1 ?_uniq.680]) @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
n : Nat @ ⟨10, 13⟩-⟨10, 14⟩ @ Lean.Elab.Term.elabIdent
|
||||
n : Nat @ ⟨10, 13⟩-⟨10, 14⟩
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
[Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.385} @ ⟨13, 11⟩-⟨13, 14⟩
|
||||
[.] `Nat : some Sort.{?_uniq.422} @ ⟨13, 11⟩-⟨13, 14⟩
|
||||
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
|
||||
x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩
|
||||
Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ «_aux_Init_Notation___macroRules_term_×__1»
|
||||
|
|
@ -11,10 +11,10 @@
|
|||
Nat × Nat : Type @ ⟨13, 18⟩†-⟨13, 27⟩ @ Lean.Elab.Term.elabApp
|
||||
Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 27⟩†
|
||||
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.389} @ ⟨13, 18⟩-⟨13, 21⟩
|
||||
[.] `Nat : some Type.{?_uniq.426} @ ⟨13, 18⟩-⟨13, 21⟩
|
||||
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
|
||||
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.388} @ ⟨13, 24⟩-⟨13, 27⟩
|
||||
[.] `Nat : some Type.{?_uniq.425} @ ⟨13, 24⟩-⟨13, 27⟩
|
||||
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
|
||||
x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩
|
||||
let y := (x, x);
|
||||
|
|
@ -41,16 +41,16 @@
|
|||
[Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.418} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
[.] `Nat : some Sort.{?_uniq.455} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
x (isBinder := true) : Nat @ ⟨17, 9⟩-⟨17, 10⟩
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.420} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
[.] `Nat : some Sort.{?_uniq.457} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
y (isBinder := true) : Nat @ ⟨17, 11⟩-⟨17, 12⟩
|
||||
Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow
|
||||
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Bool : some Sort.{?_uniq.423} @ ⟨17, 27⟩-⟨17, 31⟩
|
||||
[.] `Bool : some Sort.{?_uniq.460} @ ⟨17, 27⟩-⟨17, 31⟩
|
||||
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
|
||||
b (isBinder := true) : Bool @ ⟨17, 23⟩-⟨17, 24⟩
|
||||
x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
|
||||
|
|
@ -112,20 +112,20 @@
|
|||
[Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.542} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
[.] `Nat : some Sort.{?_uniq.579} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
x (isBinder := true) : Nat @ ⟨21, 10⟩-⟨21, 11⟩
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.544} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
[.] `Nat : some Sort.{?_uniq.581} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
y (isBinder := true) : Nat @ ⟨21, 12⟩-⟨21, 13⟩
|
||||
Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow
|
||||
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Bool : some Sort.{?_uniq.547} @ ⟨21, 28⟩-⟨21, 32⟩
|
||||
[.] `Bool : some Sort.{?_uniq.584} @ ⟨21, 28⟩-⟨21, 32⟩
|
||||
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
|
||||
b (isBinder := true) : Bool @ ⟨21, 24⟩-⟨21, 25⟩
|
||||
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.549} @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
[.] `Nat : some Sort.{?_uniq.586} @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
fun x y b =>
|
||||
let x := (x + y, x - y);
|
||||
|
|
@ -238,10 +238,10 @@
|
|||
Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
|
||||
Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩†
|
||||
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.763} @ ⟨27, 12⟩-⟨27, 15⟩
|
||||
[.] `Nat : some Type.{?_uniq.800} @ ⟨27, 12⟩-⟨27, 15⟩
|
||||
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
|
||||
Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Array : some Type.{?_uniq.762} @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
[.] `Array : some Type.{?_uniq.799} @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen
|
||||
Macro expansion
|
||||
|
|
@ -249,17 +249,17 @@
|
|||
===>
|
||||
Array Nat
|
||||
Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Array : some Type.{?_uniq.764} @ ⟨27, 25⟩-⟨27, 30⟩
|
||||
[.] `Array : some Type.{?_uniq.801} @ ⟨27, 25⟩-⟨27, 30⟩
|
||||
Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩
|
||||
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.765} @ ⟨27, 31⟩-⟨27, 34⟩
|
||||
[.] `Nat : some Type.{?_uniq.802} @ ⟨27, 31⟩-⟨27, 34⟩
|
||||
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
|
||||
s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
|
||||
Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Array : some Sort.{?_uniq.767} @ ⟨27, 39⟩-⟨27, 44⟩
|
||||
[.] `Array : some Sort.{?_uniq.804} @ ⟨27, 39⟩-⟨27, 44⟩
|
||||
Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩
|
||||
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.768} @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
[.] `Nat : some Type.{?_uniq.805} @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
|
||||
Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp
|
||||
|
|
@ -275,11 +275,11 @@
|
|||
f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩
|
||||
[Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `B : some Sort.{?_uniq.810} @ ⟨30, 14⟩-⟨30, 15⟩
|
||||
[.] `B : some Sort.{?_uniq.847} @ ⟨30, 14⟩-⟨30, 15⟩
|
||||
B : Type @ ⟨30, 14⟩-⟨30, 15⟩
|
||||
arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩
|
||||
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.812} @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
[.] `Nat : some Sort.{?_uniq.849} @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩
|
||||
A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp
|
||||
|
|
@ -294,11 +294,11 @@
|
|||
f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩
|
||||
[Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.833} @ ⟨33, 12⟩-⟨33, 15⟩
|
||||
[.] `Nat : some Sort.{?_uniq.870} @ ⟨33, 12⟩-⟨33, 15⟩
|
||||
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
|
||||
x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩
|
||||
B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `B : some Sort.{?_uniq.835} @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
[.] `B : some Sort.{?_uniq.872} @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩
|
||||
{ pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst
|
||||
|
|
@ -338,73 +338,73 @@ infoTree.lean:44:0: error: expected stx
|
|||
[.] (Command.set_option "set_option" `pp.raw) @ ⟨44, 0⟩-⟨44, 17⟩
|
||||
[Elab.info] command @ ⟨45, 0⟩-⟨47, 8⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.857} @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
[.] `Nat : some Sort.{?_uniq.894} @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
_uniq.858 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
|
||||
_uniq.895 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
|
||||
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.859} @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
[.] `Nat : some Sort.{?_uniq.896} @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
_uniq.860 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
|
||||
Eq.{1} Nat _uniq.858 _uniq.858 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
|
||||
_uniq.897 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
|
||||
Eq.{1} Nat _uniq.895 _uniq.895 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
|
||||
Macro expansion
|
||||
(«term_=_» `x "=" `x)
|
||||
===>
|
||||
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.177 `x `x)
|
||||
Eq.{1} Nat _uniq.858 _uniq.858 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
|
||||
_uniq.858 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.858 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
|
||||
_uniq.858 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.858 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
|
||||
_uniq.867 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
|
||||
_uniq.868 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
|
||||
(fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.867 _uniq.868]) f6.f7 : Eq.{1} Nat _uniq.867 _uniq.867 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
|
||||
Eq.{1} Nat _uniq.895 _uniq.895 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
|
||||
_uniq.895 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.895 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
|
||||
_uniq.895 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.895 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
|
||||
_uniq.904 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
|
||||
_uniq.905 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
|
||||
(fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.904 _uniq.905]) f6.f7 : Eq.{1} Nat _uniq.904 _uniq.904 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
|
||||
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.869} @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
[.] `Nat : some Sort.{?_uniq.906} @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
_uniq.870 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
|
||||
_uniq.907 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
|
||||
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.871} @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
[.] `Nat : some Sort.{?_uniq.908} @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
_uniq.872 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
|
||||
Eq.{1} Nat _uniq.870 _uniq.870 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
|
||||
_uniq.909 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
|
||||
Eq.{1} Nat _uniq.907 _uniq.907 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
|
||||
Macro expansion
|
||||
(«term_=_» `x "=" `x)
|
||||
===>
|
||||
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.185 `x `x)
|
||||
Eq.{1} Nat _uniq.870 _uniq.870 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel
|
||||
_uniq.870 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.870 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
|
||||
_uniq.870 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.870 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
|
||||
_uniq.877 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
|
||||
_uniq.880 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
|
||||
_uniq.881 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
|
||||
Eq.refl.{1} Nat _uniq.880 : Eq.{1} Nat _uniq.880 _uniq.880 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Eq.refl : some Eq.{?_uniq.874} Nat _uniq.880 _uniq.880 @ ⟨46, 36⟩-⟨46, 43⟩
|
||||
Eq.{1} Nat _uniq.907 _uniq.907 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel
|
||||
_uniq.907 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.907 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
|
||||
_uniq.907 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.907 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
|
||||
_uniq.914 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
|
||||
_uniq.917 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
|
||||
_uniq.918 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
|
||||
Eq.refl.{1} Nat _uniq.917 : Eq.{1} Nat _uniq.917 _uniq.917 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Eq.refl : some Eq.{?_uniq.911} Nat _uniq.917 _uniq.917 @ ⟨46, 36⟩-⟨46, 43⟩
|
||||
Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩
|
||||
_uniq.880 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.880 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
|
||||
[mdata _recApp: _uniq.877 _uniq.867 _uniq.868] : Eq.{1} Nat _uniq.867 _uniq.867 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
|
||||
_uniq.877 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
|
||||
_uniq.867 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.867 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
|
||||
_uniq.868 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.868 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
|
||||
_uniq.917 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.917 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
|
||||
[mdata _recApp: _uniq.914 _uniq.904 _uniq.905] : Eq.{1} Nat _uniq.904 _uniq.904 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
|
||||
_uniq.914 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
|
||||
_uniq.904 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.904 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
|
||||
_uniq.905 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.905 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
|
||||
f6.f7 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
|
||||
f6 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
|
||||
[Elab.info] command @ ⟨50, 0⟩-⟨50, 32⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
B : Type @ ⟨50, 12⟩-⟨50, 13⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `B : some Sort.{?_uniq.905} @ ⟨50, 12⟩-⟨50, 13⟩
|
||||
[.] `B : some Sort.{?_uniq.942} @ ⟨50, 12⟩-⟨50, 13⟩
|
||||
B : Type @ ⟨50, 12⟩-⟨50, 13⟩
|
||||
_uniq.906 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
|
||||
_uniq.943 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
|
||||
B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `B : some Sort.{?_uniq.907} @ ⟨50, 17⟩-⟨50, 18⟩
|
||||
[.] `B : some Sort.{?_uniq.944} @ ⟨50, 17⟩-⟨50, 18⟩
|
||||
B : Type @ ⟨50, 17⟩-⟨50, 18⟩
|
||||
_uniq.910 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
|
||||
B.mk (B.pair _uniq.910) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
|
||||
B.pair _uniq.910 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
|
||||
_uniq.910 : B @ ⟨50, 24⟩-⟨50, 25⟩
|
||||
[.] _uniq.910 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
|
||||
_uniq.947 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
|
||||
B.mk (B.pair _uniq.947) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
|
||||
B.pair _uniq.947 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
|
||||
_uniq.947 : B @ ⟨50, 24⟩-⟨50, 25⟩
|
||||
[.] _uniq.947 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
|
||||
B.pair : B -> (Prod.{0 0} A A) @ ⟨50, 24⟩†-⟨50, 25⟩†
|
||||
pair : Prod.{0 0} A A := B.pair _uniq.910 @ ⟨50, 22⟩†-⟨50, 32⟩
|
||||
pair : Prod.{0 0} A A := B.pair _uniq.947 @ ⟨50, 22⟩†-⟨50, 32⟩
|
||||
f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
|
||||
|
|
|
|||
|
|
@ -1,3 +1,53 @@
|
|||
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.arrow G T EG getCtx
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
|
||||
(@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
|
||||
(@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
|
|
@ -13,6 +63,21 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
|
|||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
|
|
@ -66,68 +131,3 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
|
|||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.arrow G T EG getCtx
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
|
||||
(@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
|
||||
(@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
|
|
|
|||
26
tests/lean/run/1051.lean
Normal file
26
tests/lean/run/1051.lean
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
inductive SF : Type u → Type u → Type (u+1) where
|
||||
| seq {as bs cs: Type u}: SF as bs → SF bs cs → SF as cs
|
||||
| fan {as bs cs: Type u}: SF as (bs × cs)
|
||||
|
||||
inductive SF' (m: Type (u+1) → Type u)[Monad m]: Type u → Type u → Type (u+1) where
|
||||
| seq {as bs cs: Type u}: SF' m as bs → SF' m bs cs → SF' m as cs
|
||||
| fan {as bs cs: Type u}: SF' m as (bs × cs)
|
||||
| rswitcher {as bs cs: Type u}: SF' m as (bs × cs) → SF' m as bs
|
||||
|
||||
def SF.step [Monad m] (sa: as): SF as bs → SF' m as bs × bs
|
||||
| seq sf₁ sf₂ =>
|
||||
let (sf₁', sb) := sf₁.step sa
|
||||
let (sf₂', sc) := sf₂.step sb
|
||||
(sf₁'.seq sf₂', sc)
|
||||
| fan => sorry
|
||||
|
||||
def SF'.step [Monad m] (sa: as): SF' m as bs → SF'.{u} m as bs × bs
|
||||
| seq sf₁ sf₂ =>
|
||||
let (sf₁', sb) := sf₁.step sa
|
||||
let (sf₂', sc) := sf₂.step sb
|
||||
(sf₁'.seq sf₂', sc)
|
||||
| fan => sorry
|
||||
| rswitcher f =>
|
||||
let x := f.step sa
|
||||
let (_, (sb, _)) := x
|
||||
(rswitcher f, sb)
|
||||
Loading…
Add table
Reference in a new issue