From 7f481b2159e489a90f721d3d18d6edebfa8d17df Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 8 Aug 2024 21:56:30 +1000 Subject: [PATCH 1/3] fixes --- Qq/AssertInstancesCommute.lean | 2 +- Qq/Delab.lean | 2 +- Qq/Macro.lean | 20 ++++++++++---------- lean-toolchain | 2 +- 4 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Qq/AssertInstancesCommute.lean b/Qq/AssertInstancesCommute.lean index a9b2ad8..b609849 100644 --- a/Qq/AssertInstancesCommute.lean +++ b/Qq/AssertInstancesCommute.lean @@ -17,7 +17,7 @@ def isRedundantLocalInst? (inst : FVarId) : MetaM (Option Expr) := do def findRedundantLocalInst? : QuoteM (Option (FVarId × Expr)) := do for {fvar, ..} in ← withUnquotedLCtx getLocalInstances do - if let some (.quoted (.fvar quotedFVar)) := (← read).exprBackSubst.find? fvar then + if let some (.quoted (.fvar quotedFVar)) := (← read).exprBackSubst[fvar]? then if (← quotedFVar.getDecl).hasValue then continue if let some result ← withUnquotedLCtx do isRedundantLocalInst? fvar.fvarId! then return (fvar.fvarId!, result) diff --git a/Qq/Delab.lean b/Qq/Delab.lean index 96e9c74..565abf0 100644 --- a/Qq/Delab.lean +++ b/Qq/Delab.lean @@ -51,7 +51,7 @@ def withDelabQuoted (k : StateT UnquoteState DelabM Term) : Delab := let showNested := `pp.qq._nested if (← getOptions).get showNested true then for fv in (← get).abstractedFVars.reverse do - if let some (.quoted expr) := (← get).exprBackSubst.find? (.fvar fv) then + if let some (.quoted expr) := (← get).exprBackSubst[Expr.fvar fv]? then if let some decl := (← get).unquoted.find? fv then if (res.1.find? (·.getId == decl.userName)).isSome then if let some name := removeDollar decl.userName then diff --git a/Qq/Macro.lean b/Qq/Macro.lean index 070502a..cf33967 100644 --- a/Qq/Macro.lean +++ b/Qq/Macro.lean @@ -32,19 +32,19 @@ structure UnquoteState where mvars : List (Expr × MVarSynth) := [] /-- Maps quoted expressions (of type Level) in the old context to level parameter names in the new context -/ - levelSubst : HashMap Expr Level := {} + levelSubst : Std.HashMap Expr Level := {} /-- Maps quoted expressions (of type Expr) in the old context to expressions in the new context -/ - exprSubst : HashMap Expr Expr := {} + exprSubst : Std.HashMap Expr Expr := {} /-- New unquoted local context -/ unquoted := LocalContext.empty /-- Maps free variables in the new context to expressions in the old context (of type Expr) -/ - exprBackSubst : HashMap Expr ExprBackSubstResult := {} + exprBackSubst : Std.HashMap Expr ExprBackSubstResult := {} /-- Maps free variables in the new context to levels in the old context (of type Level) -/ - levelBackSubst : HashMap Level Expr := {} + levelBackSubst : Std.HashMap Level Expr := {} /-- New free variables in the new context that were newly introduced for irreducible expressions. -/ abstractedFVars : Array FVarId := #[] @@ -133,7 +133,7 @@ mutual partial def unquoteLevel (e : Expr) : UnquoteM Level := do let e ← whnf e - if let some l := (← get).levelSubst.find? e then + if let some l := (← get).levelSubst[e]? then return l if e.isAppOfArity ``Level.zero 0 then pure .zero else if e.isAppOfArity ``Level.succ 1 then return .succ (← unquoteLevel (e.getArg! 0)) @@ -236,7 +236,7 @@ partial def unquoteExpr (e : Expr) : UnquoteM Expr := do let e ← instantiateMVars (← whnf e) let eTy ← whnfR (← inferType e) if eTy.isAppOfArity ``Quoted 1 then - if let some e' := (← get).exprSubst.find? e then + if let some e' := (← get).exprSubst[e]? then return e' if ← isAssignablePattern e then return ← unquoteExprMVar e @@ -359,13 +359,13 @@ def quoteLevel : Level → QuoteM Expr | .zero => return .const ``Level.zero [] | .succ u => return mkApp (.const ``Level.succ []) (← quoteLevel u) | l@(.mvar ..) => do - if let some e := (← read).levelBackSubst.find? l then + if let some e := (← read).levelBackSubst[l]? then return e throwError "cannot quote level mvar {l}" | .max a b => return mkApp2 (.const ``Level.max []) (← quoteLevel a) (← quoteLevel b) | .imax a b => return mkApp2 (.const ``Level.imax []) (← quoteLevel a) (← quoteLevel b) | l@(.param n) => do - match (← read).levelBackSubst.find? l with + match (← read).levelBackSubst[l]? with | some e => return e | none => match ← isLevelFVar n with @@ -382,12 +382,12 @@ def quoteLevelList : List Level → QuoteM Expr partial def quoteExpr : Expr → QuoteM Expr | .bvar i => return mkApp (.const ``Expr.bvar []) (toExpr i) | e@(.fvar ..) => do - let some r := (← read).exprBackSubst.find? e | throwError "unknown free variable {e}" + let some r := (← read).exprBackSubst[e]? | throwError "unknown free variable {e}" match r with | .quoted r => return r | .unquoted r => quoteExpr r | e@(.mvar ..) => do - if let some (.quoted r) := (← read).exprBackSubst.find? e then return r + if let some (.quoted r) := (← read).exprBackSubst[e]? then return r throwError "resulting term contains metavariable {e}" | .sort u => return mkApp (.const ``Expr.sort []) (← quoteLevel u) | .const n ls => return mkApp2 (.const ``Expr.const []) (toExpr n) (← quoteLevelList ls) diff --git a/lean-toolchain b/lean-toolchain index 0ba3faf..9f6eaf7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.9.0-rc1 +leanprover/lean4:nightly-2024-08-08 From 6e87b74d74c99137adcfc6f7d47d77b65b1eb927 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 23 Sep 2024 14:09:21 +0200 Subject: [PATCH 2/3] chore: account for UInt refactoring --- Qq/ForLean/ReduceEval.lean | 11 ++++++++++- lean-toolchain | 2 +- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/Qq/ForLean/ReduceEval.lean b/Qq/ForLean/ReduceEval.lean index a3f664e..8191dec 100644 --- a/Qq/ForLean/ReduceEval.lean +++ b/Qq/ForLean/ReduceEval.lean @@ -25,11 +25,20 @@ instance : ReduceEval (Fin (n+1)) where else throwFailedToEval e +instance {n : Nat} : ReduceEval (BitVec n) where + reduceEval := fun e => do + let e ← whnf e + if e.isAppOfArity ``BitVec.ofFin 2 then + have : 2^n - 1 + 1 = 2^n := Nat.sub_one_add_one_eq_of_pos (Nat.two_pow_pos n) + let _ : ReduceEval (Fin (2^n)) := this ▸ (inferInstanceAs <| ReduceEval (Fin (2^n - 1 + 1))) + pure ⟨(← reduceEval (e.getArg! 1))⟩ + else + throwFailedToEval e + instance : ReduceEval UInt64 where reduceEval := fun e => do let e ← whnf e if e.isAppOfArity ``UInt64.mk 1 then - let _ : ReduceEval (Fin UInt64.size) := inferInstanceAs <| ReduceEval (Fin (_ + 1)) pure ⟨(← reduceEval (e.getArg! 0))⟩ else throwFailedToEval e diff --git a/lean-toolchain b/lean-toolchain index 98556ba..ba3ea96 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.12.0-rc1 +leanprover/lean4-pr-releases:pr-release-5323 From c20ed8dc330ac0122779b1cc31b1a30c8d4f22b6 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 18 Oct 2024 15:37:39 +0000 Subject: [PATCH 3/3] simplify --- Qq/ForLean/ReduceEval.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Qq/ForLean/ReduceEval.lean b/Qq/ForLean/ReduceEval.lean index da46458..477fbb3 100644 --- a/Qq/ForLean/ReduceEval.lean +++ b/Qq/ForLean/ReduceEval.lean @@ -29,8 +29,6 @@ instance {n : Nat} : ReduceEval (BitVec n) where reduceEval := fun e => do let e ← whnf e if e.isAppOfArity ``BitVec.ofFin 2 then - have : 2^n - 1 + 1 = 2^n := Nat.sub_one_add_one_eq_of_pos (Nat.two_pow_pos n) - let _ : ReduceEval (Fin (2^n)) := this ▸ (inferInstanceAs <| ReduceEval (Fin (2^n - 1 + 1))) pure ⟨(← reduceEval (e.getArg! 1))⟩ else throwFailedToEval e