/*
Type Traits (TTrait)
Operation Traits (OTrait)
Types (implement TTraits)
Operations on types (implement OTraits)
*/

trait QuotientRemainder<T: Any>:
	proc quotient(a: T, b: T): T
	proc remainder(a: T, b: T): T

induce QuotientRemainder on Self: Any having
						   `+`<Self>: BinOp | Invertible | UniqueIdentity,
						   `<`<Self>: POrder, // NOTE: PartialOrders implement BinOp
						   `==`<Self>: EqRel -> // NOTE: EqRels implement BinOp
	// `let` is a macro that replaces all instances following code's
	// AST with whatever values were defined via alias
	// (it does NOT change scope at all)
	with (
		// define aliases for the inverse of an element as both a
		// prefixed unary operation and a infix binary operation
		preunary `-`(a: Self) -> +.inverse(a) // -a = +(inverse(a))
		binop `-`(a: Self, b: Self) -> a + +.inverse(b) // a - b = a +(inverse(b))
		// define aliases for <= by simply inducing <= from < and = on Self
		binop `<=`(a: Self, b: Self) -> a == b or a < b
	):
		// NOTE: any proc for a trait can be overriden, the standard definitions
		// NOTE: are just the standard "induced" definitions
		
		proc quotient(a: Self, b: Self): Self ->
			var quotient: Integer = 1
			alias delta -> b
			while not (delta <= b):
				delta = delta - b
				quotient++
			return quotient

		// NOTE: assumes a is passed by value not by reference
		proc remainder(a: Self, b: Self): Self ->
			alias delta -> a // compiler alias
			while not (delta <= b):
				delta = delta - b
			return delta

// define the standard induce of Modulo via QuotientRemainder
induce Modulo on T: QuotientRemainder ->
	binop mod(a: T, b: T): T -> T.remainder(a, b)

// NOTE: the Slicable trait allow us to take slices ie `1..5`
type CycGrp<T: Modulo | Slicable having `+`<T>: BinOp|Invertible|UniqueIdentity>: Group<T> ->
	// intrinsic variables
	intrinsic modulus: T
	intrinsic elements : Set<T>

	structure(modulus: T) ->
		self.modulus = modulus
		// the following line is a generalised implementation of `1..(self.modulus-1)`
		self.elements = (self.modulus + +.inverse(self.modulus))..(self.modulus + +.inverse(+.identity))

	// "functors" allow one type to be represented as another type
	// aka functors == typecasts
	functor(value: T) -> value mod self.modulus

	




/* My attempt at formalising rings and fields in Noether
 * NOTE: the following traits are "formed" from a specific structure
 * NOTE: they have properties (`prop`) which are just aliases to 
 * NOTE: the structure that formed them
 */
trait Magma<T: Any> on (SET: Set<T>, ACTION: BinOp<T>) ->
	prop SET -> SET
	prop ACTION -> ACTION
	
trait SemiGroup<T: Any> 
		on (M: Magma<T>) 
		having M#ACTION: Associative ->
	inherit M#SET, M#ACTION

trait Group<T: Any> 
		on (SG: SemiGroup<T>)
		having SG#ACTION: UniqueIdentity | Invertible ->
	inherit SG#SET, SG#ACTION
	
trait Ring<T: Any> 
		on (SET: Set<T>, ADD: BinOp<T>, MUL: BinOp<T>)
		having (SET, ADD) : Group<T>,
			   (SET, MUL) : SemiGroup<T>,
			   (ADD, MUL) : Distributive ->
	prop SET -> SET
	prop ADD -> ADD
	prop MUL -> MUL

/*
 * Notation: (`->` as `return`)
 * x() -> expr 
 * // same as:
 * x():
 *     return expr
 */