From 4d64edfff3c8dfe189a3c657e331f956a7d04c94 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Oct 2020 08:51:11 -0700 Subject: [PATCH] chore: move to new frontend --- src/Lean/Util/ReplaceExpr.lean | 67 +++++++++++++++++----------------- 1 file changed, 34 insertions(+), 33 deletions(-) diff --git a/src/Lean/Util/ReplaceExpr.lean b/src/Lean/Util/ReplaceExpr.lean index 42bc6e1996..e42a581be2 100644 --- a/src/Lean/Util/ReplaceExpr.lean +++ b/src/Lean/Util/ReplaceExpr.lean @@ -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