Adding tests for map functionality

Author: viktorcsimma

test/AllTests.agda

@@ -69,6 +69,7 @@ import EraseType
 import Issue257
 import HaskellDataOpenImport
 import HaskellDataQualifiedImport
+import Map
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -137,4 +138,5 @@ import Inlining
 import EraseType
 import HaskellDataOpenImport
 import HaskellDataQualifiedImport
+import Map
 #-}

test/Map.agda

@@ -0,0 +1,45 @@
+-- A test pack for Data.Map.
+module Map where
+
+open import Agda.Builtin.Equality
+open import Agda.Builtin.Nat
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Ord
+import Haskell.Data.Map as Map
+open Map using (Map)
+
+firstMap : Map Nat Nat
+firstMap = Map.insert 50 5 (Map.insert 40 4 (Map.insert 100 10 Map.empty))
+{-# COMPILE AGDA2HS firstMap #-}
+
+val1 : Maybe Nat
+val1 = Map.lookup 100 firstMap
+{-# COMPILE AGDA2HS val1 #-}
+
+@0 test1 : val1 ≡ Just 10
+test1 = refl
+
+val2 : Maybe Nat
+val2 = Map.lookup 15 firstMap
+{-# COMPILE AGDA2HS val2 #-}
+
+@0 test2 : val2 ≡ Nothing
+test2 = refl
+
+secondMap : Map Nat Nat
+secondMap = Map.delete 50 firstMap
+{-# COMPILE AGDA2HS secondMap #-}
+
+val3 : Maybe Nat
+val3 = Map.lookup 50 secondMap
+{-# COMPILE AGDA2HS val3 #-}
+
+@0 test3 : val3 ≡ Nothing
+test3 = refl
+
+val4 : Maybe Nat
+val4 = Map.lookup 100 secondMap
+{-# COMPILE AGDA2HS val4 #-}
+
+@0 test4 : val4 ≡ Just 10
+test4 = refl

test/golden/AllTests.hs

@@ -66,4 +66,5 @@ import Inlining
 import EraseType
 import HaskellDataOpenImport
 import HaskellDataQualifiedImport
+import Map
 

test/golden/Map.hs

@@ -0,0 +1,25 @@
+module Map where
+
+import Data.Map (Map)
+import qualified Data.Map as Map (delete, empty, insert, lookup)
+import Numeric.Natural (Natural)
+
+firstMap :: Map Natural Natural
+firstMap
+  = Map.insert 50 5 (Map.insert 40 4 (Map.insert 100 10 Map.empty))
+
+val1 :: Maybe Natural
+val1 = Map.lookup 100 firstMap
+
+val2 :: Maybe Natural
+val2 = Map.lookup 15 firstMap
+
+secondMap :: Map Natural Natural
+secondMap = Map.delete 50 firstMap
+
+val3 :: Maybe Natural
+val3 = Map.lookup 50 secondMap
+
+val4 :: Maybe Natural
+val4 = Map.lookup 100 secondMap
+