From c1bd666bc27c85b093aa72b5df8e1281247d3e78 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 8 Oct 2019 12:44:59 -0700 Subject: [PATCH] feat: stack wrapper around array --- library/Init/Data/Default.lean | 1 + library/Init/Data/Queue/Basic.lean | 9 ++++-- library/Init/Data/Stack/Basic.lean | 41 ++++++++++++++++++++++++++ library/Init/Data/Stack/Default.lean | 7 +++++ library/Init/Lean/TypeClass/Synth.lean | 20 ++++++------- 5 files changed, 64 insertions(+), 14 deletions(-) create mode 100644 library/Init/Data/Stack/Basic.lean create mode 100644 library/Init/Data/Stack/Default.lean diff --git a/library/Init/Data/Default.lean b/library/Init/Data/Default.lean index f622e2b100..11dc7139ac 100644 --- a/library/Init/Data/Default.lean +++ b/library/Init/Data/Default.lean @@ -20,3 +20,4 @@ import Init.Data.Option import Init.Data.HashMap import Init.Data.Random import Init.Data.Queue +import Init.Data.Stack diff --git a/library/Init/Data/Queue/Basic.lean b/library/Init/Data/Queue/Basic.lean index 3b5f1f92f8..0542e17568 100644 --- a/library/Init/Data/Queue/Basic.lean +++ b/library/Init/Data/Queue/Basic.lean @@ -18,15 +18,18 @@ namespace Queue variable {α : Type u} +def empty : Queue α := +{ eList := [], dList := [] } + +def isEmpty (q : Queue α) : Bool := +q.dList.isEmpty && q.eList.isEmpty + def enqueue (v : α) (q : Queue α) : Queue α := { eList := v::q.eList .. q } def enqueueAll (vs : List α) (q : Queue α) : Queue α := { eList := vs ++ q.eList .. q } -def isEmpty (q : Queue α) : Bool := -q.dList.isEmpty && q.eList.isEmpty - def dequeue? (q : Queue α) : Option (α × Queue α) := match q.dList with | d::ds => some (d, { dList := ds, .. q }) diff --git a/library/Init/Data/Stack/Basic.lean b/library/Init/Data/Stack/Basic.lean new file mode 100644 index 0000000000..31ae8bee98 --- /dev/null +++ b/library/Init/Data/Stack/Basic.lean @@ -0,0 +1,41 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Daniel Selsam + +Simple stack API implemented using an array. +-/ +prelude +import Init.Data.Array +import Init.Data.Int +universes u v w + +structure Stack (α : Type u) := +(vals : Array α := Array.empty) + +namespace Stack + +variable {α : Type u} + +def empty : Stack α := +{ vals := Array.empty } + +def isEmpty (s : Stack α) : Bool := +s.vals.isEmpty + +def push (v : α) (s : Stack α) : Stack α := +{ vals := s.vals.push v .. s } + +def peek? (s : Stack α) : Option α := +if s.vals.isEmpty then none else s.vals.get? (s.vals.size-1) + +def peek! [Inhabited α] (s : Stack α) : α := +s.vals.back + +def pop [Inhabited α] (s : Stack α) : Stack α := +{ vals := s.vals.pop .. s } + +def modify [Inhabited α] (s : Stack α) (f : α → α) : Stack α := +{ vals := s.vals.modify (s.vals.size-1) f .. s } + +end Stack diff --git a/library/Init/Data/Stack/Default.lean b/library/Init/Data/Stack/Default.lean new file mode 100644 index 0000000000..47ab22409b --- /dev/null +++ b/library/Init/Data/Stack/Default.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Daniel Selsam +-/ +prelude +import Init.Data.Stack.Basic diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean index 325d1c4d57..be87699c97 100644 --- a/library/Init/Lean/TypeClass/Synth.lean +++ b/library/Init/Lean/TypeClass/Synth.lean @@ -14,6 +14,7 @@ import Init.Lean.Class import Init.Lean.MetavarContext import Init.Lean.TypeClass.Context import Init.Data.PersistentHashMap +import Init.Data.Stack import Init.Data.Queue namespace Lean @@ -65,9 +66,9 @@ structure TCState : Type := (env : Environment) (finalAnswer : Option TypedExpr := none) (mainMVar : Expr := default _) -(generatorStack : Array GeneratorNode := Array.empty) -(consumerStack : Array ConsumerNode := Array.empty) -(resumeQueue : Queue (ConsumerNode × TypedExpr) := {}) +(generatorStack : Stack GeneratorNode := Stack.empty) +(consumerStack : Stack ConsumerNode := Stack.empty) +(resumeQueue : Queue (ConsumerNode × TypedExpr) := Queue.empty) (tableEntries : PersistentHashMap Expr TableEntry := PersistentHashMap.empty) abbrev TCMethod : Type → Type := EState String TCState @@ -173,7 +174,8 @@ do lookupStatus ← get >>= λ ϕ => pure $ ϕ.tableEntries.find anormSubgoal; entry.waiters.mfor (wakeUp answer) def consume : TCMethod Unit := -do cNode ← get >>= λ ϕ => pure ϕ.consumerStack.back; +do cNode ← get >>= λ ϕ => pure ϕ.consumerStack.peek!; + modify $ λ ϕ => { consumerStack := ϕ.consumerStack.pop .. ϕ }; match cNode.remainingSubgoals with | [] => do let answer : TypedExpr := { @@ -182,7 +184,6 @@ do cNode ← get >>= λ ϕ => pure ϕ.consumerStack.back; }; when (Context.eHasTmpMVar answer.val || Context.eHasTmpMVar answer.type) $ throw $ "answer " ++ toString answer ++ " not fully instantiated"; - modify $ λ ϕ => { consumerStack := ϕ.consumerStack.pop .. ϕ }; newAnswer cNode.anormSubgoal answer | mvar::rest => do @@ -190,11 +191,8 @@ do cNode ← get >>= λ ϕ => pure ϕ.consumerStack.back; let waiter : Waiter := Waiter.consumerNode cNode; lookupStatus ← get >>= λ ϕ => pure $ ϕ.tableEntries.find anormSubgoal; match lookupStatus with - | none => do - newSubgoal waiter cNode.ctx mvar; - modify $ λ ϕ => { consumerStack := ϕ.consumerStack.pop .. ϕ } + | none => newSubgoal waiter cNode.ctx mvar | some entry => modify $ λ ϕ => { - consumerStack := ϕ.consumerStack.pop, resumeQueue := entry.answers.foldl (λ rq answer => rq.enqueue (cNode, answer)) ϕ.resumeQueue, tableEntries := ϕ.tableEntries.insert anormSubgoal { waiters := entry.waiters.push waiter, .. entry }, .. ϕ } @@ -214,7 +212,7 @@ do lookupStatus ← get >>= λ ϕ => pure $ ϕ.env.find instName; pure ⟨⟨instVal, instType⟩, ctx⟩ def generate : TCMethod Unit := -do gNode ← get >>= λ ϕ => pure ϕ.generatorStack.back; +do gNode ← get >>= λ ϕ => pure ϕ.generatorStack.peek!; match gNode.remainingInstances with | [] => modify $ λ ϕ => { generatorStack := ϕ.generatorStack.pop, .. ϕ } | inst::insts => do @@ -222,7 +220,7 @@ do gNode ← get >>= λ ϕ => pure ϕ.generatorStack.back; | Instance.const n => constNameToTypedExpr gNode.ctx n | Instance.lDecl lDecl => throw "local instances not yet supported"; result : Option (Context × List Expr) ← tryResolve ctx gNode.futureAnswer instTE; - modify $ λ ϕ => { generatorStack := ϕ.generatorStack.modify (ϕ.generatorStack.size-1) (λ gNode => { remainingInstances := insts .. gNode }) .. ϕ }; + modify $ λ ϕ => { generatorStack := ϕ.generatorStack.modify (λ gNode => { remainingInstances := insts .. gNode }) .. ϕ }; match result with | none => pure () | some (ctx, newMVars) => newConsumerNode gNode.toNode ctx newMVars