Add containers-prop.cabal, use in CI

Author: HeinrichApfelmus

Makefile

@@ -1,4 +1,4 @@
-.PHONY : install agda repl libHtml test testHtml golden docs
+.PHONY : install agda repl libHtml test testContainers testHtml golden docs
 FILES = $(shell find src -type f)
 
 install :
@@ -17,7 +17,10 @@ libHtml :
 test/agda2hs : $(FILES)
 	cabal install agda2hs --overwrite-policy=always --installdir=test --install-method=copy
 
-test : test/agda2hs
+testContainers:
+	cd ./lib/containers && ./generate-haskell.sh && cabal build containers-prop
+
+test : test/agda2hs testContainers
 	make -C test
 
 testHtml : test/agda2hs

cabal.project

@@ -1,3 +1,5 @@
-packages: ./agda2hs.cabal
-constraints: Agda +debug
+packages:
+  ./agda2hs.cabal
+  ./lib/containers/containers-prop.cabal
 
+constraints: Agda +debug

lib/containers/CHANGELOG.md

@@ -0,0 +1,5 @@
+# Revision history for containers-prop
+
+## 0.8.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

lib/containers/agda/Test/Agda2Hs/Data/Map.agda

@@ -0,0 +1,35 @@
+module Test.Agda2Hs.Data.Map where
+
+open import Haskell.Prelude
+
+open import Data.Map using (Map)
+import Data.Map as Map
+
+{-----------------------------------------------------------------------------
+    Test definitions
+    for exercising Data.Map
+------------------------------------------------------------------------------}
+test0 : Map Nat String
+test0 = Map.fromList ((1 , "Hello") ∷ (2 , "Map") ∷ [])
+
+test1 : Map Nat String
+test1 = Map.filter (λ x → length x > 3) test0
+
+test2 : Map Nat String
+test2 = Map.singleton 1 "Data"
+
+test3 : Map Nat String
+test3 = Map.unionWith _<>_ test0 (Map.unionWith _<>_ test1 test2)
+
+test4 : Map Nat String
+test4 = Map.intersectionWith _<>_ test2 test3
+
+testLookup0 : Maybe String
+testLookup0 = Map.lookup 1 test4
+
+{-# COMPILE AGDA2HS test0 #-}
+{-# COMPILE AGDA2HS test1 #-}
+{-# COMPILE AGDA2HS test2 #-}
+{-# COMPILE AGDA2HS test3 #-}
+{-# COMPILE AGDA2HS test4 #-}
+{-# COMPILE AGDA2HS testLookup0 #-}

lib/containers/agda/Test/Agda2Hs/Data/Set.agda

@@ -0,0 +1,35 @@
+module Test.Agda2Hs.Data.Set where
+
+open import Haskell.Prelude
+
+open import Data.Set using (Set)
+import Data.Set as Set
+
+{-----------------------------------------------------------------------------
+    Test definitions
+    for exercising Data.Set
+------------------------------------------------------------------------------}
+test0 : Set String
+test0 = Set.fromList ("Hello" ∷ "Set" ∷ [])
+
+test1 : Set String
+test1 = Set.filter (λ x → length x > 3) test0
+
+test2 : Set String
+test2 = Set.singleton "Data"
+
+test3 : Set String
+test3 = Set.union test0 (Set.union test1 test2)
+
+test4 : Set String
+test4 = Set.intersection test2 test3
+
+testBool0 : Bool
+testBool0 = Set.isSubsetOf test2 test4
+
+{-# COMPILE AGDA2HS test0 #-}
+{-# COMPILE AGDA2HS test1 #-}
+{-# COMPILE AGDA2HS test2 #-}
+{-# COMPILE AGDA2HS test3 #-}
+{-# COMPILE AGDA2HS test4 #-}
+{-# COMPILE AGDA2HS testBool0 #-}

lib/containers/agda/containers.agda

@@ -2,3 +2,6 @@
 
 import Data.Map
 import Data.Set
+
+import Test.Agda2Hs.Data.Map
+import Test.Agda2Hs.Data.Set

lib/containers/agda2hs-libraries

@@ -0,0 +1 @@
+./../base/base.agda-lib

lib/containers/containers-prop.cabal

@@ -0,0 +1,52 @@
+cabal-version:      3.0
+name:               containers-prop
+build-type:         Simple
+version:            0.8
+synopsis:           Properties of containers, machine-checked
+description:
+  This package collects properties about data structures from the
+  [containers](https://hackage.haskell.org/package/containers) package,
+  such as `Data.Set` and `Data.Map`.
+  .
+  Basic properties are postulated, hoping that the implementation
+  satisfies them.
+  However, more complicated properties are proven from the basic properties.
+  These proofs are formalized and machine-checked
+  using [agda2hs](https://hackage.haskell.org/package/agda2hs).
+
+homepage:           https://github.com/agda/agda2hs
+license:            BSD-3-Clause
+author:             Heinrich Apfelmus
+maintainer:         [email protected]
+copyright:          2025 Cardano Foundation
+category:           Language
+extra-doc-files:    CHANGELOG.md
+extra-source-files:
+  agda/**/*.agda
+  containers.agda-lib
+  generate-haskell.sh
+
+common language
+  default-language: Haskell2010
+
+common opts-lib
+  ghc-options:
+    -Wall -Wcompat -Wincomplete-record-updates
+    -Wno-incomplete-uni-patterns -Wno-redundant-constraints
+    -Wno-unused-matches -Wno-unused-imports
+
+library
+  import:          language, opts-lib
+  hs-source-dirs:  haskell
+  build-depends:
+    , base        >=4.13 && <4.21
+    , containers  >=0.6  && <0.9
+
+  exposed-modules:
+
+  --    Data.Maps.Maybe
+  --    Data.Map.Prop
+  --    Data.Map.Set
+  autogen-modules:
+    Test.Agda2Hs.Data.Map
+    Test.Agda2Hs.Data.Set

lib/containers/generate-haskell.sh

@@ -0,0 +1,9 @@
+#!/bin/sh
+ROOT=containers.agda
+AGDA2HS="cabal run agda2hs --"
+${AGDA2HS} \
+    --local-interfaces \
+    --no-default-libraries \
+    --library-file ./agda2hs-libraries \
+    -o ./haskell/ \
+    ./agda/${ROOT}