mirror of
https://github.com/Smaug123/fsharp-vectors
synced 2025-10-05 03:28:40 +00:00
55 lines
2.3 KiB
Forth
55 lines
2.3 KiB
Forth
namespace Vector.Naturals
|
|
|
|
type Dummy =
|
|
private
|
|
| Dummy
|
|
static member inline singleton () = ()
|
|
|
|
/// Zero, in the Peano encoding of the naturals
|
|
type Z =
|
|
private
|
|
| Z
|
|
|
|
/// Successor, in the Peano encoding of the naturals
|
|
type S<'a> =
|
|
private
|
|
| S
|
|
// Computation rules
|
|
static member inline refine< ^n1, ^n2 when ^n1 : (static member refine : ^n1 -> ^n2)> (_ : S<'n1>) : S<'n2> = Unchecked.defaultof<_>
|
|
|
|
/// Type representing the sum of two naturals
|
|
type Add<'a, 'b> =
|
|
private
|
|
| Add
|
|
// Computation rules
|
|
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<_>
|