summaryrefslogtreecommitdiff
path: root/testdata/data.out
diff options
context:
space:
mode:
Diffstat (limited to 'testdata/data.out')
-rw-r--r--testdata/data.out84
1 files changed, 78 insertions, 6 deletions
diff --git a/testdata/data.out b/testdata/data.out
index bf9da023..498f6f32 100644
--- a/testdata/data.out
+++ b/testdata/data.out
@@ -1,19 +1,82 @@
1------------ desugared source code
2data Data0 :: Type where
3 Data0 :: Data0
4data Data1 (_ :: Type) (_ :: Type) (_ :: Type) :: Type where
5 Data1 :: _c -> _b -> _a -> Data1 _c _b _a
6data Data2 :: Type where
7 Data21 :: Int -> Data2
8 Data22 :: Int -> Int -> Data2
9 Data23 :: Int -> Data2
10 Data24 :: Data2
11x
12 = \(a :: _) -> 'Data2Case
13 \_ -> _ :: _
14 \_ -> _rhs undefined
15 \(b :: _) -> \_ -> _rhs b
16 \(c :: _) -> _rhs c
17 (_rhs undefined)
18 a
19y
20 = \(a :: _) -> 'Data2Case
21 \_ -> _ :: _
22 \_ -> _rhs undefined
23 \_ (b :: _) -> _rhs b
24 \_ -> _rhs undefined
25 (_rhs undefined)
26 a
27data Data5 (_ :: Type) (_ :: Type) (_ :: Type) :: Type where
28 Data51 :: _c -> Data5 _c _b _a
29 Data52 :: _c -> _b -> _a -> Data5 _c _b _a
30 Data53 :: Int -> _c -> Float -> _b -> _a -> Data5 _c _b _a
31a5
32 = \(a :: _) -> 'Data5Case
33 \_ -> _ :: _
34 \(b :: _) -> _rhs b
35 \(c :: _) -> \_ -> \_ -> _rhs c
36 \_ -> \_ -> \_ -> \_ -> \_ -> _rhs undefined
37 a
38b5
39 = \(a :: _) -> 'Data5Case
40 \_ -> _ :: _
41 \_ -> _rhs undefined
42 \_ (b :: _) -> \_ -> _rhs b
43 \_ -> \_ -> \_ -> \_ -> \_ -> _rhs undefined
44 a
45c5
46 = \(a :: _) -> 'Data5Case
47 \_ -> _ :: _
48 \_ -> _rhs undefined
49 \_ -> \_ (b :: _) -> _rhs b
50 \_ -> \_ -> \_ -> \_ -> \_ -> _rhs undefined
51 a
1main is not found 52main is not found
2------------ trace 53------------ trace
3'Data0 :: Type 54'Data0 :: Type
4Data0 :: Data0 55Data0 :: Data0
5'Data0Case :: forall (a :: Data0 -> Type) -> a 'Data0 -> forall (b :: Data0) -> a b 56'Data0Case
57 :: forall (a :: Data0 -> Type) -> a 'Data0 -> forall (b :: Data0) -> a b
6match'Data0 :: forall (a :: Type -> Type) -> a Data0 -> forall b -> a b -> a b 58match'Data0 :: forall (a :: Type -> Type) -> a Data0 -> forall b -> a b -> a b
7'Data1 :: Type -> Type -> Type -> Type 59'Data1 :: Type -> Type -> Type -> Type
8Data1 :: forall a b c . a -> b -> c -> Data1 a b c 60Data1 :: forall a b c . a -> b -> c -> Data1 a b c
9'Data1Case :: forall a b c . forall (d :: Data1 a b c -> Type) -> (forall (e :: a) (f :: b) (g :: c) -> d ('Data1 e f g)) -> forall (h :: Data1 a b c) -> d h 61'Data1Case
10match'Data1 :: forall (a :: Type -> Type) -> (forall b c d -> a (Data1 b c d)) -> forall e -> a e -> a e 62 :: forall a b c
63 . forall (d :: Data1 a b c -> Type)
64 -> (forall (e :: a) (f :: b) (g :: c) -> d ('Data1 e f g))
65 -> forall (h :: Data1 a b c) -> d h
66match'Data1
67 :: forall (a :: Type -> Type)
68 -> (forall b c d -> a (Data1 b c d)) -> forall e -> a e -> a e
11'Data2 :: Type 69'Data2 :: Type
12Data21 :: Int -> Data2 70Data21 :: Int -> Data2
13Data22 :: Int -> Int -> Data2 71Data22 :: Int -> Int -> Data2
14Data23 :: Int -> Data2 72Data23 :: Int -> Data2
15Data24 :: Data2 73Data24 :: Data2
16'Data2Case :: forall (a :: Data2 -> Type) -> (forall (b :: Int) -> a ('Data21 b)) -> (forall (c :: Int) (d :: Int) -> a ('Data22 c d)) -> (forall (e :: Int) -> a ('Data23 e)) -> a 'Data24 -> forall (f :: Data2) -> a f 74'Data2Case
75 :: forall (a :: Data2 -> Type)
76 -> (forall (b :: Int) -> a ('Data21 b))
77 -> (forall (c :: Int) (d :: Int) -> a ('Data22 c d))
78 -> (forall (e :: Int) -> a ('Data23 e))
79 -> a 'Data24 -> forall (f :: Data2) -> a f
17match'Data2 :: forall (a :: Type -> Type) -> a Data2 -> forall b -> a b -> a b 80match'Data2 :: forall (a :: Type -> Type) -> a Data2 -> forall b -> a b -> a b
18x :: Data2 -> Int 81x :: Data2 -> Int
19y :: Data2 -> Int 82y :: Data2 -> Int
@@ -21,8 +84,17 @@ y :: Data2 -> Int
21Data51 :: forall a b c . a -> Data5 a b c 84Data51 :: forall a b c . a -> Data5 a b c
22Data52 :: forall a b c . a -> b -> c -> Data5 a b c 85Data52 :: forall a b c . a -> b -> c -> Data5 a b c
23Data53 :: forall a b c . Int -> a -> Float -> b -> c -> Data5 a b c 86Data53 :: forall a b c . Int -> a -> Float -> b -> c -> Data5 a b c
24'Data5Case :: forall a b c . forall (d :: Data5 a b c -> Type) -> (forall (e :: a) -> d ('Data51 e)) -> (forall (f :: a) (g :: b) (h :: c) -> d ('Data52 f g h)) -> (forall (i :: Int) (j :: a) (k :: Float) (l :: b) (m :: c) -> d ('Data53 i j k l m)) -> forall (n :: Data5 a b c) -> d n 87'Data5Case
25match'Data5 :: forall (a :: Type -> Type) -> (forall b c d -> a (Data5 b c d)) -> forall e -> a e -> a e 88 :: forall a b c
89 . forall (d :: Data5 a b c -> Type)
90 -> (forall (e :: a) -> d ('Data51 e))
91 -> (forall (f :: a) (g :: b) (h :: c) -> d ('Data52 f g h))
92 -> (forall (i :: Int) (j :: a) (k :: Float) (l :: b) (m :: c)
93 -> d ('Data53 i j k l m))
94 -> forall (n :: Data5 a b c) -> d n
95match'Data5
96 :: forall (a :: Type -> Type)
97 -> (forall b c d -> a (Data5 b c d)) -> forall e -> a e -> a e
26a5 :: forall a b c . Data5 a b c -> a 98a5 :: forall a b c . Data5 a b c -> a
27b5 :: forall a b c . Data5 a b c -> b 99b5 :: forall a b c . Data5 a b c -> b
28c5 :: forall a b c . Data5 a b c -> c 100c5 :: forall a b c . Data5 a b c -> c
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-29 18:12:34 +0000