# Author: Paul Fitzpatrick, paulfitz@ai.mit.edu
# Copyright (c) 2003 Paul Fitzpatrick
#
# This file is part of CosmicOS.
#
# CosmicOS is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# CosmicOS is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with CosmicOS; if not, write to the Free Software
# Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
#

# MATH introduce numbers (in unary notation)
(intro 0);
(intro .0);
(intro ..0);
(intro ...0);
(intro ....0);
(intro .....0);
(intro ......0);
(intro .......0);
(intro ........0);
(intro .........0);
(intro ..........0);
(intro ...........0);
(intro ............0);
(intro .............0);
(intro ..............0);
(intro ...............0);
(intro ................0);
(intro .................0);
(intro ..................0);
(intro ...................0);
(intro ....................0);
(intro .....................0);
(intro ......................0);
(intro .......................0);
(intro ........................0);
(intro .........................0);
(intro ..........................0);
(intro ...........................0);
(intro ...........................0);
(intro ..........................0);
(intro .........................0);
(intro ........................0);
(intro .......................0);
(intro ......................0);
(intro .....................0);
(intro ....................0);
(intro ...................0);
(intro ..................0);
(intro .................0);
(intro ................0);
(intro ...............0);
(intro ..............0);
(intro .............0);
(intro ............0);
(intro ...........0);
(intro ..........0);
(intro .........0);
(intro ........0);
(intro .......0);
(intro ......0);
(intro .....0);
(intro ....0);
(intro ...0);
(intro ..0);
(intro .0);
(intro 0);
(intro 0);
(intro .0);
(intro ..0);
(intro ...0);
(intro .....0);
(intro .......0);
(intro ...........0);
(intro .............0);
(intro .................0);
(intro ...................0);
(intro .......................0);
(intro 0);
(intro .0);
(intro ....0);
(intro .........0);
(intro ................0);
(intro .........................0);
(intro 0);
(intro .0);
(intro ........0);
(intro ...........................0);
# MATH now show equality
(intro =);
(= 0 0);
(= ....0 ....0);
(= ......0 ......0);
(= ..0 ..0);
(= ...0 ...0);
# MATH now show other relational operators
(intro >);
(> ...0 .0);
(> .0 0);
(> ......0 0);
(> ....0 0);
(> .....0 0);
(> ....0 0);
(> .0 0);
(> ......0 .0);
(> ......0 ..0);
(> ...0 .0);
(> .....0 0);
(intro <);
(< 0 ......0);
(< 0 .0);
(< 0 .0);
(< 0 ..0);
(< .0 ...0);
(< 0 ..0);
(< ..0 ....0);
(< ...0 .....0);
(< 0 ..0);
(< 0 .....0);
(< ...0 ......0);
(< ..0 ...0);
(> ..0 .0);
(> .....0 .0);
(= ...0 ...0);
(= ...0 ...0);
(> .0 0);
(< .0 ....0);
(= ....0 ....0);
(> ...0 ..0);
(= ...0 ...0);
(< ...0 .....0);
# MATH introduce the NOT logical operator
(intro not);
(= .0 .0);
(not (< .0 .0));
(not (> .0 .0));
(= ...0 ...0);
(not (< ...0 ...0));
(not (> ...0 ...0));
(= 0 0);
(not (< 0 0));
(not (> 0 0));
(= ...0 ...0);
(not (< ...0 ...0));
(not (> ...0 ...0));
(= .0 .0);
(not (< .0 .0));
(not (> .0 .0));
(= .....0 .....0);
(not (< .....0 .....0));
(not (> .....0 .....0));
(not (= .0 ....0));
(< .0);
(not (> .0 ....0));
(not (= ..0 ....0));
(< ..0);
(not (> ..0 ....0));
(not (= .....0 .......0));
(< .....0);
(not (> .....0 .......0));
(not (= .....0 .......0));
(< .....0);
(not (> .....0 .......0));
(not (= .0 ...0));
(< .0);
(not (> .0 ...0));
(not (= .....0 ......0));
(< .....0);
(not (> .....0 ......0));
(not (= .....0 ....0));
(> .....0 ....0);
(not (< .....0 ....0));
(not (= .......0 .....0));
(> .......0 .....0);
(not (< .......0 .....0));
(not (= .......0 .....0));
(> .......0 .....0);
(not (< .......0 .....0));
(not (= ...0 .0));
(> ...0 .0);
(not (< ...0 .0));
(not (= .......0 .....0));
(> .......0 .....0);
(not (< .......0 .....0));
(not (= ......0 ...0));
(> ......0 ...0);
(not (< ......0 ...0));
# MATH introduce the AND logical operator
(intro and);
(and (< .....0 .......0) (> ....0 ...0));
(and (= .0 .0) (= .....0 .....0));
(and (> ....0 ...0) (> ....0 .0));
(and (< .....0 ......0) (= .....0 .....0));
(and (> .......0 .....0) (= ..0 ..0));
(and (< ...0 ......0) (> .....0 ....0));
(and (= ..0 ..0) (< 0 ..0));
(and (> .....0 ..0) (= ..0 ..0));
(and (< .0 ....0) (= ....0 ....0));
(and (< .0 ..0) (= ..0 ..0));
(not (and (> ....0 ...0) (> 0 .0)));
(not (and (< ...0 .....0) (= ..0 ....0)));
(not (and (< ....0 ......0) (> .0 .....0)));
(not (and (< ....0 ......0) (= ...0 .....0)));
(not (and (= .0 .0) (< .....0 ..0)));
(not (and (> ..0 ...0) (< .0 ...0)));
(not (and (< ......0 .0) (> ...0 ..0)));
(not (and (= .....0 ....0) (> ..0 0)));
(not (and (= .0 0) (> .......0 .....0)));
(not (and (> ...0 .....0) (< ...0 ......0)));
(not (and (< .....0 ....0) (> ......0 ......0)));
(not (and (= ....0 0) (> 0 ...0)));
(not (and (= .....0 0) (> ...0 ...0)));
(not (and (> 0 ....0) (> ..0 ..0)));
(not (and (= 0 ....0) (= .....0 .0)));
(not (and (< ..0 ....0) (< ...0 .0)));
(and (< ...0 ......0) (> ........0 .....0));
(not (and (> ......0 ...0) (> ..0 ...0)));
(not (and (> .0 0) (< ...0 ..0)));
(and (< 0 ..0) (> .0 0));
(not (and (= ....0 .0) (> 0 ...0)));
(not (and (> .....0 ......0) (= ..0 ..0)));
(not (and (= ..0 .0) (> .0 ...0)));
(not (and (> ....0 ....0) (= .0 .0)));
(not (and (> ..0 ..0) (< .....0 ......0)));
# MATH introduce the OR logical operator
(intro or);
(or (= .....0 .....0) (> ......0 ...0));
(or (< .0 ..0) (> ..0 0));
(or (> ....0 .0) (< ..0 ....0));
(or (< .0 ....0) (> .0 0));
(or (< ....0 .....0) (= 0 0));
(or (> .....0 ..0) (= .....0 .....0));
(or (> .....0 ..0) (> ......0 .....0));
(or (< .....0 ........0) (< .....0 ........0));
(or (= 0 0) (= ..0 ..0));
(or (< 0 ...0) (= 0 0));
(or (< 0 ..0) (= ....0 ..0));
(or (> ...0 .0) (= 0 ..0));
(or (= .....0 .....0) (= .0 .....0));
(or (< ..0 ....0) (< ......0 .....0));
(or (> .....0 ...0) (> ..0 ....0));
(or (> 0 ....0) (= 0 0));
(or (= ..0 0) (< 0 ..0));
(or (< ......0 ..0) (< .....0 .......0));
(or (= ..0 0) (= 0 0));
(or (> .....0 ......0) (< .0 ..0));
(not (or (> .0 ......0) (> ....0 ....0)));
(not (or (> ..0 ......0) (> ..0 .....0)));
(not (or (> ...0 ....0) (= .0 0)));
(not (or (> ...0 ...0) (< .....0 ...0)));
(not (or (= .....0 ....0) (> 0 0)));
(not (or (> 0 .0) (< .....0 ..0)));
(not (or (> .0 ......0) (< ..0 0)));
(or (> 0 ...0) (> ....0 ...0));
(or (< ....0 0) (< .....0 ........0));
(or (= ...0 ...0) (= ..0 ..0));
(not (or (< .....0 ...0) (< ..0 .0)));
(or (> ....0 .0) (> .0 ......0));
(or (< ....0 ...0) (= ....0 ....0));
(not (or (> 0 0) (= ..0 ...0)));
(or (> .....0 ..0) (< ...0 .0));
# MATH use equality for truth values
(= (> ....0 ..0) (> .....0 ....0));
(= (= ..0 ..0) (< ....0 .......0));
(= (> ......0 .....0) (> ...0 .0));
(= (> .....0 ....0) (< .....0 ......0));
(= (= ..0 ..0) (< ....0 ......0));
(= (= ...0 ..0) (= .0 0));
(= (> 0 .0) (< ....0 .0));
(= (> .0 .....0) (> ...0 ...0));
(= (> ..0 .....0) (< .0 0));
(= (= ...0 ....0) (= 0 ....0));
(not (= (= .0 0) (< .....0 ......0)));
(not (= (= .....0 ..0) (= 0 0)));
(not (= (< .....0 ..0) (= .....0 .....0)));
(not (= (= 0 .0) (> .....0 ....0)));
(not (= (> .0 ....0) (< ...0 ....0)));
(not (= (> ......0 ...0) (= ....0 .0)));
(not (= (< ....0 ......0) (> ...0 ....0)));
(not (= (< 0 ..0) (= .....0 ....0)));
(not (= (> ......0 ....0) (< ..0 0)));
(not (= (< ....0 .....0) (= ...0 0)));
(intro true);
(intro false);
(= true (= ...0 ...0));
(= true (= 0 0));
(= true (> .....0 ..0));
(= true (< ...0 ....0));
(= true (> ........0 .....0));
(= (< .0 ....0) true);
(= (< ...0 ....0) true);
(= (= ...0 ...0) true);
(= (< ...0 ....0) true);
(= (= ....0 ....0) true);
(= false (> ..0 ......0));
(= false (= ..0 ....0));
(= false (< ..0 0));
(= false (> ...0 ......0));
(= false (< ....0 ...0));
(= (> ..0 .....0) false);
(= (= ..0 .0) false);
(= (= ..0 .....0) false);
(= (< ......0 ..0) false);
(= (< ...0 .0) false);
(= true true);
(= false false);
(not (= true false));
(not (= false true));
# MATH introduce addition
(intro +);
(= (+ ...0 ....0) .......0);
(= (+ 0 ...0) ...0);
(= (+ 0 ...0) ...0);
(= (+ .0 0) .0);
(= (+ 0 0) 0);
(= (+ .0 ...0) ....0);
(= (+ .0 0) .0);
(= (+ .0 0) .0);
(= (+ ..0 ...0) .....0);
(= (+ 0 0) 0);
# MATH introduce subtraction
(intro -);
(= (- ......0 ...0) ...0);
(= (- .......0 ...0) ....0);
(= (- .......0 ....0) ...0);
(= (- .....0 ..0) ...0);
(= (- .0 .0) 0);
(= (- 0 0) 0);
(= (- ..0 0) ..0);
(= (- .......0 ...0) ....0);
(= (- ....0 ....0) 0);
(= (- ...0 0) ...0);
# MATH introduce multiplication
(intro *);
(= (* 0 0) 0);
(= (* 0 .0) 0);
(= (* 0 ..0) 0);
(= (* 0 ...0) 0);
(= (* .0 0) 0);
(= (* .0 .0) .0);
(= (* .0 ..0) ..0);
(= (* .0 ...0) ...0);
(= (* ..0 0) 0);
(= (* ..0 .0) ..0);
(= (* ..0 ..0) ....0);
(= (* ..0 ...0) ......0);
(= (* ...0 0) 0);
(= (* ...0 .0) ...0);
(= (* ...0 ..0) ......0);
(= (* ...0 ...0) .........0);
(= (* ...0 0) 0);
(= (* 0 .0) 0);
(= (* 0 .0) 0);
(= (* 0 .0) 0);
(= (* 0 ..0) 0);
(= (* ...0 .0) ...0);
(= (* ...0 ...0) .........0);
(= (* .0 ..0) ..0);
(= (* 0 .0) 0);
(= (* 0 ...0) 0);
# MATH introduce doubling as a special case of multiplication
# as prelude to binary representation
(intro :);
(= (: 0) 0);
(= (: .0) ..0);
(= (: ..0) ....0);
(= (: ...0) ......0);
(= (: ....0) ........0);
(= 0 (: 0));
(= ..0 (: .0));
(= ....0 (: ..0));
(= ......0 (: ...0));
(= ........0 (: ....0));
(= (* 0 ..0) (: 0));
(= (* .0 ..0) (: .0));
(= (* ..0 ..0) (: ..0));
(= (* ...0 ..0) (: ...0));
(= (* ....0 ..0) (: ....0));
(= :0 (: 0));
(= :.0 (: .0));
(= :..0 (: ..0));
(= :...0 (: ...0));
(= :....0 (: ....0));
# MATH introduce a simple form of binary notation
# After this lesson, in the higher-level version of the message,
# will expand decimal to stand for the binary notation given.
(= 0 0);
(= .0 .0);
(= ..0 :.0);
(= ...0 .:.0);
(= ....0 ::.0);
(= .....0 .::.0);
(= ......0 :.:.0);
(= .......0 .:.:.0);
(= ........0 :::.0);
(= .........0 .:::.0);
(= ..........0 :.::.0);
(= ...........0 .:.::.0);
(= ............0 ::.:.0);
(= .............0 .::.:.0);
(= ..............0 :.:.:.0);
(= ...............0 .:.:.:.0);
(= .::.:.0 .............0);
(= .:.0 ...0);
(= .::.:.0 .............0);
(= .::.0 .....0);
(= .:::.0 .........0);
(= .::.:.0 .............0);
(= .::.0 .....0);
(= .:.:.:.0 ...............0);
(= .:::.0 .........0);
(= :.:.0 ......0);
(= .:.:.0 .......0);
(= ::.0 ....0);
(= .::.:.0 .............0);
(= .:.:.0 .......0);
(= :.:.:.0 ..............0);
(= .::.0 .....0);
(= (+ :.0 .::.0) .:.:.0);
(= (+ :.:.0 :.:.0) ::.:.0);
(= (+ ::.:.0 .:.0) .:.:.:.0);
(= (+ :.0 .:.0) .::.0);
(= (+ :::.0 :::.0) ::::.0);
(= (+ .::.:.0 :.:.:.0) .:.::.:.0);
(= (+ .:.:.0 :.::.0) .::::.0);
(= (+ ::.:.0 .:.::.0) .:.:.::.0);
(= (* .::.:.0 .:::.0) .::.::.:.:.0);
(= (* ::.:.0 .::.:.0) ::.:.:.:::.0);
(= (* ::.:.0 :.::.0) :::.:.:.:.0);
(= (* ::.:.0 .:.:.:.0) ::.::.:.::.0);
(= (* .0 :.:.0) :.:.0);
(= (* :.:.0 :.::.0) ::.:.:.:.0);
(= (* ::.0 :.:.:.0) :::.:.:.0);
(= (* .:.:.:.0 .:::.0) .:.:.:::::.0);
# MATH demonstrate idea of leaving gaps in an expression
# and then filling them in afterwards
# the examples given leave a lot to be desired!
((? x (= (+ 2 x) 13)) 11);
((? x (= (+ 11 x) 21)) 10);
((? x (= (+ 9 x) 11)) 2);
((? x (= (+ 12 x) 18)) 6);
((? x (= (+ 6 x) 20)) 14);
((? x (= (+ 8 x) 10)) 2);
((? x (= (+ 11 x) 18)) 7);
((? x (= (+ 8 x) 13)) 5);
(((? x (? y (= (* x y) 12))) 6) 2);
(((? x (? y (= (* x y) 84))) 12) 7);
(((? x (? y (= (* x y) 45))) 15) 3);
(((? x (? y (= (* x y) 18))) 3) 6);
(((? x (? y (= (* x y) 90))) 15) 6);
(((? x (? y (= (* x y) 36))) 3) 12);
(((? x (? y (= (* x y) 30))) 2) 15);
(((? x (? y (= (* x y) 32))) 8) 4);
((((? x (? y (? z (= (* x y) z)))) 11) 1) 11);
((((? x (? y (? z (= (* x y) z)))) 121) 11) 11);
((((? x (? y (? z (= (* x y) z)))) 156) 12) 13);
((((? x (? y (? z (= (* x y) z)))) 16) 2) 8);
((((? x (? y (? z (= (* x y) z)))) 0) 4) 0);
((((? x (? y (? z (= (* x y) z)))) 108) 12) 9);
((((? x (? y (? z (= (* x y) z)))) 80) 10) 8);
((((? x (? y (? z (= (* x y) z)))) 8) 8) 1);
# MATH show some simple function calls
# and show a way to remember functions across statements
(= ((? square (square 1)) (? x (* x x))) 1);
(= ((? square (square 2)) (? x (* x x))) 4);
(= ((? square (square 0)) (? x (* x x))) 0);
(= ((? square (square 8)) (? x (* x x))) 64);
(= ((? square (square 5)) (? x (* x x))) 25);
(= ((? square (square 1)) (? x (* x x))) 1);
(= ((? square (square 8)) (? x (* x x))) 64);
(= ((? square (square 3)) (? x (* x x))) 9);
(define square (? x (* x x)));
(= (square 0) 0);
(= (square 7) 49);
(= (square 5) 25);
(= (square 6) 36);
(define plusone (? x (+ x 1)));
(= (plusone 7) 8);
(= (plusone 3) 4);
(= (plusone 6) 7);
(= (plusone 9) 10);
# MATH show mechanisms for branching
(intro if);
(= (if true 8 4) 8);
(= (if true 0 0) 0);
(= (if true 2 7) 2);
(= (if true 9 7) 9);
(= (if true 0 3) 0);
(= (if true 0 4) 0);
(= (if true 4 9) 4);
(= (if false 7 9) 9);
(= (if false 0 8) 8);
(= (if false 6 3) 3);
(= (if false 2 8) 8);
(= (if false 0 3) 3);
(= (if true 8 0) 8);
(= (if false 2 1) 1);
(= (if true 4 7) 4);
(= (if false 2 6) 6);
# MATH show an example of recursive evaluation
# skipping over a lot of definitions and desugarings
(define factorial (? x (if (> x 0) (* x (factorial (- x 1))) 1)));
(= (factorial 0) 1);
(= (factorial 1) 1);
(= (factorial 2) 2);
(= (factorial 3) 6);
(= (factorial 4) 24);
(= (factorial 5) 120);
# MATH introduce universal quantifier
# really need to link with sets for true correctness
# and the examples here are REALLY sparse, need much more
(intro forall);
(< 5 (+ 5 1));
(< 4 (+ 4 1));
(< 3 (+ 3 1));
(< 2 (+ 2 1));
(< 1 (+ 1 1));
(< 0 (+ 0 1));
(forall (? x (< x (+ x 1))));
(< 5 (* 5 2));
(< 4 (* 4 2));
(< 3 (* 3 2));
(< 2 (* 2 2));
(< 1 (* 1 2));
(not (< 0 (* 0 2)));
(not (forall (? x (< x (* x 2)))));
# MATH introduce existential quantifier
# really need to link with sets for true correctness
# and the examples here are REALLY sparse, need much more
(not (= 5 (* 2 2)));
(= 4 (* 2 2));
(not (= 3 (* 2 2)));
(not (= 2 (* 2 2)));
(not (= 1 (* 2 2)));
(not (= 0 (* 2 2)));
(intro exists);
(exists (? x (= x (* 2 2))));
(not (= 5 (+ 5 2)));
(not (= 4 (+ 4 2)));
(not (= 3 (+ 3 2)));
(not (= 2 (+ 2 2)));
(not (= 1 (+ 1 2)));
(not (= 0 (+ 0 2)));
(not (exists (? x (= x (+ x 2)))));
# MATH introduce logical implication
(intro =>);
(=> true true);
(not (=> true false));
(=> false true);
(=> false false);
(forall x (forall y (=> (=> x y) (=> (not y) (not x)))));
# MATH introduce sets and set membership
(element 7 (set 1 7 9 2));
(element 1 (set 1 7 9 2));
(element 7 (set 1 7 9 2));
(element 6 (set 6 3 9 2 5));
(element 2 (set 6 3 9 2 5));
(element 5 (set 6 3 9 2 5));
(element 6 (set 6 0 7 9));
(element 7 (set 6 0 7 9));
(element 9 (set 6 0 7 9));
(element 0 (set 8 0 7 9 5));
(element 5 (set 8 0 7 9 5));
(element 5 (set 8 0 7 9 5));
(element 2 (set 7 9 2 5));
(element 2 (set 7 9 2 5));
(element 5 (set 7 9 2 5));
(not (element 6 (set 4 2 5)));
(not (element 8 (set 1 9 2 5)));
(not (element 6 (set 4 0 7 9 5)));
(not (element 8 (set 6 1 2 5)));
(not (element 6 (set 8 3 7 2)));
(= (set 1 5 9) (set 5 1 9));
(= (set 1 5 9) (set 9 1 5));
(not (= (set 1 5 9) (set 1 5)));
(element 5 (all (? x (= (+ x 10) 15))));
(element 3 (all (? x (= (* x 3) (+ x 6)))));
(define empty_set (set));
(element 0 natural_set);
(forall (? x (=> (element x natural_set) (element (+ x 1) natural_set))));
(element 1 natural_set);
(element 2 natural_set);
(element 3 natural_set);
(element 4 natural_set);
(element 5 natural_set);
(element 6 natural_set);
(element 7 natural_set);
(element 8 natural_set);
(element 9 natural_set);
(not (element true natural_set));
(not (element false natural_set));
(define boolean_set (set true false));
(element true boolean_set);
(element false boolean_set);
(not (element 0 boolean_set));
(define even_natural_set (all (? x (exists (? y (and (element y natural_set) (equals (* 2 y) x)))))));
(element 0 natural_set);
(element 0 even_natural_set);
(element 1 natural_set);
(not (element 1 even_natural_set));
(element 2 natural_set);
(element 2 even_natural_set);
(element 3 natural_set);
(not (element 3 even_natural_set));
(element 4 natural_set);
(element 4 even_natural_set);
(element 5 natural_set);
(not (element 5 even_natural_set));
(element 6 natural_set);
(element 6 even_natural_set);
# MATH illustrate lists and some list operators
# still using examples rather than definition by formula -
# could change this to reduce ambiguity, but that would create
# more order constraints in the lessons
(= (head (list 0)) 0);
(= (tail (list 0)) (list));
(= (head (list 6 11 19)) 6);
(= (tail (list 6 11 19)) (list 11 19));
(= (head (list 12 2 15)) 12);
(= (tail (list 12 2 15)) (list 2 15));
(= (head (list 19 3 4 4 2 15 3)) 19);
(= (tail (list 19 3 4 4 2 15 3)) (list 3 4 4 2 15 3));
(= (head (list 6 11 3 2 15 2 19 15 12)) 6);
(= (tail (list 6 11 3 2 15 2 19 15 12)) (list 11 3 2 15 2 19 15 12));
(= (head (list 11 0 12 14 8 17 5 9 11)) 11);
(= (tail (list 11 0 12 14 8 17 5 9 11)) (list 0 12 14 8 17 5 9 11));
(= (head (list 10)) 10);
(= (tail (list 10)) (list));
(= (head (list 9 4 19 10)) 9);
(= (tail (list 9 4 19 10)) (list 4 19 10));
(= (head (list 8 4 2 7 12 18 9 13)) 8);
(= (tail (list 8 4 2 7 12 18 9 13)) (list 4 2 7 12 18 9 13));
(= (head (list 0)) 0);
(= (tail (list 0)) (list));
(= (list-ref (list 10 1 9) 2) 9);
(= (list-ref (list 4 4 14 0 14 4 17 7 3 17) 0) 4);
(= (list-ref (list 10 13 6 14 3 13 9 18) 0) 10);
(= (list-ref (list 3 1 0 2) 2) 0);
(= (list-ref (list 13 7 18 13 12) 1) 7);
(= (list-ref (list 19 16 9) 2) 9);
(= (list-ref (list 12 14 5 14 4) 4) 4);
(= (list-ref (list 10 17) 1) 17);
(= (list-ref (list 1 12 10 18) 3) 18);
(= (list-ref (list 17 7 2 4 19 15 4 9) 0) 17);
(= (list) (list));
(= (list 7) (list 7));
(= (list 1 19) (list 1 19));
(= (list 18 1 18) (list 18 1 18));
(= (list 13 15 10 6) (list 13 15 10 6));
# this next batch of examples are a bit misleading, should streamline
(not (= (list) (list 0)));
(not (= (list) (list 6)));
(not (= (list 9) (list 6 9)));
(not (= (list 9) (list 9 7)));
(not (= (list 1 6) (list 2 1 6)));
(not (= (list 1 6) (list 1 6 0)));
(not (= (list 10 9 12) (list 5 10 9 12)));
(not (= (list 10 9 12) (list 10 9 12 3)));
(not (= (list 17 9 1 0) (list 4 17 9 1 0)));
(not (= (list 17 9 1 0) (list 17 9 1 0 4)));
# some helpful functions
(define list-length (? x (if (= x (list)) 0 (+ 1 (list-length (tail x))))));
(= (list-length (list 3 7 5 2 4 9)) 6);
(= (list-length (list 2 4 0 6 9 7 8 1 5)) 9);
(= (list-length (list)) 0);
(= (list-length (list 2 1 9)) 3);
(= (list-length (list 3 9 8 7 2)) 5);
(define pair (? x (? y (list x y))));
(= (pair 4 5) (list 4 5));
(= (first (pair 4 5)) 4);
(= (second (pair 4 5)) 5);
(= (pair 2 0) (list 2 0));
(= (first (pair 2 0)) 2);
(= (second (pair 2 0)) 0);
(= (pair 3 2) (list 3 2));
(= (first (pair 3 2)) 3);
(= (second (pair 3 2)) 2);
# MATH build up functions of several variables
# there should be nothing actually new here, if the basic
# symbols are interpreted correctly - but this isn't obvious
(= ((?x?y (- x y)) 9 7) 2);
(= ((?x?y (- x y)) 6 3) 3);
(= ((?x?y (- x y)) 9 9) 0);
(= ((?x?y (- x y)) 4 1) 3);
(= ((?x?y (- x y)) 15 6) 9);
(define apply (?x?y (if (= y (list)) x (apply (x (head y)) (tail y)))));
(= (apply (?x?y (- x y)) (list 9 3)) 6);
(= (apply (?x?y (- x y)) (list 11 2)) 9);
(= (apply (?x?y (- x y)) (list 7 4)) 3);
(= (apply (?x?y (- x y)) (list 5 5)) 0);
(= (apply (?x?y (- x y)) (list 6 1)) 5);
# MATH introduce environment/hashmap structure
# note that something written as {name} is just converted to a number
# it does NOT yield an identifier
# this section needs a LOT more examples :-)
(define hash-add (?h?x?y?z (if (= z x) y (h z))));
(define hash-ref (?h?x (h x)));
(define hash-null (? z undefined));
(define test-hash (hash-add (hash-add hash-null 3 2) 4 9));
(= (hash-ref test-hash 4) 9);
(= (hash-ref test-hash 3) 2);
(= (hash-ref test-hash 8) undefined);
(= (hash-ref test-hash 15) undefined);
(= (hash-ref (hash-add test-hash 15 33) 15) 33);
(= (hash-ref test-hash 15) undefined);
(define make-hash (? x (= x (list)) hash-null (hash-add (make-hash (tail x)) (first (head x)) (second (head x)))));
(= (hash-ref (make-hash (list (pair 3 10) (pair 2 20) (pair 1 30))) 3) 10);
(= (hash-ref (make-hash (list (pair 3 10) (pair 2 20) (pair 1 30))) 1) 30);
# MATH introduce mutable objects, and side-effects
(intro make-cell);
(intro set!);
(intro get!);
(define demo-mut1 (make-cell 0));
(set! demo-mut1 15);
(= (get! demo-mut1) 15);
(set! demo-mut1 5);
(set! demo-mut1 7);
(= (get! demo-mut1) 7);
(define demo-mut2 (make-cell 11));
(= (get! demo-mut2) 11);
(set! demo-mut2 22);
(= (get! demo-mut2) 22);
(= (get! demo-mut1) 7);
(= (+ (get! demo-mut1) (get! demo-mut2)) 29);
(if (= (get! demo-mut1) 7) (set! demo-mut1 88) (set! demo-mut1 99));
(= (get! demo-mut1) 88);
(if (= (get! demo-mut1) 7) (set! demo-mut1 88) (set! demo-mut1 99));
(= (get! demo-mut1) 99);
# MUD under development
# need a lot more structure/record/object abstractions
# adding these to MATH section...
# currently just use this section to play around
(intro reflect);
(define reflect (? x (x x)));