Skip to content

Commit 3575937

Browse files
andreiburdusattuegel
andreiburdusa
and
ttuegel
authored
Make concatMap symbol function instead of functional (#2122)
* wip * Update four tests * Update last test * Change concatSetSymbol Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
1 parent 6ef19e9 commit 3575937

File tree

3 files changed

+130
-10
lines changed

3 files changed

+130
-10
lines changed

‎kore/test/Test/Kore/Step/MockSymbols.hs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -575,7 +575,7 @@ elementMapSymbol =
575575
concatMapSymbol :: Symbol
576576
concatMapSymbol =
577577
symbol concatMapId [mapSort, mapSort] mapSort
578-
& functional & hook "MAP.concat"
578+
& function & hook "MAP.concat"
579579

580580
opaqueMapSymbol :: Symbol
581581
opaqueMapSymbol =
@@ -620,7 +620,7 @@ unitListSymbol = symbol unitListId [] listSort & functional & hook "LIST.unit"
620620
concatSetSymbol :: Symbol
621621
concatSetSymbol =
622622
symbol concatSetId [setSort, setSort] setSort
623-
& functional & hook "SET.concat"
623+
& function & hook "SET.concat"
624624

625625
elementSetSymbol :: Symbol
626626
elementSetSymbol =

‎kore/test/Test/Kore/Step/Simplification/Equals.hs‎

Lines changed: 100 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -713,8 +713,30 @@ test_equalsSimplification_TermLike =
713713
(Mock.builtinMap [(Mock.b, mkElemVar Mock.x)])
714714
)
715715
, testCase "concrete Map with framed Map"
716-
(assertTermEquals
717-
Conditional
716+
(assertTermEqualsMulti
717+
[ Conditional
718+
{ term = ()
719+
, predicate =
720+
makeAndPredicate
721+
(makeNotPredicate
722+
(makeAndPredicate
723+
(makeCeilPredicate_ fOfA)
724+
(makeCeilPredicate_ fOfB)
725+
)
726+
)
727+
(makeNotPredicate
728+
(makeCeilPredicate_
729+
(Mock.concatMap
730+
(Mock.builtinMap
731+
[(Mock.a, mkElemVar Mock.x)]
732+
)
733+
(mkElemVar Mock.m)
734+
)
735+
)
736+
)
737+
, substitution = mempty
738+
}
739+
, Conditional
718740
{ term = ()
719741
, predicate =
720742
makeAndPredicate
@@ -726,15 +748,38 @@ test_equalsSimplification_TermLike =
726748
, (inject Mock.m, Mock.builtinMap [(Mock.b, fOfB)])
727749
]
728750
}
751+
]
729752
(Mock.builtinMap [(Mock.a, fOfA), (Mock.b, fOfB)])
730753
(Mock.concatMap
731754
(Mock.builtinMap [(Mock.a, mkElemVar Mock.x)])
732755
(mkElemVar Mock.m)
733756
)
734757
)
735758
, testCase "concrete Map with framed Map"
736-
(assertTermEquals
737-
Conditional
759+
(assertTermEqualsMulti
760+
[ Conditional
761+
{ term = ()
762+
, predicate =
763+
makeAndPredicate
764+
(makeNotPredicate
765+
(makeAndPredicate
766+
(makeCeilPredicate_ fOfA)
767+
(makeCeilPredicate_ fOfB)
768+
)
769+
)
770+
(makeNotPredicate
771+
(makeCeilPredicate_
772+
(Mock.concatMap
773+
(mkElemVar Mock.m)
774+
(Mock.builtinMap
775+
[(Mock.a, mkElemVar Mock.x)]
776+
)
777+
)
778+
)
779+
)
780+
, substitution = mempty
781+
}
782+
, Conditional
738783
{ term = ()
739784
, predicate =
740785
makeAndPredicate
@@ -746,15 +791,38 @@ test_equalsSimplification_TermLike =
746791
, (inject Mock.m, Mock.builtinMap [(Mock.b, fOfB)])
747792
]
748793
}
794+
]
749795
(Mock.builtinMap [(Mock.a, fOfA), (Mock.b, fOfB)])
750796
(Mock.concatMap
751797
(mkElemVar Mock.m)
752798
(Mock.builtinMap [(Mock.a, mkElemVar Mock.x)])
753799
)
754800
)
755801
, testCase "framed Map with concrete Map"
756-
(assertTermEquals
757-
Conditional
802+
(assertTermEqualsMulti
803+
[ Conditional
804+
{ term = ()
805+
, predicate =
806+
makeAndPredicate
807+
(makeNotPredicate
808+
(makeAndPredicate
809+
(makeCeilPredicate_ fOfA)
810+
(makeCeilPredicate_ fOfB)
811+
)
812+
)
813+
(makeNotPredicate
814+
(makeCeilPredicate_
815+
(Mock.concatMap
816+
(Mock.builtinMap
817+
[(Mock.a, mkElemVar Mock.x)]
818+
)
819+
(mkElemVar Mock.m)
820+
)
821+
)
822+
)
823+
, substitution = mempty
824+
}
825+
, Conditional
758826
{ term = ()
759827
, predicate =
760828
makeAndPredicate
@@ -766,15 +834,38 @@ test_equalsSimplification_TermLike =
766834
, (inject Mock.m, Mock.builtinMap [(Mock.b, fOfB)])
767835
]
768836
}
837+
]
769838
(Mock.concatMap
770839
(Mock.builtinMap [(Mock.a, mkElemVar Mock.x)])
771840
(mkElemVar Mock.m)
772841
)
773842
(Mock.builtinMap [(Mock.a, fOfA), (Mock.b, fOfB)])
774843
)
775844
, testCase "framed Map with concrete Map"
776-
(assertTermEquals
777-
Conditional
845+
(assertTermEqualsMulti
846+
[ Conditional
847+
{ term = ()
848+
, predicate =
849+
makeAndPredicate
850+
(makeNotPredicate
851+
(makeAndPredicate
852+
(makeCeilPredicate_ fOfA)
853+
(makeCeilPredicate_ fOfB)
854+
)
855+
)
856+
(makeNotPredicate
857+
(makeCeilPredicate_
858+
(Mock.concatMap
859+
(mkElemVar Mock.m)
860+
(Mock.builtinMap
861+
[(Mock.a, mkElemVar Mock.x)]
862+
)
863+
)
864+
)
865+
)
866+
, substitution = mempty
867+
}
868+
, Conditional
778869
{ term = ()
779870
, predicate =
780871
makeAndPredicate
@@ -786,6 +877,7 @@ test_equalsSimplification_TermLike =
786877
, (inject Mock.m, Mock.builtinMap [(Mock.b, fOfB)])
787878
]
788879
}
880+
]
789881
(Mock.concatMap
790882
(mkElemVar Mock.m)
791883
(Mock.builtinMap [(Mock.a, mkElemVar Mock.x)])

‎kore/test/Test/Kore/Unification/Unifier.hs‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -587,6 +587,34 @@ test_unification =
587587
)
588588
)
589589
[ UnificationResult
590+
{ term =
591+
constr20
592+
Mock.a
593+
(Mock.concatMap
594+
(Mock.builtinMap [(a, constr a)])
595+
(mkElemVar Mock.xMap)
596+
)
597+
, predicate =
598+
Predicate.makeAndPredicate
599+
(Predicate.makeNotPredicate
600+
(Predicate.makeCeilPredicate_
601+
(Mock.concatMap
602+
(Mock.builtinMap [(a, constr a)])
603+
(mkElemVar Mock.xMap)
604+
)
605+
)
606+
)
607+
( Predicate.makeNotPredicate
608+
( Predicate.makeCeilPredicate_
609+
(Mock.concatMap
610+
(Mock.builtinMap [(a, x)])
611+
(mkElemVar Mock.m)
612+
)
613+
)
614+
)
615+
, substitution = [ ("y", a) ]
616+
}
617+
, UnificationResult
590618
{ term =
591619
constr20
592620
Mock.a

0 commit comments

Comments
 (0)