Add Data.Primitives.Views

libs/base/Data/Primitives/Views.idr

@@ -0,0 +1,82 @@
+module Data.Primitives.Views
+
+-- We need all the believe_mes and asserts throughout this file because we're
+-- working with primitive here! We also have separate implementations per
+-- primitive, rather than using interfaces, because we're only going to trust
+-- the primitive implementations.
+
+namespace IntegerV
+  ||| View for expressing a number as a multiplication + a remainder
+  public export
+  data Divides : Integer -> (d : Integer) -> Type where
+       DivByZero : Divides x 0
+       DivBy : (div, rem : _) ->
+               (prf : rem >= 0 && rem < d = True) ->
+               Divides ((d * div) + rem) d
+
+  ||| Covering function for the `Divides` view
+  public export
+  divides : (val : Integer) -> (d : Integer) -> Divides val d
+  divides val 0 = DivByZero
+  divides val d
+         = assert_total $
+             let dividend = if d < 0 then -(val `div` abs d)
+                                     else val `div` d
+                 remainder = abs (val - dividend * d) in
+                 believe_me (DivBy {d} dividend remainder
+                            (believe_me (Refl {x = True})))
+
+  ||| View for recursion over Integers
+  public export
+  data IntegerRec : Integer -> Type where
+       IntegerZ : IntegerRec 0
+       IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
+       IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
+
+  ||| Covering function for `IntegerRec`
+  public export
+  integerRec : (x : Integer) -> IntegerRec x
+  integerRec 0 = IntegerZ
+  integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
+                      else believe_me (IntegerPred {n = -x}
+                                (assert_total (believe_me (integerRec (x + 1)))))
+
+namespace IntV
+  ||| View for expressing a number as a multiplication + a remainder
+  public export
+  data Divides : Int -> (d : Int) -> Type where
+       DivByZero : IntV.Divides x 0
+       DivBy : (div, rem : _) ->
+               (prf : rem >= 0 && rem < d = True) ->
+               IntV.Divides ((d * div) + rem) d
+
+  -- I have assumed, but not actually verified, that this will still
+  -- give a right result (i.e. still adding up) when the Ints overflow.
+  -- TODO: Someone please check this and fix if necessary...
+
+  ||| Covering function for the `Divides` view
+  public export
+  divides : (val : Int) -> (d : Int) -> Divides val d
+  divides val 0 = DivByZero
+  divides val d
+         = assert_total $
+             let dividend = if d < 0 then -(val `div` abs d)
+                                     else val `div` d
+                 remainder = abs (val - dividend * d) in
+                 believe_me (DivBy {d} dividend remainder
+                            (believe_me (Refl {x = True})))
+
+  ||| View for recursion over Ints
+  public export
+  data IntRec : Int -> Type where
+       IntZ : IntRec 0
+       IntSucc : IntRec (n - 1) -> IntRec n
+       IntPred : IntRec ((-n) + 1) -> IntRec (-n)
+
+  ||| Covering function for `IntRec`
+  public export
+  intRec : (x : Int) -> IntRec x
+  intRec 0 = IntZ
+  intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
+                      else believe_me (IntPred {n = -x}
+                                (assert_total (believe_me (intRec (x + 1)))))

libs/base/base.ipkg

@@ -4,12 +4,13 @@ modules = Control.WellFounded,
 
           Data.Buffer,
           Data.Fin,
+          Data.IORef,
           Data.List,
           Data.List.Views,
           Data.Maybe,
           Data.Nat,
           Data.Nat.Views,
-          Data.IORef,
+          Data.Primitives.Views,
           Data.So,
           Data.Stream,
           Data.Strings,