diff --git a/tests/ideMode/ideMode001/expected b/tests/ideMode/ideMode001/expected index 3270bc4..d390c5a 100644 --- a/tests/ideMode/ideMode001/expected +++ b/tests/ideMode/ideMode001/expected @@ -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) diff --git a/tests/ideMode/ideMode003/expected b/tests/ideMode/ideMode003/expected index 0ebd0e1..0b4505a 100644 --- a/tests/ideMode/ideMode003/expected +++ b/tests/ideMode/ideMode003/expected @@ -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) diff --git a/tests/idris2/basic030/expected b/tests/idris2/basic030/expected index 5e514f4..12247fc 100644 --- a/tests/idris2/basic030/expected +++ b/tests/idris2/basic030/expected @@ -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 diff --git a/tests/ttimp/basic006/expected b/tests/ttimp/basic006/expected index 3060e09..a24cc2b 100644 --- a/tests/ttimp/basic006/expected +++ b/tests/ttimp/basic006/expected @@ -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! diff --git a/tests/ttimp/coverage001/expected b/tests/ttimp/coverage001/expected index 99883c0..69004c9 100644 --- a/tests/ttimp/coverage001/expected +++ b/tests/ttimp/coverage001/expected @@ -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! diff --git a/tests/ttimp/coverage002/expected b/tests/ttimp/coverage002/expected index 5f45a6e..ee75a26 100644 --- a/tests/ttimp/coverage002/expected +++ b/tests/ttimp/coverage002/expected @@ -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! diff --git a/tests/ttimp/dot001/expected b/tests/ttimp/dot001/expected index b7e04f5..402a419 100644 --- a/tests/ttimp/dot001/expected +++ b/tests/ttimp/dot001/expected @@ -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! diff --git a/tests/ttimp/eta002/expected b/tests/ttimp/eta002/expected index 3209bae..11fc7d6 100644 --- a/tests/ttimp/eta002/expected +++ b/tests/ttimp/eta002/expected @@ -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!