From a3a89e8ae7491bfed2becf10a71fcf53959ec15c Mon Sep 17 00:00:00 2001
From: Ben Moon <software@guiltydolphin.com>
Date: Fri, 10 Jul 2020 23:12:46 +0100
Subject: [PATCH 1/4] Generalise OOZ semiring to arbitrary Mod

---
 examples/ooz.gr                                |  8 ++++----
 .../Language/Granule/Checker/Constraints.hs    | 18 ++++++++++++++----
 .../Checker/Constraints/SymbolicGrades.hs      | 15 ++++++---------
 .../src/Language/Granule/Checker/Primitives.hs |  2 +-
 frontend/src/Language/Granule/Syntax/Type.hs   |  4 ++++
 5 files changed, 29 insertions(+), 18 deletions(-)

diff --git a/examples/ooz.gr b/examples/ooz.gr
index bd00f6706..2dad41c58 100644
--- a/examples/ooz.gr
+++ b/examples/ooz.gr
@@ -1,13 +1,13 @@
 -- examples using a semiring {0, 1} with 1 + 1 = 0
 
-oozZero : forall a b. b -> a [0 : OOZ] -> b
+oozZero : forall a b. b -> a [0 : Mod 2] -> b
 oozZero f [x] = f
 
-oozOne : forall a b. (a -> b) -> a [1 : OOZ] -> b
+oozOne : forall a b. (a -> b) -> a [1 : Mod 2] -> b
 oozOne f [x] = f x
 
-oozTwo : forall a b. (f : a -> a -> b) -> a [0 : OOZ] -> b
+oozTwo : forall a b. (f : a -> a -> b) -> a [0 : Mod 2] -> b
 oozTwo f [x] = f x x
 
-oozThree : forall a b. (f : a -> a -> a -> b) -> a [1 : OOZ] -> b
+oozThree : forall a b. (f : a -> a -> a -> b) -> a [1 : Mod 2] -> b
 oozThree f [x] = f x x x
diff --git a/frontend/src/Language/Granule/Checker/Constraints.hs b/frontend/src/Language/Granule/Checker/Constraints.hs
index 8b0d6ee7c..62f56bbd1 100644
--- a/frontend/src/Language/Granule/Checker/Constraints.hs
+++ b/frontend/src/Language/Granule/Checker/Constraints.hs
@@ -148,6 +148,10 @@ freshCVarScoped quant name (isInterval -> Just t) q k =
             , SInterval solverVarLb solverVarUb )
           ))
 
+freshCVarScoped quant name (isMod -> Just n) q k =
+   quant q name (\solverVar ->
+    k (solverVar .>= 0 .&& (fromIntegral n) .> (0 :: SInteger), SMod solverVar n))
+
 freshCVarScoped quant name (isProduct -> Just (t1, t2)) q k =
 
   freshCVarScoped quant (name <> ".fst") t1 q
@@ -169,7 +173,6 @@ freshCVarScoped quant name (TyCon conName) q k =
                   .|| solverVar .== literal publicRepresentation
                   .|| solverVar .== literal unusedRepresentation
                     , SLevel solverVar)
-        "OOZ"    -> k (solverVar .== 0 .|| solverVar .== 1, SOOZ (ite (solverVar .== 0) sFalse sTrue))
         k -> solverError $ "I don't know how to make a fresh solver variable of type " <> show conName)
 
 freshCVarScoped quant name t q k | t == extendedNat = do
@@ -313,6 +316,9 @@ compileCoeffect (CNat n) k _ | k == nat =
 compileCoeffect (CNat n) k _ | k == extendedNat =
   return (SExtNat . fromInteger . toInteger $ n, sTrue)
 
+compileCoeffect (CNat n) (isMod -> Just i) _ =
+  pure (SMod (fromInteger . toInteger $ n) i, sTrue)
+
 compileCoeffect (CFloat r) (TyCon k) _ | internalName k == "Q" =
   return (SFloat  . fromRational $ r, sTrue)
 
