Use semilattice from mathlib

Changes

1 changed files (+5/-3)

• Mutable.lean
  • @@ -1,4 +1,5 @@
    import Std.Data + import Mathlib.Order.Lattice def TypeListToTuple : List Type → Type | [] => Unit
  • @@ -110,7 +111,7 @@ (hh : ∀ rel, Hashable <| TypeListToTuple <| relations rel) :=
    Std.DHashMap String fun rel ↦ Std.HashMap (TypeListToTuple <| relations rel) (relType rel) def naiveEval - (relJoin : (rel : String) → relType rel → relType rel → relType rel) + (relJoin : (rel : String) → SemilatticeInf <| relType rel) (rules : List (Rule relations vars relType)) (hb : ∀ rel, BEq <| TypeListToTuple <| relations rel) (hh : ∀ rel, Hashable <| TypeListToTuple <| relations rel)
  • @@ -140,7 +141,7 @@ if h : headRel ∈ cur then
    let tups := cur.get headRel h if ht : tup ∈ tups then let orig := tups.get tup ht - let joined := relJoin headRel fn orig + let joined := @SemilatticeInf.inf (relType headRel) _ fn orig if joined != orig then (true, nxt.modify headRel (·.insert tup fn)) else
  • @@ -187,7 +188,8 @@ def vars : String → Type := fun _ ↦ Nat
    def relType : String → Type := fun _ ↦ Nat - def relJoin : (rel : String) → relType rel → relType rel → relType rel := fun _ ↦ Nat.min + @[instance_reducible] + def relJoin : (rel : String) → SemilatticeInf (relType rel) := fun _ ↦ instDistribLatticeNat.toSemilatticeInf def pathRule : Rule relations vars relType := { headRel := "path"