Skip to content

Commit 0a17d13

Browse files
hargoniXhargoniX
committed
tests
1 parent 7a192ba commit 0a17d13

File tree

1 file changed

+299
-0
lines changed

1 file changed

+299
-0
lines changed

‎tests/elab/simple_ground_extraction.lean‎

Lines changed: 299 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -606,3 +606,302 @@ trace: [Compiler.simpleGround] Marked usizePair._closed_0._boxed_const_1 as simp
606606
set_option trace.Compiler.saveImpure true in
607607
set_option trace.Compiler.simpleGround true in
608608
def usizePair : USize × USize := (1,3)
609+
610+
/--
611+
trace: [Compiler.simpleGround] Marked arrayNatTest._closed_0 as simple ground expr
612+
[Compiler.simpleGround] Marked arrayNatTest as simple ground expr
613+
[Compiler.saveImpure] size: 7
614+
def arrayNatTest._closed_0 : obj :=
615+
let _x.1 := 2;
616+
let _x.2 := 1;
617+
let _x.3 := 3;
618+
let _x.4 := Array.mkEmpty ◾ _x.3;
619+
let _x.5 := Array.push ◾ _x.4 _x.2;
620+
let _x.6 := Array.push ◾ _x.5 _x.1;
621+
let _x.7 := Array.push ◾ _x.6 _x.3;
622+
return _x.7
623+
[Compiler.saveImpure] size: 1
624+
def arrayNatTest : obj :=
625+
let _x.1 := arrayNatTest._closed_0;
626+
return _x.1
627+
-/
628+
#guard_msgs in
629+
set_option trace.Compiler.saveImpure true in
630+
set_option trace.Compiler.simpleGround true in
631+
def arrayNatTest : Array Nat := #[1, 2, 3]
632+
633+
/--
634+
trace: [Compiler.simpleGround] Marked emptyArrayTest._closed_0 as simple ground expr
635+
[Compiler.simpleGround] Marked emptyArrayTest as simple ground expr
636+
[Compiler.saveImpure] size: 2
637+
def emptyArrayTest._closed_0 : obj :=
638+
let _x.1 := 0;
639+
let _x.2 := Array.mkEmpty ◾ _x.1;
640+
return _x.2
641+
[Compiler.saveImpure] size: 1
642+
def emptyArrayTest : obj :=
643+
let _x.1 := emptyArrayTest._closed_0;
644+
return _x.1
645+
-/
646+
#guard_msgs in
647+
set_option trace.Compiler.saveImpure true in
648+
set_option trace.Compiler.simpleGround true in
649+
def emptyArrayTest : Array Nat := #[]
650+
651+
/--
652+
trace: [Compiler.simpleGround] Marked arrayStringTest._closed_0 as simple ground expr
653+
[Compiler.simpleGround] Marked arrayStringTest._closed_1 as simple ground expr
654+
[Compiler.simpleGround] Marked arrayStringTest._closed_2 as simple ground expr
655+
[Compiler.simpleGround] Marked arrayStringTest as simple ground expr
656+
[Compiler.saveImpure] size: 1
657+
def arrayStringTest._closed_0 : obj :=
658+
let _x.1 := "hello";
659+
return _x.1
660+
[Compiler.saveImpure] size: 1
661+
def arrayStringTest._closed_1 : obj :=
662+
let _x.1 := "world";
663+
return _x.1
664+
[Compiler.saveImpure] size: 6
665+
def arrayStringTest._closed_2 : obj :=
666+
let _x.1 := arrayStringTest._closed_1;
667+
let _x.2 := arrayStringTest._closed_0;
668+
let _x.3 := 2;
669+
let _x.4 := Array.mkEmpty ◾ _x.3;
670+
let _x.5 := Array.push ◾ _x.4 _x.2;
671+
let _x.6 := Array.push ◾ _x.5 _x.1;
672+
return _x.6
673+
[Compiler.saveImpure] size: 1
674+
def arrayStringTest : obj :=
675+
let _x.1 := arrayStringTest._closed_2;
676+
return _x.1
677+
-/
678+
#guard_msgs in
679+
set_option trace.Compiler.saveImpure true in
680+
set_option trace.Compiler.simpleGround true in
681+
def arrayStringTest : Array String := #["hello", "world"]
682+
683+
/--
684+
trace: [Compiler.simpleGround] Marked arrayUInt8Test._closed_0 as simple ground expr
685+
[Compiler.simpleGround] Marked arrayUInt8Test as simple ground expr
686+
[Compiler.saveImpure] size: 11
687+
def arrayUInt8Test._closed_0 : obj :=
688+
let _x.1 := 3;
689+
let _x.2 := 2;
690+
let _x.3 := 1;
691+
let _x.4 := 3;
692+
let _x.5 := Array.mkEmpty ◾ _x.4;
693+
let _x.6 := box _x.3;
694+
let _x.7 := Array.push ◾ _x.5 _x.6;
695+
let _x.8 := box _x.2;
696+
let _x.9 := Array.push ◾ _x.7 _x.8;
697+
let _x.10 := box _x.1;
698+
let _x.11 := Array.push ◾ _x.9 _x.10;
699+
return _x.11
700+
[Compiler.saveImpure] size: 1
701+
def arrayUInt8Test : obj :=
702+
let _x.1 := arrayUInt8Test._closed_0;
703+
return _x.1
704+
-/
705+
#guard_msgs in
706+
set_option trace.Compiler.saveImpure true in
707+
set_option trace.Compiler.simpleGround true in
708+
def arrayUInt8Test : Array UInt8 := #[1, 2, 3]
709+
710+
/--
711+
trace: [Compiler.simpleGround] Marked arrayUInt16Test._closed_0 as simple ground expr
712+
[Compiler.simpleGround] Marked arrayUInt16Test as simple ground expr
713+
[Compiler.saveImpure] size: 11
714+
def arrayUInt16Test._closed_0 : obj :=
715+
let _x.1 := 3;
716+
let _x.2 := 2;
717+
let _x.3 := 1;
718+
let _x.4 := 3;
719+
let _x.5 := Array.mkEmpty ◾ _x.4;
720+
let _x.6 := box _x.3;
721+
let _x.7 := Array.push ◾ _x.5 _x.6;
722+
let _x.8 := box _x.2;
723+
let _x.9 := Array.push ◾ _x.7 _x.8;
724+
let _x.10 := box _x.1;
725+
let _x.11 := Array.push ◾ _x.9 _x.10;
726+
return _x.11
727+
[Compiler.saveImpure] size: 1
728+
def arrayUInt16Test : obj :=
729+
let _x.1 := arrayUInt16Test._closed_0;
730+
return _x.1
731+
-/
732+
#guard_msgs in
733+
set_option trace.Compiler.saveImpure true in
734+
set_option trace.Compiler.simpleGround true in
735+
def arrayUInt16Test : Array UInt16 := #[1, 2, 3]
736+
737+
/--
738+
trace: [Compiler.simpleGround] Marked arrayUInt64._closed_0._boxed_const_1 as simple ground expr
739+
[Compiler.simpleGround] Marked arrayUInt64._closed_0._boxed_const_2 as simple ground expr
740+
[Compiler.simpleGround] Marked arrayUInt64._closed_0._boxed_const_3 as simple ground expr
741+
[Compiler.simpleGround] Marked arrayUInt64._closed_0 as simple ground expr
742+
[Compiler.simpleGround] Marked arrayUInt64 as simple ground expr
743+
[Compiler.saveImpure] size: 2
744+
def arrayUInt64._closed_0._boxed_const_1 : tobj :=
745+
let _x.1 := 34;
746+
let _x.2 := box _x.1;
747+
return _x.2
748+
[Compiler.saveImpure] size: 2
749+
def arrayUInt64._closed_0._boxed_const_2 : tobj :=
750+
let _x.1 := 23;
751+
let _x.2 := box _x.1;
752+
return _x.2
753+
[Compiler.saveImpure] size: 2
754+
def arrayUInt64._closed_0._boxed_const_3 : tobj :=
755+
let _x.1 := 11;
756+
let _x.2 := box _x.1;
757+
return _x.2
758+
[Compiler.saveImpure] size: 8
759+
def arrayUInt64._closed_0 : obj :=
760+
let _x.1 := 3;
761+
let _x.2 := Array.mkEmpty ◾ _x.1;
762+
let _x.3 := arrayUInt64._closed_0._boxed_const_3;
763+
let _x.4 := Array.push ◾ _x.2 _x.3;
764+
let _x.5 := arrayUInt64._closed_0._boxed_const_2;
765+
let _x.6 := Array.push ◾ _x.4 _x.5;
766+
let _x.7 := arrayUInt64._closed_0._boxed_const_1;
767+
let _x.8 := Array.push ◾ _x.6 _x.7;
768+
return _x.8
769+
[Compiler.saveImpure] size: 1
770+
def arrayUInt64 : obj :=
771+
let _x.1 := arrayUInt64._closed_0;
772+
return _x.1
773+
-/
774+
#guard_msgs in
775+
set_option trace.Compiler.saveImpure true in
776+
set_option trace.Compiler.simpleGround true in
777+
def arrayUInt64 : Array UInt64 := #[11, 23, 34]
778+
779+
/--
780+
trace: [Compiler.simpleGround] Marked arrayUSize._closed_0._boxed_const_1 as simple ground expr
781+
[Compiler.simpleGround] Marked arrayUSize._closed_0._boxed_const_2 as simple ground expr
782+
[Compiler.simpleGround] Marked arrayUSize._closed_0._boxed_const_3 as simple ground expr
783+
[Compiler.simpleGround] Marked arrayUSize._closed_0 as simple ground expr
784+
[Compiler.simpleGround] Marked arrayUSize as simple ground expr
785+
[Compiler.saveImpure] size: 2
786+
def arrayUSize._closed_0._boxed_const_1 : tobj :=
787+
let _x.1 := 37;
788+
let _x.2 := box _x.1;
789+
return _x.2
790+
[Compiler.saveImpure] size: 2
791+
def arrayUSize._closed_0._boxed_const_2 : tobj :=
792+
let _x.1 := 27;
793+
let _x.2 := box _x.1;
794+
return _x.2
795+
[Compiler.saveImpure] size: 2
796+
def arrayUSize._closed_0._boxed_const_3 : tobj :=
797+
let _x.1 := 17;
798+
let _x.2 := box _x.1;
799+
return _x.2
800+
[Compiler.saveImpure] size: 8
801+
def arrayUSize._closed_0 : obj :=
802+
let _x.1 := 3;
803+
let _x.2 := Array.mkEmpty ◾ _x.1;
804+
let _x.3 := arrayUSize._closed_0._boxed_const_3;
805+
let _x.4 := Array.push ◾ _x.2 _x.3;
806+
let _x.5 := arrayUSize._closed_0._boxed_const_2;
807+
let _x.6 := Array.push ◾ _x.4 _x.5;
808+
let _x.7 := arrayUSize._closed_0._boxed_const_1;
809+
let _x.8 := Array.push ◾ _x.6 _x.7;
810+
return _x.8
811+
[Compiler.saveImpure] size: 1
812+
def arrayUSize : obj :=
813+
let _x.1 := arrayUSize._closed_0;
814+
return _x.1
815+
-/
816+
#guard_msgs in
817+
set_option trace.Compiler.saveImpure true in
818+
set_option trace.Compiler.simpleGround true in
819+
def arrayUSize : Array USize := #[17, 27, 37]
820+
821+
/--
822+
trace: [Compiler.simpleGround] Marked arrayNatPair._closed_0 as simple ground expr
823+
[Compiler.simpleGround] Marked arrayNatPair._closed_1 as simple ground expr
824+
[Compiler.simpleGround] Marked arrayNatPair._closed_2 as simple ground expr
825+
[Compiler.simpleGround] Marked arrayNatPair as simple ground expr
826+
[Compiler.saveImpure] size: 3
827+
def arrayNatPair._closed_0 : obj :=
828+
let _x.1 := 2;
829+
let _x.2 := 1;
830+
let _x.3 := ctor_0[Prod.mk] _x.2 _x.1;
831+
return _x.3
832+
[Compiler.saveImpure] size: 3
833+
def arrayNatPair._closed_1 : obj :=
834+
let _x.1 := 4;
835+
let _x.2 := 3;
836+
let _x.3 := ctor_0[Prod.mk] _x.2 _x.1;
837+
return _x.3
838+
[Compiler.saveImpure] size: 6
839+
def arrayNatPair._closed_2 : obj :=
840+
let _x.1 := arrayNatPair._closed_1;
841+
let _x.2 := arrayNatPair._closed_0;
842+
let _x.3 := 2;
843+
let _x.4 := Array.mkEmpty ◾ _x.3;
844+
let _x.5 := Array.push ◾ _x.4 _x.2;
845+
let _x.6 := Array.push ◾ _x.5 _x.1;
846+
return _x.6
847+
[Compiler.saveImpure] size: 1
848+
def arrayNatPair : obj :=
849+
let _x.1 := arrayNatPair._closed_2;
850+
return _x.1
851+
-/
852+
#guard_msgs in
853+
set_option trace.Compiler.saveImpure true in
854+
set_option trace.Compiler.simpleGround true in
855+
def arrayNatPair : Array (Nat × Nat) := #[(1,2), (3,4)]
856+
857+
/--
858+
trace: [Compiler.simpleGround] Marked byteArrayTest._closed_0 as simple ground expr
859+
[Compiler.simpleGround] Marked byteArrayTest as simple ground expr
860+
[Compiler.saveImpure] size: 12
861+
def byteArrayTest._closed_0 : obj :=
862+
let _x.1 := 67;
863+
let _x.2 := 66;
864+
let _x.3 := 65;
865+
let _x.4 := 3;
866+
let _x.5 := Array.mkEmpty ◾ _x.4;
867+
let _x.6 := box _x.3;
868+
let _x.7 := Array.push ◾ _x.5 _x.6;
869+
let _x.8 := box _x.2;
870+
let _x.9 := Array.push ◾ _x.7 _x.8;
871+
let _x.10 := box _x.1;
872+
let _x.11 := Array.push ◾ _x.9 _x.10;
873+
let _x.12 := ByteArray.mk _x.11;
874+
return _x.12
875+
[Compiler.saveImpure] size: 1
876+
def byteArrayTest : obj :=
877+
let _x.1 := byteArrayTest._closed_0;
878+
return _x.1
879+
-/
880+
#guard_msgs in
881+
set_option trace.Compiler.saveImpure true in
882+
set_option trace.Compiler.simpleGround true in
883+
def byteArrayTest : ByteArray := ⟨#[65, 66, 67]⟩
884+
885+
/--
886+
trace: [Compiler.simpleGround] Marked emptyByteArrayTest._closed_0 as simple ground expr
887+
[Compiler.simpleGround] Marked emptyByteArrayTest._closed_1 as simple ground expr
888+
[Compiler.simpleGround] Marked emptyByteArrayTest as simple ground expr
889+
[Compiler.saveImpure] size: 2
890+
def emptyByteArrayTest._closed_0 : obj :=
891+
let _x.1 := 0;
892+
let _x.2 := Array.mkEmpty ◾ _x.1;
893+
return _x.2
894+
[Compiler.saveImpure] size: 2
895+
def emptyByteArrayTest._closed_1 : obj :=
896+
let _x.1 := emptyByteArrayTest._closed_0;
897+
let _x.2 := ByteArray.mk _x.1;
898+
return _x.2
899+
[Compiler.saveImpure] size: 1
900+
def emptyByteArrayTest : obj :=
901+
let _x.1 := emptyByteArrayTest._closed_1;
902+
return _x.1
903+
-/
904+
#guard_msgs in
905+
set_option trace.Compiler.saveImpure true in
906+
set_option trace.Compiler.simpleGround true in
907+
def emptyByteArrayTest : ByteArray := ⟨#[]⟩

0 commit comments

Comments
 (0)