git.iko.soy/Idris-dev
on master help sign in
Add type-directed HVect functions and supporting Elem functions
c5979f4Melvar Chen
lib/Data/HVect.idr+14
compare with master
unifiedsplit
@@ -1,5 +1,7 @@
1module Data.HVect
1module Data.HVect
2
2
3+import Data.Vect
4+
3using (k : Nat, ts : Vect Type k)
5using (k : Nat, ts : Vect Type k)
4 data HVect : Vect Type k -> Type where
6 data HVect : Vect Type k -> Type where
5 Nil : HVect []
7 Nil : HVect []
@@ -44,3 +46,15 @@ using (k : Nat, ts : Vect Type k)
44 instance (Shows k ts) => Show (HVect ts) where
46 instance (Shows k ts) => Show (HVect ts) where
45 show xs = show (shows xs)
47 show xs = show (shows xs)
46
48
49+ get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
50+ get {p = Here} (x::xs) = x
51+ get {p = There p'} (x::xs) = get {p = p'} xs
52+
53+ put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
54+ put {p = Here} y (x::xs) = y :: xs
55+ put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
56+
57+ update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
58+ update {p = Here} f (x::xs) = f x :: xs
59+ update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
60+
lib/Data/Vect.idrnew file+29
@@ -0,0 +1,29 @@
1+module Data.Vect
2+
3+import Language.Reflection
4+
5+--------------------------------------------------------------------------------
6+-- Elem
7+--------------------------------------------------------------------------------
8+
9+data Elem : a -> Vect a k -> Type where
10+ Here : {xs : Vect a k} -> Elem x (x::xs)
11+ There : {xs : Vect a k} -> Elem x xs -> Elem x (y::xs)
12+
13+findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic
14+findElem O ctxt goal = Refine "Here" `Seq` Solve
15+findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
16+
17+replaceElem : (xs : Vect t k) -> Elem x xs -> (y : t) -> (ys : Vect t k ** Elem y ys)
18+replaceElem (x::xs) Here y = (y :: xs ** Here)
19+replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)
20+ | (ys ** yinys) = (x :: ys ** There yinys)
21+
22+replaceByElem : (xs : Vect t k) -> Elem x xs -> t -> Vect t k
23+replaceByElem (x::xs) Here y = y :: xs
24+replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y
25+
26+mapElem : {xs : Vect t k} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)
27+mapElem Here = Here
28+mapElem (There e) = There (mapElem e)
29+
lib/base.ipkg+1−1
@@ -25,7 +25,7 @@ modules = Builtins, Prelude, IO, System,
25 Data.Bits, Data.Mod2,
25 Data.Bits, Data.Mod2,
26 Data.Z, Data.Sign,
26 Data.Z, Data.Sign,
27 Data.SortedMap, Data.SortedSet, Data.BoundedList,
27 Data.SortedMap, Data.SortedSet, Data.BoundedList,
28− Data.HVect, Data.Vect.Quantifiers,
28+ Data.Vect, Data.HVect, Data.Vect.Quantifiers,
29
29
30 Control.Monad.Identity, Control.Monad.State, Control.Category,
30 Control.Monad.Identity, Control.Monad.State, Control.Category,
31 Control.Arrow,
31 Control.Arrow,