add spaces in named/implicit function application (#403)

spidr/src/BayesianOptimization/Acquisition.idr

@@ -62,11 +62,11 @@ expectedImprovement :
   Acquisition 1 features
 expectedImprovement model best at = do
   marginal <- marginalise model at
-  best' <- broadcast {to=[_, 1]} best
+  best' <- broadcast {to = [_, 1]} best
   let pdf = pdf marginal best'
       cdf = cdf marginal best'
-      mean = squeeze !(mean {event=[1]} {dim=1} marginal)
-      variance = squeeze !(variance {event=[1]} marginal)
+      mean = squeeze !(mean {event = [1]} {dim = 1} marginal)
+      variance = squeeze !(variance {event = [1]} marginal)
   (pure best - mean) * cdf + variance * pdf
 
 ||| Build an acquisition function that returns the absolute improvement, expected by the model, in
@@ -76,7 +76,7 @@ expectedImprovementByModel :
   ProbabilisticModel features [1] Gaussian modelType =>
   Reader (DataModel modelType) $ Acquisition 1 features
 expectedImprovementByModel = asks $ \env, at => do
-  best <- squeeze =<< reduce @{Min} [0] !(mean {event=[1]} !(marginalise env.model env.dataset.features))
+  best <- squeeze =<< reduce @{Min} [0] !(mean {event = [1]} !(marginalise env.model env.dataset.features))
   expectedImprovement env.model best at
 
 ||| Build an acquisition function that returns the probability that any given point will take a
@@ -88,7 +88,7 @@ probabilityOfFeasibility :
   ProbabilisticModel features [1] dist modelType =>
   Reader (DataModel modelType) $ Acquisition 1 features
 probabilityOfFeasibility limit =
-  asks $ \env, at => do cdf !(marginalise env.model at) !(broadcast {to=[_, 1]} limit)
+  asks $ \env, at => do cdf !(marginalise env.model at) !(broadcast {to = [_, 1]} limit)
 
 ||| Build an acquisition function that returns the negative of the lower confidence bound of the
 ||| probabilistic model. The variance contribution is weighted by a factor `beta`.
@@ -102,7 +102,7 @@ negativeLowerConfidenceBound :
   Reader (DataModel modelType) $ Acquisition 1 features
 negativeLowerConfidenceBound beta = asks $ \env, at => do
   marginal <- marginalise env.model at
-  squeeze =<< mean {event=[1]} marginal - fromDouble beta * variance {event=[1]} marginal
+  squeeze =<< mean {event = [1]} marginal - fromDouble beta * variance {event = [1]} marginal
 
 ||| Build the expected improvement acquisition function in the context of a constraint on the input
 ||| domain, where points that do not satisfy the constraint do not offer an improvement. The

spidr/src/Compiler/Eval.idr

@@ -194,8 +194,8 @@ interpret xlaBuilder (MkFn params root env) = do
       Asinh      => asinh
       Acosh      => acosh
       Atanh      => atanh
-  interpretE (Argmin {out} axis x) = argMin {outputType=out} !(get x) axis
-  interpretE (Argmax {out} axis x) = argMax {outputType=out} !(get x) axis
+  interpretE (Argmin {out} axis x) = argMin {outputType = out} !(get x) axis
+  interpretE (Argmax {out} axis x) = argMax {outputType = out} !(get x) axis
   interpretE (Select pred true false) = select !(get pred) !(get true) !(get false)
   interpretE (Cond pred fTrue true fFalse false) = do
     subBuilderT <- createSubBuilder xlaBuilder "truthy computation"
@@ -221,11 +221,11 @@ interpret xlaBuilder (MkFn params root env) = do
       ThreeFry
       !(get minval)
       !(get maxval)
-      !(mkShape {dtype=F64} shape)
+      !(mkShape {dtype = F64} shape)
     tuple xlaBuilder [value rngOutput, state rngOutput]
   interpretE (NormalFloatingPoint key initialState shape) = do
     rngOutput <- normalFloatingPointDistribution
-      !(get key) !(get initialState) ThreeFry !(mkShape {dtype=F64} shape)
+      !(get key) !(get initialState) ThreeFry !(mkShape {dtype = F64} shape)
     tuple xlaBuilder [value rngOutput, state rngOutput]
 
 export covering

spidr/src/Compiler/Xla/Client/Lib/Arithmetic.idr

@@ -26,7 +26,7 @@ prim__argMax : GCAnyPtr -> Int -> Int -> PrimIO AnyPtr
 export
 argMax : (HasIO io, Primitive outputType) => XlaOp -> Nat -> io XlaOp
 argMax (MkXlaOp input) axis = do
-  opPtr <- primIO $ prim__argMax input (xlaIdentifier {dtype=outputType}) (cast axis)
+  opPtr <- primIO $ prim__argMax input (xlaIdentifier {dtype = outputType}) (cast axis)
   opPtr <- onCollectAny opPtr XlaOp.delete
   pure (MkXlaOp opPtr)
 
@@ -36,6 +36,6 @@ prim__argMin : GCAnyPtr -> Int -> Int -> PrimIO AnyPtr
 export
 argMin : (HasIO io, Primitive outputType) => XlaOp -> Nat -> io XlaOp
 argMin (MkXlaOp input) axis = do
-  opPtr <- primIO $ prim__argMin input (xlaIdentifier {dtype=outputType}) (cast axis)
+  opPtr <- primIO $ prim__argMin input (xlaIdentifier {dtype = outputType}) (cast axis)
   opPtr <- onCollectAny opPtr XlaOp.delete
   pure (MkXlaOp opPtr)

spidr/src/Data.idr

@@ -41,5 +41,5 @@ record Dataset (0 featureShape, targetShape : Shape) where
 ||| Concatenate two datasets along their leading axis.
 export
 concat : Dataset features targets -> Dataset features targets -> Graph $ Dataset features targets
-concat (MkDataset {s=s} x y) (MkDataset {s=s'} x' y') =
-  [| MkDataset {s=s + S s'} (concat 0 x x') (concat 0 y y') |]
+concat (MkDataset {s = s} x y) (MkDataset {s = s'} x' y') =
+  [| MkDataset {s = s + S s'} (concat 0 x x') (concat 0 y y') |]

spidr/src/Distribution.idr

@@ -38,7 +38,7 @@ interface Distribution (0 dist : (0 event : Shape) -> (0 dim : Nat) -> Type) whe
 ||| The variance of a single random variable.
 export
 variance : {event : _} -> Distribution dist => dist event 1 -> Graph $ Tensor (1 :: event) F64
-variance dist = squeeze {from=(1 :: 1 :: event)} =<< cov dist
+variance dist = squeeze {from = (1 :: 1 :: event)} =<< cov dist
 
 ||| A joint, or multivariate distribution over a tensor of floating point values, where the density
 ||| function and corresponding cumulative density function are known (either analytically or via
@@ -79,13 +79,13 @@ Distribution Gaussian where
 export
 ClosedFormDistribution [1] Gaussian where
   pdf (MkGaussian {d} mean cov) x = do
-    cholCov <- cholesky =<< squeeze {to=[S d, S d]} cov
+    cholCov <- cholesky =<< squeeze {to = [S d, S d]} cov
     tri <- pure cholCov |\ squeeze !(pure x - pure mean)
     let exponent = - pure tri @@ pure tri / 2.0
         covSqrtDet = reduce @{Prod} [0] !(diag cholCov)
         denominator = (fromDouble $ pow (2.0 * pi) (cast (S d) / 2.0)) * covSqrtDet
     (exp !exponent) / denominator
 
-  cdf (MkGaussian {d=S _} _ _) _ = ?multivariate_cdf
-  cdf (MkGaussian {d=0} mean cov) x =
+  cdf (MkGaussian {d = S _} _ _) _ = ?multivariate_cdf
+  cdf (MkGaussian {d = 0} mean cov) x =
     (1.0 + erf !(squeeze !(pure x - pure mean) / (sqrt !(squeeze cov * 2.0)))) / 2.0

spidr/src/Literal.idr

@@ -38,7 +38,7 @@ data Literal : Shape -> Type -> Type where
 
 export
 fromInteger : Integer -> Literal [] Int32
-fromInteger = Scalar . cast {to=Int32}
+fromInteger = Scalar . cast {to = Int32}
 
 export
 fromDouble : Double -> Literal [] Double
@@ -181,8 +181,8 @@ export
     showWithIndent : {shape : _} -> String -> Literal shape a -> String
     showWithIndent _ (Scalar x) = show x
     showWithIndent _ [] = "[]"
-    showWithIndent {shape=[S _]} _ x = show (toList x)
-    showWithIndent {shape=(S d :: dd :: ddd)} indent (x :: xs) =
+    showWithIndent {shape = [S _]} _ x = show (toList x)
+    showWithIndent {shape = (S d :: dd :: ddd)} indent (x :: xs) =
       let indent = " " ++ indent
           first = showWithIndent indent x
           rest = foldMap (\e => ",\n" ++ indent ++ showWithIndent indent e) (toVect xs)

spidr/src/Model/GaussianProcess.idr

@@ -128,4 +128,4 @@ fit optimizer (MkDataset x y) (MkConjugateGPR {p} mkPrior gpParams noise) = do
     where
     %hint
     reflexive : {n : _} -> LTE n n
-    reflexive = Relation.reflexive {ty=Nat}
+    reflexive = Relation.reflexive {ty = Nat}

spidr/src/Model/Kernel.idr

@@ -39,7 +39,7 @@ scaledL2Norm :
   Tensor [n', S d] F64 ->
   Graph $ Tensor [n, n'] F64
 scaledL2Norm len x x' =
-  let xs = broadcast {to=[n, n', S d]} =<< expand 1 x
+  let xs = broadcast {to = [n, n', S d]} =<< expand 1 x
    in reduce @{Sum} [2] =<< ((xs - broadcast !(expand 0 x')) / pure len) ^ fill 2.0
 
 ||| The radial basis function, or squared exponential kernel. This is a stationary kernel with form

spidr/src/Tensor.idr

@@ -196,15 +196,15 @@ export
   min = addTensor $ MinFiniteValue {dtype}
   max = addTensor $ MaxFiniteValue {dtype}
 
-||| Cast the element type. For example, `castDtype (tensor {dtype=S32} [1, -2])` is
-||| `tensor {dtype=F64} [1.0, -2.0]`.
+||| Cast the element type. For example, `castDtype (tensor {dtype = S32} [1, -2])` is
+||| `tensor {dtype = F64} [1.0, -2.0]`.
 export
 castDtype : Primitive.Integral a => Tensor shape a -> Graph $ Tensor shape F64
 castDtype $ MkTensor x = addTensor $ ConvertElementType {dtype = F64} x
 
 ----------------------------- structural operations ----------------------------
 
-||| Reshape a `Tensor`. For example, `reshape {to=[2, 1]} (tensor [3, 4])` is
+||| Reshape a `Tensor`. For example, `reshape {to = [2, 1]} (tensor [3, 4])` is
 ||| `tensor [[3], [4]]`. The output can have a different rank to the input.
 export
 reshape :
@@ -317,7 +317,7 @@ public export
 ||| Slice across all indices along an axis. See `slice` for details.
 public export
 all : {d : _} -> SliceOrIndex d
-all = Slice 0 @{%search} @{reflexive {ty=Nat}} d
+all = Slice 0 @{%search} @{reflexive {ty = Nat}} d
 
 ||| A `MultiSlice shape` is a valid multi-dimensionsal slice into a tensor with shape `shape`.
 ||| See `slice` for details.
@@ -332,10 +332,10 @@ namespace MultiSlice
   public export
   slice : {shape : _} -> MultiSlice shape -> Shape
   slice {shape} [] = shape
-  slice {shape=(_ :: _)} (Slice {size} _ _ :: xs) = size :: slice xs
-  slice {shape=(_ :: _)} (Index _ :: xs) = slice xs
-  slice {shape=(_ :: _)} (DynamicSlice _ size :: xs) = size :: slice xs
-  slice {shape=(_ :: _)} (DynamicIndex _ :: xs) = slice xs
+  slice {shape = (_ :: _)} (Slice {size} _ _ :: xs) = size :: slice xs
+  slice {shape = (_ :: _)} (Index _ :: xs) = slice xs
+  slice {shape = (_ :: _)} (DynamicSlice _ size :: xs) = size :: slice xs
+  slice {shape = (_ :: _)} (DynamicIndex _ :: xs) = slice xs
 
 ||| Slice or index `Tensor` axes. Each axis can be sliced or indexed, and this can be done with
 ||| either static (`Nat`) or dynamic (scalar `U64`) indices.
@@ -453,7 +453,7 @@ slice at $ MkTensor x = do
       stop f {d} _ = f d
 
       size : (Nat -> Nat) -> {d : Nat} -> SliceOrIndex d -> Nat
-      size _ (Slice {size=size'} _ _) = size'
+      size _ (Slice {size = size'} _ _) = size'
       size _ (Index _) = 1
       size _ (DynamicSlice _ size') = size'
       size _ (DynamicIndex _) = 1
@@ -694,7 +694,7 @@ broadcast $ MkTensor {shape = _} x = addTensor $ Broadcast {dtype} from to x
 ||| ```
 export
 fill : PrimitiveRW dtype ty => {shape : _} -> ty -> Graph $ Tensor shape dtype
-fill x = broadcast {shapesOK=scalarToAnyOk shape} !(tensor (Scalar x))
+fill x = broadcast {shapesOK = scalarToAnyOk shape} !(tensor (Scalar x))
 
 ||| A constant where values increment from zero along the specified `axis`. For example,
 ||| ```
@@ -1189,8 +1189,8 @@ namespace Scalarwise
         Graph (Tensor (d :: ds) dtype) ->
         Graph (Tensor (d :: ds) dtype)
   l * r = do
-    MkTensor {shape=_ :: _} _ <- r
-    broadcast {shapesOK=scalarToAnyOk (d :: ds)} !l * r
+    MkTensor {shape = _ :: _} _ <- r
+    broadcast {shapesOK = scalarToAnyOk (d :: ds)} !l * r
 
 namespace Semigroup
   export
@@ -1227,7 +1227,7 @@ namespace Scalarwise
         Graph (Tensor (d :: ds) dtype)
   l / r = do
     MkTensor {shape = _ :: _} _ <- l
-    l / broadcast {shapesOK=scalarToAnyOk (d :: ds)} !r
+    l / broadcast {shapesOK = scalarToAnyOk (d :: ds)} !r
 
 ||| Element-wise division of natural numbers. For example,
 ||| `div !(tensor [Scalar 13, Scalar 8]) [3, 4]` is `tensor [4, 2]`.
@@ -1449,7 +1449,7 @@ export
 argmin : Primitive.Ord dtype => Tensor [S n] dtype -> Graph $ Tensor [] U64
 argmin x = do
   MkTensor x <- highlightNan True x
-  addTensor $ Argmin {out=U64} 0 x
+  addTensor $ Argmin {out = U64} 0 x
 
 ||| The first index of the maximum value in a vector. For example,
 ||| `argmax !(tensor [-1, 3, -2, -2, 3])` is `tensor 1`. If the vector contains NaN values,
@@ -1458,7 +1458,7 @@ export
 argmax : Primitive.Ord dtype => Tensor [S n] dtype -> Graph $ Tensor [] U64
 argmax x = do
   MkTensor x <- highlightNan False x
-  addTensor $ Argmax {out=U64} 0 x
+  addTensor $ Argmax {out = U64} 0 x
 
 ---------------------------- other ----------------------------------
 
@@ -1525,7 +1525,7 @@ namespace Vector
   export
   (\|) : Graph (Tensor [m, m] F64) -> Graph (Tensor [m] F64) -> Graph (Tensor [m] F64)
   a \| b = do
-    MkTensor {shape=[_]} i <- b
+    MkTensor {shape = [_]} i <- b
     squeeze !(a \| expand 1 (MkTensor {shape = [m]} i))
 
 ||| Sum the elements along the diagonal of the input. For example,
@@ -1536,7 +1536,7 @@ trace : (Primitive.Num dtype, Prelude.Num a) =>
         Tensor [S n, S n] dtype ->
         Graph (Tensor [] dtype)
 trace x with (x)
-  _ | MkTensor {shape=[_, _]} _ = reduce @{Sum} [0, 1] !(Tensor.(*) (pure x) identity)
+  _ | MkTensor {shape = [_, _]} _ = reduce @{Sum} [0, 1] !(Tensor.(*) (pure x) identity)
 
 ||| A `Rand a` produces a pseudo-random value of type `a` from a `Tensor [1] U64` state.
 ||| The state is updated each time a new value is generated.