From 77046e264595ed75955e7f1e899228bafa08017d Mon Sep 17 00:00:00 2001 From: Devine Lu Linvega Date: Mon, 15 Apr 2024 14:21:33 -0700 Subject: [PATCH] Updated examples --- examples/arithmetic.modal | 20 ----- examples/arithmetic2.modal | 158 ------------------------------------ examples/console_read.modal | 8 +- 3 files changed, 4 insertions(+), 182 deletions(-) delete mode 100644 examples/arithmetic.modal delete mode 100644 examples/arithmetic2.modal diff --git a/examples/arithmetic.modal b/examples/arithmetic.modal deleted file mode 100644 index 7dc5405..0000000 --- a/examples/arithmetic.modal +++ /dev/null @@ -1,20 +0,0 @@ -<> (add (s ?x) (s ?y)) (s (add ?x (s ?y))) -<> (add (s ?x) (0)) (s ?x) -<> (add (0) (s ?y)) (s ?y) -<> (add (0) (0)) (0) -<> (sub (s ?x) (s ?y)) (sub ?x ?y) -<> (sub (s ?x) (0)) (s ?x) -<> (sub (0) (s ?y)) (s ?y) -<> (sub (0) (0)) (0) -<> (mul (s ?x) (s ?y)) (add (s ?x) (mul (s ?x) (sub (s ?y) (s (0))))) -<> (mul (s ?x) (s (0))) (s ?x) -<> (mul (s (0)) (s ?y)) (s ?y) -<> (mul (s ?x) (0)) (0) -<> (mul (0) (s ?x)) (0) -<> (?x + ?y) (add ?x ?y) -<> (?x - ?y) (sub ?x ?y) -<> (?x * ?y) (mul ?x ?y) -<> (factorial (s (0))) ((s (0))) -<> (factorial (s ?x)) (((s ?x) * factorial ((s ?x) - (s (0))))) - -factorial (s (s (s (s (s (0)))))) \ No newline at end of file diff --git a/examples/arithmetic2.modal b/examples/arithmetic2.modal deleted file mode 100644 index 0438471..0000000 --- a/examples/arithmetic2.modal +++ /dev/null @@ -1,158 +0,0 @@ -<> (-- ?x) () --- ( little endian binary integers ) - --- ( constants ) -<> zero ((0 nil)) -<> one ((1 nil)) -<> two ((0 (1 nil))) -<> three ((1 (1 nil))) -<> ten ((0 (1 (0 (1 nil))))) - --- ( decimal digit to binary ) -<> (binary 0) ((0 nil)) -<> (binary 1) ((1 nil)) -<> (binary 2) ((0 (1 nil))) -<> (binary 3) ((1 (1 nil))) -<> (binary 4) ((0 (0 (1 nil)))) -<> (binary 5) ((1 (0 (1 nil)))) -<> (binary 6) ((0 (1 (1 nil)))) -<> (binary 7) ((1 (1 (1 nil)))) -<> (binary 8) ((0 (0 (0 (1 nil))))) -<> (binary 9) ((1 (0 (0 (1 nil))))) - --- ( binary to decimal digit ) -<> (decimal (0 nil)) (0) -<> (decimal (1 nil)) (1) -<> (decimal (0 (1 nil))) (2) -<> (decimal (1 (1 nil))) (3) -<> (decimal (0 (0 (1 nil)))) (4) -<> (decimal (1 (0 (1 nil)))) (5) -<> (decimal (0 (1 (1 nil)))) (6) -<> (decimal (1 (1 (1 nil)))) (7) -<> (decimal (0 (0 (0 (1 nil))))) (8) -<> (decimal (1 (0 (0 (1 nil))))) (9) - --- create nil-terminated list -<> (nilify (?h)) ((?h nil)) -<> (nilify (?h ?t)) ((?h nilify ?t)) - --- reverse nil-terminated list -<> (reverse ?x) (reverse' nil ?x) -<> (reverse' ?a nil) (?a) -<> (reverse' ?a (?h ?t)) (reverse' (?h ?a) ?t) - --- ( normalize, remove trailing zeros ) --- ( currently zero is (0 nil) though arguably it could be nil ) --- ( that change would require auditing our rules ) -<> (normalize (?h ?t)) ((?h normalize' nil ?t)) -<> (normalize' ?s nil) (nil) -<> (normalize' ?s (0 ?t)) (normalize' (0 ?s) ?t) -<> (normalize' nil (1 ?t)) ((1 normalize' nil ?t)) -<> (normalize' (0 ?s) (1 ?t)) ((0 normalize' ?s (1 ?t))) - --- ( to integer ) -<> ((int ?*)) ((sum f (one) g reverse nilify (?*))) -<> (g nil) (nil) -<> (g (?h ?t)) ((binary ?h g ?t)) -<> (f (?u) nil) (nil) -<> (f (?u) (?h ?t)) (((mul ?h ?u) f ((mul ?u ten)) ?t)) - --- ( to string: TODO, need division for this one ) - --- ( comparison operartions ) -<> ((cmp ?x ?y)) ((cmpc #eq ?x ?y)) -<> ((cmpc ?e nil nil)) (?e) -<> ((cmpc ?e (1 ?x) nil)) (#gt) -<> ((cmpc ?e (0 ?x) nil)) ((cmpc ?e ?x nil)) -<> ((cmpc ?e nil (1 ?y))) (#lt) -<> ((cmpc ?e nil (0 ?y))) ((cmpc ?e nil ?y)) -<> ((cmpc ?e (0 ?x) (0 ?y))) ((cmpc ?e ?x ?y)) -<> ((cmpc ?e (1 ?x) (0 ?y))) ((cmpc #gt ?x ?y)) -<> ((cmpc ?e (0 ?x) (1 ?y))) ((cmpc #lt ?x ?y)) -<> ((cmpc ?e (1 ?x) (1 ?y))) ((cmpc ?e ?x ?y)) - --- ( addition ) -<> ((add ?x ?y)) (addc 0 ?x ?y) -<> (addc 0 nil nil) (nil) -<> (addc 1 nil nil) ((1 nil)) -<> (addc ?c ?x nil) (addc ?c ?x (0 nil)) -<> (addc ?c nil ?y) (addc ?c (0 nil) ?y) -<> (addc 0 (0 ?x) (0 ?y)) ((0 addc 0 ?x ?y)) -<> (addc 0 (0 ?x) (1 ?y)) ((1 addc 0 ?x ?y)) -<> (addc 0 (1 ?x) (0 ?y)) ((1 addc 0 ?x ?y)) -<> (addc 0 (1 ?x) (1 ?y)) ((0 addc 1 ?x ?y)) -<> (addc 1 (0 ?x) (0 ?y)) ((1 addc 0 ?x ?y)) -<> (addc 1 (0 ?x) (1 ?y)) ((0 addc 1 ?x ?y)) -<> (addc 1 (1 ?x) (0 ?y)) ((0 addc 1 ?x ?y)) -<> (addc 1 (1 ?x) (1 ?y)) ((1 addc 1 ?x ?y)) - --- ( summation ) -<> ((sum nil)) ((0 nil)) -<> ((sum (?a nil))) (?a) -<> ((sum (?a (?b ?c)))) ((sum ((add ?a ?b) ?c))) - --- ( multiplication ) -<> ((mul ?x ?y)) (mulc nil ?x ?y) -<> (mulc ?t nil ?y) ((sum ?t)) -<> (mulc ?t (0 ?x) ?y) (mulc ?t ?x (0 ?y)) -<> (mulc ?t (1 ?x) ?y) (mulc (?y ?t) ?x (0 ?y)) - --- ( subtraction ) -<> ((sub ?x ?y)) (normalize subc 0 ?x ?y) -<> (subc 0 nil nil) (nil) -<> (subc 1 nil nil) (#err) -<> (subc 0 ?x nil) (?x) -<> (subc 1 ?x nil) (subc 1 ?x (0 nil)) -<> (subc ?c nil ?y) (subc ?c (0 nil) ?y) -<> (subc 0 (0 ?x) (0 ?y)) ((0 subc 0 ?x ?y)) -<> (subc 0 (0 ?x) (1 ?y)) ((1 subc 1 ?x ?y)) -<> (subc 0 (1 ?x) (0 ?y)) ((1 subc 0 ?x ?y)) -<> (subc 0 (1 ?x) (1 ?y)) ((0 subc 0 ?x ?y)) -<> (subc 1 (0 ?x) (0 ?y)) ((1 subc 1 ?x ?y)) -<> (subc 1 (0 ?x) (1 ?y)) ((0 subc 1 ?x ?y)) -<> (subc 1 (1 ?x) (0 ?y)) ((0 subc 0 ?x ?y)) -<> (subc 1 (1 ?x) (1 ?y)) ((1 subc 1 ?x ?y)) - --- ( dec ) -<> (dec (0 nil)) (#err) -<> (dec ?x) (normalize dec' ?x) -<> (dec' (0 ?t)) ((1 dec' ?t)) -<> (dec' (1 ?t)) ((0 ?t)) - --- ( inc ) -<> ((inc nil)) ((1 nil)) -<> ((inc (0 ?t))) ((1 ?t)) -<> ((inc (1 ?t))) ((0 (inc ?t))) - --- ( left shift; lshift x b means x< ((lshift ?x (0 nil))) (?x) -<> ((lshift ?x (1 nil))) ((0 ?x)) -<> ((lshift ?x (?h (?a ?b)))) ((lshift (0 ?x) dec (?h (?a ?b)))) - --- ( divmod, i.e. quotient and remainder ) -<> ((divmod ?x ?y)) ((divmod1 ?x ?y (cmp ?x ?y))) -<> ((divmod1 ?x ?y #lt)) (zero) -<> ((divmod1 ?x ?y #eq)) (one) -<> ((divmod1 ?x ?y #gt)) ((divmod2 ?x ?y zero (0 ?y))) -<> ((divmod2 ?x ?y ?s ?m)) ((divmod3 ?x ?y ?s ?m (cmp ?x ?m))) -<> ((divmod3 ?x ?y ?s ?m #lt)) ((divmod4 ?x ?y ?s zero)) -<> ((divmod3 ?x ?y ?s ?m #eq)) ((divmod4 ?x ?y (inc ?s) zero)) -<> ((divmod3 ?x ?y ?s ?m #gt)) ((divmod2 ?x ?y (inc ?s) (0 ?m))) -<> ((divmod4 ?x ?y (0 nil) ?d)) (((add ?d one) (sub ?x ?y))) -<> ((divmod4 ?x ?y ?s ?d)) ((divmod5 (sub ?x (lshift ?y ?s)) ?y dec ?s (add ?d (lshift one ?s)))) -<> ((divmod5 (0 nil) ?y ?s ?d)) ((?d (0 nil))) -<> ((divmod5 ?x ?y ?s ?d)) ((divmod6 ?x ?y ?s ?d (cmp ?x (lshift ?y ?s)))) -<> ((divmod6 ?x ?y (0 nil) ?d #lt)) ((?d ?x)) -<> ((divmod6 ?x ?y ?s ?d #lt)) ((divmod5 ?x ?y dec ?s ?d)) -<> ((divmod6 ?x ?y ?s ?d #eq)) ((divmod4 ?x ?y ?s ?d)) -<> ((divmod6 ?x ?y ?s ?d #gt)) ((divmod4 ?x ?y ?s ?d)) - --- ( floor divison ) -<> ((div ?x ?y)) ((div' (divmod ?x ?y))) -<> ((div' (?q ?r))) (?q) - --- ( remainder ) -<> ((mod ?x ?y)) ((mod' (divmod ?x ?y))) -<> ((mod' (?q ?r))) (?r) - -(divmod (int 1234567) (int 1357)) \ No newline at end of file diff --git a/examples/console_read.modal b/examples/console_read.modal index d4145e7..2c33054 100644 --- a/examples/console_read.modal +++ b/examples/console_read.modal @@ -1,9 +1,9 @@ -<> (read) (?~) +<> (read ?~) (?~) <> (?: print ') (?:) <> (' ?x) (?x ') (Tell me three things: \n) print ' -' (You said: read -then, you continued: read -finaly, you concluded: read) print +' (You said: read stdin +then, you continued: read stdin +finaly, you concluded: read stdin) print \ No newline at end of file