edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-08-17 03:40:33 +03:00
Code Issues Projects Releases Wiki Activity

Update test output

Browse Source
This commit is contained in:
Edwin Brady 2020-05-13 19:06:22 +01:00
parent a6e7326ab7
commit f5962e1ea4
8 changed files with 23 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
tests/ideMode/ideMode001/expected
View File

@ -2,13 +2,13 @@
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:258} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:259}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:258}_[] ?{_:259}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:263} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:264}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:263}_[] ?{_:264}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:239} : (Main.Vect n[0] a[1])) -> (({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:735:1--742:1 n[2] m[4]) a[3])))")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:735:1--742:1 n[2] m[4]) a[3])))")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

12
tests/ideMode/ideMode003/expected
View File

@ -2,13 +2,13 @@
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:258} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:259}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:258}_[] ?{_:259}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:263} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:264}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:263}_[] ?{_:264}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:239} : (Main.Vect n[0] a[1])) -> (({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:735:1--742:1 n[2] m[4]) a[3])))")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:735:1--742:1 n[2] m[4]) a[3])))")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

4
tests/idris2/basic030/expected
View File

@ -1,7 +1,7 @@
1/1: Building arity (arity.idr)
arity.idr:4:16--4:22:While processing right hand side of foo at arity.idr:4:1--7:1:
When unifying (1 {arg:236} : Nat) -> MyN and MyN
When unifying (1 {arg:241} : Nat) -> MyN and MyN
Mismatch between:
(1 {arg:236} : Nat) -> MyN
(1 {arg:241} : Nat) -> MyN
and
MyN

2
tests/ttimp/basic006/expected
View File

@ -2,5 +2,5 @@ Processing as TTImp
Written TTC
Yaffle> ((Main.Just [Just a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Integer]) 1) (Main.Vect.Nil [Just a = Integer])))
Yaffle> ((Main.MkInfer [Just a = (Main.List.List Integer)]) (((Main.List.Cons [Just a = Integer]) 1) (Main.List.Nil [Just a = Integer])))
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved119 ?Main.{a:62}_[]), ($resolved99 ?Main.{a:62}_[])]
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved120 ?Main.{a:62}_[]), ($resolved100 ?Main.{a:62}_[])]
Yaffle> Bye for now!

6
tests/ttimp/coverage001/expected
View File

@ -2,10 +2,10 @@ Processing as TTImp
Written TTC
Yaffle> Bye for now!
Processing as TTImp
Vect2.yaff:25:1--26:1:{pat 0 {b:27} : Type} => {pat 0 {a:26} : Type} => ($resolved115 {b:27}[1] {a:26}[0] $resolved97 ($resolved106 {a:26}[0]) ($resolved106 {b:27}[1])) is not a valid impossible pattern because it typechecks
Vect2.yaff:25:1--26:1:{pat 0 {b:27} : Type} => {pat 0 {a:26} : Type} => ($resolved116 {b:27}[1] {a:26}[0] $resolved98 ($resolved107 {a:26}[0]) ($resolved107 {b:27}[1])) is not a valid impossible pattern because it typechecks
Yaffle> Bye for now!
Processing as TTImp
Vect3.yaff:25:1--26:1:Not a valid impossible pattern:
Vect3.yaff:25:9--25:11:When unifying: $resolved96 and ($resolved104 ?Main.{n:21}_[] ?Main.{b:19}_[])
Vect3.yaff:25:9--25:11:Type mismatch: $resolved96 and ($resolved104 ?Main.{n:21}_[] ?Main.{b:19}_[])
Vect3.yaff:25:9--25:11:When unifying: $resolved97 and ($resolved105 ?Main.{n:21}_[] ?Main.{b:19}_[])
Vect3.yaff:25:9--25:11:Type mismatch: $resolved97 and ($resolved105 ?Main.{n:21}_[] ?Main.{b:19}_[])
Yaffle> Bye for now!

2
tests/ttimp/coverage002/expected
View File

@ -2,6 +2,6 @@ Processing as TTImp
Written TTC
Yaffle> Main.lookup: All cases covered
Yaffle> Main.lookup':
($resolved146 [__] [__] (Main.FZ [__]) {arg:3})
($resolved147 [__] [__] (Main.FZ [__]) {arg:3})
Yaffle> Main.lookup'': Calls non covering function Main.lookup'
Yaffle> Bye for now!

6
tests/ttimp/dot001/expected
View File

@ -3,13 +3,13 @@ Written TTC
Yaffle> Bye for now!
Processing as TTImp
Dot2.yaff:15:1--16:1:When elaborating left hand side of Main.half:
Dot2.yaff:15:28--15:30:Pattern variable {P:n:101} unifies with ?{P:m:101}_[]
Dot2.yaff:15:28--15:30:Pattern variable {P:n:102} unifies with ?{P:m:102}_[]
Yaffle> Bye for now!
Processing as TTImp
Dot3.yaff:18:1--20:1:When elaborating left hand side of Main.addBaz3:
Dot3.yaff:18:10--18:15:Can't match on ($resolved93 ?{P:x:106}_[] ?{P:x:106}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved93 ?Main.{_:13}_[] ?Main.{_:14}_[])
Dot3.yaff:18:10--18:15:Can't match on ($resolved94 ?{P:x:107}_[] ?{P:x:107}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved94 ?Main.{_:13}_[] ?Main.{_:14}_[])
Yaffle> Bye for now!
Processing as TTImp
Dot4.yaff:17:1--19:1:When elaborating left hand side of Main.addBaz4:
Dot4.yaff:17:33--17:34:Can't match on ?{P:x:108}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
Dot4.yaff:17:33--17:34:Can't match on ?{P:x:109}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
Yaffle> Bye for now!

2
tests/ttimp/eta002/expected
View File

@ -1,5 +1,5 @@
Processing as TTImp
Eta.yaff:16:1--17:1:When elaborating right hand side of Main.etaBad:
Eta.yaff:16:10--17:1:When unifying: ($resolved98 ?Main.{b:18}_[] ?Main.{b:18}_[] \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved108 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]) \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved108 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]])) and ($resolved98 ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved107)) (({arg:11} : Integer) -> (({arg:12} : Integer) -> $resolved107)) $resolved108 \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved108 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]))
Eta.yaff:16:10--17:1:When unifying: ($resolved99 ?Main.{b:18}_[] ?Main.{b:18}_[] \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved109 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]) \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved109 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]])) and ($resolved99 ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved108)) (({arg:11} : Integer) -> (({arg:12} : Integer) -> $resolved108)) $resolved109 \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved109 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]))
Eta.yaff:16:10--17:1:Type mismatch: Char and Integer
Yaffle> Bye for now!