[idris] Try a different approach

elba.toml

@@ -1,6 +1,6 @@
 [package]
 name = "yurrriq/gis"
-version = "0.3.1"
+version = "0.4.0"
 authors = ["Eric Bailey <eric@ericb.me>"]
 repository = "https://github.com/yurrriq/gis"
 # TODO: readme = "README.md"
@@ -15,6 +15,7 @@ license = "MIT"
 path = "src/"
 mods = [
   "Data.GIS",
+  "Data.GIS.Verified",
   "Data.Int.Algebra",
   "Data.Music",
 ]
@@ -23,9 +24,9 @@ idris_opts = ["-p", "contrib"]
 [[targets.test]]
 path = "test/"
 main = "Data.GIS.Test.runTests"
-idris_opts = ["-p", "specdris"]
+idris_opts = ["-p", "contrib", "-p", "specdris"]
 
 [[targets.test]]
 path = "test/"
 main = "Data.Music.Test.runTests"
-idris_opts = ["-p", "specdris"]
+idris_opts = ["-p", "contrib", "-p", "specdris"]

src/Data/GIS.idr

@@ -2,48 +2,49 @@ module Data.GIS
 
 import Control.Algebra
 import Control.Algebra.NumericImplementations
+import Control.Arrow
+import Control.Category
 import Data.Int.Algebra
+import Data.Morphisms
 import Data.Music
 
 %access public export
 
-interface Group ivls => HasLabel space ivls where
-  LABEL : space -> ivls
 
-interface HasLabel space ivls => GIS space ivls where
-  int : space -> space -> ivls
+interface Group ivls => GIS space ivls | space where
+  ref     : space
+  int     : space -> space -> ivls
+  LABEL   : 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')
+  -- LABEL s = if s == ref then neutral else int ref s
 
 
-[DiatonicPitchLABEL] HasLabel Diatonic.Pitch Int using PlusZnGroup, DiatonicPitchClassRefC where
-  LABEL (pitchClass, octave) = fromNat (toNat pitchClass) + 7 * octave
+[IntScalarGIS] GIS Int Int where
+  ref   = 0
+  LABEL = id
 
-[DiatonicPitchGIS] GIS Diatonic.Pitch Int using DiatonicPitchLABEL 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')"
 
+[DiatonicPitchGIS] GIS Diatonic.Pitch Int where
+  ref   = (C, 0)
+  LABEL = cast
 
-[PSpaceLABEL] HasLabel Chromatic.Pitch Int using PlusZnGroup, PitchClassRefC where
-  LABEL (pitchClass, octave) = fromNat (toNat pitchClass) + 12 * octave
 
-[PSpaceGIS] GIS Chromatic.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')"
+[PSpaceGIS] GIS Chromatic.Pitch Int where
+  ref   = (C, 0)
+  LABEL = cast
 
 
-[PCSpaceLABEL] HasLabel Chromatic.PitchClass (Zn 12) using PlusZnGroup, PitchClassRefC where
-  LABEL = MkZn . fromNat . toNat
+[PCSpaceGIS] GIS Chromatic.PitchClass (Zn 12) where
+  ref   = C
+  LABEL = cast
 
-[PCSpaceGIS] GIS Chromatic.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')"
 
+[DiatonicPitchClassGIS] GIS Diatonic.PitchClass (Zn 7) where
+  ref   = C
+  LABEL = cast
 
-[DiatonicPitchClassLABEL] HasLabel Diatonic.PitchClass (Zn 7) using PlusZnGroup, DiatonicPitchClassRefC where
-  LABEL = MkZn . fromNat . toNat
 
-[DiatonicPitchClassGIS] GIS Diatonic.PitchClass (Zn 7) using DiatonicPitchClassLABEL 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')"
+[PitchClassRefFGIS] GIS Chromatic.PitchClass (Zn 12) where
+  ref     = F
+  LABEL s = MkZn (cast s) <-> MkZn 5

src/Data/GIS/Verified.idr

