← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to test/epic/tests/Forcing3.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
test/epic/tests/Forcing3.agda
1
 
module tests.Forcing3 where
2
 
 
3
 
open import Prelude.Nat
4
 
open import Prelude.IO
5
 
open import Prelude.Product
6
 
open import Prelude.Unit
7
 
 
8
 
data _**_ (A B : Set) : Set where
9
 
  _,_ : A -> B -> A ** B
10
 
 
11
 
data P {A B : Set} : A ** B -> Set where
12
 
  _,_ : (x : A)(y : B) -> P (x , y)
13
 
 
14
 
data Q {A : Set} : A ** A -> Set where
15
 
  [_] : (x : A) -> Q (x , x)
16
 
 
17
 
test : let t : Set
18
 
           t = (Nat ** Nat) ** Nat
19
 
         in (q : t ** t) -> Q q -> Nat
20
 
test ._   [ ( Z , Z )   , Z ]  = Z
21
 
test ._   [ ( Z , S l)  , m  ]  = S l + m
22
 
test ._   [ ( S Z , Z)  , m  ]  = S m
23
 
test ._   [ ( S Z , S l) , m ]  = S Z + m + l
24
 
test ._   [ ( S (S n) , l) , m ]  = S (S n) + m + l
25
 
test ._   [ ( n , l )  , m ]    = m
26
 
 
27
 
 
28
 
main : IO Unit
29
 
main = let tTyp : Set
30
 
           tTyp = (Nat ** Nat) ** Nat
31
 
           t0 : tTyp
32
 
           t0 = (0 , 0) , 0
33
 
           t1 : tTyp
34
 
           t1 = ( 0 , 1 ) , 2
35
 
           t2 : tTyp
36
 
           t2  = ( 1 , 0 ) , 3
37
 
           t3 : tTyp
38
 
           t3 = ( 1 , 4 ) , 5
39
 
           t4 : tTyp
40
 
           t4 = ( 3 , 2 ) , 10
41
 
           t5 : tTyp
42
 
           t5 = ( 0 , 0 ) , 4
43
 
           pn : tTyp -> IO Unit
44
 
           pn t = printNat (test (t , t) [ t ]) 
45
 
        in pn t0 ,, -- 0
46
 
           pn t1 ,, -- 3
47
 
           pn t2 ,, -- 4
48
 
           pn t3 ,, -- 9
49
 
           pn t4 ,, -- 15
50
 
           pn t5 ,, -- 4
51
 
           return unit
 
 
b'\\ No newline at end of file'