|
| 1 | +from Standard.Base import all |
| 2 | +from Standard.Test import all |
| 3 | +import Standard.Base.Errors.Common.Type_Error |
| 4 | +import Standard.Base.Errors.Common.No_Such_Conversion |
| 5 | +import Standard.Base.Errors.Common.No_Such_Method |
| 6 | + |
| 7 | +from project.Semantic.Type_Refinement.Types import A, B, make_a_and_b |
| 8 | + |
| 9 | +id_a (x : A) -> A = x |
| 10 | +id_b (x : B) -> B = x |
| 11 | + |
| 12 | +add_specs suite_builder = |
| 13 | + suite_builder.group "Multi Value as type refinement" group_builder-> |
| 14 | + group_builder.specify "conversion A -> B should not be available" <| |
| 15 | + just_a = A.A_Ctor 1 |
| 16 | + Test.expect_panic Type_Error (just_a:B) |
| 17 | + Test.expect_panic No_Such_Conversion (B.from just_a) |
| 18 | + Test.expect_panic Type_Error (id_b just_a) |
| 19 | + |
| 20 | + group_builder.specify "make_a_and_b->A&B presents as both A and B" <| |
| 21 | + ab = make_a_and_b |
| 22 | + ab.is_a A . should_be_true |
| 23 | + ab.is_a B . should_be_true |
| 24 | + (ab:A).to_text . should_equal "(A_Ctor 1)" |
| 25 | + (ab:B).to_text . should_equal "(B_Ctor (A_Ctor 1))" |
| 26 | + (id_a ab).to_text . should_equal "(A_Ctor 1)" |
| 27 | + (id_b ab).to_text . should_equal "(B_Ctor (A_Ctor 1))" |
| 28 | + |
| 29 | + group_builder.specify "after passing A&B value to a function expecting A argument, B becomes hidden" <| |
| 30 | + ab = make_a_and_b |
| 31 | + a2 = id_a ab |
| 32 | + a2.is_a A . should_be_true |
| 33 | + a2.is_a B . should_be_false |
| 34 | + |
| 35 | + # Passing a2 to a function expecting B fails because B part was hidden |
| 36 | + Test.expect_panic Type_Error (id_b a2) |
| 37 | + |
| 38 | + # But it can be uncovered via explicit cast |
| 39 | + (a2:B).to_text . should_equal "(B_Ctor (A_Ctor 1))" |
| 40 | + (id_b (a2:B)).to_text . should_equal "(B_Ctor (A_Ctor 1))" |
| 41 | + |
| 42 | +main filter=Nothing = |
| 43 | + suite = Test.build suite_builder-> |
| 44 | + add_specs suite_builder |
| 45 | + suite.run_with_filter filter |
0 commit comments