@@ -0,0 +1,11 @@
+module Data.GIS.Verified
+
+import Control.Algebra
+import Data.GIS
+
+%access public export
+
+
+interface GIS space ivls => VerifiedGIS space ivls | space where
+  conditionA : (r, s, t : space) -> int r s <+> int s t = int r t
+  conditionB : (s : space) -> (i : ivls) -> (int s t = i, int s t' = i) -> t = t'

src/Data/Int/Algebra.idr

@@ -4,31 +4,33 @@ import Control.Algebra
 
 %access public export
 
-[PlusIntSemi] Semigroup Int where
-  (<+>) = (+)
 
-[PlusIntMonoid] Monoid Int using PlusIntSemi where
-  neutral = 0
+--- ||| Return the smallest non-negative representative of the class of a modulo n.
+leastPositiveResidue : (Integral ty, Ord ty) => (a : ty) -> (b : ty) -> ty
+leastPositiveResidue a n = let r = a `mod` n in if r < 0 then r + n else r
 
-[PlusIntGroup] Group Int using PlusIntMonoid where
-  inverse = (* -1)
 
 data Zn : (n : Nat) -> Type where
   MkZn : Int -> Zn n
 
-[PlusZnSemi] Semigroup (Zn n) where
+
+Semigroup (Zn n) where
   (MkZn x) <+> (MkZn y) = let z = x + y; i = fromNat n in
     MkZn $ if z < i then z else z - i
 
-[PlusZnMonoid] Monoid (Zn n) using PlusZnSemi where
+
+Monoid (Zn n) where
   neutral = MkZn 0
 
-[PlusZnGroup] Group (Zn n) using PlusZnMonoid where
+
+Group (Zn n) where
   inverse (MkZn x) = MkZn (fromNat n - x)
 
+
 Eq (Zn n) where
   (MkZn x) == (MkZn y) = x == y
 
+
 DecEq (Zn n) where
   decEq x y =
       case x == y of
@@ -40,9 +42,6 @@ DecEq (Zn n) where
       primitiveNotEq : x = y -> Void
       primitiveNotEq prf = believe_me {b = Void} ()
 
---- ||| Return the smallest non-negative representative of the class of a modulo n.
-leastPositiveResidue : (Integral ty, Ord ty) => (a : ty) -> (b : ty) -> ty
-leastPositiveResidue a n = let r = a `mod` n in if r < 0 then r + n else r
 
 Show (Zn n) where
   show (MkZn a) = show (leastPositiveResidue a (fromNat n))

src/Data/Music.idr

@@ -3,11 +3,19 @@ module Data.Music
 import Data.Combinators
 import Data.Int.Algebra
 
+
+private
+divMod : Nat -> Nat -> (Nat, Nat)
+divMod n d = (n `div` d, n `mod` d)
+
+
 %access public export
 
+
 Octave : Type
 Octave = Int
 
+
 namespace Chromatic
   data PitchClass
     = C
@@ -23,7 +31,7 @@ namespace Chromatic
     | Ais
     | B
 
-  [PitchClassRefC] Enum PitchClass where
+  Enum PitchClass where
     pred C   = B
     pred Cis = C
     pred D   = Cis
@@ -66,76 +74,16 @@ namespace Chromatic
     fromNat Z = C
     fromNat (S k) = succ (fromNat k)
 
-  [PitchClassRefCis] Enum PitchClass where
-    pred = pred@{PitchClassRefC}
-    succ = succ@{PitchClassRefC}
-    toNat = Nat.pred . toNat@{PitchClassRefC}
-    fromNat = fromNat@{PitchClassRefC} . succ
-
-  [PitchClassRefD] Enum PitchClass where
-    pred = pred@{PitchClassRefCis}
-    succ = succ@{PitchClassRefCis}
-    toNat = Nat.pred . toNat@{PitchClassRefCis}
-    fromNat = fromNat@{PitchClassRefCis} . succ
-
-  [PitchClassRefDis] Enum PitchClass where
-    pred = pred@{PitchClassRefD}
-    succ = succ@{PitchClassRefD}
-    toNat = Nat.pred . toNat@{PitchClassRefD}
-    fromNat = fromNat@{PitchClassRefD} . succ
-
-  [PitchClassRefE] Enum PitchClass where
-    pred = pred@{PitchClassRefDis}
-    succ = succ@{PitchClassRefDis}
-    toNat = Nat.pred . toNat@{PitchClassRefDis}
-    fromNat = fromNat@{PitchClassRefDis} . succ
-
-  [PitchClassRefF] Enum PitchClass where
-    pred = pred@{PitchClassRefE}
-    succ = succ@{PitchClassRefE}
-    toNat = Nat.pred . toNat@{PitchClassRefE}
-    fromNat = fromNat@{PitchClassRefE} . succ
-
-  [PitchClassRefFis] Enum PitchClass where
-    pred = pred@{PitchClassRefF}
-    succ = succ@{PitchClassRefF}
-    toNat = Nat.pred . toNat@{PitchClassRefF}
-    fromNat = fromNat@{PitchClassRefF} . succ
-
-  [PitchClassRefG] Enum PitchClass where
-    pred = pred@{PitchClassRefFis}
-    succ = succ@{PitchClassRefFis}
-    toNat = Nat.pred . toNat@{PitchClassRefFis}
-    fromNat = fromNat@{PitchClassRefFis} . succ
-
-  [PitchClassRefGis] Enum PitchClass where
-    pred = pred@{PitchClassRefG}
-    succ = succ@{PitchClassRefG}
-    toNat = Nat.pred . toNat@{PitchClassRefG}
-    fromNat = fromNat@{PitchClassRefG} . succ
-
-  [PitchClassRefA] Enum PitchClass where
-    pred = pred@{PitchClassRefGis}
-    succ = succ@{PitchClassRefGis}
-    toNat = Nat.pred . toNat@{PitchClassRefGis}
-    fromNat = fromNat@{PitchClassRefGis} . succ
-
-  [PitchClassRefAis] Enum PitchClass where
-    pred = pred@{PitchClassRefA}
-    succ = succ@{PitchClassRefA}
-    toNat = Nat.pred . toNat@{PitchClassRefA}
-    fromNat = fromNat@{PitchClassRefA} . succ
-
-  [PitchClassRefB] Enum PitchClass where
-    pred = pred@{PitchClassRefAis}
-    succ = succ@{PitchClassRefAis}
-    toNat = Nat.pred . toNat@{PitchClassRefAis}
-    fromNat = fromNat@{PitchClassRefAis} . succ
-
-  Eq PitchClass using PitchClassRefC where
+  Cast PitchClass Int where
+    cast = toIntNat . toNat
+
+  Cast PitchClass (Zn n) where
+    cast = MkZn . cast
+
+  Eq PitchClass where
     (==) = (==) `on` toNat
 
-  Ord PitchClass using PitchClassRefC where
+  Ord PitchClass where
     compare = compare `on` toNat
 
   Show PitchClass where
@@ -155,9 +103,25 @@ namespace Chromatic
   Pitch : Type
   Pitch = Pair PitchClass Octave
 
+  Enum Pitch where
+    succ (B, oct)  = (C, oct + 1)
+    succ (pc, oct) = (succ C, oct)
+
+    pred (C, oct)  = (B, oct - 1)
+    pred (pc, oct) = (pred pc, oct)
+
+    toNat (pc, oct) = toNat pc + 12 * (toNat oct)
+
+    fromNat k =
+      let (pc, oct) = assert_total (divMod k 12) in
+        (fromNat pc, toIntNat oct)
+
   Cast Pitch PitchClass where
     cast = fst
 
+  Cast Pitch Int where
+    cast (pc, oct) = toIntNat (toNat pc) + 12 * oct
+
   [PitchOrd] Ord Pitch where
     compare (pc1, oct1) (pc2, oct2) =
       case compare oct1 oct2 of
@@ -178,7 +142,7 @@ namespace Diatonic
     | A
     | B
 
-  [DiatonicPitchClassRefC] Enum Diatonic.PitchClass where
+  Enum Diatonic.PitchClass where
     pred C = B
     pred D = C
     pred E = D
@@ -206,12 +170,18 @@ namespace Diatonic
     fromNat Z     = C
     fromNat (S k) = succ (fromNat k)
 
-  Eq Diatonic.PitchClass using DiatonicPitchClassRefC where
+  Eq Diatonic.PitchClass where
     (==) = (==) `on` toNat
 
-  Ord Diatonic.PitchClass using DiatonicPitchClassRefC where
+  Ord Diatonic.PitchClass where
     compare = compare `on` toNat
 
+  Cast Diatonic.PitchClass Int where
+    cast = toIntNat . toNat
+
+  Cast Diatonic.PitchClass (Zn n) where
+    cast = MkZn . cast
+
   Cast Diatonic.PitchClass Chromatic.PitchClass where
     cast C = C
     cast D = D
@@ -227,12 +197,28 @@ namespace Diatonic
   Pitch : Type
   Pitch = Pair Diatonic.PitchClass Octave
 
+  Enum Diatonic.Pitch where
+    succ (B, oct)  = (C, oct + 1)
+    succ (pc, oct) = (succ C, oct)
+
+    pred (C, oct)  = (B, oct - 1)
+    pred (pc, oct) = (pred C, oct)
+
+    toNat (pc, oct) = toNat pc + 7 * (toNat oct)
+
+    fromNat k =
+      let (pc, oct) = assert_total (divMod k 7) in
+        (fromNat pc, toIntNat oct)
+
   Cast Diatonic.Pitch Diatonic.PitchClass where
     cast = fst
 
   Cast Diatonic.Pitch Chromatic.Pitch where
     cast (dpc, octave) = (cast dpc, octave)
 
+  Cast Diatonic.Pitch Int where
+    cast (pc, oct) = toIntNat (toNat pc) + 7 * oct
+
   [DiatonicPitchOrd] Ord Diatonic.Pitch where
     compare = compare@{PitchOrd} `on` cast
 

test/Data/GIS/Test.idr

@@ -1,5 +1,6 @@
 module Data.GIS.Test
 
+import Control.Algebra.NumericImplementations
 import Data.GIS
 import Data.Int.Algebra
 import Data.Music
@@ -9,7 +10,7 @@ import Specdris.Spec
 %access export
 
 lewin2_1_1 : SpecTree
-lewin2_1_1 = let int = int@{DiatonicPitchGIS}; (<+>) = (<+>)@{PlusIntSemi} in
+lewin2_1_1 = let int = int@{DiatonicPitchGIS} in
   describe "Diatonic pitch examples (Lewin, 2.1.1)" $ do
     it "int(C4, C4) = 0" $ do
       int (C, 4) (C, 4) === 0
@@ -43,7 +44,7 @@ lewin2_1_2 = let int = int@{PSpaceGIS} in
       int (C, 4) (F, 2) === -19
 
 lewin2_1_3 : SpecTree
-lewin2_1_3 = let int = int@{PCSpaceGIS}; fromNat = fromNat@{PitchClassRefC} in
+lewin2_1_3 = let int = int@{PCSpaceGIS} in
   describe "pc-space examples (Lewin, 2.1.3)" $ do
     it "int(8, 1) = 5" $ do
       int (fromNat 8) (fromNat 1) === MkZn 5