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.
commit41925a6c66c72b1c0c746bf5c13ae9835acc7a89 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateSun 19 Jan 2014, 22:03 (13 years ago) parent10c257b
4 files changed+55
compare with master
unifiedsplit
libs/base/Data/Rel.idr+15 libs/base/Data/VectFun.idr+5 libs/base/Decidable/Decidable.idr+21 libs/base/Decidable/Order.idr+14
libs/base/Data/Rel.idrnew file+15
@@ -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 @@
11module Decidable.Decidable
22
3+import Data.VectFun -- FIXME let's see if this is needed
4+import Data.Rel
5+
36%access public
47
58--------------------------------------------------------------------------------
69-- Typeclass for decidable n-ary Relations
710--------------------------------------------------------------------------------
811
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+{-
929using (t : Type)
1030 class Rel (p : t) where
1131 total liftRel : (Type -> Type) -> Type
1232
1333 class (Rel p) => Decidable (p : t) where
1434 total decide : liftRel {p} Dec
35+-}
1536
1637using (P : Type, p : P)
1738 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))
7171 | Yes nLTEm = Yes (nLTESm nLTEm)
7272 | No nGTm = No (nGTSm nGTm)
7373
74+{-
7475instance Rel NatLTE where
7576 liftRel P = (n : Nat) -> (m : Nat) -> P (NatLTE n m)
7677
@@ -79,4 +80,17 @@ instance Decidable NatLTE where
7980
8081lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
8182lte m n = decide {p = NatLTE} m n
83+-}
8284
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?