git.iko.soy/Idris-dev
on master help sign in
Add test, create the DepPair typeclass.
f13c6adMatus Tejiscak
idris.cabal+3
compare with master
unifiedsplit
@@ -270,6 +270,9 @@ Extra-source-files:
270 test/basic009/*.idr
270 test/basic009/*.idr
271 test/basic009/expected
271 test/basic009/expected
272 test/basic009/B/*.idr
272 test/basic009/B/*.idr
273+ test/basic010/run
274+ test/basic010/*.idr
275+ test/basic010/expected
273
276
274 test/buffer001-disabled/*.idr
277 test/buffer001-disabled/*.idr
275 test/buffer001-disabled/run
278 test/buffer001-disabled/run
libs/prelude/Builtins.idr−8
@@ -9,14 +9,6 @@
9data Pair : (a : Type) -> (P : a -> Type) -> Type where
9data Pair : (a : Type) -> (P : a -> Type) -> Type where
10 pair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Pair a P
10 pair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Pair a P
11
11
12−||| The first projection from a dependent pair
13−getWitness : {P : a -> Type} -> Pair a P -> a
14−getWitness (a ** v) = a
15−
16−||| The second projection from a dependent pair
17−getProof : {P : a -> Type} -> (s : Pair a P) -> P (getWitness s)
18−getProof (a ** v) = v
19−
20||| The eliminator for the empty type.
12||| The eliminator for the empty type.
21FalseElim : _|_ -> a
13FalseElim : _|_ -> a
22
14
libs/prelude/Prelude/Pairs.idr+31−6
@@ -1,12 +1,37 @@
1module Prelude.Pairs
1module Prelude.Pairs
2
2
3+import Builtins
4+
3%access public
5%access public
4%default total
6%default total
5
7
8+using (a : Type, P : a -> Type)
9+
6−||| Dependent pair where the first field is erased.
10+ ||| Dependent pair where the first field is erased.
11+ data Exists : (P : a -> Type) -> Type where
12+ evidence : .{x : a} -> (pf : P x) -> Exists P
13+
14+ ||| Dependent pair where the second field is erased.
7−data Exists : {a : Type} -> (P : a -> Type) -> Type where
15+ data Subset : (a : Type) -> (P : a -> Type) -> Type where
8− witness : .{P : a -> Type} -> .{x : a} -> (pf : P x) -> Exists P
16+ element : (x : a) -> .(pf : P x) -> Subset a P
17+
18+ ||| The type class of dependent pairs.
19+ class DepPair (a : Type) (P : a -> Type) (T : Type) where
20+
21+ ||| The first projection from a dependent pair.
22+ getWitness : (x : T) -> a
23+
24+ ||| The second projection from a dependent pair.
25+ getProof : (x : T) -> P (getWitness x)
26+
27+ instance DepPair a P (Exists {a} P) where
28+ getWitness (evidence {x=x} pf) = x
29+ getProof (evidence {x=x} pf) = pf
30+
31+ instance DepPair a P (Subset a P) where
32+ getWitness (element x pf) = x
33+ getProof (element x pf) = pf
9
34
10−||| Dependent pair where the second field is erased.
35+ instance DepPair a P (Pair a P) where
11−data Subset : (a : Type) -> (P : a -> Type) -> Type where
36+ getWitness (pair x pf) = x
12− element : .{P : a -> Type} -> (x : a) -> .(pf : P x) -> Subset a P
37+ getProof (pair x pf) = pf
test/basic010/Main.idrnew file+12
@@ -0,0 +1,12 @@
1+module Main
2+
3+qib : Nat -> Nat
4+qib Z = 1
5+qib (S Z) = 1
6+qib (S (S n)) = qib n * qib (S n)
7+
8+f : (n : Nat) -> Exists (\k => qib n = k)
9+f n = witness (qib n) refl
10+
11+main : IO ()
12+main = print "hello world"
test/basic010/expectednew file+5
@@ -0,0 +1,5 @@
1+MAIN-PASS
2+Faulty.idr:6:7:When elaborating type of Faulty.fault:
3+When elaborating an application of type constructor =:
4+ Can't disambiguate name: A.num, B.C.num
5+Multiple.idr:3:1:import alias not unique: "X"
test/basic010/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ Main.idr --nocolour --check --warnreach -o basic010
3+./basic010
4+rm -f *.ibc basic010