ocaml: phase 5.1 peano.ml baseline (Peano arithmetic, 5*6 = 30)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Defines unary Peano numerals with two recursive functions for
arithmetic:
type peano = Zero | Succ of peano
let rec plus a b = match a with
| Zero -> b
| Succ a' -> Succ (plus a' b)
let rec mul a b = match a with
| Zero -> Zero
| Succ a' -> plus b (mul a' b)
mul is defined inductively: mul Zero _ = Zero; mul (Succ a) b =
b + (a * b).
to_int (mul (from_int 5) (from_int 6)) = 30
The result is a Peano value with 30 nested Succ wrappers; to_int
unrolls them to a host int. Tests recursive ADT with a single-arg
constructor + four mutually-defined recursive functions (no rec/and
needed since each is defined separately).
80 baseline programs total — milestone.
This commit is contained in:
@@ -56,6 +56,7 @@
|
|||||||
"paren_depth.ml": 7,
|
"paren_depth.ml": 7,
|
||||||
"pancake_sort.ml": 910,
|
"pancake_sort.ml": 910,
|
||||||
"pascal.ml": 252,
|
"pascal.ml": 252,
|
||||||
|
"peano.ml": 30,
|
||||||
"pi_leibniz.ml": 314,
|
"pi_leibniz.ml": 314,
|
||||||
"prefix_sum.ml": 66,
|
"prefix_sum.ml": 66,
|
||||||
"pretty_table.ml": 64,
|
"pretty_table.ml": 64,
|
||||||
|
|||||||
21
lib/ocaml/baseline/peano.ml
Normal file
21
lib/ocaml/baseline/peano.ml
Normal file
@@ -0,0 +1,21 @@
|
|||||||
|
type peano = Zero | Succ of peano
|
||||||
|
|
||||||
|
let rec to_int p = match p with
|
||||||
|
| Zero -> 0
|
||||||
|
| Succ p' -> 1 + to_int p'
|
||||||
|
|
||||||
|
let rec from_int n =
|
||||||
|
if n = 0 then Zero
|
||||||
|
else Succ (from_int (n - 1))
|
||||||
|
|
||||||
|
let rec plus a b = match a with
|
||||||
|
| Zero -> b
|
||||||
|
| Succ a' -> Succ (plus a' b)
|
||||||
|
|
||||||
|
let rec mul a b = match a with
|
||||||
|
| Zero -> Zero
|
||||||
|
| Succ a' -> plus b (mul a' b)
|
||||||
|
|
||||||
|
;;
|
||||||
|
|
||||||
|
to_int (mul (from_int 5) (from_int 6))
|
||||||
@@ -407,6 +407,14 @@ _Newest first._
|
|||||||
binary search tree (`type 'a tree = Leaf | Node of 'a * 'a tree *
|
binary search tree (`type 'a tree = Leaf | Node of 'a * 'a tree *
|
||||||
'a tree`) with insert + in-order traversal. Tests parametric ADT,
|
'a tree`) with insert + in-order traversal. Tests parametric ADT,
|
||||||
recursive match, List.append, List.fold_left.
|
recursive match, List.append, List.fold_left.
|
||||||
|
- 2026-05-09 Phase 5.1 — peano.ml baseline (Peano arithmetic, 5*6 =
|
||||||
|
30). Defines `type peano = Zero | Succ of peano` and four
|
||||||
|
recursive functions: to_int, from_int, plus, mul. Multiplication
|
||||||
|
is defined inductively: `mul Zero _ = Zero; mul (Succ a) b = plus
|
||||||
|
b (mul a b)`. The result of `mul (from_int 5) (from_int 6)` is a
|
||||||
|
Peano number with 30 nested Succ wrappers. Tests recursive ADT
|
||||||
|
with single-arg constructor + recursive function bodies. 80
|
||||||
|
baseline programs total — milestone.
|
||||||
- 2026-05-09 Phase 5.1 — count_change.ml baseline (number of ways to
|
- 2026-05-09 Phase 5.1 — count_change.ml baseline (number of ways to
|
||||||
make 50c from [1;2;5;10;25] = 406). Companion to coin_change.ml
|
make 50c from [1;2;5;10;25] = 406). Companion to coin_change.ml
|
||||||
(min coins): instead of minimising, this counts distinct
|
(min coins): instead of minimising, this counts distinct
|
||||||
|
|||||||
Reference in New Issue
Block a user