chore: move to new frontend
This commit is contained in:
Leonardo de Moura
parent
3e9c5e1653
commit
4d64edfff3
1 changed files with 34 additions and 33 deletions
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -13,40 +14,41 @@ namespace ReplaceImpl
|
|||
abbrev cacheSize : USize := 8192
|
||||
|
||||
structure State :=
|
||||
(keys : Array Expr) -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr
|
||||
(results : Array Expr)
|
||||
(keys : Array Expr) -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr
|
||||
(results : Array Expr)
|
||||
|
||||
abbrev ReplaceM := StateM State
|
||||
|
||||
@[inline] unsafe def cache (i : USize) (key : Expr) (result : Expr) : ReplaceM Expr := do
|
||||
modify $ fun s => { keys := s.keys.uset i key lcProof, results := s.results.uset i result lcProof };
|
||||
pure result
|
||||
modify fun s => { keys := s.keys.uset i key lcProof, results := s.results.uset i result lcProof };
|
||||
pure result
|
||||
|
||||
@[specialize] unsafe def replaceUnsafeM (f? : Expr → Option Expr) (size : USize) : Expr → ReplaceM Expr
|
||||
| e => do
|
||||
c ← get;
|
||||
let h := ptrAddrUnsafe e;
|
||||
let i := h % size;
|
||||
if ptrAddrUnsafe (c.keys.uget i lcProof) == h then
|
||||
pure $ c.results.uget i lcProof
|
||||
else match f? e with
|
||||
| some eNew => cache i e eNew
|
||||
| none => match e with
|
||||
| Expr.forallE _ d b _ => do d ← replaceUnsafeM d; b ← replaceUnsafeM b; cache i e $ e.updateForallE! d b
|
||||
| Expr.lam _ d b _ => do d ← replaceUnsafeM d; b ← replaceUnsafeM b; cache i e $ e.updateLambdaE! d b
|
||||
| Expr.mdata _ b _ => do b ← replaceUnsafeM b; cache i e $ e.updateMData! b
|
||||
| Expr.letE _ t v b _ => do t ← replaceUnsafeM t; v ← replaceUnsafeM v; b ← replaceUnsafeM b; cache i e $ e.updateLet! t v b
|
||||
| Expr.app f a _ => do f ← replaceUnsafeM f; a ← replaceUnsafeM a; cache i e $ e.updateApp! f a
|
||||
| Expr.proj _ _ b _ => do b ← replaceUnsafeM b; cache i e $ e.updateProj! b
|
||||
| Expr.localE _ _ _ _ => unreachable!
|
||||
| e => pure e
|
||||
@[specialize] unsafe def replaceUnsafeM (f? : Expr → Option Expr) (size : USize) (e : Expr) : ReplaceM Expr := do
|
||||
let rec visit (e : Expr) := do
|
||||
let c ← get
|
||||
let h := ptrAddrUnsafe e
|
||||
let i := h % size
|
||||
if ptrAddrUnsafe (c.keys.uget i lcProof) == h then
|
||||
pure $ c.results.uget i lcProof
|
||||
else match f? e with
|
||||
| some eNew => cache i e eNew
|
||||
| none => match e with
|
||||
| Expr.forallE _ d b _ => cache i e $ e.updateForallE! (← visit d) (← visit b)
|
||||
| Expr.lam _ d b _ => cache i e $ e.updateLambdaE! (← visit d) (← visit b)
|
||||
| Expr.mdata _ b _ => cache i e $ e.updateMData! (← visit b)
|
||||
| Expr.letE _ t v b _ => cache i e $ e.updateLet! (← visit t) (← visit v) (← visit b)
|
||||
| Expr.app f a _ => cache i e $ e.updateApp! (← visit f) (← visit a)
|
||||
| Expr.proj _ _ b _ => cache i e $ e.updateProj! (← visit b)
|
||||
| Expr.localE _ _ _ _ => unreachable!
|
||||
| e => pure e
|
||||
visit e
|
||||
|
||||
unsafe def initCache : State :=
|
||||
{ keys := mkArray cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr`
|
||||
results := mkArray cacheSize.toNat (arbitrary _) }
|
||||
{ keys := mkArray cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr`
|
||||
results := mkArray cacheSize.toNat (arbitrary _) }
|
||||
|
||||
@[inline] unsafe def replaceUnsafe (f? : Expr → Option Expr) (e : Expr) : Expr :=
|
||||
(replaceUnsafeM f? cacheSize e).run' initCache
|
||||
(replaceUnsafeM f? cacheSize e).run' initCache
|
||||
|
||||
end ReplaceImpl
|
||||
|
||||
|
|
@ -54,18 +56,17 @@ end ReplaceImpl
|
|||
We also need an invariant at `State` and proofs for the `uget` operations. -/
|
||||
|
||||
@[implementedBy ReplaceImpl.replaceUnsafe]
|
||||
partial def replace (f? : Expr → Option Expr) : Expr → Expr
|
||||
| e =>
|
||||
partial def replace (f? : Expr → Option Expr) (e : Expr) : Expr :=
|
||||
/- This is a reference implementation for the unsafe one above -/
|
||||
match f? e with
|
||||
| some eNew => eNew
|
||||
| none => match e with
|
||||
| Expr.forallE _ d b _ => let d := replace d; let b := replace b; e.updateForallE! d b
|
||||
| Expr.lam _ d b _ => let d := replace d; let b := replace b; e.updateLambdaE! d b
|
||||
| Expr.mdata _ b _ => let b := replace b; e.updateMData! b
|
||||
| Expr.letE _ t v b _ => let t := replace t; let v := replace v; let b := replace b; e.updateLet! t v b
|
||||
| Expr.app f a _ => let f := replace f; let a := replace a; e.updateApp! f a
|
||||
| Expr.proj _ _ b _ => let b := replace b; e.updateProj! b
|
||||
| Expr.forallE _ d b _ => let d := replace f? d; let b := replace f? b; e.updateForallE! d b
|
||||
| Expr.lam _ d b _ => let d := replace f? d; let b := replace f? b; e.updateLambdaE! d b
|
||||
| Expr.mdata _ b _ => let b := replace f? b; e.updateMData! b
|
||||
| Expr.letE _ t v b _ => let t := replace f? t; let v := replace f? v; let b := replace f? b; e.updateLet! t v b
|
||||
| Expr.app f a _ => let f := replace f? f; let a := replace f? a; e.updateApp! f a
|
||||
| Expr.proj _ _ b _ => let b := replace f? b; e.updateProj! b
|
||||
| e => e
|
||||
end Expr
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue