From e19b4e7051066ce8bff0e4b3c51b06e1169d4fb1 Mon Sep 17 00:00:00 2001 From: Péter Diviánszky Date: Fri, 5 Feb 2016 16:35:12 +0100 Subject: refactor Builtins.lc --- lc/Builtins.lc | 27 +- src/LambdaCube/Compiler/CoreToIR.hs | 6 +- src/LambdaCube/Compiler/Infer.hs | 4 +- testdata/Builtins.out | 2116 +++++++++++++++++------------------ 4 files changed, 1073 insertions(+), 1080 deletions(-) diff --git a/lc/Builtins.lc b/lc/Builtins.lc index a8b9e98b..80a818eb 100644 --- a/lc/Builtins.lc +++ b/lc/Builtins.lc @@ -295,12 +295,12 @@ type family FragOps a where FragOps (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4) = (t1, t2, t3, t4) FragOps (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4, FragmentOperation t5) = (t1, t2, t3, t4, t5) -} -type family FragOps' a where - FragOps' (t1, t2) = (FragmentOperation t1, FragmentOperation t2) - FragOps' (t1, t2, t3) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3) - FragOps' (t1, t2, t3, t4) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4) - FragOps' (t1, t2, t3, t4, t5) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4, FragmentOperation t5) - FragOps' t = (FragmentOperation t) +type family FragOps a where + FragOps (t1, t2) = (FragmentOperation t1, FragmentOperation t2) + FragOps (t1, t2, t3) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3) + FragOps (t1, t2, t3, t4) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4) + FragOps (t1, t2, t3, t4, t5) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4, FragmentOperation t5) + FragOps t = (FragmentOperation t) [] ++ ys = ys x:xs ++ ys = x : xs ++ ys @@ -407,11 +407,12 @@ rasterize rasterizePrimitives ctx is s = concat (map (rasterize is ctx) s) -data Image :: Nat -> Type -> Type where - ColorImage :: forall a d t color . (Num t, color ~ VecScalar d t) - => color -> Image a (Color color) - DepthImage :: forall a . Float -> Image a (Depth Float) - StencilImage :: forall a . Int -> Image a (Stencil Int) +data Image :: Nat -> Type -> Type + +ColorImage :: forall a d t color . (Num t, color ~ VecScalar d t) + => color -> Image a (Color color) +DepthImage :: forall a . Float -> Image a (Depth Float) +StencilImage :: forall a . Int -> Image a (Stencil Int) type family SameLayerCounts a where SameLayerCounts (Image n1 t1) = Unit @@ -427,8 +428,8 @@ instance (DefaultFragOp a, DefaultFragOp b) => DefaultFragOps (FragmentOperation defaultFragOps = -- (undefined @(), undefined) (defaultFragOp @a @_, defaultFragOp @b @_) -} -data FrameBuffer (n :: Nat) b where - Accumulate :: FragOps' b -> FragmentStream n (RemSemantics b) -> FrameBuffer n b -> FrameBuffer n b +data FrameBuffer (n :: Nat) t +Accumulate :: FragOps b -> FragmentStream n (RemSemantics b) -> FrameBuffer n b -> FrameBuffer n b type family TFFrameBuffer a where TFFrameBuffer (Image n1 t1) = FrameBuffer n1 t1 diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs index 9c67cb02..2a3c78eb 100644 --- a/src/LambdaCube/Compiler/CoreToIR.hs +++ b/src/LambdaCube/Compiler/CoreToIR.hs @@ -225,7 +225,7 @@ getCommands e = case e of rt <- newFrameBufferTarget (tyOf a) (subCmds,cmds) <- getCommands a return (subCmds,IR.SetRenderTarget rt : cmds) - A3 "Accumulate" actx (getFragmentShader . removeDepthHandler -> (frag, getFragFilter -> (ffilter, Prim3 "foldr" (EtaPrim2_2 "++") (A0 "Nil") (Prim2 "map" (EtaPrim3 "rasterize" {-rp-} is rctx) (getVertexShader -> (vert, input)))))) fbuf -> do + Prim3 "Accumulate" actx (getFragmentShader . removeDepthHandler -> (frag, getFragFilter -> (ffilter, Prim3 "foldr" (EtaPrim2_2 "++") (A0 "Nil") (Prim2 "map" (EtaPrim3 "rasterize" {-rp-} is rctx) (getVertexShader -> (vert, input)))))) fbuf -> do let rp = compRC' rctx (smpBindingsV,vertCmds) <- getRenderTextureCommands vert (smpBindingsR,rastCmds) <- maybe (return mempty) getRenderTextureCommands ffilter @@ -267,8 +267,8 @@ getUniforms e = case e of compFrameBuffer x = case x of ETuple a -> concatMap compFrameBuffer a - A1 "DepthImage" a -> [(IR.Depth, compValue a)] - A1 "ColorImage" a -> [(IR.Color, compValue a)] + Prim1 "DepthImage" a -> [(IR.Depth, compValue a)] + Prim1 "ColorImage" a -> [(IR.Color, compValue a)] x -> error $ "compFrameBuffer " ++ ppShow x compSemantic x = case x of diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 3df27eaa..70fab42f 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs @@ -574,8 +574,8 @@ cstrT_ typ = cstr__ [] cstr_ [] (UL (FunN "'VecScalar" [a, b])) t@(TTyCon0 n) | isElemTy n = t2 (cstrT TNat a (ENat 1)) (cstr__ [] b t) cstr_ [] t@(TTyCon0 n) (UL (FunN "'VecScalar" [a, b])) | isElemTy n = t2 (cstrT TNat a (ENat 1)) (cstr__ [] b t) - cstr_ ns@[] (UL (FunN "'FragOps'" [a])) (TyConN "'FragmentOperation" [x]) = cstr__ ns a x - cstr_ ns@[] (UL (FunN "'FragOps'" [a])) (TyConN "'Tuple2" [TyConN "'FragmentOperation" [x], TyConN "'FragmentOperation" [y]]) = cstr__ ns a $ TTuple2 x y + cstr_ ns@[] (UL (FunN "'FragOps" [a])) (TyConN "'FragmentOperation" [x]) = cstr__ ns a x + cstr_ ns@[] (UL (FunN "'FragOps" [a])) (TyConN "'Tuple2" [TyConN "'FragmentOperation" [x], TyConN "'FragmentOperation" [y]]) = cstr__ ns a $ TTuple2 x y cstr_ ns@[] (TyConN "'Tuple2" [x, y]) (UL (FunN "'JoinTupleType" [x', y'])) = t2 (cstr__ ns x x') (cstr__ ns y y') cstr_ ns@[] (UL (FunN "'JoinTupleType" [x', y'])) (TyConN "'Tuple2" [x, y]) = t2 (cstr__ ns x' x) (cstr__ ns y' y) diff --git a/testdata/Builtins.out b/testdata/Builtins.out index e982ec21..d93f0422 100644 --- a/testdata/Builtins.out +++ b/testdata/Builtins.out @@ -972,74 +972,74 @@ testdata/Builtins.lc 289:71-289:104 Type testdata/Builtins.lc 289:89-289:104 Type testdata/Builtins.lc 289:90-289:97 Type->Type testdata/Builtins.lc 289:98-289:103 Type -testdata/Builtins.lc 299:5-299:13 Type->Type -testdata/Builtins.lc 299:15-299:21 Type -testdata/Builtins.lc 299:15-299:69 Type->Type -testdata/Builtins.lc 299:15-303:39 Type | Type->Type -testdata/Builtins.lc 299:25-299:69 Type | Type -> Type->Type | Type->Type -testdata/Builtins.lc 299:26-299:43 Type->Type -testdata/Builtins.lc 299:26-299:46 Type -testdata/Builtins.lc 299:44-299:46 Type -testdata/Builtins.lc 299:48-299:65 Type->Type -testdata/Builtins.lc 299:48-299:68 Type -testdata/Builtins.lc 299:66-299:68 Type -testdata/Builtins.lc 300:15-300:25 Type -testdata/Builtins.lc 300:15-300:95 Type->Type -testdata/Builtins.lc 300:15-303:39 Type -testdata/Builtins.lc 300:29-300:95 Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type -testdata/Builtins.lc 300:30-300:47 Type->Type -testdata/Builtins.lc 300:30-300:50 Type -testdata/Builtins.lc 300:30-300:72 Type->Type -testdata/Builtins.lc 300:48-300:50 Type -testdata/Builtins.lc 300:52-300:69 Type->Type -testdata/Builtins.lc 300:52-300:72 Type -testdata/Builtins.lc 300:70-300:72 Type -testdata/Builtins.lc 300:74-300:91 Type->Type -testdata/Builtins.lc 300:74-300:94 Type -testdata/Builtins.lc 300:92-300:94 Type -testdata/Builtins.lc 301:15-301:29 Type -testdata/Builtins.lc 301:15-301:122 Type->Type -testdata/Builtins.lc 301:15-303:39 Type -testdata/Builtins.lc 301:34-301:122 Type | Type -> Type -> Type -> Type->Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type -testdata/Builtins.lc 301:35-301:52 Type->Type -testdata/Builtins.lc 301:35-301:55 Type -testdata/Builtins.lc 301:35-301:77 Type -> Type->Type -testdata/Builtins.lc 301:35-301:99 Type->Type -testdata/Builtins.lc 301:53-301:55 Type -testdata/Builtins.lc 301:57-301:74 Type->Type -testdata/Builtins.lc 301:57-301:77 Type -testdata/Builtins.lc 301:75-301:77 Type -testdata/Builtins.lc 301:79-301:96 Type->Type -testdata/Builtins.lc 301:79-301:99 Type -testdata/Builtins.lc 301:97-301:99 Type -testdata/Builtins.lc 301:101-301:118 Type->Type -testdata/Builtins.lc 301:101-301:121 Type -testdata/Builtins.lc 301:119-301:121 Type -testdata/Builtins.lc 302:15-302:33 Type -testdata/Builtins.lc 302:15-302:148 Type->Type -testdata/Builtins.lc 302:15-303:39 Type -testdata/Builtins.lc 302:38-302:148 Type | Type -> Type -> Type -> Type -> Type->Type | Type -> Type -> Type -> Type->Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type -testdata/Builtins.lc 302:39-302:56 Type->Type -testdata/Builtins.lc 302:39-302:59 Type -testdata/Builtins.lc 302:39-302:81 Type -> Type -> Type->Type -testdata/Builtins.lc 302:39-302:103 Type -> Type->Type -testdata/Builtins.lc 302:39-302:125 Type->Type -testdata/Builtins.lc 302:57-302:59 Type -testdata/Builtins.lc 302:61-302:78 Type->Type -testdata/Builtins.lc 302:61-302:81 Type -testdata/Builtins.lc 302:79-302:81 Type -testdata/Builtins.lc 302:83-302:100 Type->Type -testdata/Builtins.lc 302:83-302:103 Type -testdata/Builtins.lc 302:101-302:103 Type -testdata/Builtins.lc 302:105-302:122 Type->Type -testdata/Builtins.lc 302:105-302:125 Type -testdata/Builtins.lc 302:123-302:125 Type -testdata/Builtins.lc 302:127-302:144 Type->Type -testdata/Builtins.lc 302:127-302:147 Type -testdata/Builtins.lc 302:145-302:147 Type -testdata/Builtins.lc 303:18-303:39 Type -testdata/Builtins.lc 303:19-303:36 Type->Type -testdata/Builtins.lc 303:37-303:38 Type +testdata/Builtins.lc 299:5-299:12 Type->Type +testdata/Builtins.lc 299:14-299:20 Type +testdata/Builtins.lc 299:14-299:68 Type->Type +testdata/Builtins.lc 299:14-303:38 Type | Type->Type +testdata/Builtins.lc 299:24-299:68 Type | Type -> Type->Type | Type->Type +testdata/Builtins.lc 299:25-299:42 Type->Type +testdata/Builtins.lc 299:25-299:45 Type +testdata/Builtins.lc 299:43-299:45 Type +testdata/Builtins.lc 299:47-299:64 Type->Type +testdata/Builtins.lc 299:47-299:67 Type +testdata/Builtins.lc 299:65-299:67 Type +testdata/Builtins.lc 300:14-300:24 Type +testdata/Builtins.lc 300:14-300:94 Type->Type +testdata/Builtins.lc 300:14-303:38 Type +testdata/Builtins.lc 300:28-300:94 Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type +testdata/Builtins.lc 300:29-300:46 Type->Type +testdata/Builtins.lc 300:29-300:49 Type +testdata/Builtins.lc 300:29-300:71 Type->Type +testdata/Builtins.lc 300:47-300:49 Type +testdata/Builtins.lc 300:51-300:68 Type->Type +testdata/Builtins.lc 300:51-300:71 Type +testdata/Builtins.lc 300:69-300:71 Type +testdata/Builtins.lc 300:73-300:90 Type->Type +testdata/Builtins.lc 300:73-300:93 Type +testdata/Builtins.lc 300:91-300:93 Type +testdata/Builtins.lc 301:14-301:28 Type +testdata/Builtins.lc 301:14-301:121 Type->Type +testdata/Builtins.lc 301:14-303:38 Type +testdata/Builtins.lc 301:33-301:121 Type | Type -> Type -> Type -> Type->Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type +testdata/Builtins.lc 301:34-301:51 Type->Type +testdata/Builtins.lc 301:34-301:54 Type +testdata/Builtins.lc 301:34-301:76 Type -> Type->Type +testdata/Builtins.lc 301:34-301:98 Type->Type +testdata/Builtins.lc 301:52-301:54 Type +testdata/Builtins.lc 301:56-301:73 Type->Type +testdata/Builtins.lc 301:56-301:76 Type +testdata/Builtins.lc 301:74-301:76 Type +testdata/Builtins.lc 301:78-301:95 Type->Type +testdata/Builtins.lc 301:78-301:98 Type +testdata/Builtins.lc 301:96-301:98 Type +testdata/Builtins.lc 301:100-301:117 Type->Type +testdata/Builtins.lc 301:100-301:120 Type +testdata/Builtins.lc 301:118-301:120 Type +testdata/Builtins.lc 302:14-302:32 Type +testdata/Builtins.lc 302:14-302:147 Type->Type +testdata/Builtins.lc 302:14-303:38 Type +testdata/Builtins.lc 302:37-302:147 Type | Type -> Type -> Type -> Type -> Type->Type | Type -> Type -> Type -> Type->Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type +testdata/Builtins.lc 302:38-302:55 Type->Type +testdata/Builtins.lc 302:38-302:58 Type +testdata/Builtins.lc 302:38-302:80 Type -> Type -> Type->Type +testdata/Builtins.lc 302:38-302:102 Type -> Type->Type +testdata/Builtins.lc 302:38-302:124 Type->Type +testdata/Builtins.lc 302:56-302:58 Type +testdata/Builtins.lc 302:60-302:77 Type->Type +testdata/Builtins.lc 302:60-302:80 Type +testdata/Builtins.lc 302:78-302:80 Type +testdata/Builtins.lc 302:82-302:99 Type->Type +testdata/Builtins.lc 302:82-302:102 Type +testdata/Builtins.lc 302:100-302:102 Type +testdata/Builtins.lc 302:104-302:121 Type->Type +testdata/Builtins.lc 302:104-302:124 Type +testdata/Builtins.lc 302:122-302:124 Type +testdata/Builtins.lc 302:126-302:143 Type->Type +testdata/Builtins.lc 302:126-302:146 Type +testdata/Builtins.lc 302:144-302:146 Type +testdata/Builtins.lc 303:17-303:38 Type +testdata/Builtins.lc 303:18-303:35 Type->Type +testdata/Builtins.lc 303:36-303:37 Type testdata/Builtins.lc 305:6-305:8 {a} -> List a -> List a -> List a testdata/Builtins.lc 305:14-305:16 V3 testdata/Builtins.lc 305:14-306:26 List V0 -> List V1 | V0->V1 @@ -1516,330 +1516,301 @@ testdata/Builtins.lc 408:55-408:57 V8 testdata/Builtins.lc 408:58-408:61 V7 testdata/Builtins.lc 408:63-408:64 V2 testdata/Builtins.lc 410:6-410:11 Nat -> Type->Type | Type -testdata/Builtins.lc 410:6-414:68 Type testdata/Builtins.lc 410:15-410:18 Type testdata/Builtins.lc 410:22-410:26 Type testdata/Builtins.lc 410:22-410:34 Type testdata/Builtins.lc 410:30-410:34 Type -testdata/Builtins.lc 411:3-411:13 Image V6 (Color V3) | {a:Nat} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : d ~ VecScalar b c} -> d -> Image a (Color d) -testdata/Builtins.lc 411:3-412:57 Type -testdata/Builtins.lc 411:47-412:57 Type -testdata/Builtins.lc 411:48-411:51 Type->Type -testdata/Builtins.lc 411:48-411:53 Type -testdata/Builtins.lc 411:52-411:53 V3 -testdata/Builtins.lc 411:55-411:60 V2 -testdata/Builtins.lc 411:55-411:62 Type->Type -testdata/Builtins.lc 411:55-411:76 Type -testdata/Builtins.lc 411:55-412:57 Type -testdata/Builtins.lc 411:61-411:62 Type -> Type->Type -testdata/Builtins.lc 411:63-411:72 Nat -> Type->Type -testdata/Builtins.lc 411:63-411:74 Type->Type -testdata/Builtins.lc 411:63-411:76 Type -testdata/Builtins.lc 411:73-411:74 V4 -testdata/Builtins.lc 411:75-411:76 Type -testdata/Builtins.lc 412:26-412:31 Type -testdata/Builtins.lc 412:26-412:57 Type -testdata/Builtins.lc 412:36-412:41 Nat -> Type->Type -testdata/Builtins.lc 412:36-412:43 Type->Type -testdata/Builtins.lc 412:36-412:57 Type -testdata/Builtins.lc 412:42-412:43 Nat | V7 -testdata/Builtins.lc 412:42-412:57 Image V6 (Color V3) -> Type -testdata/Builtins.lc 412:44-412:57 Type -testdata/Builtins.lc 412:45-412:50 Type->Type -testdata/Builtins.lc 412:51-412:56 Type -testdata/Builtins.lc 413:3-413:13 Image V1 (Depth Float) | {a:Nat} -> Float -> Image a (Depth Float) -testdata/Builtins.lc 413:3-413:68 Type -testdata/Builtins.lc 413:37-413:42 Type -testdata/Builtins.lc 413:37-413:68 Type -testdata/Builtins.lc 413:47-413:52 Nat -> Type->Type -testdata/Builtins.lc 413:47-413:54 Type->Type -testdata/Builtins.lc 413:47-413:68 Type -testdata/Builtins.lc 413:53-413:54 Nat | V2 -testdata/Builtins.lc 413:53-413:68 Image V1 (Depth Float) -> Type -testdata/Builtins.lc 413:55-413:68 Type -testdata/Builtins.lc 413:56-413:61 Type->Type -testdata/Builtins.lc 413:62-413:67 Type -testdata/Builtins.lc 414:3-414:15 Image V1 (Stencil Int) | {a:Nat} -> Int -> Image a (Stencil Int) -testdata/Builtins.lc 414:3-414:68 Type -testdata/Builtins.lc 414:37-414:40 Type -testdata/Builtins.lc 414:37-414:68 Type -testdata/Builtins.lc 414:47-414:52 Nat -> Type->Type -testdata/Builtins.lc 414:47-414:54 Type->Type -testdata/Builtins.lc 414:47-414:68 Type -testdata/Builtins.lc 414:53-414:54 Nat | V2 -testdata/Builtins.lc 414:53-414:68 Image V1 (Stencil Int) -> Type -testdata/Builtins.lc 414:55-414:68 Type -testdata/Builtins.lc 414:56-414:63 Type->Type -testdata/Builtins.lc 414:64-414:67 Type -testdata/Builtins.lc 417:5-417:20 Type->Type -testdata/Builtins.lc 417:28-417:33 Type -testdata/Builtins.lc 417:28-417:41 Type->Type -testdata/Builtins.lc 417:28-419:99 Type | Type->Type -testdata/Builtins.lc 417:37-417:41 Nat -> Type->Type | Type | Type->Type -testdata/Builtins.lc 418:22-418:46 Type -testdata/Builtins.lc 418:22-418:64 Type->Type -testdata/Builtins.lc 418:22-419:99 Type -testdata/Builtins.lc 418:50-418:54 a:Type -> a -> a->Type -testdata/Builtins.lc 418:50-418:58 Nat -> Nat->Type -testdata/Builtins.lc 418:50-418:61 Nat->Type -testdata/Builtins.lc 418:50-418:64 Nat -> Type->Type | Type | Type -> Type->Type | Type->Type -testdata/Builtins.lc 418:55-418:58 Type -testdata/Builtins.lc 418:59-418:61 Nat -testdata/Builtins.lc 418:62-418:64 Nat -testdata/Builtins.lc 419:22-419:59 Type -testdata/Builtins.lc 419:22-419:99 Type->Type -testdata/Builtins.lc 419:63-419:65 Type -> Type->Type -testdata/Builtins.lc 419:63-419:82 Type->Type -testdata/Builtins.lc 419:63-419:99 Nat -> Type->Type | Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type -testdata/Builtins.lc 419:66-419:82 Type -testdata/Builtins.lc 419:67-419:71 a:Type -> a -> a->Type -testdata/Builtins.lc 419:67-419:75 Nat -> Nat->Type -testdata/Builtins.lc 419:67-419:78 Nat->Type -testdata/Builtins.lc 419:72-419:75 Type -testdata/Builtins.lc 419:76-419:78 Nat -testdata/Builtins.lc 419:79-419:81 Nat -testdata/Builtins.lc 419:83-419:99 Type -testdata/Builtins.lc 419:84-419:88 a:Type -> a -> a->Type -testdata/Builtins.lc 419:84-419:92 Nat -> Nat->Type -testdata/Builtins.lc 419:84-419:95 Nat->Type -testdata/Builtins.lc 419:89-419:92 Type -testdata/Builtins.lc 419:93-419:95 Nat -testdata/Builtins.lc 419:96-419:98 Nat -testdata/Builtins.lc 421:7-421:20 Type->Type -testdata/Builtins.lc 421:7-421:65 Type -testdata/Builtins.lc 421:29-421:42 {a} -> {b} -> {c : DefaultFragOp b} -> FragmentOperation b -testdata/Builtins.lc 421:46-421:63 Type->Type -testdata/Builtins.lc 421:46-421:65 Type -testdata/Builtins.lc 421:64-421:65 Type -testdata/Builtins.lc 422:37-422:42 Type -testdata/Builtins.lc 422:37-422:112 ({a : DefaultFragOp V1} -> FragmentOperation V2) -> {c : DefaultFragOp V2} -> FragmentOperation V3 -testdata/Builtins.lc 422:37-423:36 Type | Type->Type -testdata/Builtins.lc 422:37-423:77 {a : DefaultFragOp V1} -> FragmentOperation V2 | {a} -> {b : DefaultFragOp a} -> FragmentOperation a -testdata/Builtins.lc 422:69-422:76 {a} -> {b:Nat} -> {c} -> {d} -> {e : a ~ VecScalar b Bool} -> {f : c ~ VecScalar b d} -> {g : Num d} -> Blending d -> a -> FragmentOperation (Color c) -testdata/Builtins.lc 422:69-422:87 VecScalar V2 Bool -> FragmentOperation (Color (VecScalar V3 V2)) -testdata/Builtins.lc 422:69-422:112 FragmentOperation (Color (VecS V1 4)) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ ('Succ ('Succ a))))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ ('Succ ('Succ a)))))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ ('Succ a)))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ ('Succ a))))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ a))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ a)))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ a)))} -> FragmentOperation (Color (VecS Float ('Succ a))) | a:Nat -> {b : DefaultFragOp (Color (VecS V1 a))} -> FragmentOperation (Color (VecS V2 a)) | a:Type -> b:Nat -> {c : DefaultFragOp (Color (VecS a b))} -> FragmentOperation (Color (VecS a b)) | a:Type -> {b : DefaultFragOp (Color a)} -> FragmentOperation (Color a) -testdata/Builtins.lc 422:77-422:87 {a} -> Blending a -testdata/Builtins.lc 422:88-422:112 VecS Bool 4 -testdata/Builtins.lc 422:89-422:91 {a} -> a -> a -> a -> a -> VecS a 4 -testdata/Builtins.lc 422:89-422:96 Bool -> Bool -> Bool -> VecS Bool 4 -testdata/Builtins.lc 422:89-422:101 Bool -> Bool -> VecS Bool 4 -testdata/Builtins.lc 422:89-422:106 Bool -> VecS Bool 4 -testdata/Builtins.lc 422:92-422:96 Bool -testdata/Builtins.lc 422:97-422:101 Bool -testdata/Builtins.lc 422:102-422:106 Bool -testdata/Builtins.lc 422:107-422:111 Bool -testdata/Builtins.lc 423:31-423:36 Type -testdata/Builtins.lc 423:31-423:77 ({a : DefaultFragOp V1} -> FragmentOperation V2) -> {c : DefaultFragOp V2} -> FragmentOperation V3 -testdata/Builtins.lc 423:60-423:67 ComparisonFunction -> Bool -> FragmentOperation (Depth Float) -testdata/Builtins.lc 423:60-423:72 Bool -> FragmentOperation (Depth Float) -testdata/Builtins.lc 423:60-423:77 FragmentOperation (Depth Float) | a:Type -> {b : DefaultFragOp (Depth a)} -> FragmentOperation (Depth a) -testdata/Builtins.lc 423:68-423:72 ComparisonFunction -testdata/Builtins.lc 423:73-423:77 Bool -testdata/Builtins.lc 430:6-430:17 Nat -> Type->Type | Type -testdata/Builtins.lc 430:6-431:13 Type -testdata/Builtins.lc 430:24-430:27 Type -testdata/Builtins.lc 431:3-431:13 FrameBuffer V5 V4 | Type | {a:Nat} -> {b} -> FragOps' b -> List (Vector a (Maybe (SimpleFragment (RemSemantics b)))) -> FrameBuffer a b -> FrameBuffer a b -testdata/Builtins.lc 431:19-431:27 Type->Type -testdata/Builtins.lc 431:19-431:29 Type -testdata/Builtins.lc 431:19-431:104 Type -testdata/Builtins.lc 431:28-431:29 Type -testdata/Builtins.lc 431:33-431:47 Nat -> Type->Type -testdata/Builtins.lc 431:33-431:49 Type->Type -testdata/Builtins.lc 431:33-431:66 Type -testdata/Builtins.lc 431:33-431:104 Type -testdata/Builtins.lc 431:48-431:49 Nat -testdata/Builtins.lc 431:50-431:66 Type -testdata/Builtins.lc 431:51-431:63 Type->Type -testdata/Builtins.lc 431:64-431:65 Type -testdata/Builtins.lc 431:70-431:81 Nat -> Type->Type -testdata/Builtins.lc 431:70-431:83 Type->Type -testdata/Builtins.lc 431:70-431:85 Type -testdata/Builtins.lc 431:70-431:104 Type -testdata/Builtins.lc 431:82-431:83 Nat -testdata/Builtins.lc 431:84-431:85 Type -testdata/Builtins.lc 431:89-431:100 Nat -> Type->Type -testdata/Builtins.lc 431:89-431:102 Type->Type -testdata/Builtins.lc 431:89-431:104 Type -testdata/Builtins.lc 431:101-431:102 Nat -testdata/Builtins.lc 431:103-431:104 Type -testdata/Builtins.lc 434:5-434:18 Type->Type -testdata/Builtins.lc 434:26-434:31 Type -testdata/Builtins.lc 434:26-434:52 Type->Type -testdata/Builtins.lc 434:26-436:88 Type | Type->Type -testdata/Builtins.lc 434:35-434:46 Nat -> Type->Type -testdata/Builtins.lc 434:35-434:49 Type->Type -testdata/Builtins.lc 434:35-434:52 Nat -> Type->Type | Type | Type->Type -testdata/Builtins.lc 434:47-434:49 Nat -testdata/Builtins.lc 434:50-434:52 Type -testdata/Builtins.lc 435:20-435:44 Type -testdata/Builtins.lc 435:20-435:71 Type->Type -testdata/Builtins.lc 435:20-436:88 Type -testdata/Builtins.lc 435:48-435:59 Nat -> Type->Type -testdata/Builtins.lc 435:48-435:62 Type->Type -testdata/Builtins.lc 435:48-435:71 Nat -> Type->Type | Type | Type -> Type->Type | Type->Type -testdata/Builtins.lc 435:60-435:62 Nat -testdata/Builtins.lc 435:63-435:71 Type -testdata/Builtins.lc 435:64-435:66 Type -testdata/Builtins.lc 435:68-435:70 Type -testdata/Builtins.lc 436:20-436:57 Type -testdata/Builtins.lc 436:20-436:88 Type->Type -testdata/Builtins.lc 436:61-436:72 Nat -> Type->Type -testdata/Builtins.lc 436:61-436:75 Type->Type -testdata/Builtins.lc 436:61-436:88 Nat -> Type->Type | Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type -testdata/Builtins.lc 436:73-436:75 Nat -testdata/Builtins.lc 436:76-436:88 Type -testdata/Builtins.lc 436:77-436:79 Type -testdata/Builtins.lc 436:77-436:83 Type->Type -testdata/Builtins.lc 436:81-436:83 Type -testdata/Builtins.lc 436:85-436:87 Type -testdata/Builtins.lc 438:1-438:12 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a -testdata/Builtins.lc 438:17-438:115 Type -testdata/Builtins.lc 438:18-438:34 Type->Type -testdata/Builtins.lc 438:18-438:36 Type -testdata/Builtins.lc 438:35-438:36 V5 -testdata/Builtins.lc 438:38-438:53 Type->Type -testdata/Builtins.lc 438:38-438:55 Type -testdata/Builtins.lc 438:38-438:115 Type -testdata/Builtins.lc 438:54-438:55 V4 -testdata/Builtins.lc 438:57-438:68 Nat -> Type->Type -testdata/Builtins.lc 438:57-438:70 Type->Type -testdata/Builtins.lc 438:57-438:72 Type -testdata/Builtins.lc 438:57-438:74 Type->Type -testdata/Builtins.lc 438:57-438:90 Type -testdata/Builtins.lc 438:57-438:115 Type -testdata/Builtins.lc 438:69-438:70 V3 -testdata/Builtins.lc 438:71-438:72 Type -testdata/Builtins.lc 438:73-438:74 Type -> Type->Type -testdata/Builtins.lc 438:75-438:88 Type->Type -testdata/Builtins.lc 438:75-438:90 Type -testdata/Builtins.lc 438:89-438:90 Type -testdata/Builtins.lc 438:95-438:96 Type -testdata/Builtins.lc 438:95-438:115 Type -testdata/Builtins.lc 438:100-438:111 Nat -> Type->Type -testdata/Builtins.lc 438:100-438:113 Type->Type -testdata/Builtins.lc 438:100-438:115 Type -testdata/Builtins.lc 438:112-438:113 Nat -testdata/Builtins.lc 438:114-438:115 Type -testdata/Builtins.lc 440:1-440:11 {a:Nat} -> {b} -> {c} -> FragOps' b -> (c -> RemSemantics b) -> List (Vector a (Maybe (SimpleFragment c))) -> FrameBuffer a b -> FrameBuffer a b -testdata/Builtins.lc 440:34-440:44 {a:Nat} -> {b} -> FragOps' b -> List (Vector a (Maybe (SimpleFragment (RemSemantics b)))) -> FrameBuffer a b -> FrameBuffer a b -testdata/Builtins.lc 440:34-440:48 List (Vector V1 (Maybe (SimpleFragment (RemSemantics V0)))) -> FrameBuffer V2 V1 -> FrameBuffer V3 V2 -testdata/Builtins.lc 440:34-440:76 FrameBuffer V2 V1 -> FrameBuffer V3 V2 -testdata/Builtins.lc 440:34-440:79 FrameBuffer V2 V1 -testdata/Builtins.lc 440:45-440:48 V9 -testdata/Builtins.lc 440:49-440:76 List (Vector V2 (Maybe (SimpleFragment (RemSemantics V1)))) -testdata/Builtins.lc 440:50-440:62 {a} -> {b} -> {c:Nat} -> a->b -> List (Vector c (Maybe (SimpleFragment a))) -> List (Vector c (Maybe (SimpleFragment b))) -testdata/Builtins.lc 440:50-440:70 List (Vector V0 (Maybe (SimpleFragment V2))) -> List (Vector V1 (Maybe (SimpleFragment V2))) -testdata/Builtins.lc 440:63-440:70 V10 -testdata/Builtins.lc 440:71-440:75 V6 -testdata/Builtins.lc 440:77-440:79 V4 -testdata/Builtins.lc 442:1-442:20 {a} -> a->a -testdata/Builtins.lc 442:25-442:26 V1 -testdata/Builtins.lc 445:1-445:9 {a} -> FrameBuffer 1 a -> Image 1 a -testdata/Builtins.lc 445:24-445:35 Nat -> Type->Type -testdata/Builtins.lc 445:24-445:37 Type->Type -testdata/Builtins.lc 445:24-445:39 Type -testdata/Builtins.lc 445:24-445:52 Type -testdata/Builtins.lc 445:36-445:37 V1 -testdata/Builtins.lc 445:38-445:39 V1 -testdata/Builtins.lc 445:43-445:48 Nat -> Type->Type -testdata/Builtins.lc 445:43-445:50 Type->Type -testdata/Builtins.lc 445:43-445:52 Type -testdata/Builtins.lc 445:49-445:50 V1 -testdata/Builtins.lc 445:51-445:52 Type -testdata/Builtins.lc 446:1-446:14 FrameBuffer 1 (Tuple2 (Depth Float) (Color (VecS Float 4))) -> Image 1 (Color (VecS Float 4)) +testdata/Builtins.lc 412:1-412:11 {a:Nat} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : d ~ VecScalar b c} -> d -> Image a (Color d) +testdata/Builtins.lc 412:45-413:55 Type +testdata/Builtins.lc 412:46-412:49 Type->Type +testdata/Builtins.lc 412:46-412:51 Type +testdata/Builtins.lc 412:50-412:51 V3 +testdata/Builtins.lc 412:53-412:58 V2 +testdata/Builtins.lc 412:53-412:60 Type->Type +testdata/Builtins.lc 412:53-412:74 Type +testdata/Builtins.lc 412:53-413:55 Type +testdata/Builtins.lc 412:59-412:60 Type -> Type->Type +testdata/Builtins.lc 412:61-412:70 Nat -> Type->Type +testdata/Builtins.lc 412:61-412:72 Type->Type +testdata/Builtins.lc 412:61-412:74 Type +testdata/Builtins.lc 412:71-412:72 V4 +testdata/Builtins.lc 412:73-412:74 Type +testdata/Builtins.lc 413:24-413:29 Type +testdata/Builtins.lc 413:24-413:55 Type +testdata/Builtins.lc 413:34-413:39 Nat -> Type->Type +testdata/Builtins.lc 413:34-413:41 Type->Type +testdata/Builtins.lc 413:34-413:55 Type +testdata/Builtins.lc 413:40-413:41 V7 +testdata/Builtins.lc 413:42-413:55 Type +testdata/Builtins.lc 413:43-413:48 Type->Type +testdata/Builtins.lc 413:49-413:54 Type +testdata/Builtins.lc 414:1-414:11 {a:Nat} -> Float -> Image a (Depth Float) +testdata/Builtins.lc 414:35-414:40 Type +testdata/Builtins.lc 414:35-414:66 Type +testdata/Builtins.lc 414:45-414:50 Nat -> Type->Type +testdata/Builtins.lc 414:45-414:52 Type->Type +testdata/Builtins.lc 414:45-414:66 Type +testdata/Builtins.lc 414:51-414:52 V2 +testdata/Builtins.lc 414:53-414:66 Type +testdata/Builtins.lc 414:54-414:59 Type->Type +testdata/Builtins.lc 414:60-414:65 Type +testdata/Builtins.lc 415:1-415:13 {a:Nat} -> Int -> Image a (Stencil Int) +testdata/Builtins.lc 415:35-415:38 Type +testdata/Builtins.lc 415:35-415:66 Type +testdata/Builtins.lc 415:45-415:50 Nat -> Type->Type +testdata/Builtins.lc 415:45-415:52 Type->Type +testdata/Builtins.lc 415:45-415:66 Type +testdata/Builtins.lc 415:51-415:52 V2 +testdata/Builtins.lc 415:53-415:66 Type +testdata/Builtins.lc 415:54-415:61 Type->Type +testdata/Builtins.lc 415:62-415:65 Type +testdata/Builtins.lc 418:5-418:20 Type->Type +testdata/Builtins.lc 418:28-418:33 Type +testdata/Builtins.lc 418:28-418:41 Type->Type +testdata/Builtins.lc 418:28-420:99 Type | Type->Type +testdata/Builtins.lc 418:37-418:41 Nat -> Type->Type | Type | Type->Type +testdata/Builtins.lc 419:22-419:46 Type +testdata/Builtins.lc 419:22-419:64 Type->Type +testdata/Builtins.lc 419:22-420:99 Type +testdata/Builtins.lc 419:50-419:54 a:Type -> a -> a->Type +testdata/Builtins.lc 419:50-419:58 Nat -> Nat->Type +testdata/Builtins.lc 419:50-419:61 Nat->Type +testdata/Builtins.lc 419:50-419:64 Nat -> Type->Type | Type | Type -> Type->Type | Type->Type +testdata/Builtins.lc 419:55-419:58 Type +testdata/Builtins.lc 419:59-419:61 Nat +testdata/Builtins.lc 419:62-419:64 Nat +testdata/Builtins.lc 420:22-420:59 Type +testdata/Builtins.lc 420:22-420:99 Type->Type +testdata/Builtins.lc 420:63-420:65 Type -> Type->Type +testdata/Builtins.lc 420:63-420:82 Type->Type +testdata/Builtins.lc 420:63-420:99 Nat -> Type->Type | Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type +testdata/Builtins.lc 420:66-420:82 Type +testdata/Builtins.lc 420:67-420:71 a:Type -> a -> a->Type +testdata/Builtins.lc 420:67-420:75 Nat -> Nat->Type +testdata/Builtins.lc 420:67-420:78 Nat->Type +testdata/Builtins.lc 420:72-420:75 Type +testdata/Builtins.lc 420:76-420:78 Nat +testdata/Builtins.lc 420:79-420:81 Nat +testdata/Builtins.lc 420:83-420:99 Type +testdata/Builtins.lc 420:84-420:88 a:Type -> a -> a->Type +testdata/Builtins.lc 420:84-420:92 Nat -> Nat->Type +testdata/Builtins.lc 420:84-420:95 Nat->Type +testdata/Builtins.lc 420:89-420:92 Type +testdata/Builtins.lc 420:93-420:95 Nat +testdata/Builtins.lc 420:96-420:98 Nat +testdata/Builtins.lc 422:7-422:20 Type->Type +testdata/Builtins.lc 422:7-422:65 Type +testdata/Builtins.lc 422:29-422:42 {a} -> {b} -> {c : DefaultFragOp b} -> FragmentOperation b +testdata/Builtins.lc 422:46-422:63 Type->Type +testdata/Builtins.lc 422:46-422:65 Type +testdata/Builtins.lc 422:64-422:65 Type +testdata/Builtins.lc 423:37-423:42 Type +testdata/Builtins.lc 423:37-423:112 ({a : DefaultFragOp V1} -> FragmentOperation V2) -> {c : DefaultFragOp V2} -> FragmentOperation V3 +testdata/Builtins.lc 423:37-424:36 Type | Type->Type +testdata/Builtins.lc 423:37-424:77 {a : DefaultFragOp V1} -> FragmentOperation V2 | {a} -> {b : DefaultFragOp a} -> FragmentOperation a +testdata/Builtins.lc 423:69-423:76 {a} -> {b:Nat} -> {c} -> {d} -> {e : a ~ VecScalar b Bool} -> {f : c ~ VecScalar b d} -> {g : Num d} -> Blending d -> a -> FragmentOperation (Color c) +testdata/Builtins.lc 423:69-423:87 VecScalar V2 Bool -> FragmentOperation (Color (VecScalar V3 V2)) +testdata/Builtins.lc 423:69-423:112 FragmentOperation (Color (VecS V1 4)) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ ('Succ ('Succ a))))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ ('Succ ('Succ a)))))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ ('Succ a)))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ ('Succ a))))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ a))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ a)))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ a)))} -> FragmentOperation (Color (VecS Float ('Succ a))) | a:Nat -> {b : DefaultFragOp (Color (VecS V1 a))} -> FragmentOperation (Color (VecS V2 a)) | a:Type -> b:Nat -> {c : DefaultFragOp (Color (VecS a b))} -> FragmentOperation (Color (VecS a b)) | a:Type -> {b : DefaultFragOp (Color a)} -> FragmentOperation (Color a) +testdata/Builtins.lc 423:77-423:87 {a} -> Blending a +testdata/Builtins.lc 423:88-423:112 VecS Bool 4 +testdata/Builtins.lc 423:89-423:91 {a} -> a -> a -> a -> a -> VecS a 4 +testdata/Builtins.lc 423:89-423:96 Bool -> Bool -> Bool -> VecS Bool 4 +testdata/Builtins.lc 423:89-423:101 Bool -> Bool -> VecS Bool 4 +testdata/Builtins.lc 423:89-423:106 Bool -> VecS Bool 4 +testdata/Builtins.lc 423:92-423:96 Bool +testdata/Builtins.lc 423:97-423:101 Bool +testdata/Builtins.lc 423:102-423:106 Bool +testdata/Builtins.lc 423:107-423:111 Bool +testdata/Builtins.lc 424:31-424:36 Type +testdata/Builtins.lc 424:31-424:77 ({a : DefaultFragOp V1} -> FragmentOperation V2) -> {c : DefaultFragOp V2} -> FragmentOperation V3 +testdata/Builtins.lc 424:60-424:67 ComparisonFunction -> Bool -> FragmentOperation (Depth Float) +testdata/Builtins.lc 424:60-424:72 Bool -> FragmentOperation (Depth Float) +testdata/Builtins.lc 424:60-424:77 FragmentOperation (Depth Float) | a:Type -> {b : DefaultFragOp (Depth a)} -> FragmentOperation (Depth a) +testdata/Builtins.lc 424:68-424:72 ComparisonFunction +testdata/Builtins.lc 424:73-424:77 Bool +testdata/Builtins.lc 431:6-431:17 Nat -> Type->Type | Type +testdata/Builtins.lc 431:24-431:27 Type +testdata/Builtins.lc 432:1-432:11 {a} -> {b:Nat} -> FragOps a -> List (Vector b (Maybe (SimpleFragment (RemSemantics a)))) -> FrameBuffer b a -> FrameBuffer b a +testdata/Builtins.lc 432:15-432:22 Type->Type +testdata/Builtins.lc 432:15-432:24 Type +testdata/Builtins.lc 432:15-432:99 Type +testdata/Builtins.lc 432:23-432:24 V3 +testdata/Builtins.lc 432:28-432:42 Nat -> Type->Type +testdata/Builtins.lc 432:28-432:44 Type->Type +testdata/Builtins.lc 432:28-432:61 Type +testdata/Builtins.lc 432:28-432:99 Type +testdata/Builtins.lc 432:43-432:44 V2 +testdata/Builtins.lc 432:45-432:61 Type +testdata/Builtins.lc 432:46-432:58 Type->Type +testdata/Builtins.lc 432:59-432:60 Type +testdata/Builtins.lc 432:65-432:76 Nat -> Type->Type +testdata/Builtins.lc 432:65-432:78 Type->Type +testdata/Builtins.lc 432:65-432:80 Type +testdata/Builtins.lc 432:65-432:99 Type +testdata/Builtins.lc 432:77-432:78 Nat +testdata/Builtins.lc 432:79-432:80 Type +testdata/Builtins.lc 432:84-432:95 Nat -> Type->Type +testdata/Builtins.lc 432:84-432:97 Type->Type +testdata/Builtins.lc 432:84-432:99 Type +testdata/Builtins.lc 432:96-432:97 Nat +testdata/Builtins.lc 432:98-432:99 Type +testdata/Builtins.lc 435:5-435:18 Type->Type +testdata/Builtins.lc 435:26-435:31 Type +testdata/Builtins.lc 435:26-435:52 Type->Type +testdata/Builtins.lc 435:26-437:88 Type | Type->Type +testdata/Builtins.lc 435:35-435:46 Nat -> Type->Type +testdata/Builtins.lc 435:35-435:49 Type->Type +testdata/Builtins.lc 435:35-435:52 Nat -> Type->Type | Type | Type->Type +testdata/Builtins.lc 435:47-435:49 Nat +testdata/Builtins.lc 435:50-435:52 Type +testdata/Builtins.lc 436:20-436:44 Type +testdata/Builtins.lc 436:20-436:71 Type->Type +testdata/Builtins.lc 436:20-437:88 Type +testdata/Builtins.lc 436:48-436:59 Nat -> Type->Type +testdata/Builtins.lc 436:48-436:62 Type->Type +testdata/Builtins.lc 436:48-436:71 Nat -> Type->Type | Type | Type -> Type->Type | Type->Type +testdata/Builtins.lc 436:60-436:62 Nat +testdata/Builtins.lc 436:63-436:71 Type +testdata/Builtins.lc 436:64-436:66 Type +testdata/Builtins.lc 436:68-436:70 Type +testdata/Builtins.lc 437:20-437:57 Type +testdata/Builtins.lc 437:20-437:88 Type->Type +testdata/Builtins.lc 437:61-437:72 Nat -> Type->Type +testdata/Builtins.lc 437:61-437:75 Type->Type +testdata/Builtins.lc 437:61-437:88 Nat -> Type->Type | Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type +testdata/Builtins.lc 437:73-437:75 Nat +testdata/Builtins.lc 437:76-437:88 Type +testdata/Builtins.lc 437:77-437:79 Type +testdata/Builtins.lc 437:77-437:83 Type->Type +testdata/Builtins.lc 437:81-437:83 Type +testdata/Builtins.lc 437:85-437:87 Type +testdata/Builtins.lc 439:1-439:12 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a +testdata/Builtins.lc 439:17-439:115 Type +testdata/Builtins.lc 439:18-439:34 Type->Type +testdata/Builtins.lc 439:18-439:36 Type +testdata/Builtins.lc 439:35-439:36 V5 +testdata/Builtins.lc 439:38-439:53 Type->Type +testdata/Builtins.lc 439:38-439:55 Type +testdata/Builtins.lc 439:38-439:115 Type +testdata/Builtins.lc 439:54-439:55 V4 +testdata/Builtins.lc 439:57-439:68 Nat -> Type->Type +testdata/Builtins.lc 439:57-439:70 Type->Type +testdata/Builtins.lc 439:57-439:72 Type +testdata/Builtins.lc 439:57-439:74 Type->Type +testdata/Builtins.lc 439:57-439:90 Type +testdata/Builtins.lc 439:57-439:115 Type +testdata/Builtins.lc 439:69-439:70 V3 +testdata/Builtins.lc 439:71-439:72 Type +testdata/Builtins.lc 439:73-439:74 Type -> Type->Type +testdata/Builtins.lc 439:75-439:88 Type->Type +testdata/Builtins.lc 439:75-439:90 Type +testdata/Builtins.lc 439:89-439:90 Type +testdata/Builtins.lc 439:95-439:96 Type +testdata/Builtins.lc 439:95-439:115 Type +testdata/Builtins.lc 439:100-439:111 Nat -> Type->Type +testdata/Builtins.lc 439:100-439:113 Type->Type +testdata/Builtins.lc 439:100-439:115 Type +testdata/Builtins.lc 439:112-439:113 Nat +testdata/Builtins.lc 439:114-439:115 Type +testdata/Builtins.lc 441:1-441:11 {a} -> {b:Nat} -> {c} -> FragOps a -> (c -> RemSemantics a) -> List (Vector b (Maybe (SimpleFragment c))) -> FrameBuffer b a -> FrameBuffer b a +testdata/Builtins.lc 441:34-441:44 {a} -> {b:Nat} -> FragOps a -> List (Vector b (Maybe (SimpleFragment (RemSemantics a)))) -> FrameBuffer b a -> FrameBuffer b a +testdata/Builtins.lc 441:34-441:48 List (Vector V0 (Maybe (SimpleFragment (RemSemantics V1)))) -> FrameBuffer V1 V2 -> FrameBuffer V2 V3 +testdata/Builtins.lc 441:34-441:76 FrameBuffer V1 V2 -> FrameBuffer V2 V3 +testdata/Builtins.lc 441:34-441:79 FrameBuffer V1 V2 +testdata/Builtins.lc 441:45-441:48 V9 +testdata/Builtins.lc 441:49-441:76 List (Vector V1 (Maybe (SimpleFragment (RemSemantics V2)))) +testdata/Builtins.lc 441:50-441:62 {a} -> {b} -> {c:Nat} -> a->b -> List (Vector c (Maybe (SimpleFragment a))) -> List (Vector c (Maybe (SimpleFragment b))) +testdata/Builtins.lc 441:50-441:70 List (Vector V0 (Maybe (SimpleFragment V2))) -> List (Vector V1 (Maybe (SimpleFragment V2))) +testdata/Builtins.lc 441:63-441:70 V10 +testdata/Builtins.lc 441:71-441:75 V6 +testdata/Builtins.lc 441:77-441:79 V4 +testdata/Builtins.lc 443:1-443:20 {a} -> a->a +testdata/Builtins.lc 443:25-443:26 V1 +testdata/Builtins.lc 446:1-446:9 {a} -> FrameBuffer 1 a -> Image 1 a testdata/Builtins.lc 446:24-446:35 Nat -> Type->Type testdata/Builtins.lc 446:24-446:37 Type->Type -testdata/Builtins.lc 446:24-446:72 Type +testdata/Builtins.lc 446:24-446:39 Type +testdata/Builtins.lc 446:24-446:52 Type testdata/Builtins.lc 446:36-446:37 V1 -testdata/Builtins.lc 446:38-446:72 Type -testdata/Builtins.lc 446:39-446:44 Type->Type -testdata/Builtins.lc 446:39-446:50 Type -testdata/Builtins.lc 446:45-446:50 Type -testdata/Builtins.lc 446:52-446:57 Type->Type -testdata/Builtins.lc 446:52-446:71 Type -testdata/Builtins.lc 446:58-446:71 Type -testdata/Builtins.lc 446:59-446:62 Nat -> Type->Type -testdata/Builtins.lc 446:59-446:64 Type->Type -testdata/Builtins.lc 446:63-446:64 V1 -testdata/Builtins.lc 446:65-446:70 Type -testdata/Builtins.lc 446:76-446:81 Nat -> Type->Type -testdata/Builtins.lc 446:76-446:83 Type->Type -testdata/Builtins.lc 446:76-446:105 Type -testdata/Builtins.lc 446:82-446:83 V1 -testdata/Builtins.lc 446:84-446:105 Type -testdata/Builtins.lc 446:85-446:90 Type->Type -testdata/Builtins.lc 446:91-446:104 Type -testdata/Builtins.lc 446:92-446:95 Nat -> Type->Type -testdata/Builtins.lc 446:92-446:97 Type->Type -testdata/Builtins.lc 446:96-446:97 V1 -testdata/Builtins.lc 446:98-446:103 Type -testdata/Builtins.lc 448:6-448:12 Type -testdata/Builtins.lc 448:6-449:12 Type -testdata/Builtins.lc 449:3-449:12 Output | Type | {a:Nat} -> {b} -> FrameBuffer a b -> Output -testdata/Builtins.lc 449:26-449:37 Nat -> Type->Type -testdata/Builtins.lc 449:26-449:39 Type->Type -testdata/Builtins.lc 449:26-449:41 Type -testdata/Builtins.lc 449:26-449:51 Type -testdata/Builtins.lc 449:38-449:39 V3 -testdata/Builtins.lc 449:40-449:41 V1 -testdata/Builtins.lc 449:45-449:51 Type -testdata/Builtins.lc 455:1-455:8 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a -testdata/Builtins.lc 455:10-455:17 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a -testdata/Builtins.lc 455:19-455:26 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a -testdata/Builtins.lc 455:34-455:37 Type->Type -testdata/Builtins.lc 455:34-455:58 Type -testdata/Builtins.lc 455:34-455:73 Type -testdata/Builtins.lc 455:38-455:58 Type -testdata/Builtins.lc 455:39-455:55 Type->Type -testdata/Builtins.lc 455:56-455:57 V1 -testdata/Builtins.lc 455:62-455:63 Type -testdata/Builtins.lc 455:62-455:73 Type -testdata/Builtins.lc 455:67-455:68 Type -testdata/Builtins.lc 455:67-455:73 Type -testdata/Builtins.lc 455:72-455:73 Type -testdata/Builtins.lc 456:1-456:9 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b -testdata/Builtins.lc 456:11-456:19 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b -testdata/Builtins.lc 456:21-456:29 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b -testdata/Builtins.lc 456:34-456:80 Type -testdata/Builtins.lc 456:35-456:36 V3 -testdata/Builtins.lc 456:35-456:38 Type->Type -testdata/Builtins.lc 456:35-456:57 Type -testdata/Builtins.lc 456:37-456:38 Type -> Type->Type +testdata/Builtins.lc 446:38-446:39 V1 +testdata/Builtins.lc 446:43-446:48 Nat -> Type->Type +testdata/Builtins.lc 446:43-446:50 Type->Type +testdata/Builtins.lc 446:43-446:52 Type +testdata/Builtins.lc 446:49-446:50 V1 +testdata/Builtins.lc 446:51-446:52 Type +testdata/Builtins.lc 447:1-447:14 FrameBuffer 1 (Tuple2 (Depth Float) (Color (VecS Float 4))) -> Image 1 (Color (VecS Float 4)) +testdata/Builtins.lc 447:24-447:35 Nat -> Type->Type +testdata/Builtins.lc 447:24-447:37 Type->Type +testdata/Builtins.lc 447:24-447:72 Type +testdata/Builtins.lc 447:36-447:37 V1 +testdata/Builtins.lc 447:38-447:72 Type +testdata/Builtins.lc 447:39-447:44 Type->Type +testdata/Builtins.lc 447:39-447:50 Type +testdata/Builtins.lc 447:45-447:50 Type +testdata/Builtins.lc 447:52-447:57 Type->Type +testdata/Builtins.lc 447:52-447:71 Type +testdata/Builtins.lc 447:58-447:71 Type +testdata/Builtins.lc 447:59-447:62 Nat -> Type->Type +testdata/Builtins.lc 447:59-447:64 Type->Type +testdata/Builtins.lc 447:63-447:64 V1 +testdata/Builtins.lc 447:65-447:70 Type +testdata/Builtins.lc 447:76-447:81 Nat -> Type->Type +testdata/Builtins.lc 447:76-447:83 Type->Type +testdata/Builtins.lc 447:76-447:105 Type +testdata/Builtins.lc 447:82-447:83 V1 +testdata/Builtins.lc 447:84-447:105 Type +testdata/Builtins.lc 447:85-447:90 Type->Type +testdata/Builtins.lc 447:91-447:104 Type +testdata/Builtins.lc 447:92-447:95 Nat -> Type->Type +testdata/Builtins.lc 447:92-447:97 Type->Type +testdata/Builtins.lc 447:96-447:97 V1 +testdata/Builtins.lc 447:98-447:103 Type +testdata/Builtins.lc 449:6-449:12 Type +testdata/Builtins.lc 449:6-450:12 Type +testdata/Builtins.lc 450:3-450:12 Output | Type | {a:Nat} -> {b} -> FrameBuffer a b -> Output +testdata/Builtins.lc 450:26-450:37 Nat -> Type->Type +testdata/Builtins.lc 450:26-450:39 Type->Type +testdata/Builtins.lc 450:26-450:41 Type +testdata/Builtins.lc 450:26-450:51 Type +testdata/Builtins.lc 450:38-450:39 V3 +testdata/Builtins.lc 450:40-450:41 V1 +testdata/Builtins.lc 450:45-450:51 Type +testdata/Builtins.lc 456:1-456:8 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a +testdata/Builtins.lc 456:10-456:17 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a +testdata/Builtins.lc 456:19-456:26 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a +testdata/Builtins.lc 456:34-456:37 Type->Type +testdata/Builtins.lc 456:34-456:58 Type +testdata/Builtins.lc 456:34-456:73 Type +testdata/Builtins.lc 456:38-456:58 Type testdata/Builtins.lc 456:39-456:55 Type->Type -testdata/Builtins.lc 456:39-456:57 Type testdata/Builtins.lc 456:56-456:57 V1 -testdata/Builtins.lc 456:59-456:62 Type->Type -testdata/Builtins.lc 456:59-456:64 Type -testdata/Builtins.lc 456:59-456:80 Type -testdata/Builtins.lc 456:63-456:64 Type -testdata/Builtins.lc 456:69-456:70 Type -testdata/Builtins.lc 456:69-456:80 Type -testdata/Builtins.lc 456:74-456:75 Type -testdata/Builtins.lc 456:74-456:80 Type -testdata/Builtins.lc 456:79-456:80 Type -testdata/Builtins.lc 457:1-457:8 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b -testdata/Builtins.lc 457:10-457:17 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b -testdata/Builtins.lc 457:34-457:75 Type +testdata/Builtins.lc 456:62-456:63 Type +testdata/Builtins.lc 456:62-456:73 Type +testdata/Builtins.lc 456:67-456:68 Type +testdata/Builtins.lc 456:67-456:73 Type +testdata/Builtins.lc 456:72-456:73 Type +testdata/Builtins.lc 457:1-457:9 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b +testdata/Builtins.lc 457:11-457:19 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b +testdata/Builtins.lc 457:21-457:29 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b +testdata/Builtins.lc 457:34-457:80 Type +testdata/Builtins.lc 457:35-457:36 V3 testdata/Builtins.lc 457:35-457:38 Type->Type -testdata/Builtins.lc 457:35-457:40 Type -testdata/Builtins.lc 457:39-457:40 V5 -testdata/Builtins.lc 457:42-457:43 V4 -testdata/Builtins.lc 457:42-457:45 Type->Type -testdata/Builtins.lc 457:42-457:59 Type -testdata/Builtins.lc 457:42-457:75 Type -testdata/Builtins.lc 457:44-457:45 Type -> Type->Type -testdata/Builtins.lc 457:46-457:55 Nat -> Type->Type -testdata/Builtins.lc 457:46-457:57 Type->Type -testdata/Builtins.lc 457:46-457:59 Type -testdata/Builtins.lc 457:56-457:57 V2 -testdata/Builtins.lc 457:58-457:59 Type -testdata/Builtins.lc 457:64-457:65 Type -testdata/Builtins.lc 457:64-457:75 Type +testdata/Builtins.lc 457:35-457:57 Type +testdata/Builtins.lc 457:37-457:38 Type -> Type->Type +testdata/Builtins.lc 457:39-457:55 Type->Type +testdata/Builtins.lc 457:39-457:57 Type +testdata/Builtins.lc 457:56-457:57 V1 +testdata/Builtins.lc 457:59-457:62 Type->Type +testdata/Builtins.lc 457:59-457:64 Type +testdata/Builtins.lc 457:59-457:80 Type +testdata/Builtins.lc 457:63-457:64 Type testdata/Builtins.lc 457:69-457:70 Type -testdata/Builtins.lc 457:69-457:75 Type +testdata/Builtins.lc 457:69-457:80 Type testdata/Builtins.lc 457:74-457:75 Type -testdata/Builtins.lc 458:1-458:9 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b -testdata/Builtins.lc 458:11-458:19 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b +testdata/Builtins.lc 457:74-457:80 Type +testdata/Builtins.lc 457:79-457:80 Type +testdata/Builtins.lc 458:1-458:8 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b +testdata/Builtins.lc 458:10-458:17 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b testdata/Builtins.lc 458:34-458:75 Type testdata/Builtins.lc 458:35-458:38 Type->Type testdata/Builtins.lc 458:35-458:40 Type @@ -1859,41 +1830,40 @@ testdata/Builtins.lc 458:64-458:75 Type testdata/Builtins.lc 458:69-458:70 Type testdata/Builtins.lc 458:69-458:75 Type testdata/Builtins.lc 458:74-458:75 Type -testdata/Builtins.lc 459:1-459:8 {a} -> {b : Signed (MatVecScalarElem a)} -> a->a -testdata/Builtins.lc 459:34-459:40 Type->Type -testdata/Builtins.lc 459:34-459:61 Type -testdata/Builtins.lc 459:34-459:71 Type -testdata/Builtins.lc 459:41-459:61 Type -testdata/Builtins.lc 459:42-459:58 Type->Type -testdata/Builtins.lc 459:59-459:60 V1 -testdata/Builtins.lc 459:65-459:66 Type -testdata/Builtins.lc 459:65-459:71 Type -testdata/Builtins.lc 459:70-459:71 Type -testdata/Builtins.lc 461:1-461:9 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b -testdata/Builtins.lc 461:11-461:18 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b -testdata/Builtins.lc 461:20-461:28 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b -testdata/Builtins.lc 461:34-461:80 Type -testdata/Builtins.lc 461:35-461:43 Type->Type -testdata/Builtins.lc 461:35-461:45 Type -testdata/Builtins.lc 461:44-461:45 V5 -testdata/Builtins.lc 461:47-461:48 V4 -testdata/Builtins.lc 461:47-461:50 Type->Type -testdata/Builtins.lc 461:47-461:64 Type -testdata/Builtins.lc 461:47-461:80 Type -testdata/Builtins.lc 461:49-461:50 Type -> Type->Type -testdata/Builtins.lc 461:51-461:60 Nat -> Type->Type -testdata/Builtins.lc 461:51-461:62 Type->Type -testdata/Builtins.lc 461:51-461:64 Type -testdata/Builtins.lc 461:61-461:62 V2 -testdata/Builtins.lc 461:63-461:64 Type -testdata/Builtins.lc 461:69-461:70 Type -testdata/Builtins.lc 461:69-461:80 Type -testdata/Builtins.lc 461:74-461:75 Type -testdata/Builtins.lc 461:74-461:80 Type -testdata/Builtins.lc 461:79-461:80 Type -testdata/Builtins.lc 462:1-462:10 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b -testdata/Builtins.lc 462:12-462:20 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b -testdata/Builtins.lc 462:22-462:31 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b +testdata/Builtins.lc 459:1-459:9 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b +testdata/Builtins.lc 459:11-459:19 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b +testdata/Builtins.lc 459:34-459:75 Type +testdata/Builtins.lc 459:35-459:38 Type->Type +testdata/Builtins.lc 459:35-459:40 Type +testdata/Builtins.lc 459:39-459:40 V5 +testdata/Builtins.lc 459:42-459:43 V4 +testdata/Builtins.lc 459:42-459:45 Type->Type +testdata/Builtins.lc 459:42-459:59 Type +testdata/Builtins.lc 459:42-459:75 Type +testdata/Builtins.lc 459:44-459:45 Type -> Type->Type +testdata/Builtins.lc 459:46-459:55 Nat -> Type->Type +testdata/Builtins.lc 459:46-459:57 Type->Type +testdata/Builtins.lc 459:46-459:59 Type +testdata/Builtins.lc 459:56-459:57 V2 +testdata/Builtins.lc 459:58-459:59 Type +testdata/Builtins.lc 459:64-459:65 Type +testdata/Builtins.lc 459:64-459:75 Type +testdata/Builtins.lc 459:69-459:70 Type +testdata/Builtins.lc 459:69-459:75 Type +testdata/Builtins.lc 459:74-459:75 Type +testdata/Builtins.lc 460:1-460:8 {a} -> {b : Signed (MatVecScalarElem a)} -> a->a +testdata/Builtins.lc 460:34-460:40 Type->Type +testdata/Builtins.lc 460:34-460:61 Type +testdata/Builtins.lc 460:34-460:71 Type +testdata/Builtins.lc 460:41-460:61 Type +testdata/Builtins.lc 460:42-460:58 Type->Type +testdata/Builtins.lc 460:59-460:60 V1 +testdata/Builtins.lc 460:65-460:66 Type +testdata/Builtins.lc 460:65-460:71 Type +testdata/Builtins.lc 460:70-460:71 Type +testdata/Builtins.lc 462:1-462:9 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b +testdata/Builtins.lc 462:11-462:18 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b +testdata/Builtins.lc 462:20-462:28 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b testdata/Builtins.lc 462:34-462:80 Type testdata/Builtins.lc 462:35-462:43 Type->Type testdata/Builtins.lc 462:35-462:45 Type @@ -1913,15 +1883,17 @@ testdata/Builtins.lc 462:69-462:80 Type testdata/Builtins.lc 462:74-462:75 Type testdata/Builtins.lc 462:74-462:80 Type testdata/Builtins.lc 462:79-462:80 Type -testdata/Builtins.lc 463:1-463:9 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b->b -testdata/Builtins.lc 463:34-463:75 Type +testdata/Builtins.lc 463:1-463:10 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b +testdata/Builtins.lc 463:12-463:20 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b +testdata/Builtins.lc 463:22-463:31 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b +testdata/Builtins.lc 463:34-463:80 Type testdata/Builtins.lc 463:35-463:43 Type->Type testdata/Builtins.lc 463:35-463:45 Type testdata/Builtins.lc 463:44-463:45 V5 testdata/Builtins.lc 463:47-463:48 V4 testdata/Builtins.lc 463:47-463:50 Type->Type testdata/Builtins.lc 463:47-463:64 Type -testdata/Builtins.lc 463:47-463:75 Type +testdata/Builtins.lc 463:47-463:80 Type testdata/Builtins.lc 463:49-463:50 Type -> Type->Type testdata/Builtins.lc 463:51-463:60 Nat -> Type->Type testdata/Builtins.lc 463:51-463:62 Type->Type @@ -1929,127 +1901,132 @@ testdata/Builtins.lc 463:51-463:64 Type testdata/Builtins.lc 463:61-463:62 V2 testdata/Builtins.lc 463:63-463:64 Type testdata/Builtins.lc 463:69-463:70 Type -testdata/Builtins.lc 463:69-463:75 Type +testdata/Builtins.lc 463:69-463:80 Type testdata/Builtins.lc 463:74-463:75 Type -testdata/Builtins.lc 464:1-464:12 {a} -> {b} -> {c:Nat} -> {d} -> {e : Integral a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Word} -> b -> d->b -testdata/Builtins.lc 464:14-464:25 {a} -> {b} -> {c:Nat} -> {d} -> {e : Integral a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Word} -> b -> d->b -testdata/Builtins.lc 464:34-464:102 Type +testdata/Builtins.lc 463:74-463:80 Type +testdata/Builtins.lc 463:79-463:80 Type +testdata/Builtins.lc 464:1-464:9 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b->b +testdata/Builtins.lc 464:34-464:75 Type testdata/Builtins.lc 464:35-464:43 Type->Type testdata/Builtins.lc 464:35-464:45 Type -testdata/Builtins.lc 464:44-464:45 V7 -testdata/Builtins.lc 464:47-464:48 V6 +testdata/Builtins.lc 464:44-464:45 V5 +testdata/Builtins.lc 464:47-464:48 V4 testdata/Builtins.lc 464:47-464:50 Type->Type testdata/Builtins.lc 464:47-464:64 Type -testdata/Builtins.lc 464:47-464:102 Type +testdata/Builtins.lc 464:47-464:75 Type testdata/Builtins.lc 464:49-464:50 Type -> Type->Type testdata/Builtins.lc 464:51-464:60 Nat -> Type->Type testdata/Builtins.lc 464:51-464:62 Type->Type testdata/Builtins.lc 464:51-464:64 Type -testdata/Builtins.lc 464:61-464:62 V4 +testdata/Builtins.lc 464:61-464:62 V2 testdata/Builtins.lc 464:63-464:64 Type -testdata/Builtins.lc 464:66-464:67 V3 -testdata/Builtins.lc 464:66-464:69 Type->Type -testdata/Builtins.lc 464:66-464:86 Type -testdata/Builtins.lc 464:66-464:102 Type -testdata/Builtins.lc 464:68-464:69 Type -> Type->Type -testdata/Builtins.lc 464:70-464:79 Nat -> Type->Type -testdata/Builtins.lc 464:70-464:81 Type->Type -testdata/Builtins.lc 464:70-464:86 Type -testdata/Builtins.lc 464:80-464:81 Nat -testdata/Builtins.lc 464:82-464:86 Type -testdata/Builtins.lc 464:91-464:92 Type -testdata/Builtins.lc 464:91-464:102 Type -testdata/Builtins.lc 464:96-464:97 Type -testdata/Builtins.lc 464:96-464:102 Type -testdata/Builtins.lc 464:101-464:102 Type -testdata/Builtins.lc 465:1-465:13 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> Word->b -testdata/Builtins.lc 465:15-465:27 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> Word->b -testdata/Builtins.lc 465:34-465:83 Type +testdata/Builtins.lc 464:69-464:70 Type +testdata/Builtins.lc 464:69-464:75 Type +testdata/Builtins.lc 464:74-464:75 Type +testdata/Builtins.lc 465:1-465:12 {a} -> {b} -> {c:Nat} -> {d} -> {e : Integral a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Word} -> b -> d->b +testdata/Builtins.lc 465:14-465:25 {a} -> {b} -> {c:Nat} -> {d} -> {e : Integral a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Word} -> b -> d->b +testdata/Builtins.lc 465:34-465:102 Type testdata/Builtins.lc 465:35-465:43 Type->Type testdata/Builtins.lc 465:35-465:45 Type -testdata/Builtins.lc 465:44-465:45 V5 -testdata/Builtins.lc 465:47-465:48 V4 +testdata/Builtins.lc 465:44-465:45 V7 +testdata/Builtins.lc 465:47-465:48 V6 testdata/Builtins.lc 465:47-465:50 Type->Type testdata/Builtins.lc 465:47-465:64 Type -testdata/Builtins.lc 465:47-465:83 Type +testdata/Builtins.lc 465:47-465:102 Type testdata/Builtins.lc 465:49-465:50 Type -> Type->Type testdata/Builtins.lc 465:51-465:60 Nat -> Type->Type testdata/Builtins.lc 465:51-465:62 Type->Type testdata/Builtins.lc 465:51-465:64 Type -testdata/Builtins.lc 465:61-465:62 V2 +testdata/Builtins.lc 465:61-465:62 V4 testdata/Builtins.lc 465:63-465:64 Type -testdata/Builtins.lc 465:69-465:70 Type -testdata/Builtins.lc 465:69-465:83 Type -testdata/Builtins.lc 465:74-465:78 Type -testdata/Builtins.lc 465:74-465:83 Type -testdata/Builtins.lc 465:82-465:83 Type -testdata/Builtins.lc 467:1-467:8 Bool -> Bool->Bool -testdata/Builtins.lc 467:10-467:16 Bool -> Bool->Bool -testdata/Builtins.lc 467:18-467:25 Bool -> Bool->Bool -testdata/Builtins.lc 467:34-467:38 Type -testdata/Builtins.lc 467:42-467:46 Type -testdata/Builtins.lc 467:42-467:54 Type -testdata/Builtins.lc 467:50-467:54 Type -testdata/Builtins.lc 468:1-468:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Bool} -> a->a -testdata/Builtins.lc 468:34-468:56 Type -testdata/Builtins.lc 468:34-468:66 Type -testdata/Builtins.lc 468:35-468:36 V3 -testdata/Builtins.lc 468:35-468:38 Type->Type -testdata/Builtins.lc 468:37-468:38 Type -> Type->Type -testdata/Builtins.lc 468:39-468:48 Nat -> Type->Type -testdata/Builtins.lc 468:39-468:50 Type->Type -testdata/Builtins.lc 468:39-468:55 Type -testdata/Builtins.lc 468:49-468:50 V1 -testdata/Builtins.lc 468:51-468:55 Type -testdata/Builtins.lc 468:60-468:61 Type -testdata/Builtins.lc 468:60-468:66 Type -testdata/Builtins.lc 468:65-468:66 Type -testdata/Builtins.lc 469:1-469:8 {a:Nat} -> VecScalar a Bool -> Bool -testdata/Builtins.lc 469:10-469:17 {a:Nat} -> VecScalar a Bool -> Bool -testdata/Builtins.lc 469:34-469:43 Nat -> Type->Type -testdata/Builtins.lc 469:34-469:45 Type->Type -testdata/Builtins.lc 469:34-469:50 Type -testdata/Builtins.lc 469:34-469:58 Type -testdata/Builtins.lc 469:44-469:45 V1 -testdata/Builtins.lc 469:46-469:50 Type -testdata/Builtins.lc 469:54-469:58 Type -testdata/Builtins.lc 472:1-472:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:11-472:20 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:22-472:30 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:32-472:41 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:43-472:51 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:53-472:62 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:64-472:71 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:73-472:81 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:83-472:94 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:96-472:107 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:109-472:116 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:118-472:126 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:128-472:135 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:137-472:145 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:147-472:154 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:156-472:163 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:165-472:173 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:175-472:183 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:185-472:193 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 472:195-472:206 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 473:34-473:57 Type -testdata/Builtins.lc 473:34-473:67 Type -testdata/Builtins.lc 473:35-473:36 V3 -testdata/Builtins.lc 473:35-473:38 Type->Type -testdata/Builtins.lc 473:37-473:38 Type -> Type->Type -testdata/Builtins.lc 473:39-473:48 Nat -> Type->Type -testdata/Builtins.lc 473:39-473:50 Type->Type -testdata/Builtins.lc 473:39-473:56 Type -testdata/Builtins.lc 473:49-473:50 V1 -testdata/Builtins.lc 473:51-473:56 Type -testdata/Builtins.lc 473:61-473:62 Type -testdata/Builtins.lc 473:61-473:67 Type -testdata/Builtins.lc 473:66-473:67 Type -testdata/Builtins.lc 474:1-474:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a -testdata/Builtins.lc 474:10-474:19 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a +testdata/Builtins.lc 465:66-465:67 V3 +testdata/Builtins.lc 465:66-465:69 Type->Type +testdata/Builtins.lc 465:66-465:86 Type +testdata/Builtins.lc 465:66-465:102 Type +testdata/Builtins.lc 465:68-465:69 Type -> Type->Type +testdata/Builtins.lc 465:70-465:79 Nat -> Type->Type +testdata/Builtins.lc 465:70-465:81 Type->Type +testdata/Builtins.lc 465:70-465:86 Type +testdata/Builtins.lc 465:80-465:81 Nat +testdata/Builtins.lc 465:82-465:86 Type +testdata/Builtins.lc 465:91-465:92 Type +testdata/Builtins.lc 465:91-465:102 Type +testdata/Builtins.lc 465:96-465:97 Type +testdata/Builtins.lc 465:96-465:102 Type +testdata/Builtins.lc 465:101-465:102 Type +testdata/Builtins.lc 466:1-466:13 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> Word->b +testdata/Builtins.lc 466:15-466:27 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> Word->b +testdata/Builtins.lc 466:34-466:83 Type +testdata/Builtins.lc 466:35-466:43 Type->Type +testdata/Builtins.lc 466:35-466:45 Type +testdata/Builtins.lc 466:44-466:45 V5 +testdata/Builtins.lc 466:47-466:48 V4 +testdata/Builtins.lc 466:47-466:50 Type->Type +testdata/Builtins.lc 466:47-466:64 Type +testdata/Builtins.lc 466:47-466:83 Type +testdata/Builtins.lc 466:49-466:50 Type -> Type->Type +testdata/Builtins.lc 466:51-466:60 Nat -> Type->Type +testdata/Builtins.lc 466:51-466:62 Type->Type +testdata/Builtins.lc 466:51-466:64 Type +testdata/Builtins.lc 466:61-466:62 V2 +testdata/Builtins.lc 466:63-466:64 Type +testdata/Builtins.lc 466:69-466:70 Type +testdata/Builtins.lc 466:69-466:83 Type +testdata/Builtins.lc 466:74-466:78 Type +testdata/Builtins.lc 466:74-466:83 Type +testdata/Builtins.lc 466:82-466:83 Type +testdata/Builtins.lc 468:1-468:8 Bool -> Bool->Bool +testdata/Builtins.lc 468:10-468:16 Bool -> Bool->Bool +testdata/Builtins.lc 468:18-468:25 Bool -> Bool->Bool +testdata/Builtins.lc 468:34-468:38 Type +testdata/Builtins.lc 468:42-468:46 Type +testdata/Builtins.lc 468:42-468:54 Type +testdata/Builtins.lc 468:50-468:54 Type +testdata/Builtins.lc 469:1-469:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Bool} -> a->a +testdata/Builtins.lc 469:34-469:56 Type +testdata/Builtins.lc 469:34-469:66 Type +testdata/Builtins.lc 469:35-469:36 V3 +testdata/Builtins.lc 469:35-469:38 Type->Type +testdata/Builtins.lc 469:37-469:38 Type -> Type->Type +testdata/Builtins.lc 469:39-469:48 Nat -> Type->Type +testdata/Builtins.lc 469:39-469:50 Type->Type +testdata/Builtins.lc 469:39-469:55 Type +testdata/Builtins.lc 469:49-469:50 V1 +testdata/Builtins.lc 469:51-469:55 Type +testdata/Builtins.lc 469:60-469:61 Type +testdata/Builtins.lc 469:60-469:66 Type +testdata/Builtins.lc 469:65-469:66 Type +testdata/Builtins.lc 470:1-470:8 {a:Nat} -> VecScalar a Bool -> Bool +testdata/Builtins.lc 470:10-470:17 {a:Nat} -> VecScalar a Bool -> Bool +testdata/Builtins.lc 470:34-470:43 Nat -> Type->Type +testdata/Builtins.lc 470:34-470:45 Type->Type +testdata/Builtins.lc 470:34-470:50 Type +testdata/Builtins.lc 470:34-470:58 Type +testdata/Builtins.lc 470:44-470:45 V1 +testdata/Builtins.lc 470:46-470:50 Type +testdata/Builtins.lc 470:54-470:58 Type +testdata/Builtins.lc 473:1-473:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:11-473:20 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:22-473:30 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:32-473:41 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:43-473:51 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:53-473:62 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:64-473:71 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:73-473:81 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:83-473:94 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:96-473:107 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:109-473:116 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:118-473:126 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:128-473:135 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:137-473:145 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:147-473:154 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:156-473:163 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:165-473:173 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:175-473:183 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:185-473:193 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 473:195-473:206 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a testdata/Builtins.lc 474:34-474:57 Type -testdata/Builtins.lc 474:34-474:72 Type +testdata/Builtins.lc 474:34-474:67 Type testdata/Builtins.lc 474:35-474:36 V3 testdata/Builtins.lc 474:35-474:38 Type->Type testdata/Builtins.lc 474:37-474:38 Type -> Type->Type @@ -2059,52 +2036,46 @@ testdata/Builtins.lc 474:39-474:56 Type testdata/Builtins.lc 474:49-474:50 V1 testdata/Builtins.lc 474:51-474:56 Type testdata/Builtins.lc 474:61-474:62 Type -testdata/Builtins.lc 474:61-474:72 Type +testdata/Builtins.lc 474:61-474:67 Type testdata/Builtins.lc 474:66-474:67 Type -testdata/Builtins.lc 474:66-474:72 Type -testdata/Builtins.lc 474:71-474:72 Type -testdata/Builtins.lc 476:1-476:10 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 476:12-476:21 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 476:23-476:32 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 476:34-476:47 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 476:49-476:57 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 476:59-476:68 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 477:34-477:57 Type -testdata/Builtins.lc 477:34-477:67 Type -testdata/Builtins.lc 477:35-477:36 V3 -testdata/Builtins.lc 477:35-477:38 Type->Type -testdata/Builtins.lc 477:37-477:38 Type -> Type->Type -testdata/Builtins.lc 477:39-477:48 Nat -> Type->Type -testdata/Builtins.lc 477:39-477:50 Type->Type -testdata/Builtins.lc 477:39-477:56 Type -testdata/Builtins.lc 477:49-477:50 V1 -testdata/Builtins.lc 477:51-477:56 Type -testdata/Builtins.lc 477:61-477:62 Type -testdata/Builtins.lc 477:61-477:67 Type -testdata/Builtins.lc 477:66-477:67 Type -testdata/Builtins.lc 478:1-478:8 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b -testdata/Builtins.lc 478:10-478:17 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b -testdata/Builtins.lc 478:34-478:75 Type +testdata/Builtins.lc 475:1-475:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a +testdata/Builtins.lc 475:10-475:19 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a +testdata/Builtins.lc 475:34-475:57 Type +testdata/Builtins.lc 475:34-475:72 Type +testdata/Builtins.lc 475:35-475:36 V3 +testdata/Builtins.lc 475:35-475:38 Type->Type +testdata/Builtins.lc 475:37-475:38 Type -> Type->Type +testdata/Builtins.lc 475:39-475:48 Nat -> Type->Type +testdata/Builtins.lc 475:39-475:50 Type->Type +testdata/Builtins.lc 475:39-475:56 Type +testdata/Builtins.lc 475:49-475:50 V1 +testdata/Builtins.lc 475:51-475:56 Type +testdata/Builtins.lc 475:61-475:62 Type +testdata/Builtins.lc 475:61-475:72 Type +testdata/Builtins.lc 475:66-475:67 Type +testdata/Builtins.lc 475:66-475:72 Type +testdata/Builtins.lc 475:71-475:72 Type +testdata/Builtins.lc 477:1-477:10 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 477:12-477:21 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 477:23-477:32 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 477:34-477:47 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 477:49-477:57 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 477:59-477:68 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 478:34-478:57 Type +testdata/Builtins.lc 478:34-478:67 Type +testdata/Builtins.lc 478:35-478:36 V3 testdata/Builtins.lc 478:35-478:38 Type->Type -testdata/Builtins.lc 478:35-478:40 Type -testdata/Builtins.lc 478:39-478:40 V5 -testdata/Builtins.lc 478:42-478:43 V4 -testdata/Builtins.lc 478:42-478:45 Type->Type -testdata/Builtins.lc 478:42-478:59 Type -testdata/Builtins.lc 478:42-478:75 Type -testdata/Builtins.lc 478:44-478:45 Type -> Type->Type -testdata/Builtins.lc 478:46-478:55 Nat -> Type->Type -testdata/Builtins.lc 478:46-478:57 Type->Type -testdata/Builtins.lc 478:46-478:59 Type -testdata/Builtins.lc 478:56-478:57 V2 -testdata/Builtins.lc 478:58-478:59 Type -testdata/Builtins.lc 478:64-478:65 Type -testdata/Builtins.lc 478:64-478:75 Type -testdata/Builtins.lc 478:69-478:70 Type -testdata/Builtins.lc 478:69-478:75 Type -testdata/Builtins.lc 478:74-478:75 Type -testdata/Builtins.lc 479:1-479:9 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b -testdata/Builtins.lc 479:11-479:19 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b +testdata/Builtins.lc 478:37-478:38 Type -> Type->Type +testdata/Builtins.lc 478:39-478:48 Nat -> Type->Type +testdata/Builtins.lc 478:39-478:50 Type->Type +testdata/Builtins.lc 478:39-478:56 Type +testdata/Builtins.lc 478:49-478:50 V1 +testdata/Builtins.lc 478:51-478:56 Type +testdata/Builtins.lc 478:61-478:62 Type +testdata/Builtins.lc 478:61-478:67 Type +testdata/Builtins.lc 478:66-478:67 Type +testdata/Builtins.lc 479:1-479:8 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b +testdata/Builtins.lc 479:10-479:17 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b testdata/Builtins.lc 479:34-479:75 Type testdata/Builtins.lc 479:35-479:38 Type->Type testdata/Builtins.lc 479:35-479:40 Type @@ -2124,89 +2095,88 @@ testdata/Builtins.lc 479:64-479:75 Type testdata/Builtins.lc 479:69-479:70 Type testdata/Builtins.lc 479:69-479:75 Type testdata/Builtins.lc 479:74-479:75 Type -testdata/Builtins.lc 480:1-480:10 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c -testdata/Builtins.lc 480:12-480:21 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c -testdata/Builtins.lc 480:34-480:89 Type -testdata/Builtins.lc 480:35-480:36 V5 +testdata/Builtins.lc 480:1-480:9 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b +testdata/Builtins.lc 480:11-480:19 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b +testdata/Builtins.lc 480:34-480:75 Type testdata/Builtins.lc 480:35-480:38 Type->Type -testdata/Builtins.lc 480:35-480:56 Type -testdata/Builtins.lc 480:37-480:38 Type -> Type->Type -testdata/Builtins.lc 480:39-480:48 Nat -> Type->Type -testdata/Builtins.lc 480:39-480:50 Type->Type -testdata/Builtins.lc 480:39-480:56 Type -testdata/Builtins.lc 480:49-480:50 V3 -testdata/Builtins.lc 480:51-480:56 Type -testdata/Builtins.lc 480:58-480:59 V2 -testdata/Builtins.lc 480:58-480:61 Type->Type -testdata/Builtins.lc 480:58-480:78 Type -testdata/Builtins.lc 480:58-480:89 Type -testdata/Builtins.lc 480:60-480:61 Type -> Type->Type -testdata/Builtins.lc 480:62-480:71 Nat -> Type->Type -testdata/Builtins.lc 480:62-480:73 Type->Type -testdata/Builtins.lc 480:62-480:78 Type -testdata/Builtins.lc 480:72-480:73 Nat -testdata/Builtins.lc 480:74-480:78 Type -testdata/Builtins.lc 480:83-480:84 Type -testdata/Builtins.lc 480:83-480:89 Type -testdata/Builtins.lc 480:88-480:89 Type -testdata/Builtins.lc 481:1-481:8 {a} -> {b} -> {c:Nat} -> {d : Signed a} -> {e : b ~ VecScalar c a} -> b->b -testdata/Builtins.lc 481:10-481:18 {a} -> {b} -> {c:Nat} -> {d : Signed a} -> {e : b ~ VecScalar c a} -> b->b -testdata/Builtins.lc 481:34-481:73 Type -testdata/Builtins.lc 481:35-481:41 Type->Type -testdata/Builtins.lc 481:35-481:43 Type -testdata/Builtins.lc 481:42-481:43 V5 -testdata/Builtins.lc 481:45-481:46 V4 -testdata/Builtins.lc 481:45-481:48 Type->Type -testdata/Builtins.lc 481:45-481:62 Type -testdata/Builtins.lc 481:45-481:73 Type -testdata/Builtins.lc 481:47-481:48 Type -> Type->Type -testdata/Builtins.lc 481:49-481:58 Nat -> Type->Type -testdata/Builtins.lc 481:49-481:60 Type->Type -testdata/Builtins.lc 481:49-481:62 Type -testdata/Builtins.lc 481:59-481:60 V2 -testdata/Builtins.lc 481:61-481:62 Type -testdata/Builtins.lc 481:67-481:68 Type -testdata/Builtins.lc 481:67-481:73 Type -testdata/Builtins.lc 481:72-481:73 Type -testdata/Builtins.lc 482:1-482:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> Tuple2 a a -testdata/Builtins.lc 482:34-482:57 Type -testdata/Builtins.lc 482:34-482:72 Type -testdata/Builtins.lc 482:35-482:36 V3 -testdata/Builtins.lc 482:35-482:38 Type->Type -testdata/Builtins.lc 482:37-482:38 Type -> Type->Type -testdata/Builtins.lc 482:39-482:48 Nat -> Type->Type -testdata/Builtins.lc 482:39-482:50 Type->Type -testdata/Builtins.lc 482:39-482:56 Type -testdata/Builtins.lc 482:49-482:50 V1 -testdata/Builtins.lc 482:51-482:56 Type +testdata/Builtins.lc 480:35-480:40 Type +testdata/Builtins.lc 480:39-480:40 V5 +testdata/Builtins.lc 480:42-480:43 V4 +testdata/Builtins.lc 480:42-480:45 Type->Type +testdata/Builtins.lc 480:42-480:59 Type +testdata/Builtins.lc 480:42-480:75 Type +testdata/Builtins.lc 480:44-480:45 Type -> Type->Type +testdata/Builtins.lc 480:46-480:55 Nat -> Type->Type +testdata/Builtins.lc 480:46-480:57 Type->Type +testdata/Builtins.lc 480:46-480:59 Type +testdata/Builtins.lc 480:56-480:57 V2 +testdata/Builtins.lc 480:58-480:59 Type +testdata/Builtins.lc 480:64-480:65 Type +testdata/Builtins.lc 480:64-480:75 Type +testdata/Builtins.lc 480:69-480:70 Type +testdata/Builtins.lc 480:69-480:75 Type +testdata/Builtins.lc 480:74-480:75 Type +testdata/Builtins.lc 481:1-481:10 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c +testdata/Builtins.lc 481:12-481:21 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c +testdata/Builtins.lc 481:34-481:89 Type +testdata/Builtins.lc 481:35-481:36 V5 +testdata/Builtins.lc 481:35-481:38 Type->Type +testdata/Builtins.lc 481:35-481:56 Type +testdata/Builtins.lc 481:37-481:38 Type -> Type->Type +testdata/Builtins.lc 481:39-481:48 Nat -> Type->Type +testdata/Builtins.lc 481:39-481:50 Type->Type +testdata/Builtins.lc 481:39-481:56 Type +testdata/Builtins.lc 481:49-481:50 V3 +testdata/Builtins.lc 481:51-481:56 Type +testdata/Builtins.lc 481:58-481:59 V2 +testdata/Builtins.lc 481:58-481:61 Type->Type +testdata/Builtins.lc 481:58-481:78 Type +testdata/Builtins.lc 481:58-481:89 Type +testdata/Builtins.lc 481:60-481:61 Type -> Type->Type +testdata/Builtins.lc 481:62-481:71 Nat -> Type->Type +testdata/Builtins.lc 481:62-481:73 Type->Type +testdata/Builtins.lc 481:62-481:78 Type +testdata/Builtins.lc 481:72-481:73 Nat +testdata/Builtins.lc 481:74-481:78 Type +testdata/Builtins.lc 481:83-481:84 Type +testdata/Builtins.lc 481:83-481:89 Type +testdata/Builtins.lc 481:88-481:89 Type +testdata/Builtins.lc 482:1-482:8 {a} -> {b} -> {c:Nat} -> {d : Signed a} -> {e : b ~ VecScalar c a} -> b->b +testdata/Builtins.lc 482:10-482:18 {a} -> {b} -> {c:Nat} -> {d : Signed a} -> {e : b ~ VecScalar c a} -> b->b +testdata/Builtins.lc 482:34-482:73 Type +testdata/Builtins.lc 482:35-482:41 Type->Type +testdata/Builtins.lc 482:35-482:43 Type +testdata/Builtins.lc 482:42-482:43 V5 +testdata/Builtins.lc 482:45-482:46 V4 +testdata/Builtins.lc 482:45-482:48 Type->Type +testdata/Builtins.lc 482:45-482:62 Type +testdata/Builtins.lc 482:45-482:73 Type +testdata/Builtins.lc 482:47-482:48 Type -> Type->Type +testdata/Builtins.lc 482:49-482:58 Nat -> Type->Type +testdata/Builtins.lc 482:49-482:60 Type->Type +testdata/Builtins.lc 482:49-482:62 Type +testdata/Builtins.lc 482:59-482:60 V2 testdata/Builtins.lc 482:61-482:62 Type -testdata/Builtins.lc 482:61-482:72 Type -testdata/Builtins.lc 482:66-482:72 Type testdata/Builtins.lc 482:67-482:68 Type -testdata/Builtins.lc 482:70-482:71 Type -testdata/Builtins.lc 483:1-483:10 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b -> b->b -testdata/Builtins.lc 483:34-483:80 Type +testdata/Builtins.lc 482:67-482:73 Type +testdata/Builtins.lc 482:72-482:73 Type +testdata/Builtins.lc 483:1-483:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> Tuple2 a a +testdata/Builtins.lc 483:34-483:57 Type +testdata/Builtins.lc 483:34-483:72 Type +testdata/Builtins.lc 483:35-483:36 V3 testdata/Builtins.lc 483:35-483:38 Type->Type -testdata/Builtins.lc 483:35-483:40 Type -testdata/Builtins.lc 483:39-483:40 V5 -testdata/Builtins.lc 483:42-483:43 V4 -testdata/Builtins.lc 483:42-483:45 Type->Type -testdata/Builtins.lc 483:42-483:59 Type -testdata/Builtins.lc 483:42-483:80 Type -testdata/Builtins.lc 483:44-483:45 Type -> Type->Type -testdata/Builtins.lc 483:46-483:55 Nat -> Type->Type -testdata/Builtins.lc 483:46-483:57 Type->Type -testdata/Builtins.lc 483:46-483:59 Type -testdata/Builtins.lc 483:56-483:57 V2 -testdata/Builtins.lc 483:58-483:59 Type -testdata/Builtins.lc 483:64-483:65 Type -testdata/Builtins.lc 483:64-483:80 Type -testdata/Builtins.lc 483:69-483:70 Type -testdata/Builtins.lc 483:69-483:80 Type -testdata/Builtins.lc 483:74-483:75 Type -testdata/Builtins.lc 483:74-483:80 Type -testdata/Builtins.lc 483:79-483:80 Type -testdata/Builtins.lc 484:1-484:11 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a -> a->b +testdata/Builtins.lc 483:37-483:38 Type -> Type->Type +testdata/Builtins.lc 483:39-483:48 Nat -> Type->Type +testdata/Builtins.lc 483:39-483:50 Type->Type +testdata/Builtins.lc 483:39-483:56 Type +testdata/Builtins.lc 483:49-483:50 V1 +testdata/Builtins.lc 483:51-483:56 Type +testdata/Builtins.lc 483:61-483:62 Type +testdata/Builtins.lc 483:61-483:72 Type +testdata/Builtins.lc 483:66-483:72 Type +testdata/Builtins.lc 483:67-483:68 Type +testdata/Builtins.lc 483:70-483:71 Type +testdata/Builtins.lc 484:1-484:10 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b -> b->b testdata/Builtins.lc 484:34-484:80 Type testdata/Builtins.lc 484:35-484:38 Type->Type testdata/Builtins.lc 484:35-484:40 Type @@ -2228,27 +2198,31 @@ testdata/Builtins.lc 484:69-484:80 Type testdata/Builtins.lc 484:74-484:75 Type testdata/Builtins.lc 484:74-484:80 Type testdata/Builtins.lc 484:79-484:80 Type -testdata/Builtins.lc 485:1-485:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a -testdata/Builtins.lc 485:34-485:57 Type -testdata/Builtins.lc 485:34-485:77 Type -testdata/Builtins.lc 485:35-485:36 V3 +testdata/Builtins.lc 485:1-485:11 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a -> a->b +testdata/Builtins.lc 485:34-485:80 Type testdata/Builtins.lc 485:35-485:38 Type->Type -testdata/Builtins.lc 485:37-485:38 Type -> Type->Type -testdata/Builtins.lc 485:39-485:48 Nat -> Type->Type -testdata/Builtins.lc 485:39-485:50 Type->Type -testdata/Builtins.lc 485:39-485:56 Type -testdata/Builtins.lc 485:49-485:50 V1 -testdata/Builtins.lc 485:51-485:56 Type -testdata/Builtins.lc 485:61-485:62 Type -testdata/Builtins.lc 485:61-485:77 Type -testdata/Builtins.lc 485:66-485:67 Type -testdata/Builtins.lc 485:66-485:77 Type -testdata/Builtins.lc 485:71-485:72 Type -testdata/Builtins.lc 485:71-485:77 Type -testdata/Builtins.lc 485:76-485:77 Type -testdata/Builtins.lc 486:1-486:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> Float->a +testdata/Builtins.lc 485:35-485:40 Type +testdata/Builtins.lc 485:39-485:40 V5 +testdata/Builtins.lc 485:42-485:43 V4 +testdata/Builtins.lc 485:42-485:45 Type->Type +testdata/Builtins.lc 485:42-485:59 Type +testdata/Builtins.lc 485:42-485:80 Type +testdata/Builtins.lc 485:44-485:45 Type -> Type->Type +testdata/Builtins.lc 485:46-485:55 Nat -> Type->Type +testdata/Builtins.lc 485:46-485:57 Type->Type +testdata/Builtins.lc 485:46-485:59 Type +testdata/Builtins.lc 485:56-485:57 V2 +testdata/Builtins.lc 485:58-485:59 Type +testdata/Builtins.lc 485:64-485:65 Type +testdata/Builtins.lc 485:64-485:80 Type +testdata/Builtins.lc 485:69-485:70 Type +testdata/Builtins.lc 485:69-485:80 Type +testdata/Builtins.lc 485:74-485:75 Type +testdata/Builtins.lc 485:74-485:80 Type +testdata/Builtins.lc 485:79-485:80 Type +testdata/Builtins.lc 486:1-486:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a testdata/Builtins.lc 486:34-486:57 Type -testdata/Builtins.lc 486:34-486:81 Type +testdata/Builtins.lc 486:34-486:77 Type testdata/Builtins.lc 486:35-486:36 V3 testdata/Builtins.lc 486:35-486:38 Type->Type testdata/Builtins.lc 486:37-486:38 Type -> Type->Type @@ -2258,174 +2232,177 @@ testdata/Builtins.lc 486:39-486:56 Type testdata/Builtins.lc 486:49-486:50 V1 testdata/Builtins.lc 486:51-486:56 Type testdata/Builtins.lc 486:61-486:62 Type -testdata/Builtins.lc 486:61-486:81 Type +testdata/Builtins.lc 486:61-486:77 Type testdata/Builtins.lc 486:66-486:67 Type -testdata/Builtins.lc 486:66-486:81 Type -testdata/Builtins.lc 486:71-486:76 Type -testdata/Builtins.lc 486:71-486:81 Type -testdata/Builtins.lc 486:80-486:81 Type -testdata/Builtins.lc 487:1-487:9 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a -> a -> c->a -testdata/Builtins.lc 487:34-487:99 Type -testdata/Builtins.lc 487:35-487:36 V5 +testdata/Builtins.lc 486:66-486:77 Type +testdata/Builtins.lc 486:71-486:72 Type +testdata/Builtins.lc 486:71-486:77 Type +testdata/Builtins.lc 486:76-486:77 Type +testdata/Builtins.lc 487:1-487:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> Float->a +testdata/Builtins.lc 487:34-487:57 Type +testdata/Builtins.lc 487:34-487:81 Type +testdata/Builtins.lc 487:35-487:36 V3 testdata/Builtins.lc 487:35-487:38 Type->Type -testdata/Builtins.lc 487:35-487:56 Type testdata/Builtins.lc 487:37-487:38 Type -> Type->Type testdata/Builtins.lc 487:39-487:48 Nat -> Type->Type testdata/Builtins.lc 487:39-487:50 Type->Type testdata/Builtins.lc 487:39-487:56 Type -testdata/Builtins.lc 487:49-487:50 V3 +testdata/Builtins.lc 487:49-487:50 V1 testdata/Builtins.lc 487:51-487:56 Type -testdata/Builtins.lc 487:58-487:59 V2 -testdata/Builtins.lc 487:58-487:61 Type->Type -testdata/Builtins.lc 487:58-487:78 Type -testdata/Builtins.lc 487:58-487:99 Type -testdata/Builtins.lc 487:60-487:61 Type -> Type->Type -testdata/Builtins.lc 487:62-487:71 Nat -> Type->Type -testdata/Builtins.lc 487:62-487:73 Type->Type -testdata/Builtins.lc 487:62-487:78 Type -testdata/Builtins.lc 487:72-487:73 Nat -testdata/Builtins.lc 487:74-487:78 Type -testdata/Builtins.lc 487:83-487:84 Type -testdata/Builtins.lc 487:83-487:99 Type -testdata/Builtins.lc 487:88-487:89 Type -testdata/Builtins.lc 487:88-487:99 Type -testdata/Builtins.lc 487:93-487:94 Type -testdata/Builtins.lc 487:93-487:99 Type -testdata/Builtins.lc 487:98-487:99 Type -testdata/Builtins.lc 488:1-488:9 {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a -> a->a -testdata/Builtins.lc 488:34-488:53 Type -testdata/Builtins.lc 488:34-488:68 Type -testdata/Builtins.lc 488:35-488:36 V3 +testdata/Builtins.lc 487:61-487:62 Type +testdata/Builtins.lc 487:61-487:81 Type +testdata/Builtins.lc 487:66-487:67 Type +testdata/Builtins.lc 487:66-487:81 Type +testdata/Builtins.lc 487:71-487:76 Type +testdata/Builtins.lc 487:71-487:81 Type +testdata/Builtins.lc 487:80-487:81 Type +testdata/Builtins.lc 488:1-488:9 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a -> a -> c->a +testdata/Builtins.lc 488:34-488:99 Type +testdata/Builtins.lc 488:35-488:36 V5 testdata/Builtins.lc 488:35-488:38 Type->Type +testdata/Builtins.lc 488:35-488:56 Type testdata/Builtins.lc 488:37-488:38 Type -> Type->Type -testdata/Builtins.lc 488:39-488:44 Nat -> Type->Type -testdata/Builtins.lc 488:39-488:46 Type->Type -testdata/Builtins.lc 488:39-488:52 Type -testdata/Builtins.lc 488:45-488:46 V1 -testdata/Builtins.lc 488:47-488:52 Type -testdata/Builtins.lc 488:57-488:58 Type -testdata/Builtins.lc 488:57-488:68 Type -testdata/Builtins.lc 488:62-488:63 Type -testdata/Builtins.lc 488:62-488:68 Type -testdata/Builtins.lc 488:67-488:68 Type -testdata/Builtins.lc 489:1-489:10 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> Float -> a->a -testdata/Builtins.lc 489:34-489:57 Type -testdata/Builtins.lc 489:34-489:76 Type +testdata/Builtins.lc 488:39-488:48 Nat -> Type->Type +testdata/Builtins.lc 488:39-488:50 Type->Type +testdata/Builtins.lc 488:39-488:56 Type +testdata/Builtins.lc 488:49-488:50 V3 +testdata/Builtins.lc 488:51-488:56 Type +testdata/Builtins.lc 488:58-488:59 V2 +testdata/Builtins.lc 488:58-488:61 Type->Type +testdata/Builtins.lc 488:58-488:78 Type +testdata/Builtins.lc 488:58-488:99 Type +testdata/Builtins.lc 488:60-488:61 Type -> Type->Type +testdata/Builtins.lc 488:62-488:71 Nat -> Type->Type +testdata/Builtins.lc 488:62-488:73 Type->Type +testdata/Builtins.lc 488:62-488:78 Type +testdata/Builtins.lc 488:72-488:73 Nat +testdata/Builtins.lc 488:74-488:78 Type +testdata/Builtins.lc 488:83-488:84 Type +testdata/Builtins.lc 488:83-488:99 Type +testdata/Builtins.lc 488:88-488:89 Type +testdata/Builtins.lc 488:88-488:99 Type +testdata/Builtins.lc 488:93-488:94 Type +testdata/Builtins.lc 488:93-488:99 Type +testdata/Builtins.lc 488:98-488:99 Type +testdata/Builtins.lc 489:1-489:9 {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a -> a->a +testdata/Builtins.lc 489:34-489:53 Type +testdata/Builtins.lc 489:34-489:68 Type testdata/Builtins.lc 489:35-489:36 V3 testdata/Builtins.lc 489:35-489:38 Type->Type testdata/Builtins.lc 489:37-489:38 Type -> Type->Type -testdata/Builtins.lc 489:39-489:48 Nat -> Type->Type -testdata/Builtins.lc 489:39-489:50 Type->Type -testdata/Builtins.lc 489:39-489:56 Type -testdata/Builtins.lc 489:49-489:50 V1 -testdata/Builtins.lc 489:51-489:56 Type -testdata/Builtins.lc 489:61-489:66 Type -testdata/Builtins.lc 489:61-489:76 Type -testdata/Builtins.lc 489:70-489:71 Type -testdata/Builtins.lc 489:70-489:76 Type -testdata/Builtins.lc 489:75-489:76 Type -testdata/Builtins.lc 490:1-490:15 {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a -> a -> a->a -testdata/Builtins.lc 490:34-490:53 Type -testdata/Builtins.lc 490:34-490:73 Type +testdata/Builtins.lc 489:39-489:44 Nat -> Type->Type +testdata/Builtins.lc 489:39-489:46 Type->Type +testdata/Builtins.lc 489:39-489:52 Type +testdata/Builtins.lc 489:45-489:46 V1 +testdata/Builtins.lc 489:47-489:52 Type +testdata/Builtins.lc 489:57-489:58 Type +testdata/Builtins.lc 489:57-489:68 Type +testdata/Builtins.lc 489:62-489:63 Type +testdata/Builtins.lc 489:62-489:68 Type +testdata/Builtins.lc 489:67-489:68 Type +testdata/Builtins.lc 490:1-490:10 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> Float -> a->a +testdata/Builtins.lc 490:34-490:57 Type +testdata/Builtins.lc 490:34-490:76 Type testdata/Builtins.lc 490:35-490:36 V3 testdata/Builtins.lc 490:35-490:38 Type->Type testdata/Builtins.lc 490:37-490:38 Type -> Type->Type -testdata/Builtins.lc 490:39-490:44 Nat -> Type->Type -testdata/Builtins.lc 490:39-490:46 Type->Type -testdata/Builtins.lc 490:39-490:52 Type -testdata/Builtins.lc 490:45-490:46 V1 -testdata/Builtins.lc 490:47-490:52 Type -testdata/Builtins.lc 490:57-490:58 Type -testdata/Builtins.lc 490:57-490:73 Type -testdata/Builtins.lc 490:62-490:63 Type -testdata/Builtins.lc 490:62-490:73 Type -testdata/Builtins.lc 490:67-490:68 Type -testdata/Builtins.lc 490:67-490:73 Type -testdata/Builtins.lc 490:72-490:73 Type -testdata/Builtins.lc 491:1-491:16 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> Float -> Float -> a->a -testdata/Builtins.lc 491:34-491:57 Type -testdata/Builtins.lc 491:34-491:85 Type +testdata/Builtins.lc 490:39-490:48 Nat -> Type->Type +testdata/Builtins.lc 490:39-490:50 Type->Type +testdata/Builtins.lc 490:39-490:56 Type +testdata/Builtins.lc 490:49-490:50 V1 +testdata/Builtins.lc 490:51-490:56 Type +testdata/Builtins.lc 490:61-490:66 Type +testdata/Builtins.lc 490:61-490:76 Type +testdata/Builtins.lc 490:70-490:71 Type +testdata/Builtins.lc 490:70-490:76 Type +testdata/Builtins.lc 490:75-490:76 Type +testdata/Builtins.lc 491:1-491:15 {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a -> a -> a->a +testdata/Builtins.lc 491:34-491:53 Type +testdata/Builtins.lc 491:34-491:73 Type testdata/Builtins.lc 491:35-491:36 V3 testdata/Builtins.lc 491:35-491:38 Type->Type testdata/Builtins.lc 491:37-491:38 Type -> Type->Type -testdata/Builtins.lc 491:39-491:48 Nat -> Type->Type -testdata/Builtins.lc 491:39-491:50 Type->Type -testdata/Builtins.lc 491:39-491:56 Type -testdata/Builtins.lc 491:49-491:50 V1 -testdata/Builtins.lc 491:51-491:56 Type -testdata/Builtins.lc 491:61-491:66 Type -testdata/Builtins.lc 491:61-491:85 Type -testdata/Builtins.lc 491:70-491:75 Type -testdata/Builtins.lc 491:70-491:85 Type -testdata/Builtins.lc 491:79-491:80 Type -testdata/Builtins.lc 491:79-491:85 Type -testdata/Builtins.lc 491:84-491:85 Type -testdata/Builtins.lc 494:1-494:19 {a:Nat} -> VecScalar a Float -> VecScalar a Int -testdata/Builtins.lc 494:34-494:43 Nat -> Type->Type -testdata/Builtins.lc 494:34-494:45 Type->Type -testdata/Builtins.lc 494:34-494:51 Type -testdata/Builtins.lc 494:34-494:70 Type -testdata/Builtins.lc 494:44-494:45 V1 -testdata/Builtins.lc 494:46-494:51 Type -testdata/Builtins.lc 494:55-494:64 Nat -> Type->Type -testdata/Builtins.lc 494:55-494:66 Type->Type -testdata/Builtins.lc 494:55-494:70 Type -testdata/Builtins.lc 494:65-494:66 Nat -testdata/Builtins.lc 494:67-494:70 Type -testdata/Builtins.lc 495:1-495:20 {a:Nat} -> VecScalar a Float -> VecScalar a Word +testdata/Builtins.lc 491:39-491:44 Nat -> Type->Type +testdata/Builtins.lc 491:39-491:46 Type->Type +testdata/Builtins.lc 491:39-491:52 Type +testdata/Builtins.lc 491:45-491:46 V1 +testdata/Builtins.lc 491:47-491:52 Type +testdata/Builtins.lc 491:57-491:58 Type +testdata/Builtins.lc 491:57-491:73 Type +testdata/Builtins.lc 491:62-491:63 Type +testdata/Builtins.lc 491:62-491:73 Type +testdata/Builtins.lc 491:67-491:68 Type +testdata/Builtins.lc 491:67-491:73 Type +testdata/Builtins.lc 491:72-491:73 Type +testdata/Builtins.lc 492:1-492:16 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> Float -> Float -> a->a +testdata/Builtins.lc 492:34-492:57 Type +testdata/Builtins.lc 492:34-492:85 Type +testdata/Builtins.lc 492:35-492:36 V3 +testdata/Builtins.lc 492:35-492:38 Type->Type +testdata/Builtins.lc 492:37-492:38 Type -> Type->Type +testdata/Builtins.lc 492:39-492:48 Nat -> Type->Type +testdata/Builtins.lc 492:39-492:50 Type->Type +testdata/Builtins.lc 492:39-492:56 Type +testdata/Builtins.lc 492:49-492:50 V1 +testdata/Builtins.lc 492:51-492:56 Type +testdata/Builtins.lc 492:61-492:66 Type +testdata/Builtins.lc 492:61-492:85 Type +testdata/Builtins.lc 492:70-492:75 Type +testdata/Builtins.lc 492:70-492:85 Type +testdata/Builtins.lc 492:79-492:80 Type +testdata/Builtins.lc 492:79-492:85 Type +testdata/Builtins.lc 492:84-492:85 Type +testdata/Builtins.lc 495:1-495:19 {a:Nat} -> VecScalar a Float -> VecScalar a Int testdata/Builtins.lc 495:34-495:43 Nat -> Type->Type testdata/Builtins.lc 495:34-495:45 Type->Type testdata/Builtins.lc 495:34-495:51 Type -testdata/Builtins.lc 495:34-495:71 Type +testdata/Builtins.lc 495:34-495:70 Type testdata/Builtins.lc 495:44-495:45 V1 testdata/Builtins.lc 495:46-495:51 Type testdata/Builtins.lc 495:55-495:64 Nat -> Type->Type testdata/Builtins.lc 495:55-495:66 Type->Type -testdata/Builtins.lc 495:55-495:71 Type +testdata/Builtins.lc 495:55-495:70 Type testdata/Builtins.lc 495:65-495:66 Nat -testdata/Builtins.lc 495:67-495:71 Type -testdata/Builtins.lc 496:1-496:19 {a:Nat} -> VecScalar a Int -> VecScalar a Float +testdata/Builtins.lc 495:67-495:70 Type +testdata/Builtins.lc 496:1-496:20 {a:Nat} -> VecScalar a Float -> VecScalar a Word testdata/Builtins.lc 496:34-496:43 Nat -> Type->Type testdata/Builtins.lc 496:34-496:45 Type->Type -testdata/Builtins.lc 496:34-496:49 Type -testdata/Builtins.lc 496:34-496:72 Type +testdata/Builtins.lc 496:34-496:51 Type +testdata/Builtins.lc 496:34-496:71 Type testdata/Builtins.lc 496:44-496:45 V1 -testdata/Builtins.lc 496:46-496:49 Type +testdata/Builtins.lc 496:46-496:51 Type testdata/Builtins.lc 496:55-496:64 Nat -> Type->Type testdata/Builtins.lc 496:55-496:66 Type->Type -testdata/Builtins.lc 496:55-496:72 Type +testdata/Builtins.lc 496:55-496:71 Type testdata/Builtins.lc 496:65-496:66 Nat -testdata/Builtins.lc 496:67-496:72 Type -testdata/Builtins.lc 497:1-497:20 {a:Nat} -> VecScalar a Word -> VecScalar a Float +testdata/Builtins.lc 496:67-496:71 Type +testdata/Builtins.lc 497:1-497:19 {a:Nat} -> VecScalar a Int -> VecScalar a Float testdata/Builtins.lc 497:34-497:43 Nat -> Type->Type testdata/Builtins.lc 497:34-497:45 Type->Type -testdata/Builtins.lc 497:34-497:50 Type +testdata/Builtins.lc 497:34-497:49 Type testdata/Builtins.lc 497:34-497:72 Type testdata/Builtins.lc 497:44-497:45 V1 -testdata/Builtins.lc 497:46-497:50 Type +testdata/Builtins.lc 497:46-497:49 Type testdata/Builtins.lc 497:55-497:64 Nat -> Type->Type testdata/Builtins.lc 497:55-497:66 Type->Type testdata/Builtins.lc 497:55-497:72 Type testdata/Builtins.lc 497:65-497:66 Nat testdata/Builtins.lc 497:67-497:72 Type -testdata/Builtins.lc 499:1-499:11 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->Float -testdata/Builtins.lc 499:34-499:57 Type -testdata/Builtins.lc 499:34-499:71 Type -testdata/Builtins.lc 499:35-499:36 V3 -testdata/Builtins.lc 499:35-499:38 Type->Type -testdata/Builtins.lc 499:37-499:38 Type -> Type->Type -testdata/Builtins.lc 499:39-499:48 Nat -> Type->Type -testdata/Builtins.lc 499:39-499:50 Type->Type -testdata/Builtins.lc 499:39-499:56 Type -testdata/Builtins.lc 499:49-499:50 V1 -testdata/Builtins.lc 499:51-499:56 Type -testdata/Builtins.lc 499:61-499:62 Type -testdata/Builtins.lc 499:61-499:71 Type -testdata/Builtins.lc 499:66-499:71 Type -testdata/Builtins.lc 500:1-500:13 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->Float -testdata/Builtins.lc 500:15-500:22 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->Float +testdata/Builtins.lc 498:1-498:20 {a:Nat} -> VecScalar a Word -> VecScalar a Float +testdata/Builtins.lc 498:34-498:43 Nat -> Type->Type +testdata/Builtins.lc 498:34-498:45 Type->Type +testdata/Builtins.lc 498:34-498:50 Type +testdata/Builtins.lc 498:34-498:72 Type +testdata/Builtins.lc 498:44-498:45 V1 +testdata/Builtins.lc 498:46-498:50 Type +testdata/Builtins.lc 498:55-498:64 Nat -> Type->Type +testdata/Builtins.lc 498:55-498:66 Type->Type +testdata/Builtins.lc 498:55-498:72 Type +testdata/Builtins.lc 498:65-498:66 Nat +testdata/Builtins.lc 498:67-498:72 Type +testdata/Builtins.lc 500:1-500:11 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->Float testdata/Builtins.lc 500:34-500:57 Type -testdata/Builtins.lc 500:34-500:76 Type +testdata/Builtins.lc 500:34-500:71 Type testdata/Builtins.lc 500:35-500:36 V3 testdata/Builtins.lc 500:35-500:38 Type->Type testdata/Builtins.lc 500:37-500:38 Type -> Type->Type @@ -2435,14 +2412,13 @@ testdata/Builtins.lc 500:39-500:56 Type testdata/Builtins.lc 500:49-500:50 V1 testdata/Builtins.lc 500:51-500:56 Type testdata/Builtins.lc 500:61-500:62 Type -testdata/Builtins.lc 500:61-500:76 Type -testdata/Builtins.lc 500:66-500:67 Type -testdata/Builtins.lc 500:66-500:76 Type -testdata/Builtins.lc 500:71-500:76 Type -testdata/Builtins.lc 501:1-501:10 {a} -> {b : a ~ VecS Float 3} -> a -> a->a +testdata/Builtins.lc 500:61-500:71 Type +testdata/Builtins.lc 500:66-500:71 Type +testdata/Builtins.lc 501:1-501:13 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->Float +testdata/Builtins.lc 501:15-501:22 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->Float testdata/Builtins.lc 501:34-501:57 Type -testdata/Builtins.lc 501:34-501:72 Type -testdata/Builtins.lc 501:35-501:36 V1 +testdata/Builtins.lc 501:34-501:76 Type +testdata/Builtins.lc 501:35-501:36 V3 testdata/Builtins.lc 501:35-501:38 Type->Type testdata/Builtins.lc 501:37-501:38 Type -> Type->Type testdata/Builtins.lc 501:39-501:48 Nat -> Type->Type @@ -2451,14 +2427,14 @@ testdata/Builtins.lc 501:39-501:56 Type testdata/Builtins.lc 501:49-501:50 V1 testdata/Builtins.lc 501:51-501:56 Type testdata/Builtins.lc 501:61-501:62 Type -testdata/Builtins.lc 501:61-501:72 Type +testdata/Builtins.lc 501:61-501:76 Type testdata/Builtins.lc 501:66-501:67 Type -testdata/Builtins.lc 501:66-501:72 Type -testdata/Builtins.lc 501:71-501:72 Type -testdata/Builtins.lc 502:1-502:14 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 501:66-501:76 Type +testdata/Builtins.lc 501:71-501:76 Type +testdata/Builtins.lc 502:1-502:10 {a} -> {b : a ~ VecS Float 3} -> a -> a->a testdata/Builtins.lc 502:34-502:57 Type -testdata/Builtins.lc 502:34-502:67 Type -testdata/Builtins.lc 502:35-502:36 V3 +testdata/Builtins.lc 502:34-502:72 Type +testdata/Builtins.lc 502:35-502:36 V1 testdata/Builtins.lc 502:35-502:38 Type->Type testdata/Builtins.lc 502:37-502:38 Type -> Type->Type testdata/Builtins.lc 502:39-502:48 Nat -> Type->Type @@ -2467,12 +2443,13 @@ testdata/Builtins.lc 502:39-502:56 Type testdata/Builtins.lc 502:49-502:50 V1 testdata/Builtins.lc 502:51-502:56 Type testdata/Builtins.lc 502:61-502:62 Type -testdata/Builtins.lc 502:61-502:67 Type +testdata/Builtins.lc 502:61-502:72 Type testdata/Builtins.lc 502:66-502:67 Type -testdata/Builtins.lc 503:1-503:16 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a -testdata/Builtins.lc 503:18-503:29 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a +testdata/Builtins.lc 502:66-502:72 Type +testdata/Builtins.lc 502:71-502:72 Type +testdata/Builtins.lc 503:1-503:14 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a testdata/Builtins.lc 503:34-503:57 Type -testdata/Builtins.lc 503:34-503:77 Type +testdata/Builtins.lc 503:34-503:67 Type testdata/Builtins.lc 503:35-503:36 V3 testdata/Builtins.lc 503:35-503:38 Type->Type testdata/Builtins.lc 503:37-503:38 Type -> Type->Type @@ -2482,15 +2459,12 @@ testdata/Builtins.lc 503:39-503:56 Type testdata/Builtins.lc 503:49-503:50 V1 testdata/Builtins.lc 503:51-503:56 Type testdata/Builtins.lc 503:61-503:62 Type -testdata/Builtins.lc 503:61-503:77 Type +testdata/Builtins.lc 503:61-503:67 Type testdata/Builtins.lc 503:66-503:67 Type -testdata/Builtins.lc 503:66-503:77 Type -testdata/Builtins.lc 503:71-503:72 Type -testdata/Builtins.lc 503:71-503:77 Type -testdata/Builtins.lc 503:76-503:77 Type -testdata/Builtins.lc 504:1-504:12 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a +testdata/Builtins.lc 504:1-504:16 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a +testdata/Builtins.lc 504:18-504:29 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a testdata/Builtins.lc 504:34-504:57 Type -testdata/Builtins.lc 504:34-504:72 Type +testdata/Builtins.lc 504:34-504:77 Type testdata/Builtins.lc 504:35-504:36 V3 testdata/Builtins.lc 504:35-504:38 Type->Type testdata/Builtins.lc 504:37-504:38 Type -> Type->Type @@ -2500,223 +2474,229 @@ testdata/Builtins.lc 504:39-504:56 Type testdata/Builtins.lc 504:49-504:50 V1 testdata/Builtins.lc 504:51-504:56 Type testdata/Builtins.lc 504:61-504:62 Type -testdata/Builtins.lc 504:61-504:72 Type +testdata/Builtins.lc 504:61-504:77 Type testdata/Builtins.lc 504:66-504:67 Type -testdata/Builtins.lc 504:66-504:72 Type +testdata/Builtins.lc 504:66-504:77 Type testdata/Builtins.lc 504:71-504:72 Type -testdata/Builtins.lc 506:1-506:14 {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> Mat b a c -testdata/Builtins.lc 506:34-506:37 Nat -> Nat -> Type->Type -testdata/Builtins.lc 506:34-506:39 Nat -> Type->Type -testdata/Builtins.lc 506:34-506:41 Type->Type -testdata/Builtins.lc 506:34-506:43 Type -testdata/Builtins.lc 506:34-506:56 Type -testdata/Builtins.lc 506:38-506:39 V5 -testdata/Builtins.lc 506:40-506:41 V3 -testdata/Builtins.lc 506:42-506:43 V1 -testdata/Builtins.lc 506:47-506:50 Nat -> Nat -> Type->Type -testdata/Builtins.lc 506:47-506:52 Nat -> Type->Type -testdata/Builtins.lc 506:47-506:54 Type->Type -testdata/Builtins.lc 506:47-506:56 Type -testdata/Builtins.lc 506:51-506:52 Nat -testdata/Builtins.lc 506:53-506:54 Nat -testdata/Builtins.lc 506:55-506:56 Type -testdata/Builtins.lc 507:1-507:16 {a:Nat} -> {b} -> Mat a a b -> Float +testdata/Builtins.lc 504:71-504:77 Type +testdata/Builtins.lc 504:76-504:77 Type +testdata/Builtins.lc 505:1-505:12 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a +testdata/Builtins.lc 505:34-505:57 Type +testdata/Builtins.lc 505:34-505:72 Type +testdata/Builtins.lc 505:35-505:36 V3 +testdata/Builtins.lc 505:35-505:38 Type->Type +testdata/Builtins.lc 505:37-505:38 Type -> Type->Type +testdata/Builtins.lc 505:39-505:48 Nat -> Type->Type +testdata/Builtins.lc 505:39-505:50 Type->Type +testdata/Builtins.lc 505:39-505:56 Type +testdata/Builtins.lc 505:49-505:50 V1 +testdata/Builtins.lc 505:51-505:56 Type +testdata/Builtins.lc 505:61-505:62 Type +testdata/Builtins.lc 505:61-505:72 Type +testdata/Builtins.lc 505:66-505:67 Type +testdata/Builtins.lc 505:66-505:72 Type +testdata/Builtins.lc 505:71-505:72 Type +testdata/Builtins.lc 507:1-507:14 {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> Mat b a c testdata/Builtins.lc 507:34-507:37 Nat -> Nat -> Type->Type testdata/Builtins.lc 507:34-507:39 Nat -> Type->Type testdata/Builtins.lc 507:34-507:41 Type->Type testdata/Builtins.lc 507:34-507:43 Type -testdata/Builtins.lc 507:34-507:52 Type -testdata/Builtins.lc 507:38-507:39 V3 -testdata/Builtins.lc 507:40-507:41 Nat +testdata/Builtins.lc 507:34-507:56 Type +testdata/Builtins.lc 507:38-507:39 V5 +testdata/Builtins.lc 507:40-507:41 V3 testdata/Builtins.lc 507:42-507:43 V1 -testdata/Builtins.lc 507:47-507:52 Type -testdata/Builtins.lc 508:1-508:12 {a:Nat} -> {b} -> Mat a a b -> Mat a a b +testdata/Builtins.lc 507:47-507:50 Nat -> Nat -> Type->Type +testdata/Builtins.lc 507:47-507:52 Nat -> Type->Type +testdata/Builtins.lc 507:47-507:54 Type->Type +testdata/Builtins.lc 507:47-507:56 Type +testdata/Builtins.lc 507:51-507:52 Nat +testdata/Builtins.lc 507:53-507:54 Nat +testdata/Builtins.lc 507:55-507:56 Type +testdata/Builtins.lc 508:1-508:16 {a:Nat} -> {b} -> Mat a a b -> Float testdata/Builtins.lc 508:34-508:37 Nat -> Nat -> Type->Type testdata/Builtins.lc 508:34-508:39 Nat -> Type->Type testdata/Builtins.lc 508:34-508:41 Type->Type testdata/Builtins.lc 508:34-508:43 Type -testdata/Builtins.lc 508:34-508:56 Type +testdata/Builtins.lc 508:34-508:52 Type testdata/Builtins.lc 508:38-508:39 V3 testdata/Builtins.lc 508:40-508:41 Nat testdata/Builtins.lc 508:42-508:43 V1 -testdata/Builtins.lc 508:47-508:50 Nat -> Nat -> Type->Type -testdata/Builtins.lc 508:47-508:52 Nat -> Type->Type -testdata/Builtins.lc 508:47-508:54 Type->Type -testdata/Builtins.lc 508:47-508:56 Type -testdata/Builtins.lc 508:51-508:52 Nat -testdata/Builtins.lc 508:53-508:54 Nat -testdata/Builtins.lc 508:55-508:56 Type -testdata/Builtins.lc 509:1-509:17 {a:Nat} -> {b} -> {c:Nat} -> VecS b a -> VecS b c -> Mat c a b -testdata/Builtins.lc 509:34-509:37 Nat -> Type->Type -testdata/Builtins.lc 509:34-509:39 Type->Type -testdata/Builtins.lc 509:34-509:41 Type -testdata/Builtins.lc 509:34-509:69 Type -testdata/Builtins.lc 509:38-509:39 V5 -testdata/Builtins.lc 509:40-509:41 V3 -testdata/Builtins.lc 509:47-509:50 Nat -> Type->Type -testdata/Builtins.lc 509:47-509:52 Type->Type -testdata/Builtins.lc 509:47-509:54 Type -testdata/Builtins.lc 509:47-509:69 Type -testdata/Builtins.lc 509:51-509:52 V2 -testdata/Builtins.lc 509:53-509:54 Type -testdata/Builtins.lc 509:60-509:63 Nat -> Nat -> Type->Type -testdata/Builtins.lc 509:60-509:65 Nat -> Type->Type -testdata/Builtins.lc 509:60-509:67 Type->Type -testdata/Builtins.lc 509:60-509:69 Type -testdata/Builtins.lc 509:64-509:65 Nat -testdata/Builtins.lc 509:66-509:67 Nat -testdata/Builtins.lc 509:68-509:69 Type -testdata/Builtins.lc 510:1-510:14 {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> VecS c b -> VecS c a -testdata/Builtins.lc 510:34-510:37 Nat -> Nat -> Type->Type -testdata/Builtins.lc 510:34-510:39 Nat -> Type->Type -testdata/Builtins.lc 510:34-510:41 Type->Type -testdata/Builtins.lc 510:34-510:43 Type -testdata/Builtins.lc 510:34-510:67 Type +testdata/Builtins.lc 508:47-508:52 Type +testdata/Builtins.lc 509:1-509:12 {a:Nat} -> {b} -> Mat a a b -> Mat a a b +testdata/Builtins.lc 509:34-509:37 Nat -> Nat -> Type->Type +testdata/Builtins.lc 509:34-509:39 Nat -> Type->Type +testdata/Builtins.lc 509:34-509:41 Type->Type +testdata/Builtins.lc 509:34-509:43 Type +testdata/Builtins.lc 509:34-509:56 Type +testdata/Builtins.lc 509:38-509:39 V3 +testdata/Builtins.lc 509:40-509:41 Nat +testdata/Builtins.lc 509:42-509:43 V1 +testdata/Builtins.lc 509:47-509:50 Nat -> Nat -> Type->Type +testdata/Builtins.lc 509:47-509:52 Nat -> Type->Type +testdata/Builtins.lc 509:47-509:54 Type->Type +testdata/Builtins.lc 509:47-509:56 Type +testdata/Builtins.lc 509:51-509:52 Nat +testdata/Builtins.lc 509:53-509:54 Nat +testdata/Builtins.lc 509:55-509:56 Type +testdata/Builtins.lc 510:1-510:17 {a:Nat} -> {b} -> {c:Nat} -> VecS b a -> VecS b c -> Mat c a b +testdata/Builtins.lc 510:34-510:37 Nat -> Type->Type +testdata/Builtins.lc 510:34-510:39 Type->Type +testdata/Builtins.lc 510:34-510:41 Type +testdata/Builtins.lc 510:34-510:69 Type testdata/Builtins.lc 510:38-510:39 V5 testdata/Builtins.lc 510:40-510:41 V3 -testdata/Builtins.lc 510:42-510:43 V1 testdata/Builtins.lc 510:47-510:50 Nat -> Type->Type testdata/Builtins.lc 510:47-510:52 Type->Type testdata/Builtins.lc 510:47-510:54 Type -testdata/Builtins.lc 510:47-510:67 Type -testdata/Builtins.lc 510:51-510:52 Nat +testdata/Builtins.lc 510:47-510:69 Type +testdata/Builtins.lc 510:51-510:52 V2 testdata/Builtins.lc 510:53-510:54 Type -testdata/Builtins.lc 510:60-510:63 Nat -> Type->Type -testdata/Builtins.lc 510:60-510:65 Type->Type -testdata/Builtins.lc 510:60-510:67 Type +testdata/Builtins.lc 510:60-510:63 Nat -> Nat -> Type->Type +testdata/Builtins.lc 510:60-510:65 Nat -> Type->Type +testdata/Builtins.lc 510:60-510:67 Type->Type +testdata/Builtins.lc 510:60-510:69 Type testdata/Builtins.lc 510:64-510:65 Nat -testdata/Builtins.lc 510:66-510:67 Type -testdata/Builtins.lc 511:1-511:14 {a:Nat} -> {b} -> {c:Nat} -> VecS b a -> Mat a c b -> VecS b c -testdata/Builtins.lc 511:34-511:37 Nat -> Type->Type -testdata/Builtins.lc 511:34-511:39 Type->Type -testdata/Builtins.lc 511:34-511:41 Type +testdata/Builtins.lc 510:66-510:67 Nat +testdata/Builtins.lc 510:68-510:69 Type +testdata/Builtins.lc 511:1-511:14 {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> VecS c b -> VecS c a +testdata/Builtins.lc 511:34-511:37 Nat -> Nat -> Type->Type +testdata/Builtins.lc 511:34-511:39 Nat -> Type->Type +testdata/Builtins.lc 511:34-511:41 Type->Type +testdata/Builtins.lc 511:34-511:43 Type testdata/Builtins.lc 511:34-511:67 Type testdata/Builtins.lc 511:38-511:39 V5 testdata/Builtins.lc 511:40-511:41 V3 -testdata/Builtins.lc 511:47-511:50 Nat -> Nat -> Type->Type -testdata/Builtins.lc 511:47-511:52 Nat -> Type->Type -testdata/Builtins.lc 511:47-511:54 Type->Type -testdata/Builtins.lc 511:47-511:56 Type +testdata/Builtins.lc 511:42-511:43 V1 +testdata/Builtins.lc 511:47-511:50 Nat -> Type->Type +testdata/Builtins.lc 511:47-511:52 Type->Type +testdata/Builtins.lc 511:47-511:54 Type testdata/Builtins.lc 511:47-511:67 Type testdata/Builtins.lc 511:51-511:52 Nat -testdata/Builtins.lc 511:53-511:54 V2 -testdata/Builtins.lc 511:55-511:56 Type +testdata/Builtins.lc 511:53-511:54 Type testdata/Builtins.lc 511:60-511:63 Nat -> Type->Type testdata/Builtins.lc 511:60-511:65 Type->Type testdata/Builtins.lc 511:60-511:67 Type testdata/Builtins.lc 511:64-511:65 Nat testdata/Builtins.lc 511:66-511:67 Type -testdata/Builtins.lc 512:1-512:14 {a:Nat} -> {b:Nat} -> {c} -> {d:Nat} -> Mat a b c -> Mat b d c -> Mat a d c -testdata/Builtins.lc 512:34-512:37 Nat -> Nat -> Type->Type -testdata/Builtins.lc 512:34-512:39 Nat -> Type->Type -testdata/Builtins.lc 512:34-512:41 Type->Type -testdata/Builtins.lc 512:34-512:43 Type -testdata/Builtins.lc 512:34-512:69 Type -testdata/Builtins.lc 512:38-512:39 V7 -testdata/Builtins.lc 512:40-512:41 V5 -testdata/Builtins.lc 512:42-512:43 V3 +testdata/Builtins.lc 512:1-512:14 {a:Nat} -> {b} -> {c:Nat} -> VecS b a -> Mat a c b -> VecS b c +testdata/Builtins.lc 512:34-512:37 Nat -> Type->Type +testdata/Builtins.lc 512:34-512:39 Type->Type +testdata/Builtins.lc 512:34-512:41 Type +testdata/Builtins.lc 512:34-512:67 Type +testdata/Builtins.lc 512:38-512:39 V5 +testdata/Builtins.lc 512:40-512:41 V3 testdata/Builtins.lc 512:47-512:50 Nat -> Nat -> Type->Type testdata/Builtins.lc 512:47-512:52 Nat -> Type->Type testdata/Builtins.lc 512:47-512:54 Type->Type testdata/Builtins.lc 512:47-512:56 Type -testdata/Builtins.lc 512:47-512:69 Type +testdata/Builtins.lc 512:47-512:67 Type testdata/Builtins.lc 512:51-512:52 Nat testdata/Builtins.lc 512:53-512:54 V2 testdata/Builtins.lc 512:55-512:56 Type -testdata/Builtins.lc 512:60-512:63 Nat -> Nat -> Type->Type -testdata/Builtins.lc 512:60-512:65 Nat -> Type->Type -testdata/Builtins.lc 512:60-512:67 Type->Type -testdata/Builtins.lc 512:60-512:69 Type +testdata/Builtins.lc 512:60-512:63 Nat -> Type->Type +testdata/Builtins.lc 512:60-512:65 Type->Type +testdata/Builtins.lc 512:60-512:67 Type testdata/Builtins.lc 512:64-512:65 Nat -testdata/Builtins.lc 512:66-512:67 Nat -testdata/Builtins.lc 512:68-512:69 Type -testdata/Builtins.lc 514:1-514:13 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d -testdata/Builtins.lc 514:15-514:32 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d -testdata/Builtins.lc 514:34-514:49 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d -testdata/Builtins.lc 514:51-514:71 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d -testdata/Builtins.lc 514:73-514:83 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d -testdata/Builtins.lc 514:85-514:98 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d -testdata/Builtins.lc 515:34-515:97 Type -testdata/Builtins.lc 515:35-515:38 Type->Type -testdata/Builtins.lc 515:35-515:40 Type -testdata/Builtins.lc 515:39-515:40 V7 -testdata/Builtins.lc 515:42-515:43 V6 -testdata/Builtins.lc 515:42-515:45 Type->Type -testdata/Builtins.lc 515:42-515:59 Type -testdata/Builtins.lc 515:42-515:97 Type -testdata/Builtins.lc 515:44-515:45 Type -> Type->Type -testdata/Builtins.lc 515:46-515:55 Nat -> Type->Type -testdata/Builtins.lc 515:46-515:57 Type->Type -testdata/Builtins.lc 515:46-515:59 Type -testdata/Builtins.lc 515:56-515:57 V4 -testdata/Builtins.lc 515:58-515:59 Type -testdata/Builtins.lc 515:61-515:62 V3 -testdata/Builtins.lc 515:61-515:64 Type->Type -testdata/Builtins.lc 515:61-515:81 Type -testdata/Builtins.lc 515:61-515:97 Type -testdata/Builtins.lc 515:63-515:64 Type -> Type->Type -testdata/Builtins.lc 515:65-515:74 Nat -> Type->Type -testdata/Builtins.lc 515:65-515:76 Type->Type -testdata/Builtins.lc 515:65-515:81 Type -testdata/Builtins.lc 515:75-515:76 Nat -testdata/Builtins.lc 515:77-515:81 Type -testdata/Builtins.lc 515:86-515:87 Type -testdata/Builtins.lc 515:86-515:97 Type -testdata/Builtins.lc 515:91-515:92 Type -testdata/Builtins.lc 515:91-515:97 Type -testdata/Builtins.lc 515:96-515:97 Type -testdata/Builtins.lc 516:1-516:10 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool -testdata/Builtins.lc 516:12-516:24 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool -testdata/Builtins.lc 516:34-516:58 Type -testdata/Builtins.lc 516:34-516:76 Type -testdata/Builtins.lc 516:35-516:36 V3 +testdata/Builtins.lc 512:66-512:67 Type +testdata/Builtins.lc 513:1-513:14 {a:Nat} -> {b:Nat} -> {c} -> {d:Nat} -> Mat a b c -> Mat b d c -> Mat a d c +testdata/Builtins.lc 513:34-513:37 Nat -> Nat -> Type->Type +testdata/Builtins.lc 513:34-513:39 Nat -> Type->Type +testdata/Builtins.lc 513:34-513:41 Type->Type +testdata/Builtins.lc 513:34-513:43 Type +testdata/Builtins.lc 513:34-513:69 Type +testdata/Builtins.lc 513:38-513:39 V7 +testdata/Builtins.lc 513:40-513:41 V5 +testdata/Builtins.lc 513:42-513:43 V3 +testdata/Builtins.lc 513:47-513:50 Nat -> Nat -> Type->Type +testdata/Builtins.lc 513:47-513:52 Nat -> Type->Type +testdata/Builtins.lc 513:47-513:54 Type->Type +testdata/Builtins.lc 513:47-513:56 Type +testdata/Builtins.lc 513:47-513:69 Type +testdata/Builtins.lc 513:51-513:52 Nat +testdata/Builtins.lc 513:53-513:54 V2 +testdata/Builtins.lc 513:55-513:56 Type +testdata/Builtins.lc 513:60-513:63 Nat -> Nat -> Type->Type +testdata/Builtins.lc 513:60-513:65 Nat -> Type->Type +testdata/Builtins.lc 513:60-513:67 Type->Type +testdata/Builtins.lc 513:60-513:69 Type +testdata/Builtins.lc 513:64-513:65 Nat +testdata/Builtins.lc 513:66-513:67 Nat +testdata/Builtins.lc 513:68-513:69 Type +testdata/Builtins.lc 515:1-515:13 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d +testdata/Builtins.lc 515:15-515:32 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d +testdata/Builtins.lc 515:34-515:49 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d +testdata/Builtins.lc 515:51-515:71 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d +testdata/Builtins.lc 515:73-515:83 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d +testdata/Builtins.lc 515:85-515:98 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d +testdata/Builtins.lc 516:34-516:97 Type testdata/Builtins.lc 516:35-516:38 Type->Type -testdata/Builtins.lc 516:37-516:38 Type -> Type->Type -testdata/Builtins.lc 516:39-516:55 Type->Type -testdata/Builtins.lc 516:39-516:57 Type -testdata/Builtins.lc 516:56-516:57 V1 -testdata/Builtins.lc 516:62-516:63 Type -testdata/Builtins.lc 516:62-516:76 Type -testdata/Builtins.lc 516:67-516:68 Type -testdata/Builtins.lc 516:67-516:76 Type -testdata/Builtins.lc 516:72-516:76 Type -testdata/Builtins.lc 518:1-518:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 518:11-518:19 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 518:21-518:31 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a -testdata/Builtins.lc 519:34-519:57 Type -testdata/Builtins.lc 519:34-519:67 Type -testdata/Builtins.lc 519:35-519:36 V3 -testdata/Builtins.lc 519:35-519:38 Type->Type -testdata/Builtins.lc 519:37-519:38 Type -> Type->Type -testdata/Builtins.lc 519:39-519:48 Nat -> Type->Type -testdata/Builtins.lc 519:39-519:50 Type->Type -testdata/Builtins.lc 519:39-519:56 Type -testdata/Builtins.lc 519:49-519:50 V1 -testdata/Builtins.lc 519:51-519:56 Type -testdata/Builtins.lc 519:61-519:62 Type -testdata/Builtins.lc 519:61-519:67 Type -testdata/Builtins.lc 519:66-519:67 Type -testdata/Builtins.lc 521:1-521:11 {a:Nat} -> VecScalar a Float -> Float -testdata/Builtins.lc 521:34-521:43 Nat -> Type->Type -testdata/Builtins.lc 521:34-521:45 Type->Type -testdata/Builtins.lc 521:34-521:51 Type -testdata/Builtins.lc 521:34-521:60 Type -testdata/Builtins.lc 521:44-521:45 V1 -testdata/Builtins.lc 521:46-521:51 Type -testdata/Builtins.lc 521:55-521:60 Type -testdata/Builtins.lc 522:1-522:11 {a:Nat} -> VecScalar a Float -> VecS Float 2 +testdata/Builtins.lc 516:35-516:40 Type +testdata/Builtins.lc 516:39-516:40 V7 +testdata/Builtins.lc 516:42-516:43 V6 +testdata/Builtins.lc 516:42-516:45 Type->Type +testdata/Builtins.lc 516:42-516:59 Type +testdata/Builtins.lc 516:42-516:97 Type +testdata/Builtins.lc 516:44-516:45 Type -> Type->Type +testdata/Builtins.lc 516:46-516:55 Nat -> Type->Type +testdata/Builtins.lc 516:46-516:57 Type->Type +testdata/Builtins.lc 516:46-516:59 Type +testdata/Builtins.lc 516:56-516:57 V4 +testdata/Builtins.lc 516:58-516:59 Type +testdata/Builtins.lc 516:61-516:62 V3 +testdata/Builtins.lc 516:61-516:64 Type->Type +testdata/Builtins.lc 516:61-516:81 Type +testdata/Builtins.lc 516:61-516:97 Type +testdata/Builtins.lc 516:63-516:64 Type -> Type->Type +testdata/Builtins.lc 516:65-516:74 Nat -> Type->Type +testdata/Builtins.lc 516:65-516:76 Type->Type +testdata/Builtins.lc 516:65-516:81 Type +testdata/Builtins.lc 516:75-516:76 Nat +testdata/Builtins.lc 516:77-516:81 Type +testdata/Builtins.lc 516:86-516:87 Type +testdata/Builtins.lc 516:86-516:97 Type +testdata/Builtins.lc 516:91-516:92 Type +testdata/Builtins.lc 516:91-516:97 Type +testdata/Builtins.lc 516:96-516:97 Type +testdata/Builtins.lc 517:1-517:10 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool +testdata/Builtins.lc 517:12-517:24 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool +testdata/Builtins.lc 517:34-517:58 Type +testdata/Builtins.lc 517:34-517:76 Type +testdata/Builtins.lc 517:35-517:36 V3 +testdata/Builtins.lc 517:35-517:38 Type->Type +testdata/Builtins.lc 517:37-517:38 Type -> Type->Type +testdata/Builtins.lc 517:39-517:55 Type->Type +testdata/Builtins.lc 517:39-517:57 Type +testdata/Builtins.lc 517:56-517:57 V1 +testdata/Builtins.lc 517:62-517:63 Type +testdata/Builtins.lc 517:62-517:76 Type +testdata/Builtins.lc 517:67-517:68 Type +testdata/Builtins.lc 517:67-517:76 Type +testdata/Builtins.lc 517:72-517:76 Type +testdata/Builtins.lc 519:1-519:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 519:11-519:19 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 519:21-519:31 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a +testdata/Builtins.lc 520:34-520:57 Type +testdata/Builtins.lc 520:34-520:67 Type +testdata/Builtins.lc 520:35-520:36 V3 +testdata/Builtins.lc 520:35-520:38 Type->Type +testdata/Builtins.lc 520:37-520:38 Type -> Type->Type +testdata/Builtins.lc 520:39-520:48 Nat -> Type->Type +testdata/Builtins.lc 520:39-520:50 Type->Type +testdata/Builtins.lc 520:39-520:56 Type +testdata/Builtins.lc 520:49-520:50 V1 +testdata/Builtins.lc 520:51-520:56 Type +testdata/Builtins.lc 520:61-520:62 Type +testdata/Builtins.lc 520:61-520:67 Type +testdata/Builtins.lc 520:66-520:67 Type +testdata/Builtins.lc 522:1-522:11 {a:Nat} -> VecScalar a Float -> Float testdata/Builtins.lc 522:34-522:43 Nat -> Type->Type testdata/Builtins.lc 522:34-522:45 Type->Type testdata/Builtins.lc 522:34-522:51 Type -testdata/Builtins.lc 522:34-522:66 Type +testdata/Builtins.lc 522:34-522:60 Type testdata/Builtins.lc 522:44-522:45 V1 testdata/Builtins.lc 522:46-522:51 Type -testdata/Builtins.lc 522:55-522:58 Nat -> Type->Type -testdata/Builtins.lc 522:55-522:60 Type->Type -testdata/Builtins.lc 522:55-522:66 Type -testdata/Builtins.lc 522:59-522:60 V1 -testdata/Builtins.lc 522:61-522:66 Type -testdata/Builtins.lc 523:1-523:11 {a:Nat} -> VecScalar a Float -> VecS Float 3 +testdata/Builtins.lc 522:55-522:60 Type +testdata/Builtins.lc 523:1-523:11 {a:Nat} -> VecScalar a Float -> VecS Float 2 testdata/Builtins.lc 523:34-523:43 Nat -> Type->Type testdata/Builtins.lc 523:34-523:45 Type->Type testdata/Builtins.lc 523:34-523:51 Type @@ -2728,7 +2708,7 @@ testdata/Builtins.lc 523:55-523:60 Type->Type testdata/Builtins.lc 523:55-523:66 Type testdata/Builtins.lc 523:59-523:60 V1 testdata/Builtins.lc 523:61-523:66 Type -testdata/Builtins.lc 524:1-524:11 {a:Nat} -> VecScalar a Float -> VecS Float 4 +testdata/Builtins.lc 524:1-524:11 {a:Nat} -> VecScalar a Float -> VecS Float 3 testdata/Builtins.lc 524:34-524:43 Nat -> Type->Type testdata/Builtins.lc 524:34-524:45 Type->Type testdata/Builtins.lc 524:34-524:51 Type @@ -2740,82 +2720,94 @@ testdata/Builtins.lc 524:55-524:60 Type->Type testdata/Builtins.lc 524:55-524:66 Type testdata/Builtins.lc 524:59-524:60 V1 testdata/Builtins.lc 524:61-524:66 Type -testdata/Builtins.lc 540:6-540:13 Type -testdata/Builtins.lc 540:6-544:12 Type -testdata/Builtins.lc 541:3-541:16 String->Texture | Texture | Type -testdata/Builtins.lc 541:20-541:26 Type -testdata/Builtins.lc 542:20-542:27 Type -testdata/Builtins.lc 544:3-544:12 Texture | Type | VecS Int 2 -> Image 1 (Color (VecS Float 4)) -> Texture -testdata/Builtins.lc 544:20-544:23 Nat -> Type->Type -testdata/Builtins.lc 544:20-544:25 Type->Type -testdata/Builtins.lc 544:20-544:29 Type -testdata/Builtins.lc 544:24-544:25 V1 -testdata/Builtins.lc 544:26-544:29 Type -testdata/Builtins.lc 545:20-545:25 Nat -> Type->Type -testdata/Builtins.lc 545:20-545:27 Type->Type -testdata/Builtins.lc 545:20-545:49 Type -testdata/Builtins.lc 545:20-546:27 Type -testdata/Builtins.lc 545:26-545:27 V1 -testdata/Builtins.lc 545:28-545:49 Type -testdata/Builtins.lc 545:29-545:34 Type->Type -testdata/Builtins.lc 545:35-545:48 Type -testdata/Builtins.lc 545:36-545:39 Nat -> Type->Type -testdata/Builtins.lc 545:36-545:41 Type->Type -testdata/Builtins.lc 545:40-545:41 V1 -testdata/Builtins.lc 545:42-545:47 Type -testdata/Builtins.lc 546:20-546:27 Type -testdata/Builtins.lc 548:6-548:12 Type -testdata/Builtins.lc 548:6-550:17 Type -testdata/Builtins.lc 549:5-549:16 Filter -testdata/Builtins.lc 550:5-550:17 Filter -testdata/Builtins.lc 552:6-552:14 Type -testdata/Builtins.lc 552:6-555:16 Type -testdata/Builtins.lc 553:5-553:11 EdgeMode -testdata/Builtins.lc 554:5-554:19 EdgeMode -testdata/Builtins.lc 555:5-555:16 EdgeMode -testdata/Builtins.lc 557:6-557:13 Type -testdata/Builtins.lc 557:6-557:23 Type -testdata/Builtins.lc 557:6-557:47 Type -testdata/Builtins.lc 557:16-557:23 Filter -> EdgeMode -> Texture->Sampler | Sampler | Type -testdata/Builtins.lc 557:24-557:30 Type -testdata/Builtins.lc 557:31-557:39 Type -testdata/Builtins.lc 557:40-557:47 Type -testdata/Builtins.lc 560:1-560:10 Sampler -> VecS Float 2 -> VecS Float 4 -testdata/Builtins.lc 560:14-560:21 Type -testdata/Builtins.lc 560:25-560:28 Nat -> Type->Type -testdata/Builtins.lc 560:25-560:30 Type->Type -testdata/Builtins.lc 560:25-560:36 Type -testdata/Builtins.lc 560:25-560:51 Type -testdata/Builtins.lc 560:29-560:30 V1 -testdata/Builtins.lc 560:31-560:36 Type -testdata/Builtins.lc 560:40-560:43 Nat -> Type->Type -testdata/Builtins.lc 560:40-560:45 Type->Type -testdata/Builtins.lc 560:40-560:51 Type -testdata/Builtins.lc 560:44-560:45 V1 -testdata/Builtins.lc 560:46-560:51 Type -testdata/Builtins.lc 563:1-563:15 {a} -> {b} -> a -> b -> Tuple2 a b -testdata/Builtins.lc 563:24-563:32 Tuple2 V3 V1 -testdata/Builtins.lc 563:25-563:28 V5 -testdata/Builtins.lc 563:30-563:31 V2 -testdata/Builtins.lc 564:1-564:8 {a:Nat} -> {b} -> FrameBuffer a b -> Tuple2 (FragOps' b) (List (Vector a (Maybe (SimpleFragment (RemSemantics b))))) -> FrameBuffer a b -testdata/Builtins.lc 564:13-564:21 V3 -testdata/Builtins.lc 564:13-564:46 FrameBuffer V1 V0 -testdata/Builtins.lc 564:25-564:35 {a:Nat} -> {b} -> FragOps' b -> List (Vector a (Maybe (SimpleFragment (RemSemantics b)))) -> FrameBuffer a b -> FrameBuffer a b -testdata/Builtins.lc 564:25-564:39 List (Vector V1 (Maybe (SimpleFragment (RemSemantics V0)))) -> FrameBuffer V2 V1 -> FrameBuffer V3 V2 -testdata/Builtins.lc 564:25-564:43 FrameBuffer V1 V0 -> FrameBuffer V2 V1 -testdata/Builtins.lc 564:25-564:46 FrameBuffer V1 V0 | V2 -> V2->V2 | V2->V2 -testdata/Builtins.lc 564:36-564:39 V6 -testdata/Builtins.lc 564:40-564:43 V5 -testdata/Builtins.lc 564:44-564:46 V7 -testdata/Builtins.lc 565:1-565:12 {a:Nat} -> {b} -> FrameBuffer a b -> Output -testdata/Builtins.lc 565:15-565:24 {a:Nat} -> {b} -> FrameBuffer a b -> Output -testdata/Builtins.lc 566:1-566:11 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a -testdata/Builtins.lc 566:14-566:25 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a -testdata/Builtins.lc 567:1-567:16 Float -> Image 1 (Depth Float) -testdata/Builtins.lc 567:19-567:29 {a:Nat} -> Float -> Image a (Depth Float) -testdata/Builtins.lc 567:19-567:32 Float -> Image 1 (Depth Float) -testdata/Builtins.lc 567:31-567:32 V1 -testdata/Builtins.lc 568:1-568:16 {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 (Color c) -testdata/Builtins.lc 568:19-568:29 {a:Nat} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : d ~ VecScalar b c} -> d -> Image a (Color d) -testdata/Builtins.lc 568:19-568:32 {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 (Color c) +testdata/Builtins.lc 525:1-525:11 {a:Nat} -> VecScalar a Float -> VecS Float 4 +testdata/Builtins.lc 525:34-525:43 Nat -> Type->Type +testdata/Builtins.lc 525:34-525:45 Type->Type +testdata/Builtins.lc 525:34-525:51 Type +testdata/Builtins.lc 525:34-525:66 Type +testdata/Builtins.lc 525:44-525:45 V1 +testdata/Builtins.lc 525:46-525:51 Type +testdata/Builtins.lc 525:55-525:58 Nat -> Type->Type +testdata/Builtins.lc 525:55-525:60 Type->Type +testdata/Builtins.lc 525:55-525:66 Type +testdata/Builtins.lc 525:59-525:60 V1 +testdata/Builtins.lc 525:61-525:66 Type +testdata/Builtins.lc 541:6-541:13 Type +testdata/Builtins.lc 541:6-545:12 Type +testdata/Builtins.lc 542:3-542:16 String->Texture | Texture | Type +testdata/Builtins.lc 542:20-542:26 Type +testdata/Builtins.lc 543:20-543:27 Type +testdata/Builtins.lc 545:3-545:12 Texture | Type | VecS Int 2 -> Image 1 (Color (VecS Float 4)) -> Texture +testdata/Builtins.lc 545:20-545:23 Nat -> Type->Type +testdata/Builtins.lc 545:20-545:25 Type->Type +testdata/Builtins.lc 545:20-545:29 Type +testdata/Builtins.lc 545:24-545:25 V1 +testdata/Builtins.lc 545:26-545:29 Type +testdata/Builtins.lc 546:20-546:25 Nat -> Type->Type +testdata/Builtins.lc 546:20-546:27 Type->Type +testdata/Builtins.lc 546:20-546:49 Type +testdata/Builtins.lc 546:20-547:27 Type +testdata/Builtins.lc 546:26-546:27 V1 +testdata/Builtins.lc 546:28-546:49 Type +testdata/Builtins.lc 546:29-546:34 Type->Type +testdata/Builtins.lc 546:35-546:48 Type +testdata/Builtins.lc 546:36-546:39 Nat -> Type->Type +testdata/Builtins.lc 546:36-546:41 Type->Type +testdata/Builtins.lc 546:40-546:41 V1 +testdata/Builtins.lc 546:42-546:47 Type +testdata/Builtins.lc 547:20-547:27 Type +testdata/Builtins.lc 549:6-549:12 Type +testdata/Builtins.lc 549:6-551:17 Type +testdata/Builtins.lc 550:5-550:16 Filter +testdata/Builtins.lc 551:5-551:17 Filter +testdata/Builtins.lc 553:6-553:14 Type +testdata/Builtins.lc 553:6-556:16 Type +testdata/Builtins.lc 554:5-554:11 EdgeMode +testdata/Builtins.lc 555:5-555:19 EdgeMode +testdata/Builtins.lc 556:5-556:16 EdgeMode +testdata/Builtins.lc 558:6-558:13 Type +testdata/Builtins.lc 558:6-558:23 Type +testdata/Builtins.lc 558:6-558:47 Type +testdata/Builtins.lc 558:16-558:23 Filter -> EdgeMode -> Texture->Sampler | Sampler | Type +testdata/Builtins.lc 558:24-558:30 Type +testdata/Builtins.lc 558:31-558:39 Type +testdata/Builtins.lc 558:40-558:47 Type +testdata/Builtins.lc 561:1-561:10 Sampler -> VecS Float 2 -> VecS Float 4 +testdata/Builtins.lc 561:14-561:21 Type +testdata/Builtins.lc 561:25-561:28 Nat -> Type->Type +testdata/Builtins.lc 561:25-561:30 Type->Type +testdata/Builtins.lc 561:25-561:36 Type +testdata/Builtins.lc 561:25-561:51 Type +testdata/Builtins.lc 561:29-561:30 V1 +testdata/Builtins.lc 561:31-561:36 Type +testdata/Builtins.lc 561:40-561:43 Nat -> Type->Type +testdata/Builtins.lc 561:40-561:45 Type->Type +testdata/Builtins.lc 561:40-561:51 Type +testdata/Builtins.lc 561:44-561:45 V1 +testdata/Builtins.lc 561:46-561:51 Type +testdata/Builtins.lc 564:1-564:15 {a} -> {b} -> a -> b -> Tuple2 a b +testdata/Builtins.lc 564:24-564:32 Tuple2 V3 V1 +testdata/Builtins.lc 564:25-564:28 V5 +testdata/Builtins.lc 564:30-564:31 V2 +testdata/Builtins.lc 565:1-565:8 {a} -> {b:Nat} -> FrameBuffer b a -> Tuple2 (FragOps a) (List (Vector b (Maybe (SimpleFragment (RemSemantics a))))) -> FrameBuffer b a +testdata/Builtins.lc 565:13-565:21 V3 +testdata/Builtins.lc 565:13-565:46 FrameBuffer V0 V1 +testdata/Builtins.lc 565:25-565:35 {a} -> {b:Nat} -> FragOps a -> List (Vector b (Maybe (SimpleFragment (RemSemantics a)))) -> FrameBuffer b a -> FrameBuffer b a +testdata/Builtins.lc 565:25-565:39 List (Vector V0 (Maybe (SimpleFragment (RemSemantics V1)))) -> FrameBuffer V1 V2 -> FrameBuffer V2 V3 +testdata/Builtins.lc 565:25-565:43 FrameBuffer V0 V1 -> FrameBuffer V1 V2 +testdata/Builtins.lc 565:25-565:46 FrameBuffer V0 V1 | V2 -> V2->V2 | V2->V2 +testdata/Builtins.lc 565:36-565:39 V6 +testdata/Builtins.lc 565:40-565:43 V5 +testdata/Builtins.lc 565:44-565:46 V7 +testdata/Builtins.lc 566:1-566:12 {a:Nat} -> {b} -> FrameBuffer a b -> Output +testdata/Builtins.lc 566:15-566:24 {a:Nat} -> {b} -> FrameBuffer a b -> Output +testdata/Builtins.lc 567:1-567:11 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a +testdata/Builtins.lc 567:14-567:25 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a +testdata/Builtins.lc 568:1-568:16 Float -> Image 1 (Depth Float) +testdata/Builtins.lc 568:19-568:29 {a:Nat} -> Float -> Image a (Depth Float) +testdata/Builtins.lc 568:19-568:32 Float -> Image 1 (Depth Float) testdata/Builtins.lc 568:31-568:32 V1 +testdata/Builtins.lc 569:1-569:16 {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 (Color c) +testdata/Builtins.lc 569:19-569:29 {a:Nat} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : d ~ VecScalar b c} -> d -> Image a (Color d) +testdata/Builtins.lc 569:19-569:32 {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 (Color c) +testdata/Builtins.lc 569:31-569:32 V1 -- cgit v1.2.3