From 3c515dcd2159aecc5807fbe12fb232b4fefc8e7c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Dec 2019 09:09:45 -0800 Subject: [PATCH] feat: missing methods --- src/Init/Lean/Meta/AbstractMVars.lean | 2 + src/Init/Lean/Meta/SynthInstance.lean | 180 ++++++++++++++++++-------- 2 files changed, 129 insertions(+), 53 deletions(-) diff --git a/src/Init/Lean/Meta/AbstractMVars.lean b/src/Init/Lean/Meta/AbstractMVars.lean index 4f1131d026..ab95004720 100644 --- a/src/Init/Lean/Meta/AbstractMVars.lean +++ b/src/Init/Lean/Meta/AbstractMVars.lean @@ -14,6 +14,8 @@ structure AbstractMVarsResult := (numMVars : Nat) (expr : Expr) +instance AbstractMVarsResult.inhabited : Inhabited AbstractMVarsResult := ⟨⟨#[], 0, arbitrary _⟩⟩ + def AbstractMVarsResult.beq (r₁ r₂ : AbstractMVarsResult) : Bool := r₁.paramNames == r₂.paramNames && r₁.numMVars == r₂.numMVars && r₁.expr == r₂.expr diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean index 70d65617f1..739b682a7e 100644 --- a/src/Init/Lean/Meta/SynthInstance.lean +++ b/src/Init/Lean/Meta/SynthInstance.lean @@ -29,6 +29,8 @@ structure ConsumerNode := (mctx : MetavarContext) (subgoals : List Expr) +instance Consumernode.inhabited : Inhabited ConsumerNode := ⟨⟨arbitrary _, arbitrary _, arbitrary _, []⟩⟩ + inductive Waiter | consumerNode : ConsumerNode → Waiter | root : Waiter @@ -131,11 +133,11 @@ instance tracer : SimpleMonadTracerAdapter SynthM := getTraceState := getTraceState, modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } } -@[inline] def trace (cls : Name) (mctx : MetavarContext) (msg : Unit → MessageData) : SynthM Unit := +@[inline] def trace (cls : Name) (msg : Unit → MessageData) : SynthM Unit := whenM (MonadTracerAdapter.isTracingEnabledFor cls) $ do ctx ← read; s ← get; - MonadTracerAdapter.addTrace cls (MessageData.context s.env mctx ctx.lctx (msg ())) + MonadTracerAdapter.addTrace cls (MessageData.context s.env s.mctx ctx.lctx (msg ())) @[inline] def liftMeta {α} (x : MetaM α) : SynthM α := adaptState (fun (s : State) => (s.toState, s)) (fun s' s => { toState := s', .. s }) x @@ -151,6 +153,9 @@ forallTelescopeReducing type $ fun _ type => do | some className => do globalInstances ← getGlobalInstances; result ← globalInstances.getUnify type; + result ← result.mapM $ fun c => match c with + | Expr.const constName us _ => do us ← us.mapM (fun _ => mkFreshLevelMVar); pure $ c.updateConst! us + | _ => panic! "global instance is not a constant"; localInstances ← getLocalInstances; let result := localInstances.foldl (fun (result : Array Expr) linst => if linst.className == className then result.push linst.fvar else result) @@ -178,10 +183,6 @@ do mvarType ← inferType mvar; tableEntries := s.tableEntries.insert key entry, .. s } -def wakeUp (answer : Answer) : Waiter → SynthM Unit -| Waiter.root => modify $ fun s => s -- TODO -| Waiter.consumerNode cNode => modify $ fun s => { resumeStack := s.resumeStack.push (cNode, answer), .. s } - def findEntry (key : Expr) : SynthM (Option TableEntry) := do s ← get; pure $ s.tableEntries.find key @@ -192,6 +193,74 @@ do entry? ← findEntry key; | none => panic! "invalid key at synthInstance" | some entry => pure entry +def mkTableKeyFor (mctx : MetavarContext) (mvar : Expr) : MetaM Expr := +withMCtx mctx $ do + mvarType ← inferType mvar; + pure $ mkTableKey mctx mvarType + +private partial def mkInstanceTelescopeAux + (xs : Array Expr) : Array Expr → Nat → List Expr → Expr → Expr → MetaM (List Expr × Expr × Expr) +| subst, j, subgoals, instVal, Expr.forallE n d b c => do + let d := d.instantiateRevRange j subst.size subst; + type ← mkForall xs d; + mvar ← mkFreshExprMVar type; + let arg := mkAppN mvar xs; + let instVal := mkApp instVal arg; + let subgoals := if c.binderInfo.isInstImplicit then mvar::subgoals else subgoals; + let subst := subst.push (mkAppN mvar xs); + mkInstanceTelescopeAux subst j subgoals instVal b +| subst, j, subgoals, instVal, type => do + let type := type.instantiateRevRange j subst.size subst; + type ← whnf type; + if type.isForall then + mkInstanceTelescopeAux subst subst.size subgoals instVal type + else + pure (subgoals, instVal, type) + +def mkInstanceTelescope (xs : Array Expr) (inst : Expr) : MetaM (List Expr × Expr × Expr) := +do instType ← inferType inst; + mkInstanceTelescopeAux xs #[] 0 [] inst instType + +def tryResolveCore (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) := +do mvarType ← inferType mvar; + forallTelescopeReducing mvarType $ fun xs mvarTypeBody => do + (subgoals, instVal, instTypeBody) ← mkInstanceTelescope xs inst; + Meta.trace `Meta.synthInstance.tryResolve $ fun _ => mvarTypeBody ++ " =?= " ++ instTypeBody; + condM (isDefEq mvarTypeBody instTypeBody) + (do instVal ← mkLambda xs instVal; + condM (isDefEq mvar instVal) + (do Meta.trace `Meta.synthInstance.tryResolve $ fun _ => fmt "success"; + mctx ← getMCtx; + pure (some (mctx, subgoals))) + (do Meta.trace `Meta.synthInstance.tryResolve $ fun _ => fmt "failure assigning"; + pure none)) + (do Meta.trace `Meta.synthInstance.tryResolve $ fun _ => fmt "failure"; + pure none) + +def tryResolve (mctx : MetavarContext) (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) := +withMCtx mctx $ tryResolveCore mvar inst + +def tryAnswer (mctx : MetavarContext) (mvar : Expr) (answer : Answer) : MetaM (Option (MetavarContext × List Expr)) := +withMCtx mctx $ do + (_, _, val) ← openAbstractMVarsResult answer; + tryResolveCore mvar val + +def wakeUp (answer : Answer) : Waiter → SynthM Unit +| Waiter.root => + if answer.paramNames.isEmpty && answer.numMVars == 0 then do + s ← get; + let mvar := s.mainMVarId; + condM (isDefEq (mkMVar mvar) answer.expr) + (pure ()) + (do trace `Meta.synthInstance $ fun _ => "fail to assign main metavariable " ++ answer.expr; + pure ()) + else do + (_, _, answerExpr) ← openAbstractMVarsResult answer; + trace `Meta.synthInstance $ fun _ => "answer contains metavariables " ++ answerExpr; + pure () + +| Waiter.consumerNode cNode => modify $ fun s => { resumeStack := s.resumeStack.push (cNode, answer), .. s } + def newAnswer (key : Expr) (answer : Answer) : SynthM Unit := do entry ← getEntry key; if entry.answers.contains answer then pure () @@ -205,11 +274,6 @@ withMCtx cNode.mctx $ do val ← instantiateMVars cNode.mvar; abstractMVars val -def mkTableKeyFor (mctx : MetavarContext) (mvar : Expr) : MetaM Expr := -withMCtx mctx $ do - mvarType ← inferType mvar; - pure $ mkTableKey mctx mvarType - def consume (cNode : ConsumerNode) : SynthM Unit := match cNode.subgoals with | [] => do @@ -226,41 +290,6 @@ match cNode.subgoals with tableEntries := s.tableEntries.insert key { waiters := entry.waiters.push waiter, .. entry }, .. s } -private partial def mkInstanceTelescopeAux - (xs : Array Expr) : Array Expr → Nat → List Expr → Expr → Expr → MetaM (List Expr × Expr × Expr) -| mvars, j, subgoals, instVal, Expr.forallE n d b c => do - let d := d.instantiateRevRange j mvars.size mvars; - type ← mkForall xs d; - mvar ← mkFreshExprMVar type; - let arg := mkAppN mvar xs; - let instVal := mkApp instVal arg; - let subgoals := if c.binderInfo.isInstImplicit then mvar::subgoals else subgoals; - let mvars := mvars.push mvar; - mkInstanceTelescopeAux mvars j subgoals instVal b -| mvars, j, subgoals, instVal, type => do - let type := type.instantiateRevRange j mvars.size mvars; - type ← whnf type; - if type.isForall then - mkInstanceTelescopeAux mvars mvars.size subgoals instVal type - else - pure (subgoals, instVal, type) - -def mkInstanceTelescope (xs : Array Expr) (inst : Expr) : MetaM (List Expr × Expr × Expr) := -do instType ← inferType inst; - mkInstanceTelescopeAux xs #[] 0 [] inst instType - -def tryResolve (mctx : MetavarContext) (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) := -withMCtx mctx $ do - mvarType ← inferType mvar; - forallTelescopeReducing mvarType $ fun xs mvarTypeBody => do - (subgoals, instVal, instTypeBody) ← mkInstanceTelescope xs inst; - condM (isDefEq mvarTypeBody instTypeBody) - (do instVal ← mkLambda xs instVal; - condM (isDefEq mvar instVal) - (do mctx ← getMCtx; pure (some (mctx, subgoals))) - (pure none)) - (pure none) - def getTop : SynthM GeneratorNode := do s ← get; pure s.generatorStack.back @@ -276,15 +305,60 @@ do gNode ← getTop; let idx := gNode.currInstanceIdx - 1; modifyTop $ fun gNode => { currInstanceIdx := idx, .. gNode }; let inst := gNode.instances.get! idx; + trace `Meta.synthInstance $ fun _ => "try instance " ++ inst; result? ← tryResolve gNode.mctx gNode.mvar inst; match result? with | none => pure () | some (mctx, subgoals) => consume { key := gNode.key, mvar := gNode.mvar, subgoals := subgoals, mctx := mctx } -def main (type : Expr) : MetaM (Option Expr) := -do Meta.trace `Meta.synthInstance $ fun _ => type; +def getNextToResume : SynthM (ConsumerNode × Answer) := +do s ← get; + let r := s.resumeStack.back; + modify $ fun s => { resumeStack := s.resumeStack.pop, .. s }; + pure r + +def resume : SynthM Unit := +do (cNode, answer) ← getNextToResume; + match cNode.subgoals with + | [] => panic! "resume found no remaining subgoals" + | mvar::rest => do + result? ← tryAnswer cNode.mctx mvar answer; + match result? with + | none => pure () + | some (mctx, subgoals) => consume { key := cNode.key, mvar := cNode.mvar, subgoals := subgoals ++ rest, mctx := mctx } + + +def step : SynthM Bool := +do s ← get; + if !s.resumeStack.isEmpty then do resume; pure true + else if !s.generatorStack.isEmpty then do generate; pure true + else pure false + +partial def synth : Nat → SynthM (Option Expr) +| 0 => do + trace `Meta.synthInstance $ fun _ => fmt "synthInstance is out of fule"; + pure none +| n+1 => do + condM step + (do s ← get; + val? ← getExprMVarAssignment s.mainMVarId; + match val? with + | none => synth n + | some val => do + val ← instantiateMVars val; + pure (some val)) + (do trace `Meta.synthInstance $ fun _ => fmt "failed"; + pure none) + +def main (type : Expr) (fuel : Nat) : MetaM (Option Expr) := +traceCtx `Meta.synthInstance $ do + Meta.trace `Meta.synthInstance $ fun _ => "main goal " ++ type; mvar ← mkFreshExprMVar type; - pure none -- TODO + mctx ← getMCtx; + let key := mkTableKey mctx type; + adaptState' (fun (s : Meta.State) => { State . mainMVarId := mvar.mvarId!, .. s }) (fun (s : State) => s.toState) $ do + newSubgoal key mvar Waiter.root; + synth fuel end SynthInstance @@ -348,7 +422,7 @@ try $ <&&> r.exprReplacements.allM (fun ⟨e, e'⟩ => isExprDefEqAux e e') -def synthInstance (type : Expr) : MetaM (Option Expr) := +def synthInstance (type : Expr) (fuel : Nat := 10000) : MetaM (Option Expr) := usingTransparency TransparencyMode.reducible $ do type ← instantiateMVars type; type ← preprocess type; @@ -358,7 +432,7 @@ usingTransparency TransparencyMode.reducible $ do | none => do result ← withNewMCtxDepth $ do { (normType, replacements) ← preprocessOutParam type; - result? ← SynthInstance.main normType; + result? ← SynthInstance.main normType fuel; match result? with | none => pure none | some result => do @@ -378,10 +452,10 @@ usingTransparency TransparencyMode.reducible $ do /-- Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if instance cannot be synthesized right now because `type` contains metavariables. -/ -def trySynthInstance (type : Expr) : MetaM (LOption Expr) := +def trySynthInstance (type : Expr) (fuel : Nat := 10000) : MetaM (LOption Expr) := adaptReader (fun (ctx : Context) => { config := { isDefEqStuckEx := true, .. ctx.config }, .. ctx }) $ catch - (toLOptionM $ synthInstance type) + (toLOptionM $ synthInstance type fuel) (fun ex => match ex with | Exception.isExprDefEqStuck _ _ _ => pure LOption.undef | Exception.isLevelDefEqStuck _ _ _ => pure LOption.undef