git.iko.soy/Idris-dev
on master help sign in
Merge pull request #789 from tpsinnem/master
858b6edEdwin Brady
libs/base/Data/Fun.idrnew file+8
compare with master
unifiedsplit
@@ -0,0 +1,8 @@
1+module Data.Fun
2+
3+--------------------------------------------------------------------------------
4+-- Build an n-ary function type from a Vect of Types and a result type
5+--------------------------------------------------------------------------------
6+Fun : Vect n Type -> Type -> Type
7+Fun [] r = r
8+Fun (t::ts) r = t -> Fun ts r
libs/base/Data/Rel.idrnew file+13
@@ -0,0 +1,13 @@
1+module Data.Rel
2+
3+import Data.Fun
4+
5+--------------------------------------------------------------------------------
6+-- Build an n-ary relation type from a Vect of Types
7+--------------------------------------------------------------------------------
8+Rel : Vect n Type -> Type
9+Rel ts = Fun ts Type
10+
11+liftRel : (ts : Vect n Type) -> (p : Rel ts) -> (Type -> Type) -> Type
12+liftRel [] p f = f p
13+liftRel (t :: ts) p f = (x : t) -> liftRel ts (p x) f
libs/base/Decidable/Decidable.idr+9−5
@@ -1,17 +1,21 @@
1module Decidable.Decidable
1module Decidable.Decidable
2
2
3+import Data.Rel
4+
3%access public
5%access public
4
6
5--------------------------------------------------------------------------------
7--------------------------------------------------------------------------------
6-- Typeclass for decidable n-ary Relations
8-- Typeclass for decidable n-ary Relations
7--------------------------------------------------------------------------------
9--------------------------------------------------------------------------------
8
10
9−using (t : Type)
11+-- Note: Instance resolution for Decidable is likely to not work in the REPL
12+-- at the moment.
10− class Rel (p : t) where
13+class Decidable (ts : Vect k Type) (p : Rel ts) where
11− total liftRel : (Type -> Type) -> Type
14+ total decide : liftRel ts p Dec
12
15
13− class (Rel p) => Decidable (p : t) where
16+-- 'No such variable {k506}'
14− total decide : liftRel {p} Dec
17+--decision : Decidable ts p => (ts : Vect k Type) -> (p : Rel ts) -> liftRel ts p Dec
18+--decision ts p = decide {ts} {p}
15
19
16using (P : Type, p : P)
20using (P : Type, p : P)
17 data Given : Dec P -> Type where
21 data Given : Dec P -> Type where
libs/base/Decidable/Order.idr+2−6
@@ -71,12 +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−instance Rel NatLTE where
75− liftRel P = (n : Nat) -> (m : Nat) -> P (NatLTE n m)
76−
77−instance Decidable NatLTE where
74+instance Decidable [Nat,Nat] NatLTE where
78 decide = decideNatLTE
75 decide = decideNatLTE
79
76
80lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
77lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
81−lte m n = decide {p = NatLTE} m n
78+lte m n = decide {ts = [Nat,Nat]} {p = NatLTE} m n
82−
libs/base/base.ipkg+2−1
@@ -23,7 +23,8 @@ modules = System,
23 Data.ZZ, Data.Sign,
23 Data.ZZ, Data.Sign,
24 Data.SortedMap, Data.SortedSet, Data.BoundedList,
24 Data.SortedMap, Data.SortedSet, Data.BoundedList,
25 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
25 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
26− Data.Floats, Data.Complex, Data.Heap,
26+ Data.Floats, Data.Complex, Data.Heap, Data.Fun,
27+ Data.Rel,
27
28
28 Control.Isomorphism,
29 Control.Isomorphism,
29 Control.Monad.Identity,
30 Control.Monad.Identity,