From 53a9cd6fa5b3282cb9e33703a0bb7cbe4758680c Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Fri, 8 May 2020 17:56:31 +0100
Subject: [PATCH] Add vector Replicate

---
 Vector.Test/TestVector.fs | 87 +++++++++++++++++++++++++++++++++++++++
 Vector/Arithmetic.fs      | 38 +++++++++++++++--
 Vector/Vector.fs          |  7 ++++
 3 files changed, 128 insertions(+), 4 deletions(-)

diff --git a/Vector.Test/TestVector.fs b/Vector.Test/TestVector.fs
index cd08a5f..210ac9f 100644
--- a/Vector.Test/TestVector.fs
+++ b/Vector.Test/TestVector.fs
@@ -67,3 +67,90 @@ module TestVector =
         |> Vector.cast
         |> Vector.cast
         |> shouldEqual otherTwice
+
+    [<Test>]
+    let ``Vector replication`` () =
+        let v1 = 6 ** 5 ** 3 ** -()
+        let v2 = () ** () ** -()
+
+        let u = Vector.replicate v2 v1
+        let expected = 6 ** 5 ** 3 ** 6 ** 5 ** 3 ** -()
+        u
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> shouldEqual expected
+
+        let v1 = 6 ** 5 ** -()
+        let six = Vector.replicate (() ** () ** () ** -()) (() ** () ** -())
+
+        let u = Vector.replicate six v1
+        let expected =
+            6 ** 5
+            ** 6 ** 5
+            ** 6 ** 5
+            ** 6 ** 5
+            ** 6 ** 5
+            ** 6 ** 5
+            ** -()
+        u
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> Vector.cast
+        |> shouldEqual expected
+
diff --git a/Vector/Arithmetic.fs b/Vector/Arithmetic.fs
index 96a7ba8..246a42f 100644
--- a/Vector/Arithmetic.fs
+++ b/Vector/Arithmetic.fs
@@ -1,5 +1,10 @@
 namespace Vector.Naturals
 
+type Dummy =
+    private
+    | Dummy
+    static member inline singleton () = ()
+
 /// Zero, in the Peano encoding of the naturals
 type Z =
     private
@@ -17,8 +22,33 @@ type Add<'a, 'b> =
     private
     | Add
     // Computation rules
-    static member inline refine (_ : Add<Z, Z>) : Z = Unchecked.defaultof<_>
-    static member inline refine< ^n1, ^n2> (_ : Add< S< ^n1>, S< ^n2>>) : S<S<Add< ^n1, ^n2>>> = Unchecked.defaultof<_>
-    static member inline refine< ^n1, ^n2> (_ : Add< Z, ^n1>) : ^n2 = Unchecked.defaultof<_>
-    static member inline refine< ^n1, ^n2 > (_ : Add< ^n1, Z>) : ^n2 = Unchecked.defaultof<_>
+    static member inline refine< ^n1, ^n2> (_ : Add< S< ^n1>, ^n2>) : S<Add< ^n1, ^n2>> = Unchecked.defaultof<_>
+    //static member inline refine< ^n1, ^n2> (_ : Add< S< ^n1>, S< ^n2>>) : S<S<Add< ^n1, ^n2>>> = Unchecked.defaultof<_>
+    static member inline refine< ^n1> (_ : Add< Z, ^n1>) : ^n1 = Unchecked.defaultof<_>
 
+    // We define a hierarchy of operations, making sure to complete all lower operations before attempting a higher one.
+    // This is how we guarantee there is at most one operation to perform per computation step.
+    static member additionOrHigher () = ()
+
+    static member inline refine< ^n1, ^n2, ^n3 when ^n1 : (static member refine : ^n1 -> ^n3) and ^n1 : (static member additionOrHigher : unit -> unit)>
+        (_ : Add< ^n1, ^n2>) : Add< ^n3, ^n2> = Unchecked.defaultof<_>
+
+
+/// Type representing the product of two naturals
+type Times<'x, 'y> =
+    private
+    | Times
+    // Computation rules
+    static member inline refine< ^c> (_ : Times<Z, ^c>) : Z = Unchecked.defaultof<_>
+    static member inline refine< ^n1, ^n2>
+        (_ : Times<S< ^n1>, ^n2>) : Add< ^n2, Times< ^n1, ^n2>> = Unchecked.defaultof<_>
+    static member inline refine< ^a, ^b, ^c> (_ : Times<Add< ^a, ^b>, ^c>) : Add<Times< ^a, ^c>, Times< ^b, ^c>> = Unchecked.defaultof<_>
+
+    // Multiplication is only to be performed after all the additions below are complete...
+    static member inline additionOrHigher () = ()
+
+    // ... and also after all the multiplications below are complete.
+    static member inline multiplicationOrHigher () = ()
+
+    static member inline refine< ^a, ^b, ^c when ^a : (static member multiplicationOrHigher : unit -> unit) and ^a : (static member refine : ^a -> ^c)>
+        (_ : Times< ^a, ^b>) : Times< ^c, ^b> = Unchecked.defaultof<_>
diff --git a/Vector/Vector.fs b/Vector/Vector.fs
index 03720e1..f691e45 100644
--- a/Vector/Vector.fs
+++ b/Vector/Vector.fs
@@ -60,6 +60,13 @@ module Vector =
     let head<'a, 'n> (Vector v : Vector<'a, S<'n>>) : 'a = List.head v
     let tail<'a, 'n> (Vector v : Vector<'a, S<'n>>) : Vector<'a, 'n> = List.tail v |> Vector
 
+    /// We currently have no way to express an integer literal at the type level, so we use a dummy first argument
+    /// which is a vector of the right length.
+    let replicate<'a, 'x, 'm, 'n> (Vector len : Vector<'x, 'm>) (Vector v : Vector<'a, 'n>) : Vector<'a, Times<'m, 'n>> =
+        List.replicate (List.length len) v
+        |> List.collect id
+        |> Vector
+
     [<RequireQualifiedAccess>]
     module Unsafe =
         let cast<'a, 'n, 'm> (Vector a : Vector<'a, 'n>) : Vector<'a, 'm> = Vector a