edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-28 14:06:26 +03:00
Code Issues Projects Releases Wiki Activity
fa190ab1a9
Idris2-boot/libs/base/Decidable/Equality.idr

146 lines
5.5 KiB
Idris
Raw Normal View History

More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway).
2019-07-01 01:54:50 +03:00
module Decidable.Equality
Delay case elaboration This helps a few things because it delays elaboration of the block until as much as possible is known about its type. Also added a few libraries.
2019-07-02 18:53:41 +03:00
import Data.Maybe
import Data.Nat
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway).
2019-07-01 01:54:50 +03:00
--------------------------------------------------------------------------------
-- Decidable equality
--------------------------------------------------------------------------------
||| Decision procedures for propositional equality
public export
interface DecEq t where
||| Decide whether two elements of `t` are propositionally equal
total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
--------------------------------------------------------------------------------
-- Utility lemmas
--------------------------------------------------------------------------------
||| The negation of equality is symmetric (follows from symmetry of equality)
Remove trailing whitespace from Idris sources. This is the result of running the command: $ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} + I confirmed before running it that this would not affect any markdown formatting in documentation comments.
2019-10-26 00:24:25 +03:00
export total
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway).
2019-07-01 01:54:50 +03:00
negEqSym : forall a, b . (a = b -> Void) -> (b = a -> Void)
negEqSym p h = p (sym h)
||| Everything is decidably equal to itself
Remove trailing whitespace from Idris sources. This is the result of running the command: $ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} + I confirmed before running it that this would not affect any markdown formatting in documentation comments.
2019-10-26 00:24:25 +03:00
export total
Change equality elaboration Elaborate via either === (homogeneous equality) or ~=~ (heterogeneous equality) both of which are synonyms for Equal. This is to get the Idris 1 behaviour that equality is homogeneous by default to reduce the need for type annotations, but heterogeneous if that doesn't work.
2019-07-05 13:26:45 +03:00
decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway).
2019-07-01 01:54:50 +03:00
decEqSelfIsYes {x} with (decEq x x)
decEqSelfIsYes {x} | Yes Refl = Refl
decEqSelfIsYes {x} | No contra = absurd $ contra Refl
--------------------------------------------------------------------------------
--- Unit
--------------------------------------------------------------------------------
Delay case elaboration This helps a few things because it delays elaboration of the block until as much as possible is known about its type. Also added a few libraries.
2019-07-02 18:53:41 +03:00
export
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway).
2019-07-01 01:54:50 +03:00
implementation DecEq () where
decEq () () = Yes Refl
Delay case elaboration This helps a few things because it delays elaboration of the block until as much as possible is known about its type. Also added a few libraries.
2019-07-02 18:53:41 +03:00
--------------------------------------------------------------------------------
-- Booleans
--------------------------------------------------------------------------------
total trueNotFalse : True = False -> Void
trueNotFalse Refl impossible
export
implementation DecEq Bool where
decEq True True = Yes Refl
decEq False False = Yes Refl
decEq True False = No trueNotFalse
decEq False True = No (negEqSym trueNotFalse)
--------------------------------------------------------------------------------
-- Nat
--------------------------------------------------------------------------------
total ZnotS : Z = S n -> Void
ZnotS Refl impossible
export
implementation DecEq Nat where
decEq Z Z = Yes Refl
decEq Z (S _) = No ZnotS
decEq (S _) Z = No (negEqSym ZnotS)
decEq (S n) (S m) with (decEq n m)
decEq (S n) (S m) | Yes p = Yes $ cong S p
decEq (S n) (S m) | No p = No $ \h : (S n = S m) => p $ succInjective n m h
--------------------------------------------------------------------------------
-- Maybe
--------------------------------------------------------------------------------
total nothingNotJust : {x : t} -> (Nothing {ty = t} = Just x) -> Void
nothingNotJust Refl impossible
export
implementation (DecEq t) => DecEq (Maybe t) where
decEq Nothing Nothing = Yes Refl
decEq (Just x') (Just y') with (decEq x' y')
decEq (Just x') (Just y') | Yes p = Yes $ cong Just p
Remove trailing whitespace from Idris sources. This is the result of running the command: $ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} + I confirmed before running it that this would not affect any markdown formatting in documentation comments.
2019-10-26 00:24:25 +03:00
decEq (Just x') (Just y') | No p
Delay case elaboration This helps a few things because it delays elaboration of the block until as much as possible is known about its type. Also added a few libraries.
2019-07-02 18:53:41 +03:00
= No $ \h : Just x' = Just y' => p $ justInjective h
decEq Nothing (Just _) = No nothingNotJust
decEq (Just _) Nothing = No (negEqSym nothingNotJust)
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
-- TODO: Other prelude data types
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway).
2019-07-01 01:54:50 +03:00
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
-- For the primitives, we have to cheat because we don't have access to their
Remove trailing whitespace from Idris sources. This is the result of running the command: $ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} + I confirmed before running it that this would not affect any markdown formatting in documentation comments.
2019-10-26 00:24:25 +03:00
-- internal implementations. We use believe_me for the inequality proofs
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
-- because we don't them to reduce (and they should never be needed anyway...)
-- A postulate would be better, but erasure analysis may think they're needed
-- for computation in a higher order setting.
Delay case elaboration This helps a few things because it delays elaboration of the block until as much as possible is known about its type. Also added a few libraries.
2019-07-02 18:53:41 +03:00
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
--------------------------------------------------------------------------------
-- Int
--------------------------------------------------------------------------------
Need to export DecEq implementations!
2019-07-05 20:41:50 +03:00
export
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
implementation DecEq Int where
decEq x y = case x == y of -- Blocks if x or y not concrete
Remove trailing whitespace from Idris sources. This is the result of running the command: $ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} + I confirmed before running it that this would not affect any markdown formatting in documentation comments.
2019-10-26 00:24:25 +03:00
True => Yes primitiveEq
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
False => No primitiveNotEq
where primitiveEq : forall x, y . x = y
primitiveEq = believe_me (Refl {x})
primitiveNotEq : forall x, y . x = y -> Void
primitiveNotEq prf = believe_me {b = Void} ()
--------------------------------------------------------------------------------
-- Char
--------------------------------------------------------------------------------
Need to export DecEq implementations!
2019-07-05 20:41:50 +03:00
export
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
implementation DecEq Char where
decEq x y = case x == y of -- Blocks if x or y not concrete
Remove trailing whitespace from Idris sources. This is the result of running the command: $ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} + I confirmed before running it that this would not affect any markdown formatting in documentation comments.
2019-10-26 00:24:25 +03:00
True => Yes primitiveEq
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
False => No primitiveNotEq
where primitiveEq : forall x, y . x = y
primitiveEq = believe_me (Refl {x})
primitiveNotEq : forall x, y . x = y -> Void
primitiveNotEq prf = believe_me {b = Void} ()
--------------------------------------------------------------------------------
-- Integer
--------------------------------------------------------------------------------
Need to export DecEq implementations!
2019-07-05 20:41:50 +03:00
export
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
implementation DecEq Integer where
decEq x y = case x == y of -- Blocks if x or y not concrete
Remove trailing whitespace from Idris sources. This is the result of running the command: $ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} + I confirmed before running it that this would not affect any markdown formatting in documentation comments.
2019-10-26 00:24:25 +03:00
True => Yes primitiveEq
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
False => No primitiveNotEq
where primitiveEq : forall x, y . x = y
primitiveEq = believe_me (Refl {x})
primitiveNotEq : forall x, y . x = y -> Void
primitiveNotEq prf = believe_me {b = Void} ()
--------------------------------------------------------------------------------
-- String
--------------------------------------------------------------------------------
Need to export DecEq implementations!
2019-07-05 20:41:50 +03:00
export
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
implementation DecEq String where
decEq x y = case x == y of -- Blocks if x or y not concrete
Remove trailing whitespace from Idris sources. This is the result of running the command: $ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} + I confirmed before running it that this would not affect any markdown formatting in documentation comments.
2019-10-26 00:24:25 +03:00
True => Yes primitiveEq
A bit more library support, for Chapter 9 Also a tweak to errors when compiling to scheme, so that it properly reports an error then quits if it's supposed to crash.
2019-07-05 19:24:15 +03:00
False => No primitiveNotEq
where primitiveEq : forall x, y . x = y
primitiveEq = believe_me (Refl {x})
primitiveNotEq : forall x, y . x = y -> Void
primitiveNotEq prf = believe_me {b = Void} ()
Delay case elaboration This helps a few things because it delays elaboration of the block until as much as possible is known about its type. Also added a few libraries.
2019-07-02 18:53:41 +03:00
Reference in New Issue Copy Permalink