idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

[ fix ] highlighting of tuples

Browse Source
This commit is contained in:
Guillaume ALLAIS 2021-05-13 23:09:17 +01:00 committed by G. Allais
parent 3610464a10
commit 4917d124aa
8 changed files with 253 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
src/Idris/Parser.idr
View File

@ -409,35 +409,38 @@ mutual
nonEmptyTuple : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
nonEmptyTuple fname s indents e
= do rest <- bounds (forget <$> some (bounds (decoratedSymbol fname "," *> optional (bounds (expr pdef fname indents))))
<* continueWith indents ")")
pure $ buildOutput rest (mergePairs 0 rest rest.val)
= do vals <- some $ do b <- bounds (symbol ",")
exp <- optional (expr pdef fname indents)
pure (boundToFC fname b, exp)
end <- continueWithDecorated fname indents ")"
act [(toNonEmptyFC (boundToFC fname s), Keyword, Nothing)]
pure $ let (start ::: rest) = vals in
buildOutput (fst start) (mergePairs 0 start rest)
where
lams : List (FC, PTerm) -> PTerm -> PTerm
lams [] e = e
lams ((fc, var) :: vars) e
= PLam fc top Explicit var (PInfer fc)
$ lams vars e
= let vfc = virtualiseFC fc in
PLam vfc top Explicit var (PInfer vfc) $ lams vars e
buildOutput : WithBounds t' -> (List (FC, PTerm), PTerm) -> PTerm
buildOutput rest (vars, scope) = lams vars $ PPair (boundToFC fname (mergeBounds s rest)) e scope
buildOutput : FC -> (List (FC, PTerm), PTerm) -> PTerm
buildOutput fc (vars, scope) = lams vars $ PPair fc e scope
optionalPair : Int -> WithBounds (Maybe (WithBounds PTerm)) -> (Int, (List (FC, PTerm), PTerm))
optionalPair i exp = case exp.val of
Just e => (i, ([], e.val))
Nothing => let fc = boundToFC fname exp in
let var = PRef fc (MN "__infixTupleSection" i) in
(i+1, ([(fc, var)], var))
optionalPair : Int ->
(FC, Maybe PTerm) -> (Int, (List (FC, PTerm), PTerm))
optionalPair i (fc, Just e) = (i, ([], e))
optionalPair i (fc, Nothing) =
let var = PRef fc (MN "__infixTupleSection" i) in
(i+1, ([(fc, var)], var))
mergePairs : Int -> WithBounds t' -> List (WithBounds (Maybe (WithBounds PTerm))) ->
(List (FC, PTerm), PTerm)
mergePairs _ end [] = ([], PUnit (boundToFC fname (mergeBounds s end)))
mergePairs i end [exp] = snd (optionalPair i exp)
mergePairs i end (exp :: rest)
= let (j, (var, t)) = optionalPair i exp in
let (vars, ts) = mergePairs j end rest in
(var ++ vars, PPair (boundToFC fname (mergeBounds exp end)) t ts)
mergePairs : Int -> (FC, Maybe PTerm) ->
List (FC, Maybe PTerm) -> (List (FC, PTerm), PTerm)
mergePairs i hd [] = snd (optionalPair i hd)
mergePairs i hd (exp :: rest)
= let (j, (var, t)) = optionalPair i hd in
let (vars, ts) = mergePairs j exp rest in
(var ++ vars, PPair (fst exp) t ts)
-- A pair, dependent pair, or just a single expression
tuple : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm

15
tests/ideMode/ideMode005/Tuples.idr Normal file
View File

@ -0,0 +1,15 @@
init : a -> c -> List b -> List (a, b, c)
init a c = map (uncurry (,)) . map (a,) . map (,c)
unzip : List (a, b) -> (List a, List b)
unzip [] = ([], [])
unzip ((a, b) :: abs)
= let (as, bs) = unzip abs in
(a :: as, b :: bs)
unzip4 : List (a, b, c, d) -> (List a, List b, List c, List d)
unzip4 [] = ([], [], [], [])
unzip4 (abcd :: abcds)
= let (a, b, c, d) = abcd
(as, bs, cs, ds) = unzip4 abcds
in (a :: as, b :: bs, c :: cs, d :: ds)

35
tests/ideMode/ideMode005/expected1
View File

