Merge pull request #30 from stefan-hoeck/style

[ style ] adhere to style guide
stefan-hoeck · Aug 22, 2023 · d470999 · d470999
2 parents 80a7c46 + ae3ac95
commit d470999
Show file tree

Hide file tree

Showing 40 changed files with 798 additions and 638 deletions.
diff --git a/docs/src/Documentation.md b/docs/src/Documentation.md
@@ -76,9 +76,10 @@ to manually define values of type `(<)`, is annotated with
 a `%hint` pragma.
 
 ```idris
-fromInteger :  (n : Integer)
-            -> (0 prf : cast n > the Bits64 0)
-            => Positive
+fromInteger :
+     (n : Integer)
+  -> {auto 0 prf : cast n > the Bits64 0}
+  -> Positive
 fromInteger n = Element (cast n) prf
 
 twelve : Positive
@@ -120,10 +121,11 @@ record Base where
 
 namespace Base
   public export
-  fromInteger :  (n : Integer)
-              -> (0 gt1   : cast n > the Bits64 1)
-              => (0 lte16 : cast n <= the Bits64 16)
-              => Base
+  fromInteger :
+       (n : Integer)
+    -> {auto 0 gt1   : cast n > the Bits64 1}
+    -> {auto 0 lte16 : cast n <= the Bits64 16}
+    -> Base
   fromInteger n = MkBase (cast n) gt1 lte16
 ```
 
@@ -150,14 +152,16 @@ is quite verbose.
 lit : Bits64 -> Base -> String
 lit 0 _ = "0"
 lit x (MkBase b gt1 lte16) = go [] x
-  where go : List Char -> Bits64 -> String
-        go cs 0 = pack cs
-        go cs v =
-          let 0 gt0         = the (0 < b) $ trans %search gt1
-              Element d ltb = rmod v b
-              v2            = sdiv v b
-              c             = hexChar d {prf = trans_LT_LTE ltb lte16}
-           in go (c :: cs) (assert_smaller v v2)
+
+  where
+    go : List Char -> Bits64 -> String
+    go cs 0 = pack cs
+    go cs v =
+      let 0 gt0         := the (0 < b) $ trans %search gt1
+          Element d ltb := rmod v b
+          v2            := sdiv v b
+          c             := hexChar d {prf = trans_LT_LTE ltb lte16}
+       in go (c :: cs) (assert_smaller v v2)
 ```
 
 Functions `rmod` and `sdiv` each require a proof that `b` is larger than zero.
@@ -209,11 +213,13 @@ lt16 = trans_LT_LTE
 lit2 : Bits64 -> Base -> String
 lit2 0 _ = "0"
 lit2 x (MkBase b geq2 lte16) = go [] x
-  where go : List Char -> Bits64 -> String
-        go cs 0 = pack cs
-        go cs v =
-          let Element d ltb = rmod v b
-           in go (hexChar d :: cs) (assert_smaller v $ sdiv v b)
+
+  where
+    go : List Char -> Bits64 -> String
+    go cs 0 = pack cs
+    go cs v =
+      let Element d ltb := rmod v b
+       in go (hexChar d :: cs) (assert_smaller v $ sdiv v b)
 ```
 
 That looks pretty nice. The only ugly (and unsafe!) piece is the
@@ -257,14 +263,16 @@ Here is how to do this for `Bits64` and `(<)`:
 lit3 : Bits64 -> Base -> String
 lit3 0 _ = "0"
 lit3 x (MkBase b _ _) = go [] x (accessLT x)
