← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/Alonzo/Records.hs

  • 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:
examples/outdated-and-incorrect/Alonzo/Records.hs
1
 
{-# OPTIONS -fglasgow-exts #-}
2
 
 
3
 
 
4
 
module Records where
5
 
import RTS
6
 
import qualified RTP
7
 
import qualified Nat
8
 
import qualified Bool
9
 
name1 = "Point"
10
 
 
11
 
data T1 a b = C1 a b
12
 
d1 = ()
13
 
name2 = "x"
14
 
d2 = d2_1
15
 
  where d2_1 (Records.C1 v0 _) = cast v0
16
 
name3 = "y"
17
 
d3 = d3_1
18
 
  where d3_1 (Records.C1 _ v0) = cast v0
19
 
name4 = "Point'"
20
 
 
21
 
data T4 a b = C7 a b
22
 
d4 = ()
23
 
name7 = "mkPoint"
24
 
name8 = "origin"
25
 
d8 = d8_1
26
 
  where d8_1
27
 
          = cast
28
 
              (Records.C1 (cast (RTP._primIntToNat (0 :: Prelude.Int)))
29
 
                 (cast (RTP._primIntToNat (0 :: Prelude.Int))))
30
 
name9 = "origin'"
31
 
d9 = d9_1
32
 
  where d9_1
33
 
          = cast
34
 
              (Records.C7 (cast (RTP._primIntToNat (0 :: Prelude.Int)))
35
 
                 (cast (RTP._primIntToNat (0 :: Prelude.Int))))
36
 
name10 = "getX"
37
 
d10 = d10_1
38
 
  where d10_1 = cast Records.d2
39
 
name11 = "sum"
40
 
d11 = d11_1
41
 
  where d11_1 v0
42
 
          = cast
43
 
              (Nat.d4 (cast (Records.d16 (cast v0)))
44
 
                 (cast (Records.d17 (cast v0))))
45
 
name16 = "x"
46
 
d16 = d16_1
47
 
  where d16_1 v0 = cast (Records.d2 (cast v0))
48
 
name17 = "y"
49
 
d17 = d17_1
50
 
  where d17_1 v0 = cast (Records.d3 (cast v0))
51
 
name20 = "_==_"
52
 
 
53
 
data T20 = C23
54
 
d20 v2 v1 = ()
55
 
name23 = "refl"
56
 
name25 = "\951-Point"
57
 
d25 = d25_1
58
 
  where d25_1 _ = cast Records.C23
59
 
name27 = "True"
60
 
 
61
 
data T27 = C27
62
 
d27 = ()
63
 
name28 = "tt"
64
 
d28 = d28_1
65
 
  where d28_1 = cast Records.C27
66
 
name29 = "False"
67
 
 
68
 
data T29 = C29
69
 
d29 = ()
70
 
name30 = "NonZero"
71
 
d30 = d30_1
72
 
  where d30_1 (Nat.C2) = cast Records.d29
73
 
        d30_1 a = cast d30_2 a
74
 
        d30_2 (Nat.C3 _) = cast Records.d27
75
 
name34 = "_/_"
76
 
d34 = d34_1
77
 
  where d34_1 _ (Nat.C2) _ = undefined
78
 
        d34_1 a b c = cast d34_2 a b c
79
 
        d34_2 (Nat.C2) (Nat.C3 _) v0 = cast Nat.C2
80
 
        d34_2 a b c = cast d34_3 a b c
81
 
        d34_3 (Nat.C3 v0) (Nat.C3 v1) v2
82
 
          = cast
83
 
              (Records.d41 (cast v0) (cast v1) (cast v2)
84
 
                 (cast (Nat.C3 (cast v0)))
85
 
                 (cast (Nat.C3 (cast v1)))
86
 
                 (cast v1))
87
 
name41 = "div"
88
 
d41 = d41_1
89
 
  where d41_1 v0 v1 v2 (Nat.C2) (Nat.C2) _
90
 
          = cast (Nat.C3 (cast Nat.C2))
91
 
        d41_1 a b c d e f = cast d41_2 a b c d e f
92
 
        d41_2 v0 v1 v2 (Nat.C2) (Nat.C3 _) v3 = cast Nat.C2
93
 
        d41_2 a b c d e f = cast d41_3 a b c d e f
94
 
        d41_3 v0 v1 v2 (Nat.C3 v3) (Nat.C2) v4
95
 
          = cast
96
 
              (Nat.C3
97
 
                 (cast
98
 
                    (Records.d41 (cast v0) (cast v1) (cast v2) (cast v3) (cast v4)
99
 
                       (cast v4))))
100
 
        d41_3 a b c d e f = cast d41_4 a b c d e f
101
 
        d41_4 v0 v1 v2 (Nat.C3 v3) (Nat.C3 v4) v5
102
 
          = cast
103
 
              (Records.d41 (cast v0) (cast v1) (cast v2) (cast v3) (cast v4)
104
 
                 (cast v5))
105
 
name50 = "five"
106
 
d50 = d50_1
107
 
  where d50_1
108
 
          = cast
109
 
              (Records.d34 (cast (RTP._primIntToNat (17 :: Prelude.Int)))
110
 
                 (cast (RTP._primIntToNat (3 :: Prelude.Int)))
111
 
                 (cast Records.C27))
112
 
name53 = "\8707"
113
 
 
114
 
data T53 a b = C53 a b
115
 
d53 = ()
116
 
name56 = "witness"
117
 
d56 = d56_1
118
 
  where d56_1 _ _ (Records.C53 v0 _) = cast v0
119
 
name57 = "proof"
120
 
d57 = d57_1
121
 
  where d57_1 _ _ (Records.C53 _ v0) = cast v0