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

feat: solves mvars in reverse order during tabled tc

Browse source
This commit is contained in:
Daniel Selsam 2019-11-09 17:04:58 -08:00 • committed by Leonardo de Moura
parent 1dd8770b3a
commit bff5e4ed37
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/Init/Lean/TypeClass/Synth.lean
View file

@ -125,13 +125,13 @@ do let mvarType := ctx.eInstantiate (ctx.eInfer mvar);
.. ϕ
}
partial def introduceMVars (lctx : LocalContext) (locals : Array Expr) : Context → Expr → Expr → Array Expr → Context × Expr × Expr × Array Expr
partial def introduceMVars (lctx : LocalContext) (locals : Array Expr) : Context → Expr → Expr → List Expr → Context × Expr × Expr × List Expr
| ctx, instVal, Expr.forallE _ info domain body, mvars => do
let ⟨mvar, ctx⟩ := (Context.eNewMeta $ lctx.mkForall locals domain).run ctx;
let arg := mkApp mvar locals;
let instVal := Expr.app instVal arg;
let instType := body.instantiate1 arg;
let mvars := if info.isInstImplicit then mvars.push mvar else mvars;
let mvars := if info.isInstImplicit then mvar::mvars else mvars;
introduceMVars ctx instVal instType mvars
| ctx, instVal, instType, mvars => (ctx, instVal, instType, mvars)
@ -149,10 +149,10 @@ def tryResolve (ctx : Context) (futureAnswer : TypedExpr) (instTE : TypedExpr) :
do let ⟨mvar, mvarType⟩ := futureAnswer;
let ⟨instVal, instType⟩ := instTE;
let ⟨lctx, mvarType, locals⟩ := introduceLocals 0 {} #[] mvarType;
let ⟨ctx, instVal, instType, newMVars⟩ := introduceMVars lctx locals ctx instVal instType #[];
let ⟨ctx, instVal, instType, newMVars⟩ := introduceMVars lctx locals ctx instVal instType [];
match (Context.eUnify mvarType instType *> Context.eUnify mvar (lctx.mkLambda locals instVal)).run ctx with
| EStateM.Result.error msg _ => pure none
| EStateM.Result.ok _ ctx => pure $ some $ (ctx, newMVars.toList) -- TODO(dselsam): rm toList
| EStateM.Result.ok _ ctx => pure $ some $ (ctx, newMVars)
def newConsumerNode (node : Node) (ctx : Context) (newMVars : List Expr) : TCMethod Unit :=
let cNode : ConsumerNode := { remainingSubgoals := newMVars, ctx := ctx, .. node };

2
tests/lean/run/typeclass_coerce.lean
View file

@ -13,7 +13,7 @@ class HasCoerce (a b : Type) :=
def coerce {a b : Type} [HasCoerce a b] : a → b :=
@HasCoerce.coerce a b _
instance coerceTrans {a b c : Type} [HasCoerce a b] [HasCoerce b c] : HasCoerce a c :=
instance coerceTrans {a b c : Type} [HasCoerce b c] [HasCoerce a b] : HasCoerce a c :=
⟨fun x => coerce (coerce x : b)⟩
instance coerceBoolToProp : HasCoerce Bool Prop :=