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

chore: move to new frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-19 11:38:00 -07:00
parent a1828d5ef4
commit 7f5ef0c30b
1 changed files with 88 additions and 77 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

165
src/Lean/Meta/DiscrTree.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -7,9 +8,7 @@ import Lean.Meta.Basic
import Lean.Meta.FunInfo
import Lean.Meta.InferType
namespace Lean
namespace Meta
namespace DiscrTree
namespace Lean.Meta.DiscrTree
/-
(Imperfect) discrimination trees.
@ -63,7 +62,8 @@ def Key.lt : Key → Key → Bool
| Key.const n₁ a₁, Key.const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
| k₁, k₂ => k₁.ctorIdx < k₂.ctorIdx
instance Key.hasLess : HasLess Key := ⟨fun a b => Key.lt a b⟩
instance : HasLess Key := ⟨fun a b => Key.lt a b⟩
instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
def Key.format : Key → Format
| Key.star => "*"
@ -73,14 +73,14 @@ def Key.format : Key → Format
| Key.const k _ => fmt k
| Key.fvar k _ => fmt k
instance Key.hasFormat : HasFormat Key := ⟨Key.format⟩
instance : HasFormat Key := ⟨Key.format⟩
def Key.arity : Key → Nat
| Key.const _ a => a
| Key.fvar _ a => a
| _ => 0
instance Trie.inhabited {α} : Inhabited (Trie α) := ⟨Trie.node #[] #[]⟩
instance {α} : Inhabited (Trie α) := ⟨Trie.node #[] #[]⟩
def empty {α} : DiscrTree α := { root := {} }
@ -123,7 +123,7 @@ instance {α} : Inhabited (DiscrTree α) := ⟨{}⟩
-/
private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Bool :=
if h : i < infos.size then
let info := infos.get ⟨i, h⟩;
let info := infos.get ⟨i, h⟩
if info.instImplicit then
pure true
else if info.implicit then
@ -134,15 +134,16 @@ else
isProof a
private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Array Expr → MetaM (Array Expr)
| i, Expr.app f a _, todo =>
condM (ignoreArg a i infos)
(pushArgsAux (i-1) f (todo.push tmpStar))
(pushArgsAux (i-1) f (todo.push a))
| i, Expr.app f a _, todo => do
if (← ignoreArg a i infos) then
pushArgsAux infos (i-1) f (todo.push tmpStar)
else
pushArgsAux infos (i-1) f (todo.push a)
| _, _, todo => pure todo
private partial def whnfEta : Expr → MetaM Expr
| e => do
e ← whnf e;
let e ← whnf e
match e.etaExpandedStrict? with
| some e => whnfEta e
| none => pure e
@ -155,54 +156,56 @@ private def shouldAddAsStar (constName : Name) : Bool :=
constName == `Nat.zero || constName == `Nat.succ || constName == `Nat.add || constName == `HasAdd.add
private def pushArgs (todo : Array Expr) (e : Expr) : MetaM (Key × Array Expr) := do
e ← whnfEta e;
let fn := e.getAppFn;
let push (k : Key) (nargs : Nat) : MetaM (Key × Array Expr) := do {
info ← getFunInfoNArgs fn nargs;
todo ← pushArgsAux info.paramInfo (nargs-1) e todo;
let e ← whnfEta e
let fn := e.getAppFn
let push (k : Key) (nargs : Nat) : MetaM (Key × Array Expr) := do
let info ← getFunInfoNArgs fn nargs
let todo ← pushArgsAux info.paramInfo (nargs-1) e todo
pure (k, todo)
};
match fn with
| Expr.lit v _ => pure (Key.lit v, todo)
| Expr.const c _ _ =>
if shouldAddAsStar c then
pure (Key.star, todo)
else
let nargs := e.getAppNumArgs;
let nargs := e.getAppNumArgs
push (Key.const c nargs) nargs
| Expr.fvar fvarId _ => let nargs := e.getAppNumArgs; push (Key.fvar fvarId nargs) nargs
| Expr.fvar fvarId _ =>
let nargs := e.getAppNumArgs
push (Key.fvar fvarId nargs) nargs
| Expr.mvar mvarId _ =>
if mvarId == tmpMVarId then
-- We use `tmp to mark implicit arguments and proofs
pure (Key.star, todo)
else condM (isReadOnlyOrSyntheticOpaqueExprMVar mvarId)
(pure (Key.other, todo))
(pure (Key.star, todo))
| _ => pure (Key.other, todo)
else if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then
pure (Key.other, todo)
else
pure (Key.star, todo)
| _ => pure (Key.other, todo)
partial def mkPathAux : Array Expr → Array Key → MetaM (Array Key)
| todo, keys =>
| todo, keys => do
if todo.isEmpty then
pure keys
else do
let e := todo.back;
let todo := todo.pop;
(k, todo) ← pushArgs todo e;
else
let e := todo.back
let todo := todo.pop
let (k, todo) ← pushArgs todo e
mkPathAux todo (keys.push k)
private def initCapacity := 8
def mkPath (e : Expr) : MetaM (Array Key) :=
withReducible $ do
let todo : Array Expr := Array.mkEmpty initCapacity;
let keys : Array Key := Array.mkEmpty initCapacity;
withReducible do
let todo : Array Expr := Array.mkEmpty initCapacity
let keys : Array Key := Array.mkEmpty initCapacity
mkPathAux (todo.push e) keys
private partial def createNodes {α} (keys : Array Key) (v : α) : Nat → Trie α
| i =>
if h : i < keys.size then
let k := keys.get ⟨i, h⟩;
let c := createNodes (i+1);
let k := keys.get ⟨i, h⟩
let c := createNodes keys v (i+1)
Trie.node #[] #[(k, c)]
else
Trie.node #[v] #[]
@ -213,12 +216,12 @@ if vs.contains v then vs else vs.push v
private partial def insertAux {α} [HasBeq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
| i, Trie.node vs cs =>
if h : i < keys.size then
let k := keys.get ⟨i, h⟩;
let k := keys.get ⟨i, h⟩
let c := Id.run $ cs.binInsertM
(fun a b => a.1 < b.1)
(fun ⟨_, s⟩ => let c := insertAux (i+1) s; (k, c)) -- merge with existing
(fun ⟨_, s⟩ => let c := insertAux keys v (i+1) s; (k, c)) -- merge with existing
(fun _ => let c := createNodes keys v (i+1); (k, c))
(k, arbitrary _);
(k, arbitrary _)
Trie.node vs c
else
Trie.node (insertVal vs v) cs
@ -226,45 +229,50 @@ private partial def insertAux {α} [HasBeq α] (keys : Array Key) (v : α) : Nat
def insertCore {α} [HasBeq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α :=
if keys.isEmpty then panic! "invalid key sequence"
else
let k := keys.get! 0;
let k := keys[0]
match d.root.find? k with
| none =>
let c := createNodes keys v 1;
let c := createNodes keys v 1
{ root := d.root.insert k c }
| some c =>
let c := insertAux keys v 1 c;
let c := insertAux keys v 1 c
{ root := d.root.insert k c }
def insert {α} [HasBeq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := do
keys ← mkPath e;
let keys ← mkPath e
pure $ d.insertCore keys v
partial def Trie.format {α} [HasFormat α] : Trie α → Format
| Trie.node vs cs => Format.group $ Format.paren $
"node" ++ (if vs.isEmpty then Format.nil else " " ++ fmt vs)
++ Format.join (cs.toList.map $ fun ⟨k, c⟩ => Format.line ++ Format.paren (fmt k ++ " => " ++ Trie.format c))
++ Format.join (cs.toList.map $ fun ⟨k, c⟩ => Format.line ++ Format.paren (fmt k ++ " => " ++ format c))
instance Trie.hasFormat {α} [HasFormat α] : HasFormat (Trie α) := ⟨Trie.format⟩
partial def format {α} [HasFormat α] (d : DiscrTree α) : Format :=
let (_, r) := d.root.foldl
(fun (p : Bool × Format) k c =>
(false, p.2 ++ (if p.1 then Format.nil else Format.line) ++ Format.paren (fmt k ++ " => " ++ fmt c)))
(true, Format.nil);
(false, p.2 ++ (if p.1 == true then Format.nil else Format.line) ++ Format.paren (fmt k ++ " => " ++ fmt c))) -- TODO: fix p.1 == true
(true, Format.nil)
Format.group r
instance DiscrTree.hasFormat {α} [HasFormat α] : HasFormat (DiscrTree α) := ⟨format⟩
private def getKeyArgs (e : Expr) (isMatch? : Bool) : MetaM (Key × Array Expr) := do
e ← whnfEta e;
let e ← whnfEta e
match e.getAppFn with
| Expr.lit v _ => pure (Key.lit v, #[])
| Expr.const c _ _ => let nargs := e.getAppNumArgs; pure (Key.const c nargs, e.getAppRevArgs)
| Expr.fvar fvarId _ => let nargs := e.getAppNumArgs; pure (Key.fvar fvarId nargs, e.getAppRevArgs)
| Expr.const c _ _ =>
let nargs := e.getAppNumArgs
pure (Key.const c nargs, e.getAppRevArgs)
| Expr.fvar fvarId _ =>
let nargs := e.getAppNumArgs
pure (Key.fvar fvarId nargs, e.getAppRevArgs)
| Expr.mvar mvarId _ =>
if isMatch? then pure (Key.other, #[])
if isMatch? then
pure (Key.other, #[])
else do
ctx ← read;
let ctx ← read
if ctx.config.isDefEqStuckEx then
/-
When the configuration flag `isDefEqStuckEx` is set to true,
@ -281,11 +289,11 @@ match e.getAppFn with
This is incorrect because it is equivalent to saying that there is no solution even if
the caller assigns `?m` and try again. -/
pure (Key.star, #[])
else if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then
pure (Key.other, #[])
else
condM (isReadOnlyOrSyntheticOpaqueExprMVar mvarId)
(pure (Key.other, #[]))
(pure (Key.star, #[]))
| _ => pure (Key.other, #[])
pure (Key.star, #[])
| _ => pure (Key.other, #[])
private abbrev getMatchKeyArgs (e : Expr) : MetaM (Key × Array Expr) :=
getKeyArgs e true
@ -298,31 +306,34 @@ private partial def getMatchAux {α} : Array Expr → Trie α → Array α → M
if todo.isEmpty then pure $ result ++ vs
else if cs.isEmpty then pure result
else do
let e := todo.back;
let todo := todo.pop;
let first := cs.get! 0; /- Recall that `Key.star` is the minimal key -/
(k, args) ← getMatchKeyArgs e;
let e := todo.back
let todo := todo.pop
let first := cs[0] /- Recall that `Key.star` is the minimal key -/
let (k, args) ← getMatchKeyArgs e
/- We must always visit `Key.star` edges since they are wildcards.
Thus, `todo` is not used linearly when there is `Key.star` edge
and there is an edge for `k` and `k != Key.star`. -/
let visitStarChild (result : Array α) : MetaM (Array α) := if first.1 == Key.star then getMatchAux todo first.2 result else pure result;
let visitStarChild (result : Array α) : MetaM (Array α) :=
if first.1 == Key.star then getMatchAux todo first.2 result else pure result
match k with
| Key.star => visitStarChild result
| _ =>
match cs.binSearch (k, arbitrary _) (fun a b => a.1 < b.1) with
| none => visitStarChild result
| some c => do result ← visitStarChild result; getMatchAux (todo ++ args) c.2 result
| some c =>
let result ← visitStarChild result
getMatchAux (todo ++ args) c.2 result
private def getStarResult {α} (d : DiscrTree α) : Array α :=
let result : Array α := Array.mkEmpty initCapacity;
let result : Array α := Array.mkEmpty initCapacity
match d.root.find? Key.star with
| none => result
| some (Trie.node vs _) => result ++ vs
def getMatch {α} (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
withReducible $ do
let result := getStarResult d;
(k, args) ← getMatchKeyArgs e;
withReducible do
let result := getStarResult d
let (k, args) ← getMatchKeyArgs e
match k with
| Key.star => pure result
| _ =>
@ -334,34 +345,34 @@ private partial def getUnifyAux {α} : Nat → Array Expr → Trie α → (Array
| skip+1, todo, Trie.node vs cs, result =>
if cs.isEmpty then pure result
else cs.foldlM (fun result ⟨k, c⟩ => getUnifyAux (skip + k.arity) todo c result) result
| 0, todo, Trie.node vs cs, result =>
| 0, todo, Trie.node vs cs, result => do
if todo.isEmpty then pure (result ++ vs)
else if cs.isEmpty then pure result
else do
let e := todo.back;
let todo := todo.pop;
(k, args) ← getUnifyKeyArgs e;
else
let e := todo.back
let todo := todo.pop
let (k, args) ← getUnifyKeyArgs e
match k with
| Key.star => cs.foldlM (fun result ⟨k, c⟩ => getUnifyAux k.arity todo c result) result
| _ =>
let first := cs.get! 0;
let first := cs[0]
let visitStarChild (result : Array α) : MetaM (Array α) :=
if first.1 == Key.star then getUnifyAux 0 todo first.2 result else pure result;
if first.1 == Key.star then getUnifyAux 0 todo first.2 result else pure result
match cs.binSearch (k, arbitrary _) (fun a b => a.1 < b.1) with
| none => visitStarChild result
| some c => do result ← visitStarChild result; getUnifyAux 0 (todo ++ args) c.2 result
| some c =>
let result ← visitStarChild result
getUnifyAux 0 (todo ++ args) c.2 result
def getUnify {α} (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
withReducible $ do
(k, args) ← getUnifyKeyArgs e;
withReducible do
let (k, args) ← getUnifyKeyArgs e
match k with
| Key.star => d.root.foldlM (fun result k c => getUnifyAux k.arity #[] c result) #[]
| _ =>
let result := getStarResult d;
let result := getStarResult d
match d.root.find? k with
| none => pure result
| some c => getUnifyAux 0 args c result
end DiscrTree
end Meta
end Lean
end Lean.Meta.DiscrTree