@ -128,26 +128,30 @@
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 30 12) (:end 30 12)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 30 14) (:end 30 14)) ((:decor :keyword)))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 30 16) (:end 30 16)) ((:decor :data)))))) 1)
0000d4(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 8) (:end 31 13)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 8) (:end 31 8)) ((:decor :keyword)))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 9) (:end 31 9)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 10) (:end 31 10)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 10) (:end 31 10)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 12) (:end 31 12)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 13) (:end 31 13)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 15) (:end 31 16)) ((:decor :keyword)))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 18) (:end 31 21)) ((:name "Just") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 23) (:end 31 28)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 23) (:end 31 23)) ((:decor :keyword)))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 24) (:end 31 24)) ((:decor :data)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 25) (:end 31 25)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 25) (:end 31 25)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 27) (:end 31 27)) ((:decor :data)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 31 28) (:end 31 28)) ((:decor :keyword)))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 8) (:end 32 10)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 12) (:end 32 17)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 12) (:end 32 12)) ((:decor :keyword)))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 13) (:end 32 13)) ((:name "d") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 14) (:end 32 14)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 14) (:end 32 14)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 16) (:end 32 16)) ((:name "e") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 17) (:end 32 17)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 19) (:end 32 19)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 21) (:end 32 26)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 21) (:end 32 21)) ((:decor :keyword)))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 22) (:end 32 22)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 23) (:end 32 23)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 23) (:end 32 23)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 25) (:end 32 25)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 32 26) (:end 32 26)) ((:decor :keyword)))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 33 8) (:end 33 8)) ((:name "f") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 33 10) (:end 33 11)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 33 13) (:end 33 14)) ((:decor :keyword)))))) 1)
@ -265,25 +269,28 @@
0000e1(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 11) (:end 49 13)) ((:name "map") (:namespace "Prelude.Interfaces") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 15) (:end 49 15)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 16) (:end 49 16)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 18) (:end 49 23)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 18) (:end 49 18)) ((:decor :keyword)))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 19) (:end 49 19)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 20) (:end 49 20)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 20) (:end 49 20)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 22) (:end 49 22)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 23) (:end 49 23)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 25) (:end 49 26)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 28) (:end 49 33)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 28) (:end 49 28)) ((:decor :keyword)))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 29) (:end 49 29)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 30) (:end 49 30)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 30) (:end 49 30)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 32) (:end 49 32)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 33) (:end 49 33)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 49 34) (:end 49 34)) ((:decor :keyword)))))) 1)
0000e1(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 11) (:end 50 13)) ((:name "map") (:namespace "Prelude.Interfaces") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 15) (:end 50 15)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 16) (:end 50 16)) ((:decor :keyword)))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 18) (:end 50 18)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 20) (:end 50 21)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 23) (:end 50 28)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 23) (:end 50 23)) ((:decor :keyword)))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 24) (:end 50 24)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 25) (:end 50 25)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 25) (:end 50 25)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 27) (:end 50 27)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 28) (:end 50 28)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 50 29) (:end 50 29)) ((:decor :keyword)))))) 1)
0000e1(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 51 11) (:end 51 13)) ((:name "map") (:namespace "Prelude.Interfaces") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 51 15) (:end 51 15)) ((:decor :keyword)))))) 1)

5
tests/ideMode/ideMode005/expectedE
View File

