mirror of https://git.sr.ht/~rabbits/modal
145 lines
2.9 KiB
Plaintext
145 lines
2.9 KiB
Plaintext
1 -> (s (0));
|
|
|
|
|
|
neg (neg ?x) -> ?x;
|
|
neg (0) -> 0;
|
|
|
|
|
|
add (s ?x) (s ?y) -> s (add ?x (s ?y));
|
|
add (0) (s ?x) -> s ?x;
|
|
add (s ?x) (0) -> s ?x;
|
|
add (0) (0) -> 0;
|
|
|
|
|
|
?x + ?y + ?z -> (?x + ?y) + ?z;
|
|
|
|
|
|
?x + ?y -> add ?x ?y;
|
|
|
|
|
|
sub (s ?x) (s ?y) -> sub ?x ?y;
|
|
sub (s ?x) (0) -> s ?x;
|
|
sub (0) (s ?x) -> neg (s ?x);
|
|
sub (0) (0) -> 0;
|
|
|
|
|
|
?x - ?y -> sub ?x ?y;
|
|
|
|
|
|
mul (s ?x) (s ?y) -> (s ?x) + (mul (s ?x) ((s ?y) - 1));
|
|
mul (s ?x) (s (0)) -> s ?x;
|
|
mul (s ?x) (0) -> 0;
|
|
mul (0) (s ?x) -> 0;
|
|
|
|
|
|
?x * ?y -> mul ?x ?y;
|
|
|
|
|
|
Ensures that a list or a number has been reduced to its normal form. ;
|
|
|
|
reduced (0) -> true;
|
|
reduced (nil) -> true;
|
|
reduced (s ?x) -> reduced ?x;
|
|
reduced (?h : ?t) -> reduced ?t;
|
|
reduced ?x -> false;
|
|
|
|
|
|
Because there may be conflicts with expressions that
|
|
are currently being reduced, we need to fold over reduced
|
|
lists, i.e ones that have already been fully generated. ;
|
|
|
|
fold (?f) ?i ?l -> fold reduced ?l (?f) ?i ?l;
|
|
fold true (?f) ?i (nil) -> ?i;
|
|
fold true (?f) ?i (?h : (nil)) -> ?f ?i ?h;
|
|
fold true (?f) ?i (?h : ?t) -> ?f ?i (fold (?f) ?h ?t);
|
|
fold false (?f) ?i ?l -> fold (?f) ?i ?l;
|
|
|
|
|
|
factorial (s (0)) -> s (0);
|
|
factorial (s ?x) -> (s ?x) * (factorial ((s ?x) - 1));
|
|
|
|
|
|
sum (?h : ?t) -> fold (add) (0) (?h : ?t);
|
|
|
|
|
|
range ?x (s (0)) -> ?x : (nil);
|
|
range ?x (s ?y) -> ?x : (range (?x + 1) ((s ?y) - 1));
|
|
|
|
|
|
Disgusting (yet valid) hack for currying.
|
|
We need lambdas. ;
|
|
|
|
unpack (?h : nil) -> ?h;
|
|
unpack (?h : ?t) -> ?h unpack ?t;
|
|
unpack (?x) -> ?x;
|
|
unpack (?x . -> ?x unpack (;
|
|
|
|
|
|
:: (?f) ?a -> ?f unpack ?a;
|
|
|
|
|
|
mapp (?f) ?a (nil) -> nil;
|
|
mapp (?f) ?a (?h : (nil)) -> (?f unpack ?a ?h) : (nil);
|
|
mapp (?f) ?a (?h : ?t) -> (?f unpack ?a ?h) : (mapp (?f) ?a ?t);
|
|
|
|
|
|
map (?f) (nil) -> nil;
|
|
map (?f) (?h : nil) -> (?f ?h) : (nil);
|
|
map (?f) (?h : ?t) -> (?f ?h) : (map (?f) ?t);
|
|
|
|
|
|
product ?x -> fold (mul) 1 ?x;
|
|
|
|
|
|
factorial2 ?x -> product (range 1 ?x);
|
|
|
|
|
|
contains ?x (nil) -> false;
|
|
contains ?x (?x : ?t) -> true;
|
|
contains ?x (?h : ?t) -> contains ?x ?t;
|
|
|
|
|
|
unique (nil) -> nil;
|
|
unique false (?h : ?t) -> ?h : (unique ?t);
|
|
unique true (?h : ?t) -> unique ?t;
|
|
unique (?h : ?t) -> unique contains ?h ?t (?h : ?t);
|
|
|
|
|
|
length (nil) -> 0;
|
|
length (?h : ?t) -> s (length ?t);
|
|
|
|
|
|
zipWith (?f) (nil) (nil) -> nil;
|
|
zipWith (?f) (?h : ?t) (nil) -> nil;
|
|
zipWith (?f) (nil) (?h : ?t) -> nil;
|
|
zipWith (?f) (?h1 : ?t1) (?h2 : ?t2) -> (?f ?h1 ?h2) : (zipWith (?f) ?t1 ?t2);
|
|
|
|
|
|
evens ?x -> zipWith (add) (range (0) ?x) (range (0) ?x);
|
|
|
|
|
|
not (not ?x) -> ?x;
|
|
not true -> false;
|
|
not false -> true;
|
|
|
|
|
|
any ?x -> contains true ?x;
|
|
|
|
|
|
all ?x -> not contains false ?x;
|
|
|
|
|
|
none ?x -> not any ?x;
|
|
|
|
|
|
add1 ?x -> add ?x 1;
|
|
|
|
|
|
square ?x -> ?x * ?x;
|
|
|
|
|
|
reduce (s ?x) -> s (reduce ?x);
|
|
reduce (0) -> (0);
|
|
reduce (?h : ?t) -> ?h : (reduce ?t);
|
|
reduce (nil) -> nil;
|