Interval Set

IntervalSet operations like IntervalSet.canonicalize or IntervalSet.intersection

def IntervalSet.Acc.with_none (acc : Interval.Acc) (n : NonemptyInterval Char) (h : acc.next.isNone = true) : Interval.Acc

Equations

• IntervalSet.Acc.with_none acc n h = { next := some n, set := acc.set, nonOverlapping := ⋯ }

def IntervalSet.Acc.with_next (acc : Interval.Acc) (n : NonemptyInterval Char) (h1 : Interval.is_start_eq acc.next n) : Interval.Acc

Equations

• IntervalSet.Acc.with_next acc n h1 = { next := some n, set := acc.set, nonOverlapping := ⋯ }

def IntervalSet.Acc.with_next_set (acc : Interval.Acc) (l : NonemptyInterval Char) (r : NonemptyInterval Char) (h1 : Interval.nonOverlapping l r) (h2 : acc.next = some l) : Interval.Acc

Equations

• One or more equations did not get rendered due to their size.

instance IntervalSet.instInhabitedAcc : Inhabited Interval.Acc

Equations

• IntervalSet.instInhabitedAcc = { default := { next := none, set := default, nonOverlapping := IntervalSet.instInhabitedAcc.proof_1 } }

def IntervalSet.canonicalize (ranges : Array (NonemptyInterval Char)) : IntervalSet Char

Converts ranges into IntervalSet with canonical ordering.

Equations

• One or more equations did not get rendered due to their size.

def IntervalSet.negate (interval : IntervalSet Char) : IntervalSet Char

Negate a interval set wrt the corresponding BoundedOrder instBoundedOrderCharInstLEChar .

Equations

• One or more equations did not get rendered due to their size.

def IntervalSet.intersection (interval1 : IntervalSet Char) (interval2 : IntervalSet Char) : IntervalSet Char

Intersection of interval sets

Equations

• interval1.intersection interval2 = let ranges := IntervalSet.intersection.loop 0 0 interval1.intervals interval2.intervals #[]; IntervalSet.canonicalize ranges

@[irreducible]

def IntervalSet.intersection.loop (a : Nat) (b : Nat) (ra : Array (NonemptyInterval Char)) (rb : Array (NonemptyInterval Char)) (acc : Array (NonemptyInterval Char)) : Array (NonemptyInterval Char)

Equations

• One or more equations did not get rendered due to their size.

def IntervalSet.difference (interval1 : IntervalSet Char) (interval2 : IntervalSet Char) : IntervalSet Char

Subtract the interval set interval2 from interval1.

Equations

• interval1.difference interval2 = interval1.intersection interval2.negate

def IntervalSet.union (interval1 : IntervalSet Char) (interval2 : IntervalSet Char) : IntervalSet Char

Union of interval sets.

Equations

• One or more equations did not get rendered due to their size.

def IntervalSet.symmetric_difference (interval1 : IntervalSet Char) (interval2 : IntervalSet Char) : IntervalSet Char

Compute the symmetric difference (A⊖B = (A∪B)(A∩B)) of the two sets.

Equations

• interval1.symmetric_difference interval2 = let intervalI := interval1.intersection interval2; let intervalU := interval1.union interval2; intervalU.difference intervalI