@ -26,10 +26,11 @@
00007e(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 6 23) (:end 6 23)) ((:decor :keyword)))))) 1)
00007e(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 6 25) (:end 6 26)) ((:decor :keyword)))))) 1)
0000e3(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 6 28) (:end 6 31)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000dc(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 6 33) (:end 6 43)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
00007e(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 6 33) (:end 6 33)) ((:decor :keyword)))))) 1)
0000e3(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 6 34) (:end 6 37)) ((:name "Bool") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
00007e(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 6 38) (:end 6 38)) ((:decor :keyword)))))) 1)
0000dc(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 6 38) (:end 6 38)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000e1(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 6 40) (:end 6 42)) ((:name "Nat") (:namespace "Prelude.Types") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
00007e(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 6 43) (:end 6 43)) ((:decor :keyword)))))) 1)
0000db(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 7 1) (:end 7 4)) ((:name "proj") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000e0(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 7 6) (:end 7 7)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
00007e(:output (:ok (:highlight-source ((((:filename "RecordProjections.idr") (:start 7 16) (:end 7 16)) ((:decor :keyword)))))) 1)

185
tests/ideMode/ideMode005/expectedF Normal file
View File

@ -0,0 +1,185 @@
000018(:protocol-version 2 0)
000036(:write-string "1/1: Building Tuples (Tuples.idr)" 1)
000072(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 1) (:end 1 4)) ((:decor :function)))))) 1)
000071(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 6) (:end 1 6)) ((:decor :keyword)))))) 1)
0000c6(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 8) (:end 1 8)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 10) (:end 1 11)) ((:decor :keyword)))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 13) (:end 1 13)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 15) (:end 1 16)) ((:decor :keyword)))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 18) (:end 1 21)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 23) (:end 1 23)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 25) (:end 1 26)) ((:decor :keyword)))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 28) (:end 1 31)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 33) (:end 1 33)) ((:decor :keyword)))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 34) (:end 1 34)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 35) (:end 1 35)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 37) (:end 1 37)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 38) (:end 1 38)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 40) (:end 1 40)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 1 41) (:end 1 41)) ((:decor :keyword)))))) 1)
0000d0(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 1) (:end 2 4)) ((:name "init") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c6(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 6) (:end 2 6)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c6(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 8) (:end 2 8)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 10) (:end 2 10)) ((:decor :keyword)))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 12) (:end 2 14)) ((:name "map") (:namespace "Prelude.Interfaces") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 16) (:end 2 16)) ((:decor :keyword)))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 17) (:end 2 23)) ((:name "uncurry") (:namespace "Prelude.Basics") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 25) (:end 2 25)) ((:decor :keyword)))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 26) (:end 2 26)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 27) (:end 2 27)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 28) (:end 2 28)) ((:decor :keyword)))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 30) (:end 2 30)) ((:name ".") (:namespace "Prelude.Basics") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 32) (:end 2 34)) ((:name "map") (:namespace "Prelude.Interfaces") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 36) (:end 2 36)) ((:decor :keyword)))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 37) (:end 2 37)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 38) (:end 2 38)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 39) (:end 2 39)) ((:decor :keyword)))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 41) (:end 2 41)) ((:name ".") (:namespace "Prelude.Basics") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 43) (:end 2 45)) ((:name "map") (:namespace "Prelude.Interfaces") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 47) (:end 2 47)) ((:decor :keyword)))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 48) (:end 2 48)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 49) (:end 2 49)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 2 50) (:end 2 50)) ((:decor :keyword)))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 1) (:end 4 5)) ((:decor :function)))))) 1)
000071(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 7) (:end 4 7)) ((:decor :keyword)))))) 1)
0000d7(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 9) (:end 4 12)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 14) (:end 4 14)) ((:decor :keyword)))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 15) (:end 4 15)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 16) (:end 4 16)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 18) (:end 4 18)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 19) (:end 4 19)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 21) (:end 4 22)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 24) (:end 4 24)) ((:decor :keyword)))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 25) (:end 4 28)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 30) (:end 4 30)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 31) (:end 4 31)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 33) (:end 4 36)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 38) (:end 4 38)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 4 39) (:end 4 39)) ((:decor :keyword)))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 5 1) (:end 5 5)) ((:name "unzip") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 5 7) (:end 5 8)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 5 10) (:end 5 10)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 5 12) (:end 5 12)) ((:decor :keyword)))))) 1)
0000d7(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 5 13) (:end 5 14)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 5 15) (:end 5 15)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d7(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 5 17) (:end 5 18)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 5 19) (:end 5 19)) ((:decor :keyword)))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 6 1) (:end 6 5)) ((:name "unzip") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000071(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 6 7) (:end 6 7)) ((:decor :keyword)))))) 1)
000071(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 6 8) (:end 6 8)) ((:decor :keyword)))))) 1)
0000c6(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 6 9) (:end 6 9)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 6 10) (:end 6 10)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 6 12) (:end 6 12)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 6 13) (:end 6 13)) ((:decor :keyword)))))) 1)
0000d6(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 6 15) (:end 6 16)) ((:name "::") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 6 18) (:end 6 20)) ((:name "abs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 6 21) (:end 6 21)) ((:decor :keyword)))))) 1)
000071(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 3) (:end 7 3)) ((:decor :keyword)))))) 1)
000071(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 5) (:end 7 7)) ((:decor :keyword)))))) 1)
000071(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 9) (:end 7 9)) ((:decor :keyword)))))) 1)
0000c9(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 10) (:end 7 11)) ((:name "as") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 12) (:end 7 12)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c9(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 14) (:end 7 15)) ((:name "bs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 16) (:end 7 16)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 18) (:end 7 18)) ((:decor :keyword)))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 20) (:end 7 24)) ((:name "unzip") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 26) (:end 7 28)) ((:name "abs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 7 30) (:end 7 31)) ((:decor :keyword)))))) 1)
000071(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 8 5) (:end 8 5)) ((:decor :keyword)))))) 1)
0000c6(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 8 6) (:end 8 6)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d4(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 8 8) (:end 8 9)) ((:name "::") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c9(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 8 11) (:end 8 12)) ((:name "as") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 8 13) (:end 8 13)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 8 15) (:end 8 15)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d6(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 8 17) (:end 8 18)) ((:name "::") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c9(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 8 20) (:end 8 21)) ((:name "bs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 8 22) (:end 8 22)) ((:decor :keyword)))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 1) (:end 10 6)) ((:decor :function)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 8) (:end 10 8)) ((:decor :keyword)))))) 1)
0000da(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 10) (:end 10 13)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 15) (:end 10 15)) ((:decor :keyword)))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 16) (:end 10 16)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 17) (:end 10 17)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 19) (:end 10 19)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 20) (:end 10 20)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 22) (:end 10 22)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 23) (:end 10 23)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 25) (:end 10 25)) ((:name "d") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 26) (:end 10 26)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 28) (:end 10 29)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 31) (:end 10 31)) ((:decor :keyword)))))) 1)
0000da(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 32) (:end 10 35)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 37) (:end 10 37)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 38) (:end 10 38)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000da(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 40) (:end 10 43)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 45) (:end 10 45)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 46) (:end 10 46)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000da(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 48) (:end 10 51)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 53) (:end 10 53)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 54) (:end 10 54)) ((:name "Pair") (:namespace "Builtin") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000da(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 56) (:end 10 59)) ((:name "List") (:namespace "Prelude.Basics") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 61) (:end 10 61)) ((:name "d") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 10 62) (:end 10 62)) ((:decor :keyword)))))) 1)
0000d4(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 1) (:end 11 6)) ((:name "unzip4") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d7(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 8) (:end 11 9)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 11) (:end 11 11)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 13) (:end 11 13)) ((:decor :keyword)))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 14) (:end 11 15)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 16) (:end 11 16)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 18) (:end 11 19)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 20) (:end 11 20)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 22) (:end 11 23)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 24) (:end 11 24)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 26) (:end 11 27)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 11 28) (:end 11 28)) ((:decor :keyword)))))) 1)
0000d4(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 12 1) (:end 12 6)) ((:name "unzip4") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 12 8) (:end 12 8)) ((:decor :keyword)))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 12 9) (:end 12 12)) ((:name "abcd") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 12 14) (:end 12 15)) ((:name "::") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ce(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 12 17) (:end 12 21)) ((:name "abcds") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 12 22) (:end 12 22)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 3) (:end 13 3)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 5) (:end 13 7)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 9) (:end 13 9)) ((:decor :keyword)))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 10) (:end 13 10)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 11) (:end 13 11)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 13) (:end 13 13)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 14) (:end 13 14)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 16) (:end 13 16)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 17) (:end 13 17)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 19) (:end 13 19)) ((:name "d") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 20) (:end 13 20)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 22) (:end 13 22)) ((:decor :keyword)))))) 1)
0000cd(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 13 24) (:end 13 27)) ((:name "abcd") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 9) (:end 14 9)) ((:decor :keyword)))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 10) (:end 14 11)) ((:name "as") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 12) (:end 14 12)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 14) (:end 14 15)) ((:name "bs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 16) (:end 14 16)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 18) (:end 14 19)) ((:name "cs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 20) (:end 14 20)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 22) (:end 14 23)) ((:name "ds") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 24) (:end 14 24)) ((:decor :keyword)))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 26) (:end 14 26)) ((:decor :keyword)))))) 1)
0000d6(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 28) (:end 14 33)) ((:name "unzip4") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ce(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 14 35) (:end 14 39)) ((:name "abcds") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 5) (:end 15 6)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 8) (:end 15 8)) ((:decor :keyword)))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 9) (:end 15 9)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 11) (:end 15 12)) ((:name "::") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 14) (:end 15 15)) ((:name "as") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 16) (:end 15 16)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 18) (:end 15 18)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 20) (:end 15 21)) ((:name "::") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 23) (:end 15 24)) ((:name "bs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 25) (:end 15 25)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 27) (:end 15 27)) ((:name "c") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 29) (:end 15 30)) ((:name "::") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 32) (:end 15 33)) ((:name "cs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 34) (:end 15 34)) ((:name "MkPair") (:namespace "Builtin") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 36) (:end 15 36)) ((:name "d") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 38) (:end 15 39)) ((:name "::") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 41) (:end 15 42)) ((:name "ds") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000075(:output (:ok (:highlight-source ((((:filename "Tuples.idr") (:start 15 43) (:end 15 43)) ((:decor :keyword)))))) 1)
000015(:return (:ok ()) 1)
Alas the file is done, aborting

1
tests/ideMode/ideMode005/inputF Normal file
View File

@ -0,0 +1 @@
00001d((:load-file "Tuples.idr") 1)

1
tests/ideMode/ideMode005/regenerate
View File

@ -14,6 +14,7 @@ $1 --no-color --console-width 0 --ide-mode < inputB > expectedB
$1 --no-color --console-width 0 --ide-mode < inputC > expectedC
$1 --no-color --console-width 0 --ide-mode < inputD > expectedD
$1 --no-color --console-width 0 --ide-mode < inputE > expectedE
$1 --no-color --console-width 0 --ide-mode < inputF > expectedF
rm -f expected output*
touch expected

3
tests/ideMode/ideMode005/run
View File

@ -42,4 +42,7 @@ diff expectedD outputD >> output
$1 --no-color --console-width 0 --ide-mode < inputE > outputE
diff expectedE outputE >> output
$1 --no-color --console-width 0 --ide-mode < inputF > outputF
diff expectedF outputF >> output
rm -rf build