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.
commit1b511c7b8688d18d3c572f81f33f1a1eb3fe62f2 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateMon 20 Jan 2014, 00:34 (13 years ago) parent41925a6
3 files changed+3−45
compare with master
unifiedsplit
libs/base/Data/Rel.idr−5 libs/base/Decidable/Decidable.idr+3−22 libs/base/Decidable/Order.idr−18
libs/base/Data/Rel.idr−5
@@ -5,11 +5,6 @@ import Data.VectFun
55Rel : Vect n Type -> Type
66Rel ts = VectFun ts Type
77
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
138liftRel : (ts : Vect k Type) -> (p : Rel ts) -> (Type -> Type) -> Type
149liftRel [] p f = f p
1510liftRel (t :: ts) p f = (x : t) -> liftRel ts (p x) f
libs/base/Decidable/Decidable.idr+3−22
@@ -1,6 +1,5 @@
11module Decidable.Decidable
22
3−import Data.VectFun -- FIXME let's see if this is needed
43import Data.Rel
54
65%access public
@@ -9,30 +8,12 @@ import Data.Rel
98-- Typeclass for decidable n-ary Relations
109--------------------------------------------------------------------------------
1110
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
2511class Decidable (ts : Vect k Type) (p : Rel ts) where
2612 total decide : liftRel ts p Dec
2713
28−{-
29−using (t : Type)
30− class Rel (p : t) where
31− total liftRel : (Type -> Type) -> Type
32−
33− class (Rel p) => Decidable (p : t) where
34− total decide : liftRel {p} Dec
35−-}
14+-- 'No such variable {k506}'
15+--decision : Decidable ts p => (ts : Vect k Type) -> (p : Rel ts) -> liftRel ts p Dec
16+--decision ts p = decide {ts} {p}
3617
3718using (P : Type, p : P)
3819 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))
7171 | Yes nLTEm = Yes (nLTESm nLTEm)
7272 | No nGTm = No (nGTSm nGTm)
7373
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−
8574instance Decidable [Nat,Nat] NatLTE where
8675 decide = decideNatLTE
8776
88−--lte : DecProc [Nat,Nat] NatLTE
89−--lte m n = decide m n -- FIXME can this work?
90−--lte : liftRel [Nat,Nat] NatLTE Dec
9177lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
9278lte 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?