Adding Constant Flow Distribution Agreement etc. (superfluid-finance#…

…1017) - Major refactoring re agreement category, now with rigorous agreement laws as properties usable in quickchecks. - Constant FlowAgreement tested against the agreement laws. - Constant Flow Distribution Agreement modeled and tested against the agreement laws. - Some simplification of type value system. - Reorganize type modules into CoreTypes and SystemTypes.
SoyElga · Aug 16, 2022 · 3c955c7 · 3c955c7
1 parent 8464790
commit 3c955c7
Show file tree

Hide file tree

Showing 62 changed files with 2,816 additions and 1,473 deletions.
diff --git a/.github/workflows/call.test-spec-haskell.yml b/.github/workflows/call.test-spec-haskell.yml
@@ -17,9 +17,9 @@ jobs:
     strategy:
       matrix:
         include:
-          - compiler: ghc-9.2.2
+          - compiler: ghc-9.2.4
             compilerKind: ghc
-            compilerVersion: 9.2.2
+            compilerVersion: 9.2.4
             setup-method: ghcup
             allow-failure: false
       fail-fast: false

diff --git a/packages/spec-haskell/.hlint.yaml b/packages/spec-haskell/.hlint.yaml
@@ -69,3 +69,4 @@
 #
 
 - ignore: {name: Use camelCase}
+- ignore: {name: Use newtype instead of data}
diff --git a/packages/spec-haskell/Makefile b/packages/spec-haskell/Makefile
@@ -9,9 +9,10 @@ TEST_BUILDDIR ?= dist-test
 TEST_COVERAGE_BUILDDIR ?= dist-coverage
 DOCS_BUILDDIR ?= dist-docs
 
-CABAL_TEST = $(CABAL) --builddir=$(TEST_BUILDDIR)
-CABAL_COVERAGE = $(CABAL) --builddir=$(TEST_COVERAGE_BUILDDIR) # --project-file=cabal.project.coverage
-CABAL_DOCS = $(CABAL) --builddir=$(DOCS_BUILDDIR)
+CABAL_TEST     = $(CABAL) --builddir=$(TEST_BUILDDIR)
+CABAL_COVERAGE = $(CABAL) --builddir=$(TEST_COVERAGE_BUILDDIR)
+CABAL_DOCS     = $(CABAL) --builddir=$(DOCS_BUILDDIR)
+
 TEST_OPTIONS = \
 	--test-show-details=$(TEST_SHOW_DETAILS_MODE) \
 	--test-options="--maximum-generated-tests=$(TEST_PROP_NUM_RUNS)"
@@ -21,56 +22,47 @@ default: build
 #
 # Build
 #
-prepare:
-	$(CABAL_TEST) v2-update
-
 build:
+	$(CABAL) v2-build all
+
+build-test:
 	$(CABAL_TEST) v2-build all
 
-clean-docs:
+clean:
 	rm -rf $(DOCS_BUILDDIR)
-
-clean-test:
 	rm -rf $(TEST_BUILDDIR)
-
-clean-coverage:
 	rm -rf $(TEST_COVERAGE_BUILDDIR)
+	rm -rf dist-*
 
-clean: clean-docs clean-test clean-coverage
-	rm -rf dist-newstyle
-
-.PHONY: default prepare build clean clean-*
+.PHONY: default build* clean
 
 #
 # Testing
 #
 test:
-	$(CABAL_TEST) \
-		v2-test --enable-tests \
-		$(TEST_OPTIONS) \
-		all
+	$(CABAL_TEST) v2-test all --enable-tests \
+		$(TEST_OPTIONS)
 
 test-coverage:
-	$(CABAL_COVERAGE) \
-		v2-test --enable-tests --enable-coverage \
-		$(TEST_OPTIONS) \
-		all
+	$(CABAL_COVERAGE) v2-build all --enable-tests --enable-coverage
+	$(CABAL_COVERAGE) v2-test all --enable-tests --enable-coverage \
+		$(TEST_OPTIONS)
+
+.PHONY: test test-*
 
 #
 # Demos
 #
-demo-expo: build
+demo-expo: build-test
 	$(CABAL_TEST) v2-exec superfluid-validator -- --demo expo
 
