First Commit
This commit is contained in:
commit
b0864dff38
12 changed files with 232 additions and 0 deletions
0
lib/cp.ml
Normal file
0
lib/cp.ml
Normal file
110
lib/cpcore.ml
Normal file
110
lib/cpcore.ml
Normal file
|
@ -0,0 +1,110 @@
|
|||
(*Renaming *)
|
||||
let const a _ = a
|
||||
let id x = x
|
||||
let (!) a = const () a
|
||||
let p1 = fst
|
||||
let p2 = snd
|
||||
|
||||
let either f g x = match x with
|
||||
| Either.Left a -> f a
|
||||
| Either.Right b -> g b
|
||||
|
||||
(*
|
||||
This is the infix composition operator
|
||||
*)
|
||||
let (<.) f g x= f (g x)
|
||||
|
||||
(* (1) Product -------------------------------------------------------*)
|
||||
let split f g x = (f x, g x)
|
||||
(* Example : split ((+) 1) ((+) 3) 5 *)
|
||||
|
||||
let (><) f g = split (f <. p1) (g <. p2)
|
||||
|
||||
(*dup*)
|
||||
let diag x = split id id x
|
||||
|
||||
(* (2) Coproduct -------------------------------------------------------*)
|
||||
|
||||
(*Renaming *)
|
||||
let i1 x = Either.Left x
|
||||
let i2 x = Either.Right x
|
||||
|
||||
let (-|-) f g x = either (i1 <. f) (i2 <. g) x
|
||||
|
||||
(* McCarthy's conditional *)
|
||||
|
||||
let grd p x = if p x then i1 x else i2 x
|
||||
|
||||
let cond p f g = ((either f g) <. (grd p))
|
||||
|
||||
(*dup*)
|
||||
let codiag x = either id id x
|
||||
|
||||
(* (3) Exponentiation -------------------------------------------------------*)
|
||||
|
||||
let curry f x y = f (x,y)
|
||||
let uncurry f (x,y) = f x y
|
||||
|
||||
let ap (f,x) = f x
|
||||
|
||||
let expn f = curry (f <. ap)
|
||||
|
||||
let p2p p b = if b then (snd p) else (fst p)
|
||||
|
||||
(*Natural isomorphisms*)
|
||||
|
||||
let swap x = split p2 p1 x
|
||||
|
||||
let assocr x = split (p1 <. p1) (p2 >< id) x
|
||||
|
||||
let assocl x = split (id >< p1) (p2 <. p2) x
|
||||
|
||||
let undistr x = either (id >< i1) (id >< i2) x
|
||||
|
||||
let undistl x = either (i1 >< id) (i2 >< id) x
|
||||
|
||||
let flatr (a,(b,c)) = (a,b,c)
|
||||
|
||||
let flatl ((a,b),c) = (a,b,c)
|
||||
|
||||
let br x = split id (!) x
|
||||
|
||||
let bl x = split (!) id x
|
||||
|
||||
let coswap x = either i2 i1 x
|
||||
|
||||
let coassocr x = either (id -|- i1) (i2 <. i2) x
|
||||
|
||||
let coassocl x = either (i1<.i1) (i2 -|- id) x
|
||||
|
||||
let distl x = uncurry (either (curry i1) (curry i2)) x
|
||||
|
||||
let distr x = ((swap -|- swap) <. distl <. swap) x
|
||||
|
||||
let colambda (a,b) c = if c then a else b
|
||||
|
||||
let lambda f = (f false, f true)
|
||||
|
||||
let singl a = [a]
|
||||
|
||||
let bang = (!)
|
||||
|
||||
let dup x = split id id x
|
||||
|
||||
let zero x = const 0 x
|
||||
|
||||
let one x = const 1 x
|
||||
|
||||
let nil (_: 'a list) : 'a list = []
|
||||
|
||||
let cons (a,b) = a :: b
|
||||
|
||||
let add = uncurry ( + )
|
||||
|
||||
let mul = uncurry ( * )
|
||||
|
||||
(* mul not working because of comment syntax *)
|
||||
|
||||
let conc a b = (uncurry (@)) (a,b)
|
||||
|
||||
let umax a b = (uncurry max) (a,b)
|
32
lib/cplist.ml
Normal file
32
lib/cplist.ml
Normal file
|
@ -0,0 +1,32 @@
|
|||
open Cpcore
|
||||
|
||||
let inList x = either nil cons x
|
||||
|
||||
let outList l = match l with
|
||||
| [] -> i1 ()
|
||||
| (x::xs) -> i2 (x,xs)
|
||||
|
||||
let baseList g f = id -|- (g >< f)
|
||||
|
||||
|
||||
(* (2) Ana + cata + hylo) ----------------------------------------------- *)
|
||||
|
||||
let recList f l = (id -|- (id >< f)) l
|
||||
|
||||
let rec cataList g l = (g <. recList (cataList g) <. outList) l
|
||||
|
||||
let rec anaList g l = (inList <. recList (anaList g) <. g) l
|
||||
|
||||
let hyloList f g l = (cataList f -|- anaList g) l
|
||||
|
||||
let rec len l = match l with
|
||||
| [] -> 0
|
||||
| (_::xs) -> 1 + len xs
|
||||
|
||||
let head l = match l with
|
||||
| [] -> 0
|
||||
| (x::_) -> x
|
||||
|
||||
let sum l = cataList (either (const 0) (add)) l
|
||||
|
||||
|
22
lib/cpnat.ml
Normal file
22
lib/cpnat.ml
Normal file
|
@ -0,0 +1,22 @@
|
|||
open Cpcore
|
||||
|
||||
let inNat n = either (const 0) succ n
|
||||
|
||||
let outNat num = match num with
|
||||
| 0 -> i1 ()
|
||||
| n when n>0 -> i2 (n-1)
|
||||
| _ -> invalid_arg "outNat: negative integer not supported"
|
||||
|
||||
(* (2) Ana + cata + hylo ----------------------------------------------- *)
|
||||
|
||||
let recNat f n = (id -|- f) n
|
||||
|
||||
let rec cataNat g n = (g <. recNat (cataNat g) <. outNat) n
|
||||
|
||||
let rec anaNat g n = (inNat <. recNat (anaNat g) <. g) n
|
||||
|
||||
let hyloNat f g n = (cataNat f <. anaNat g) n
|
||||
|
||||
let forNat b i = cataNat (either (const i) b)
|
||||
|
||||
let fib = p2 <. (forNat (split add p1) (1,1))
|
3
lib/dune
Normal file
3
lib/dune
Normal file
|
@ -0,0 +1,3 @@
|
|||
(library
|
||||
(name cp)
|
||||
(modules Cpcore Cplist Cpnat))
|
Loading…
Add table
Add a link
Reference in a new issue