
package dbmodel

/** Version 11.1
 *
 *  Synchrony iterators need canSee predicates. Some common predicates
 *  are provided below. In order to exploit Synchrony iterators, it is
 *  important to know whether a predicate is left-, right-, 
 *  bi-convex/bounded, and anti-monotonic, as well as how to decompose
 *  it into such components.
 *
 *  Organization of this module:
 *  // HasOrder (equal, lt, lteq, gt, gteq), 
 *  // HasSize (szpercent), 
 *  // HasDistance (intdist, dbldist, dl, dleq, dg, dgeq), 
 *  // LINETOPO (overlap, near, far, inside, enclose, touch).
 *  // DBNumeric, dInt, dInt2, dDbl
 *
 *  The predicates provided to be used with Synchrony iterators:
 *  // EQ, LT, LTEQ, GT, GTEQ, SZPERCENT, DL, DLEQ, DG, DGEQ,
 *  // OVERLAP, ENCLOSE, INSIDE, NEAR, FAR, TOUCH, NEIGHBOUR
 *
 *  For reference, here are the definitions of left-, right-,
 *  and bi-convexity/boundedness, and monotonicity and 
 *  anti-monotonicity:
 *
 *  Given list [[B]] of objects [[b1, b2, ..., bn]] sorted
 *  wrt an ordering [[<=B]] such that [[bi <=B bj]] if i < j.
 *  
 *  Given also list [[A]] of objects [[a1, a2, ..., am]] sorted
 *  wrt an ordering [[<=A]] such that [[ai <=A aj]] if i < j.
 *
 *  We omit the A-/B- annotation and simply write [[<=]] and [[<]]
 *  instead of [[<=A]], [[<A]], [[<=B]], and [[<B]].
 *  
 *  An "isBefore" predicate [[bf(b,a)]] is said to be MONOTONIC 
 *  wrt the lists [[(B,A)]] iff
 *     [[ai <= aj && bf(b,ai)]] implies [[bf(b,aj)]], and
 *     [[bi <= bj && bf(bj,a)]] implies [[bf(bi,a)]]
 *
 *  Quite often [[b]] and [[a]] are the same type [[T]] of objects.
 *  So, there is already an associated ordering (denoted as [[<T]],
 *  or [[ Ordering[T] ]] in Scala) on them. This is taken to be 
 *  the default "isBefore" pedicate.
 *
 *  A predicate [[anti(b,a)]] is said to be ANTI-MONOTONIC
 *  wrt [[bf]] (which is monotonic wrt [[(B,A)]]) iff
 *     [[ai <= aj && bf(b,ai) && !anti(b,ai)]] implies [[!anti(b,aj)]]
 *
 *  A "canSee" predicate [[csl(b,a)]] is said to be LEFT-CONVEX
 *  wrt [[bf]] (which is monotonic wrt [[(B,A)]]) iff
 *     for each [[a]] and [[b' <= b]],
 *        [[bf(b,a) && !csl(b,a)]] implies [[!csl(b',a)]]
 *
 *  Further, a left-convex [[csl(b,a)]] is said to be LEFT-BOUNDED
 *  wrt [[bf]] iff for each [[a]], there is a [[b]], such that
 *  [[bf(b,a) && !csl(b,a)]].
 *
 *  A "canSee" predicate [[csr(b,a)]] is said to be RIGHT-CONVEX
 *  wrt [[bf]] (which is monotonic wrt [[(B,A)]]) iff
 *     for each [[a]] and [[b <= b']],
 *        [[!bf(b,a) && !csr(b,a)]] implies [[!csr(b',a)]]
 *
 *  Further, a right-convex [[csr(b,a)]] is said to be RIGHT-BOUNDED
 *  wrt [[bf]] iff for each [[a]], there is a [[b]], such that
 *  [[!bf(b,a) && !csr(b,a)]].
 *
 *  A "canSee" predicate [[cs(b,a)]] is said to be BI-CONVEX
 *  wrt [[bf]] (which is monotonic wrt [[(B,A)]]) iff it is both
 *  left- and right-convex wrt [[bf]].
 *     
 *  A Synchrony iterator [[siterator(pred)]] on [[(B,A)]] enables
 *  an efficient synchronized iteration on [[(B,A)]] to compute
 *  a "join" conceptually equivalent to
 *     [[ for a <- A yield (a, B filter { b => pred(b, a) }) ]]
 *
 *  The efficiency is enabled by exploiting left-, right-, bi-
 *  convexity/boundedness, monotonicity and anti-monotonicity properties
 *  that [[pred(b,a)]] might enjoy wrt [[(B,A)]] and the associated
 *  orderings. In particular, the predicate [[pred(b,a)]] is 
 *  conceptually decomposed into a quintet of predicates:
 *
 *     [[bf(b,a)]]   - monotonic wrt [[(B,A)]],
 *
 *     [[csl(b,a)]]  - left-convex & preferably left-bounded wrt [[bf]],
 *
 *     [[csr(b,a)]]  - right-convex & preferably right-bounded wrt [[bf]],
 *
 *     [[anti(b,a)]] - anti-monotonic wrt [[bf]], and
 *
 *     [[sc(b,a)]]   - a residual predicate; 
 *
 *   such that
 *
 *     [[pred(b,a)]] iff [[csl(b,a) && csr(b,a) && sc(b,a)]]
 *
 *     [[!anti(b,a)]] implies [[!csl(b,a) || !csr(b,a)]]
 *
 *  Conceptually, as much as possible, [[pred(b,a)]] is decomposed
 *  into a left-convex [[csl]] and a right-convex [[csr]], with
 *  possibly a residual filtering predicate [[sc(b,a)]].
 *
 *  Intuitively, given an [[a <- A]] and we want to find
 *  all [[b <- B]] that satisfy [[pred(b,a)]]. Then, 
 *     [[!csl(b,a)]] means we dont have to look at [[b' <= b]];
 *     [[!csr(b,a)]] means we dont have to look at [[b <= b']];
 *     [[!anti(b,a)]] means we dont have to consider this [[b]] for [[a <= a']].
 *  A synchrony iterator uses these properties to prune useless
 *  steps from the iteration on [[(B,A)]] to achieve efficiency.
 *
 *  Wong Limsoon
 *  4 May 2023
 */

  object Predicates:
  

    import dbmodel.{ Synchrony, KEY, DEBUG }
    import Synchrony.{ CANSEE, ANTI, ISBEFORE, SCREEN, SIterator  }
    // import Synchrony.{ SITERATOR, SIteratorException }
    // import OrderedCollection.{ OColl, Key }
    import scala.language.implicitConversions

    type Bool      = Boolean       
    type Ord[K]    = Ordering[K]



    /** Helper functions to combine two predicates
     */

    extension [B,A](f: (B, A) => Bool)

      def and(g: (B, A) => Bool): (B,A) => Bool =
        if f==null & g==null then null
        else if g == null then f
        else if f == null then g
        else (b: B, a: A) => f(b, a) && g(b, a)

      def or(g: (B, A) => Bool): (B,A) => Bool =
        if f==null & g==null then null
        else if g == null then f
        else if f == null then g
        else (b: B, a: A) => f(b, a) || g(b, a)

      def butnot(g: (B, A) => Bool): (B,A) => Bool =
        if f==null & g==null then null
        else if g == null then f
        else if f == null then (b: B, a: A) => !g(b, a)
        else (b: B, a: A) => f(b, a) && !g(b, a)

      def negated: (B,A) => Bool = 
        if f==null then null else (b: B, a: A) => !f(b, a)

      def orelse(g: (B, A) => Bool): (B,A) => Bool = if f==null then g else f



    /** [[Pred(pred, csl, csr, anti, bf, ord, screen)]] wraps a 
     *  predicate [[pred]] and associate its left-convex/bounded, 
     *  right-convex/bounded, and other components.
     *
     *  @param pred   the predicate, which can be decomposed into:
     *
     *  @param csl    left-convex & preferably -bounded predicate wrt [[bf]]
     *  @param csr    right-conve &  preferably -bounded predicate wrt [[bf]]
     *  @param screen residual predicate
     *  @require [[pred]] iff [[csl && csr && screen]].
     *
     *  In addition, as per the requirement of Synchrony iterators,
     *  @param ord    ordering on the sorting key of collections
     *  @param bf     monotonic predicate wrt [[ord]]
     *  @param anti   anti-monotonic predicate wrt [[bf]]
     *  @require [[!anti]] implies [[!csl]] or [[!csr]]
     */

    case class Pred[K](
           pred: (K, K) => Bool, 
           _csl: CANSEE[K,K],
           _csr: CANSEE[K,K],
           _anti: ANTI[K,K],
           _bf: ISBEFORE[K,K],
           ord: Ord[K], 
           _screen: SCREEN[K,K]):

      def pass(kb: K, ka: K) = true
      val bf     = _bf orelse ord.lt
      val csl    = _csl orelse pass
      val csr    = _csr orelse pass 
      val anti   = _anti orelse pass
      val screen = _screen orelse pass

      def apply(kb: K, ka: K): Bool = pred(kb, ka)

      def addFilter(sc: SCREEN[K,K]) = this.copy(
        pred = pred and sc, 
        _screen = screen and sc)

      def OR(p: Pred[K]): Pred[K] =
        require(ord == p.ord) 
        /** [[_bf == p._bf]] is required as well. But this cant be checked. */
        Pred(
          pred = pred or p.pred, 
          _csl = csl or p.csl,
          _csr = csr or p.csr,
          _anti = anti or p.anti,
          _bf = bf,
          ord = ord,
          _screen = pred or p.pred)

      def AND(p: Pred[K]): Pred[K] =
        require(ord == p.ord)
        /** [[_bf == p._bf]] is required as well. But this cant be checked. */
        Pred(
          pred = pred and p.pred,
          _csl = _csl and p._csl,
          _csr = _csr and p._csr,
          _anti = _anti and p._anti,
          _bf = bf,
          ord = ord,
          _screen = _screen and p._screen)

      def wrt(fb: K => K, fa: K =>K): Pred[K] = 
        def lift(h: (K,K) => Bool) = (kb: K, ka: K) => h(fb(kb), fa(ka))
        Pred(
          pred = lift(pred),
          _csl = lift(csl),
          _csr = lift(csr),
          _anti = lift(anti),
          _bf = bf,
          ord = ord,
          _screen = lift(screen))



    object Pred:

      /** Alternative constructor for general predicates
       *  which lack convexity/boundedness properties.
       */
        
      def mkGen[K:HasOrder](pred: (K, K) => Bool): Pred[K] =
        val HO = summon[HasOrder[K]]
        Pred(pred, null, null, null, null, HO.ord, pred)


      /** Alternative constructors for predicates which have convexity/
       *  boundedness properties. 
       *
       *  @require [[pred]] is either left-, right-, or bi-convex/bounded.
       *  The convexity/boundedness properties of [[pred]] is specified by
       *  providing non-null values for [[csl]] and [[csr]], leaving either
       *  of these null if [[pred]] lacks the corresponding convexity/
       *  boundedness property.
       *
       *  However, if both [[csl]] and [[csr]] are unspecified, [[pred]]
       *  is assumed to be right-convex/bounded; thus, [[csr]] is "autoset"
       *  to [[pred]] in such a situation.
       *
       *  @require [[pred]] has an associated anti-monotonicity [[anti]].
       *  If [[anti]] is not specified, it is assumed to be [[csl]].
       *  If [[csl]] is not specified, it is assumed to be [[csr]].
       *  If neither [[csl]] nor [[csr]] is specified, it is assumed
       *  to be [[pred]] itself.
       */
        
      def mkWithOrder[K:HasOrder]
             (pred: (K, K) => Bool,
              csl: CANSEE[K,K] = null, 
              csr: CANSEE[K,K] = null, 
              anti: ANTI[K,K] = null, 
              bf: ISBEFORE[K,K] = null,
              screen: SCREEN[K,K] = null)
          : Pred[K] =
        val HO = summon[HasOrder[K]]
        val _csr = csr orelse (if csl == null then pred else null)
        val _anti = anti orelse (csl orelse _csr)
        Pred(pred, csl, _csr, _anti, bf, HO.ord, screen)


      def mkConvex[K:HasOrder](pred: (K, K) => Bool): Pred[K] =
        mkWithOrder(pred = pred, csl = pred, csr = pred)

      def mkLeftConvex[K:HasOrder](csl: (K, K) => Bool): Pred[K] =
        mkWithOrder(pred = csl, csl = csl)

      def mkRightConvex[K:HasOrder](csr: (K, K) => Bool): Pred[K] =
        mkWithOrder(pred = csr, csr = csr)

      def mkBiConvex[K:HasOrder](
              csl: (K, K) => Bool,
              csr: (K, K) => Bool)
          : Pred[K] =
        mkWithOrder(pred = csl and csr, csl = csl, csr = csr)

    end Pred




    /** Provide a nicer syntax for constructing predicates,
     *  like this...
     *
     *   val CSE4 =
     *     import dbmodel.Predicates.{ Synchronizer, Synchronizee }
     *     val a = Synchronizer[Int]()
     *     val b = Synchronizee[Int]()
     *     (b EQ a{_ - 3}) OR ((b GTEQ a) AND (b LTEQ a{_ + 4}))
     */

    case class Synchronizer[K](f: K => K = (k: K) => k):
      def apply(g: K => K) = Synchronizer(g compose f)


    case class Synchronizee[K](f: K => K = (k: K) => k):
      def apply(g: K => K) = Synchronizee(g compose f)


    extension [K](b: Synchronizee[K])(using HO: HasOrder[K])

      def EQ(a: Synchronizer[K]) = 
        val gteq = (kb: K, ka: K) => HO.ord.gteq(b.f(kb), a.f(ka))
        val lteq = (kb: K, ka: K) => HO.ord.lteq(b.f(kb), a.f(ka))
        Pred.mkBiConvex(gteq, lteq)

      def LTEQ(a: Synchronizer[K]) = 
        val lteq = (kb: K, ka: K) => HO.ord.lteq(b.f(kb), a.f(ka))
        Pred.mkRightConvex(lteq)

      def LT(a: Synchronizer[K]) = 
        val lt = (kb: K, ka: K) => HO.ord.lt(b.f(kb), a.f(ka))
        Pred.mkRightConvex(lt)

      def GTEQ(a: Synchronizer[K]) = 
        val gteq = (kb: K, ka: K) => HO.ord.gteq(b.f(kb), a.f(ka))
        Pred.mkLeftConvex(gteq)

      def GT(a: Synchronizer[K]) = 
        val gt = (kb: K, ka: K) => HO.ord.gt(b.f(kb), a.f(ka))
        Pred.mkLeftConvex(gt)

  

    /** Set up infrastructure for predicates that assume some default
     *  underlying ordering on the objects.
     *
     *  Our setup below enables adhoc polymorphism, so that the same
     *  predicate name e.g., [[lt]] can be used as the "less than" 
     *  predicate on different type [[K]]. Here, lowercase [[lt]] is
     *  used for normal function. Uppercase [[LT]] is the corresponding
     *  decomposed predicate designed to be used with Synchrony iterators.
     */
     
    trait HasOrder[K]:
      /** @require 
       *     [[equal]] - bi-convex & anti-mono wrt [[ord]]
       *     [[lt]]    - right-convex/bounded & anti-mono wrt [[ord]]
       *     [[lteq]]  - right-convex/bounded & anti-mono wrt [[ord]]
       *     [[gt]]    - left-convex/bounded & anti-mono wrt [[ord]]
       *     [[gteq]]  - left-convex/bounded & anti-mono wrt [[ord]]
       */
      val ord: Ord[K]
      def equal(b: K, a: K) = b == a          
      def lt(b: K, a: K) = ord.lt(b, a)       
      def lteq(b: K, a: K) = ord.lteq(b, a)   
      def gt(b: K, a: K) = ord.gt(b, a)       
      def gteq(b: K, a: K) = ord.gteq(b, a)   

    /** Realizing adhoc polymorphic functions
     */

    def eq[K:HasOrder](kb: K, ka: K) = summon[HasOrder[K]].equal(kb, ka)
    def lt[K:HasOrder](kb: K, ka: K)  = summon[HasOrder[K]].lt(kb, ka)
    def lteq[K:HasOrder](kb: K, ka: K) = summon[HasOrder[K]].lteq(kb, ka)
    def gt[K:HasOrder](kb: K, ka: K) = summon[HasOrder[K]].gt(kb, ka)
    def gteq[K:HasOrder](kb: K, ka: K) = summon[HasOrder[K]].gteq(kb, ka)

    /** Corresponding predicates for Synchrony iterators
     */

    def LT[K:HasOrder]: Pred[K] = Pred.mkRightConvex(lt[K])
    def LTEQ[K:HasOrder]: Pred[K] = Pred.mkRightConvex(lteq[K])
    def GTEQ[K:HasOrder]: Pred[K] = Pred.mkLeftConvex(gteq[K])
    def GT[K:HasOrder]: Pred[K] = Pred.mkLeftConvex(gt[K])
    def EQ[K:HasOrder]: Pred[K] = Pred.mkWithOrder(eq[K], gteq[K], lteq[K])



    /** Set up infrastructure for "distance" predicates.
     */
  
    trait HasDistance[K]:
      /** @require
       *     [[dl]]    - right-convex/bounded & anti-mono, wrt [[ Ordering[K] ]]
       *     [[dleq]]  - right-convex/bounded & anti-mono, wrt [[ Ordering[K] ]]
       */
      def intdist(b: K, a: K): Int
      def dl(n: Int): (K,K) => Bool = (b: K, a: K) => intdist(b, a) < n
      def dleq(n: Int): (K,K) => Bool = (b: K, a: K) => intdist(b, a) <= n
      def dg(n: Int): (K,K) => Bool = (b: K, a: K) => intdist(b, a) > n
      def dgeq(n: Int): (K,K) => Bool = (b: K, a: K) => intdist(b, a) >= n

    def dl[K:HasDistance](n:Int)(kb:K, ka:K) = summon[HasDistance[K]].dl(n)(kb, ka)
    def dg[K:HasDistance](n:Int)(kb:K, ka:K) = summon[HasDistance[K]].dg(n)(kb, ka)
    def dleq[K:HasDistance](n:Int)(kb:K, ka:K) = summon[HasDistance[K]].dleq(n)(kb, ka)
    def dgeq[K:HasDistance](n: Int)(kb:K, ka:K) = summon[HasDistance[K]].dgeq(n)(kb, ka)

    def DL[K:HasDistance:HasOrder](n: Int): Pred[K] = Pred.mkRightConvex(dl[K](n))
    def DLEQ[K:HasDistance:HasOrder](n: Int): Pred[K] = Pred.mkRightConvex(dleq[K](n))
    def DG[K:HasDistance:HasOrder](n: Int): Pred[K] = Pred.mkGen(dg[K](n))
    def DGEQ[K:HasDistance:HasOrder](n: Int): Pred[K] = Pred.mkGen(dgeq[K](n))



    /** Set up infrastructure for "size" predicates.
     */

    trait HasSize[K]: 
      /** @require
       *     [[szpercent]] - bi-convex/bounded, anti-monotonic wrt [[ Ordering[K] ]]
       */
      def sz(a: K): Double
      def szpercent(n: Double): (K,K) => Bool = (b:K, a: K) =>
        val mn = sz(a) min sz(b)
        val mx = sz(a) max sz(b)
        (mx < mn * n)

    /** [[szpercent(n)(kb,ka)]] checks whether [[max(b,a)]] is within
     *  [[n*100%]] of [[min(b,a)]]
     */
    def szpercent[K:HasSize](n:Double)(kb:K, ka:K) = summon[HasSize[K]].szpercent(n)(kb, ka)

    def SZPERCENT[K:HasSize:HasOrder](n:Double): Pred[K] = Pred.mkConvex(szpercent[K](n))



    /** Set up infrastructure for "line topology" predicates.
     */

    trait LINETOPO[K]:
      /** @require
       *     [[near(n)]]    - right-convex/bounded, antimonotonic wrt [[ Ordering[K] ]]
       *     [[overlap(0)]] - bi-convex/bounded, antimonotonic wrt [[ Ordering[K] ]]
       */
      def overlap(n: Int): (K,K) => Bool
      def near(n: Int): (K,K) => Bool
      def far(n: Int): (K,K) => Bool
      def touch: (K,K) => Bool = b1_at_a2 or b2_at_a1
      def outside: (K,K) => Bool = b2_before_a1 or b1_after_a2
      def enclose: (K,K) => Bool = b1_before_a1 and b2_after_a2
      def inside: (K,K) => Bool = b1_after_a1 and b2_before_a2
      def neighbour(n: Int): (K,K) => Bool = near(n) and outside 

      def outsideNonStrict: (K,K) => Bool = outside or touch

      def encloseNonStrict: (K,K) => Bool = 
        (b1_before_a1 or b1_at_a1) and (b2_after_a2 or b2_at_a2)

      def insideNonStrict: (K,K) => Bool = 
        (b1_after_a1 or b1_at_a1) and (b2_before_a2 or b2_at_a2)

      def b1_before_a1: (K, K) => Bool
      def b1_after_a1: (K, K) => Bool
      def b2_before_a2: (K, K) => Bool
      def b2_after_a2: (K, K) => Bool
      def b1_before_a2: (K, K) => Bool
      def b1_after_a2: (K, K) => Bool
      def b2_before_a1: (K, K) => Bool
      def b2_after_a1: (K, K) => Bool
      def b2_at_a2: (K, K) => Bool
      def b2_at_a1: (K, K) => Bool
      def b1_at_a2: (K, K) => Bool
      def b1_at_a1: (K, K) => Bool
  
    def overlap[K:LINETOPO](n: Int)(kb: K, ka: K) = summon[LINETOPO[K]].overlap(n)(kb, ka)
    def near[K:LINETOPO](n: Int)(kb: K, ka: K) = summon[LINETOPO[K]].near(n)(kb, ka)
    def far[K:LINETOPO](n: Int)(kb: K, ka: K) = summon[LINETOPO[K]].far(n)(kb, ka)
    def inside[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].inside(kb, ka)
    def enclose[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].enclose(kb, ka)
    def touch[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].touch(kb, ka)
    def outside[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].outside(kb, ka)
    def neighbour[K:LINETOPO](n: Int)(kb: K, ka: K) = summon[LINETOPO[K]].neighbour(n)(kb, ka)
    def insideNonStrict[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].insideNonStrict(kb, ka)
    def encloseNonStrict[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].encloseNonStrict(kb, ka)
    def outsideNonStrict[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].outsideNonStrict(kb, ka)
    def b1_before_a1[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b1_before_a1(kb, ka)
    def b1_after_a1[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b1_after_a1(kb, ka)
    def b2_before_a2[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b2_before_a2(kb, ka)
    def b2_after_a2[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b2_after_a2(kb, ka)
    def b1_before_a2[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b1_before_a2(kb, ka)
    def b1_after_a2[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b1_after_a2(kb, ka)
    def b2_before_a1[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b2_before_a1(kb, ka)
    def b2_after_a1[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b2_after_a1(kb, ka)
    def b2_at_a2[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b2_at_a2(kb, ka)
    def b2_at_a1[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b2_at_a1(kb, ka)
    def b1_at_a2[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b1_at_a2(kb, ka)
    def b1_at_a1[K:LINETOPO](kb: K, ka: K) = summon[LINETOPO[K]].b1_at_a1(kb, ka)

    def b1_BEFORE_a1[K:LINETOPO:HasOrder]: Pred[K] = Pred.mkRightConvex(b1_before_a1[K])
    def b1_AFTER_a1[K:LINETOPO:HasOrder]: Pred[K] = Pred.mkLeftConvex(b1_after_a1[K])
    def b1_BEFORE_a2[K:LINETOPO:HasOrder]: Pred[K] = Pred.mkRightConvex(b1_before_a2[K])
    def b1_AFTER_a2[K:LINETOPO:HasOrder]: Pred[K] = Pred.mkLeftConvex(b1_after_a2[K])
    def b1_AT_a2[K:LINETOPO:HasOrder]: Pred[K] = Pred. mkLeftConvex(b1_at_a2[K])
    def b1_AT_a1[K:LINETOPO:HasOrder]: Pred[K] = Pred. mkWithOrder(
      pred = b1_at_a1[K], 
      csl  = b1_after_a1[K] or b1_at_a1,
      csr  = b1_before_a1[K] or b1_at_a1)

    def b2_BEFORE_a2[K:LINETOPO:HasOrder]: Pred[K] = Pred.mkWithOrder(
      pred = b2_before_a2[K],
      csr = b1_before_a2[K],
      anti = b1_before_a2[K],
      screen = b2_before_a2[K])
 
    def b2_AFTER_a2[K:LINETOPO:HasOrder]: Pred[K] = Pred.mkWithOrder(
      pred = b2_after_a2[K],
      csl = b2_after_a1[K],
      anti = b2_after_a1[K],
      screen = b2_after_a2[K])

    def NEAR[K:LINETOPO:HasOrder](n: Int): Pred[K] = Pred.mkRightConvex(near[K](n))
    def FAR[K:LINETOPO:HasOrder](n: Int): Pred[K] = Pred.mkGen(far[K](n))
    def OUTSIDE[K:LINETOPO:HasOrder]: Pred[K] = Pred.mkGen(outside[K])

    /** [[OVERLAP(n)]] is tricky because for [[n > 1]],
     *  it is not left- and right-convex.
     */
    def OVERLAP[K:LINETOPO:HasOrder](n: Int): Pred[K] = 
      Pred.mkWithOrder(
        pred = overlap[K](n),
        csl = (kb: K, ka: K) => true,
        csr = b2_after_a1[K] and b1_before_a2[K],
        anti = b2_after_a1[K],
        screen = overlap[K](n))

    def TOUCH[K:LINETOPO:HasOrder]: Pred[K] =
      Pred.mkWithOrder(
        pred = touch[K],
        csl = (kb: K, ka: K) => true,
        csr = touch[K] or (b1_before_a2[K] and b2_after_a1),
        anti = b2_after_a1[K] or b2_at_a1[K],
        screen = touch[K])

    def INSIDE[K:LINETOPO:HasOrder]: Pred[K] =
      Pred.mkWithOrder(
        pred = inside[K],
        csl = b1_after_a1[K] and b2_before_a2[K], 
        csr = b1_before_a2[K],
        anti = b1_after_a1[K],
        bf = lteq[K])

    def ENCLOSE[K:LINETOPO:HasOrder]: Pred[K] = 
      Pred.mkWithOrder(
        pred = enclose[K],
        csl = (kb: K, ka: K) => true,
        csr = b1_before_a1[K] and b2_after_a2[K],
        anti = b2_after_a1[K],
        bf = lt[K])
          
    def NEIGHBOUR[K:LINETOPO:HasOrder](n: Int): Pred[K] =
      NEAR[K](n).addFilter(outside[K])





    /** The types and values below are needed to support adhoc 
     *  polymorphism over numeric types used in the predicates above.
     *  Scala's [[Numeric[K]]] has some problems because it causes,
     *  e.g., [[Int]] to be auto/implicitly converted to another
     *  Integer type.
     */

    trait DBNumeric[K] extends HasOrder[K]:
      val MinValue: K
      val MaxValue: K
      def plus(b: K, a: K): K
      def times(b: K, a: K): K
      def fromInt(n: Int): K
      def min(b: K, a: K): K = ord.min(b, a)
      def max(b: K, a: K): K = ord.max(b, a)



    /** As examples, instantiate predicates on [[String]], [[Int]]
     *  and [[(Int,Int)]]
     */

    trait DSTRING extends HasOrder[String], HasSize[String]

    given dString: DSTRING with
      val ord = Ordering[String]
      def sz(n: String) = n.length




    trait DINT extends 
      HasOrder[Int], HasDistance[Int], HasSize[Int], DBNumeric[Int]

    given dInt: DINT with
      def intdist(b: Int, a: Int) = (b - a).abs
      def sz(n: Int) = n.toDouble 
      val ord = Ordering[Int]
      val MinValue = Int.MinValue
      val MaxValue = Int.MaxValue
      def fromInt(n:Int) = n
      def plus(b: Int, a: Int) = b + a
      def times(b: Int, a: Int) = b * a




    trait DDBL extends 
      HasOrder[Double], HasDistance[Double], 
      HasSize[Double], DBNumeric[Double]

    given dDbl: DDBL with
      def intdist(b: Double, a: Double) = (b - a).abs.toInt
      def sz(n: Double) = n 
      val ord = Ordering[Double]
      val MinValue = Double.MinValue
      val MaxValue = Double.MaxValue
      def fromInt(n:Int) = n.toDouble
      def plus(b: Double, a: Double) = b + a
      def times(b: Double, a: Double) = b * a



    trait DDbl2 extends HasOrder[(Double,Double)]

    given dDbl2: DDbl2 with
      type Dbl2 = (Double,Double)
      val ord = Ordering[(Double,Double)]



    trait DINT2 extends 
      HasOrder[(Int,Int)], HasDistance[(Int,Int)], LINETOPO[(Int,Int)]

    given dInt2: DINT2 with
      type Int2 = (Int,Int)

      val ord = Ordering[(Int,Int)]

      /** Removed, [[szpercent]] is not convex wrt [[ Ordering[(Int,Int)] ]]
       *
      def sz(a: Int2) =
        val (a1, a2) = a  // Assume a1 < a2
        (a2 - a1).toDouble
       *
       */

      def intdist(b: Int2, a: Int2) =
        val (b1, b2) = b  // Assume b1 < b2
        val (a1, a2) = a  // Assume a1 < a2
        if a2 < b1 then b1 - a2 else if b2 < a1 then a1 - b2 else 0

      def overlap(n: Int) = (b: Int2, a: Int2) =>
        val (b1, b2) = b  // Assume b1 < b2
        val (a1, a2) = a  // Assume a1 < a2
        (a1 < b2 && b1 < a2) &&
        ((a2 min b2) - (a1 max b1) >= n) 

      def near(n: Int) = this.dleq(n)
      def far(n: Int) = this.dgeq(n)
      def b2_after_a2 = (b: Int2, a: Int2) => a._2 < b._2
      def b2_after_a1 = (b: Int2, a: Int2) => a._1 < b._2
      def b2_before_a2 = (b: Int2, a: Int2) => a._2 > b._2
      def b2_before_a1 = (b: Int2, a: Int2) => a._1 > b._2
      def b1_after_a2 = (b: Int2, a: Int2) => a._2 < b._1
      def b1_after_a1 = (b: Int2, a: Int2) => a._1 < b._1
      def b1_before_a2 = (b: Int2, a: Int2) => b._1 < a._2
      def b1_before_a1 = (b: Int2, a: Int2) => b._1 < a._1
      def b2_at_a2 = (b: Int2, a: Int2) => b._2 == a._2
      def b2_at_a1 = (b: Int2, a: Int2) => b._2 == a._1
      def b1_at_a2 = (b: Int2, a: Int2) => b._1 == a._2
      def b1_at_a1 = (b: Int2, a: Int2) => b._1 == a._1

  end Predicates