@@ -360,7 +366,6 @@ compileCoeffect (CZero k') k vars  =
         "Nat"       -> return (SNat 0, sTrue)
         "Q"         -> return (SFloat (fromRational 0), sTrue)
         "Set"       -> return (SSet (S.fromList []), sTrue)
-        "OOZ"       -> return (SOOZ sFalse, sTrue)
         _           -> solverError $ "I don't know how to compile a 0 for " <> pretty k'
     (otherK', otherK) | (otherK' == extendedNat || otherK == extendedNat) ->
       return (SExtNat 0, sTrue)
@@ -375,6 +380,9 @@ compileCoeffect (CZero k') k vars  =
         (compileCoeffect (CZero t) t' vars)
         (compileCoeffect (CZero t) t' vars)
 
+    (isMod -> Just i, isMod -> Just j) | i == j ->
+      pure (SMod 0 i, sTrue)
+
     (TyVar _, _) -> return (SUnknown (SynLeaf (Just 0)), sTrue)
     _ -> solverError $ "I don't know how to compile a 0 for " <> pretty k'
 
@@ -386,7 +394,6 @@ compileCoeffect (COne k') k vars =
         "Nat"       -> return (SNat 1, sTrue)
         "Q"         -> return (SFloat (fromRational 1), sTrue)
         "Set"       -> return (SSet (S.fromList []), sTrue)
-        "OOZ"       -> return (SOOZ sTrue, sTrue)
         _           -> solverError $ "I don't know how to compile a 1 for " <> pretty k'
 
     (otherK', otherK) | (otherK' == extendedNat || otherK == extendedNat) ->
@@ -403,6 +410,9 @@ compileCoeffect (COne k') k vars =
           (compileCoeffect (COne t) t' vars)
           (compileCoeffect (COne t) t' vars)
 
+    (isMod -> Just i, isMod -> Just j) | i == j ->
+      pure (SMod 1 i, sTrue)
+
     (TyVar _, _) -> return (SUnknown (SynLeaf (Just 1)), sTrue)
 
     _ -> solverError $ "I don't know how to compile a 1 for " <> pretty k'
@@ -453,7 +463,7 @@ approximatedByOrEqualConstraint (SNat n) (SNat m)      = return $ n .== m
 approximatedByOrEqualConstraint (SFloat n) (SFloat m)  = return $ n .<= m
 approximatedByOrEqualConstraint SPoint SPoint          = return $ sTrue
 approximatedByOrEqualConstraint (SExtNat x) (SExtNat y) = return $ x .== y
-approximatedByOrEqualConstraint (SOOZ s) (SOOZ r) = pure $ s .== r
+approximatedByOrEqualConstraint (SMod s i) (SMod r j) | i == j = pure $ sMod s (fromIntegral i) .== sMod r (fromIntegral i)
 approximatedByOrEqualConstraint (SSet s) (SSet t) =
   return $ if s == t then sTrue else sFalse
 
diff --git a/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs b/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
index 95651e5da..ad8eb2bc2 100644
--- a/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
+++ b/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
@@ -35,10 +35,8 @@ data SGrade =
      -- Single point coeffect (not exposed at the moment)
      | SPoint
      | SProduct { sfst :: SGrade, ssnd :: SGrade }
-     -- | Coeffect with 1 + 1 = 0. False is 0, True is 1.
-     -- |
-     -- | Grade '0' denotes even usage, and grade '1' denotes odd usage.
-     | SOOZ SBool
+     -- | SMod k n is a Nat @k mod n@.
+     | SMod SInteger Int
 
      -- A kind of embedded uninterpreted sort which can accept some equations
      -- Used for doing some limited solving over poly coeffect grades
@@ -115,7 +113,7 @@ match (SInterval s1 s2) (SInterval t1 t2) = match s1 t1 && match t1 t2
 match SPoint SPoint = True
 match (SProduct s1 s2) (SProduct t1 t2) = match s1 t1 && match s2 t2
 match (SUnknown _) (SUnknown _) = True
-match (SOOZ _) (SOOZ _) = True
+match (SMod _ i) (SMod _ j) = i == j
 match _ _ = False
 
 isSProduct :: SGrade -> Bool
@@ -219,7 +217,7 @@ symGradeEq (SLevel n) (SLevel n') = return $ n .== n'
 symGradeEq (SSet n) (SSet n')     = solverError "Can't compare symbolic sets yet"
 symGradeEq (SExtNat n) (SExtNat n') = return $ n .== n'
 symGradeEq SPoint SPoint          = return $ sTrue
-symGradeEq (SOOZ s) (SOOZ r)      = pure $ s .== r
+symGradeEq (SMod s i) (SMod r j)  | i == j = pure $ sMod s (fromIntegral i) .== sMod r (fromIntegral i)
 symGradeEq s t | isSProduct s || isSProduct t =
     either solverError id (applyToProducts symGradeEq (.&&) (const sTrue) s t)
 
@@ -276,8 +274,7 @@ symGradePlus (SInterval lb1 ub1) (SInterval lb2 ub2) =
 symGradePlus SPoint SPoint = return $ SPoint
 symGradePlus s t | isSProduct s || isSProduct t =
   either solverError id (applyToProducts symGradePlus SProduct id s t)
--- 1 + 1 = 0
-symGradePlus (SOOZ s) (SOOZ r) = pure . SOOZ $ ite s (sNot r) r
+symGradePlus (SMod s i) (SMod r j) | i == j = pure $ SMod (s + r) i
 
 -- Direct encoding of additive unit
 symGradePlus (SUnknown t@(SynLeaf (Just u))) (SUnknown t'@(SynLeaf (Just u'))) =
@@ -309,7 +306,7 @@ symGradeTimes (SLevel lev1) (SLevel lev2) = return $
             (SLevel $ lev1 `smax` lev2)
 symGradeTimes (SFloat n1) (SFloat n2) = return $ SFloat $ n1 * n2
 symGradeTimes (SExtNat x) (SExtNat y) = return $ SExtNat (x * y)
-symGradeTimes (SOOZ s) (SOOZ r) = pure . SOOZ $ s .&& r
+symGradeTimes (SMod s i) (SMod r j) | i == j = pure $ SMod (s * r) i
 
 symGradeTimes (SInterval lb1 ub1) (SInterval lb2 ub2) =
     liftM2 SInterval (comb symGradeMeet) (comb symGradeJoin)
diff --git a/frontend/src/Language/Granule/Checker/Primitives.hs b/frontend/src/Language/Granule/Checker/Primitives.hs
index a1094207c..930dc2a58 100644
--- a/frontend/src/Language/Granule/Checker/Primitives.hs
+++ b/frontend/src/Language/Granule/Checker/Primitives.hs
@@ -40,7 +40,7 @@ typeConstructors =
     , (mkId "Private", (KPromote (TyCon $ mkId "Level"), [], False))
     , (mkId "Public", (KPromote (TyCon $ mkId "Level"), [], False))
     , (mkId "Unused", (KPromote (TyCon $ mkId "Level"), [], False))
-    , (mkId "OOZ", (KCoeffect, [], False)) -- 1 + 1 = 0
+    , (mkId "Mod", (KFun (KPromote (TyCon $ mkId "Nat")) KCoeffect, [], False)) -- modulo semiring
     , (mkId "Interval", (KFun KCoeffect KCoeffect, [], False))
     , (mkId "Set", (KFun (KVar $ mkId "k") (KFun (kConstr $ mkId "k") KCoeffect), [], False))
     -- Channels and protocol types
diff --git a/frontend/src/Language/Granule/Syntax/Type.hs b/frontend/src/Language/Granule/Syntax/Type.hs
index 9f5241e51..663e09ef9 100644
--- a/frontend/src/Language/Granule/Syntax/Type.hs
+++ b/frontend/src/Language/Granule/Syntax/Type.hs
@@ -269,6 +269,10 @@ isProduct (TyApp (TyApp (TyCon c) t) t') | internalName c == "×" =
     Just (t, t')
 isProduct _ = Nothing
 
+isMod :: Type -> Maybe Int
+isMod (TyApp (TyCon c) (TyInt n)) | internalName c == "Mod" = Just n
+isMod _ = Nothing
+
 ----------------------------------------------------------------------
 -- Helpers
 

From 530109d93e3adc1ccecab28524719f7d5bbb7e6c Mon Sep 17 00:00:00 2001
From: Ben Moon <software@guiltydolphin.com>
Date: Fri, 10 Jul 2020 22:13:41 +0100
Subject: [PATCH 2/4] Add initial support for mod on grades

---
 .../src/Language/Granule/Checker/Constraints.hs  |  3 +++
 .../Checker/Constraints/SymbolicGrades.hs        |  6 ++++++
 frontend/src/Language/Granule/Checker/Kinds.hs   |  1 +
 .../src/Language/Granule/Checker/Substitution.hs | 10 ++++++++++
 frontend/src/Language/Granule/Syntax/Lexer.x     |  2 ++
 frontend/src/Language/Granule/Syntax/Parser.y    |  4 +++-
 frontend/src/Language/Granule/Syntax/Pretty.hs   |  2 ++
 frontend/src/Language/Granule/Syntax/Type.hs     | 16 +++++++++++++++-
 8 files changed, 42 insertions(+), 2 deletions(-)

diff --git a/frontend/src/Language/Granule/Checker/Constraints.hs b/frontend/src/Language/Granule/Checker/Constraints.hs
index 62f56bbd1..567342c86 100644
--- a/frontend/src/Language/Granule/Checker/Constraints.hs
+++ b/frontend/src/Language/Granule/Checker/Constraints.hs
@@ -345,6 +345,9 @@ compileCoeffect c@(CTimes n m) k vars =
 compileCoeffect c@(CMinus n m) k vars =
   bindM2And symGradeMinus (compileCoeffect n k vars) (compileCoeffect m k vars)
 
+compileCoeffect c@(CMod n m) k vars =
+  bindM2And symGradeMod (compileCoeffect n k vars) (compileCoeffect m k vars)
+
 compileCoeffect c@(CExpon n m) k vars = do
   (g1, p1) <- compileCoeffect n k vars
   (g2, p2) <- compileCoeffect m k vars
diff --git a/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs b/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
index ad8eb2bc2..3fed4393e 100644
--- a/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
+++ b/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
@@ -360,6 +360,12 @@ symGradeMinus s t | isSProduct s || isSProduct t =
   either solverError id (applyToProducts symGradeMinus SProduct id s t)
 symGradeMinus s t = solverError $ cannotDo "minus" s t
 
+-- | Mod operation on symbolic grades
+symGradeMod :: SGrade -> SGrade -> Symbolic SGrade
+-- TODO: perhaps fail here if dividing by 0? (2020-07-10)
+symGradeMod s@(SNat n1) t@(SNat n2) = pure . SNat $ sMod n1 n2
+symGradeMod s t = solverError $ cannotDo "mod" s t
+
 cannotDo :: String -> SGrade -> SGrade -> String
 cannotDo op (SUnknown s) (SUnknown t) =
   "It is unknown whether "
diff --git a/frontend/src/Language/Granule/Checker/Kinds.hs b/frontend/src/Language/Granule/Checker/Kinds.hs
index 8e94fe21e..13b531dee 100644
--- a/frontend/src/Language/Granule/Checker/Kinds.hs
+++ b/frontend/src/Language/Granule/Checker/Kinds.hs
@@ -242,6 +242,7 @@ inferCoeffectTypeInContext s _ (CTimes c c') = fmap fst2 $ mguCoeffectTypesFromC
 inferCoeffectTypeInContext s _ (CMeet c c')  = fmap fst2 $ mguCoeffectTypesFromCoeffects s c c'
 inferCoeffectTypeInContext s _ (CJoin c c')  = fmap fst2 $ mguCoeffectTypesFromCoeffects s c c'
 inferCoeffectTypeInContext s _ (CExpon c c') = fmap fst2 $ mguCoeffectTypesFromCoeffects s c c'
+inferCoeffectTypeInContext s _ (CMod c c')   = fmap fst2 $ mguCoeffectTypesFromCoeffects s c c'
 
 -- Coeffect variables should have a type in the cvar->kind context
 inferCoeffectTypeInContext s ctxt (CVar cvar) = do
diff --git a/frontend/src/Language/Granule/Checker/Substitution.hs b/frontend/src/Language/Granule/Checker/Substitution.hs
index 48aedb03d..31533ae98 100644
--- a/frontend/src/Language/Granule/Checker/Substitution.hs
+++ b/frontend/src/Language/Granule/Checker/Substitution.hs
@@ -130,6 +130,11 @@ instance Substitutable Coeffect where
         c2' <- substitute subst c2
         return $ CProduct c1' c2'
 
+    substitute subst (CMod c1 c2) = do
+        c1' <- substitute subst c1
+        c2' <- substitute subst c2
+        return $ CMod c1' c2'
+
     substitute subst (CVar v) =
         case lookup v subst of
             Just (SubstC c) -> do
@@ -672,6 +677,11 @@ instance Unifiable Coeffect where
         u2 <- unify c2 c2'
         u1 <<>> u2
 
+    unify (CMod c1 c2) (CMod c1' c2') = do
+        u1 <- unify c1 c1'
+        u2 <- unify c2 c2'
+        u1 <<>> u2
+
     unify (CInfinity k) (CInfinity k') = do
         unify k k'
 
diff --git a/frontend/src/Language/Granule/Syntax/Lexer.x b/frontend/src/Language/Granule/Syntax/Lexer.x
index 2c65bf0eb..84fd166cf 100755
--- a/frontend/src/Language/Granule/Syntax/Lexer.x
+++ b/frontend/src/Language/Granule/Syntax/Lexer.x
@@ -86,6 +86,7 @@ tokens :-
   \_                            { \p _ -> TokenUnderscore p }
   \|                            { \p s -> TokenPipe p }
   \/                            { \p s -> TokenForwardSlash p }
+  "%"                           { \p s -> TokenPercent p }
   "≤"                           { \p s -> TokenLesserEq p }
   "<="                          { \p s -> TokenLesserEq p }
   "≥"                           { \p s -> TokenGreaterEq p }
@@ -170,6 +171,7 @@ data Token
   | TokenEmptyHole AlexPosn
   | TokenHoleStart AlexPosn
   | TokenHoleEnd AlexPosn
+  | TokenPercent AlexPosn
 
   deriving (Eq, Show, Generic)
 
diff --git a/frontend/src/Language/Granule/Syntax/Parser.y b/frontend/src/Language/Granule/Syntax/Parser.y
index 5b394e19b..74e4844b0 100644
--- a/frontend/src/Language/Granule/Syntax/Parser.y
+++ b/frontend/src/Language/Granule/Syntax/Parser.y
@@ -91,6 +91,7 @@ import Language.Granule.Utils hiding (mkSpan)
     '.'   { TokenPeriod _ }
     '`'   { TokenBackTick _ }
     '^'   { TokenCaret _ }
+    '%'   { TokenPercent _ }
     '..'  { TokenDotDot _ }
     "\\/" { TokenJoin _ }
     "/\\" { TokenMeet _ }
@@ -323,7 +324,7 @@ TyApp :: { Type }
  | TyAtom                     { $1 }
 
 TyJuxt :: { Type }
-  : TyJuxt '`' TyAtom '`'     { TyApp $3 $1 } 
+  : TyJuxt '`' TyAtom '`'     { TyApp $3 $1 }
   | TyJuxt TyAtom             { TyApp $1 $2 }
   | TyAtom                    { $1 }
   | TyAtom '+' TyAtom         { TyInfix TyOpPlus $1 $3 }
@@ -369,6 +370,7 @@ Coeffect :: { Coeffect }
   | Coeffect '*' Coeffect       { CTimes $1 $3 }
   | Coeffect '-' Coeffect       { CMinus $1 $3 }
   | Coeffect '^' Coeffect       { CExpon $1 $3 }
+  | Coeffect '%' Coeffect       { CMod   $1 $3 }
   | Coeffect "/\\" Coeffect       { CMeet $1 $3 }
   | Coeffect "\\/" Coeffect       { CJoin $1 $3 }
   | '(' Coeffect ')'            { $2 }
diff --git a/frontend/src/Language/Granule/Syntax/Pretty.hs b/frontend/src/Language/Granule/Syntax/Pretty.hs
index 8c61c8ff5..aca40884f 100644
--- a/frontend/src/Language/Granule/Syntax/Pretty.hs
+++ b/frontend/src/Language/Granule/Syntax/Pretty.hs
@@ -88,6 +88,8 @@ instance Pretty Coeffect where
       prettyNested c <> " * " <> prettyNested d
     pretty (CMinus c d) =
       prettyNested c <> " - " <> prettyNested d
+    pretty (CMod c1 c2) =
+      prettyNested c1 <> " % " <> prettyNested c2
     pretty (CSet xs) =
       "{" <> intercalate "," (map (\(name, t) -> name <> " : " <> prettyNested t) xs) <> "}"
     pretty (CSig c t) =
diff --git a/frontend/src/Language/Granule/Syntax/Type.hs b/frontend/src/Language/Granule/Syntax/Type.hs
index 663e09ef9..fd807af72 100644
--- a/frontend/src/Language/Granule/Syntax/Type.hs
+++ b/frontend/src/Language/Granule/Syntax/Type.hs
@@ -145,6 +145,7 @@ data Coeffect = CNat      Int
               | CSig      Coeffect Type
               | CExpon    Coeffect Coeffect
               | CProduct  Coeffect Coeffect
+              | CMod      Coeffect Coeffect
     deriving (Eq, Ord, Show, Rp.Data)
 
 -- Algebra for coeffects
@@ -165,7 +166,9 @@ data CoeffectFold a = CoeffectFold
   , cSet   :: [(String, Type)] -> a
   , cSig   :: a -> Type -> a
   , cExpon :: a -> a -> a
-  , cProd  :: a -> a -> a }
+  , cProd  :: a -> a -> a
+  , cMod   :: a -> a -> a
+  }
 
 -- Base monadic algebra
 baseCoeffectFold :: CoeffectFold Coeffect
@@ -188,6 +191,7 @@ baseCoeffectFold =
     , cSig = CSig
     , cExpon = CExpon
     , cProd = CProduct
+    , cMod  = CMod
     }
 
 -- | Fold on a `coeffect` type
@@ -245,6 +249,10 @@ coeffectFold algebra = go
       c1' = go c1
       c2' = go c2
       in (cProd algebra) c1' c2'
+    go (CMod c1 c2) = let
+      c1' = go c1
+      c2' = go c2
+      in (cMod algebra) c1' c2'
 
 publicRepresentation, privateRepresentation :: Integer
 privateRepresentation = 1
@@ -430,6 +438,7 @@ instance Term Coeffect where
     freeVars (CExpon c1 c2) = freeVars c1 <> freeVars c2
     freeVars (CMeet c1 c2) = freeVars c1 <> freeVars c2
     freeVars (CJoin c1 c2) = freeVars c1 <> freeVars c2
+    freeVars (CMod c1 c2) = freeVars c1 <> freeVars c2
     freeVars CNat{}  = []
     freeVars CFloat{} = []
     freeVars CInfinity{} = []
@@ -524,6 +533,11 @@ instance Freshenable m Coeffect where
       c2' <- freshen c2
       return $ CJoin c1' c2'
 
+    freshen (CMod c1 c2) = do
+      c1' <- freshen c1
+      c2' <- freshen c2
+      return $ CMod c1' c2'
+
     freshen (CSet cs) = do
        cs' <- mapM (\(s, t) -> freshen t >>= (\t' -> return (s, t'))) cs
        return $ CSet cs'

From c6b74d7179026a58d68ff65ca178be5f5521fc22 Mon Sep 17 00:00:00 2001
From: Ben Moon <software@guiltydolphin.com>
Date: Fri, 10 Jul 2020 22:15:28 +0100
Subject: [PATCH 3/4] Space nits

---
 examples/LeftPadTutorial.gr                                   | 2 +-
 frontend/src/Language/Granule/Checker/Constraints.hs          | 2 +-
 .../Language/Granule/Checker/Constraints/SymbolicGrades.hs    | 4 ++--
 frontend/src/Language/Granule/Checker/Kinds.hs                | 2 +-
 frontend/src/Language/Granule/Checker/Substitution.hs         | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/examples/LeftPadTutorial.gr b/examples/LeftPadTutorial.gr
index 901ac03dd..dd6f8bba1 100644
--- a/examples/LeftPadTutorial.gr
+++ b/examples/LeftPadTutorial.gr
@@ -135,4 +135,4 @@ input = Cons 1 (Cons 2 (Cons 3 Nil))
 -- vector length 6
 
 main : Vec 6 Int
-main = leftPad input [0] (S (S (S (S (S (S Z))))))
\ No newline at end of file
+main = leftPad input [0] (S (S (S (S (S (S Z))))))
diff --git a/frontend/src/Language/Granule/Checker/Constraints.hs b/frontend/src/Language/Granule/Checker/Constraints.hs
index 567342c86..133bff2b2 100644
--- a/frontend/src/Language/Granule/Checker/Constraints.hs
+++ b/frontend/src/Language/Granule/Checker/Constraints.hs
@@ -631,4 +631,4 @@ bindM2And' k ma mb = do
   return (p .&& q .&& c)
 
 liftM2And :: Monad m => (t1 -> t2 -> b) -> m (t1, SBool) -> m (t2, SBool) -> m (b, SBool)
-liftM2And k = bindM2And (\a b -> return (k a b))
\ No newline at end of file
+liftM2And k = bindM2And (\a b -> return (k a b))
diff --git a/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs b/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
index 3fed4393e..bd5652be4 100644
--- a/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
+++ b/frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
@@ -96,7 +96,7 @@ sLtTree (SynPlus s s') (SynPlus t t')   = liftM2 (.&&) (sLtTree s t) (sLtTree s'
 sLtTree (SynTimes s s') (SynTimes t t') = liftM2 (.&&) (sLtTree s t) (sLtTree s' t')
 sLtTree (SynMeet s s') (SynMeet t t')   = liftM2 (.&&) (sLtTree s t) (sLtTree s' t')
 sLtTree (SynJoin s s') (SynJoin t t')   = liftM2 (.&&) (sLtTree s t) (sLtTree s' t')
-sLtTree (SynMerge sb s s') (SynMerge sb' t t') = 
+sLtTree (SynMerge sb s s') (SynMerge sb' t t') =
   liftM2 (.&&) (return $ sb .== sb') (liftM2 (.&&) (sLtTree s t) (sLtTree s' t'))
 sLtTree (SynLeaf Nothing) (SynLeaf Nothing) = return $ sFalse
 sLtTree (SynLeaf (Just n)) (SynLeaf (Just n')) = return $ n .< n'
@@ -378,4 +378,4 @@ cannotDo op s t =
   "Cannot perform symbolic operation `"
       <> op <> "` on "
       <> show s <> " and "
-      <> show t
\ No newline at end of file
+      <> show t
diff --git a/frontend/src/Language/Granule/Checker/Kinds.hs b/frontend/src/Language/Granule/Checker/Kinds.hs
index 13b531dee..0c55c0001 100644
--- a/frontend/src/Language/Granule/Checker/Kinds.hs
+++ b/frontend/src/Language/Granule/Checker/Kinds.hs
@@ -323,4 +323,4 @@ isEffectTypeFromKind s kind =
             if isEffectKind kind'
                 then return $ Right effTy
                 else return $ Left kind
-        _ -> return $ Left kind
\ No newline at end of file
+        _ -> return $ Left kind
diff --git a/frontend/src/Language/Granule/Checker/Substitution.hs b/frontend/src/Language/Granule/Checker/Substitution.hs
index 31533ae98..0e47acf20 100644
--- a/frontend/src/Language/Granule/Checker/Substitution.hs
+++ b/frontend/src/Language/Granule/Checker/Substitution.hs
@@ -757,4 +757,4 @@ updateTyVar s tyVar k = do
      | tyVar == kindVar = (name, (k, q)) : rewriteCtxt ctxt
     rewriteCtxt ((name, (KVar kindVar, q)) : ctxt)
      | tyVar == kindVar = (name, (k, q)) : rewriteCtxt ctxt
-    rewriteCtxt (x : ctxt) = x : rewriteCtxt ctxt
\ No newline at end of file
+    rewriteCtxt (x : ctxt) = x : rewriteCtxt ctxt

From f390cf3ea9240af683f0467db41e872679286e1a Mon Sep 17 00:00:00 2001
From: Ben Moon <software@guiltydolphin.com>
Date: Sun, 12 Jul 2020 12:20:39 +0100
Subject: [PATCH 4/4] Add file with Mod properties

---
 examples/modSR.gr | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 examples/modSR.gr

diff --git a/examples/modSR.gr b/examples/modSR.gr
new file mode 100644
index 000000000..915695cc3
--- /dev/null
+++ b/examples/modSR.gr
@@ -0,0 +1,36 @@
+-- examples using the 'Mod k' semiring
+
+-- todo: support arbitrary nats for the Mod index
+
+isAssocPlus1 : forall {a b : Type, n m k : Mod 7} . (a [(n + m) + k] -> b) -> (a [n + (m + k)] -> b)
+isAssocPlus1 f = f
+
+isAssocPlus2 : forall {a b : Type, n m k : Mod 7} . (a [n + (m + k)] -> b) -> (a [(n + m) + k] -> b)
+isAssocPlus2 f = f
+
+isAssocMult1 : forall {a b : Type, n m k : Mod 7} . (a [(n * m) * k] -> b) -> (a [n * (m * k)] -> b)
+isAssocMult1 f = f
+
+isAssocMult2 : forall {a b : Type, n m k : Mod 7} . (a [n * (m * k)] -> b) -> (a [(n * m) * k] -> b)
+isAssocMult2 f = f
+
+isDistrib1 : forall {a b : Type, n m k : Mod 7} . (a [(n + m) * k] -> b) -> (a [(n * k) + (m * k)] -> b)
+isDistrib1 f = f
+
+isDistrib2 : forall {a b : Type, n m k : Mod 7} . (a [(n * k) + (m * k)] -> b) -> (a [(n + m) * k] -> b)
+isDistrib2 f = f
+
+isCommutePlus : forall {a b : Type, n m : Mod 7} . (a [n + m] -> b) -> (a [m + n] -> b)
+isCommutePlus f = f
+
+isCommuteMult : forall {a b : Type, n m : Mod 7} . (a [n * m] -> b) -> (a [m * n] -> b)
+isCommuteMult f = f
+
+zeroPlusIdentity : forall {a b : Type, n : Mod 7} . (a [n + (0 : Mod 7)] -> b) -> (a [n] -> b)
+zeroPlusIdentity f = f
+
+oneTimesIdentity : forall {a b : Type, n : Mod 7} . (a [n * (1 : Mod 7)] -> b) -> (a [n] -> b)
+oneTimesIdentity f = f
+
+zeroAbsorbs : forall {a b : Type, n : Mod 7} . (a [n * (0 : Mod 7)] -> b) -> (a [0 : Mod 7] -> b)
+zeroAbsorbs f = f