git.iko.soy/Idris-dev
on master help sign in
Cleaned up, and added a commented-out attempt at a 'decision' convenience function, which now fails work.
1b511c7Timo Petteri Sinnemäki
libs/base/Data/Rel.idr−5
compare with master
unifiedsplit
@@ -5,11 +5,6 @@ import Data.VectFun
5Rel : Vect n Type -> Type
5Rel : Vect n Type -> Type
6Rel ts = VectFun ts Type
6Rel ts = VectFun ts Type
7
7
8−-- ATM it seems that using this at least for Decidable results in
9−-- inconvenience in the form of necessity of explicit instance declarations.
10−--liftRel : (ts : Vect k Type) -> (p : VectFun ts Type) -> (Type -> Type) -> Type
11−--liftRel [] p f = f p
12−--liftRel (t :: ts) p f = (x : t) -> liftRel ts (p x) f
13liftRel : (ts : Vect k Type) -> (p : Rel ts) -> (Type -> Type) -> Type
8liftRel : (ts : Vect k Type) -> (p : Rel ts) -> (Type -> Type) -> Type
14liftRel [] p f = f p
9liftRel [] p f = f p
15liftRel (t :: ts) p f = (x : t) -> liftRel ts (p x) f
10liftRel (t :: ts) p f = (x : t) -> liftRel ts (p x) f
libs/base/Decidable/Decidable.idr+3−22
@@ -1,6 +1,5 @@
1module Decidable.Decidable
1module Decidable.Decidable
2
2
3−import Data.VectFun -- FIXME let's see if this is needed
4import Data.Rel
3import Data.Rel
5
4
6%access public
5%access public
@@ -9,30 +8,12 @@ import Data.Rel
9-- Typeclass for decidable n-ary Relations
8-- Typeclass for decidable n-ary Relations
10--------------------------------------------------------------------------------
9--------------------------------------------------------------------------------
11
10
12−--DecProc : (ts : Vect k Type) -> (p : Rel ts) -> Type
13−--DecProc [] p = Dec p
14−--DecProc (t::ts) p = (x : t) -> DecProc ts (p x)
15−--DecProc : (ts : Vect k Type) -> (p : VectFun ts Type) -> Type
16−--DecProc [] p = Dec p
17−--DecProc (t::ts) p = (x : t) -> DecProc ts (p x)
18−
19−--class Decidable (ts : Vect k Type) (p : VectFun ts Type) where
20−-- total decide : DecProc ts p
21−--class Decidable (ts : Vect k Type) (p : Rel ts) where
22−-- total decide : DecProc ts p
23−--class Decidable (ts : Vect k Type) (p : VectFun ts Type) where
24−-- total decide : liftRel ts p Dec
25class Decidable (ts : Vect k Type) (p : Rel ts) where
11class Decidable (ts : Vect k Type) (p : Rel ts) where
26 total decide : liftRel ts p Dec
12 total decide : liftRel ts p Dec
27
13
28−{-
14+-- 'No such variable {k506}'
29−using (t : Type)
15+--decision : Decidable ts p => (ts : Vect k Type) -> (p : Rel ts) -> liftRel ts p Dec
30− class Rel (p : t) where
16+--decision ts p = decide {ts} {p}
31− total liftRel : (Type -> Type) -> Type
32−
33− class (Rel p) => Decidable (p : t) where
34− total decide : liftRel {p} Dec
35−-}
36
17
37using (P : Type, p : P)
18using (P : Type, p : P)
38 data Given : Dec P -> Type where
19 data Given : Dec P -> Type where
libs/base/Decidable/Order.idr−18
@@ -71,26 +71,8 @@ decideNatLTE x (S y) with (decEq x (S y))
71 | Yes nLTEm = Yes (nLTESm nLTEm)
71 | Yes nLTEm = Yes (nLTESm nLTEm)
72 | No nGTm = No (nGTSm nGTm)
72 | No nGTm = No (nGTSm nGTm)
73
73
74−{-
75−instance Rel NatLTE where
76− liftRel P = (n : Nat) -> (m : Nat) -> P (NatLTE n m)
77−
78−instance Decidable NatLTE where
79− decide = decideNatLTE
80−
81−lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
82−lte m n = decide {p = NatLTE} m n
83−-}
84−
85instance Decidable [Nat,Nat] NatLTE where
74instance Decidable [Nat,Nat] NatLTE where
86 decide = decideNatLTE
75 decide = decideNatLTE
87
76
88−--lte : DecProc [Nat,Nat] NatLTE
89−--lte m n = decide m n -- FIXME can this work?
90−--lte : liftRel [Nat,Nat] NatLTE Dec
91lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
77lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
92lte m n = decide {ts = [Nat,Nat]} {p = NatLTE} m n
78lte m n = decide {ts = [Nat,Nat]} {p = NatLTE} m n
93−--lte m n = decide {p = NatLTE} m n
94−--lte = decide
95−--lte m n = decide m n -- FIXME can this work?
96−--lte = decide -- FIXME can this work?