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