Kind2/example/example.kind2

// 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