1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-22 19:21:39 +03:00
Idris2/libs/base/Data/Primitives/Views.idr

83 lines
3.1 KiB
Idris
Raw Normal View History

2020-05-18 15:59:07 +03:00
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)))))