mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
182 lines
6.2 KiB
Plaintext
182 lines
6.2 KiB
Plaintext
// Data.U60
|
|
// ---
|
|
|
|
Data.U60.to_nat (x: Data.U60) : Data.Nat
|
|
Data.U60.to_nat 0 = Data.Nat.zero
|
|
Data.U60.to_nat n = (Data.Nat.succ (Data.U60.to_nat (- n 1)))
|
|
|
|
// Empty
|
|
// -----
|
|
|
|
Empty : Type
|
|
|
|
// Unit
|
|
// ----
|
|
|
|
Unit : Type
|
|
Unit.new : Unit
|
|
|
|
// Data.Bool
|
|
// ----
|
|
|
|
type Data.Bool {
|
|
true : Data.Bool
|
|
false : Data.Bool
|
|
}
|
|
|
|
Data.Bool.not (a: Data.Bool) : Data.Bool
|
|
Data.Bool.not Data.Bool.true = Data.Bool.false
|
|
Data.Bool.not Data.Bool.false = Data.Bool.true
|
|
|
|
Data.Bool.and (a: Data.Bool) (b: Data.Bool) : Data.Bool
|
|
Data.Bool.and Data.Bool.true Data.Bool.true = Data.Bool.true
|
|
Data.Bool.and Data.Bool.true Data.Bool.false = Data.Bool.false
|
|
Data.Bool.and Data.Bool.false Data.Bool.true = Data.Bool.false
|
|
Data.Bool.and Data.Bool.false Data.Bool.false = Data.Bool.false
|
|
|
|
Data.Bool.if <r: Type> (b: Data.Bool) (if_t: r) (if_f: r) : r
|
|
Data.Bool.if r Data.Bool.true if_t if_f = if_t
|
|
Data.Bool.if r Data.Bool.false if_t if_f = if_f
|
|
|
|
Data.Bool.not_not_theorem (a: Data.Bool) : (Equal Data.Bool a (Data.Bool.not (Data.Bool.not a)))
|
|
Data.Bool.not_not_theorem Data.Bool.true = (Equal.refl Data.Bool Data.Bool.true)
|
|
Data.Bool.not_not_theorem Data.Bool.false = (Equal.refl Data.Bool Data.Bool.false)
|
|
|
|
Data.Bool.true_not_false (e: (Equal Data.Bool Data.Bool.true Data.Bool.false)) : Empty
|
|
Data.Bool.true_not_false e = (Equal.rewrite e (x => (Data.Bool.if Type x Unit Empty)) Unit.new)
|
|
|
|
// Data.Nat
|
|
// ---
|
|
|
|
type Data.Nat {
|
|
zero : Data.Nat
|
|
succ (pred: Data.Nat) : Data.Nat
|
|
}
|
|
|
|
Data.Nat.double (x: Data.Nat) : Data.Nat
|
|
Data.Nat.double (Data.Nat.succ x) = (Data.Nat.succ (Data.Nat.succ (Data.Nat.double x)))
|
|
Data.Nat.double (Data.Nat.zero) = (Data.Nat.zero)
|
|
|
|
Data.Nat.add (a: Data.Nat) (b: Data.Nat) : Data.Nat
|
|
Data.Nat.add (Data.Nat.succ a) b = (Data.Nat.succ (Data.Nat.add a b))
|
|
Data.Nat.add Data.Nat.zero b = b
|
|
|
|
Data.Nat.comm.a (a: Data.Nat) : (Equal Data.Nat a (Data.Nat.add a Data.Nat.zero))
|
|
Data.Nat.comm.a Data.Nat.zero = Equal.refl
|
|
Data.Nat.comm.a (Data.Nat.succ a) = (Equal.apply (x => (Data.Nat.succ x)) (Data.Nat.comm.a a))
|
|
|
|
Data.Nat.comm.b (a: Data.Nat) (b: Data.Nat): (Equal Data.Nat (Data.Nat.add a (Data.Nat.succ b)) (Data.Nat.succ (Data.Nat.add a b)))
|
|
Data.Nat.comm.b Data.Nat.zero b = Equal.refl
|
|
Data.Nat.comm.b (Data.Nat.succ a) b = (Equal.apply (x => (Data.Nat.succ x)) (Data.Nat.comm.b a b))
|
|
|
|
Data.Nat.comm (a: Data.Nat) (b: Data.Nat) : (Equal Data.Nat (Data.Nat.add a b) (Data.Nat.add b a))
|
|
Data.Nat.comm Data.Nat.zero b = (Data.Nat.comm.a b)
|
|
Data.Nat.comm (Data.Nat.succ a) b =
|
|
let e0 = (Equal.apply (x => (Data.Nat.succ x)) (Data.Nat.comm a b))
|
|
let e1 = (Equal.mirror (Data.Nat.comm.b b a))
|
|
(Equal.chain e0 e1)
|
|
|
|
Data.Nat.to_u60 (n: Data.Nat) : Data.U60
|
|
Data.Nat.to_u60 Data.Nat.zero = 0
|
|
Data.Nat.to_u60 (Data.Nat.succ n) = (+ 1 (Data.Nat.to_u60 n))
|
|
|
|
Data.Nat.mul (a: Data.Nat) (b: Data.Nat) : Data.Nat
|
|
Data.Nat.mul (Data.Nat.succ a) b = (Data.Nat.add (Data.Nat.mul a b) b) // (a + 1) * b = a*b + b
|
|
Data.Nat.mul Data.Nat.zero b = Data.Nat.zero // 0b = 0
|
|
|
|
Data.Nat.mul.comm.a (x: Data.Nat): (Equal (Data.Nat.mul x Data.Nat.zero) Data.Nat.zero)
|
|
Data.Nat.mul.comm.a Data.Nat.zero = Equal.refl
|
|
Data.Nat.mul.comm.a (Data.Nat.succ x) =
|
|
let e0 = (Data.Nat.mul.comm.a x)
|
|
let e1 = (Equal.apply (y => (Data.Nat.add y Data.Nat.zero)) e0)
|
|
e1
|
|
|
|
// Data.List
|
|
// ----
|
|
|
|
Data.List (a: Type) : Type
|
|
Data.List.nil <a> : (Data.List a)
|
|
Data.List.cons <a> (x: a) (xs: (Data.List a)) : (Data.List a)
|
|
|
|
Data.List.negate (xs: (Data.List Data.Bool)) : (Data.List Data.Bool)
|
|
Data.List.negate (Data.List.cons Data.Bool x xs) = (Data.List.cons Data.Bool (Data.Bool.not x) (Data.List.negate xs))
|
|
Data.List.negate (Data.List.nil Data.Bool) = (Data.List.nil Data.Bool)
|
|
|
|
Data.List.tail <a> (xs: (Data.List a)) : (Data.List a)
|
|
Data.List.tail a (Data.List.cons t x xs) = xs
|
|
|
|
Data.List.map <a> <b> (x: (Data.List a)) (f: (x: a) -> b) : (Data.List b)
|
|
Data.List.map a b (Data.List.nil t) f = Data.List.nil
|
|
Data.List.map a b (Data.List.cons t x xs) f = (Data.List.cons (f x) (Data.List.map xs f))
|
|
|
|
Data.List.concat <a> (xs: (Data.List a)) (ys: (Data.List a)) : (Data.List a)
|
|
Data.List.concat a (Data.List.cons u x xs) ys = (Data.List.cons u x (Data.List.concat a xs ys))
|
|
Data.List.concat a (Data.List.nil u) ys = ys
|
|
|
|
Data.List.flatten <a> (xs: (Data.List (Data.List a))) : (Data.List a)
|
|
Data.List.flatten a (Data.List.cons u x xs) = (Data.List.concat x (Data.List.flatten xs))
|
|
Data.List.flatten a (Data.List.nil u) = Data.List.nil
|
|
|
|
Data.List.bind <a: Type> <b: Type> (xs: (Data.List a)) (f: a -> (Data.List b)) : (Data.List b)
|
|
Data.List.bind a b xs f = (Data.List.flatten b (Data.List.map xs f))
|
|
|
|
Data.List.pure <t: Type> (x: t) : (Data.List t)
|
|
Data.List.pure t x = (Data.List.cons t x (Data.List.nil t))
|
|
|
|
Data.List.range.go (lim: Data.Nat) (res: (Data.List Data.Nat)) : (Data.List Data.Nat)
|
|
Data.List.range.go Data.Nat.zero res = res
|
|
Data.List.range.go (Data.Nat.succ n) res = (Data.List.range.go n (Data.List.cons n res))
|
|
|
|
Data.List.sum (xs: (Data.List Data.Nat)) : Data.Nat
|
|
Data.List.sum (Data.List.nil t) = Data.Nat.zero
|
|
Data.List.sum (Data.List.cons t x xs) = (Data.Nat.add x (Data.List.sum xs))
|
|
|
|
// Equal
|
|
// -----
|
|
|
|
Equal <t> (a: t) (b: t) : Type
|
|
Equal.refl <t> <a: t> : (Equal t a a)
|
|
|
|
Equal.mirror <t> <a: t> <b: t> (e: (Equal t a b)) : (Equal t b a)
|
|
Equal.mirror t a b (Equal.refl u k) = (Equal.refl u k)
|
|
|
|
Equal.apply <t> <u> <a: t> <b: t> (f: t -> t) (e: (Equal t a b)) : (Equal t (f a) (f b))
|
|
Equal.apply t u a b f (Equal.refl v k) = (Equal.refl v (f k))
|
|
|
|
Equal.rewrite <t> <a: t> <b: t> (e: (Equal t a b)) (p: t -> Type) (x: (p a)) : (p b)
|
|
Equal.rewrite t a b (Equal.refl u k) p x = (x :: (p k))
|
|
|
|
Equal.chain <t> <a: t> <b: t> <c: t> (e0: (Equal t a b)) (e1: (Equal t b c)) : (Equal t a c)
|
|
Equal.chain t a b c e0 (Equal.refl u x) = (e0 :: (Equal t a x))
|
|
|
|
// Monad
|
|
// -----
|
|
|
|
Monad (f: Type -> Type) : Type
|
|
Monad.new (f: Type -> Type)
|
|
(pure: (a: Type) -> (x: a) -> (f a))
|
|
(bind: (a: Type) -> (b: Type) -> (x: (f a)) -> (y: a -> (f b)) -> (f b))
|
|
: (Monad f)
|
|
|
|
// Variadic
|
|
// --------
|
|
|
|
Variadic (r: Type) (n: Data.Nat) : Type
|
|
Variadic r Data.Nat.zero = r
|
|
Variadic r (Data.Nat.succ n) = r -> (Variadic r n)
|
|
|
|
// Examples
|
|
// --------
|
|
|
|
SNat : Type
|
|
SNat = (p: Type) -> ((SNat) -> p) -> p -> p
|
|
|
|
SZ : SNat
|
|
SZ = p => s => z => z
|
|
|
|
|
|
|
|
|
|
|
|
|