Rework Idris implementation (WIP)

.dir-locals.el

@@ -4,5 +4,12 @@
 ((gap-mode
   (gap-executable . "gap"))
  (idris-mode
-  (idris-interpreter-flags "-p" "contrib")
+  (eval
+   let ((project-dir
+         (concat (getenv "HOME") "/src/github.com/yurrriq/gis")))
+   (setq idris-interpreter-flags
+         (list "-i" (concat project-dir "/src")
+               "-i" (concat project-dir "/test")
+               "-p" "contrib"
+               "-p" "specdris")))
   (idris-interpreter-path . "idris")))

LICENSE

@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright © 2020 Eric Bailey <eric@ericb.me>
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the “Software”), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.

elba.lock

@@ -1,4 +1,4 @@
 [[packages]]
-id = 'yurrriq/gis@dir+/home/e.bailey/src/github.com/yurrriq/gis'
-version = '0.0.1'
+id = 'yurrriq/gis@dir+/home/yurrriq/src/github.com/yurrriq/gis'
+version = '0.1.0'
 dependencies = []

elba.toml

@@ -1,15 +1,26 @@
 [package]
 name = "yurrriq/gis"
-version = "0.0.1"
+version = "0.1.0"
 authors = ["Eric Bailey <eric@ericb.me>"]
 repository = "https://github.com/yurrriq/gis"
+# TODO: readme = "README.md"
 license = "MIT"
 
-[dependencies]
+# [dev_dependencies]
+# [dev_dependencies."pheymann/specdris"]
+# git = "https://github.com/pheymann/specdris"
+# tag = "v0.3.1"
 
 [targets.lib]
 path = "src/"
 mods = [
   "Data.GIS",
+  "Data.Int.Algebra",
+  "Data.Music",
 ]
 idris_opts = ["-p", "contrib"]
+
+[[targets.test]]
+path = "test/"
+main = "Data.GIS.Test.runTests"
+idris_opts = ["-p", "specdris"]

shell.nix

