edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 04:43:25 +03:00
Code Issues Projects Releases Wiki Activity

Update idemode tests

Browse Source 
Change in evaluation order changes the internal names - not that we
should be exposing these anyway, but that can be tidied up later...
This commit is contained in:
Edwin Brady 2020-03-27 00:34:21 +00:00
parent bce7a5e747
commit 654c306ed5
2 changed files with 14 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
tests/ideMode/ideMode001/expected
View File

@ -1,14 +1,14 @@
000018(:protocol-version 2 0)
000038(:write-string "1/1: Building LocType (LocType.idr)" 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:176} a)")))))) 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)
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:176}_[] ?{_:177}_[])")))))) 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 "?{_:177}_[]")))))) 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 ?{_:178}_[] ?{_:177}_[])")))))) 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)
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 ?{_:169}_[] ?{_:168}_[])")))))) 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:159} : (Main.Vect n[0] a[1])) -> (({arg:160} : (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 ?{_: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)
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)

14
tests/ideMode/ideMode003/expected
View File

@ -1,14 +1,14 @@
000018(:protocol-version 2 0)
000038(:write-string "1/1: Building LocType (LocType.idr)" 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:176} a)")))))) 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)
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:176}_[] ?{_:177}_[])")))))) 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 "?{_:177}_[]")))))) 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 ?{_:178}_[] ?{_:177}_[])")))))) 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)
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 ?{_:169}_[] ?{_:168}_[])")))))) 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:159} : (Main.Vect n[0] a[1])) -> (({arg:160} : (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 ?{_: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)
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)