Commit e73caa8eb1f5731c5fdf8503058e4da964c3ff19 - pico-ml-old

+26

-0

stdlib/Collections.pml less more

	1	exports
	2	( HasLength(..)
	3	, length
	4	, null
	5	, Sequence(..)
	6	, Functor(..)
	7	, map
	8	)
	9
	10	record HasLength f = { .length (f -> Nat) }
	11
	12	length : implicit (HasLength l) -> l -> Nat
	13	(implicit l) = l.length
	14
	15	null : implicit (HasLength l) -> l -> Bool
	16	(implicit l) ls = l.length ls == 0
	17
	18	record Sequence f =
	19	{ .toList (f a -> List a)
	20	, .fromList (List a -> f a)
	21	}
	22
	23	record Functor f = { .map ((a -> b) -> f a -> f b) }
	24
	25	map : implicit (Functor f) -> (a -> b) -> f a -> f b
	26	f = f.map

+34

-0

stdlib/List.pml less more

	1	import list
	2	import monoid
	3
	4	implicit listHasLength : HasLength List =
	5	{ .length
	6	Cons _ xs = 1 + length xs
	7	Nil = 0
	8	}
	9
	10	implicit listSequence : Sequence List =
	11	{ .toList = id
	12	, .fromList = id
	13	}
	14
	15	implicit listFunctor : Functor List =
	16	{ .map
	17	f (Cons x xs) = Cons (f x) xs
	18	_ Nil = Nil
	19	}
	20
	21	implicit listMonoid : Monoid List =
	22	{ .empty = []
	23	, .append
	24	Nil ys = ys
	25	(Cons x xs) ys = Cons x (append xs ys)
	26	}
	27
	28	head : List a -> a
	29	x :: _ = x
	30	Nil = error "head: empty list"
	31
	32	tail : List a -> List a
	33	_ :: xs = xs
	34	Nil = error "tail: empty list"

+69

-0

stdlib/Monoid.pml less more

	1	exports
	2	( Monoid(..)
	3	, empty
	4	, _<>_
	5	)
	6
	7	import Num
	8
	9	-- The Monoid type
	10
	11	record Monoid m =
	12	{ .empty m
	13	, .append (m -> m -> m)
	14	}
	15
	16	-- implicit sugars for the Monoid operations
	17
	18	empty : implicit (Monoid m) -> m
	19	m = m.empty
	20
	21	_<>_ : m -> m -> implicit (Monoid m) -> m
	22	x y m = m.append x y
	23
	24	-- some Monoid values
	25
	26	implicit unitMonoid : Monoid () =
	27	{ .empty = ()
	28	, .append _ _ = ()
	29	}
	30
	31	additive : implicit (Add m) -> Monoid m
	32	add = { .empty = add.zero
	33	, .append = add.plus
	34	}
	35
	36	multiplicative : implicit (Mul m) -> Monoid m
	37	mul = { .empty = mul.one
	38	, .append = mul.times
	39	}
	40
	41	implicit conjunctive : Monoid Bool =
	42	{ .empty = False
	43	, .append = _&&_
	44	}
	45
	46	disjunctive : Monoid Bool =
	47	{ .empty = True
	48	, .append = _\|\|_
	49	}
	50
	51	dual : Monoid m -> Monoid m
	52	m = { .empty = m.empty
	53	, .append x y = m.append y x
	54	}
	55
	56	endo : Monoid (a -> a) =
	57	{ .empty = id
	58	, .append x y = compose x y
	59	}
	60
	61	reader : implicit (Monoid b) -> Monoid (a -> b)
	62	m = { .empty _ = m.empty
	63	, .append x f g = m.append (f x) (g x)
	64	}
	65
	66	pair : implicit (Monoid l) -> implicit (Monoid r) -> Monoid (l * r)
	67	l r = { .empty = (l.empty, r.empty)
	68	, .append (x1, y1) (x2, y2) = (l.append x1 x2, r.append y1 y2)
	69	}

+43

-0

stdlib/Num.pml less more

	1	exports
	2	( Add(..)
	3	, Mul(..)
	4	, _+_
	5	, _*_
	6	)
	7
	8	-- mathematical operations
	9
	10	record IsNumber n = { .fromInteger (Int -> n) }
	11
	12	record Add n =
	13	{ .zero n
	14	, .plus (n -> n -> n)
	15	}
	16
	17	record Mul n =
	18	{ .one n
	19	, .times (n -> n -> n)
	20	}
	21
	22	record Sub n =
	23	{ .pSubAdd (Add n)
	24	, .sub (n -> n -> n)
	25	}
	26
	27	record Div n =
	28	{ .pDivMul (Mul n)
	29	, .div (n -> n -> n)
	30	, .mod (n -> n -> n)
	31	, .rem (n -> n -> n)
	32	}
	33
	34	-- some teaspoons for mathematical operations
	35
	36	fromInteger : implicit (IsNumber n) -> Int -> n
	37	i = i.fromInteger
	38
	39	_+_ : n -> n -> implicit (Add n) -> n
	40	x y add = add.plus x y
	41
	42	_*_ : n -> n -> implicit (Mul n) -> n
	43	x y mul = mul.times x y