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