@@ -0,0 +1,49 @@
1+module Data.Primitives.Views
2+
3+-- We need all the believe_mes and asserts throughout this file because we're
4+-- working with primitive here! We also have separate implementations per
5+-- primitive, rather than using interfaces, because we're only going to trust
6+-- the primitive implementations.
7+
8+namespace Integer
9+ ||| View for expressing a number as a multiplication + a remainder
10+ public export
11+ data Divides : Integer -> (d : Integer) -> Type where
12+ DivByZero : Divides x 0
13+ DivBy : (prf : rem >= 0 && rem < d = True) ->
14+ Divides ((d * div) + rem) d
15+
16+ ||| Covering function for the `Divides` view
17+ export
18+ divides : (val : Integer) -> (d : Integer) -> Divides val d
19+ divides val 0 = DivByZero
20+ divides val d
21+ = let dividend = if d < 0 then -(val `div` abs d)
22+ else val `div` d
23+ remainder = val `mod` d in
24+ believe_me (DivBy {d} {div = dividend} {rem = remainder}
25+ (believe_me (Refl {x = True})))
26+
27+namespace Int
28+ ||| View for expressing a number as a multiplication + a remainder
29+ public export
30+ data Divides : Int -> (d : Int) -> Type where
31+ DivByZero : Int.Divides x 0
32+ DivBy : (prf : rem >= 0 && rem < d = True) ->
33+ Int.Divides ((d * div) + rem) d
34+
35+ -- I have assumed, but not actually verified, that this will still
36+ -- give a right result (i.e. still adding up) when the Ints overflow.
37+ -- TODO: Someone please check this and fix if necessary...
38+
39+ ||| Covering function for the `Divides` view
40+ export
41+ divides : (val : Int) -> (d : Int) -> Divides val d
42+ divides val 0 = DivByZero
43+ divides val d
44+ = let dividend = if d < 0 then -(val `div` abs d)
45+ else val `div` d
46+ remainder = val `mod` d in
47+ believe_me (DivBy {d} {div = dividend} {rem = remainder}
48+ (believe_me (Refl {x = True})))
49+