git.iko.soy/Idris-dev
on master help sign in
Add another interface test
57719e8Edwin Brady
test/interfaces005/expectednew file+7
compare with master
unifiedsplit
@@ -0,0 +1,7 @@
1+interfaces005a.idr:18:3:
2+Set.TreeSet.Set must be defined by a type or data constructor
3+No such variable TreeSet
4+interfaces005b.idr:4:11:
5+Data definitions not allowed in a class declaration
6+interfaces005b.idr:18:3:SetSig is not an interface
7+No such variable TreeSet
test/interfaces005/interfaces005.idrnew file+50
@@ -0,0 +1,50 @@
1+module Set
2+
3+public export
4+interface SetSig a where
5+ data Set : Type -> Type
6+
7+ new : Set a
8+ insert : a -> Set a -> Set a
9+ member : a -> Set a -> Bool
10+
11+data Tree a = Leaf | Node (Tree a) a (Tree a)
12+
13+mkTree : Type -> Type
14+mkTree = Tree
15+
16+namespace TreeSet
17+ export
18+ [TreeSet] Ord a => SetSig a where
19+
20+ Set = Tree
21+
22+ new = Leaf
23+
24+ insert x Leaf = Node Leaf x Leaf
25+ insert x (Node l val r) = case compare x val of
26+ LT => Node (insert x l) val r
27+ EQ => Node l val r
28+ GT => Node l val (insert x r)
29+
30+ member x Leaf = False
31+ member x (Node l val r) = case compare x val of
32+ LT => member x l
33+ EQ => True
34+ GT => member x r
35+
36+using implementation TreeSet
37+
38+ test : Set @{TreeSet {a=Nat}} Nat
39+ test = insert 3 $
40+ insert 2 $
41+ insert 7 $
42+ insert 3 $
43+ insert 4 $
44+ insert 5 new
45+
46+ foo : Bool
47+ foo = member 6 test
48+
49+ bar : Bool
50+ bar = member 3 test
test/interfaces005/interfaces005a.idrnew file+50
@@ -0,0 +1,50 @@
1+module Set
2+
3+public export
4+interface SetSig a where
5+ data Set : Type -> Type
6+
7+ new : Set a
8+ insert : a -> Set a -> Set a
9+ member : a -> Set a -> Bool
10+
11+data Tree a = Leaf | Node (Tree a) a (Tree a)
12+
13+mkTree : Type -> Type
14+mkTree = Tree
15+
16+namespace TreeSet
17+ export
18+ [TreeSet] Ord a => SetSig a where
19+
20+ Set = mkTree
21+
22+ new = Leaf
23+
24+ insert x Leaf = Node Leaf x Leaf
25+ insert x (Node l val r) = case compare x val of
26+ LT => Node (insert x l) val r
27+ EQ => Node l val r
28+ GT => Node l val (insert x r)
29+
30+ member x Leaf = False
31+ member x (Node l val r) = case compare x val of
32+ LT => member x l
33+ EQ => True
34+ GT => member x r
35+
36+using implementation TreeSet
37+
38+ test : Set @{TreeSet {a=Nat}} Nat
39+ test = insert 3 $
40+ insert 2 $
41+ insert 7 $
42+ insert 3 $
43+ insert 4 $
44+ insert 5 new
45+
46+ foo : Bool
47+ foo = member 6 test
48+
49+ bar : Bool
50+ bar = member 3 test
test/interfaces005/interfaces005b.idrnew file+50
@@ -0,0 +1,50 @@
1+module Set
2+
3+public export
4+interface SetSig a where
5+ data Set : Type -> Type where MkSet : List a -> Set a
6+
7+ new : Set a
8+ insert : a -> Set a -> Set a
9+ member : a -> Set a -> Bool
10+
11+data Tree a = Leaf | Node (Tree a) a (Tree a)
12+
13+mkTree : Type -> Type
14+mkTree = Tree
15+
16+namespace TreeSet
17+ export
18+ [TreeSet] Ord a => SetSig a where
19+
20+ Set = Tree
21+
22+ new = Leaf
23+
24+ insert x Leaf = Node Leaf x Leaf
25+ insert x (Node l val r) = case compare x val of
26+ LT => Node (insert x l) val r
27+ EQ => Node l val r
28+ GT => Node l val (insert x r)
29+
30+ member x Leaf = False
31+ member x (Node l val r) = case compare x val of
32+ LT => member x l
33+ EQ => True
34+ GT => member x r
35+
36+using implementation TreeSet
37+
38+ test : Set @{TreeSet {a=Nat}} Nat
39+ test = insert 3 $
40+ insert 2 $
41+ insert 7 $
42+ insert 3 $
43+ insert 4 $
44+ insert 5 new
45+
46+ foo : Bool
47+ foo = member 6 test
48+
49+ bar : Bool
50+ bar = member 3 test
test/interfaces005/runnew file+5
@@ -0,0 +1,5 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces005.idr --check
3+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces005a.idr --check
4+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces005b.idr --check
5+rm -rf *.ibc