
   0 | module Libraries.Text.Bounded
   1 | 
   2 | %default total
   3 | 
   4 | 
   5 | public export
   6 | record Bounds where
   7 |   constructor MkBounds
   8 |   ||| 0-based first line
   9 |   startLine : Int
  10 |   ||| 0-based first col
  11 |   startCol : Int
  12 |   ||| 0-based last line of bound
  13 |   endLine : Int
  14 |   ||| 0-based first column after bound
  15 |   endCol : Int
  16 | 
  17 | export
  18 | Show Bounds where
  19 |   showPrec d (MkBounds sl sc el ec) =
  20 |     showCon d "MkBounds" (concat [showArg sl, showArg sc, showArg el, showArg ec])
  21 | 
  22 | export
  23 | startBounds : Bounds -> (Int, Int)
  24 | startBounds b = (b.startLine, b.startCol)
  25 | 
  26 | export
  27 | endBounds : Bounds -> (Int, Int)
  28 | endBounds b = (b.endLine, b.endCol)
  29 | 
  30 | export
  31 | union : Bounds -> Bounds -> Bounds
  32 | union b1 b2 =
  33 |   let (ur, uc) = min (startBounds b1) (startBounds b2)
  34 |       (lr, lc) = max (endBounds b1) (endBounds b2)
  35 |    in MkBounds ur uc lr lc
  36 | 
  37 | export
  38 | Eq Bounds where
  39 |   (MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') =
  40 |       sl == sl'
  41 |    && sc == sc'
  42 |    && el == el'
  43 |    && ec == ec'
  44 | 
  45 | public export
  46 | record WithBounds ty where
  47 |   constructor MkBounded
  48 |   val : ty
  49 |   isIrrelevant : Bool
  50 |   bounds : Bounds
  51 | 
  52 | export
  53 | start : WithBounds ty -> (Int, Int)
  54 | start = startBounds . bounds
  55 | 
  56 | export
  57 | end : WithBounds ty -> (Int, Int)
  58 | end = endBounds . bounds
  59 | 
  60 | export
  61 | Eq ty => Eq (WithBounds ty) where
  62 |   (MkBounded val ir bd) == (MkBounded val' ir' bd') =
  63 |     val == val' && ir == ir' && bd == bd'
  64 | 
  65 | export
  66 | Show ty => Show (WithBounds ty) where
  67 |   showPrec d (MkBounded val ir bd) =
  68 |     showCon d "MkBounded" (concat [showArg ir, showArg val, showArg bd])
  69 | 
  70 | export
  71 | Functor WithBounds where
  72 |   map f (MkBounded val ir bd) = MkBounded (f val) ir bd
  73 | 
  74 | export
  75 | Foldable WithBounds where
  76 |   foldr c n b = c b.val n
  77 | 
  78 | export
  79 | Traversable WithBounds where
  80 |   traverse f (MkBounded v a bd) = (\ v => MkBounded v a bd) <$> f v
  81 | 
  82 | export
  83 | irrelevantBounds : ty -> WithBounds ty
  84 | irrelevantBounds x = MkBounded x True (MkBounds (-1) (-1) (-1) (-1))
  85 | 
  86 | export
  87 | removeIrrelevance : WithBounds ty -> WithBounds ty
  88 | removeIrrelevance (MkBounded val ir bd) = MkBounded val True bd
  89 | 
  90 | export
  91 | mergeBounds : WithBounds ty -> WithBounds ty' -> WithBounds ty'
  92 | mergeBounds (MkBounded _ True _) (MkBounded val True _) = irrelevantBounds val
  93 | mergeBounds (MkBounded _ True _) b2 = b2
  94 | mergeBounds b1 (MkBounded val True _) = const val <$> b1
  95 | mergeBounds b1 b2 =
  96 |       MkBounded b2.val False (union (bounds b1) (bounds b2))
  97 | 
  98 | export
  99 | joinBounds : WithBounds (WithBounds ty) -> WithBounds ty
 100 | joinBounds b = mergeBounds b b.val
 101 |