git.iko.soy/Idris-dev
on master help sign in
Added type functions for n-ary functions and relations, and modified things in Decidable to use them (based on Melvar's code). Comment regarding REPL instance resolution needed, as is some cleanup.
41925a6Timo Petteri Sinnemäki
libs/base/Data/Rel.idrnew file+15
compare with master
unifiedsplit
@@ -0,0 +1,15 @@
1+module Data.Rel
2+
3+import Data.VectFun
4+
5+Rel : Vect n Type -> Type
6+Rel ts = VectFun ts Type
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
13+liftRel : (ts : Vect k Type) -> (p : Rel ts) -> (Type -> Type) -> Type
14+liftRel [] p f = f p
15+liftRel (t :: ts) p f = (x : t) -> liftRel ts (p x) f
libs/base/Data/VectFun.idrnew file+5
@@ -0,0 +1,5 @@
1+module Data.VectFun
2+
3+VectFun : Vect n Type -> Type -> Type
4+VectFun [] r = r
5+VectFun (t::ts) r = t -> VectFun ts r
libs/base/Decidable/Decidable.idr+21
@@ -1,17 +1,38 @@
1module Decidable.Decidable
1module Decidable.Decidable
2
2
3+import Data.VectFun -- FIXME let's see if this is needed
4+import Data.Rel
5+
3%access public
6%access public
4
7
5--------------------------------------------------------------------------------
8--------------------------------------------------------------------------------
6-- Typeclass for decidable n-ary Relations
9-- Typeclass for decidable n-ary Relations
7--------------------------------------------------------------------------------
10--------------------------------------------------------------------------------
8
11
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
25+class Decidable (ts : Vect k Type) (p : Rel ts) where
26+ total decide : liftRel ts p Dec
27+
28+{-
9using (t : Type)
29using (t : Type)
10 class Rel (p : t) where
30 class Rel (p : t) where
11 total liftRel : (Type -> Type) -> Type
31 total liftRel : (Type -> Type) -> Type
12
32
13 class (Rel p) => Decidable (p : t) where
33 class (Rel p) => Decidable (p : t) where
14 total decide : liftRel {p} Dec
34 total decide : liftRel {p} Dec
35+-}
15
36
16using (P : Type, p : P)
37using (P : Type, p : P)
17 data Given : Dec P -> Type where
38 data Given : Dec P -> Type where
libs/base/Decidable/Order.idr+14
@@ -71,6 +71,7 @@ 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+{-
74instance Rel NatLTE where
75instance Rel NatLTE where
75 liftRel P = (n : Nat) -> (m : Nat) -> P (NatLTE n m)
76 liftRel P = (n : Nat) -> (m : Nat) -> P (NatLTE n m)
76
77
@@ -79,4 +80,17 @@ instance Decidable NatLTE where
79
80
80lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
81lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
81lte m n = decide {p = NatLTE} m n
82lte m n = decide {p = NatLTE} m n
83+-}
82
84
85+instance Decidable [Nat,Nat] NatLTE where
86+ decide = decideNatLTE
87+
88+--lte : DecProc [Nat,Nat] NatLTE
89+--lte m n = decide m n -- FIXME can this work?
90+--lte : liftRel [Nat,Nat] NatLTE Dec
91+lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
92+lte 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?