-  where go : List Char -> (n : Bits64) -> (0 _ : Accessible (<) n) -> String
-        go cs n (Access rec) = case comp 0 n of
-          LT ngt0 _ _ =>
-            let Element d  _   = n `rmod` b
-                Element n2 ltn = n `rdiv` b
-             in go (hexChar d :: cs) n2 (rec n2 ltn)
-          EQ _    _ _   => pack cs
-          GT _    _ lt0 => void (Not_LT_MinBits64 lt0)
+
+  where
+    go : List Char -> (n : Bits64) -> (0 _ : Accessible (<) n) -> String
+    go cs n (Access rec) = case comp 0 n of
+      LT ngt0 _ _ =>
+        let Element d  _   := n `rmod` b
+            Element n2 ltn := n `rdiv` b
+         in go (hexChar d :: cs) n2 (rec n2 ltn)
+      EQ _    _ _   => pack cs
+      GT _    _ lt0 => void (Not_LT_MinBits64 lt0)
 ```
 
 Note, how we used `comp` to compare the current value against the
@@ -342,5 +350,5 @@ and with different designs to get the best compromise in terms of
 code reuse, type inference, and expressiveness.
 Therefore, this library is still bound to change in breaking ways.
 
-<!-- vi: filetype=idris2
+<!-- vi: filetype=idris2:syntax=markdown
 -->
diff --git a/src/Algebra/Ring.idr b/src/Algebra/Ring.idr
@@ -89,9 +89,10 @@ minusSelfZero =
 
 ||| Law of associativity for subtraction.
 export
-0 plusMinusAssociative :  Ring a
-                       => {k,m,n : a}
-                       -> k + (m - n) === (k + m) - n
+0 plusMinusAssociative :
+     {auto _ : Ring a}
+  -> {k,m,n : a}
+  -> k + (m - n) === (k + m) - n
 plusMinusAssociative =
   Calc $
     |~ k + (m - n)
@@ -101,10 +102,11 @@ plusMinusAssociative =
 
 ||| We can solve equations involving addition.
 export
-0 solvePlusRight :  Ring a
-               => {k,m,n : a}
-               -> k + m === n
-               -> k === n - m
+0 solvePlusRight :
+     {auto _ : Ring a}
+  -> {k,m,n : a}
+  -> k + m === n
+  -> k === n - m
 solvePlusRight prf =
   Calc $
     |~ k
@@ -115,10 +117,11 @@ solvePlusRight prf =
 
 ||| We can solve equations involving addition.
 export
-0 solvePlusLeft :  Ring a
-              => {k,m,n : a}
-              -> k + m === n
-              -> m === n - k
+0 solvePlusLeft :
+     {auto _ : Ring a}
+  -> {k,m,n : a}
+  -> k + m === n
+  -> m === n - k
 solvePlusLeft prf =
   solvePlusRight $ Calc $
     |~ m + k
@@ -150,20 +153,22 @@ plusRightInjective prf =
 ||| From `m + n === 0` follows that `n` is the
 ||| additive inverse of `m`.
 export
-0 solvePlusNegRight :  Ring a
-                    => {m,n : a}
-                    -> m + n === 0
-                    -> n === neg m
+0 solvePlusNegRight :
+     {auto _ : Ring a}
+  -> {m,n : a}
+  -> m + n === 0
+  -> n === neg m
 solvePlusNegRight prf =
   plusRightInjective (trans prf (sym plusNegRightZero))
 
 ||| From `m + n === 0` follows that `m` is the
 ||| additive inverse of `n`.
 export
-0 solvePlusNegLeft :  Ring a
-                   => {m,n : a}
-                   -> m + n === 0
-                   -> m === neg n
+0 solvePlusNegLeft :
+     {auto _ : Ring a}
+  -> {m,n : a}
+  -> m + n === 0
+  -> m === neg n
 solvePlusNegLeft prf =
   solvePlusNegRight $ Calc $
     |~ n + m
@@ -254,10 +259,11 @@ multZeroLeftAbsorbs =
 
 ||| Zero is an absorbing element of multiplication.
 export
-0 multZeroAbsorbs :  Ring a
-                  => {m,n : a}
-                  -> Either (m === 0) (n === 0)
-                  -> m * n === 0
+0 multZeroAbsorbs :
+     {auto _ : Ring a}
+  -> {m,n : a}
+  -> Either (m === 0) (n === 0)
+  -> m * n === 0
 multZeroAbsorbs (Left rfl) =
   Calc $
     |~ m * n
@@ -338,9 +344,10 @@ negMultNeg =
 
 ||| Multiplication is distributive with respect to addition.
 export
-0 rightDistributive :  Ring a
-                    => {k,m,n : a}
-                    -> (m + n) * k === m * k + n * k
+0 rightDistributive :
+     {auto _ : Ring a}
+  -> {k,m,n : a}
+  -> (m + n) * k === m * k + n * k
 rightDistributive =
   Calc $
     |~ (m + n) * k

diff --git a/src/Algebra/Semiring.idr b/src/Algebra/Semiring.idr
@@ -84,10 +84,11 @@ multZeroRightAbsorbs =
 
 ||| Zero is an absorbing element of multiplication.
 export
-multZeroAbsorbs :  Semiring a
-                => (m,n : a)
-                -> Either (m === 0) (n === 0)
-                -> m * n === 0
+multZeroAbsorbs :
+     {auto _ : Semiring a}
+  -> (m,n : a)
+  -> Either (m === 0) (n === 0)
+  -> m * n === 0
 multZeroAbsorbs m n (Left rfl) =
   Calc $
     |~ m * n
@@ -102,9 +103,10 @@ multZeroAbsorbs m n (Right rfl) =
 
 ||| Multiplication is distributive with respect to addition.
 export
-0 rightDistributive :  Semiring a
-                  => {k,m,n : a}
-                  -> (m + n) * k === m * k + n * k
+0 rightDistributive :
+     {auto _ : Semiring a}
+  -> {k,m,n : a}
+  -> (m + n) * k === m * k + n * k
 rightDistributive =
   Calc $
     |~ (m + n) * k

diff --git a/src/Algebra/Solver/CommutativeMonoid.idr b/src/Algebra/Solver/CommutativeMonoid.idr
@@ -75,9 +75,10 @@ eterm (T f p) = f <+> eprod p
 --          Proofs
 --------------------------------------------------------------------------------
 
-0 p1324 :  CommutativeMonoid a
-        => {k,l,m,n : a}
-        -> (k <+> l) <+> (m <+> n) === (k <+> m) <+> (l <+> n)
+0 p1324 :
+     {auto _ : CommutativeMonoid a}
+  -> {k,l,m,n : a}
+  -> (k <+> l) <+> (m <+> n) === (k <+> m) <+> (l <+> n)
 p1324 = Calc $
   |~ (k <+> l) <+> (m <+> n)
   ~~ ((k <+> l) <+> m) <+> n ... appendAssociative
@@ -86,20 +87,22 @@ p1324 = Calc $
   ~~ ((k <+> m) <+> l) <+> n ... cong (<+>n) appendAssociative
   ~~ (k <+> m) <+> (l <+> n) ..< appendAssociative
 
-0 pone :  CommutativeMonoid a
-       => (as : List a)
-       -> eprod {as} Prod.one === Prelude.neutral
+0 pone :
+     {auto _ : CommutativeMonoid a}
+  -> (as : List a)
+  -> eprod {as} Prod.one === Prelude.neutral
 pone []        = Refl
 pone (v :: vs) = Calc $
   |~ neutral <+> eprod {as = vs} one
   ~~ neutral <+> neutral             ... cong (neutral <+>) (pone vs)
   ~~ neutral                         ... appendLeftNeutral
 
 export
-0 pvar :  CommutativeMonoid a
-       => (as : List a)
-       -> (e  : Elem x as)
-       -> eprod (fromVar {as} e) === x
+0 pvar :
+     {auto _ : CommutativeMonoid a}
+  -> (as : List a)
+  -> (e  : Elem x as)
+  -> eprod (fromVar {as} e) === x
 pvar (x :: vs) Here      = Calc $
   |~ (x <+> neutral) <+> eprod {as = vs} one
   ~~ (x <+> neutral) <+> neutral ... cong ((x <+> neutral) <+>) (pone vs)
@@ -114,20 +117,22 @@ pvar (v :: vs) (There y) = Calc $
 pvar [] Here impossible
 pvar [] (There y) impossible
 
-0 ptimes :  CommutativeMonoid a
-         => (m,n : Nat)
-         -> (x : a)
-         -> times m x <+> times n x === times (m + n) x
+0 ptimes :
+     {auto _ : CommutativeMonoid a}
+  -> (m,n : Nat)
+  -> (x : a)
+  -> times m x <+> times n x === times (m + n) x
 ptimes 0     n x = appendLeftNeutral
 ptimes (S k) n x = Calc $
   |~ (x <+> times k x) <+> times n x
   ~~ x <+> (times k x <+> times n x) ..< appendAssociative
   ~~ x <+> times (k + n) x           ... cong (x <+>) (ptimes k n x)
 
 
-0 ppm :  CommutativeMonoid a
-      => (e1,e2 : Prod a as)
-      -> eprod e1 <+> eprod e2 === eprod (mult e1 e2)
+0 ppm :
+     {auto _ : CommutativeMonoid a}
+  -> (e1,e2 : Prod a as)
+  -> eprod e1 <+> eprod e2 === eprod (mult e1 e2)
 ppm []        []        = appendRightNeutral
 ppm {as = v :: vs} (m :: xs) (n :: ys) = Calc $
   |~ (times m v <+> eprod xs) <+> (times n v <+> eprod ys)
@@ -139,17 +144,19 @@ ppm {as = v :: vs} (m :: xs) (n :: ys) = Calc $
      ... cong (<+> eprod (mult xs ys)) (ptimes m n v)
 
 
-0 pappend :  CommutativeMonoid a
-          => (e1,e2 : Term a as)
-          -> eterm e1 <+> eterm e2 === eterm (append e1 e2)
+0 pappend :
+     {auto _ : CommutativeMonoid a}
+  -> (e1,e2 : Term a as)
+  -> eterm e1 <+> eterm e2 === eterm (append e1 e2)
 pappend (T f p) (T g q) = Calc $
   |~ (f <+> eprod p) <+> (g <+> eprod q)
   ~~ (f <+> g) <+> (eprod p <+> eprod q) ... p1324
   ~~ (f <+> g) <+> eprod (mult p q)      ... cong ((f <+> g) <+>) (ppm p q)
 
-0 pnorm :  CommutativeMonoid a
-        => (e : Expr a as)
-        -> eval e === eterm (normalize e)
+0 pnorm :
+     {auto _ : CommutativeMonoid a}
+  -> (e : Expr a as)
+  -> eval e === eterm (normalize e)
 pnorm (Lit x) = Calc $
   |~ x
   ~~ x <+> neutral        ..< appendRightNeutral
@@ -179,11 +186,12 @@ pnorm (Append x y) = Calc $
 --------------------------------------------------------------------------------
 
 export
-0 solve :  CommutativeMonoid a
-        => (as : List a)
-        -> (e1,e2 : Expr a as)
-        -> (prf : normalize e1 === normalize e2)
-        => eval e1 === eval e2
+0 solve :
+     {auto _ : CommutativeMonoid a}
+  -> (as : List a)
+  -> (e1,e2 : Expr a as)
+  -> {auto prf : normalize e1 === normalize e2}
+  -> eval e1 === eval e2
 solve _ e1 e2 = Calc $
   |~ eval e1
   ~~ eterm (normalize e1) ... pnorm e1

diff --git a/src/Algebra/Solver/Monoid.idr b/src/Algebra/Solver/Monoid.idr
@@ -44,9 +44,10 @@ normalize (Append x y) = normalize x ++ normalize y
 --          Proofs
 --------------------------------------------------------------------------------
 
-0 psum :  LMonoid a
-       => (xs,ys : List a)
-       -> esum (xs ++ ys) === esum xs <+> esum ys
+0 psum :
+     {auto _ : LMonoid a}
+  -> (xs,ys : List a)
+  -> esum (xs ++ ys) === esum xs <+> esum ys
 psum []        ys = sym appendLeftNeutral
 psum (x :: xs) ys = Calc $
   |~ x <+> esum (xs ++ ys)
@@ -71,10 +72,11 @@ pnorm (Append x y) = Calc $
 --------------------------------------------------------------------------------
 
 export
-0 solve :  LMonoid a
-        => (e1,e2 : Expr a)
-        -> (prf : normalize e1 === normalize e2)
-        => eval e1 === eval e2
+0 solve :
+     {auto _ : LMonoid a}
+  -> (e1,e2 : Expr a)
+  -> {auto prf : normalize e1 === normalize e2}
+  -> eval e1 === eval e2
 solve e1 e2 = Calc $
   |~ eval e1
   ~~ esum (normalize e1) ... pnorm e1
@@ -88,5 +90,6 @@ solve e1 e2 = Calc $
 0 solverExample : {x,y,z : String}
                 -> x ++ ((y ++ "") ++ z) === ("" ++ x) ++ (y ++ z)
 solverExample =
-  solve (Var x <+> ((Var y <+> Neutral) <+> Var z))
-        ((Neutral <+> Var x) <+> (Var y <+> Var z))
+  solve
+    (Var x <+> ((Var y <+> Neutral) <+> Var z))
+    ((Neutral <+> Var x) <+> (Var y <+> Var z))