summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPéter Diviánszky <divipp@gmail.com>2016-02-07 00:39:18 +0100
committerPéter Diviánszky <divipp@gmail.com>2016-02-07 21:36:23 +0100
commit6e291f28363cc873b809e020eef8a929c8244508 (patch)
tree0f8ec4da631da1025a2cef1023b92bd48313a17d
parent8e39dd5fae759b9aa70afd4bab55d8c53b13c0ef (diff)
try again to move injectivity checking into the libraries
Diffstat
-rw-r--r--lc/Internals.lc10
-rw-r--r--src/LambdaCube/Compiler/Infer.hs11
-rw-r--r--src/LambdaCube/Compiler/Parser.hs4
-rw-r--r--testdata/Internals.out542
4 files changed, 301 insertions, 266 deletions
diff --git a/lc/Internals.lc b/lc/Internals.lc
index e0639717..15d1a38e 100644
--- a/lc/Internals.lc
+++ b/lc/Internals.lc
@@ -37,12 +37,18 @@ type family JoinTupleType t1 t2 where
37-- conjuction of constraints 37-- conjuction of constraints
38type family T2 a b 38type family T2 a b
39 39
40match'Type :: forall (m :: Type -> Type) -> m Type -> forall (t :: Type) -> m t -> m t
41
42--testmt :: forall (t :: Type) -> t -> t
43--testmt 'Type = \'Tuple0 -> 'Tuple0
44
40-- equality constraints 45-- equality constraints
41type family EqCT (t :: Type) (a :: t) (b :: t) 46type family EqCT (t :: Type) (a :: t) (b :: t)
42 47
43type EqCTt = EqCT Type 48--type instance EqCT Type Type Type = Unit--(a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b')
49--type instance EqCT Type (a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b')
44 50
45--type instance EqCT t (a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b') 51type EqCTt = EqCT Type
46 52
47-- builtin conjuction of constraint witnesses 53-- builtin conjuction of constraint witnesses
48t2C :: Unit -> Unit -> Unit 54t2C :: Unit -> Unit -> Unit
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 21ffe022..fb418227 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -450,7 +450,9 @@ evalCaseFun a b x = error $ "evalCaseFun: " ++ show (a, x)
450 450
451evalTyCaseFun a b (Neut c) = TyCaseFun a b c 451evalTyCaseFun a b (Neut c) = TyCaseFun a b c
452evalTyCaseFun a b (FixLabel _ c) = evalTyCaseFun a b c 452evalTyCaseFun a b (FixLabel _ c) = evalTyCaseFun a b c
453evalTyCaseFun (TyCaseFunName "match'Type" ty) [_, t, f] TType = t
453evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (TyCon (TyConName n' _ _ _ _ _) vs) | n == n' = foldl app_ t vs 454evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (TyCon (TyConName n' _ _ _ _ _) vs) | n == n' = foldl app_ t vs
455evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (Fun (FunName n' _ _) vs) | n == n' = foldl app_ t vs -- hack
454evalTyCaseFun (TyCaseFunName n ty) [_, t, f] _ = f 456evalTyCaseFun (TyCaseFunName n ty) [_, t, f] _ = f
455 457
456evalCoe a b TT d = d 458evalCoe a b TT d = d
@@ -1108,6 +1110,15 @@ handleStmt defs = \case
1108 (x, t) <- inferTerm (snd n) tr id $ trSExp' $ if usedS n t__ then SBuiltin "primFix" `SAppV` SLamV (substSG0 n t__) else t__ 1110 (x, t) <- inferTerm (snd n) tr id $ trSExp' $ if usedS n t__ then SBuiltin "primFix" `SAppV` SLamV (substSG0 n t__) else t__
1109 tellStmtType (fst n) t 1111 tellStmtType (fst n) t
1110 addToEnv n (mkELet (True, n, SData mf, ar) x t, t) 1112 addToEnv n (mkELet (True, n, SData mf, ar) x t, t)
1113 -- hack
1114 when (snd (getParams t) == TType) $ do
1115 let ps' = fst $ getParams t
1116 t'' = (TType :~> TType)
1117 :~> addParams ps' (Var (length ps') `app_` Fun (FunName (snd n) mf t) (downTo 0 $ length ps'))
1118 :~> TType
1119 :~> Var 2 `app_` Var 0
1120 :~> Var 3 `app_` Var 1
1121 addToEnv (fst n, MatchName (snd n)) (lamify t'' $ \[m, tr, n', f] -> evalTyCaseFun (TyCaseFunName (snd n) t) [m, tr, f] n', t'')
1111 PrecDef{} -> return () 1122 PrecDef{} -> return ()
1112 Data s (map (second trSExp') -> ps) (trSExp' -> t_) addfa (map (second trSExp') -> cs) -> do 1123 Data s (map (second trSExp') -> ps) (trSExp' -> t_) addfa (map (second trSExp') -> cs) -> do
1113 exs <- asks fst 1124 exs <- asks fst
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index b1e149b1..b6a7a898 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -984,7 +984,9 @@ mkDesugarInfo ss =
984 ( Map.fromList $ ("'EqCTt", (Infix, -1)): [(s, f) | PrecDef (_, s) f <- ss] 984 ( Map.fromList $ ("'EqCTt", (Infix, -1)): [(s, f) | PrecDef (_, s) f <- ss]
985 , Map.fromList $ 985 , Map.fromList $
986 [(cn, Left ((t, pars ty), (snd *** pars) <$> cs)) | Data (_, t) ps ty _ cs <- ss, ((_, cn), ct) <- cs] 986 [(cn, Left ((t, pars ty), (snd *** pars) <$> cs)) | Data (_, t) ps ty _ cs <- ss, ((_, cn), ct) <- cs]
987 ++ [(t, Right $ pars $ addParamsS ps ty) | Data (_, t) ps ty _ cs <- ss] 987 ++ [(t, Right $ pars $ addParamsS ps ty) | Data (_, t) ps ty _ _ <- ss]
988-- ++ [(t, Right $ length xs) | Let (_, t) _ (Just ty) xs _ <- ss]
989 ++ [("'Type", Right 0)]
988 ) 990 )
989 where 991 where
990 pars ty = length $ filter ((== Visible) . fst) $ fst $ getParamsS ty -- todo 992 pars ty = length $ filter ((== Visible) . fst) $ fst $ getParamsS ty -- todo
diff --git a/testdata/Internals.out b/testdata/Internals.out
index c34e2a0a..91254a8e 100644
--- a/testdata/Internals.out
+++ b/testdata/Internals.out
@@ -98,271 +98,287 @@ testdata/Internals.lc 35:25-35:31 Type
98testdata/Internals.lc 35:26-35:27 Type 98testdata/Internals.lc 35:26-35:27 Type
99testdata/Internals.lc 35:29-35:30 Type 99testdata/Internals.lc 35:29-35:30 Type
100testdata/Internals.lc 38:13-38:15 Type -> Type->Type 100testdata/Internals.lc 38:13-38:15 Type -> Type->Type
101testdata/Internals.lc 41:13-41:17 a:Type -> a -> a->Type 101testdata/Internals.lc 40:1-40:11 (b : Type->Type) -> b Type -> d:Type -> b d -> b d
102testdata/Internals.lc 41:24-41:28 Type 102testdata/Internals.lc 40:28-40:32 Type
103testdata/Internals.lc 41:36-41:37 Type 103testdata/Internals.lc 40:36-40:40 Type
104testdata/Internals.lc 41:36-41:46 Type 104testdata/Internals.lc 40:45-40:46 Type->Type
105testdata/Internals.lc 41:45-41:46 Type 105testdata/Internals.lc 40:45-40:51 Type
106testdata/Internals.lc 43:6-43:11 Type -> Type->Type 106testdata/Internals.lc 40:45-40:87 Type
107testdata/Internals.lc 43:14-43:18 a:Type -> a -> a->Type 107testdata/Internals.lc 40:47-40:51 Type
108testdata/Internals.lc 43:14-43:23 Type -> Type->Type 108testdata/Internals.lc 40:55-40:87 Type
109testdata/Internals.lc 43:19-43:23 Type 109testdata/Internals.lc 40:68-40:72 Type
110testdata/Internals.lc 48:1-48:4 Unit -> Unit->Unit 110testdata/Internals.lc 40:77-40:78 Type->Type
111testdata/Internals.lc 48:8-48:12 Type 111testdata/Internals.lc 40:77-40:80 Type
112testdata/Internals.lc 48:16-48:20 Type 112testdata/Internals.lc 40:77-40:87 Type
113testdata/Internals.lc 48:16-48:28 Type 113testdata/Internals.lc 40:79-40:80 Type
114testdata/Internals.lc 48:24-48:28 Type 114testdata/Internals.lc 40:84-40:85 Type->Type
115testdata/Internals.lc 51:6-51:9 Type 115testdata/Internals.lc 40:84-40:87 Type
116testdata/Internals.lc 52:6-52:10 Type 116testdata/Internals.lc 40:86-40:87 Type
117testdata/Internals.lc 53:6-53:11 Type 117testdata/Internals.lc 46:13-46:17 a:Type -> a -> a->Type
118testdata/Internals.lc 54:6-54:10 Type 118testdata/Internals.lc 46:24-46:28 Type
119testdata/Internals.lc 56:6-56:10 Type 119testdata/Internals.lc 46:36-46:37 Type
120testdata/Internals.lc 56:6-56:25 Type 120testdata/Internals.lc 46:36-46:46 Type
121testdata/Internals.lc 56:13-56:18 Bool 121testdata/Internals.lc 46:45-46:46 Type
122testdata/Internals.lc 56:21-56:25 Bool 122testdata/Internals.lc 51:6-51:11 Type -> Type->Type
123testdata/Internals.lc 58:6-58:14 Type 123testdata/Internals.lc 51:14-51:18 a:Type -> a -> a->Type
124testdata/Internals.lc 58:6-58:29 Type 124testdata/Internals.lc 51:14-51:23 Type -> Type->Type
125testdata/Internals.lc 58:17-58:19 Ordering 125testdata/Internals.lc 51:19-51:23 Type
126testdata/Internals.lc 58:22-58:24 Ordering 126testdata/Internals.lc 54:1-54:4 Unit -> Unit->Unit
127testdata/Internals.lc 58:27-58:29 Ordering 127testdata/Internals.lc 54:8-54:12 Type
128testdata/Internals.lc 60:6-60:9 Type 128testdata/Internals.lc 54:16-54:20 Type
129testdata/Internals.lc 60:6-60:23 Type 129testdata/Internals.lc 54:16-54:28 Type
130testdata/Internals.lc 60:12-60:16 Nat 130testdata/Internals.lc 54:24-54:28 Type
131testdata/Internals.lc 60:19-60:23 Nat | Nat->Nat | Type 131testdata/Internals.lc 57:6-57:9 Type
132testdata/Internals.lc 60:24-60:27 Type 132testdata/Internals.lc 58:6-58:10 Type
133testdata/Internals.lc 63:1-63:14 Int->Word 133testdata/Internals.lc 59:6-59:11 Type
134testdata/Internals.lc 63:24-63:27 Type 134testdata/Internals.lc 60:6-60:10 Type
135testdata/Internals.lc 63:33-63:37 Type 135testdata/Internals.lc 62:6-62:10 Type
136testdata/Internals.lc 64:1-64:15 Int->Float 136testdata/Internals.lc 62:6-62:25 Type
137testdata/Internals.lc 64:24-64:27 Type 137testdata/Internals.lc 62:13-62:18 Bool
138testdata/Internals.lc 64:33-64:38 Type 138testdata/Internals.lc 62:21-62:25 Bool
139testdata/Internals.lc 65:1-65:13 Int->Nat 139testdata/Internals.lc 64:6-64:14 Type
140testdata/Internals.lc 65:24-65:27 Type 140testdata/Internals.lc 64:6-64:29 Type
141testdata/Internals.lc 65:33-65:36 Type 141testdata/Internals.lc 64:17-64:19 Ordering
142testdata/Internals.lc 66:1-66:15 Int -> Int->Ordering 142testdata/Internals.lc 64:22-64:24 Ordering
143testdata/Internals.lc 64:27-64:29 Ordering
144testdata/Internals.lc 66:6-66:9 Type
145testdata/Internals.lc 66:6-66:23 Type
146testdata/Internals.lc 66:12-66:16 Nat
147testdata/Internals.lc 66:19-66:23 Nat | Nat->Nat | Type
143testdata/Internals.lc 66:24-66:27 Type 148testdata/Internals.lc 66:24-66:27 Type
144testdata/Internals.lc 66:33-66:36 Type 149testdata/Internals.lc 69:1-69:14 Int->Word
145testdata/Internals.lc 66:33-66:50 Type 150testdata/Internals.lc 69:24-69:27 Type
146testdata/Internals.lc 66:42-66:50 Type
147testdata/Internals.lc 67:1-67:16 Word -> Word->Ordering
148testdata/Internals.lc 67:24-67:28 Type
149testdata/Internals.lc 67:33-67:37 Type
150testdata/Internals.lc 67:33-67:50 Type
151testdata/Internals.lc 67:42-67:50 Type
152testdata/Internals.lc 68:1-68:17 Float -> Float->Ordering
153testdata/Internals.lc 68:24-68:29 Type
154testdata/Internals.lc 68:33-68:38 Type
155testdata/Internals.lc 68:33-68:50 Type
156testdata/Internals.lc 68:42-68:50 Type
157testdata/Internals.lc 69:1-69:16 Char -> Char->Ordering
158testdata/Internals.lc 69:24-69:28 Type
159testdata/Internals.lc 69:33-69:37 Type 151testdata/Internals.lc 69:33-69:37 Type
160testdata/Internals.lc 69:33-69:50 Type 152testdata/Internals.lc 70:1-70:15 Int->Float
161testdata/Internals.lc 69:42-69:50 Type 153testdata/Internals.lc 70:24-70:27 Type
162testdata/Internals.lc 70:1-70:18 String -> String->Ordering 154testdata/Internals.lc 70:33-70:38 Type
163testdata/Internals.lc 70:24-70:30 Type 155testdata/Internals.lc 71:1-71:13 Int->Nat
164testdata/Internals.lc 70:34-70:40 Type
165testdata/Internals.lc 70:34-70:52 Type
166testdata/Internals.lc 70:44-70:52 Type
167testdata/Internals.lc 71:1-71:14 Int->Int
168testdata/Internals.lc 71:24-71:27 Type 156testdata/Internals.lc 71:24-71:27 Type
169testdata/Internals.lc 71:33-71:36 Type 157testdata/Internals.lc 71:33-71:36 Type
170testdata/Internals.lc 72:1-72:15 Word->Word 158testdata/Internals.lc 72:1-72:15 Int -> Int->Ordering
171testdata/Internals.lc 72:24-72:28 Type 159testdata/Internals.lc 72:24-72:27 Type
172testdata/Internals.lc 72:33-72:37 Type 160testdata/Internals.lc 72:33-72:36 Type
173testdata/Internals.lc 73:1-73:16 Float->Float 161testdata/Internals.lc 72:33-72:50 Type
174testdata/Internals.lc 73:24-73:29 Type 162testdata/Internals.lc 72:42-72:50 Type
175testdata/Internals.lc 73:33-73:38 Type 163testdata/Internals.lc 73:1-73:16 Word -> Word->Ordering
176testdata/Internals.lc 74:1-74:11 Int -> Int->Int 164testdata/Internals.lc 73:24-73:28 Type
177testdata/Internals.lc 74:24-74:27 Type 165testdata/Internals.lc 73:33-73:37 Type
178testdata/Internals.lc 74:33-74:36 Type 166testdata/Internals.lc 73:33-73:50 Type
179testdata/Internals.lc 74:33-74:45 Type 167testdata/Internals.lc 73:42-73:50 Type
180testdata/Internals.lc 74:42-74:45 Type 168testdata/Internals.lc 74:1-74:17 Float -> Float->Ordering
181testdata/Internals.lc 75:1-75:11 Int -> Int->Int 169testdata/Internals.lc 74:24-74:29 Type
182testdata/Internals.lc 75:24-75:27 Type 170testdata/Internals.lc 74:33-74:38 Type
183testdata/Internals.lc 75:33-75:36 Type 171testdata/Internals.lc 74:33-74:50 Type
184testdata/Internals.lc 75:33-75:45 Type 172testdata/Internals.lc 74:42-74:50 Type
185testdata/Internals.lc 75:42-75:45 Type 173testdata/Internals.lc 75:1-75:16 Char -> Char->Ordering
186testdata/Internals.lc 76:1-76:11 Int -> Int->Int 174testdata/Internals.lc 75:24-75:28 Type
187testdata/Internals.lc 76:24-76:27 Type 175testdata/Internals.lc 75:33-75:37 Type
188testdata/Internals.lc 76:33-76:36 Type 176testdata/Internals.lc 75:33-75:50 Type
189testdata/Internals.lc 76:33-76:45 Type 177testdata/Internals.lc 75:42-75:50 Type
190testdata/Internals.lc 76:42-76:45 Type 178testdata/Internals.lc 76:1-76:18 String -> String->Ordering
191testdata/Internals.lc 77:1-77:14 Float->Float 179testdata/Internals.lc 76:24-76:30 Type
192testdata/Internals.lc 77:24-77:29 Type 180testdata/Internals.lc 76:34-76:40 Type
193testdata/Internals.lc 77:33-77:38 Type 181testdata/Internals.lc 76:34-76:52 Type
194testdata/Internals.lc 78:1-78:10 Float->Int 182testdata/Internals.lc 76:44-76:52 Type
195testdata/Internals.lc 78:24-78:29 Type 183testdata/Internals.lc 77:1-77:14 Int->Int
196testdata/Internals.lc 78:33-78:36 Type 184testdata/Internals.lc 77:24-77:27 Type
197testdata/Internals.lc 81:19-81:23 Type 185testdata/Internals.lc 77:33-77:36 Type
198testdata/Internals.lc 81:19-81:38 Type 186testdata/Internals.lc 78:1-78:15 Word->Word
199testdata/Internals.lc 81:27-81:28 V2 187testdata/Internals.lc 78:24-78:28 Type
200testdata/Internals.lc 81:27-81:38 Type 188testdata/Internals.lc 78:33-78:37 Type
201testdata/Internals.lc 81:32-81:33 Type 189testdata/Internals.lc 79:1-79:16 Float->Float
202testdata/Internals.lc 81:32-81:38 Type 190testdata/Internals.lc 79:24-79:29 Type
203testdata/Internals.lc 81:37-81:38 Type 191testdata/Internals.lc 79:33-79:38 Type
204testdata/Internals.lc 82:1-82:15 {a} -> Bool -> a -> a->a 192testdata/Internals.lc 80:1-80:11 Int -> Int->Int
205testdata/Internals.lc 82:16-82:20 Bool 193testdata/Internals.lc 80:24-80:27 Type
206testdata/Internals.lc 82:16-83:29 Bool -> V1 -> V2->V3 | V1 -> V2->V3 | V2->V3 | V3 194testdata/Internals.lc 80:33-80:36 Type
207testdata/Internals.lc 82:28-82:29 V3 195testdata/Internals.lc 80:33-80:45 Type
208testdata/Internals.lc 82:28-83:29 Bool->V4 196testdata/Internals.lc 80:42-80:45 Type
209testdata/Internals.lc 83:28-83:29 V4 197testdata/Internals.lc 81:1-81:11 Int -> Int->Int
210testdata/Internals.lc 85:1-85:5 Ordering->Bool 198testdata/Internals.lc 81:24-81:27 Type
211testdata/Internals.lc 85:6-85:8 V1 199testdata/Internals.lc 81:33-81:36 Type
212testdata/Internals.lc 85:6-86:15 Bool 200testdata/Internals.lc 81:33-81:45 Type
213testdata/Internals.lc 85:11-85:15 Bool 201testdata/Internals.lc 81:42-81:45 Type
214testdata/Internals.lc 85:11-86:15 Bool -> Ordering->Bool 202testdata/Internals.lc 82:1-82:11 Int -> Int->Int
215testdata/Internals.lc 86:10-86:15 Bool 203testdata/Internals.lc 82:24-82:27 Type
216testdata/Internals.lc 89:7-89:10 Type->Type 204testdata/Internals.lc 82:33-82:36 Type
217testdata/Internals.lc 89:7-90:22 Type 205testdata/Internals.lc 82:33-82:45 Type
218testdata/Internals.lc 89:7-91:32 Type 206testdata/Internals.lc 82:42-82:45 Type
219testdata/Internals.lc 89:7-92:19 Type 207testdata/Internals.lc 83:1-83:14 Float->Float
220testdata/Internals.lc 90:3-90:10 {a} -> {b : Num a} -> Int->a 208testdata/Internals.lc 83:24-83:29 Type
221testdata/Internals.lc 90:14-90:17 Type 209testdata/Internals.lc 83:33-83:38 Type
222testdata/Internals.lc 90:14-90:22 Type 210testdata/Internals.lc 84:1-84:10 Float->Int
223testdata/Internals.lc 90:21-90:22 Type 211testdata/Internals.lc 84:24-84:29 Type
224testdata/Internals.lc 91:3-91:10 {a} -> {b : Num a} -> a -> a->Ordering 212testdata/Internals.lc 84:33-84:36 Type
225testdata/Internals.lc 91:14-91:15 Type 213testdata/Internals.lc 87:19-87:23 Type
226testdata/Internals.lc 91:14-91:32 Type 214testdata/Internals.lc 87:19-87:38 Type
227testdata/Internals.lc 91:19-91:20 Type 215testdata/Internals.lc 87:27-87:28 V2
228testdata/Internals.lc 91:19-91:32 Type 216testdata/Internals.lc 87:27-87:38 Type
229testdata/Internals.lc 91:24-91:32 Type 217testdata/Internals.lc 87:32-87:33 Type
230testdata/Internals.lc 92:3-92:9 {a} -> {b : Num a} -> a->a 218testdata/Internals.lc 87:32-87:38 Type
231testdata/Internals.lc 92:13-92:14 Type 219testdata/Internals.lc 87:37-87:38 Type
232testdata/Internals.lc 92:13-92:19 Type 220testdata/Internals.lc 88:1-88:15 {a} -> Bool -> a -> a->a
233testdata/Internals.lc 92:18-92:19 Type 221testdata/Internals.lc 88:16-88:20 Bool
234testdata/Internals.lc 94:14-94:17 Type 222testdata/Internals.lc 88:16-89:29 Bool -> V1 -> V2->V3 | V1 -> V2->V3 | V2->V3 | V3
235testdata/Internals.lc 94:14-95:20 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3 223testdata/Internals.lc 88:28-88:29 V3
236testdata/Internals.lc 94:14-96:27 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering 224testdata/Internals.lc 88:28-89:29 Bool->V4
237testdata/Internals.lc 94:14-97:26 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3 225testdata/Internals.lc 89:28-89:29 V4
238testdata/Internals.lc 94:14-106:17 Type | Type->Type 226testdata/Internals.lc 91:1-91:5 Ordering->Bool
239testdata/Internals.lc 94:14-107:25 {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a 227testdata/Internals.lc 91:6-91:8 V1
240testdata/Internals.lc 94:14-108:22 {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering 228testdata/Internals.lc 91:6-92:15 Bool
241testdata/Internals.lc 94:14-109:22 {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a 229testdata/Internals.lc 91:11-91:15 Bool
242testdata/Internals.lc 95:13-95:20 Int->Int 230testdata/Internals.lc 91:11-92:15 Bool -> Ordering->Bool
243testdata/Internals.lc 95:19-95:20 Int 231testdata/Internals.lc 92:10-92:15 Bool
244testdata/Internals.lc 96:13-96:27 Int -> Int->Ordering 232testdata/Internals.lc 95:7-95:10 Type->Type
245testdata/Internals.lc 97:13-97:26 Int->Int 233testdata/Internals.lc 95:7-96:22 Type
246testdata/Internals.lc 98:14-98:18 Type 234testdata/Internals.lc 95:7-97:32 Type
247testdata/Internals.lc 98:14-99:26 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3 235testdata/Internals.lc 95:7-98:19 Type
248testdata/Internals.lc 98:14-100:28 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering 236testdata/Internals.lc 96:3-96:10 {a} -> {b : Num a} -> Int->a
249testdata/Internals.lc 98:14-101:27 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3 237testdata/Internals.lc 96:14-96:17 Type
250testdata/Internals.lc 98:14-106:17 Type 238testdata/Internals.lc 96:14-96:22 Type
251testdata/Internals.lc 98:14-107:25 {a : Num V0} -> Int->V2 239testdata/Internals.lc 96:21-96:22 Type
252testdata/Internals.lc 98:14-108:22 {a : Num V0} -> V1 -> V2->Ordering 240testdata/Internals.lc 97:3-97:10 {a} -> {b : Num a} -> a -> a->Ordering
253testdata/Internals.lc 98:14-109:22 {a : Num V0} -> V1->V2 241testdata/Internals.lc 97:14-97:15 Type
254testdata/Internals.lc 99:13-99:26 Int->Word 242testdata/Internals.lc 97:14-97:32 Type
255testdata/Internals.lc 100:13-100:28 Word -> Word->Ordering 243testdata/Internals.lc 97:19-97:20 Type
256testdata/Internals.lc 101:13-101:27 Word->Word 244testdata/Internals.lc 97:19-97:32 Type
257testdata/Internals.lc 102:14-102:19 Type 245testdata/Internals.lc 97:24-97:32 Type
258testdata/Internals.lc 102:14-103:27 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3 246testdata/Internals.lc 98:3-98:9 {a} -> {b : Num a} -> a->a
259testdata/Internals.lc 102:14-104:29 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering 247testdata/Internals.lc 98:13-98:14 Type
260testdata/Internals.lc 102:14-105:28 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3 248testdata/Internals.lc 98:13-98:19 Type
261testdata/Internals.lc 102:14-106:17 Type 249testdata/Internals.lc 98:18-98:19 Type
262testdata/Internals.lc 102:14-107:25 {a : Num V0} -> Int->V2 250testdata/Internals.lc 100:14-100:17 Type
263testdata/Internals.lc 102:14-108:22 {a : Num V0} -> V1 -> V2->Ordering 251testdata/Internals.lc 100:14-101:20 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
264testdata/Internals.lc 102:14-109:22 {a : Num V0} -> V1->V2 252testdata/Internals.lc 100:14-102:27 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
265testdata/Internals.lc 103:13-103:27 Int->Float 253testdata/Internals.lc 100:14-103:26 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
266testdata/Internals.lc 104:13-104:29 Float -> Float->Ordering 254testdata/Internals.lc 100:14-112:17 Type | Type->Type
267testdata/Internals.lc 105:13-105:28 Float->Float 255testdata/Internals.lc 100:14-113:25 {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a
268testdata/Internals.lc 106:14-106:17 Type 256testdata/Internals.lc 100:14-114:22 {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering
269testdata/Internals.lc 106:14-107:25 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3 257testdata/Internals.lc 100:14-115:22 {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a
270testdata/Internals.lc 106:14-108:22 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering 258testdata/Internals.lc 101:13-101:20 Int->Int
271testdata/Internals.lc 106:14-109:22 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3 259testdata/Internals.lc 101:19-101:20 Int
272testdata/Internals.lc 107:13-107:25 Int->Nat 260testdata/Internals.lc 102:13-102:27 Int -> Int->Ordering
273testdata/Internals.lc 108:13-108:22 {a:Unit} -> Nat -> Nat->Ordering 261testdata/Internals.lc 103:13-103:26 Int->Int
274testdata/Internals.lc 109:13-109:22 {a:Unit} -> Nat->Nat 262testdata/Internals.lc 104:14-104:18 Type
275testdata/Internals.lc 111:7-111:9 Type->Type 263testdata/Internals.lc 104:14-105:26 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
276testdata/Internals.lc 111:7-112:27 Type 264testdata/Internals.lc 104:14-106:28 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
277testdata/Internals.lc 111:7-127:29 V0->V1 | {a} -> {b : Eq a} -> a -> a->Bool 265testdata/Internals.lc 104:14-107:27 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
278testdata/Internals.lc 112:5-112:9 {a} -> {b : Eq a} -> a -> a->Bool 266testdata/Internals.lc 104:14-112:17 Type
279testdata/Internals.lc 112:13-112:14 Type 267testdata/Internals.lc 104:14-113:25 {a : Num V0} -> Int->V2
280testdata/Internals.lc 112:13-112:27 Type 268testdata/Internals.lc 104:14-114:22 {a : Num V0} -> V1 -> V2->Ordering
281testdata/Internals.lc 112:18-112:19 Type 269testdata/Internals.lc 104:14-115:22 {a : Num V0} -> V1->V2
282testdata/Internals.lc 112:18-112:27 Type 270testdata/Internals.lc 105:13-105:26 Int->Word
283testdata/Internals.lc 112:23-112:27 Type 271testdata/Internals.lc 106:13-106:28 Word -> Word->Ordering
284testdata/Internals.lc 116:13-116:19 Type 272testdata/Internals.lc 107:13-107:27 Word->Word
285testdata/Internals.lc 116:13-116:63 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool 273testdata/Internals.lc 108:14-108:19 Type
286testdata/Internals.lc 116:13-124:16 Type | Type->Type 274testdata/Internals.lc 108:14-109:27 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
287testdata/Internals.lc 116:13-127:29 {a : Eq V0} -> V1 -> V2->Bool | {a} -> {b : Eq a} -> a -> a->Bool 275testdata/Internals.lc 108:14-110:29 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
288testdata/Internals.lc 116:35-116:39 Ordering->Bool 276testdata/Internals.lc 108:14-111:28 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
289testdata/Internals.lc 116:35-116:63 Bool | String -> String->Bool | String->Bool 277testdata/Internals.lc 108:14-112:17 Type
290testdata/Internals.lc 116:40-116:63 Ordering 278testdata/Internals.lc 108:14-113:25 {a : Num V0} -> Int->V2
291testdata/Internals.lc 116:41-116:58 String -> String->Ordering 279testdata/Internals.lc 108:14-114:22 {a : Num V0} -> V1 -> V2->Ordering
292testdata/Internals.lc 116:41-116:60 String->Ordering 280testdata/Internals.lc 108:14-115:22 {a : Num V0} -> V1->V2
293testdata/Internals.lc 116:59-116:60 String 281testdata/Internals.lc 109:13-109:27 Int->Float
294testdata/Internals.lc 116:61-116:62 String 282testdata/Internals.lc 110:13-110:29 Float -> Float->Ordering
295testdata/Internals.lc 117:13-117:17 Type 283testdata/Internals.lc 111:13-111:28 Float->Float
296testdata/Internals.lc 117:13-117:59 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool 284testdata/Internals.lc 112:14-112:17 Type
297testdata/Internals.lc 117:13-124:16 Type 285testdata/Internals.lc 112:14-113:25 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
298testdata/Internals.lc 117:13-127:29 {a : Eq V0} -> V1 -> V2->Bool 286testdata/Internals.lc 112:14-114:22 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
299testdata/Internals.lc 117:33-117:37 Ordering->Bool 287testdata/Internals.lc 112:14-115:22 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
300testdata/Internals.lc 117:33-117:59 Bool | Char -> Char->Bool | Char->Bool 288testdata/Internals.lc 113:13-113:25 Int->Nat
301testdata/Internals.lc 117:38-117:59 Ordering 289testdata/Internals.lc 114:13-114:22 {a:Unit} -> Nat -> Nat->Ordering
302testdata/Internals.lc 117:39-117:54 Char -> Char->Ordering 290testdata/Internals.lc 115:13-115:22 {a:Unit} -> Nat->Nat
303testdata/Internals.lc 117:39-117:56 Char->Ordering 291testdata/Internals.lc 117:7-117:9 Type->Type
304testdata/Internals.lc 117:55-117:56 Char 292testdata/Internals.lc 117:7-118:27 Type
305testdata/Internals.lc 117:57-117:58 Char 293testdata/Internals.lc 117:7-133:29 V0->V1 | {a} -> {b : Eq a} -> a -> a->Bool
306testdata/Internals.lc 118:13-118:16 Type 294testdata/Internals.lc 118:5-118:9 {a} -> {b : Eq a} -> a -> a->Bool
307testdata/Internals.lc 118:13-118:57 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool 295testdata/Internals.lc 118:13-118:14 Type
308testdata/Internals.lc 118:13-124:16 Type 296testdata/Internals.lc 118:13-118:27 Type
309testdata/Internals.lc 118:13-127:29 {a : Eq V0} -> V1 -> V2->Bool 297testdata/Internals.lc 118:18-118:19 Type
310testdata/Internals.lc 118:32-118:36 Ordering->Bool 298testdata/Internals.lc 118:18-118:27 Type
311testdata/Internals.lc 118:32-118:57 Bool | Int -> Int->Bool | Int->Bool 299testdata/Internals.lc 118:23-118:27 Type
312testdata/Internals.lc 118:37-118:57 Ordering 300testdata/Internals.lc 122:13-122:19 Type
313testdata/Internals.lc 118:38-118:52 Int -> Int->Ordering 301testdata/Internals.lc 122:13-122:63 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
314testdata/Internals.lc 118:38-118:54 Int->Ordering 302testdata/Internals.lc 122:13-130:16 Type | Type->Type
315testdata/Internals.lc 118:53-118:54 Int 303testdata/Internals.lc 122:13-133:29 {a : Eq V0} -> V1 -> V2->Bool | {a} -> {b : Eq a} -> a -> a->Bool
316testdata/Internals.lc 118:55-118:56 Int 304testdata/Internals.lc 122:35-122:39 Ordering->Bool
317testdata/Internals.lc 119:13-119:18 Type 305testdata/Internals.lc 122:35-122:63 Bool | String -> String->Bool | String->Bool
318testdata/Internals.lc 119:13-119:61 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool 306testdata/Internals.lc 122:40-122:63 Ordering
319testdata/Internals.lc 119:13-124:16 Type 307testdata/Internals.lc 122:41-122:58 String -> String->Ordering
320testdata/Internals.lc 119:13-127:29 {a : Eq V0} -> V1 -> V2->Bool 308testdata/Internals.lc 122:41-122:60 String->Ordering
321testdata/Internals.lc 119:34-119:38 Ordering->Bool 309testdata/Internals.lc 122:59-122:60 String
322testdata/Internals.lc 119:34-119:61 Bool | Float -> Float->Bool | Float->Bool 310testdata/Internals.lc 122:61-122:62 String
323testdata/Internals.lc 119:39-119:61 Ordering 311testdata/Internals.lc 123:13-123:17 Type
324testdata/Internals.lc 119:40-119:56 Float -> Float->Ordering 312testdata/Internals.lc 123:13-123:59 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
325testdata/Internals.lc 119:40-119:58 Float->Ordering 313testdata/Internals.lc 123:13-130:16 Type
326testdata/Internals.lc 119:57-119:58 Float 314testdata/Internals.lc 123:13-133:29 {a : Eq V0} -> V1 -> V2->Bool
327testdata/Internals.lc 119:59-119:60 Float 315testdata/Internals.lc 123:33-123:37 Ordering->Bool
328testdata/Internals.lc 120:13-120:17 Type 316testdata/Internals.lc 123:33-123:59 Bool | Char -> Char->Bool | Char->Bool
329testdata/Internals.lc 120:13-123:19 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool 317testdata/Internals.lc 123:38-123:59 Ordering
330testdata/Internals.lc 120:13-124:16 Type 318testdata/Internals.lc 123:39-123:54 Char -> Char->Ordering
331testdata/Internals.lc 120:13-127:29 {a : Eq V0} -> V1 -> V2->Bool 319testdata/Internals.lc 123:39-123:56 Char->Ordering
332testdata/Internals.lc 121:5-121:9 Bool 320testdata/Internals.lc 123:55-123:56 Char
333testdata/Internals.lc 121:5-123:19 Bool | Bool -> Bool->Bool | Bool->Bool 321testdata/Internals.lc 123:57-123:58 Char
334testdata/Internals.lc 121:13-121:17 Bool
335testdata/Internals.lc 121:13-123:19 Bool
336testdata/Internals.lc 121:20-121:24 Bool
337testdata/Internals.lc 121:20-123:19 Bool->Bool
338testdata/Internals.lc 122:14-122:19 Bool
339testdata/Internals.lc 122:14-123:19 Bool
340testdata/Internals.lc 122:22-122:26 Bool
341testdata/Internals.lc 122:22-123:19 Bool->Bool
342testdata/Internals.lc 123:14-123:19 Bool
343testdata/Internals.lc 124:13-124:16 Type 322testdata/Internals.lc 124:13-124:16 Type
344testdata/Internals.lc 124:13-127:29 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool 323testdata/Internals.lc 124:13-124:57 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
345testdata/Internals.lc 125:5-125:9 Nat 324testdata/Internals.lc 124:13-130:16 Type
346testdata/Internals.lc 125:5-127:29 Bool | Nat -> Nat->Bool | Nat->Bool 325testdata/Internals.lc 124:13-133:29 {a : Eq V0} -> V1 -> V2->Bool
347testdata/Internals.lc 125:15-125:19 Nat 326testdata/Internals.lc 124:32-124:36 Ordering->Bool
348testdata/Internals.lc 125:15-127:29 Bool 327testdata/Internals.lc 124:32-124:57 Bool | Int -> Int->Bool | Int->Bool
349testdata/Internals.lc 125:24-125:28 Bool 328testdata/Internals.lc 124:37-124:57 Ordering
350testdata/Internals.lc 125:24-127:29 Nat->Bool 329testdata/Internals.lc 124:38-124:52 Int -> Int->Ordering
351testdata/Internals.lc 126:15-126:19 Nat 330testdata/Internals.lc 124:38-124:54 Int->Ordering
352testdata/Internals.lc 126:15-127:29 Bool | Nat->Bool 331testdata/Internals.lc 124:53-124:54 Int
353testdata/Internals.lc 126:24-126:25 Nat 332testdata/Internals.lc 124:55-124:56 Int
354testdata/Internals.lc 126:24-126:28 Nat->Bool 333testdata/Internals.lc 125:13-125:18 Type
355testdata/Internals.lc 126:24-126:30 Bool | Nat->Bool 334testdata/Internals.lc 125:13-125:61 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
356testdata/Internals.lc 126:24-127:29 Nat->Bool 335testdata/Internals.lc 125:13-130:16 Type
357testdata/Internals.lc 126:26-126:28 {a} -> {b : Eq a} -> a -> a->Bool 336testdata/Internals.lc 125:13-133:29 {a : Eq V0} -> V1 -> V2->Bool
358testdata/Internals.lc 126:29-126:30 Nat 337testdata/Internals.lc 125:34-125:38 Ordering->Bool
359testdata/Internals.lc 127:24-127:29 Bool | Nat->Bool 338testdata/Internals.lc 125:34-125:61 Bool | Float -> Float->Bool | Float->Bool
360testdata/Internals.lc 129:6-129:10 Type | Type->Type 339testdata/Internals.lc 125:39-125:61 Ordering
361testdata/Internals.lc 129:6-129:25 Type 340testdata/Internals.lc 125:40-125:56 Float -> Float->Ordering
362testdata/Internals.lc 129:6-129:36 Type 341testdata/Internals.lc 125:40-125:58 Float->Ordering
363testdata/Internals.lc 129:15-129:18 List V1 | {a} -> List a 342testdata/Internals.lc 125:57-125:58 Float
364testdata/Internals.lc 129:21-129:25 List V4 | Type | {a} -> a -> List a -> List a 343testdata/Internals.lc 125:59-125:60 Float
365testdata/Internals.lc 129:26-129:27 Type 344testdata/Internals.lc 126:13-126:17 Type
366testdata/Internals.lc 129:28-129:36 Type 345testdata/Internals.lc 126:13-129:19 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
367testdata/Internals.lc 129:29-129:33 Type->Type 346testdata/Internals.lc 126:13-130:16 Type
368testdata/Internals.lc 129:34-129:35 Type 347testdata/Internals.lc 126:13-133:29 {a : Eq V0} -> V1 -> V2->Bool
348testdata/Internals.lc 127:5-127:9 Bool
349testdata/Internals.lc 127:5-129:19 Bool | Bool -> Bool->Bool | Bool->Bool
350testdata/Internals.lc 127:13-127:17 Bool
351testdata/Internals.lc 127:13-129:19 Bool
352testdata/Internals.lc 127:20-127:24 Bool
353testdata/Internals.lc 127:20-129:19 Bool->Bool
354testdata/Internals.lc 128:14-128:19 Bool
355testdata/Internals.lc 128:14-129:19 Bool
356testdata/Internals.lc 128:22-128:26 Bool
357testdata/Internals.lc 128:22-129:19 Bool->Bool
358testdata/Internals.lc 129:14-129:19 Bool
359testdata/Internals.lc 130:13-130:16 Type
360testdata/Internals.lc 130:13-133:29 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
361testdata/Internals.lc 131:5-131:9 Nat
362testdata/Internals.lc 131:5-133:29 Bool | Nat -> Nat->Bool | Nat->Bool
363testdata/Internals.lc 131:15-131:19 Nat
364testdata/Internals.lc 131:15-133:29 Bool
365testdata/Internals.lc 131:24-131:28 Bool
366testdata/Internals.lc 131:24-133:29 Nat->Bool
367testdata/Internals.lc 132:15-132:19 Nat
368testdata/Internals.lc 132:15-133:29 Bool | Nat->Bool
369testdata/Internals.lc 132:24-132:25 Nat
370testdata/Internals.lc 132:24-132:28 Nat->Bool
371testdata/Internals.lc 132:24-132:30 Bool | Nat->Bool
372testdata/Internals.lc 132:24-133:29 Nat->Bool
373testdata/Internals.lc 132:26-132:28 {a} -> {b : Eq a} -> a -> a->Bool
374testdata/Internals.lc 132:29-132:30 Nat
375testdata/Internals.lc 133:24-133:29 Bool | Nat->Bool
376testdata/Internals.lc 135:6-135:10 Type | Type->Type
377testdata/Internals.lc 135:6-135:25 Type
378testdata/Internals.lc 135:6-135:36 Type
379testdata/Internals.lc 135:15-135:18 List V1 | {a} -> List a
380testdata/Internals.lc 135:21-135:25 List V4 | Type | {a} -> a -> List a -> List a
381testdata/Internals.lc 135:26-135:27 Type
382testdata/Internals.lc 135:28-135:36 Type
383testdata/Internals.lc 135:29-135:33 Type->Type
384testdata/Internals.lc 135:34-135:35 Type
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-29 16:29:02 +0000