From 4ce457eb511eca812e5ff9dc939eb1a645d947dd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Dec 2019 14:57:29 -0800 Subject: [PATCH] chore: remove prototype for the new type class resolution The code has been integrated into the `Meta` module. --- src/Init/Lean.lean | 1 - src/Init/Lean/TypeClass.lean | 7 - src/Init/Lean/TypeClass/Basic.lean | 21 -- src/Init/Lean/TypeClass/Context.lean | 351 --------------------------- src/Init/Lean/TypeClass/Synth.lean | 326 ------------------------- 5 files changed, 706 deletions(-) delete mode 100644 src/Init/Lean/TypeClass.lean delete mode 100644 src/Init/Lean/TypeClass/Basic.lean delete mode 100644 src/Init/Lean/TypeClass/Context.lean delete mode 100644 src/Init/Lean/TypeClass/Synth.lean diff --git a/src/Init/Lean.lean b/src/Init/Lean.lean index dff3747ac2..80e1e09bbd 100644 --- a/src/Init/Lean.lean +++ b/src/Init/Lean.lean @@ -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 diff --git a/src/Init/Lean/TypeClass.lean b/src/Init/Lean/TypeClass.lean deleted file mode 100644 index 5173fe1068..0000000000 --- a/src/Init/Lean/TypeClass.lean +++ /dev/null @@ -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 diff --git a/src/Init/Lean/TypeClass/Basic.lean b/src/Init/Lean/TypeClass/Basic.lean deleted file mode 100644 index 4586e87754..0000000000 --- a/src/Init/Lean/TypeClass/Basic.lean +++ /dev/null @@ -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 diff --git a/src/Init/Lean/TypeClass/Context.lean b/src/Init/Lean/TypeClass/Context.lean deleted file mode 100644 index b9a0b6177d..0000000000 --- a/src/Init/Lean/TypeClass/Context.lean +++ /dev/null @@ -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 diff --git a/src/Init/Lean/TypeClass/Synth.lean b/src/Init/Lean/TypeClass/Synth.lean deleted file mode 100644 index 0c5afd35cd..0000000000 --- a/src/Init/Lean/TypeClass/Synth.lean +++ /dev/null @@ -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 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