From 1336f04b07cb29286fd1776b6b7e3564454c71dc Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 9 Aug 2024 13:03:55 +0200 Subject: [PATCH] chore: compatibility shims for HashMap, plus wider overall compat (#39) --- .github/workflows/ci.yml | 5 +- Extract.lean | 3 +- Tests.lean | 4 +- src/compat/SubVerso/Compat.lean | 63 +++++++++++++++++-- src/examples/SubVerso/Examples/Slice.lean | 9 ++- .../SubVerso/Highlighting/Code.lean | 8 ++- 6 files changed, 76 insertions(+), 16 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c30aa0c..eda612f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -9,6 +9,9 @@ jobs: strategy: matrix: toolchain: + - "4.0.0" + - "4.1.0" + - "4.2.0" - "4.3.0" - "4.4.0" - "4.5.0" @@ -18,7 +21,7 @@ jobs: - "4.9.0" - "4.10.0" - "4.11.0-rc1" - - "nightly-2024-08-08" + - "nightly-2024-08-09" platform: - os: ubuntu-latest installer: | diff --git a/Extract.lean b/Extract.lean index 86d8c91..ec0eb75 100644 --- a/Extract.lean +++ b/Extract.lean @@ -3,6 +3,7 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +import SubVerso.Compat import SubVerso.Examples.Env open Lean @@ -13,7 +14,7 @@ def main : (args : List String) → IO UInt32 try initSearchPath (← findSysroot) let modName := mod.toName - let env ← importModules #[{module := modName, runtimeOnly := false}] {} + let env ← SubVerso.Compat.importModules #[{module := modName, runtimeOnly := false}] {} let modExamples := highlighted.getState env let useful := relevant modName modExamples let exJson := Json.mkObj useful diff --git a/Tests.lean b/Tests.lean index 549306d..cfd73d4 100644 --- a/Tests.lean +++ b/Tests.lean @@ -14,7 +14,7 @@ open Lean Elab Command open SubVerso.Examples.Slice elab "#test_slicing" s:str out:ident c:command : command => do - let {original, residual, sliced} ← sliceSyntax c + let {original := _, residual, sliced} ← sliceSyntax c let mut log := "" @@ -24,7 +24,7 @@ elab "#test_slicing" s:str out:ident c:command : command => do log := log ++ s!"Slice {s}:\n{Syntax.prettyPrint stx}" let use := s.getString - if let some stx := sliced.find? use then + if let some stx := sliced[use]? then elabCommand stx else logInfo m!"Slice '{use}' not found" diff --git a/src/compat/SubVerso/Compat.lean b/src/compat/SubVerso/Compat.lean index b04a960..14aa90c 100644 --- a/src/compat/SubVerso/Compat.lean +++ b/src/compat/SubVerso/Compat.lean @@ -29,16 +29,28 @@ def realizeNameNoOverloads elab "%first_succeeding" "[" es:term,* "]" : term <= ty => do + let mut errs := #[] for e in es.getElems do try let expr ← withReader ({· with errToSorry := false}) <| - elabTerm e (some ty) - return expr - catch _ => + elabTermEnsuringType e (some ty) + let ty' ← Meta.inferType expr + if ← Meta.isDefEq ty ty' then + return expr + catch err => + errs := errs.push (e, err) continue - throwError "No alternative succeeded" + let msgErrs := errs.toList.map fun (tm, msg) => m!"{tm}: {indentD msg.toMessageData}" + throwError m!"No alternative succeeded. Attempts were: " ++ + indentD (MessageData.joinSep msgErrs Format.line) + +open Command in +elab "%if_bound" x:ident cmd:command : command => do + if (← getEnv).contains x.getId then elabCommand cmd +def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := + Lean.importModules (%first_succeeding [imports, imports.toList]) opts (trustLevel := trustLevel) def mkRefIdentFVar [Monad m] [MonadEnv m] (id : FVarId) : m Lean.Lsp.RefIdent := do pure %first_succeeding [ @@ -60,3 +72,46 @@ def refIdentCase (ri : Lsp.RefIdent) abbrev Parsec (α : Type) : Type := %first_succeeding [(Lean.Parsec α : Type), (Lean.Parsec String.Iterator α : Type)] + +def HashMap := %first_succeeding [Std.HashMap, Lean.HashMap] +def HashSet := %first_succeeding [Std.HashSet, Lean.HashSet] + +namespace HashMap + +instance [BEq α] [Hashable α] : Membership α (HashMap α β) := + %first_succeeding [ + inferInstanceAs (Membership α (Std.HashMap α β)), + ⟨fun k hm => hm.contains k⟩ + ] + +instance [BEq α] [Hashable α] {x : α} {hm : HashMap α β} : Decidable (x ∈ hm) := + %first_succeeding [ + inferInstanceAs (Decidable (x ∈ (hm : Std.HashMap α β))), + inferInstanceAs (Decidable (hm.contains x = true)) + ] + +instance instGetElemHashMap [BEq α] [Hashable α] [Inhabited β] : GetElem (HashMap α β) α β (fun m a => a ∈ m) := + %first_succeeding [ + inferInstanceAs (GetElem (Std.HashMap α β) α β (fun m a => a ∈ m)), + ⟨fun m a _ok => m.find! a⟩, + ⟨fun m a _ok => m.find! a, fun m a => Lean.HashMap.find? m a, fun m a => Lean.HashMap.find! m a⟩ + ] + +def get? {_ : BEq α} {_ : Hashable α} : HashMap α β → α → Option β := + %first_defined [Std.HashMap.get?, Lean.HashMap.find?] + +def get! {_ : BEq α} {_ : Hashable α} [Inhabited β] : HashMap α β → α → β := + %first_defined [Std.HashMap.get!, Lean.HashMap.find!] + +def getD {_ : BEq α} {_ : Hashable α} [Inhabited β] : HashMap α β → α → β → β := + %first_defined [Std.HashMap.getD, Lean.HashMap.findD] + + +%if_bound GetElem? + instance [BEq α] [Hashable α] [Inhabited β] : GetElem? (HashMap α β) α β (fun m a => a ∈ m) := + %first_succeeding [ + inferInstanceAs (GetElem? (Std.HashMap α β) α β (fun m a => a ∈ m)), + @GetElem?.mk _ _ _ _ instGetElemHashMap (fun m a => m.get? a) (fun m a => m.get! a) + ] + +instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) := ⟨%first_succeeding [Std.HashMap.empty, Lean.HashMap.empty]⟩ diff --git a/src/examples/SubVerso/Examples/Slice.lean b/src/examples/SubVerso/Examples/Slice.lean index 43e4d6a..4cbd96d 100644 --- a/src/examples/SubVerso/Examples/Slice.lean +++ b/src/examples/SubVerso/Examples/Slice.lean @@ -11,8 +11,8 @@ import SubVerso.Compat import SubVerso.Examples.Slice.Attribute -open Lean hiding Parsec -open SubVerso.Compat (Parsec) +open Lean hiding Parsec HashMap +open SubVerso.Compat (Parsec HashMap) namespace SubVerso.Examples.Slice @@ -160,7 +160,6 @@ private partial def removeRanges (env : Environment) (rngs : Array String.Range) pure <| .node info kind newSubs else pure stx - private def getSlices (slices : Array SliceCommand) : Except String (HashMap String (Array String.Range)) := do let mut opened : HashMap String (String.Pos) := {} let mut closed : HashMap String (Array String.Range) := {} @@ -170,8 +169,8 @@ private def getSlices (slices : Array SliceCommand) : Except String (HashMap Str if opened.contains name then .error s!"Slice '{name}' opened twice" else opened := opened.insert name rng.stop | .endRange name pos => - if let some p := opened.find? name then - closed := closed.insert name <| closed.findD name #[] |>.push ⟨p, pos.start⟩ + if let some p := opened[name]? then + closed := closed.insert name <| closed.getD name #[] |>.push ⟨p, pos.start⟩ opened := opened.erase name else .error s!"Slice '{name}' not open" pure closed diff --git a/src/highlighting/SubVerso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean index c2a7007..f1bf05e 100644 --- a/src/highlighting/SubVerso/Highlighting/Code.lean +++ b/src/highlighting/SubVerso/Highlighting/Code.lean @@ -10,10 +10,12 @@ import Lean.Widget.TaggedText import SubVerso.Compat import SubVerso.Highlighting.Highlighted -open Lean Elab +open Lean hiding HashMap +open Elab open Lean.Widget (TaggedText) open Lean.Widget open Lean.PrettyPrinter (InfoPerPos) +open SubVerso.Compat (HashMap) initialize registerTraceClass `SubVerso.Highlighting.Code @@ -73,7 +75,7 @@ structure State (α : Type u) where def State.init [BEq α] [Hashable α] : State α := {} def insert [Monad m] [MonadState (State α) m] [BEq α] [Hashable α] (x : α) : m Nat := do - if let some i := (← get).indices.find? x then + if let some i := (← get).indices[x]? then pure i else let i := (← get).contents.size @@ -139,7 +141,7 @@ def exprKind [Monad m] [MonadLiftT IO m] [MonadMCtx m] [MonadEnv m] match ← instantiateMVars expr with | Expr.fvar id => let seen ← - if let some y := ids.find? (← Compat.mkRefIdentFVar id) then + if let some y := ids[(← Compat.mkRefIdentFVar id)]? then Compat.refIdentCase y (onFVar := fun x => do let ty ← instantiateMVars (← runMeta <| Meta.inferType expr)