@@ -1,3 +1,11 @@
1+-- Everything here should type check but at some point in the past has
2+-- not.
3+
4+import Data.So
5+import Data.Vect
6+import Data.Fin
7+import Control.Isomorphism
8+
19class Functor f => VerifiedFunctor (f : Type -> Type) where
210 identity : (fa : f a) -> map id fa = fa
311
@@ -7,3 +15,165 @@ data Imp : Type where
715testVal : Imp
816testVal = MkImp (apply id Z)
917
18+zfin : Fin 1
19+zfin = 0
20+
21+data Infer = MkInf a
22+
23+foo : Infer
24+foo = MkInf (the (Fin 1) 0)
25+
26+isAnyBy : (alpha -> Bool) -> (n : Nat ** Vect n alpha) -> Bool
27+isAnyBy _ (_ ** Nil) = False
28+isAnyBy p (_ ** (a :: as)) = p a || isAnyBy p (_ ** as)
29+
30+filterTagP : (p : alpha -> Bool) ->
31+ (as : Vect n alpha) ->
32+ So (isAnyBy p (n ** as)) ->
33+ (m : Nat ** (Vect m (a : alpha ** So (p a)), So (m > Z)))
34+filterTagP {n = S m} p (a :: as) q with (p a)
35+ | True = (_
36+ **
37+ ((a ** believe_me Oh)
38+ ::
39+ (fst (getProof (filterTagP p as (believe_me Oh)))),
40+ Oh
41+ )
42+ )
43+ | False = filterTagP p as (believe_me Oh)
44+
45+vfoldl : (P : Nat -> Type) ->
46+ ((x : Nat) -> P x -> a -> P (S x)) -> P Z
47+ -> Vect m a -> P m
48+vfoldl P cons nil (x :: xs)
49+ = vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons Z nil x) xs
50+
51+
52+total soElim : (C : (b : Bool) -> So b -> Type) ->
53+ C True Oh ->
54+ (b : Bool) -> (s : So b) -> (C b s)
55+soElim C coh True Oh = coh
56+
57+soFalseElim : So False -> a
58+soFalseElim x = void (soElim C () False x)
59+ where
60+ C : (b : Bool) -> So b -> Type
61+ C True s = ()
62+ C False s = Void
63+
64+soTrue : So b -> b = True
65+soTrue {b = False} x = soFalseElim x
66+soTrue {b = True} x = Refl
67+
68+class Eq alpha => ReflEqEq alpha where
69+ reflexive_eqeq : (a : alpha) -> So (a == a)
70+
71+modifyFun : (Eq alpha) =>
72+ (alpha -> beta) ->
73+ (alpha, beta) ->
74+ (alpha -> beta)
75+modifyFun f (a, b) a' = if a' == a then b else f a'
76+
77+modifyFunLemma : (ReflEqEq alpha) =>
78+ (f : alpha -> beta) ->
79+ (ab : (alpha, beta)) ->
80+ modifyFun f ab (fst ab) = snd ab
81+modifyFunLemma f (a,b) =
82+ rewrite soTrue (reflexive_eqeq a) in Refl
83+
84+
85+Matrix : Type -> Nat -> Nat -> Type
86+Matrix a n m = Vect n (Vect m a)
87+
88+mytranspose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)
89+mytranspose ((x:: []) :: []) = [[x]]
90+mytranspose [x :: y :: xs] = [x] :: (mytranspose [y :: xs])
91+mytranspose (x :: y :: xs)
92+ = let tx = mytranspose [x] in
93+ let ux = mytranspose (y :: xs) in zipWith (++) tx ux
94+
95+using (A : Type, B : A->Type, C : Type)
96+ foo2 : ((x:A) -> B x -> C) -> ((x:A ** B x) -> C)
97+ foo2 f p = f (getWitness p) (getProof p)
98+
99+
100+m_add : Maybe (Either Bool Int) -> Maybe (Either Bool Int) ->
101+ Maybe (Either Bool Int)
102+m_add x y = do x' <- x -- Extract value from x
103+ y' <- y -- Extract value from y
104+ case x' of
105+ Left _ => Nothing
106+ Right _ => Nothing
107+
108+data Ty = TyBool
109+
110+data Id a = I a
111+
112+interpTy : Ty -> Type
113+interpTy TyBool = Id Bool
114+
115+data Term : Ty -> Type where
116+ TLit : Bool -> Term TyBool
117+ TNot : Term TyBool -> Term TyBool
118+
119+map : (a -> b) -> Id a -> Id b
120+map f (I x) = I (f x)
121+
122+interp : Term t -> interpTy t
123+interp (TLit x) = I x
124+interp (TNot x) = map not (interp x)
125+
126+data Result str a = Success str a | Failure String
127+
128+instance Functor (Result str) where
129+ map f (Success s x) = Success s (f x)
130+ map f (Failure e ) = Failure e
131+
132+ParserT : (Type -> Type) -> Type -> Type -> Type
133+ParserT m str a = str -> m (Result str a)
134+
135+ap : Monad m => ParserT m str (a -> b) -> ParserT m str a ->
136+ ParserT m str b
137+ap f x = \s => do f' <- f s
138+ case f' of
139+ Failure e => (pure (Failure e))
140+ Success s' g => x s' >>= pure . map g
141+
142+X : Nat -> Type
143+X t = (c : Nat ** So (c < 5))
144+
145+column : X t -> Nat
146+column = getWitness
147+
148+data Action = Left | Ahead | Right
149+
150+admissible : X t -> Action -> Bool
151+admissible {t} x Ahead = column {t} x == 0 || column {t} x == 4
152+admissible {t} x Left = column {t} x <= 2
153+admissible {t} x Right = column {t} x >= 2
154+
155+
156+class Set univ where
157+ member : univ -> univ -> Type
158+
159+isSubsetOf : Set univ => univ -> univ -> Type
160+isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)
161+
162+class Set univ => HasPower univ where
163+ Powerset : (a : univ) ->
164+ Sigma univ (\Pa => (c : univ) ->
165+ (isSubsetOf c a) -> member c Pa)
166+
167+powerset : HasPower univ => univ -> univ
168+powerset {univ} a = getWitness (Powerset a)
169+
170+mapFilter : (alpha -> beta) ->
171+ (alpha -> Bool) ->
172+ Vect n alpha ->
173+ (n : Nat ** Vect n beta)
174+mapFilter f p Nil = (_ ** Nil)
175+mapFilter f p (a :: as) with (p a)
176+ | True = (_ ** (f a) :: (getProof (mapFilter f p as)))
177+ | False = mapFilter f p as
178+
179+