@@ -8,7 +8,10 @@ pkgs.mkShell {
       gap-full
       git
       gnumake
-      (with idrisPackages; with-packages [ contrib ])
+      (with idrisPackages; with-packages [
+        contrib
+        specdris
+      ])
       nixpkgs-fmt
       niv
       rlwrap

src/Data/GIS.idr

@@ -1,99 +1,34 @@
 module Data.GIS
 
 import Control.Algebra
+import Control.Algebra.NumericImplementations
+import Data.Int.Algebra
+import Data.Music
 
-Semigroup Integer where
-  x <+> y = x + y
+%access public export
+%default partial
 
-Monoid Integer where
-  neutral = 0
+interface Group ivls => HasLabel s ivls where
+  LABEL : s -> ivls
 
-Group Integer where
-  inverse = negate
+interface HasLabel space ivls => GIS space ivls where
+  int : space -> space -> ivls
+  int s t = LABEL t <-> LABEL s
+  conditionA : int r s <+> int s t = int r t
+  conditionB : int s t = int s' t' -> (s = s', t = t')
 
-record AdditiveZ where
-  constructor GetAdditiveZ
-  _ : Integer
+%access export
 
-Eq AdditiveZ where
-  (GetAdditiveZ x) == (GetAdditiveZ y) = x == y
+[PSpaceLABEL] HasLabel Pitch Int using PlusZnGroup where
+  LABEL (pitchClass, octave) = cast pitchClass + 12 * octave
 
-Num AdditiveZ where
-  fromInteger = GetAdditiveZ
-  (GetAdditiveZ x) + (GetAdditiveZ y) = GetAdditiveZ (x + y)
-  (GetAdditiveZ x) * (GetAdditiveZ y) = GetAdditiveZ (x * y)
+[PpaceGIS] GIS Pitch Int using PSpaceLABEL where
+  conditionA = believe_me "int r s + int s t = int r t"
+  conditionB = believe_me "int s t = int s' t' -> (s = s', t = t')"
 
-Neg AdditiveZ where
-  negate (GetAdditiveZ x) = GetAdditiveZ (negate x)
-  (GetAdditiveZ x) - (GetAdditiveZ y) = GetAdditiveZ (x - y)
+[PCSpaceLABEL] HasLabel PitchClass (Zn 12) using PlusZnGroup where
+  LABEL = MkZn . cast
 
-Semigroup AdditiveZ where
-  (GetAdditiveZ x) <+> (GetAdditiveZ y) = GetAdditiveZ $ x + y
-
-Monoid AdditiveZ where
-  neutral = GetAdditiveZ 0
-
-Group AdditiveZ where
-  inverse (GetAdditiveZ x) = GetAdditiveZ (negate x)
-
-data Zn : (n : Nat) -> Type where
-  MkZn : Integer -> Zn n
-
-Eq (Zn n) where
-  (MkZn x) == (MkZn y) = x == y
-
-Num (Zn n) where
-  fromInteger x = MkZn $ x `mod` toIntegerNat n
-  (MkZn x) + (MkZn y) = MkZn $ (x + y) `mod` toIntegerNat n
-  (MkZn x) * (MkZn y) = MkZn $ (x * y) `mod` toIntegerNat n
-
-Neg (Zn n) where
-  negate (MkZn x) = MkZn $ negate x `mod` toIntegerNat n
-  (MkZn x) - (MkZn y) = MkZn $ (x - y) `mod` toIntegerNat n
-
-data AdditiveZn : (n : Nat) -> Type where
-  GetAdditiveZn : Zn n -> AdditiveZn n
-
-Eq (AdditiveZn n) where
-  (GetAdditiveZn x) == (GetAdditiveZn y) = x == y
-
-Num (AdditiveZn n) where
-  fromInteger = GetAdditiveZn . MkZn
-  (GetAdditiveZn x) + (GetAdditiveZn y) = GetAdditiveZn (x + y)
-  (GetAdditiveZn x) * (GetAdditiveZn y) = GetAdditiveZn (x * y)
-
-Neg (AdditiveZn n) where
-  negate (GetAdditiveZn x) = GetAdditiveZn (negate x)
-  (GetAdditiveZn x) - (GetAdditiveZn y) = GetAdditiveZn (x - y)
-
-Semigroup (AdditiveZn n) where
-  (GetAdditiveZn (MkZn x)) <+> (GetAdditiveZn (MkZn y)) = GetAdditiveZn (MkZn (x + y))
-
-Monoid (AdditiveZn n) where
-  neutral = GetAdditiveZn (MkZn 0)
-
-Group (AdditiveZn n) where
-  inverse (GetAdditiveZn (MkZn x)) = GetAdditiveZn (MkZn (negate x))
-
-data GIS : (lift : s -> ivls) -> Type where
-  MkGIS :
-    Group ivls =>
-    (s : Type) ->
-    (lift : s -> ivls) ->
-    (int : s -> s -> ivls) ->
-    GIS lift
-
-mkGIS : Group ivls => (lift : s -> ivls) -> GIS lift
-mkGIS {lift} {s} {ivls} = MkGIS s lift int
-  where
-    int : s -> s -> ivls
-    int x y = lift y <+> inverse (lift x)
-
-int : GIS lift {s} {ivls} -> (s -> s -> ivls)
-int (MkGIS _ _ int) = int
-
-PSpace : GIS GetAdditiveZ
-PSpace = mkGIS GetAdditiveZ
-
-PCSpace : GIS (GetAdditiveZn {n=12})
-PCSpace = mkGIS (GetAdditiveZn {n=12})
+[PCSpaceGIS] GIS PitchClass (Zn 12) using PCSpaceLABEL where
+  conditionA = believe_me "int r s + int s t = int r t"
+  conditionB = believe_me "int s t = int s' t' -> (s = s', t = t')"

src/Data/Int/Algebra.idr

@@ -0,0 +1,66 @@
+module Data.Int.Algebra
+
+import Control.Algebra
+import Interfaces.Verified
+
+%access public export
+%default total
+
+[PlusIntSemi] Semigroup Int where
+  x <+> y = x + y
+
+[PlusIntSemiV] VerifiedSemigroup Int using PlusIntSemi where
+  semigroupOpIsAssociative = believe_me "Int addition is associative"
+
+[PlusIntMonoid] Monoid Int using PlusIntSemi where
+  neutral = 0
+
+[PlusIntMonoidV] VerifiedMonoid Int using PlusIntSemiV, PlusIntMonoid where
+  monoidNeutralIsNeutralL = believe_me "x + 0 = x"
+  monoidNeutralIsNeutralR = believe_me "0 + x = x"
+
+[PlusIntGroup] Group Int using PlusIntMonoid where
+  inverse = negate
+
+[PlusIntGroupV] VerifiedGroup Int using PlusIntMonoidV, PlusIntGroup where
+  groupInverseIsInverseR = believe_me "x - x = 0"
+
+data Zn : (n : Nat) -> Type where
+  MkZn : Int -> Zn n
+
+Eq (Zn n) where
+  (MkZn x) == (MkZn y) = x == y
+
+implementation DecEq (Zn n) where
+  decEq x y =
+      case x == y of
+      True => Yes primitiveEq
+      False => No primitiveNotEq
+    where
+      primitiveEq : x = y
+      primitiveEq = really_believe_me (Refl {x})
+      primitiveNotEq : x = y -> Void
+      primitiveNotEq prf = believe_me {b = Void} ()
+
+%default partial
+
+Show (Zn n) where
+  show (MkZn x) = show (x `mod` 12)
+
+Num (Zn n) where
+  fromInteger x = MkZn $ fromInteger x `mod` fromNat n
+  (MkZn x) + (MkZn y) = MkZn $ (fromNat n + x + y) `mod` fromNat n
+  (MkZn x) * (MkZn y) = MkZn $ ((fromNat n + x) * (fromNat n + y)) `mod` fromNat n
+
+Neg (Zn n) where
+  negate (MkZn x) = MkZn $ fromNat n + negate x `mod` fromNat n
+  (MkZn x) - (MkZn y) = MkZn $ (fromNat n + x - y) `mod` fromNat n
+
+[PlusZnSemi] Semigroup (Zn n) where
+  x <+> y = x + y
+
+[PlusZnMonoid] Monoid (Zn n) using PlusZnSemi where
+  neutral = MkZn 0
+
+[PlusZnGroup] Group (Zn n) using PlusZnMonoid where
+  inverse = negate

src/Data/Music.idr

@@ -0,0 +1,118 @@
+module Data.Music
+
+import Data.Combinators
+
+%access public export
+%default total
+
+data PitchClass
+  = C
+  | Cis
+  | D
+  | Dis
+  | E
+  | F
+  | Fis
+  | G
+  | Gis
+  | A
+  | Ais
+  | B
+
+Enum PitchClass where
+  pred D   = Cis
+  pred Dis = D
+  pred E   = Dis
+  pred F   = E
+  pred Fis = F
+  pred G   = Fis
+  pred Gis = G
+  pred A   = Gis
+  pred Ais = A
+  pred B   = Ais
+  pred _   = C
+
+  succ C   = Cis
+  succ Cis = D
+  succ D   = Dis
+  succ Dis = E
+  succ E   = F
+  succ F   = Fis
+  succ Fis = G
+  succ G   = Gis
+  succ Gis = A
+  succ A   = Ais
+  succ _   = B
+
+  toNat C   = 0
+  toNat Cis = 1
+  toNat D   = 2
+  toNat Dis = 3
+  toNat E   = 4
+  toNat F   = 5
+  toNat Fis = 6
+  toNat G   = 7
+  toNat Gis = 8
+  toNat A   = 9
+  toNat Ais = 10
+  toNat B   = 11
+
+  fromNat Z                                         = C
+  fromNat (S Z)                                     = Cis
+  fromNat (S (S Z))                                 = D
+  fromNat (S (S (S Z)))                             = Dis
+  fromNat (S (S (S (S Z))))                         = E
+  fromNat (S (S (S (S (S Z)))))                     = F
+  fromNat (S (S (S (S (S (S Z))))))                 = Fis
+  fromNat (S (S (S (S (S (S (S Z)))))))             = G
+  fromNat (S (S (S (S (S (S (S (S Z))))))))         = Gis
+  fromNat (S (S (S (S (S (S (S (S (S Z)))))))))     = A
+  fromNat (S (S (S (S (S (S (S (S (S (S Z)))))))))) = Ais
+  fromNat _                                         = B
+
+Show PitchClass where
+  show C   = "C"
+  show Cis = "Cis"
+  show D   = "D"
+  show Dis = "Dis"
+  show E   = "E"
+  show F   = "F"
+  show Fis = "Fis"
+  show G   = "G"
+  show Gis = "Gis"
+  show A   = "A"
+  show Ais = "Ais"
+  show B   = "B"
+
+Eq PitchClass where
+  C   == C   = True
+  Cis == Cis = True
+  D   == D   = True
+  Dis == Dis = True
+  E   == E   = True
+  F   == F   = True
+  Fis == Fis = True
+  G   == G   = True
+  Gis == Gis = True
+  A   == A   = True
+  Ais == Ais = True
+  B   == B   = True
+  _   == _   = False
+
+Ord PitchClass where
+  compare = compare `on` toNat
+
+Cast PitchClass Int where
+  cast = fromNat . toNat
+
+Octave : Type
+Octave = Int
+
+Pitch : Type
+Pitch = Pair PitchClass Octave
+
+[PitchOrd] Ord Pitch where
+  compare (pc1, oct1) (pc2, oct2) =
+    case compare oct1 oct2 of
+      EQ => compare pc1 pc2
+      res => res