-demo-dfa: build
-	$(CABAL_TEST) v2-exec superfluid-validator -- --demo dfa > dfa.ignore.dat
-	gnuplot -p -e " \
-		plot 'dfa.ignore.dat' using 1:2 with lines title 'alice', \
-			 '' using 1:3 with lines title 'bob', \
-			 '' using 1:4 with lines title 'carol', \
-			 '' using 1:5 with lines title 'dan' \
-		"
-	rm -f dfa.ignore.dat
+demo-dfa: build-test
+	$(CABAL_TEST) v2-exec superfluid-validator -- --demo dfa | ./utils/self-gnuplot.sh
+
+demo-cfda: build-test
+	$(CABAL_TEST) v2-exec superfluid-validator -- --demo cfda | ./utils/self-gnuplot.sh
+
+.PHONY: demo-*
 
 #
 # Docs
@@ -83,9 +75,9 @@ YELLOWPAPER_ROOT = $(DOCS_BUILDDIR)/yellowpaper
 $(YELLOWPAPER_ROOT)/tex:
 	mkdir -p "$@"
 $(YELLOWPAPER_ROOT)/tex/MoneyDistributionConcepts.tex: packages/core/src/Money/Distribution/Concepts.lhs
-	./tasks/lhs2tex.sh "$<" > "$@"
+	./utils/lhs2tex.sh "$<" > "$@"
 $(YELLOWPAPER_ROOT)/tex/Communism.tex: packages/core/src/Money/Distribution/Communism.lhs
-	./tasks/lhs2tex.sh "$<" > "$@"
+	./utils/lhs2tex.sh "$<" > "$@"
 $(YELLOWPAPER_ROOT)/tex/lhsfmt.tex:
 	echo '%include lhs2TeX.fmt' | lhs2TeX > "$@"
 
@@ -120,26 +112,40 @@ docs: docs-haddock docs-yellowpaper
 # Dev Environment
 #
 dev:
-	nodemon -e lhs,hs,cabal -i "$(TEST_BUILDDIR)" -x "make $(DEV_TARGETS) || exit 1"
+	nodemon \
+		-e lhs,hs,cabal \
+		-i dist-newstyle/ -i "$(TEST_BUILDDIR)/" -i "$(TEST_COVERAGE_BUILDDIR)/" \
+		-x "make $(DEV_TARGETS) || exit 1"
+
+freeze:
+	rm -f cabal.project.freeze
+	$(CABAL) v2-freeze
+
+hlint:
+	hlint packages
 
 repl-simple:
-	$(CABAL_TEST) repl superfluid-protocol-system-simple
+	$(CABAL) repl superfluid-protocol-system-simple
 
 cloc:
 	@echo '**** Core Source Files ****'
-	cloc packages/core/src
+	cloc packages/core/src/
 	@echo
 
 	@echo '**** Simple System Source Files ****'
-	cloc packages/simple/src
+	cloc packages/simple/src/
 	@echo
 
 	@echo '**** Validator Source Files ****'
