From d98c1b43036258eeb410c3b0db6e1b1606c346bc Mon Sep 17 00:00:00 2001 From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com> Date: Wed, 12 Jun 2024 22:48:49 +0100 Subject: [PATCH] add spaces in named/implicit function application (#403) --- .../src/BayesianOptimization/Acquisition.idr | 12 +- spidr/src/Compiler/Eval.idr | 8 +- .../Compiler/Xla/Client/Lib/Arithmetic.idr | 4 +- spidr/src/Data.idr | 4 +- spidr/src/Distribution.idr | 8 +- spidr/src/Literal.idr | 6 +- spidr/src/Model/GaussianProcess.idr | 2 +- spidr/src/Model/Kernel.idr | 2 +- spidr/src/Tensor.idr | 34 ++--- test/runner/Unit/TestTensor.idr | 64 ++++----- test/runner/Unit/TestTensor/Elementwise.idr | 44 +++--- test/runner/Unit/TestTensor/HigherOrder.idr | 66 ++++----- test/runner/Unit/TestTensor/Sampling.idr | 14 +- test/runner/Unit/TestTensor/Slice.idr | 40 +++--- test/runner/Unit/TestTensor/Structure.idr | 126 +++++++++--------- test/runner/Unit/TestUtil.idr | 6 +- tutorials/BayesianOptimizationDesign.md | 4 +- 17 files changed, 222 insertions(+), 222 deletions(-) diff --git a/spidr/src/BayesianOptimization/Acquisition.idr b/spidr/src/BayesianOptimization/Acquisition.idr index a910240f1..0ecc86ade 100644 --- a/spidr/src/BayesianOptimization/Acquisition.idr +++ b/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 diff --git a/spidr/src/Compiler/Eval.idr b/spidr/src/Compiler/Eval.idr index fe1dd12ff..3b98b4716 100644 --- a/spidr/src/Compiler/Eval.idr +++ b/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 diff --git a/spidr/src/Compiler/Xla/Client/Lib/Arithmetic.idr b/spidr/src/Compiler/Xla/Client/Lib/Arithmetic.idr index 7452f2981..ae2cb6c6b 100644 --- a/spidr/src/Compiler/Xla/Client/Lib/Arithmetic.idr +++ b/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) diff --git a/spidr/src/Data.idr b/spidr/src/Data.idr index e64f38a27..a976ff892 100644 --- a/spidr/src/Data.idr +++ b/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') |] diff --git a/spidr/src/Distribution.idr b/spidr/src/Distribution.idr index 49a69f14a..25a087214 100644 --- a/spidr/src/Distribution.idr +++ b/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 diff --git a/spidr/src/Literal.idr b/spidr/src/Literal.idr index 4838b7f82..9b027e584 100644 --- a/spidr/src/Literal.idr +++ b/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) diff --git a/spidr/src/Model/GaussianProcess.idr b/spidr/src/Model/GaussianProcess.idr index 26f4aa42b..b6e3c9810 100644 --- a/spidr/src/Model/GaussianProcess.idr +++ b/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} diff --git a/spidr/src/Model/Kernel.idr b/spidr/src/Model/Kernel.idr index 40bc1ce73..60e9a7e40 100644 --- a/spidr/src/Model/Kernel.idr +++ b/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 diff --git a/spidr/src/Tensor.idr b/spidr/src/Tensor.idr index 66e670fdb..0a837f279 100644 --- a/spidr/src/Tensor.idr +++ b/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. diff --git a/test/runner/Unit/TestTensor.idr b/test/runner/Unit/TestTensor.idr index ab3f1174b..7dc8343d1 100644 --- a/test/runner/Unit/TestTensor.idr +++ b/test/runner/Unit/TestTensor.idr @@ -40,19 +40,19 @@ tensorThenEval @{device} = withTests 20 . property $ do shape <- forAll shapes x <- forAll (literal shape doubles) - x ==~ unsafePerformIO (eval device (tensor {dtype=F64} x)) + x ==~ unsafePerformIO (eval device (tensor {dtype = F64} x)) x <- forAll (literal shape int32s) - x === unsafePerformIO (eval device (tensor {dtype=S32} x)) + x === unsafePerformIO (eval device (tensor {dtype = S32} x)) x <- forAll (literal shape nats) - x === unsafePerformIO (eval device (tensor {dtype=U32} x)) + x === unsafePerformIO (eval device (tensor {dtype = U32} x)) x <- forAll (literal shape nats) - x === unsafePerformIO (eval device (tensor {dtype=U64} x)) + x === unsafePerformIO (eval device (tensor {dtype = U64} x)) x <- forAll (literal shape bool) - x === unsafePerformIO (eval device (tensor {dtype=PRED} x)) + x === unsafePerformIO (eval device (tensor {dtype = PRED} x)) partial evalTuple : Device => Property @@ -160,8 +160,8 @@ boundedNonFinite = fixedProperty $ do Types.min @{NonFinite} ===# tensor (-inf) Types.max @{NonFinite} ===# tensor inf - unsafeEval {dtype=F64} (Types.min @{NonFinite}) === -inf - unsafeEval {dtype=F64} (Types.max @{NonFinite}) === inf + unsafeEval {dtype = F64} (Types.min @{NonFinite}) === -inf + unsafeEval {dtype = F64} (Types.max @{NonFinite}) === inf partial iota : Device => Property @@ -229,7 +229,7 @@ show = fixedProperty $ do constant, shape=[], metadata={:0} """ - let x = tensor {dtype=F64} [1.3, 2.0, -0.4] + let x = tensor {dtype = F64} [1.3, 2.0, -0.4] show x === "constant, shape=[3], metadata={:0}" partial @@ -238,29 +238,29 @@ cast = property $ do shape <- forAll shapes lit <- forAll (literal shape nats) - let x : Graph $ Tensor shape F64 = (do castDtype !(tensor {dtype=U32} lit)) - x ===# tensor (map (cast {to=Double}) lit) + let x : Graph $ Tensor shape F64 = (do castDtype !(tensor {dtype = U32} lit)) + x ===# tensor (map (cast {to = Double}) lit) lit <- forAll (literal shape nats) - let x : Graph $ Tensor shape F64 = (do castDtype !(tensor {dtype=U64} lit)) - x ===# tensor (map (cast {to=Double}) lit) + let x : Graph $ Tensor shape F64 = (do castDtype !(tensor {dtype = U64} lit)) + x ===# tensor (map (cast {to = Double}) lit) lit <- forAll (literal shape int32s) - let x : Graph $ Tensor shape F64 = (do castDtype !(tensor {dtype=S32} lit)) - x ===# tensor (map (cast {to=Double}) lit) + let x : Graph $ Tensor shape F64 = (do castDtype !(tensor {dtype = S32} lit)) + x ===# tensor (map (cast {to = Double}) lit) partial identity : Device => Property identity = fixedProperty $ do - identity ===# tensor {dtype=S32} [] - identity ===# tensor {dtype=S32} [[1]] - identity ===# tensor {dtype=S32} [[1, 0], [0, 1]] - identity ===# tensor {dtype=S32} [[1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 1, 0], [0, 0, 0, 1]] - - identity ===# tensor {dtype=F64} [] - identity ===# tensor {dtype=F64} [[1.0]] - identity ===# tensor {dtype=F64} [[1.0, 0.0], [0.0, 1.0]] - identity ===# tensor {dtype=F64} [ + identity ===# tensor {dtype = S32} [] + identity ===# tensor {dtype = S32} [[1]] + identity ===# tensor {dtype = S32} [[1, 0], [0, 1]] + identity ===# tensor {dtype = S32} [[1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 1, 0], [0, 0, 0, 1]] + + identity ===# tensor {dtype = F64} [] + identity ===# tensor {dtype = F64} [[1.0]] + identity ===# tensor {dtype = F64} [[1.0, 0.0], [0.0, 1.0]] + identity ===# tensor {dtype = F64} [ [1.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0], [0.0, 0.0, 0.0, 1.0] ] @@ -268,20 +268,20 @@ namespace Vector export partial (@@) : Device => Property (@@) = fixedProperty $ do - let l = tensor {dtype=S32} [-2, 0, 1] - r = tensor {dtype=S32} [3, 1, 2] + let l = tensor {dtype = S32} [-2, 0, 1] + r = tensor {dtype = S32} [3, 1, 2] l @@ r ===# -4 namespace Matrix export partial (@@) : Device => Property (@@) = fixedProperty $ do - let l = tensor {dtype=S32} [[-2, 0, 1], [1, 3, 4]] - r = tensor {dtype=S32} [3, 3, -1] + let l = tensor {dtype = S32} [[-2, 0, 1], [1, 3, 4]] + r = tensor {dtype = S32} [3, 3, -1] l @@ r ===# tensor [-7, 8] - let l = tensor {dtype=S32} [[-2, 0, 1], [1, 3, 4]] - r = tensor {dtype=S32} [[3, -1], [3, 2], [-1, -4]] + let l = tensor {dtype = S32} [[-2, 0, 1], [1, 3, 4]] + r = tensor {dtype = S32} [[3, -1], [3, 2], [-1, -4]] l @@ r ===# tensor [[ -7, -2], [ 8, -11]] partial @@ -360,13 +360,13 @@ argmax = property $ do partial select : Device => Property select = fixedProperty $ do - let onTrue = tensor {dtype=S32} 1 + let onTrue = tensor {dtype = S32} 1 onFalse = tensor 0 (do select !(tensor True) !onTrue !onFalse) ===# onTrue (do select !(tensor False) !onTrue !onFalse) ===# onFalse let pred = tensor [[False, True, True], [True, False, False]] - onTrue = tensor {dtype=S32} [[0, 1, 2], [3, 4, 5]] + onTrue = tensor {dtype = S32} [[0, 1, 2], [3, 4, 5]] onFalse = tensor [[6, 7, 8], [9, 10, 11]] expected = tensor [[6, 1, 2], [3, 10, 11]] (do select !pred !onTrue !onFalse) ===# expected @@ -443,7 +443,7 @@ triangularSolveIgnoresOppositeElems = fixedProperty $ do partial trace : Device => Property trace = fixedProperty $ do - let x = tensor {dtype=S32} [[-1, 5], [1, 4]] + let x = tensor {dtype = S32} [[-1, 5], [1, 4]] (do trace !x) ===# 3 export partial diff --git a/test/runner/Unit/TestTensor/Elementwise.idr b/test/runner/Unit/TestTensor/Elementwise.idr index 4be08f896..22d1eb3fc 100644 --- a/test/runner/Unit/TestTensor/Elementwise.idr +++ b/test/runner/Unit/TestTensor/Elementwise.idr @@ -75,8 +75,8 @@ namespace S32 shape <- forAll shapes let int32s = literal shape int32s [x, y] <- forAll (np [int32s, int32s]) - let x' = tensor {dtype=S32} x - y' = tensor {dtype=S32} y + let x' = tensor {dtype = S32} x + y' = tensor {dtype = S32} y [| fInt x y |] === unsafeEval (fTensor x' y') partial @@ -115,8 +115,8 @@ namespace F64 shape <- forAll shapes let doubles = literal shape doubles [x, y] <- forAll (np [doubles, doubles]) - let x' = tensor {dtype=F64} x - y' = tensor {dtype=F64} y + let x' = tensor {dtype = F64} x + y' = tensor {dtype = F64} y [| fDouble x y |] ==~ unsafeEval (fTensor x' y') namespace PRED @@ -130,8 +130,8 @@ namespace PRED shape <- forAll shapes let bools = literal shape bool [x, y] <- forAll (np [bools, bools]) - let x' = tensor {dtype=PRED} x - y' = tensor {dtype=PRED} y + let x' = tensor {dtype = PRED} x + y' = tensor {dtype = PRED} y [| fBool x y |] === unsafeEval (fTensor x' y') partial @@ -142,8 +142,8 @@ scalarMultiplication = property $ do [] => success (d :: ds) => do [lit, scalar] <- forAll (np [literal (d :: ds) doubles, doubles]) - let lit' = tensor {dtype=F64} lit - scalar' = tensor {dtype=F64} (Scalar scalar) + let lit' = tensor {dtype = F64} lit + scalar' = tensor {dtype = F64} (Scalar scalar) map (scalar *) lit ==~ unsafeEval (scalar' * lit') partial @@ -154,8 +154,8 @@ scalarDivision = property $ do [] => success (d :: ds) => do [lit, scalar] <- forAll (np [literal (d :: ds) doubles, doubles]) - let lit' = tensor {dtype=F64} lit - scalar' = tensor {dtype=F64} (Scalar scalar) + let lit' = tensor {dtype = F64} lit + scalar' = tensor {dtype = F64} (Scalar scalar) map (/ scalar) lit ==~ unsafeEval (lit' / scalar') namespace S32 @@ -169,8 +169,8 @@ namespace S32 shape <- forAll shapes let int32s = literal shape int32s [x, y] <- forAll (np [int32s, int32s]) - let x' = tensor {dtype=S32} x - y' = tensor {dtype=S32} y + let x' = tensor {dtype = S32} x + y' = tensor {dtype = S32} y [| fInt x y |] === unsafeEval (fTensor x' y') namespace F64 @@ -184,8 +184,8 @@ namespace F64 shape <- forAll shapes let doubles = literal shape doubles [x, y] <- forAll (np [doubles, doubles]) - let x' = tensor {dtype=F64} x - y' = tensor {dtype=F64} y + let x' = tensor {dtype = F64} x + y' = tensor {dtype = F64} y [| fDouble x y |] === unsafeEval (fTensor x' y') namespace PRED @@ -203,14 +203,14 @@ neutralIsNeutralForSum = property $ do shape <- forAll shapes x <- forAll (literal shape doubles) - let x' = tensor {dtype=F64} x + let x' = tensor {dtype = F64} x right = (<+>) @{Sum} x' (neutral @{Sum}) left = (<+>) @{Sum} (neutral @{Sum}) x' unsafeEval right ==~ x unsafeEval left ==~ x x <- forAll (literal shape int32s) - let x' = tensor {dtype=S32} x + let x' = tensor {dtype = S32} x right = (<+>) @{Sum} x' (neutral @{Sum}) left = (<+>) @{Sum} (neutral @{Sum}) x' unsafeEval right === x @@ -222,14 +222,14 @@ neutralIsNeutralForProd = property $ do shape <- forAll shapes x <- forAll (literal shape doubles) - let x' = tensor {dtype=F64} x + let x' = tensor {dtype = F64} x right = (<+>) @{Prod} x' (neutral @{Prod}) left = (<+>) @{Prod} (neutral @{Prod}) x' unsafeEval right ==~ x unsafeEval left ==~ x x <- forAll (literal shape int32s) - let x' = tensor {dtype=S32} x + let x' = tensor {dtype = S32} x right = (<+>) @{Prod} x' (neutral @{Prod}) left = (<+>) @{Prod} (neutral @{Prod}) x' unsafeEval right === x @@ -240,7 +240,7 @@ neutralIsNeutralForAny : Device => Property neutralIsNeutralForAny = property $ do shape <- forAll shapes x <- forAll (literal shape bool) - let x' = tensor {dtype=PRED} x + let x' = tensor {dtype = PRED} x right = (<+>) @{Any} x' (neutral @{Monoid.Any}) left = (<+>) @{Any} (neutral @{Monoid.Any}) x' unsafeEval right === x @@ -251,7 +251,7 @@ neutralIsNeutralForAll : Device => Property neutralIsNeutralForAll = property $ do shape <- forAll shapes x <- forAll (literal shape bool) - let x' = tensor {dtype=PRED} x + let x' = tensor {dtype = PRED} x right = (<+>) @{All} x' (neutral @{Monoid.All}) left = (<+>) @{All} (neutral @{Monoid.All}) x' unsafeEval right === x @@ -262,7 +262,7 @@ neutralIsNeutralForMin : Device => Property neutralIsNeutralForMin = property $ do shape <- forAll shapes x <- forAll (literal shape doublesWithoutNan) - let x' = tensor {dtype=F64} x + let x' = tensor {dtype = F64} x right = (<+>) @{Min} x' (neutral @{Min}) left = (<+>) @{Min} (neutral @{Min}) x' unsafeEval right ==~ x @@ -273,7 +273,7 @@ neutralIsNeutralForMax : Device => Property neutralIsNeutralForMax = property $ do shape <- forAll shapes x <- forAll (literal shape doublesWithoutNan) - let x' = tensor {dtype=F64} x + let x' = tensor {dtype = F64} x right = (<+>) @{Max} x' (neutral @{Max}) left = (<+>) @{Max} (neutral @{Max}) x' unsafeEval right ==~ x diff --git a/test/runner/Unit/TestTensor/HigherOrder.idr b/test/runner/Unit/TestTensor/HigherOrder.idr index a35a5f5ae..c43935619 100644 --- a/test/runner/Unit/TestTensor/HigherOrder.idr +++ b/test/runner/Unit/TestTensor/HigherOrder.idr @@ -36,15 +36,15 @@ mapResult = property $ do map (1.0 /) x ==~ unsafeEval (do map (\x => 1.0 / pure x) !x') x <- forAll (literal shape int32s) - let x' = tensor {dtype=S32} x + let x' = tensor {dtype = S32} x map (+ 1) x === unsafeEval (do map (\x => pure x + 1) !x') partial mapNonTrivial : Device => Property mapNonTrivial = fixedProperty $ do - (do map {a=S32} (\x => pure x + pure x) !1) ===# 2 - (do map {a=S32} (\_ => 2) !1) ===# 2 - (do map {a=S32} (map (\x => pure x + 1)) !1) ===# 2 + (do map {a = S32} (\x => pure x + pure x) !1) ===# 2 + (do map {a = S32} (\_ => 2) !1) ===# 2 + (do map {a = S32} (map (\x => pure x + 1)) !1) ===# 2 partial map2Result : Device => Property @@ -53,15 +53,15 @@ map2Result = fixedProperty $ do let int32s = literal shape int32s [x, y] <- forAll (np [int32s, int32s]) - let x' = tensor {dtype=S32} x - y' = tensor {dtype=S32} y + let x' = tensor {dtype = S32} x + y' = tensor {dtype = S32} y [| x + y |] === unsafeEval (do map2 (\x, y => pure x + pure y) !x' !y') shape <- forAll shapes let doubles = literal shape doubles [x, y] <- forAll (np [doubles, doubles]) - let x' = tensor {dtype=F64} x - y' = tensor {dtype=F64} y + let x' = tensor {dtype = F64} x + y' = tensor {dtype = F64} y [| x + y |] ==~ unsafeEval (do map2 (\x, y => pure x + pure y) !x' !y') partial @@ -73,28 +73,28 @@ map2ResultWithReusedFnArgs = fixedProperty $ do partial reduce : Device => Property reduce = fixedProperty $ do - let x = tensor {dtype=S32} [[1, 2, 3], [-1, -2, -3]] + let x = tensor {dtype = S32} [[1, 2, 3], [-1, -2, -3]] (do reduce @{Sum} [1] !x) ===# tensor [6, -6] - let x = tensor {dtype=S32} [[1, 2, 3], [-2, -3, -4]] + let x = tensor {dtype = S32} [[1, 2, 3], [-2, -3, -4]] (do reduce @{Sum} [0, 1] !x) ===# tensor (-3) - let x = tensor {dtype=S32} [[[1], [2], [3]], [[-2], [-3], [-4]]] + let x = tensor {dtype = S32} [[[1], [2], [3]], [[-2], [-3], [-4]]] (do reduce @{Sum} [0, 1] !x) ===# tensor [-3] - let x = tensor {dtype=S32} [[[1, 2, 3]], [[-2, -3, -4]]] + let x = tensor {dtype = S32} [[[1, 2, 3]], [[-2, -3, -4]]] (do reduce @{Sum} [0, 2] !x) ===# tensor [-3] - let x = tensor {dtype=S32} [[[1, 2, 3], [-2, -3, -4]]] + let x = tensor {dtype = S32} [[[1, 2, 3], [-2, -3, -4]]] (do reduce @{Sum} [1, 2] !x) ===# tensor [-3] - let x = tensor {dtype=S32} [[[1, 2, 3], [4, 5, 6]], [[-2, -3, -4], [-6, -7, -8]]] + let x = tensor {dtype = S32} [[[1, 2, 3], [4, 5, 6]], [[-2, -3, -4], [-6, -7, -8]]] (do reduce @{Sum} [0, 2] !x) ===# tensor [-3, -6] - let x = tensor {dtype=S32} [[1, 2, 3], [-1, -2, -3]] + let x = tensor {dtype = S32} [[1, 2, 3], [-1, -2, -3]] (do reduce @{Sum} [0] !x) ===# tensor [0, 0, 0] - let x = tensor {dtype=PRED} [[True, False, True], [True, False, False]] + let x = tensor {dtype = PRED} [[True, False, True], [True, False, False]] (do reduce @{All} [1] !x) ===# tensor [False, False] partial @@ -105,7 +105,7 @@ sort = withTests 20 . property $ do ddd <- forAll dims x <- forAll (literal [S d] int32s) - let x = tensor {dtype=S32} x + let x = tensor {dtype = S32} x let sorted = (do sort (<) 0 !x) init = (do slice [0.to d] !sorted) @@ -113,7 +113,7 @@ sort = withTests 20 . property $ do diff (unsafeEval init) (\x, y => all [| x <= y |]) (unsafeEval tail) x <- forAll (literal [S d, S dd] int32s) - let x = tensor {dtype=S32} x + let x = tensor {dtype = S32} x let sorted = (do sort (<) 0 !x) init = (do slice [0.to d] !sorted) @@ -126,7 +126,7 @@ sort = withTests 20 . property $ do diff (unsafeEval init) (\x, y => all [| x <= y |]) (unsafeEval tail) x <- forAll (literal [S d, S dd, S ddd] int32s) - let x = tensor {dtype=S32} x + let x = tensor {dtype = S32} x let sorted = (do sort (<) 0 !x) init = (do slice [0.to d] !sorted) @@ -146,59 +146,59 @@ sort = withTests 20 . property $ do where %hint lteSucc : {n : _} -> LTE n (S n) - lteSucc = lteSuccRight (reflexive {ty=Nat}) + lteSucc = lteSuccRight (reflexive {ty = Nat}) %hint reflex : {n : _} -> LTE n n - reflex = reflexive {ty=Nat} + reflex = reflexive {ty = Nat} partial sortWithEmptyAxis : Device => Property sortWithEmptyAxis = fixedProperty $ do - let x = tensor {shape=[0, 2, 3]} {dtype=S32} [] + let x = tensor {shape = [0, 2, 3]} {dtype = S32} [] (do sort (<) 0 !x) ===# x - let x = tensor {shape=[0, 2, 3]} {dtype=S32} [] + let x = tensor {shape = [0, 2, 3]} {dtype = S32} [] (do sort (<) 1 !x) ===# x - let x = tensor {shape=[2, 0, 3]} {dtype=S32} [[], []] + let x = tensor {shape = [2, 0, 3]} {dtype = S32} [[], []] (do sort (<) 0 !x) ===# x - let x = tensor {shape=[2, 0, 3]} {dtype=S32} [[], []] + let x = tensor {shape = [2, 0, 3]} {dtype = S32} [[], []] (do sort (<) 1 !x) ===# x partial sortWithRepeatedElements : Device => Property sortWithRepeatedElements = fixedProperty $ do - let x = tensor {dtype=S32} [1, 3, 4, 3, 2] + let x = tensor {dtype = S32} [1, 3, 4, 3, 2] (do sort (<) 0 !x) ===# tensor [1, 2, 3, 3, 4] - let x = tensor {dtype=S32} [[1, 4, 4], [3, 2, 5]] + let x = tensor {dtype = S32} [[1, 4, 4], [3, 2, 5]] (do sort (<) 0 !x) ===# tensor [[1, 2, 4], [3, 4, 5]] (do sort (<) 1 !x) ===# tensor [[1, 4, 4], [2, 3, 5]] partial condResultTrivialUsage : Device => Property condResultTrivialUsage = fixedProperty $ do - let x = tensor {dtype=S32} 0 + let x = tensor {dtype = S32} 0 (do cond !(tensor True) (\x => pure x + 1) !x (\x => pure x - 1) !x) ===# 1 - let x = tensor {dtype=S32} 0 + let x = tensor {dtype = S32} 0 (do cond !(tensor False) (\x => pure x + 1) !x (\x => pure x - 1) !x) ===# -1 - let x = tensor {dtype=S32} [2, 3] + let x = tensor {dtype = S32} [2, 3] y = tensor [[6, 7], [8, 9]] (do cond !(tensor True) (\x => tensor 5 * pure x) !x diag !y) ===# tensor [10, 15] - let x = tensor {dtype=S32} [2, 3] + let x = tensor {dtype = S32} [2, 3] y = tensor [[6, 7], [8, 9]] (do cond !(tensor False) (\x => tensor 5 * pure x) !x diag !y) ===# tensor [6, 9] partial condResultWithReusedArgs : Device => Property condResultWithReusedArgs = fixedProperty $ do - let x = tensor {dtype=S32} 1 - y = tensor {dtype=S32} 3 + let x = tensor {dtype = S32} 1 + y = tensor {dtype = S32} 3 f : (Graph a -> Graph a -> Graph a) -> a -> Graph a f g x = g (pure x) (pure x) diff --git a/test/runner/Unit/TestTensor/Sampling.idr b/test/runner/Unit/TestTensor/Sampling.idr index ad2f84a6f..f2a92a862 100644 --- a/test/runner/Unit/TestTensor/Sampling.idr +++ b/test/runner/Unit/TestTensor/Sampling.idr @@ -38,9 +38,9 @@ iidKolmogorovSmirnov samples cdf = do let n : Nat n = product shape - let indices : Graph $ Tensor [n] F64 = castDtype !(tensor {dtype=U64} (range n)) - sampleSize : Graph $ Tensor [] F64 = castDtype !(tensor {dtype=U64} (Scalar n)) - samplesFlat <- reshape {sizesEqual=sym (product1 n)} {to=[n]} !(cdf samples) + let indices : Graph $ Tensor [n] F64 = castDtype !(tensor {dtype = U64} (range n)) + sampleSize : Graph $ Tensor [] F64 = castDtype !(tensor {dtype = U64} (Scalar n)) + samplesFlat <- reshape {sizesEqual = sym (product1 n)} {to = [n]} !(cdf samples) deviationFromCDF <- the (Graph $ Tensor [n] F64) $ indices / sampleSize - sort (<) 0 samplesFlat reduce @{Max} [0] !(abs deviationFromCDF) @@ -113,7 +113,7 @@ uniformSeedIsUpdated = withTests 20 . property $ do key <- tensor key seed <- tensor seed - rng <- uniform key {shape=[10]} !(broadcast bound) !(broadcast bound') + rng <- uniform key {shape = [10]} !(broadcast bound) !(broadcast bound') (seed', sample) <- runStateT seed rng (seed'', sample') <- runStateT seed' rng pure [seed, seed', seed'', sample, sample'] @@ -136,7 +136,7 @@ uniformIsReproducible = withTests 20 . property $ do key <- tensor key seed <- tensor seed - rng <- uniform {shape=[10]} key !(broadcast bound) !(broadcast bound') + rng <- uniform {shape = [10]} key !(broadcast bound) !(broadcast bound') sample <- evalStateT seed rng sample' <- evalStateT seed rng pure [sample, sample'] @@ -171,7 +171,7 @@ normalSeedIsUpdated = withTests 20 . property $ do let [seed, seed', seed'', sample, sample'] = unsafeEval $ do key <- tensor key seed <- tensor seed - let rng = normal key {shape=[10]} + let rng = normal key {shape = [10]} (seed', sample) <- runStateT seed rng (seed'', sample') <- runStateT seed' rng pure [seed, seed', seed'', sample, sample'] @@ -190,7 +190,7 @@ normalIsReproducible = withTests 20 . property $ do key <- tensor key seed <- tensor seed - let rng = normal {shape=[10]} key + let rng = normal {shape = [10]} key sample <- evalStateT seed rng sample' <- evalStateT seed rng pure [sample, sample'] diff --git a/test/runner/Unit/TestTensor/Slice.idr b/test/runner/Unit/TestTensor/Slice.idr index d61d7b643..118f3437e 100644 --- a/test/runner/Unit/TestTensor/Slice.idr +++ b/test/runner/Unit/TestTensor/Slice.idr @@ -30,31 +30,31 @@ namespace MultiSlice (n, idx : Nat) -> (shape : Shape) -> LT idx n -> - MultiSlice.slice {shape=n :: shape} [at idx] === shape + MultiSlice.slice {shape = n :: shape} [at idx] === shape indexFirstDim n idx shape x = Refl sliceFirstDim : (n, from, size : Nat) -> (shape : Shape) -> LTE (from + size) n -> - MultiSlice.slice {shape=n :: shape} [from.to {size} (from + size)] === (size :: shape) + MultiSlice.slice {shape = n :: shape} [from.to {size} (from + size)] === (size :: shape) sliceFirstDim n from size shape x = Refl export slice : Device => Property slice = fixedProperty $ do - slice {shape=[3, 4]} [0.to 3, 0.to 0] === [3, 0] - slice {shape=[3, 4]} [0.to 3, 0.to 1] === [3, 1] - slice {shape=[3, 4]} [0.to 3, 0.to 4] === [3, 4] + slice {shape = [3, 4]} [0.to 3, 0.to 0] === [3, 0] + slice {shape = [3, 4]} [0.to 3, 0.to 1] === [3, 1] + slice {shape = [3, 4]} [0.to 3, 0.to 4] === [3, 4] - slice {shape=[3, 4]} [at 1, 0.to 3] === [3] - slice {shape=[3, 4]} [0.to 2, at 2] === [2] - slice {shape=[3, 4]} [at 1, at 2] === Prelude.Nil + slice {shape = [3, 4]} [at 1, 0.to 3] === [3] + slice {shape = [3, 4]} [0.to 2, at 2] === [2] + slice {shape = [3, 4]} [at 1, at 2] === Prelude.Nil partial sliceStaticIndex : Device => Property sliceStaticIndex = fixedProperty $ do - let x = tensor {dtype=S32} [3, 4, 5] + let x = tensor {dtype = S32} [3, 4, 5] (do slice [at 0] !x) ===# tensor 3 (do slice [at 1] !x) ===# tensor 4 (do slice [at 2] !x) ===# tensor 5 @@ -67,7 +67,7 @@ sliceStaticIndex = fixedProperty $ do partial sliceStaticSlice : Device => Property sliceStaticSlice = fixedProperty $ do - let x = tensor {dtype=S32} [3, 4, 5] + let x = tensor {dtype = S32} [3, 4, 5] (do slice [0.to 0] !x) ===# tensor [] (do slice [0.to 1] !x) ===# tensor [3] (do slice [0.to 2] !x) ===# tensor [3, 4] @@ -81,7 +81,7 @@ sliceStaticSlice = fixedProperty $ do partial sliceStaticMixed : Device => Property sliceStaticMixed = fixedProperty $ do - let x = tensor {dtype=S32} [[3, 4, 5], [6, 7, 8]] + let x = tensor {dtype = S32} [[3, 4, 5], [6, 7, 8]] (do slice [0.to 1] !x) ===# tensor [[3, 4, 5]] (do slice [1.to 1] !x) ===# tensor [] (do slice [all, 2.to 2] !x) ===# tensor [[], []] @@ -104,14 +104,14 @@ u64 = tensor . Scalar partial sliceDynamicIndex : Device => Property sliceDynamicIndex = fixedProperty $ do - let x = tensor {dtype=S32} [3, 4, 5] + let x = tensor {dtype = S32} [3, 4, 5] (do slice [at (!(u64 0))] !x) ===# tensor 3 (do slice [at (!(u64 1))] !x) ===# tensor 4 (do slice [at (!(u64 2))] !x) ===# tensor 5 (do slice [at (!(u64 3))] !x) ===# tensor 5 (do slice [at (!(u64 5))] !x) ===# tensor 5 - let x = tensor {dtype=S32} [[3, 4, 5], [6, 7, 8]] + let x = tensor {dtype = S32} [[3, 4, 5], [6, 7, 8]] (do slice [at (!(u64 0))] !x) ===# tensor [3, 4, 5] (do slice [at (!(u64 1))] !x) ===# tensor [6, 7, 8] (do slice [at (!(u64 2))] !x) ===# tensor [6, 7, 8] @@ -120,7 +120,7 @@ sliceDynamicIndex = fixedProperty $ do partial sliceDynamicSlice : Device => Property sliceDynamicSlice = fixedProperty $ do - let x = tensor {dtype=S32} [3, 4, 5] + let x = tensor {dtype = S32} [3, 4, 5] (do slice [(!(u64 0)).size 0] !x) ===# tensor [] (do slice [(!(u64 0)).size 1] !x) ===# tensor [3] (do slice [(!(u64 0)).size 2] !x) ===# tensor [3, 4] @@ -138,7 +138,7 @@ sliceDynamicSlice = fixedProperty $ do (do slice [(!(u64 5)).size 1] !x) ===# tensor [5] (do slice [(!(u64 5)).size 3] !x) ===# tensor [3, 4, 5] - let x = tensor {dtype=S32} [[3, 4, 5], [6, 7, 8]] + let x = tensor {dtype = S32} [[3, 4, 5], [6, 7, 8]] (do slice [(!(u64 0)).size 1] !x) ===# tensor [[3, 4, 5]] (do slice [(!(u64 1)).size 0] !x) ===# tensor [] (do slice [(!(u64 2)).size 0] !x) ===# tensor [] @@ -149,7 +149,7 @@ sliceDynamicSlice = fixedProperty $ do partial sliceMixed : Device => Property sliceMixed = fixedProperty $ do - let x = tensor {dtype=S32} [[3, 4, 5], [6, 7, 8]] + let x = tensor {dtype = S32} [[3, 4, 5], [6, 7, 8]] (do slice [all, (!(u64 2)).size 0] !x) ===# tensor [[], []] (do slice [all, (!(u64 1)).size 2] !x) ===# tensor [[4, 5], [7, 8]] (do slice [all, (!(u64 3)).size 0] !x) ===# tensor [[], []] @@ -178,10 +178,10 @@ sliceMixed = fixedProperty $ do (do slice [(!(u64 4)).size 1, at 2] !x) ===# tensor [8] let x : Array [60] Int32 = fromList [0..59] - x = (do reshape {to=[2, 5, 3, 2]} !(tensor {shape=[60]} {dtype=S32} $ cast x)) + x = (do reshape {to = [2, 5, 3, 2]} !(tensor {shape = [60]} {dtype = S32} $ cast x)) - let idx = tensor {dtype=U64} 0 - start = tensor {dtype=U64} 1 + let idx = tensor {dtype = U64} 0 + start = tensor {dtype = U64} 1 (do slice [at 1, 2.to 5, (!start).size 2, at !idx] !x) ===# tensor [[44, 46], [50, 52], [56, 58]] index : (idx : Nat) -> {auto 0 inDim : LT idx n} -> Literal [n] a -> Literal [] a @@ -194,7 +194,7 @@ sliceForVariableIndex = property $ do idx <- forAll dims rem <- forAll dims lit <- forAll (literal [idx + S rem] nats) - let x = tensor {dtype=U32} lit + let x = tensor {dtype = U32} lit index @{inDim} idx lit === unsafeEval (do slice [at @{inDim} idx] !x) where diff --git a/test/runner/Unit/TestTensor/Structure.idr b/test/runner/Unit/TestTensor/Structure.idr index fa515e382..3925024a4 100644 --- a/test/runner/Unit/TestTensor/Structure.idr +++ b/test/runner/Unit/TestTensor/Structure.idr @@ -30,69 +30,69 @@ import Utils.Cases partial reshape : Device => Property reshape = fixedProperty $ do - (do reshape !3) ===# tensor {dtype=S32} [3] + (do reshape !3) ===# tensor {dtype = S32} [3] - let x = tensor {dtype=S32} [3, 4, 5] + let x = tensor {dtype = S32} [3, 4, 5] flipped = tensor [[3], [4], [5]] (do reshape !x) ===# flipped - let x = tensor {dtype=S32} [[3, 4, 5], [6, 7, 8]] + let x = tensor {dtype = S32} [[3, 4, 5], [6, 7, 8]] flipped = tensor [[3, 4], [5, 6], [7, 8]] (do reshape !x) ===# flipped - let withExtraDim = tensor {dtype=S32} [[[3, 4, 5]], [[6, 7, 8]]] + let withExtraDim = tensor {dtype = S32} [[[3, 4, 5]], [[6, 7, 8]]] (do reshape !x) ===# withExtraDim - let flattened = tensor {dtype=S32} [3, 4, 5, 6, 7, 8] + let flattened = tensor {dtype = S32} [3, 4, 5, 6, 7, 8] (do reshape !x) ===# flattened partial expand : Device => Property expand = fixedProperty $ do - (do expand 0 !3) ===# tensor {dtype=S32} [3] + (do expand 0 !3) ===# tensor {dtype = S32} [3] - let x = tensor {dtype=S32} [[3, 4, 5], [6, 7, 8]] + let x = tensor {dtype = S32} [[3, 4, 5], [6, 7, 8]] withExtraDim = tensor [[[3, 4, 5]], [[6, 7, 8]]] (do expand 1 !x) ===# withExtraDim partial broadcast : Device => Property broadcast = fixedProperty $ do - (do broadcast {to=[]} {dtype=S32} !7) ===# 7 - (do broadcast {to=[1]} {dtype=S32} !7) ===# tensor [7] - (do broadcast {to=[2, 3]} {dtype=S32} !7) ===# tensor [[7, 7, 7], [7, 7, 7]] - (do broadcast {to=[1, 1, 1]} {dtype=S32} !7) ===# tensor [[[7]]] - (do broadcast {to=[0]} {dtype=S32} !7) ===# tensor [] + (do broadcast {to = []} {dtype = S32} !7) ===# 7 + (do broadcast {to = [1]} {dtype = S32} !7) ===# tensor [7] + (do broadcast {to = [2, 3]} {dtype = S32} !7) ===# tensor [[7, 7, 7], [7, 7, 7]] + (do broadcast {to = [1, 1, 1]} {dtype = S32} !7) ===# tensor [[[7]]] + (do broadcast {to = [0]} {dtype = S32} !7) ===# tensor [] - let x = tensor {dtype=S32} [7] - (do broadcast {to=[1]} !x) ===# tensor [7] + let x = tensor {dtype = S32} [7] + (do broadcast {to = [1]} !x) ===# tensor [7] - let x = tensor {dtype=S32} [7] - (do broadcast {to=[3]} !x) ===# tensor [7, 7, 7] + let x = tensor {dtype = S32} [7] + (do broadcast {to = [3]} !x) ===# tensor [7, 7, 7] - let x = tensor {dtype=S32} [7] - (do broadcast {to=[2, 3]} !x) ===# tensor [[7, 7, 7], [7, 7, 7]] + let x = tensor {dtype = S32} [7] + (do broadcast {to = [2, 3]} !x) ===# tensor [[7, 7, 7], [7, 7, 7]] - let x = tensor {dtype=S32} [5, 7] - (do broadcast {to=[2, 0]} !x) ===# tensor [[], []] + let x = tensor {dtype = S32} [5, 7] + (do broadcast {to = [2, 0]} !x) ===# tensor [[], []] - let x = tensor {dtype=S32} [5, 7] - (do broadcast {to=[3, 2]} !x) ===# tensor [[5, 7], [5, 7], [5, 7]] + let x = tensor {dtype = S32} [5, 7] + (do broadcast {to = [3, 2]} !x) ===# tensor [[5, 7], [5, 7], [5, 7]] - let x = tensor {dtype=S32} [[2, 3, 5], [7, 11, 13]] - (do broadcast {to=[2, 3]} !x) ===# tensor [[2, 3, 5], [7, 11, 13]] + let x = tensor {dtype = S32} [[2, 3, 5], [7, 11, 13]] + (do broadcast {to = [2, 3]} !x) ===# tensor [[2, 3, 5], [7, 11, 13]] - let x = tensor {dtype=S32} [[2, 3, 5], [7, 11, 13]] - (do broadcast {to=[2, 0]} !x) ===# tensor [[], []] + let x = tensor {dtype = S32} [[2, 3, 5], [7, 11, 13]] + (do broadcast {to = [2, 0]} !x) ===# tensor [[], []] - let x = tensor {dtype=S32} [[2, 3, 5], [7, 11, 13]] - (do broadcast {to=[0, 3]} !x) ===# tensor [] + let x = tensor {dtype = S32} [[2, 3, 5], [7, 11, 13]] + (do broadcast {to = [0, 3]} !x) ===# tensor [] - let x = tensor {dtype=S32} [[2, 3, 5], [7, 11, 13]] + let x = tensor {dtype = S32} [[2, 3, 5], [7, 11, 13]] expected = tensor [[[2, 3, 5], [7, 11, 13]], [[2, 3, 5], [7, 11, 13]]] - (do broadcast {to=[2, 2, 3]} !x) ===# expected + (do broadcast {to = [2, 2, 3]} !x) ===# expected - let x = tensor {dtype=S32} [[[2, 3, 5]], [[7, 11, 13]]] + let x = tensor {dtype = S32} [[[2, 3, 5]], [[7, 11, 13]]] expected = tensor [ [ [[2, 3, 5], [2, 3, 5], [2, 3, 5], [2, 3, 5], [2, 3, 5]], @@ -103,45 +103,45 @@ broadcast = fixedProperty $ do [[7, 11, 13], [7, 11, 13], [7, 11, 13], [7, 11, 13], [7, 11, 13]] ] ] - (do broadcast {to=[2, 2, 5, 3]} !x) ===# expected + (do broadcast {to = [2, 2, 5, 3]} !x) ===# expected partial triangle : Device => Property triangle = fixedProperty $ do - let x = tensor {dtype=S32} [] + let x = tensor {dtype = S32} [] (do triangle Upper !x) ===# tensor [] (do triangle Lower !x) ===# tensor [] - let x = tensor {dtype=S32} [[3]] + let x = tensor {dtype = S32} [[3]] (do triangle Upper !x) ===# tensor [[3]] (do triangle Lower !x) ===# tensor [[3]] - let x = tensor {dtype=S32} [[1, 2], [3, 4]] + let x = tensor {dtype = S32} [[1, 2], [3, 4]] (do triangle Upper !x) ===# tensor [[1, 2], [0, 4]] (do triangle Lower !x) ===# tensor [[1, 0], [3, 4]] - let x = tensor {dtype=S32} [[1, 2, 3], [4, 5, 6], [7, 8, 9]] + let x = tensor {dtype = S32} [[1, 2, 3], [4, 5, 6], [7, 8, 9]] (do triangle Upper !x) ===# tensor [[1, 2, 3], [0, 5, 6], [0, 0, 9]] (do triangle Lower !x) ===# tensor [[1, 0, 0], [4, 5, 0], [7, 8, 9]] partial diag : Device => Property diag = fixedProperty $ do - let x = tensor {dtype=S32} [] + let x = tensor {dtype = S32} [] (do diag !x) ===# tensor [] - let x = tensor {dtype=S32} [[3]] + let x = tensor {dtype = S32} [[3]] (do diag !x) ===# tensor [3] - let x = tensor {dtype=S32} [[1, 2], [3, 4]] + let x = tensor {dtype = S32} [[1, 2], [3, 4]] (do diag !x) ===# tensor [1, 4] partial concat : Device => Property concat = fixedProperty $ do - let vector = tensor {dtype=S32} [3, 4, 5] + let vector = tensor {dtype = S32} [3, 4, 5] - let l = tensor {shape=[0]} [] + let l = tensor {shape = [0]} [] r = tensor [3, 4, 5] (do concat 0 !l !r) ===# vector @@ -154,12 +154,12 @@ concat = fixedProperty $ do (do concat 0 !l !r) ===# vector let l = tensor [3, 4, 5] - r = tensor {shape=[0]} [] + r = tensor {shape = [0]} [] (do concat 0 !l !r) ===# vector - let arr = tensor {dtype=S32} [[3, 4, 5], [6, 7, 8]] + let arr = tensor {dtype = S32} [[3, 4, 5], [6, 7, 8]] - let l = tensor {shape=[0, 3]} [] + let l = tensor {shape = [0, 3]} [] r = tensor [[3, 4, 5], [6, 7, 8]] (do concat 0 !l !r) ===# arr @@ -168,10 +168,10 @@ concat = fixedProperty $ do (do concat 0 !l !r) ===# arr let l = tensor [[3, 4, 5], [6, 7, 8]] - r = tensor {shape=[0, 3]} [] + r = tensor {shape = [0, 3]} [] (do concat 0 !l !r) ===# arr - let l = tensor {shape=[2, 0]} [[], []] + let l = tensor {shape = [2, 0]} [[], []] r = tensor [[3, 4, 5], [6, 7, 8]] (do concat 1 !l !r) ===# arr @@ -184,7 +184,7 @@ concat = fixedProperty $ do (do concat 1 !l !r) ===# arr let l = tensor [[3, 4, 5], [6, 7, 8]] - r = tensor {shape=[2, 0]} [[], []] + r = tensor {shape = [2, 0]} [[], []] (do concat 1 !l !r) ===# arr dimBroadcastable : List (a ** b ** DimBroadcastable a b) @@ -223,17 +223,17 @@ broadcastableCannotStackDimensionGtOne (Nest Same) impossible partial squeeze : Device => Property squeeze = fixedProperty $ do - let x = tensor {dtype=S32} [[3]] + let x = tensor {dtype = S32} [[3]] (do squeeze !x) ===# 3 - let x = tensor {dtype=S32} [[[3, 4, 5]], [[6, 7, 8]]] + let x = tensor {dtype = S32} [[[3, 4, 5]], [[6, 7, 8]]] (do squeeze !x) ===# x - let squeezed = tensor {dtype=S32} [[3, 4, 5], [6, 7, 8]] + let squeezed = tensor {dtype = S32} [[3, 4, 5], [6, 7, 8]] (do squeeze !x) ===# squeezed - let x = fill {shape=[1, 3, 1, 1, 2, 5, 1]} {dtype=S32} 0 - (do squeeze !x) ===# fill {shape=[3, 2, 5]} {dtype=S32} 0 + let x = fill {shape = [1, 3, 1, 1, 2, 5, 1]} {dtype = S32} 0 + (do squeeze !x) ===# fill {shape = [3, 2, 5]} {dtype = S32} 0 squeezableCannotRemoveNonOnes : Squeezable [1, 2] [] -> Void squeezableCannotRemoveNonOnes (Nest _) impossible @@ -241,21 +241,21 @@ squeezableCannotRemoveNonOnes (Nest _) impossible partial (.T) : Device => Property (.T) = fixedProperty $ do - (do (tensor {dtype=S32} []).T) ===# tensor [] - (do (tensor {dtype=S32} [[3]]).T) ===# tensor [[3]] + (do (tensor {dtype = S32} []).T) ===# tensor [] + (do (tensor {dtype = S32} [[3]]).T) ===# tensor [[3]] - let x = tensor {dtype=S32} [[1, 2, 3], [4, 5, 6], [7, 8, 9]] + let x = tensor {dtype = S32} [[1, 2, 3], [4, 5, 6], [7, 8, 9]] expected = tensor [[1, 4, 7], [2, 5, 8], [3, 6, 9]] x.T ===# expected partial transpose : Device => Property transpose = fixedProperty $ do - let x = tensor {dtype=S32} [[0, 1], [2, 3]] + let x = tensor {dtype = S32} [[0, 1], [2, 3]] (do transpose [0, 1] !x) ===# x (do transpose [1, 0] !x) ===# tensor [[0, 2], [1, 3]] - let x = tensor {dtype=S32} + let x = tensor {dtype = S32} [[[ 0, 1, 2, 3], [ 4, 5, 6, 7], [ 8, 9, 10, 11]], @@ -282,7 +282,7 @@ transpose = fixedProperty $ do [15, 19, 23]]] let x : Array [120] Int32 = fromList [0..119] - x : Graph $ Tensor [2, 3, 4, 5] S32 = (do reshape !(tensor {shape=[120]} (cast x))) + x : Graph $ Tensor [2, 3, 4, 5] S32 = (do reshape !(tensor {shape = [120]} (cast x))) (do transpose [0, 1, 2, 3] !x) ===# x (do slice [all, at 1, at 0] !(transpose [0, 2, 1, 3] !x)) ===# (do slice [all, at 0, at 1] !x) (do slice [at 2, at 4, at 0, at 1] !(transpose [2, 3, 1, 0] !x)) ===# (do slice [at 1, at 0, at 2, at 4] !x) @@ -290,23 +290,23 @@ transpose = fixedProperty $ do partial reverse : Device => Property reverse = fixedProperty $ do - let x = tensor {shape=[0]} {dtype=S32} [] + let x = tensor {shape = [0]} {dtype = S32} [] (do reverse [0] !x) ===# x - let x = tensor {shape=[0, 3]} {dtype=S32} [] + let x = tensor {shape = [0, 3]} {dtype = S32} [] (do reverse [0] !x) ===# x (do reverse [1] !x) ===# x (do reverse [0, 1] !x) ===# x - let x = tensor {dtype=S32} [-2, 0, 1] + let x = tensor {dtype = S32} [-2, 0, 1] (do reverse [0] !x) ===# tensor [1, 0, -2] - let x = tensor {dtype=S32} [[0, 1, 2], [3, 4, 5]] + let x = tensor {dtype = S32} [[0, 1, 2], [3, 4, 5]] (do reverse [0] !x) ===# tensor [[3, 4, 5], [0, 1, 2]] (do reverse [1] !x) ===# tensor [[2, 1, 0], [5, 4, 3]] (do reverse [0, 1] !x) ===# tensor [[5, 4, 3], [2, 1, 0]] - let x = tensor {dtype=S32} [ + let x = tensor {dtype = S32} [ [[[ 0, 1], [ 2, 3]], [[ 4, 5], [ 6, 7]], [[ 8, 9], [10, 11]]], [[[12, 13], [14, 15]], [[16, 17], [18, 19]], [[20, 21], [22, 23]]] ] diff --git a/test/runner/Unit/TestUtil.idr b/test/runner/Unit/TestUtil.idr index efba47d24..4fd0baf3a 100644 --- a/test/runner/Unit/TestUtil.idr +++ b/test/runner/Unit/TestUtil.idr @@ -33,7 +33,7 @@ namespace Vect export enumerate : Property enumerate = fixedProperty $ do - Vect.enumerate {a=()} [] === [] + Vect.enumerate {a = ()} [] === [] Vect.enumerate [5] === [(0, 5)] Vect.enumerate [5, 7, 9] === [(0, 5), (1, 7), (2, 9)] @@ -48,7 +48,7 @@ namespace List export enumerate : Property enumerate = fixedProperty $ do - List.enumerate {a=()} [] === [] + List.enumerate {a = ()} [] === [] List.enumerate [5] === [(0, 5)] List.enumerate [5, 7, 9] === [(0, 5), (1, 7), (2, 9)] @@ -141,7 +141,7 @@ namespace List repeatedDispersedNotLT (SCons y yltx (SCons x xlty SOne)) = ltNotReflexive x y xlty yltx increasingLT : (x : Nat) -> Sorted LT [x, S x, S (S x)] - increasingLT x = SCons x (reflexive {ty=Nat}) (SCons (S x) (reflexive {ty=Nat}) SOne) + increasingLT x = SCons x (reflexive {ty = Nat}) (SCons (S x) (reflexive {ty = Nat}) SOne) succNotLT : (x : Nat) -> LT (S x) x -> Void succNotLT 0 LTEZero impossible diff --git a/tutorials/BayesianOptimizationDesign.md b/tutorials/BayesianOptimizationDesign.md index cdb300140..849927dd0 100644 --- a/tutorials/BayesianOptimizationDesign.md +++ b/tutorials/BayesianOptimizationDesign.md @@ -87,7 +87,7 @@ optimizer f = in broadcast !(gs $ \x => do f !(broadcast x)) newPoint : Graph $ Tensor [1, 2] F64 -newPoint = optimizer $ \x => squeeze =<< mean {event=[1]} !(marginalise @{Latent} !model x) +newPoint = optimizer $ \x => squeeze =<< mean {event = [1]} !(marginalise @{Latent} !model x) ``` This is a particularly simple example of the standard approach of defining an _acquisition function_ over the input space which quantifies how useful it would be evaluate the objective at a set of points, then finding the points that optimize this acquisition function. We can visualise this: @@ -125,7 +125,7 @@ In the above example, we constructed the acquisition function from our model, th ```idris modelMean : ProbabilisticModel [2] [1] Gaussian m => m -> Acquisition 1 [2] -modelMean model x = squeeze =<< mean {event=[1]} !(marginalise model x) +modelMean model x = squeeze =<< mean {event = [1]} !(marginalise model x) newPoint' : Graph $ Tensor [1, 2] F64 newPoint' = let acquisition = MkReaderT (Id . modelMean @{Latent})