++ Contributed by Stephen Wilson.

)abbrev domain CWMMT CompWithMappingModeTest

CompWithMappingModeTest() : Exports == Implementation where

  Exports == with
     runTests : () -> Boolean

  Implementation == add

     REC ==> Record(field1 : Integer, field2 : String)
     UN  ==> Union(rec : REC, str : String)

     -- The following function accepts a map as argument to test
     -- compWithMappingMode.
     mapper(fn : Integer -> Boolean, n: Integer) : Boolean == fn n

     -- We use the following as a target for currying and to pass to 
     -- mapper above.
     pred(x: Integer, y: Integer) : Boolean == 
       x < y => true
       true

     test1(x : Integer) : Boolean == 
        r : REC := [1, ""]
        mapper(pred(r.field1, #1), 1)

     test2(x : Integer) : Boolean == 
        r : REC := [1, ""]
        i : Integer := 1
        mapper(pred(r.field1 + x, #1), 1)

     test3(x : Integer) : Boolean == 
        r : REC := [1, ""]
        i : Integer := 1
        mapper(pred(r.field1 + i, #1), 1)

     test4(x : Integer) : Boolean ==
        r : REC := [1, ""]
        i : Integer := 1
        mapper(pred((r.field1 + min(#(r.field2), i)), #1), 1)

     test5(x : Integer) : Boolean ==
        r : REC := [1, ""]
        i : Integer := 1
        mapper(pred((r.field1 + min(#(r.field2), i + x)), #1), 1)

     test6(x : Integer) : Boolean ==
        u : UN := [[1, ""]$REC]
        mapper(pred(u.rec.field1, #1), 1)

     test7(x : Integer) : Boolean == 
        u : UN := [[1, ""]$REC]
        i : Integer := 1
        mapper(pred(u.rec.field1 + x, #1), 1)

     test8(x : Integer) : Boolean == 
        u : UN := [[1, ""]$REC]
        i : Integer := 1
        mapper(pred(u.rec.field1 + i, #1), 1)

     test9(x : Integer) : Boolean ==
        u : UN := [[1, ""]$REC]
        i : Integer := 1
        mapper(pred((u.rec.field1 + min(#(u.rec.field2), i)), #1), 1)

     test10(x : Integer) : Boolean ==
        u : UN := [[1, ""]$REC]
        i : Integer := 1
        mapper(pred((u.rec.field1 + min(#(u.rec.field2), i + x)), #1), 1)

     runTests() : Boolean ==
        test1(1) and test2(1) and test3(1) _
                 and test4(1) and test5(1) _
                 and test6(1) and test7(1) _
                 and test8(1) and test9(1) _
                 and test10(1)