-	cloc packages/validator/src
+	cloc packages/validator/src/
+	@echo
+
+	@echo '**** Internal Source ****'
+	cloc packages/src-internal/
 	@echo
 
 	@echo '**** Test Files ****'
 	cloc packages/*/test
 	@echo
 
-.PHONY: demo-* test test-* dev repl-* cloc
+.PHONY: dev freeze hlint repl-* cloc
diff --git a/packages/spec-haskell/cabal.project.coverage b/packages/spec-haskell/cabal.project.coverage
diff --git a/packages/spec-haskell/cabal.project.freeze b/packages/spec-haskell/cabal.project.freeze
@@ -5,9 +5,9 @@ constraints: any.HUnit ==1.6.2.0,
              any.ansi-terminal ==0.11.3,
              ansi-terminal -example,
              any.array ==0.5.4.0,
-             any.base ==4.16.1.0,
+             any.base ==4.16.3.0,
              any.binary ==0.8.9.0,
-             any.bytestring ==0.11.3.0,
+             any.bytestring ==0.11.3.1,
              any.call-stack ==0.4.0,
              any.clock ==0.8.3,
              clock -llvm,
@@ -24,17 +24,17 @@ constraints: any.HUnit ==1.6.2.0,
              dlist -werror,
              any.exceptions ==0.10.4,
              any.filepath ==1.4.2.2,
-             any.ghc ==9.2.2,
+             any.ghc ==9.2.4,
              any.ghc-bignum ==1.2,
-             any.ghc-boot ==9.2.2,
-             any.ghc-boot-th ==9.2.2,
-             any.ghc-heap ==9.2.2,
+             any.ghc-boot ==9.2.4,
+             any.ghc-boot-th ==9.2.4,
+             any.ghc-heap ==9.2.4,
              any.ghc-prim ==0.8.0,
-             any.ghci ==9.2.2,
+             any.ghci ==9.2.4,
              any.hpc ==0.6.1.0,
-             any.hspec ==2.10.0,
-             any.hspec-core ==2.10.0,
-             any.hspec-discover ==2.10.0,
+             any.hspec ==2.10.0.1,
+             any.hspec-core ==2.10.0.1,
+             any.hspec-discover ==2.10.0.1,
              any.hspec-expectations ==0.8.2,
              any.math-extras ==0.1.1.0,
              any.microlens ==0.4.13.0,
@@ -56,4 +56,4 @@ constraints: any.HUnit ==1.6.2.0,
              any.time ==1.11.1.1,
              any.transformers ==0.5.6.2,
              any.unix ==2.7.2.2
-index-state: hackage.haskell.org 2022-07-24T13:36:30Z
+index-state: hackage.haskell.org 2022-08-12T21:03:11Z
diff --git a/packages/spec-haskell/hie.yaml b/packages/spec-haskell/hie.yaml
@@ -20,11 +20,19 @@ cradle:
       config:
         cradle:
           cabal:
+            - path: "./packages/core/src-internal"
+              component: "lib:superfluid-protocol-spec-core"
             - path: "./packages/core/src"
               component: "lib:superfluid-protocol-spec-core"
+            - path: "./packages/core/test"
+              component: "superfluid-protocol-spec-core:test:tests"
+
+            - path: "packages/simple/src-internal"
+              component: "lib:superfluid-protocol-system-simple"
             - path: "packages/simple/src"
               component: "lib:superfluid-protocol-system-simple"
             - path: "packages/simple/test"
               component: "superfluid-protocol-system-simple:test:tests"
+
             - path: "packages/validator/src"
               component: "superfluid-protocol-spec-validator:exe:superfluid-validator"
diff --git a/...askell/packages/core/src/Lens/Internal.hs → ...ckages/core/src-internal/Lens/Internal.hs b/...askell/packages/core/src/Lens/Internal.hs → ...ckages/core/src-internal/Lens/Internal.hs
@@ -2,12 +2,14 @@
 
 module Lens.Internal
     ( module Lens.Micro
+    , module Lens.Micro.Extras
     , readOnlyLens
     , field
     ) where
 
 import           Language.Haskell.TH
 import           Lens.Micro
+import           Lens.Micro.Extras
 
 -- | A short hand for creating a read only lens
 readOnlyLens :: (s -> a) -> Lens s t a b

diff --git a/packages/spec-haskell/packages/core/src/Data/Type/Any.hs b/packages/spec-haskell/packages/core/src/Data/Type/Any.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE FunctionalDependencies  #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module Data.Type.Any where
+
+import           Data.Kind  (Constraint, Type)
+import           Data.Proxy (Proxy)
+
+
+-- | ~AnyType~ ~a~ can hold wrap any instances of ~c~ constraint.
+--
+-- Note:
+--    - It can be implemented with some flavor of existential type: https://wiki.haskell.org/Existential_type.
+--
+class IsAnyTypeOf (a :: Type) (c :: Type -> Constraint) | a -> c where
+    -- | Make a ~AnyType~ from a term that is of type that has ~c~ constraint.
+    mkAny :: c e => Proxy a -> e -> a
+
+-- | Flip MPTC type params.
+class c a b => MPTC_Flip c b a
+instance c a b => MPTC_Flip c b a
Original file line number	Diff line number	Diff line change
Expand Up		@@ -69,3 +69,4 @@
		#

		- ignore: {name: Use camelCase}
		- ignore: {name: Use newtype instead of data}