0 | module Data.Primitives.Views
 1 |
 2 | %default total
 3 |
 4 | -- We need all the believe_mes and asserts throughout this file because we're
 5 | -- working with primitive here! We also have separate implementations per
 6 | -- primitive, rather than using interfaces, because we're only going to trust
 7 | -- the primitive implementations.
 8 |
 9 | namespace IntegerV
10 |   ||| View for expressing a number as a multiplication + a remainder
11 |   public export
12 |   data Divides : Integer -> (d : Integer) -> Type where
13 |        DivByZero : Divides x 0
14 |        DivBy : (div, rem : _) ->
15 |                (prf : rem >= 0 && rem < d = True) ->
16 |                Divides ((d * div) + rem) d
17 |
18 |   ||| Covering function for the `Divides` view
19 |   public export
20 |   divides : (val : Integer) -> (d : Integer) -> Divides val d
21 |   divides val 0 = DivByZero
22 |   divides val d
23 |          = assert_total $
24 |              let dividend = if d < 0 then -(val `div` abs d)
25 |                                      else val `div` d
26 |                  remainder = abs (val - dividend * d) in
27 |                  believe_me (DivBy {d} dividend remainder
28 |                             (believe_me (Refl {x = True})))
29 |
30 |   ||| View for recursion over Integers
31 |   public export
32 |   data IntegerRec : Integer -> Type where
33 |        IntegerZ : IntegerRec 0
34 |        -- adding the constant (-1 or 1) on the left keeps the view
35 |        -- similar to the inductive definition of natural numbers, and
36 |        -- is usually compatible with pattern matching on arguments
37 |        -- left-to-right.
38 |        IntegerSucc : IntegerRec (-1 + n) -> IntegerRec n
39 |        IntegerPred : IntegerRec (1 + (-n)) -> IntegerRec (-n)
40 |
41 |   ||| Covering function for `IntegerRec`
42 |   public export
43 |   integerRec : (x : Integer) -> IntegerRec x
44 |   integerRec 0 = IntegerZ
45 |   integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (-1 + x)))
46 |                       else believe_me (IntegerPred {n = -x}
47 |                                 (assert_total (believe_me (integerRec (1 + x)))))
48 |
49 | namespace IntV
50 |   ||| View for expressing a number as a multiplication + a remainder
51 |   public export
52 |   data Divides : Int -> (d : Int) -> Type where
53 |        DivByZero : IntV.Divides x 0
54 |        DivBy : (div, rem : _) ->
55 |                (prf : rem >= 0 && rem < d = True) ->
56 |                IntV.Divides ((d * div) + rem) d
57 |
58 |   -- I have assumed, but not actually verified, that this will still
59 |   -- give a right result (i.e. still adding up) when the Ints overflow.
60 |   -- TODO: Someone please check this and fix if necessary...
61 |
62 |   ||| Covering function for the `Divides` view
63 |   public export
64 |   divides : (val : Int) -> (d : Int) -> Divides val d
65 |   divides val 0 = DivByZero
66 |   divides val d
67 |          = assert_total $
68 |              let dividend = if d < 0 then -(val `div` abs d)
69 |                                      else val `div` d
70 |                  remainder = abs (val - dividend * d) in
71 |                  believe_me (DivBy {d} dividend remainder
72 |                             (believe_me (Refl {x = True})))
73 |
74 |   ||| View for recursion over Ints
75 |   public export
76 |   data IntRec : Int -> Type where
77 |        IntZ : IntRec 0
78 |        -- adding the constant (-1 or 1) on the left keeps the view
79 |        -- similar to the inductive definition of natural numbers, and
80 |        -- is usually compatible with pattern matching on arguments
81 |        -- left-to-right.
82 |        IntSucc : IntRec (-1 + n) -> IntRec n
83 |        IntPred : IntRec (1 + (-n)) -> IntRec (-n)
84 |
85 |   ||| Covering function for `IntRec`
86 |   public export
87 |   intRec : (x : Int) -> IntRec x
88 |   intRec 0 = IntZ
89 |   intRec x = if x > 0 then IntSucc (assert_total (intRec (-1 + x)))
90 |                       else believe_me (IntPred {n = -x}
91 |                                 (assert_total (believe_me (intRec (1 + x)))))
92 |