Lean4
/-- Updates the state with the atom `x`. If `x` is `⊤` or `⊥`, adds the corresponding fact. If `x`
is `y ⊔ z`, adds a fact about it, then recursively calls `addAtom` on `y` and `z`.
Similarly for `⊓`. -/
partial def addAtom {u : Level} (type : Q(Type u)) (x : Q($type)) : CollectFactsM Nat := do
modify fun res => res.insertIfNew type (.empty, #[])
let (atomToIdx, facts) := (← get).get! type
match ← (← atomToIdx.getUnify x).findM? fun (_, e) => isDefEq x e with
| some (idx, _) =>
return idx
| none =>
let idx := atomToIdx.size
let atomToIdx ← atomToIdx.insert x (idx, x)
modify fun res => res.insert type (atomToIdx, facts)
match x with
| ~q((@OrderTop.toTop _ $instLE $instTop).top) =>
addFact type (.isTop idx)
| ~q((@OrderBot.toBot _ $instLE $instBot).bot) =>
addFact type (.isBot idx)
| ~q((@SemilatticeSup.toMax _ $inst).max $a $b) =>
let aIdx ← addAtom type a
let bIdx ← addAtom type b
addFact type (.isSup aIdx bIdx idx)
| ~q((@SemilatticeInf.toMin _ $inst).min $a $b) =>
let aIdx ← addAtom type a
let bIdx ← addAtom type b
addFact type (.isInf aIdx bIdx idx)
| _ =>
pure ()
return idx
