package Ġit . uni bo . tup ro log . core Ċ Ċ import Ġit . uni bo . tup ro log . core . test utils . Assertion Utils . drop First Ċ import Ġit . uni bo . tup ro log . core . test utils . Assertion Utils . on Corre sponding Items Ċ import Ġit . uni bo . tup ro log . core . test utils . Substitution Utils Ċ import Ġit . uni bo . tup ro log . core . test utils . Var Utils . assert Different Variable Except For Name Ċ import Ġkotlin . test . Test Ċ import Ġkotlin . test . assertEquals Ċ import Ġkotlin . test . assertFalse Ċ import Ġkotlin . test . assertSame Ċ import Ġkotlin . test . assertTrue Ċ Ċ /** Ċ Ġ* ĠTest Ġclass Ġfor Ġ[ Substitution ] Ġcompanion Ġobject Ċ Ġ* Ċ Ġ* Ġ@ author ĠEn ric o Ċ Ġ*/ Ċ internal Ġclass ĠSubst itution Test Ġ{ ĊĊĠĠĠ Ġprivate Ġval Ġa Var Ġ= ĠVar . of (" A ") ĊĠĠĠ Ġprivate Ġval Ġb Var Ġ= ĠVar . of (" B ") ĊĊĠĠĠ Ġprivate Ġval Ġcorrect Instances Ġby Ġlazy Ġ{ ĠSubst itution Utils . mixed Substitution s . map ( Substitution . Companion :: of ) Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġfailed Should Return The Failed Substitution Instance () Ġ{ ĊĠĠĠĠĠĠĠ ĠassertEquals ( Substitution . failed (), ĠSubst itution . failed ()) ĊĠĠĠĠĠĠĠ ĠassertSame ( Substitution . failed (), ĠSubst itution . failed ()) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġfailed Substitution Is Failed () Ġ{ ĊĠĠĠĠĠĠĠ ĠassertTrue ( Substitution . failed (). is Failed ) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġfailed Substitution IsNot Success () Ġ{ ĊĠĠĠĠĠĠĠ ĠassertFalse ( Substitution . failed (). is Success ) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġempty Returns An Empty Substitution () Ġ{ ĊĠĠĠĠĠĠĠ ĠassertTrue ( Substitution . empty (). isEmpty ()) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġempty Substitution Is Success () Ġ{ ĊĠĠĠĠĠĠĠ ĠassertTrue ( Substitution . empty (). is Success ) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġempty Substitution IsNot Failed () Ġ{ ĊĠĠĠĠĠĠĠ ĠassertFalse ( Substitution . empty (). is Failed ) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġas Un ifier Con verts A Map Var Term To Substitution () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution Utils . mixed Substitution s . map Ġ{ Ġit . as Un ifier () Ġ} ĊĊĠĠĠĠĠĠĠ Ġon Corre sponding Items ( correct Instances , Ġto Be Tested ) Ġ{ Ġexpected , Ġactual Ġ-> ĠassertEquals ( expected , Ġactual ) Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġas Un ifier Results In Empty Substitution If Identity Mappings () Ġ{ ĊĠĠĠĠĠĠĠ ĠassertEquals ( Substitution . empty (), Ġmap Of ( a Var Ġto Ġa Var ). as Un ifier ()) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġas Un ifier Results In Empty Substitution If Indirect Identity Mappings () Ġ{ ĊĠĠĠĠĠĠĠ ĠassertEquals ( Substitution . empty (), Ġmap Of ( a Var Ġto Ġb Var , Ġb Var Ġto Ġa Var ). as Un ifier ()) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Variable And Term () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġcorrect Ġ= Ġcorrect Instances . filter Ġ{ Ġit . size Ġ== Ġ 1 Ġ} ĊĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution Utils . mixed Substitution s As Pairs . filter Ġ{ Ġit . size Ġ== Ġ 1 Ġ}. map Ġ{ Ġit . first () Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ. map Ġ{ Ġ( variable , Ġwith Term ) Ġ-> ĠSubst itution . of ( variable , Ġwith Term ) Ġ} ĊĊĠĠĠĠĠĠĠ Ġon Corre sponding Items ( correct , Ġto Be Tested ) Ġ{ Ġexpected , Ġactual Ġ-> ĠassertEquals ( expected , Ġactual ) Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof String Variable And Term () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġcorrect Ġ= Ġcorrect Instances . filter Ġ{ Ġit . size Ġ== Ġ 1 Ġ} ĊĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution Utils . mixed Substitution s As Pairs . filter Ġ{ Ġit . size Ġ== Ġ 1 Ġ}. map Ġ{ Ġit . first () Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ. map Ġ{ Ġ( variable , Ġwith Term ) Ġ-> ĠSubst itution . of ( variable . name , Ġwith Term ) Ġ} ĊĊĠĠĠĠĠĠĠ Ġon Corre sponding Items ( correct , Ġto Be Tested ) Ġ{ Ġexpected Map , Ġactual Map Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠ Ġon Corre sponding Items ( expected Map . keys , Ġactual Map . keys , Ġ:: assert Different Variable Except For Name ) ĊĠĠĠĠĠĠĠĠĠĠĠ ĠassertEquals ( expected Map . values . toList (), Ġactual Map . values . toList ()) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Variable Term Pairs () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution Utils . mixed Substitution s As Pairs . map Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . of ( it . first (), Ġ* it . drop First (). to Typed Array ()) ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġon Corre sponding Items ( correct Instances , Ġto Be Tested ) Ġ{ Ġexpected , Ġactual Ġ-> ĠassertEquals ( expected , Ġactual ) Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Variable Term Pairs Does nt Comp lain If Exact Duplicates () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution Utils . d uplicated Pair Substitution . map Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . of ( it . first (), Ġ* it . drop First (). to Typed Array ()) ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġval Ġcorrect Instances Ġ= ĠSubst itution Utils . d uplicated Pair Substitution . map Ġ{ ĠSubst itution . of ( it . toMap ()) Ġ} ĊĊĠĠĠĠĠĠĠ Ġon Corre sponding Items ( correct Instances , Ġto Be Tested ) Ġ{ Ġexpected , Ġactual Ġ-> ĠassertEquals ( expected , Ġactual ) Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Variable Term Pairs Result In Failed Substitution If Contr ad ict ing () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution Utils . contr ad ict ing Substitution s . map Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . of ( it . first (), Ġ* it . drop First (). to Typed Array ()) ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġto Be Tested . forEach Ġ{ ĠassertEquals ( Substitution . failed (), Ġit ) Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Iterable Variable Term Pairs () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution Utils . mixed Substitution s As Pairs . map Ġ{ ĠSubst itution . of ( it ) Ġ} ĊĊĠĠĠĠĠĠĠ Ġon Corre sponding Items ( correct Instances , Ġto Be Tested ) Ġ{ Ġexpected , Ġactual Ġ-> ĠassertEquals ( expected , Ġactual ) Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Iterable Variable Term Pairs Does nt Comp lain If Exact Duplicates () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution Utils . d uplicated Pair Substitution . map Ġ{ ĠSubst itution . of ( it ) Ġ} ĊĊĠĠĠĠĠĠĠ Ġval Ġcorrect Instances Ġ= ĠSubst itution Utils . d uplicated Pair Substitution . map Ġ{ ĠSubst itution . un ifier ( it . toMap ()) Ġ} ĊĊĠĠĠĠĠĠĠ Ġon Corre sponding Items ( correct Instances , Ġto Be Tested ) Ġ{ Ġexpected , Ġactual Ġ-> ĠassertEquals ( expected , Ġactual ) Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Iterable Variable Term Pairs Result In Failed Substitution If Contr ad ict ing () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution Utils . contr ad ict ing Substitution s . map Ġ{ ĠSubst itution . of ( it ) Ġ} ĊĊĠĠĠĠĠĠĠ Ġto Be Tested . forEach Ġ{ ĠassertEquals ( Substitution . failed (), Ġit ) Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Empty Iterable () Ġ{ ĊĠĠĠĠĠĠĠ ĠassertEquals ( Substitution . empty (), ĠSubst itution . of ( emptyList ())) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Substitution s () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġcorrect Ġ= ĠSubst itution . un ifier ( Substitution Utils . mixed Substitution s . reduce Ġ{ Ġmap 1 , Ġmap 2 Ġ-> Ġmap 1 Ġ+ Ġmap 2 Ġ}) ĊĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution . of ( correct Instances . first (), Ġ* correct Instances . drop First (). to Typed Array ()) ĊĊĠĠĠĠĠĠĠ ĠassertEquals ( correct , Ġto Be Tested ) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Substitution sWith Always Same Substitution s Returns The m Not D uplicated () Ġ{ ĊĠĠĠĠĠĠĠ ĠScope . of (" A ", Ġ" B ") Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġcorrect Ġ= ĠSubst itution . un ifier ( ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġmap Of ( ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġvar Of (" A ") Ġto Ġatom Of (" a "), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġvar Of (" B ") Ġto Ġatom Of (" b ") ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ) ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution . of ( ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . un ifier ( map Of ( var Of (" B ") Ġto Ġatom Of (" b ")) ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . un ifier ( map Of ( var Of (" A ") Ġto Ġatom Of (" a ")) ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . un ifier ( map Of ( var Of (" B ") Ġto Ġatom Of (" b ")) ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . un ifier ( map Of ( var Of (" A ") Ġto Ġatom Of (" a ")) ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . un ifier ( map Of ( var Of (" B ") Ġto Ġatom Of (" b "))) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ) ĊĊĠĠĠĠĠĠĠĠĠĠĠ ĠassertEquals ( correct , Ġto Be Tested ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Substitution sWith Contr ad ict ing On es Returns Failed () Ġ{ ĊĠĠĠĠĠĠĠ ĠScope . of (" A ", Ġ" B ") Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= ĠSubst itution . of ( ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . un ifier ( map Of ( var Of (" B ") Ġto Ġatom Of (" f ")) ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . un ifier ( map Of ( var Of (" B ") Ġto Ġvar Of (" A ")) ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . un ifier ( map Of ( var Of (" A ") Ġto Ġatom Of (" b ")) ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . un ifier ( map Of ( var Of (" A ") Ġto Ġatom Of (" a ")) ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . un ifier ( map Of ( var Of (" B ") Ġto Ġatom Of (" b "))) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ) ĊĊĠĠĠĠĠĠĠĠĠĠĠ ĠassertEquals ( Substitution . failed (), Ġto Be Tested ) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Substitution s Comp lies With Composition Defined In Pro log Standard () Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġx Atom Ġ= ĠAtom . of (" x ") ĊĊĠĠĠĠĠĠĠ Ġval Ġfirst Ġ= ĠSubst itution . un ifier ( map Of ( b Var Ġto ĠStruct . of (" f ", Ġa Var ))) ĊĠĠĠĠĠĠĠ Ġval Ġsecond Ġ= ĠSubst itution . un ifier ( map Of ( a Var Ġto Ġx Atom )) ĊĊĠĠĠĠĠĠĠ Ġval Ġfirst Comp osed Second Expected Ġ= ĠSubst itution . un ifier ( ĊĠĠĠĠĠĠĠĠĠĠĠ Ġmap Of ( ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġb Var Ġto ĠStruct . of (" f ", Ġx Atom ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġa Var Ġto Ġx Atom ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ) ĊĠĠĠĠĠĠĠ Ġ) ĊĊĠĠĠĠĠĠĠ Ġval Ġsecond Comp osed First Expected Ġ= ĠSubst itution . un ifier ( ĊĠĠĠĠĠĠĠĠĠĠĠ Ġmap Of ( ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġa Var Ġto Ġx Atom , ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġb Var Ġto ĠStruct . of (" f ", Ġa Var ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ) ĊĠĠĠĠĠĠĠ Ġ) ĊĊĠĠĠĠĠĠĠ ĠassertEquals ( first Comp osed Second Expected , ĠSubst itution . of ( first , Ġsecond )) ĊĠĠĠĠĠĠĠ ĠassertEquals ( second Comp osed First Expected , ĠSubst itution . of ( second , Ġfirst )) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġ@ Test ĊĠĠĠ Ġfun Ġof Implement ations Return Empty Substitution If Identity Passed In () Ġ{ ĊĠĠĠĠĠĠĠ ĠScope . empty Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġidentity Pair A Ġ= Ġvar Of (" A ") Ġto Ġvar Of (" A ") ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġidentity Pair B Ġ= Ġvar Of (" B ") Ġto Ġvar Of (" B ") ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġto Be Tested Ġ= Ġkt ListOf ( ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . of ( identity Pair A . first , Ġidentity Pair A . second ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . of ( identity Pair A , Ġidentity Pair B ), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . of ( kt ListOf ( identity Pair A , Ġidentity Pair B )), ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ ĠSubst itution . of ( Substitution . of ( identity Pair A ), ĠSubst itution . of ( identity Pair B )) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ) ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġto Be Tested . forEach Ġ{ ĠassertEquals ( Substitution . empty (), Ġit ) Ġ} ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} Ċ } Ċ