2022-07-17 06:50:50 +03:00
|
|
|
// Bool
|
|
|
|
// ----
|
|
|
|
|
2022-07-16 01:42:43 +03:00
|
|
|
Bool : Type
|
|
|
|
True : Bool
|
|
|
|
False : Bool
|
2022-07-17 08:44:50 +03:00
|
|
|
|
2022-07-16 01:42:43 +03:00
|
|
|
Bool.not (a: Bool) : Bool
|
|
|
|
Bool.not True = False
|
|
|
|
Bool.not False = True
|
|
|
|
|
|
|
|
Bool.and (a: Bool) (b: Bool) : Bool
|
|
|
|
Bool.and True True = True
|
|
|
|
Bool.and True False = False
|
|
|
|
Bool.and False True = False
|
|
|
|
Bool.and False False = False
|
|
|
|
|
2022-07-16 07:27:52 +03:00
|
|
|
Bool.not_not_theorem (a: Bool) : (Equal Bool a (Bool.not (Bool.not a)))
|
2022-07-17 06:44:44 +03:00
|
|
|
Bool.not_not_theorem True = (Refl Bool True)
|
|
|
|
Bool.not_not_theorem False = (Refl Bool False)
|
2022-07-16 06:52:56 +03:00
|
|
|
|
2022-07-17 06:50:50 +03:00
|
|
|
// Nat
|
|
|
|
// ---
|
|
|
|
|
|
|
|
Nat : Type
|
|
|
|
Zero : Nat
|
|
|
|
Succ (pred: Nat) : Nat
|
|
|
|
|
2022-07-16 06:52:56 +03:00
|
|
|
Nat.double (x: Nat) : Nat
|
|
|
|
Nat.double (Succ x) = (Succ (Succ (Nat.double x)))
|
|
|
|
Nat.double (Zero) = (Zero)
|
2022-07-17 08:44:50 +03:00
|
|
|
|
|
|
|
Nat.add (a: Nat) (b: Nat) : Nat
|
|
|
|
Nat.add (Succ a) b = (Succ (Nat.add a b))
|
|
|
|
Nat.add Zero b = b
|
|
|
|
|
|
|
|
Nat.comm.a (a: Nat) : (Equal Nat a (Nat.add a Zero))
|
|
|
|
Nat.comm.a Zero = Refl
|
|
|
|
Nat.comm.a (Succ a) = (Equal.apply @x(Succ x) (Nat.comm.a a))
|
|
|
|
|
|
|
|
Nat.comm.b (a: Nat) (b: Nat): (Equal Nat (Nat.add a (Succ b)) (Succ (Nat.add a b)))
|
|
|
|
Nat.comm.b Zero b = Refl
|
|
|
|
Nat.comm.b (Succ a) b = (Equal.apply @x(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 Zero b = (Nat.comm.a b)
|
|
|
|
Nat.comm (Succ a) b =
|
|
|
|
let e0 = (Equal.apply @x(Succ x) (Nat.comm a b))
|
|
|
|
let e1 = (Equal.mirror (Nat.comm.b b a))
|
|
|
|
(Equal.chain e0 e1)
|
2022-07-19 04:29:57 +03:00
|
|
|
|
|
|
|
Nat.to_u60 (n: Nat) : U60
|
|
|
|
Nat.to_u60 Zero = #0
|
|
|
|
Nat.to_u60 (Succ n) = (+ #1 (Nat.to_u60 n))
|
2022-07-16 06:52:56 +03:00
|
|
|
|
2022-07-17 06:50:50 +03:00
|
|
|
// List
|
|
|
|
// ----
|
|
|
|
|
|
|
|
List (a: Type) : Type
|
|
|
|
Nil <a> : (List a)
|
|
|
|
Cons <a> (x: a) (xs: (List a)) : (List a)
|
|
|
|
|
2022-07-16 01:42:43 +03:00
|
|
|
List.negate (xs: (List Bool)) : (List Bool)
|
|
|
|
List.negate (Cons Bool x xs) = (Cons Bool (Bool.not x) (List.negate xs))
|
|
|
|
List.negate (Nil Bool) = (Nil Bool)
|
|
|
|
|
2022-07-17 06:01:57 +03:00
|
|
|
List.tail <a> (xs: (List a)) : (List a)
|
2022-07-16 06:52:56 +03:00
|
|
|
List.tail a (Cons t x xs) = xs
|
|
|
|
|
2022-07-17 06:01:57 +03:00
|
|
|
List.map <a> <b> (x: (List a)) (f: (x: a) b) : (List b)
|
2022-07-19 04:47:18 +03:00
|
|
|
List.map a b (Nil t) f = Nil
|
|
|
|
List.map a b (Cons t x xs) f = (Cons (f x) (List.map xs f))
|
2022-07-16 02:10:59 +03:00
|
|
|
|
2022-07-18 03:38:45 +03:00
|
|
|
List.concat <a> (xs: (List a)) (ys: (List a)) : (List a)
|
|
|
|
List.concat a (Cons u x xs) ys = (Cons u x (List.concat a xs ys))
|
|
|
|
List.concat a (Nil u) ys = ys
|
|
|
|
|
|
|
|
List.flatten <a> (xs: (List (List a))) : (List a)
|
|
|
|
List.flatten a (Cons u x xs) = (List.concat x (List.flatten xs))
|
|
|
|
List.flatten a (Nil u) = 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))
|
|
|
|
|
2022-07-19 04:29:57 +03:00
|
|
|
List.range.go (lim: Nat) (res: (List Nat)) : (List Nat)
|
|
|
|
List.range.go Zero res = res
|
|
|
|
List.range.go (Succ n) res = (List.range.go n (Cons n res))
|
|
|
|
|
|
|
|
List.sum (xs: (List Nat)) : Nat
|
|
|
|
List.sum (Nil t) = Zero
|
|
|
|
List.sum (Cons t x xs) = (Nat.add x (List.sum xs))
|
|
|
|
|
2022-07-17 06:50:50 +03:00
|
|
|
// Equal
|
|
|
|
// -----
|
|
|
|
|
|
|
|
Equal <t> (a: t) (b: t) : Type
|
2022-07-17 08:44:50 +03:00
|
|
|
Refl <t> <a: t> : (Equal t a a)
|
2022-07-17 06:50:50 +03:00
|
|
|
|
2022-07-17 08:44:50 +03:00
|
|
|
Equal.mirror <t> <a: t> <b: t> (e: (Equal t a b)) : (Equal t b a)
|
2022-07-16 01:42:43 +03:00
|
|
|
Equal.mirror t a b (Refl u k) = (Refl u k)
|
|
|
|
|
2022-07-17 08:44:50 +03:00
|
|
|
Equal.apply <t> <u> <a: t> <b: t> (f: t -> t) (e: (Equal t a b)) : (Equal t (f a) (f b))
|
2022-07-16 01:42:43 +03:00
|
|
|
Equal.apply t u a b f (Refl v k) = (Refl v (f k))
|
|
|
|
|
2022-07-17 06:01:57 +03:00
|
|
|
Equal.rewrite <t> (a: t) (b: t) (e: (Equal t a b)) (p: t -> Type) (x: (p a)) : (p b)
|
2022-07-16 01:42:43 +03:00
|
|
|
Equal.rewrite t a b (Refl u k) p x = {x :: (p k)}
|
|
|
|
|
2022-07-17 08:44:50 +03:00
|
|
|
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 (Refl u x) = {e0 :: (Equal t a x)}
|
|
|
|
|
2022-07-18 03:38:45 +03:00
|
|
|
// Monad
|
|
|
|
// -----
|
|
|
|
|
|
|
|
Monad (f: Type -> Type) : Type
|
|
|
|
Monad.new (f: Type -> Type)
|
|
|
|
(pure: (a: Type) (x: a) (Monad (f a)))
|
|
|
|
(bind: (a: Type) (b: Type) (x: (Monad a)) (y: a -> (Monad b)) (Monad b))
|
|
|
|
: (Monad f)
|
|
|
|
|
2022-07-17 06:50:50 +03:00
|
|
|
// Examples
|
|
|
|
// --------
|
2022-07-17 04:35:48 +03:00
|
|
|
|
2022-07-18 03:38:45 +03:00
|
|
|
// Generates combinations!
|
|
|
|
// - Run with : `kind2 run example.kind2`
|
|
|
|
// - Check with : `kind2 check example.kind2
|
2022-07-19 04:29:57 +03:00
|
|
|
Main : U60 {
|
|
|
|
let f = {@x (Succ (Succ x)) :: Nat -> Nat}
|
|
|
|
let f = {@x (f (f x)) :: Nat -> Nat}
|
|
|
|
let f = {@x (f (f x)) :: Nat -> Nat}
|
|
|
|
let f = {@x (f (f x)) :: Nat -> Nat}
|
|
|
|
let f = {@x (f (f x)) :: Nat -> Nat}
|
|
|
|
let f = {@x (f (f x)) :: Nat -> Nat}
|
|
|
|
let f = {@x (f (f x)) :: Nat -> Nat}
|
|
|
|
let f = {@x (f (f x)) :: Nat -> Nat}
|
|
|
|
let f = {@x (f (f x)) :: Nat -> Nat}
|
|
|
|
let n = (f Zero)
|
|
|
|
let list = (List.range.go n Nil)
|
|
|
|
(Nat.to_u60 (List.sum list))
|
2022-07-18 02:05:49 +03:00
|
|
|
}
|