chore: remove prototype for the new type class resolution
The code has been integrated into the `Meta` module.
This commit is contained in:
Leonardo de Moura
parent
e0089c89df
commit
4ce457eb51
5 changed files with 0 additions and 706 deletions
|
|
@ -18,7 +18,6 @@ import Init.Lean.EqnCompiler
|
|||
import Init.Lean.Class
|
||||
import Init.Lean.LocalContext
|
||||
import Init.Lean.MetavarContext
|
||||
import Init.Lean.TypeClass
|
||||
import Init.Lean.Trace
|
||||
import Init.Lean.AuxRecursor
|
||||
import Init.Lean.Linter
|
||||
|
|
|
|||
|
|
@ -1,7 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Daniel Selsam, Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import Init.Lean.TypeClass.Basic
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Daniel Selsam, Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import Init.Lean.Environment
|
||||
import Init.Lean.TypeClass.Synth
|
||||
|
||||
namespace Lean
|
||||
namespace TypeClass
|
||||
|
||||
/- Entry point for the `#synth` command used for testing. -/
|
||||
@[export lean_typeclass_synth_command]
|
||||
def synthCommand (env : Environment) (goalType : Expr) : ExceptT String Id Expr :=
|
||||
match (synth goalType).run { env := env } with
|
||||
| EStateM.Result.ok val _ => pure val
|
||||
| EStateM.Result.error msg _ => throw msg
|
||||
|
||||
end TypeClass
|
||||
end Lean
|
||||
|
|
@ -1,351 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Daniel Selsam
|
||||
|
||||
Custom unifier for tabled typeclass resolution.
|
||||
|
||||
Note: this file will be removed once the unifier is implemented in Lean.
|
||||
-/
|
||||
prelude
|
||||
import Init.Data.Nat
|
||||
import Init.Data.PersistentArray
|
||||
import Init.Lean.Expr
|
||||
import Init.Lean.MetavarContext
|
||||
|
||||
namespace Lean
|
||||
namespace TypeClass
|
||||
|
||||
structure Context : Type :=
|
||||
(uVals : PersistentArray (Option Level) := PersistentArray.empty)
|
||||
(eTypes : PersistentArray Expr := PersistentArray.empty)
|
||||
(eVals : PersistentArray (Option Expr) := PersistentArray.empty)
|
||||
|
||||
instance Context.Inhabited : Inhabited Context := ⟨{}⟩
|
||||
|
||||
structure ContextFail : Type :=
|
||||
(msg : String)
|
||||
|
||||
abbrev ContextFn : Type → Type := EStateM ContextFail Context
|
||||
|
||||
namespace Context
|
||||
|
||||
def metaPrefix : Name :=
|
||||
`_tc_meta
|
||||
|
||||
def alphaMetaPrefix : Name :=
|
||||
`_tc_alpha
|
||||
|
||||
-- Expressions
|
||||
|
||||
def eMetaIdx : Expr → Option Nat
|
||||
| Expr.mvar (Name.num n idx _) _ => guard (n == metaPrefix) *> pure idx
|
||||
| _ => none
|
||||
|
||||
def eIsMeta (e : Expr) : Bool := (eMetaIdx e).toBool
|
||||
|
||||
def eNewMeta (type : Expr) : StateM Context Expr :=
|
||||
do ctx ← get;
|
||||
let idx := ctx.eTypes.size;
|
||||
set { eTypes := ctx.eTypes.push type, eVals := ctx.eVals.push none, .. ctx };
|
||||
pure $ mkMVar (mkNameNum metaPrefix idx)
|
||||
|
||||
def eLookupIdx (idx : Nat) : StateM Context (Option Expr) :=
|
||||
do ctx ← get; pure $ ctx.eVals.get! idx
|
||||
|
||||
partial def eShallowInstantiate : Expr → StateM Context Expr
|
||||
| e =>
|
||||
match eMetaIdx e with
|
||||
| some idx => get >>= λ ctx =>
|
||||
match ctx.eVals.get! idx with
|
||||
| none => pure e
|
||||
| some v => eShallowInstantiate v
|
||||
| none => pure e
|
||||
|
||||
def eInferIdx (idx : Nat) : StateM Context Expr :=
|
||||
do ctx ← get; pure $ ctx.eTypes.get! idx
|
||||
|
||||
def eInfer (ctx : Context) (mvar : Expr) : Expr :=
|
||||
match eMetaIdx mvar with
|
||||
| some idx => ctx.eTypes.get! idx
|
||||
| none => panic! "eInfer called on non-(tmp-)mvar"
|
||||
|
||||
def eAssignIdx (idx : Nat) (e : Expr) : StateM Context Unit :=
|
||||
modify $ λ ctx => { eVals := ctx.eVals.set idx (some e) .. ctx }
|
||||
|
||||
def eAssign (mvar : Expr) (e : Expr) : StateM Context Unit :=
|
||||
match eMetaIdx mvar with
|
||||
| some idx => modify $ λ ctx => { eVals := ctx.eVals.set idx (some e) .. ctx }
|
||||
| _ => panic! "eAssign called on non-(tmp-)mvar"
|
||||
|
||||
partial def eFind (f : Expr → Bool) : Expr → Bool
|
||||
| e =>
|
||||
if f e
|
||||
then true
|
||||
else
|
||||
match e with
|
||||
| Expr.app f a _ => eFind f || eFind a
|
||||
| Expr.forallE _ d b _ => eFind d || eFind b
|
||||
| _ => false
|
||||
|
||||
def eOccursIn (t₀ : Expr) (e : Expr) : Bool :=
|
||||
eFind (λ t => t == t₀) e
|
||||
|
||||
def eHasETmpMVar (e : Expr) : Bool :=
|
||||
eFind eIsMeta e
|
||||
|
||||
-- Levels
|
||||
|
||||
def uMetaIdx : Level → Option Nat
|
||||
| Level.mvar (Name.num n idx _) _ => guard (n == metaPrefix) *> pure idx
|
||||
| _ => none
|
||||
|
||||
def uIsMeta (l : Level) : Bool := (uMetaIdx l).toBool
|
||||
|
||||
def uNewMeta : StateM Context Level :=
|
||||
do ctx ← get;
|
||||
let idx := ctx.uVals.size;
|
||||
set { uVals := ctx.uVals.push none, .. ctx };
|
||||
pure $ mkLevelMVar (mkNameNum metaPrefix idx)
|
||||
|
||||
def uLookupIdx (idx : Nat) : StateM Context (Option Level) :=
|
||||
do ctx ← get; pure $ ctx.uVals.get! idx
|
||||
|
||||
partial def uShallowInstantiate : Level → StateM Context Level
|
||||
| l =>
|
||||
match uMetaIdx l with
|
||||
| some idx => get >>= λ ctx =>
|
||||
match ctx.uVals.get! idx with
|
||||
| none => pure l
|
||||
| some v => uShallowInstantiate v
|
||||
| none => pure l
|
||||
|
||||
def uAssignIdx (idx : Nat) (l : Level) : StateM Context Unit :=
|
||||
modify $ λ ctx => { uVals := ctx.uVals.set idx (some l) .. ctx }
|
||||
|
||||
def uAssign (umvar : Level) (l : Level) : StateM Context Unit :=
|
||||
match uMetaIdx umvar with
|
||||
| some idx => modify $ λ ctx => { uVals := ctx.uVals.set idx (some l) .. ctx }
|
||||
| _ => panic! "uassign called on non-(tmp-)mvar"
|
||||
|
||||
partial def uFind (f : Level → Bool) : Level → Bool
|
||||
| l =>
|
||||
if f l
|
||||
then true
|
||||
else
|
||||
match l with
|
||||
| Level.succ l _ => uFind l
|
||||
| Level.max l₁ l₂ _ => uFind l₁ || uFind l₂
|
||||
| Level.imax l₁ l₂ _ => uFind l₁ || uFind l₂
|
||||
| _ => false
|
||||
|
||||
def uOccursIn (l₀ : Level) (l : Level) : Bool :=
|
||||
uFind (λ l => l == l₀) l
|
||||
|
||||
def uHasTmpMVar (l : Level) : Bool :=
|
||||
uFind uIsMeta l
|
||||
|
||||
partial def uUnify : Level → Level → EStateM String Context Unit
|
||||
| l₁, l₂ => do
|
||||
l₁ ← EStateM.fromStateM $ uShallowInstantiate l₁;
|
||||
l₂ ← EStateM.fromStateM $ uShallowInstantiate l₂;
|
||||
if uIsMeta l₂ && !(uIsMeta l₁)
|
||||
then uUnify l₂ l₁
|
||||
else
|
||||
match l₁, l₂ with
|
||||
| Level.zero _, Level.zero _ => pure ()
|
||||
| Level.param p₁ _, Level.param p₂ _ => when (p₁ != p₂) $ throw "Level.param clash"
|
||||
| Level.succ l₁ _, Level.succ l₂ _ => uUnify l₁ l₂
|
||||
| Level.max l₁₁ l₁₂ _, Level.max l₂₁ l₂₂ _ => uUnify l₁₁ l₂₁ *> uUnify l₁₂ l₂₂
|
||||
| Level.imax l₁₁ l₁₂ _, Level.imax l₂₁ l₂₂ _ => uUnify l₁₁ l₂₁ *> uUnify l₁₂ l₂₂
|
||||
| Level.mvar _ _, _ =>
|
||||
match uMetaIdx l₁ with
|
||||
| none => when (!(l₁ == l₂)) $ throw "Level.mvar clash"
|
||||
| some idx => do when (uOccursIn l₁ l₂) $ throw "occurs";
|
||||
EStateM.fromStateM $ uAssignIdx idx l₂
|
||||
| _, _ => throw $ "lUnify: " ++ toString l₁ ++ " !=?= " ++ toString l₂
|
||||
|
||||
partial def uInstantiate (ctx : Context) : Level → Level
|
||||
| l => if (!l.hasMVar)
|
||||
then l
|
||||
else
|
||||
match uMetaIdx l with
|
||||
| some idx => match (Context.uLookupIdx idx).run' ctx with
|
||||
| some t => uInstantiate t
|
||||
| none => l
|
||||
| none =>
|
||||
match l with
|
||||
| Level.succ l _ => mkLevelSucc $ uInstantiate l
|
||||
| Level.max l₁ l₂ _ => mkLevelMax (uInstantiate l₁) (uInstantiate l₂)
|
||||
| Level.imax l₁ l₂ _ => mkLevelIMax (uInstantiate l₁) (uInstantiate l₂)
|
||||
| _ => l
|
||||
|
||||
-- Expressions and Levels
|
||||
|
||||
def eHasTmpMVar (e : Expr) : Bool :=
|
||||
if e.hasMVar
|
||||
then eFind (λ t => eIsMeta t || (t.isConst && t.constLevels!.any uHasTmpMVar)) e
|
||||
else false
|
||||
|
||||
partial def slowWhnfApp (args : Array Expr) : Expr → Nat → Expr
|
||||
| f@(Expr.lam _ d b _), i =>
|
||||
if h : i < args.size then
|
||||
slowWhnfApp (b.instantiate1 (args.get ⟨i, h⟩)) (i+1)
|
||||
else
|
||||
f
|
||||
| f, i =>
|
||||
if h : i < args.size then
|
||||
slowWhnfApp (mkApp f (args.get ⟨i, h⟩)) (i+1)
|
||||
else
|
||||
f
|
||||
|
||||
partial def slowWhnf : Expr → Expr
|
||||
| e => if e.isApp then slowWhnfApp e.getAppArgs (slowWhnf e.getAppFn) 0 else e
|
||||
|
||||
partial def eUnify : Expr → Expr → EStateM String Context Unit
|
||||
| e₁, e₂ =>
|
||||
if !e₁.hasMVar && !e₂.hasMVar
|
||||
then unless (e₁ == e₂) $ throw $ "eUnify: " ++ toString e₁ ++ " !=?= " ++ toString e₂
|
||||
else do
|
||||
e₁ ← slowWhnf <$> (EStateM.fromStateM $ eShallowInstantiate e₁);
|
||||
e₂ ← slowWhnf <$> (EStateM.fromStateM $ eShallowInstantiate e₂);
|
||||
if e₁.isMVar && e₂.isMVar && e₁ == e₂ then pure ()
|
||||
else if eIsMeta e₂ && !(eIsMeta e₁) then eUnify e₂ e₁
|
||||
else if e₁.isBVar && e₂.isBVar && e₁.bvarIdx! == e₂.bvarIdx! then pure ()
|
||||
else if e₁.isFVar && e₂.isFVar && e₁.fvarId! == e₂.fvarId! then pure ()
|
||||
else if e₁.isConst && e₂.isConst && e₁.constName! == e₂.constName! then
|
||||
List.forM₂ uUnify e₁.constLevels! e₂.constLevels!
|
||||
else if e₁.isApp && e₂.isApp && e₁.getAppNumArgs == e₂.getAppNumArgs then do
|
||||
let args₁ := e₁.getAppArgs;
|
||||
let args₂ := e₂.getAppArgs;
|
||||
eUnify e₁.getAppFn e₂.getAppFn;
|
||||
args₁.size.forM $ fun i => eUnify (args₁.get! i) (args₂.get! i)
|
||||
else if e₁.isForall && e₂.isForall then do
|
||||
eUnify e₁.bindingDomain! e₂.bindingDomain!;
|
||||
eUnify e₁.bindingBody! e₂.bindingBody!
|
||||
else if eIsMeta e₁ && !(eOccursIn e₂ e₁) then
|
||||
match eMetaIdx e₁ with
|
||||
| some idx => EStateM.fromStateM $ eAssignIdx idx e₂
|
||||
| none => panic! "UNREACHABLE"
|
||||
else
|
||||
throw $ "eUnify: " ++ toString e₁ ++ " !=?= " ++ toString e₂
|
||||
|
||||
partial def eInstantiate (ctx : Context) : Expr → Expr
|
||||
| e =>
|
||||
if !e.hasMVar -- conservative check (includes regular mvars as well)
|
||||
then e
|
||||
else
|
||||
match e with
|
||||
| Expr.forallE n d b c => mkForall n c.binderInfo (eInstantiate d) (eInstantiate b)
|
||||
| Expr.lam n d b c => mkLambda n c.binderInfo (eInstantiate d) (eInstantiate b)
|
||||
| Expr.const n ls _ => mkConst n (ls.map $ uInstantiate ctx)
|
||||
| Expr.app e₁ e₂ _ => mkApp (eInstantiate e₁) (eInstantiate e₂)
|
||||
| _ =>
|
||||
match eMetaIdx e with
|
||||
| none => e
|
||||
| some idx => do
|
||||
match (eLookupIdx idx).run' ctx with
|
||||
| some t => eInstantiate t
|
||||
| none => e
|
||||
|
||||
-- AlphaNormalization
|
||||
|
||||
structure MetaNormData (α : Type) : Type :=
|
||||
(ctx : α)
|
||||
(eRenameMap : RBMap Nat Nat (λ n₁ n₂ => n₁ < n₂) := mkRBMap _ _ _)
|
||||
(uRenameMap : RBMap Nat Nat (λ n₁ n₂ => n₁ < n₂) := mkRBMap _ _ _)
|
||||
|
||||
structure MetaNormFuncs (α : Type) : Type :=
|
||||
(uNewMeta : Nat → StateM (MetaNormData α) Level)
|
||||
(uMkMeta : Nat → StateM (MetaNormData α) Level)
|
||||
(eNewMeta : Nat → StateM (MetaNormData α) Expr)
|
||||
(eMkMeta : Nat → StateM (MetaNormData α) Expr)
|
||||
|
||||
partial def uMetaNormalizeCore {α : Type} (fs : MetaNormFuncs α) : Level → StateM (MetaNormData α) Level
|
||||
| l =>
|
||||
if !l.hasMVar then pure l else
|
||||
match l with
|
||||
| Level.zero _ => pure l
|
||||
| Level.param _ _ => pure l
|
||||
| Level.succ l _ => do l ← uMetaNormalizeCore l;
|
||||
pure $ mkLevelSucc l
|
||||
| Level.max l₁ l₂ _ => do l₁ ← uMetaNormalizeCore l₁;
|
||||
l₂ ← uMetaNormalizeCore l₂;
|
||||
pure $ mkLevelMax l₁ l₂
|
||||
| Level.imax l₁ l₂ _ => do l₁ ← uMetaNormalizeCore l₁;
|
||||
l₂ ← uMetaNormalizeCore l₂;
|
||||
pure $ mkLevelIMax l₁ l₂
|
||||
| Level.mvar m _ =>
|
||||
match uMetaIdx l with
|
||||
| none => pure l
|
||||
| some idx => do
|
||||
lookupStatus ← get >>= λ ϕ => pure $ ϕ.uRenameMap.find idx;
|
||||
match lookupStatus with
|
||||
| none => fs.uNewMeta idx
|
||||
| some idx => fs.uMkMeta idx
|
||||
|
||||
partial def eMetaNormalizeCore {α : Type} (fs : MetaNormFuncs α) : Expr → StateM (MetaNormData α) Expr
|
||||
| e =>
|
||||
if e.isConst then do
|
||||
ls ← e.constLevels!.mapM (uMetaNormalizeCore fs);
|
||||
pure $ Expr.updateConst! e ls
|
||||
else if e.isFVar then pure e
|
||||
else if !e.hasMVar then pure e
|
||||
else match e with
|
||||
| Expr.app f a _ => do
|
||||
f ← eMetaNormalizeCore f;
|
||||
a ← eMetaNormalizeCore a;
|
||||
pure $ mkApp f a
|
||||
| Expr.forallE n d b c => do
|
||||
d ← eMetaNormalizeCore d;
|
||||
b ← eMetaNormalizeCore b;
|
||||
pure $ mkForall n c.binderInfo d b
|
||||
| _ =>
|
||||
match eMetaIdx e with
|
||||
| none => pure e
|
||||
| some idx => do
|
||||
lookupStatus ← get >>= λ ϕ => pure $ ϕ.eRenameMap.find idx;
|
||||
match lookupStatus with
|
||||
| none => fs.eNewMeta idx
|
||||
| some idx => fs.eMkMeta idx
|
||||
|
||||
def αNorm (e : Expr) : Expr :=
|
||||
let fs : MetaNormFuncs Unit := {
|
||||
uNewMeta := λ idx => do {
|
||||
l ← get >>= λ ϕ => pure $ mkLevelMVar (mkNameNum alphaMetaPrefix ϕ.uRenameMap.size);
|
||||
modify $ λ ϕ => { uRenameMap := ϕ.uRenameMap.insert idx ϕ.uRenameMap.size .. ϕ };
|
||||
pure l },
|
||||
uMkMeta := λ idx => pure $ mkLevelMVar (mkNameNum alphaMetaPrefix idx),
|
||||
eNewMeta := λ idx => do {
|
||||
e ← get >>= λ ϕ => pure $ mkMVar (mkNameNum alphaMetaPrefix ϕ.eRenameMap.size);
|
||||
modify $ λ ϕ => { eRenameMap := ϕ.eRenameMap.insert idx ϕ.eRenameMap.size .. ϕ };
|
||||
pure e },
|
||||
eMkMeta := λ idx => pure $ mkMVar (mkNameNum alphaMetaPrefix idx)
|
||||
};
|
||||
(eMetaNormalizeCore fs e).run' { ctx := () }
|
||||
|
||||
def internalize (oldCtx : Context) (val type : Expr) (newCtx : Context) : Expr × Expr × Context :=
|
||||
let fs : MetaNormFuncs (Context × Context) := {
|
||||
uNewMeta := λ idx => do {
|
||||
(oldCtx, newCtx) ← get >>= λ ϕ => pure ϕ.ctx;
|
||||
(l, newCtx) ← pure $ StateT.run Context.uNewMeta newCtx;
|
||||
match Context.uMetaIdx l with
|
||||
| some newIdx => modify $ λ ϕ => { ctx := (oldCtx, newCtx), uRenameMap := ϕ.uRenameMap.insert idx newIdx, .. ϕ }
|
||||
| none => panic "unreachable";
|
||||
pure l },
|
||||
uMkMeta := λ idx => pure $ mkLevelMVar (mkNameNum metaPrefix idx),
|
||||
eNewMeta := λ idx => do {
|
||||
(oldCtx, newCtx) ← get >>= λ ϕ => pure ϕ.ctx;
|
||||
(e, newCtx) ← pure $ StateT.run (Context.eNewMeta $ oldCtx.eTypes.get! idx) newCtx;
|
||||
match Context.eMetaIdx e with
|
||||
| some newIdx => modify $ λ ϕ => { ctx := (oldCtx, newCtx), eRenameMap := ϕ.eRenameMap.insert idx newIdx, .. ϕ }
|
||||
| none => panic "unreachable";
|
||||
pure e },
|
||||
eMkMeta := λ idx => pure $ mkMVar (mkNameNum metaPrefix idx)
|
||||
};
|
||||
match (do newType ← eMetaNormalizeCore fs type; newVal ← eMetaNormalizeCore fs val; pure (newVal, newType)).run { ctx := (oldCtx, newCtx) } with
|
||||
| ((newVal, newType), ϕ) => (newVal, newType, ϕ.ctx.2)
|
||||
|
||||
end Context
|
||||
end TypeClass
|
||||
end Lean
|
||||
|
|
@ -1,326 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Daniel Selsam
|
||||
|
||||
Typeclass synthesis using tabled resolution.
|
||||
|
||||
Note: this file will be need to be updated once the unifier is implemented in Lean.
|
||||
-/
|
||||
prelude
|
||||
import Init.Lean.Expr
|
||||
import Init.Lean.Environment
|
||||
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
|
||||
namespace TypeClass
|
||||
|
||||
structure TypedExpr : Type :=
|
||||
(val type : Expr)
|
||||
|
||||
instance TypedExpr.HasToString : HasToString TypedExpr :=
|
||||
⟨λ ⟨val, type⟩ => "TypedExpr(" ++ toString val ++ ", " ++ toString type ++ ")"⟩
|
||||
|
||||
instance TypedExpr.Inhabited : Inhabited TypedExpr :=
|
||||
⟨⟨arbitrary _, arbitrary _⟩⟩
|
||||
|
||||
structure Answer : Type :=
|
||||
(ctx : Context) (typedExpr : TypedExpr)
|
||||
|
||||
instance Answer.HasToString : HasToString Answer :=
|
||||
⟨λ ⟨_, ⟨val, type⟩⟩ => "Answer(" ++ toString val ++ ", " ++ toString type ++ ")"⟩
|
||||
|
||||
instance Answer.Inhabited : Inhabited TypedExpr :=
|
||||
⟨⟨arbitrary _, arbitrary _⟩⟩
|
||||
|
||||
structure Node : Type :=
|
||||
(anormSubgoal : Expr)
|
||||
(ctx : Context)
|
||||
(futureAnswer : TypedExpr)
|
||||
|
||||
instance Node.Inhabited : Inhabited Node :=
|
||||
⟨⟨arbitrary _, {}, arbitrary _⟩⟩
|
||||
|
||||
structure ConsumerNode extends Node :=
|
||||
(remainingSubgoals : List Expr)
|
||||
|
||||
instance ConsumerNode.Inhabited : Inhabited ConsumerNode :=
|
||||
⟨⟨arbitrary _, arbitrary _⟩⟩
|
||||
|
||||
inductive Waiter : Type
|
||||
| consumerNode : ConsumerNode → Waiter
|
||||
| root : Waiter
|
||||
|
||||
def Waiter.isRoot : Waiter → Bool
|
||||
| Waiter.consumerNode _ => false
|
||||
| root => true
|
||||
|
||||
-- TODO(dselsam): support local instances once elaborator is in Lean
|
||||
inductive Instance : Type
|
||||
| lDecl : LocalDecl → Instance
|
||||
| const : Name → Instance
|
||||
|
||||
structure GeneratorNode extends Node :=
|
||||
(remainingInstances : List Instance)
|
||||
|
||||
instance GeneratorNode.Inhabited : Inhabited GeneratorNode :=
|
||||
⟨⟨arbitrary _, arbitrary _⟩⟩
|
||||
|
||||
structure TableEntry : Type :=
|
||||
(waiters : Array Waiter)
|
||||
(answers : Array Answer := #[])
|
||||
|
||||
structure TCState : Type :=
|
||||
(env : Environment)
|
||||
(finalAnswer : Option TypedExpr := none)
|
||||
(mainMVar : Expr := arbitrary _)
|
||||
(generatorStack : Stack GeneratorNode := Stack.empty)
|
||||
(consumerStack : Stack ConsumerNode := Stack.empty)
|
||||
(resumeQueue : Queue (ConsumerNode × Answer) := Queue.empty)
|
||||
(tableEntries : PersistentHashMap Expr TableEntry := PersistentHashMap.empty)
|
||||
|
||||
abbrev TCMethod : Type → Type := EStateM String TCState
|
||||
|
||||
-- TODO(dselsam): once `whnf` is ready, need a more expensive pass as a backup,
|
||||
-- that creates locals and calls `whnf` on every recursion.
|
||||
-- See: [type_context.cpp] optional<name> type_context_old::is_full_class(expr type)
|
||||
-- TODO(dselsam): check if we need to call `get_decl()` as well in the `const` case.
|
||||
def quickIsClass (env : Environment) : Expr → Option (Option Name)
|
||||
| Expr.letE _ _ _ _ _ => none
|
||||
| Expr.proj _ _ _ _ => none
|
||||
| Expr.mdata _ e _ => quickIsClass e
|
||||
| Expr.const n _ _ => if isClass env n then some (some n) else none
|
||||
| Expr.forallE _ _ b _ => quickIsClass b
|
||||
| Expr.app e _ _ =>
|
||||
let f := e.getAppFn;
|
||||
if f.isConst && isClass env f.constName! then some (some f.constName!)
|
||||
else if f.isLambda then none
|
||||
else some none
|
||||
| _ => some none
|
||||
|
||||
def newSubgoal (waiter : Waiter) (ctx : Context) (anormSubgoal mvar : Expr) : TCMethod Unit :=
|
||||
do let mvarType := ctx.eInstantiate (ctx.eInfer mvar);
|
||||
isClassStatus ← get >>= λ ϕ => pure $ quickIsClass ϕ.env mvarType;
|
||||
match isClassStatus with
|
||||
| none => throw $ "quickIsClass not sufficient to show `" ++ toString mvarType ++ "` is a class"
|
||||
| some none => throw $ "found non-class goal `" ++ toString mvarType ++ "`"
|
||||
| some (some n) => do
|
||||
let ⟨newVal, newType, newCtx⟩ := Context.internalize ctx mvar mvarType {};
|
||||
gNode ← get >>= λ ϕ => pure {
|
||||
GeneratorNode .
|
||||
ctx := newCtx,
|
||||
anormSubgoal := anormSubgoal,
|
||||
futureAnswer := ⟨newVal, newType⟩,
|
||||
remainingInstances := (getClassInstances ϕ.env n).map Instance.const
|
||||
};
|
||||
let tableEntry : TableEntry := { waiters := #[waiter] };
|
||||
modify $ λ ϕ => {
|
||||
generatorStack := ϕ.generatorStack.push gNode,
|
||||
tableEntries := ϕ.tableEntries.insert gNode.anormSubgoal tableEntry,
|
||||
.. ϕ
|
||||
}
|
||||
|
||||
partial def introduceMVars (lctx : LocalContext) (locals : Array Expr) : Context → Expr → Expr → List Expr → Context × Expr × Expr × List Expr
|
||||
| ctx, instVal, Expr.forallE _ domain body c, mvars => do
|
||||
let info := c.binderInfo;
|
||||
let ⟨mvar, ctx⟩ := (Context.eNewMeta $ lctx.mkForall locals domain).run ctx;
|
||||
let arg := mkAppN mvar locals;
|
||||
let instVal := mkApp instVal arg;
|
||||
let instType := body.instantiate1 arg;
|
||||
let mvars := if info.isInstImplicit then mvar::mvars else mvars;
|
||||
introduceMVars ctx instVal instType mvars
|
||||
|
||||
| ctx, instVal, instType, mvars => (ctx, instVal, instType, mvars)
|
||||
|
||||
partial def introduceLocals : Nat → LocalContext → Array Expr → Expr → LocalContext × Expr × Array Expr
|
||||
| nextIdx, lctx, ls, Expr.forallE name domain body c =>
|
||||
let info := c.binderInfo;
|
||||
let idxName : Name := mkNameNum `_tmp nextIdx;
|
||||
let lctx := lctx.mkLocalDecl idxName name domain info;
|
||||
let l : Expr := mkFVar idxName;
|
||||
introduceLocals (nextIdx + 1) lctx (ls.push l) (body.instantiate1 l)
|
||||
|
||||
| _, lctx, ls, e => (lctx, e, ls)
|
||||
|
||||
def tryResolve (ctx : Context) (futureAnswer : TypedExpr) (instTE : TypedExpr) : TCMethod (Option (Context × List Expr)) :=
|
||||
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 [];
|
||||
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)
|
||||
|
||||
def newConsumerNode (node : Node) (ctx : Context) (newMVars : List Expr) : TCMethod Unit :=
|
||||
let cNode : ConsumerNode := { remainingSubgoals := newMVars, ctx := ctx, .. node };
|
||||
modify $ λ ϕ => { consumerStack := ϕ.consumerStack.push cNode, .. ϕ }
|
||||
|
||||
def resume : TCMethod Unit :=
|
||||
do ((cNode, answer), resumeQueue) ← get >>= λ ϕ =>
|
||||
match ϕ.resumeQueue.dequeue? with
|
||||
| none => throw "resume found nothing to resume"
|
||||
| some result => pure result;
|
||||
match cNode.remainingSubgoals with
|
||||
| [] => throw "resume found no remaining subgoals"
|
||||
| (mvar::rest) => do
|
||||
let newCtx : Context := cNode.ctx;
|
||||
let ⟨newVal, newType, newCtx⟩ : Expr × Expr × Context := Context.internalize answer.ctx answer.typedExpr.val answer.typedExpr.type newCtx;
|
||||
result : Option (Context × List Expr) ←
|
||||
tryResolve newCtx ⟨mvar, newCtx.eInfer mvar⟩ ⟨newVal, newType⟩;
|
||||
modify $ λ ϕ => { resumeQueue := resumeQueue, .. ϕ };
|
||||
match result with
|
||||
| none => pure ()
|
||||
| some (newCtx, newMVars) => newConsumerNode cNode.toNode newCtx (newMVars ++ rest)
|
||||
|
||||
def wakeUp (answer : Answer) : Waiter → TCMethod Unit
|
||||
| Waiter.root => modify $ λ ϕ => { finalAnswer := some answer.typedExpr .. ϕ }
|
||||
| Waiter.consumerNode cNode => modify $ λ ϕ => { resumeQueue := ϕ.resumeQueue.enqueue (cNode, answer), .. ϕ }
|
||||
|
||||
def newAnswer (anormSubgoal : Expr) (answer : Answer) : TCMethod Unit :=
|
||||
do lookupStatus ← get >>= λ ϕ => pure $ ϕ.tableEntries.find anormSubgoal;
|
||||
match lookupStatus with
|
||||
| none => throw $ "[newAnswer]: " ++ toString anormSubgoal ++ " not found in table!"
|
||||
| some entry => do
|
||||
if entry.answers.any (λ answer₁ => Context.αNorm (answer₁.typedExpr.type) == Context.αNorm (answer.typedExpr.type)) then pure ()
|
||||
else if entry.waiters.any Waiter.isRoot
|
||||
&& (Context.eHasTmpMVar answer.typedExpr.type || Context.eHasTmpMVar answer.typedExpr.val) then pure()
|
||||
else do
|
||||
let newEntry : TableEntry := { answers := entry.answers.push answer .. entry };
|
||||
modify $ λ ϕ => { tableEntries := ϕ.tableEntries.insert anormSubgoal newEntry .. ϕ };
|
||||
entry.waiters.forM (wakeUp answer)
|
||||
|
||||
def consume : TCMethod Unit :=
|
||||
do cNode ← get >>= λ ϕ => pure ϕ.consumerStack.peek!;
|
||||
modify $ λ ϕ => { consumerStack := ϕ.consumerStack.pop .. ϕ };
|
||||
match cNode.remainingSubgoals with
|
||||
| [] => do
|
||||
let answer : Answer := {
|
||||
ctx := cNode.ctx,
|
||||
typedExpr := {
|
||||
val := cNode.ctx.eInstantiate cNode.futureAnswer.val,
|
||||
type := cNode.ctx.eInstantiate cNode.futureAnswer.type
|
||||
}};
|
||||
newAnswer cNode.anormSubgoal answer
|
||||
|
||||
| mvar::rest => do
|
||||
let anormSubgoal : Expr := Context.αNorm (cNode.ctx.eInstantiate $ cNode.ctx.eInfer mvar);
|
||||
let waiter : Waiter := Waiter.consumerNode cNode;
|
||||
lookupStatus ← get >>= λ ϕ => pure $ ϕ.tableEntries.find anormSubgoal;
|
||||
match lookupStatus with
|
||||
| none => newSubgoal waiter cNode.ctx anormSubgoal mvar
|
||||
| some entry => modify $ λ ϕ => {
|
||||
resumeQueue := entry.answers.foldl (λ rq answer => rq.enqueue (cNode, answer)) ϕ.resumeQueue,
|
||||
tableEntries := ϕ.tableEntries.insert anormSubgoal { waiters := entry.waiters.push waiter, .. entry },
|
||||
.. ϕ }
|
||||
|
||||
def constNameToTypedExpr (ctx : Context) (instName : Name) : TCMethod (TypedExpr × Context) :=
|
||||
do lookupStatus ← get >>= λ ϕ => pure $ ϕ.env.find instName;
|
||||
match lookupStatus with
|
||||
| none => throw $ "instance " ++ toString instName ++ " not found in env"
|
||||
| some cInfo =>
|
||||
let ⟨uMetas, ctx⟩ : List Level × Context :=
|
||||
cInfo.lparams.foldl (λ ⟨uMetas, ctx⟩ _ =>
|
||||
let ⟨uMeta, ctx⟩ := Context.uNewMeta.run ctx;
|
||||
⟨uMeta::uMetas, ctx⟩)
|
||||
([], ctx);
|
||||
let instVal := mkConst instName uMetas;
|
||||
let instType := cInfo.instantiateTypeLevelParams uMetas;
|
||||
pure ⟨⟨instVal, instType⟩, ctx⟩
|
||||
|
||||
def generate : TCMethod Unit :=
|
||||
do gNode ← get >>= λ ϕ => pure ϕ.generatorStack.peek!;
|
||||
match gNode.remainingInstances with
|
||||
| [] => modify $ λ ϕ => { generatorStack := ϕ.generatorStack.pop, .. ϕ }
|
||||
| inst::insts => do
|
||||
⟨instTE, ctx⟩ ← match inst with
|
||||
| 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 (λ gNode => { remainingInstances := insts .. gNode }) .. ϕ };
|
||||
match result with
|
||||
| none => pure ()
|
||||
| some (ctx, newMVars) => newConsumerNode gNode.toNode ctx newMVars
|
||||
|
||||
def step : TCMethod Unit :=
|
||||
do ϕ ← get;
|
||||
if !ϕ.resumeQueue.isEmpty then resume
|
||||
else if !ϕ.consumerStack.isEmpty then consume
|
||||
else if !ϕ.generatorStack.isEmpty then generate
|
||||
else throw "FAILED TO SYNTHESIZE"
|
||||
|
||||
partial def synthCore (ctx₀ : Context) (goalType : Expr) : Nat → TCMethod TypedExpr
|
||||
| 0 => throw "[synthCore] out of fuel"
|
||||
| n+1 => do
|
||||
step;
|
||||
finalAnswer ← get >>= λ ϕ => pure ϕ.finalAnswer;
|
||||
match finalAnswer with
|
||||
| none => synthCore n
|
||||
| some ⟨answerVal, answerType⟩ => pure ⟨answerVal, answerType⟩
|
||||
|
||||
def collectUReplacements : List Level → Context → Array (Level × Level) → Array Level
|
||||
→ Context × Array (Level × Level) × Array Level
|
||||
| [], ctx, uReplacements, fLevels => (ctx, uReplacements, fLevels)
|
||||
|
||||
| l::ls, ctx, uReplacements, fLevels =>
|
||||
if l.hasMVar then
|
||||
let ⟨uMeta, ctx⟩ := Context.uNewMeta.run ctx;
|
||||
collectUReplacements ls ctx (uReplacements.push (uMeta,l)) (fLevels.push uMeta)
|
||||
else
|
||||
collectUReplacements ls ctx uReplacements (fLevels.push l)
|
||||
|
||||
def collectEReplacements (env : Environment) (lctx : LocalContext) (locals : Array Expr)
|
||||
: Expr → List Expr → Context → Array (Expr × Expr) → Array Expr
|
||||
→ Context × Array (Expr × Expr) × Array Expr
|
||||
| _, [], ctx, eReplacements, fArgs => (ctx, eReplacements, fArgs)
|
||||
|
||||
| Expr.forallE _ d b _, arg::args, ctx, eReplacements, fArgs =>
|
||||
if isOutParam d then
|
||||
let ⟨eMeta, ctx⟩ := (Context.eNewMeta $ lctx.mkForall locals d).run ctx;
|
||||
let fArg : Expr := mkAppN eMeta locals;
|
||||
collectEReplacements (b.instantiate1 fArg) args ctx (eReplacements.push (eMeta, arg)) (fArgs.push fArg)
|
||||
else
|
||||
collectEReplacements (b.instantiate1 arg) args ctx eReplacements (fArgs.push arg)
|
||||
|
||||
| _, arg::args, _, _, _ => panic! "TODO(dselsam): this case not yet handled"
|
||||
|
||||
def preprocessForOutParams (env : Environment) (goalType : Expr) : Context × Expr × Array (Level × Level) × Array (Expr × Expr) :=
|
||||
if !goalType.hasMVar && goalType.getAppFn.isConst && !hasOutParams env goalType.getAppFn.constName!
|
||||
then ({}, goalType, #[], #[])
|
||||
else
|
||||
let ⟨lctx, bodyGoalType, locals⟩ := introduceLocals 0 {} #[] goalType;
|
||||
let f := goalType.getAppFn;
|
||||
let fArgs := goalType.getAppArgs;
|
||||
if !(f.isConst && isClass env f.constName!)
|
||||
then ({}, goalType, #[], #[])
|
||||
else
|
||||
let ⟨ctx, uReplacements, CLevels⟩ := collectUReplacements f.constLevels! {} #[] #[];
|
||||
let f := if uReplacements.isEmpty then f else mkConst f.constName! CLevels.toList;
|
||||
let fType :=
|
||||
match env.find f.constName! with
|
||||
| none => panic! "found constant not in the environment"
|
||||
| some cInfo => cInfo.instantiateTypeLevelParams CLevels.toList;
|
||||
let (ctx, eReplacements, fArgs) := collectEReplacements env lctx locals fType fArgs.toList ctx #[] #[]; -- TODO: avoid fArgs.toList
|
||||
(ctx, lctx.mkForall locals $ mkAppN f fArgs, uReplacements, eReplacements)
|
||||
|
||||
def synth (goalType₀ : Expr) (fuel : Nat := 100000) : TCMethod Expr :=
|
||||
do env ← get >>= λ ϕ => pure ϕ.env;
|
||||
let ⟨ctx₀, goalType, uReplacements, eReplacements⟩ := preprocessForOutParams env goalType₀;
|
||||
let ⟨mvar, ctx⟩ := (Context.eNewMeta goalType).run ctx₀;
|
||||
let anormSubgoal : Expr := Context.αNorm goalType;
|
||||
newSubgoal Waiter.root ctx anormSubgoal mvar;
|
||||
modify $ λ ϕ => { mainMVar := mvar .. ϕ };
|
||||
⟨instVal, instType⟩ ← synthCore ctx₀ goalType fuel;
|
||||
match (Context.eUnify goalType₀ instType).run ctx with
|
||||
| EStateM.Result.error msg _ => throw $ "outParams do not match: " ++ toString goalType₀ ++ " ≠ " ++ toString instType
|
||||
| EStateM.Result.ok _ ctx => do
|
||||
let instVal : Expr := ctx.eInstantiate instVal;
|
||||
when (Context.eHasTmpMVar instVal) $ throw "synthesized instance has mvar";
|
||||
pure instVal
|
||||
|
||||
end TypeClass
|
||||
end Lean
|
||||
Loading…
Add table
Reference in a new issue