diff --git a/tests/ideMode/ideMode001/expected b/tests/ideMode/ideMode001/expected index a56f175..a4dd830 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:190} 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 "?{_:191}_[]")))))) 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:190}_[] ?{_:191}_[])")))))) 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 ?{_:192}_[] ?{_:191}_[])")))))) 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:222} 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 "?{_:223}_[]")))))) 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:222}_[] ?{_:223}_[])")))))) 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 ?{_:224}_[] ?{_:223}_[])")))))) 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 ?{_:182}_[] ?{_:181}_[])")))))) 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:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637: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 ?{_:214}_[] ?{_:213}_[])")))))) 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:204} : (Main.Vect n[0] a[1])) -> (({arg:205} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637: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 932e3ad..610dd7d 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:190} 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 "?{_:191}_[]")))))) 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:190}_[] ?{_:191}_[])")))))) 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 ?{_:192}_[] ?{_:191}_[])")))))) 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:222} 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 "?{_:223}_[]")))))) 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:222}_[] ?{_:223}_[])")))))) 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 ?{_:224}_[] ?{_:223}_[])")))))) 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 ?{_:182}_[] ?{_:181}_[])")))))) 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:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637: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 ?{_:214}_[] ?{_:213}_[])")))))) 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:204} : (Main.Vect n[0] a[1])) -> (({arg:205} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637: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 5dbeaac..f38445d 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:169} : Nat) -> MyN and MyN +When unifying (1 {arg:201} : Nat) -> MyN and MyN Mismatch between: - (1 {arg:169} : Nat) -> MyN + (1 {arg:201} : Nat) -> MyN and MyN diff --git a/tests/idris2/record002/Record.idr b/tests/idris2/record002/Record.idr index 09b2e83..c3595aa 100644 --- a/tests/idris2/record002/Record.idr +++ b/tests/idris2/record002/Record.idr @@ -35,4 +35,4 @@ testPerson : Person testPerson = MkPerson "Fred" 1337 10 (MkStats 10 10) grow : Person -> Person -grow = record { more->height $= (+1) } +grow = record { more.height $= (+1) } diff --git a/tests/idris2/record002/input b/tests/idris2/record002/input index 1179c70..3e4deaf 100644 --- a/tests/idris2/record002/input +++ b/tests/idris2/record002/input @@ -2,5 +2,5 @@ grow testPerson grow (grow testPerson) cons 10 testPair cons' 10 testPair -record { more -> weight = 94 } testPerson +record { more.weight = 94 } testPerson :q diff --git a/tests/idris2/reg010/recordname.idr b/tests/idris2/reg010/Recordname.idr similarity index 71% rename from tests/idris2/reg010/recordname.idr rename to tests/idris2/reg010/Recordname.idr index 7abe744..54955a3 100644 --- a/tests/idris2/reg010/recordname.idr +++ b/tests/idris2/reg010/Recordname.idr @@ -1,4 +1,4 @@ -module recordname +module Recordname namespace Foo export @@ -9,4 +9,4 @@ namespace Foo x : Name -> Int x = foo -test : recordname.Foo.Name +test : Recordname.Foo.Name diff --git a/tests/idris2/reg010/expected b/tests/idris2/reg010/expected index 6830eab..0eb2106 100644 --- a/tests/idris2/reg010/expected +++ b/tests/idris2/reg010/expected @@ -1 +1 @@ -1/1: Building recordname (recordname.idr) +1/1: Building Recordname (Recordname.idr) diff --git a/tests/idris2/reg010/run b/tests/idris2/reg010/run index 0b5a0fb..4605350 100755 --- a/tests/idris2/reg010/run +++ b/tests/idris2/reg010/run @@ -1,3 +1,3 @@ -$1 recordname.idr --check +$1 Recordname.idr --check rm -rf build diff --git a/tests/typedd-book/chapter12/ArithState.idr b/tests/typedd-book/chapter12/ArithState.idr index ea4db61..5066d35 100644 --- a/tests/typedd-book/chapter12/ArithState.idr +++ b/tests/typedd-book/chapter12/ArithState.idr @@ -23,11 +23,11 @@ initState : GameState initState = MkGameState (MkScore 0 0) 12 addWrong : GameState -> GameState -addWrong = record { score->attempted $= (+1) } +addWrong = record { score.attempted $= (+1) } addCorrect : GameState -> GameState -addCorrect = record { score->correct $= (+1), - score->attempted $= (+1) } +addCorrect = record { score.correct $= (+1), + score.attempted $= (+1) } setDifficulty : Int -> GameState -> GameState setDifficulty newDiff state = record { difficulty = newDiff } state