0 | module Data.Refined.Bits64
 1 |
 2 | import Control.Relation.ReflexiveClosure
 3 | import Control.Relation
 4 | import public Data.Prim.Bits64
 5 | import public Data.Refined.Core
 6 |
 7 | %default total
 8 |
 9 | public export %inline
10 | {x : Bits64} -> HDec0 Bits64 (< x) where
11 |   hdec0 v = lt v x
12 |
13 | public export %inline
14 | {x : Bits64} -> HDec0 Bits64 (x <) where
15 |   hdec0 v = lt x v
16 |
17 | public export %inline
18 | {x : Bits64} -> HDec0 Bits64 (<= x) where
19 |   hdec0 v = lte v x
20 |
21 | public export %inline
22 | {x : Bits64} -> HDec0 Bits64 (x <=) where
23 |   hdec0 v = lte x v
24 |
25 | --------------------------------------------------------------------------------
26 | --          Non-operators
27 | --------------------------------------------------------------------------------
28 |
29 | ||| `LessThan m n` is an alias for `n < m`.
30 | |||
31 | ||| This is useful when defining ranges such as
32 | ||| `From 2 && LessThan 10`, but it gives the wrong idea when used in
33 | ||| infix notation. So, don't do this: ```x `LessThan` 10```.
34 | public export
35 | 0 LessThan : Bits64 -> Bits64 -> Type
36 | LessThan m n = n < m
37 |
38 | ||| `From m n` is an alias for `n <= m`.
39 | public export
40 | 0 To : Bits64 -> Bits64 -> Type
41 | To m n = ReflexiveClosure (<) n m
42 |
43 | ||| `GreaterThan m n` is an alias for `m < n`.
44 | |||
45 | ||| This is useful when defining ranges such as
46 | ||| `From 2 && LessThan 10`, but it gives the wrong idea when used in
47 | ||| infix notation. So, don't do this: ```x `GreaterThan` 10```.
48 | public export
49 | 0 GreaterThan : Bits64 -> Bits64 -> Type
50 | GreaterThan = (<)
51 |
52 | ||| `From m n` is an alias for `m <= n`.
53 | public export
54 | 0 From : Bits64 -> Bits64 -> Type
55 | From = ReflexiveClosure (<)
56 |
57 | ||| `FromTo m n` is an alias for `From m && To n`.
58 | public export
59 | 0 FromTo : Bits64 -> Bits64 -> Bits64 -> Type
60 | FromTo m n = From m && To n
61 |
62 | ||| `Between m n` is an alias for `GreaterThan m && LessThan n`.
63 | public export
64 | 0 Between : Bits64 -> Bits64 -> Bits64 -> Type
65 | Between m n = GreaterThan m && LessThan n
66 |
67 | --------------------------------------------------------------------------------
68 | --          Widenings
69 | --------------------------------------------------------------------------------
70 |
71 | export
72 | 0 widen :
73 |      FromTo m n x
74 |   -> {auto 0 p1 : m2 <= m}
75 |   -> {auto 0 p2 : n  <= n2}
76 |   -> FromTo m2 n2 x
77 | widen (And y z) = And (transitive p1 y) (transitive z p2)
78 |
79 | export
80 | 0 widen' :
81 |      Between m n x
82 |   -> {auto 0 p1 : m2 <= m}
83 |   -> {auto 0 p2 : n  <= n2}
84 |   -> Between m2 n2 x
85 | widen' (And y z) = And (strictRight p1 y) (strictLeft z p2)
86 |