# 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)
[
hear] (intro (unary 0));
[hear] (intro (unary 1 0));
[hear] (intro (unary 1 1 0));
[hear] (intro (unary 1 1 1 0));
[hear] (intro (unary 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 0));
[hear] (intro (unary 1 1 1 0));
[hear] (intro (unary 1 1 0));
[hear] (intro (unary 1 0));
[hear] (intro (unary 0));
[hear] (intro (unary 0));
[hear] (intro (unary 1 0));
[hear] (intro (unary 1 1 0));
[hear] (intro (unary 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 0));
[hear] (intro (unary 1 0));
[hear] (intro (unary 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 0));
[hear] (intro (unary 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
       # MATH now show equality
[
hear] (intro =);
[hear] (= (unary 0) (unary 0));
[hear] (= (unary 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0));
[hear] (= (unary 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
       # MATH now show other relational operators
[
hear] (intro >);
[hear] (> (unary 1 1 1 0) (unary 1 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 1 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 0) (unary 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 1 1 0) (unary 1 0));
[hear] (> (unary 1 1 1 1 1 1 0) (unary 1 1 0));
[hear] (> (unary 1 1 1 0) (unary 1 0));
[hear] (> (unary 1 1 1 1 1 0) (unary 0));
[hear] (intro <);
[hear] (< (unary 0) (unary 1 1 1 1 1 1 0));
[hear] (< (unary 0) (unary 1 0));
[hear] (< (unary 0) (unary 1 0));
[hear] (< (unary 0) (unary 1 1 0));
[hear] (< (unary 1 0) (unary 1 1 1 0));
[hear] (< (unary 0) (unary 1 1 0));
[hear] (< (unary 1 1 0) (unary 1 1 1 1 0));
[hear] (< (unary 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (< (unary 0) (unary 1 1 0));
[hear] (< (unary 0) (unary 1 1 1 1 1 0));
[hear] (< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0));
[hear] (< (unary 1 1 0) (unary 1 1 1 0));
[hear] (> (unary 1 1 0) (unary 1 0));
[hear] (> (unary 1 1 1 1 1 0) (unary 1 0));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (< (unary 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (> (unary 1 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (< (unary 1 1 1 0) (unary 1 1 1 1 1 0));
       # MATH introduce the NOT logical operator
[
hear] (intro not);
[hear] (= (unary 1 0) (unary 1 0));
[hear] (not (< (unary 1 0) (unary 1 0)));
[hear] (not (> (unary 1 0) (unary 1 0)));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (not (< (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (not (> (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (unary 0) (unary 0));
[hear] (not (< (unary 0) (unary 0)));
[hear] (not (> (unary 0) (unary 0)));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (not (< (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (not (> (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (unary 1 0) (unary 1 0));
[hear] (not (< (unary 1 0) (unary 1 0)));
[hear] (not (> (unary 1 0) (unary 1 0)));
[hear] (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not (= (unary 1 0) (unary 1 1 1 1 0)));
[hear] (< (unary 1 0) (unary 1 1 1 1 0));
[hear] (not (> (unary 1 0) (unary 1 1 1 1 0)));
[hear] (not (= (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (< (unary 1 1 0) (unary 1 1 1 1 0));
[hear] (not (> (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0));
[hear] (not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0));
[hear] (not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (not (= (unary 1 0) (unary 1 1 1 0)));
[hear] (< (unary 1 0) (unary 1 1 1 0));
[hear] (not (> (unary 1 0) (unary 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0));
[hear] (not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 0) (unary 1 0)));
[hear] (> (unary 1 1 1 0) (unary 1 0));
[hear] (not (< (unary 1 1 1 0) (unary 1 0)));
[hear] (not (= (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)));
       # MATH introduce the AND logical operator
[
hear] (intro and);
[hear] (and (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0))
            (> (unary 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (and (= (unary 1 0) (unary 1 0))
            (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (and (> (unary 1 1 1 1 0) (unary 1 1 1 0))
            (> (unary 1 1 1 1 0) (unary 1 0)));
[hear] (and (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
            (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (and (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
            (= (unary 1 1 0) (unary 1 1 0)));
[hear] (and (< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0))
            (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (and (= (unary 1 1 0) (unary 1 1 0))
            (< (unary 0) (unary 1 1 0)));
[hear] (and (> (unary 1 1 1 1 1 0) (unary 1 1 0))
            (= (unary 1 1 0) (unary 1 1 0)));
[hear] (and (< (unary 1 0) (unary 1 1 1 1 0))
            (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (and (< (unary 1 0) (unary 1 1 0))
            (= (unary 1 1 0) (unary 1 1 0)));
[hear] (not (and (> (unary 1 1 1 1 0) (unary 1 1 1 0)) (> (unary 0) (unary 1 0))));
[hear] (not
        (and (< (unary 1 1 1 0) (unary 1 1 1 1 1 0))
             (= (unary 1 1 0) (unary 1 1 1 1 0))));
[hear] (not
        (and (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
             (> (unary 1 0) (unary 1 1 1 1 1 0))));
[hear] (not
        (and (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
             (= (unary 1 1 1 0) (unary 1 1 1 1 1 0))));
[hear] (not (and (= (unary 1 0) (unary 1 0)) (< (unary 1 1 1 1 1 0) (unary 1 1 0))));
[hear] (not (and (> (unary 1 1 0) (unary 1 1 1 0)) (< (unary 1 0) (unary 1 1 1 0))));
[hear] (not
        (and (< (unary 1 1 1 1 1 1 0) (unary 1 0))
             (> (unary 1 1 1 0) (unary 1 1 0))));
[hear] (not
        (and (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))
             (> (unary 1 1 0) (unary 0))));
[hear] (not
        (and (= (unary 1 0) (unary 0))
             (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0))));
[hear] (not
        (and (> (unary 1 1 1 0) (unary 1 1 1 1 1 0))
             (< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0))));
[hear] (not
        (and (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))
             (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))));
[hear] (not (and (= (unary 1 1 1 1 0) (unary 0)) (> (unary 0) (unary 1 1 1 0))));
[hear] (not
        (and (= (unary 1 1 1 1 1 0) (unary 0))
             (> (unary 1 1 1 0) (unary 1 1 1 0))));
[hear] (not (and (> (unary 0) (unary 1 1 1 1 0)) (> (unary 1 1 0) (unary 1 1 0))));
[hear] (not (and (= (unary 0) (unary 1 1 1 1 0)) (= (unary 1 1 1 1 1 0) (unary 1 0))));
[hear] (not (and (< (unary 1 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 1 0) (unary 1 0))));
[hear] (and (< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0))
            (> (unary 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not
        (and (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0))
             (> (unary 1 1 0) (unary 1 1 1 0))));
[hear] (not (and (> (unary 1 0) (unary 0)) (< (unary 1 1 1 0) (unary 1 1 0))));
[hear] (and (< (unary 0) (unary 1 1 0))
            (> (unary 1 0) (unary 0)));
[hear] (not (and (= (unary 1 1 1 1 0) (unary 1 0)) (> (unary 0) (unary 1 1 1 0))));
[hear] (not
        (and (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
             (= (unary 1 1 0) (unary 1 1 0))));
[hear] (not (and (= (unary 1 1 0) (unary 1 0)) (> (unary 1 0) (unary 1 1 1 0))));
[hear] (not (and (> (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 1 0) (unary 1 0))));
[hear] (not
        (and (> (unary 1 1 0) (unary 1 1 0))
             (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))));
       # MATH introduce the OR logical operator
[
hear] (intro or);
[hear] (or (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
           (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (or (< (unary 1 0) (unary 1 1 0))
           (> (unary 1 1 0) (unary 0)));
[hear] (or (> (unary 1 1 1 1 0) (unary 1 0))
           (< (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (or (< (unary 1 0) (unary 1 1 1 1 0))
           (> (unary 1 0) (unary 0)));
[hear] (or (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0))
           (= (unary 0) (unary 0)));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 0))
           (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 0))
           (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 1 0))
           (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 1 0)));
[hear] (or (= (unary 0) (unary 0))
           (= (unary 1 1 0) (unary 1 1 0)));
[hear] (or (< (unary 0) (unary 1 1 1 0))
           (= (unary 0) (unary 0)));
[hear] (or (< (unary 0) (unary 1 1 0))
           (= (unary 1 1 1 1 0) (unary 1 1 0)));
[hear] (or (> (unary 1 1 1 0) (unary 1 0))
           (= (unary 0) (unary 1 1 0)));
[hear] (or (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
           (= (unary 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (< (unary 1 1 0) (unary 1 1 1 1 0))
           (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 1 0))
           (> (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (or (> (unary 0) (unary 1 1 1 1 0))
           (= (unary 0) (unary 0)));
[hear] (or (= (unary 1 1 0) (unary 0))
           (< (unary 0) (unary 1 1 0)));
[hear] (or (< (unary 1 1 1 1 1 1 0) (unary 1 1 0))
           (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (or (= (unary 1 1 0) (unary 0))
           (= (unary 0) (unary 0)));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
           (< (unary 1 0) (unary 1 1 0)));
[hear] (not
        (or (> (unary 1 0) (unary 1 1 1 1 1 1 0))
            (> (unary 1 1 1 1 0) (unary 1 1 1 1 0))));
[hear] (not
        (or (> (unary 1 1 0) (unary 1 1 1 1 1 1 0))
            (> (unary 1 1 0) (unary 1 1 1 1 1 0))));
[hear] (not (or (> (unary 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 1 0) (unary 0))));
[hear] (not
        (or (> (unary 1 1 1 0) (unary 1 1 1 0))
            (< (unary 1 1 1 1 1 0) (unary 1 1 1 0))));
[hear] (not (or (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)) (> (unary 0) (unary 0))));
[hear] (not (or (> (unary 0) (unary 1 0)) (< (unary 1 1 1 1 1 0) (unary 1 1 0))));
[hear] (not (or (> (unary 1 0) (unary 1 1 1 1 1 1 0)) (< (unary 1 1 0) (unary 0))));
[hear] (or (> (unary 0) (unary 1 1 1 0))
           (> (unary 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (or (< (unary 1 1 1 1 0) (unary 0))
           (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 1 0)));
[hear] (or (= (unary 1 1 1 0) (unary 1 1 1 0))
           (= (unary 1 1 0) (unary 1 1 0)));
[hear] (not
        (or (< (unary 1 1 1 1 1 0) (unary 1 1 1 0))
            (< (unary 1 1 0) (unary 1 0))));
[hear] (or (> (unary 1 1 1 1 0) (unary 1 0))
           (> (unary 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (or (< (unary 1 1 1 1 0) (unary 1 1 1 0))
           (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (not (or (> (unary 0) (unary 0)) (= (unary 1 1 0) (unary 1 1 1 0))));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 0))
           (< (unary 1 1 1 0) (unary 1 0)));
       # MATH use equality for truth values
[
hear] (= (> (unary 1 1 1 1 0) (unary 1 1 0))
          (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (= (= (unary 1 1 0) (unary 1 1 0))
          (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (= (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
          (> (unary 1 1 1 0) (unary 1 0)));
[hear] (= (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))
          (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (= (= (unary 1 1 0) (unary 1 1 0)) (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (= (= (unary 1 1 1 0) (unary 1 1 0)) (= (unary 1 0) (unary 0)));
[hear] (= (> (unary 0) (unary 1 0)) (< (unary 1 1 1 1 0) (unary 1 0)));
[hear] (= (> (unary 1 0) (unary 1 1 1 1 1 0)) (> (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (> (unary 1 1 0) (unary 1 1 1 1 1 0)) (< (unary 1 0) (unary 0)));
[hear] (= (= (unary 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 0) (unary 1 1 1 1 0)));
[hear] (not
        (= (= (unary 1 0) (unary 0)) (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))));
[hear] (not (= (= (unary 1 1 1 1 1 0) (unary 1 1 0)) (= (unary 0) (unary 0))));
[hear] (not
        (= (< (unary 1 1 1 1 1 0) (unary 1 1 0))
           (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))));
[hear] (not (= (= (unary 0) (unary 1 0)) (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))));
[hear] (not
        (= (> (unary 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 1 0) (unary 1 1 1 1 0))));
[hear] (not
        (= (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0))
           (= (unary 1 1 1 1 0) (unary 1 0))));
[hear] (not
        (= (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
           (> (unary 1 1 1 0) (unary 1 1 1 1 0))));
[hear] (not (= (< (unary 0) (unary 1 1 0)) (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))));
[hear] (not
        (= (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 0) (unary 0))));
[hear] (not
        (= (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0)) (= (unary 1 1 1 0) (unary 0))));
[hear] (intro true);
[hear] (intro false);
[hear] (= (true) (= (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (true) (= (unary 0) (unary 0)));
[hear] (= (true) (> (unary 1 1 1 1 1 0) (unary 1 1 0)));
[hear] (= (true) (< (unary 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (= (true) (> (unary 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (= (< (unary 1 0) (unary 1 1 1 1 0)) (true));
[hear] (= (< (unary 1 1 1 0) (unary 1 1 1 1 0)) (true));
[hear] (= (= (unary 1 1 1 0) (unary 1 1 1 0)) (true));
[hear] (= (< (unary 1 1 1 0) (unary 1 1 1 1 0)) (true));
[hear] (= (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (true));
[hear] (= (false) (> (unary 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (= (false) (= (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (= (false) (< (unary 1 1 0) (unary 0)));
[hear] (= (false) (> (unary 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (= (false) (< (unary 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (> (unary 1 1 0) (unary 1 1 1 1 1 0)) (false));
[hear] (= (= (unary 1 1 0) (unary 1 0)) (false));
[hear] (= (= (unary 1 1 0) (unary 1 1 1 1 1 0)) (false));
[hear] (= (< (unary 1 1 1 1 1 1 0) (unary 1 1 0)) (false));
[hear] (= (< (unary 1 1 1 0) (unary 1 0)) (false));
[hear] (= (true) (true));
[hear] (= (false) (false));
[hear] (not (= (true) (false)));
[hear] (not (= (false) (true)));
       # MATH introduce addition
[
hear] (intro +);
[hear] (= (+ (unary 1 1 1 0) (unary 1 1 1 1 0)) (unary 1 1 1 1 1 1 1 0));
[hear] (= (+ (unary 0) (unary 1 1 1 0)) (unary 1 1 1 0));
[hear] (= (+ (unary 0) (unary 1 1 1 0)) (unary 1 1 1 0));
[hear] (= (+ (unary 1 0) (unary 0)) (unary 1 0));
[hear] (= (+ (unary 0) (unary 0)) (unary 0));
[hear] (= (+ (unary 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 0));
[hear] (= (+ (unary 1 0) (unary 0)) (unary 1 0));
[hear] (= (+ (unary 1 0) (unary 0)) (unary 1 0));
[hear] (= (+ (unary 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 0));
[hear] (= (+ (unary 0) (unary 0)) (unary 0));
       # MATH introduce subtraction
[
hear] (intro -);
[hear] (= (- (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 0));
[hear] (= (- (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 0));
[hear] (= (- (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0)) (unary 1 1 1 0));
[hear] (= (- (unary 1 1 1 1 1 0) (unary 1 1 0)) (unary 1 1 1 0));
[hear] (= (- (unary 1 0) (unary 1 0)) (unary 0));
[hear] (= (- (unary 0) (unary 0)) (unary 0));
[hear] (= (- (unary 1 1 0) (unary 0)) (unary 1 1 0));
[hear] (= (- (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 0));
[hear] (= (- (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (unary 0));
[hear] (= (- (unary 1 1 1 0) (unary 0)) (unary 1 1 1 0));
       # MATH introduce multiplication
[
hear] (intro *);
[hear] (= (* (unary 0) (unary 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 1 1 0)) (unary 0));
[hear] (= (* (unary 1 0) (unary 0)) (unary 0));
[hear] (= (* (unary 1 0) (unary 1 0)) (unary 1 0));
[hear] (= (* (unary 1 0) (unary 1 1 0)) (unary 1 1 0));
[hear] (= (* (unary 1 0) (unary 1 1 1 0)) (unary 1 1 1 0));
[hear] (= (* (unary 1 1 0) (unary 0)) (unary 0));
[hear] (= (* (unary 1 1 0) (unary 1 0)) (unary 1 1 0));
[hear] (= (* (unary 1 1 0) (unary 1 1 0)) (unary 1 1 1 1 0));
[hear] (= (* (unary 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 1 0));
[hear] (= (* (unary 1 1 1 0) (unary 0)) (unary 0));
[hear] (= (* (unary 1 1 1 0) (unary 1 0)) (unary 1 1 1 0));
[hear] (= (* (unary 1 1 1 0) (unary 1 1 0)) (unary 1 1 1 1 1 1 0));
[hear] (= (* (unary 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (= (* (unary 1 1 1 0) (unary 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 1 0)) (unary 0));
[hear] (= (* (unary 1 1 1 0) (unary 1 0)) (unary 1 1 1 0));
[hear] (= (* (unary 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (= (* (unary 1 0) (unary 1 1 0)) (unary 1 1 0));
[hear] (= (* (unary 0) (unary 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 1 1 0)) (unary 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.
[
hear] (= (unary 0) (.));
[hear] (= (unary 1 0) (:));
[hear] (= (unary 1 1 0) (:.));
[hear] (= (unary 1 1 1 0) (::));
[hear] (= (unary 1 1 1 1 0) (:..));
[hear] (= (unary 1 1 1 1 1 0) (:.:));
[hear] (= (unary 1 1 1 1 1 1 0) (::.));
[hear] (= (unary 1 1 1 1 1 1 1 0) (:::));
[hear] (= (unary 1 1 1 1 1 1 1 1 0) (:...));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 0) (:..:));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 0) (:.:.));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 0) (:.::));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 0) (::..));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (::.:));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (:::.));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (::::));
[hear] (= (::.:) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (::) (unary 1 1 1 0));
[hear] (= (::.:) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:.:) (unary 1 1 1 1 1 0));
[hear] (= (:..:) (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (= (::.:) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:.:) (unary 1 1 1 1 1 0));
[hear] (= (::::) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:..:) (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (= (::.) (unary 1 1 1 1 1 1 0));
[hear] (= (:::) (unary 1 1 1 1 1 1 1 0));
[hear] (= (:..) (unary 1 1 1 1 0));
[hear] (= (::.:) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:::) (unary 1 1 1 1 1 1 1 0));
[hear] (= (:::.) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:.:) (unary 1 1 1 1 1 0));
[hear] (= (+ (:.) (:.:)) (:::));
[hear] (= (+ (::.) (::.))
          (::..));
[hear] (= (+ (::..) (::))
          (::::));
[hear] (= (+ (:.) (::)) (:.:));
[hear] (= (+ (:...) (:...))
          (:....));
[hear] (= (+ (::.:) (:::.))
          (::.::));
[hear] (= (+ (:::) (:.:.))
          (:...:));
[hear] (= (+ (::..) (:.::))
          (:.:::));
[hear] (= (* (::.:) (:..:))
          (:::.:.:));
[hear] (= (* (::..) (::.:))
          (:..:::..));
[hear] (= (* (::..) (:.:.))
          (::::...));
[hear] (= (* (::..) (::::))
          (:.::.:..));
[hear] (= (* (:) (::.)) (::.));
[hear] (= (* (::.) (:.:.))
          (::::..));
[hear] (= (* (:..) (:::.))
          (:::...));
[hear] (= (* (::::) (:..:))
          (:....:::));
       # MATH demonstrate idea of leaving gaps in an expression
       # and then filling them in afterwards
       # the examples given leave a lot to be desired!
[
hear] ((? x (= (+ 2 (x)) 13)) 11);
[hear] ((? x (= (+ 11 (x)) 21)) 10);
[hear] ((? x (= (+ 9 (x)) 11)) 2);
[hear] ((? x (= (+ 12 (x)) 18)) 6);
[hear] ((? x (= (+ 6 (x)) 20)) 14);
[hear] ((? x (= (+ 8 (x)) 10)) 2);
[hear] ((? x (= (+ 11 (x)) 18)) 7);
[hear] ((? x (= (+ 8 (x)) 13)) 5);
[hear] (((? x (? y (= (* (x) (y)) 12))) 6) 2);
[hear] (((? x (? y (= (* (x) (y)) 84))) 12) 7);
[hear] (((? x (? y (= (* (x) (y)) 45))) 15) 3);
[hear] (((? x (? y (= (* (x) (y)) 18))) 3) 6);
[hear] (((? x (? y (= (* (x) (y)) 90))) 15) 6);
[hear] (((? x (? y (= (* (x) (y)) 36))) 3) 12);
[hear] (((? x (? y (= (* (x) (y)) 30))) 2) 15);
[hear] (((? x (? y (= (* (x) (y)) 32))) 8) 4);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 11) 1)
        11);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 121) 11)
        11);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 156) 12)
        13);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 16) 2)
        8);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 0) 4) 0);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 108) 12)
        9);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 80) 10)
        8);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 8) 8) 1);
       # MATH show some simple function calls
       # and show a way to remember functions across statements
[
hear] (= ((? square (square 1)) (? x (* (x) (x)))) 1);
[hear] (= ((? square (square 2)) (? x (* (x) (x)))) 4);
[hear] (= ((? square (square 0)) (? x (* (x) (x)))) 0);
[hear] (= ((? square (square 8)) (? x (* (x) (x)))) 64);
[hear] (= ((? square (square 5)) (? x (* (x) (x)))) 25);
[hear] (= ((? square (square 1)) (? x (* (x) (x)))) 1);
[hear] (= ((? square (square 8)) (? x (* (x) (x)))) 64);
[hear] (= ((? square (square 3)) (? x (* (x) (x)))) 9);
[hear] (define square (? x (* (x) (x))));
[hear] (= (square 0) 0);
[hear] (= (square 7) 49);
[hear] (= (square 5) 25);
[hear] (= (square 6) 36);
[hear] (define plusone (? x (+ (x) 1)));
[hear] (= (plusone 7) 8);
[hear] (= (plusone 3) 4);
[hear] (= (plusone 6) 7);
[hear] (= (plusone 9) 10);
       # MATH show mechanisms for branching
[
hear] (intro if);
[hear] (= (if (true) 8 4) 8);
[hear] (= (if (true) 0 0) 0);
[hear] (= (if (true) 2 7) 2);
[hear] (= (if (true) 9 7) 9);
[hear] (= (if (true) 0 3) 0);
[hear] (= (if (true) 0 4) 0);
[hear] (= (if (true) 4 9) 4);
[hear] (= (if (false) 7 9) 9);
[hear] (= (if (false) 0 8) 8);
[hear] (= (if (false) 6 3) 3);
[hear] (= (if (false) 2 8) 8);
[hear] (= (if (false) 0 3) 3);
[hear] (= (if (true) 8 0) 8);
[hear] (= (if (false) 2 1) 1);
[hear] (= (if (true) 4 7) 4);
[hear] (= (if (false) 2 6) 6);
       # MATH some pure lambda calculus definitions - optional
       # these definitions are not quite what we want
       # since thinking of everything as a function requires headscratching
       # it would be better to use these as a parallel means of evaluation
       # ... for expressions
[
hear] (define pure-if (? x (? y (? z (x (y) (z))))));
[hear] (define pure-true (? y (? z (y))));
[hear] (define pure-false (? y (? z (z))));
[hear] (define pure-cons
         (? x (? y (? z (pure-if (z) (x) (y))))));
[hear] (define pure-car (? x (x (pure-true))));
[hear] (define pure-cdr (? x (x (pure-false))));
[hear] (define zero (? f (? x (x))));
[hear] (define one (? f (? x (f (x)))));
[hear] (define two (? f (? x (f (f (x))))));
[hear] (define succ (? n (? f (? x (f ((n (f)) (x)))))));
[hear] (define add (? a (? b ((a (succ)) (b)))));
[hear] (define mult (? a (? b ((a (add (b))) (zero)))));
[hear] (define pred
         (? n
           (pure-cdr
             ((n (? p
                   (pure-cons (succ (pure-car (p))) (pure-car (p)))))
              (pure-cons (zero) (zero))))));
[hear] (define is-zero
         (? n ((n (? dummy (pure-false)) (pure-true)))));
[hear] (define fixed-point
         (? f ((? x (f (x (x)))) (? x (f (x (x)))))));
       # .. but for rest of message will assume that define does fixed-point for us
       # now build a link between numbers and church number functions
[hear] (define unchurch (? c (c (? x (+ (x) 1)) 0)));
[hear] (= 0 (unchurch (zero)));
[hear] (= 1 (unchurch (one)));
[hear] (= 2 (unchurch (two)));
[hear] (define church
         (? x
           (if (= 0 (x)) (zero) (succ (church (- (x) 1))))));
       # MATH show an example of recursive evaluation
       # skipping over a lot of definitions and desugarings
[
hear] (define easy-factorial
         (? f
           (? x (if (> (x) 0) (* (x) (f (f) (- (x) 1))) 1))));
[hear] (define factorial
         (? x
           (if (> (x) 0) (* (x) (factorial (- (x) 1))) 1)));
[hear] (= (easy-factorial (easy-factorial) 0) 1);
[hear] (= (easy-factorial (easy-factorial) 1) 1);
[hear] (= (easy-factorial (easy-factorial) 2) 2);
[hear] (= (easy-factorial (easy-factorial) 3) 6);
[hear] (= (easy-factorial (easy-factorial) 4) 24);
[hear] (= (easy-factorial (easy-factorial) 5) 120);
[hear] (= (factorial 0) 1);
[hear] (= (factorial 1) 1);
[hear] (= (factorial 2) 2);
[hear] (= (factorial 3) 6);
[hear] (= (factorial 4) 24);
[hear] (= (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
[
hear] (intro forall);
[hear] (< 5 (+ 5 1));
[hear] (< 4 (+ 4 1));
[hear] (< 3 (+ 3 1));
[hear] (< 2 (+ 2 1));
[hear] (< 1 (+ 1 1));
[hear] (< 0 (+ 0 1));
[hear] (forall (? x (< (x) (+ (x) 1))));
[hear] (< 5 (* 5 2));
[hear] (< 4 (* 4 2));
[hear] (< 3 (* 3 2));
[hear] (< 2 (* 2 2));
[hear] (< 1 (* 1 2));
[hear] (not (< 0 (* 0 2)));
[hear] (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
[
hear] (not (= 5 (* 2 2)));
[hear] (= 4 (* 2 2));
[hear] (not (= 3 (* 2 2)));
[hear] (not (= 2 (* 2 2)));
[hear] (not (= 1 (* 2 2)));
[hear] (not (= 0 (* 2 2)));
[hear] (intro exists);
[hear] (exists (? x (= (x) (* 2 2))));
[hear] (not (= 5 (+ 5 2)));
[hear] (not (= 4 (+ 4 2)));
[hear] (not (= 3 (+ 3 2)));
[hear] (not (= 2 (+ 2 2)));
[hear] (not (= 1 (+ 1 2)));
[hear] (not (= 0 (+ 0 2)));
[hear] (not (exists (? x (= (x) (+ (x) 2)))));
       # MATH introduce logical implication
[
hear] (intro =>);
[hear] (define => (? x (? y (not (and (x) (not (y)))))));
[hear] (=> (true) (true));
[hear] (not (=> (true) (false)));
[hear] (=> (false) (true));
[hear] (=> (false) (false));
[hear] (forall
         (? x
           (forall
             (? y (=> (=> (x) (y)) (=> (not (y)) (not (x))))))));
       # MATH illustrate lists and some list operators
       # to make list describable as a function, need to preceed lists
       # ... with an argument count
       # lists will be written as [1 2 1] = (list 3 1 2 1) after this lesson
       # it would be nice to include such syntactic sugar in the message but that
       # ... is a fight for another day
       # finally, lists keep an explicit record of their length
       # this is to avoid the need for using a special 'nil' symbol
       # ... which cannot itself be placed in the list.
       #
       
# MISSING - intro to cons, car, cdr
       # used to be pure-cons pure-car pure-cdr but changed for better interface to scheme
       # also should introduce number? check function
       #
[
hear] (define list-helper
         (? n
           (? ret
             (if (> (n) 1)
               (? x
                 (list-helper
                   (- (n) 1)
                   (? y (? z (ret (+ 1 (y)) (cons (x) (z)))))))
               (? x (ret 1 (x)))))));
[hear] (define list
         (? n
           (if (= (n) 0)
             (cons 0 0)
             (list-helper (n) (? y (? z (cons (y) (z))))))));
[hear] (define head
         (? lst
           (if (= (car (lst)) 0)
             (undefined)
             (if (= (car (lst)) 1)
               (cdr (lst))
               (car (cdr (lst)))))));
[hear] (define tail
         (? lst
           (if (= (car (lst)) 0)
             (undefined)
             (if (= (car (lst)) 1)
               (cons 0 0)
               (cons (- (car (lst)) 1) (cdr (cdr (lst))))))));
[hear] (define list-length (? lst (car (lst))));
[hear] (define list-ref
         (? lst
           (? n
             (if (= (list-ref (lst)) 0)
               (undefined)
               (if (= (n) 0)
                 (head (lst))
                 (list-ref (tail (lst)) (- (n) 1)))))));
[hear] (define prepend
         (? x
           (? lst
             (if (= (list-length (lst)) 0)
               (cons 1 (x))
               (cons (+ (list-length (lst)) 1)
                     (cons (x) (cdr (lst))))))));
[hear] (define list=
         (? x
           (? y
             (if (= (list-length (x)) (list-length (y)))
               (if (> (list-length (x)) 0)
                 (and (= (head (x)) (head (y)))
                      (list= (tail (x)) (tail (y))))
                 (true))
               (false)))));
[hear] (= (list-length ((list 1) 3)) 1);
[hear] (= (list-length ((list 8) 9 8 0 4 7 3 6 5)) 8);
[hear] (= (list-length ((list 5) 8 6 4 2 5)) 5);
[hear] (= (list-length ((list 9) 5 8 4 3 9 6 1 7 2)) 9);
[hear] (= (list-length ((list 7) 2 4 9 6 5 0 8)) 7);
[hear] (= (head ((list 8) 12 1 4 13 17 3 10 4)) 12);
[hear] (list= (tail ((list 8) 12 1 4 13 17 3 10 4))
              ((list 7) 1 4 13 17 3 10 4));
[hear] (= (head ((list 9) 6 13 15 4 12 1 0 5 6)) 6);
[hear] (list= (tail ((list 9) 6 13 15 4 12 1 0 5 6))
              ((list 8) 13 15 4 12 1 0 5 6));
[hear] (= (head ((list 6) 19 4 12 2 15 12)) 19);
[hear] (list= (tail ((list 6) 19 4 12 2 15 12))
              ((list 5) 4 12 2 15 12));
[hear] (= (head ((list 10) 3 4 4 2 15 3 17 6 11 3)) 3);
[hear] (list= (tail ((list 10) 3 4 4 2 15 3 17 6 11 3))
              ((list 9) 4 4 2 15 3 17 6 11 3));
[hear] (= (head ((list 2) 15 2)) 15);
[hear] (list= (tail ((list 2) 15 2)) ((list 1) 2));
[hear] (= (head ((list 10) 15 12 17 11 0 12 14 8 17 5))
          15);
[hear] (list= (tail ((list 10) 15 12 17 11 0 12 14 8 17 5))
              ((list 9) 12 17 11 0 12 14 8 17 5));
[hear] (= (head ((list 5) 11 1 10 7 9)) 11);
[hear] (list= (tail ((list 5) 11 1 10 7 9))
              ((list 4) 1 10 7 9));
[hear] (= (head ((list 3) 19 10 14)) 19);
[hear] (list= (tail ((list 3) 19 10 14))
              ((list 2) 10 14));
[hear] (= (head ((list 5) 4 2 7 12 18)) 4);
[hear] (list= (tail ((list 5) 4 2 7 12 18))
              ((list 4) 2 7 12 18));
[hear] (= (head ((list 5) 13 1 0 5 10)) 13);
[hear] (list= (tail ((list 5) 13 1 0 5 10))
              ((list 4) 1 0 5 10));
[hear] (= (list-ref ((list 1) 9) 0) 9);
[hear] (= (list-ref ((list 10) 4 4 14 0 14 4 17 7 3 17) 0)
          4);
[hear] (= (list-ref ((list 8) 10 13 6 14 3 13 9 18) 0)
          10);
[hear] (= (list-ref ((list 4) 3 1 0 2) 2) 0);
[hear] (= (list-ref ((list 5) 13 7 18 13 12) 1) 7);
[hear] (= (list-ref ((list 3) 19 16 9) 2) 9);
[hear] (= (list-ref ((list 5) 12 14 5 14 4) 4) 4);
[hear] (= (list-ref ((list 2) 10 17) 1) 17);
[hear] (= (list-ref ((list 4) 1 12 10 18) 3) 18);
[hear] (= (list-ref ((list 8) 17 7 2 4 19 15 4 9) 0) 17);
[hear] (list= ((list 0)) ((list 0)));
[hear] (list= ((list 1) 7) ((list 1) 7));
[hear] (list= ((list 2) 1 19) ((list 2) 1 19));
[hear] (list= ((list 3) 18 1 18) ((list 3) 18 1 18));
[hear] (list= ((list 4) 13 15 10 6)
              ((list 4) 13 15 10 6));
       # this next batch of examples are a bit misleading, should streamline
[hear] (not (list= ((list 0)) ((list 1) 0)));
[hear] (not (list= ((list 0)) ((list 1) 6)));
[hear] (not (list= ((list 1) 9) ((list 2) 6 9)));
[hear] (not (list= ((list 1) 9) ((list 2) 9 7)));
[hear] (not (list= ((list 2) 1 6) ((list 3) 2 1 6)));
[hear] (not (list= ((list 2) 1 6) ((list 3) 1 6 0)));
[hear] (not (list= ((list 3) 10 9 12) ((list 4) 5 10 9 12)));
[hear] (not (list= ((list 3) 10 9 12) ((list 4) 10 9 12 3)));
[hear] (not (list= ((list 4) 17 9 1 0) ((list 5) 4 17 9 1 0)));
[hear] (not (list= ((list 4) 17 9 1 0) ((list 5) 17 9 1 0 4)));
       # some helpful functions
[hear] (list= (prepend 12 ((list 0))) ((list 1) 12));
[hear] (list= (prepend 0 ((list 1) 14)) ((list 2) 0 14));
[hear] (list= (prepend 10 ((list 2) 8 19))
              ((list 3) 10 8 19));
[hear] (list= (prepend 12 ((list 3) 10 2 1))
              ((list 4) 12 10 2 1));
[hear] (list= (prepend 14 ((list 4) 6 16 14 5))
              ((list 5) 14 6 16 14 5));
[hear] (list= (prepend 4 ((list 5) 15 2 3 11 8))
              ((list 6) 4 15 2 3 11 8));
[hear] (list= (prepend 12 ((list 6) 9 2 19 7 2 0))
              ((list 7) 12 9 2 19 7 2 0));
[hear] (list= (prepend 11 ((list 7) 17 17 2 4 16 5 14))
              ((list 8) 11 17 17 2 4 16 5 14));
[hear] (define pair (? x (? y ((list 2) (x) (y)))));
[hear] (define first (? lst (head (lst))));
[hear] (define second (? lst (head (tail (lst)))));
[hear] (list= (pair 3 6) ((list 2) 3 6));
[hear] (= (first (pair 3 6)) 3);
[hear] (= (second (pair 3 6)) 6);
[hear] (list= (pair 8 8) ((list 2) 8 8));
[hear] (= (first (pair 8 8)) 8);
[hear] (= (second (pair 8 8)) 8);
[hear] (list= (pair 9 2) ((list 2) 9 2));
[hear] (= (first (pair 9 2)) 9);
[hear] (= (second (pair 9 2)) 2);
[hear] (define list-find-helper
         (? lst
           (? key
             (? fail
               (? idx
                 (if (= (list-length (lst)) 0)
                   (fail 0)
                   (if (= (head (lst)) (key))
                     (idx)
                     (list-find-helper
                       (tail (lst))
                       (key)
                       (fail)
                       (+ (idx) 1)))))))));
[hear] (define list-find
         (? lst
           (? key
             (? fail (list-find-helper (lst) (key) (fail) 0)))));
[hear] (define example-fail (? x 100));
[hear] (= (list-find ((list 1) 15) 15 (example-fail)) 0);
[hear] (= (list-find ((list 2) 9 6) 9 (example-fail)) 0);
[hear] (= (list-find
            ((list 4) 19 7 14 6)
            19
            (example-fail))
          0);
[hear] (= (list-find
            ((list 8) 10 0 6 9 5 10 2 2)
            5
            (example-fail))
          4);
[hear] (= (list-find ((list 4) 14 5 7 6) 6 (example-fail))
          3);
[hear] (= (list-find ((list 1) 2) 2 (example-fail)) 0);
[hear] (= (list-find
            ((list 7) 19 7 12 4 18 8 7)
            4
            (example-fail))
          3);
[hear] (= (list-find ((list 1) 2) 2 (example-fail)) 0);
[hear] (= (list-find
            ((list 4) 5 19 13 13)
            19
            (example-fail))
          1);
[hear] (= (list-find
            ((list 10) 17 14 17 8 6 1 2 12 10 4)
            1
            (example-fail))
          5);
[hear] (= (list-find
            ((list 4) 15 13 6 17)
            14
            (example-fail))
          100);
[hear] (= (list-find
            ((list 6) 16 13 10 3 0 19)
            2
            (example-fail))
          100);
[hear] (= (list-find
            ((list 8) 13 19 4 17 11 9 2 3)
            15
            (example-fail))
          100);
       # HACK describe changes to the implicit interpreter to allow new special forms
[
hear] (define base-translate (translate));
[hear] (define translate
         (? x (if (= (x) 10) 15 (base-translate (x)))));
[hear] (= 10 15);
[hear] (= (+ 10 15) 30);
[hear] (define translate (base-translate));
[hear] (not (= 10 15));
[hear] (= (+ 10 15) 25);
       # now can create a special form for lists
[hear] (define translate
         (? x
           (if (number? (x))
             (base-translate (x))
             (if (= (head (x)) vector)
               (translate
                 (prepend
                   ((list 2) list (list-length (tail (x))))
                   (tail (x))))
               (base-translate (x))))));
[hear] (= (vector 1 2 3) ((list 3) 1 2 3));
       # now to desugar let expressions
[hear] (define translate-with-vector (translate));
[hear] (define translate-let-form
         (? x
           (? body
             (if (= (list-length (x)) 0)
               (translate (body))
               (translate-let-form
                 (tail (x))
                 (vector
                   (vector ? (head (head (x))) (body))
                   (head (tail (head (x))))))))));
[hear] (define translate
         (? x
           (if (number? (x))
             (translate-with-vector (x))
             (if (= (head (x)) let)
               (translate-let-form
                 (head (tail (x)))
                 (head (tail (tail (x)))))
               (translate-with-vector (x))))));
[hear] (let ((x 20)) (= (x) 20));
[hear] (let ((x 50) (y 20)) (= (- (x) (y)) 30));
       # the is-list function is now on dubious ground
       # this stuff will be replaced with typing ASAP
[hear] (define is-list (? x (not (number? (x)))));
[hear] (is-list ((list 2) 1 3));
[hear] (is-list ((list 0)));
[hear] (not (is-list 23));
[hear] (is-list
         ((list 3) ((list 2) 2 3) 1 (? x (+ (x) 10))));
       # MATH introduce sugar for let
       # if would be good to introduce desugarings more rigorously, but for now...
       # ... just a very vague sketch
[
hear] (intro let);
[hear] (= (let ((x 10)) (+ (x) 5)) ((? x (+ (x) 5)) 10));
[hear] (= (let ((x 10) (y 5)) (+ (x) (y)))
          (((? x (? y (+ (x) (y)))) 10) 5));
       # MATH build up functions of several variables
[
hear] (= ((? x (? y (- (x) (y)))) 12 6) 6);
[hear] (= ((? x (? y (- (x) (y)))) 3 0) 3);
[hear] (= ((? x (? y (- (x) (y)))) 8 7) 1);
[hear] (= ((? x (? y (- (x) (y)))) 7 6) 1);
[hear] (= ((? x (? y (- (x) (y)))) 7 6) 1);
[hear] (define last
         (? x (list-ref (x) (- (list-length (x)) 1))));
[hear] (define except-last
         (? x
           (if (> (list-length (x)) 1)
             (prepend (head (x)) (except-last (tail (x))))
             (vector))));
       # test last and except-last
[hear] (= 15 (last (vector 4 5 15)));
[hear] (list= (vector 4 5)
              (except-last (vector 4 5 15)));
[hear] (intro lambda);
[hear] (define prev-translate (translate));
[hear] (define translate
         (let ((prev (prev-translate)))
           (? x
             (if (number? (x))
               (prev (x))
               (if (= (head (x)) lambda)
                 (let ((formals (head (tail (x))))
                       (body (head (tail (tail (x))))))
                   (if (> (list-length (formals)) 0)
                     (translate
                       (vector
                         lambda
                         (except-last (formals))
                         (vector ? (last (formals)) (body))))
                     (translate (body))))
                 (prev (x)))))));
       # test lambda
[hear] (= (? x (- (x) 5)) (lambda (x) (- (x) 5)));
[hear] (= (? x (? y (- (x) (y))))
          (lambda (x y) (- (x) (y))));
[hear] (= ((lambda (x y) (- (x) (y))) 17 9) 8);
[hear] (= ((lambda (x y) (- (x) (y))) 9 2) 7);
[hear] (= ((lambda (x y) (- (x) (y))) 13 8) 5);
[hear] (= ((lambda (x y) (- (x) (y))) 8 6) 2);
[hear] (= ((lambda (x y) (- (x) (y))) 3 3) 0);
[hear] (define apply
         (lambda (x y)
           (if (list= (y) (vector))
             (x)
             (apply ((x) (head (y))) (tail (y))))));
[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 12 6))
          6);
[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 10 7))
          3);
[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 12 3))
          9);
[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 6 5))
          1);
[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 0 0))
          0);
       # MATH show map function for applying a function across the elements of a list
[
hear] (define map
         (lambda (p lst)
           (if (> (list-length (lst)) 0)
             (prepend (p (head (lst))) (map (p) (tail (lst))))
             (vector))));
[hear] (= (map (? x (* (x) 2)) (vector 3 18 17))
          (vector 6 36 34));
[hear] (= (map (? x (* (x) 2)) (vector 6 11 7 9))
          (vector 12 22 14 18));
[hear] (= (map (? x (* (x) 2)) (vector 6 14 16 1 11))
          (vector 12 28 32 2 22));
[hear] (= (map (? x (* (x) 2)) (vector 13 11 19 9 7 16))
          (vector 26 22 38 18 14 32));
[hear] (= (map (? x 42) (vector 15 3 19))
          (vector 42 42 42));
[hear] (= (map (? x 42) (vector 2 15 6 19))
          (vector 42 42 42 42));
[hear] (= (map (? x 42) (vector 2 9 11 5 13))
          (vector 42 42 42 42 42));
[hear] (= (map (? x 42) (vector 19 12 17 18 5 8))
          (vector 42 42 42 42 42 42));
[hear] (define crunch
         (lambda (p lst)
           (if (>= (list-length (lst)) 2)
             (p (head (lst)) (crunch (p) (tail (lst))))
             (if (= (list-length (lst)) 1)
               (head (lst))
               (undefined)))));
[hear] (= (crunch (+) (vector 17 7 18)) 42);
[hear] (= (crunch (+) (vector 19 10 0 11)) 40);
[hear] (= (crunch (+) (vector 7 16 11 8 19)) 61);
[hear] (= (crunch (+) (vector 1 5 14 16 15 19)) 70);
       # MATH introduce mutable objects, and side-effects
[
hear] (intro make-cell);
[hear] (intro set!);
[hear] (intro get!);
[hear] (define demo-mut1 (make-cell 0));
[hear] (set! (demo-mut1) 15);
[hear] (= (get! (demo-mut1)) 15);
[hear] (set! (demo-mut1) 5);
[hear] (set! (demo-mut1) 7);
[hear] (= (get! (demo-mut1)) 7);
[hear] (define demo-mut2 (make-cell 11));
[hear] (= (get! (demo-mut2)) 11);
[hear] (set! (demo-mut2) 22);
[hear] (= (get! (demo-mut2)) 22);
[hear] (= (get! (demo-mut1)) 7);
[hear] (= (+ (get! (demo-mut1)) (get! (demo-mut2))) 29);
[hear] (if (= (get! (demo-mut1)) 7)
         (set! (demo-mut1) 88)
         (set! (demo-mut1) 99));
[hear] (= (get! (demo-mut1)) 88);
[hear] (if (= (get! (demo-mut1)) 7)
         (set! (demo-mut1) 88)
         (set! (demo-mut1) 99));
[hear] (= (get! (demo-mut1)) 99);
       # MATH show how to execute a sequence of instructions
[
hear] (intro begin);
[hear] (define prev-translate (translate));
[hear] (define reverse
         (? x
           (if (>= (list-length (x)) 1)
             (prepend (last (x)) (reverse (except-last (x))))
             (x))));
       # test reverse
[hear] (list= (vector 1 2 3) (reverse (vector 3 2 1)));
[hear] (define translate
         (let ((prev (prev-translate)))
           (? x
             (if (number? (x))
               (prev (x))
               (if (= (head (x)) begin)
                 (translate
                   (vector
                     (vector ? x (vector head (vector x)))
                     (prepend vector (reverse (tail (x))))))
                 (prev (x)))))));
[hear] (= (begin 1 7 2 4) 4);
[hear] (= (begin
            (set! (demo-mut1) 88)
            (set! (demo-mut1) 6)
            (get! (demo-mut1)))
          6);
[hear] (= (begin
            (set! (demo-mut2) 88)
            (set! (demo-mut1) 6)
            (get! (demo-mut2)))
          88);
[hear] (= (begin
            (set! (demo-mut1) 88)
            (set! (demo-mut1) 6)
            (get! (demo-mut1))
            4)
          4);
       # MATH introduce environment/hashmap structure
       # this section needs a LOT more examples :-)
       # note that at the time of writing (h 1 2) is same as ((h) 1 2)
[
hear] (define hash-add
         (lambda (h x y z) (if (= (z) (x)) (y) (h (z)))));
[hear] (define hash-ref (lambda (h x) (h (x))));
[hear] (define hash-null (? x (undefined)));
[hear] (define test-hash
         (hash-add (hash-add (hash-null) 3 2) 4 9));
[hear] (= (hash-ref (test-hash) 4) 9);
[hear] (= (hash-ref (test-hash) 3) 2);
[hear] (= (hash-ref (test-hash) 8) (undefined));
[hear] (= (hash-ref (test-hash) 15) (undefined));
[hear] (= (hash-ref (hash-add (test-hash) 15 33) 15) 33);
[hear] (= (hash-ref (test-hash) 15) (undefined));
[hear] (define make-hash
         (? x
           (if (list= (x) (vector))
             (hash-null)
             (hash-add
               (make-hash (tail (x)))
               (first (head (x)))
               (second (head (x)))))));
[hear] (= (hash-ref
            (make-hash
              (vector (pair 3 10) (pair 2 20) (pair 1 30)))
            3)
          10);
[hear] (= (hash-ref
            (make-hash
              (vector (pair 3 10) (pair 2 20) (pair 1 30)))
            1)
          30);
       # OBJECT introduce simple mutable structures
[
hear] (define mutable-struct
         (? lst
           (let ((data (map (? x (make-cell 0)) (lst))))
             (? key
               (list-ref (data) (list-find (lst) (key) (? x 0)))))));
[hear] (define test-struct1
         (mutable-struct (vector item1 item2 item3)));
[hear] (set! (test-struct1 item1) 15);
[hear] (= (get! (test-struct1 item1)) 15);
       # OBJECT introduce method handler wrappers
[
hear] (define add-method
         (lambda (object name method)
           (hash-add
             (object)
             (name)
             (? dummy (method (object))))));
[hear] (define call (? x (x 0)));
[hear] (define test-struct2
         (mutable-struct (vector x y)));
[hear] (set! (test-struct2 x) 10);
[hear] (set! (test-struct2 y) 20);
[hear] (= (get! (test-struct2 x)) 10);
[hear] (= (get! (test-struct2 y)) 20);
[hear] (define test-struct3
         (add-method
           (test-struct2)
           sum
           (? self (+ (get! (self x)) (get! (self y))))));
[hear] (= (get! (test-struct3 x)) 10);
[hear] (= (get! (test-struct3 y)) 20);
[hear] (= (call (test-struct3 sum)) 30);
[hear] (set! (test-struct3 y) 10);
[hear] (= (call (test-struct3 sum)) 20);
[hear] (set! (test-struct2 y) 5);
[hear] (= (call (test-struct3 sum)) 15);
       # TURING introduce turing machine model
       # just for fun!
[
hear] (define safe-tail
         (? x
           (if (> (list-length (x)) 0)
             (if (> (list-length (x)) 1)
               (tail (x))
               (vector (false)))
             (? vector (false)))));
[hear] (define safe-head
         (? x
           (if (> (list-length (x)) 0) (head (x)) (false))));
[hear] (define tape-read
         (? tape
           (let ((x (second (tape))))
             (if (> (list-length (x)) 0) (head (x)) (false)))));
[hear] (define tape-transition
         (lambda (tape shift value)
           (if (= (shift) 1)
             (pair (prepend (value) (first (tape)))
                   (safe-tail (second (tape))))
             (if (= (shift) 0)
               (pair (safe-tail (first (tape)))
                     (prepend
                       (safe-head (first (tape)))
                       (prepend (value) (safe-tail (second (tape))))))
               (pair (first (tape))
                     (prepend (value) (safe-tail (second (tape)))))))));
[hear] (define turing
         (lambda (machine current last tape)
           (if (= (current) (last))
             (tape)
             (let ((next (machine (current) (tape-read (tape)))))
               (turing
                 (machine)
                 (list-ref (next) 0)
                 (last)
                 (tape-transition
                   (tape)
                   (list-ref (next) 1)
                   (list-ref (next) 2)))))));
[hear] (define make-tape (? x (pair (vector) (x))));
[hear] (define remove-trail
         (? x
           (? lst
             (if (> (list-length (lst)) 0)
               (if (= (last (lst)) (x))
                 (remove-trail (x) (except-last (lst)))
                 (lst))
               (lst)))));
[hear] (define extract-tape
         (? x (remove-trail (false) (second (x)))));
[hear] (define tm-binary-increment
         (make-hash
           (vector
             (pair right
                   (make-hash
                     (vector
                       (pair 0 (vector right 1 0))
                       (pair 1 (vector right 1 1))
                       (pair (false) (vector inc 0 (false))))))
             (pair inc
                   (make-hash
                     (vector
                       (pair 0 (vector noinc 0 1))
                       (pair 1 (vector inc 0 0))
                       (pair (false) (vector halt 2 1)))))
             (pair noinc
                   (make-hash
                     (vector
                       (pair 0 (vector noinc 0 0))
                       (pair 1 (vector noinc 0 1))
                       (pair (false) (vector halt 1 (false))))))
             (pair halt (make-hash (vector))))));
[hear] (= (extract-tape
            (turing
              (tm-binary-increment)
              right
              halt
              (make-tape (vector 1 0 0 1))))
          (vector 1 0 1 0));
[hear] (= (extract-tape
            (turing
              (tm-binary-increment)
              right
              halt
              (make-tape (vector 1 1 1))))
          (vector 1 0 0 0));
[hear] (= (extract-tape
            (turing
              (tm-binary-increment)
              right
              halt
              (make-tape (vector 1 1 1 0 0 0 1 1 1))))
          (vector 1 1 1 0 0 1 0 0 0));
       # MATH introduce sets and set membership
[
hear] (intro element);
[hear] (define element
         (? x
           (? lst
             (not (= (list-find (lst) (x) (? y (false))) (false))))));
[hear] (element 9 (vector 7 9 5 6));
[hear] (element 6 (vector 7 9 5 6));
[hear] (element 7 (vector 7 9 5 6));
[hear] (element 9 (vector 7 1 9 2 4));
[hear] (element 1 (vector 7 1 9 2 4));
[hear] (element 9 (vector 7 1 9 2 4));
[hear] (element 2 (vector 7 8 0 9 2 6));
[hear] (element 9 (vector 7 8 0 9 2 6));
[hear] (element 0 (vector 7 8 0 9 2 6));
[hear] (element 1 (vector 9 1 3 6));
[hear] (element 1 (vector 9 1 3 6));
[hear] (element 1 (vector 9 1 3 6));
[hear] (element 4 (vector 8 1 2 3 4));
[hear] (element 8 (vector 8 1 2 3 4));
[hear] (element 1 (vector 8 1 2 3 4));
[hear] (not (element 0 (vector 8 2 3 5)));
[hear] (not (element 8 (vector 0 1 3 5)));
[hear] (not (element 0 (vector 8 3 4)));
[hear] (not (element 7 (vector 8 4 5 6)));
[hear] (not (element 7 (vector 0 9 2 3)));
       # rules for set equality
[hear] (define set-subset
         (? x
           (? y
             (if (> (list-length (x)) 0)
               (and (element (head (x)) (y))
                    (set-subset (tail (x)) (y)))
               (true)))));
[hear] (define set=
         (? x
           (? y
             (and (set-subset (x) (y)) (set-subset (y) (x))))));
[hear] (set= (vector 1 5 9) (vector 5 1 9));
[hear] (set= (vector 1 5 9) (vector 9 1 5));
[hear] (not (set= (vector 1 5 9) (vector 1 5)));
       # let's go leave ourselves wide open to Russell's paradox
       # ... by using characteristic functions
       # ... since it doesn't really matter for communication purposes
       # ... and so far this is just used/tested with sets of integers really
[hear] (element 5 (all (? x (= (+ (x) 10) 15))));
[hear] (element 3 (all (? x (= (* (x) 3) (+ (x) 6)))));
[hear] (define empty-set (vector));
[hear] (element 0 (natural-set));
[hear] (forall
         (? x
           (=> (element (x) (natural-set))
               (element (+ (x) 1) (natural-set)))));
[hear] (element 1 (natural-set));
[hear] (element 2 (natural-set));
[hear] (element 3 (natural-set));
[hear] (element 4 (natural-set));
[hear] (element 5 (natural-set));
[hear] (element 6 (natural-set));
[hear] (element 7 (natural-set));
[hear] (element 8 (natural-set));
[hear] (element 9 (natural-set));
[hear] (not (element (true) (natural-set)));
[hear] (not (element (false) (natural-set)));
[hear] (define boolean-set (vector (true) (false)));
[hear] (element (true) (boolean-set));
[hear] (element (false) (boolean-set));
[hear] (not (element 0 (boolean-set)));
[hear] (define even-natural-set
         (all (? x
                (exists
                  (? y
                    (and (element (y) (natural-set))
                         (= (* 2 (y)) (x))))))));
[hear] (element 0 (natural-set));
[hear] (element 0 (even-natural-set));
[hear] (element 1 (natural-set));
[hear] (not (element 1 (even-natural-set)));
[hear] (element 2 (natural-set));
[hear] (element 2 (even-natural-set));
[hear] (element 3 (natural-set));
[hear] (not (element 3 (even-natural-set)));
[hear] (element 4 (natural-set));
[hear] (element 4 (even-natural-set));
[hear] (element 5 (natural-set));
[hear] (not (element 5 (even-natural-set)));
[hear] (element 6 (natural-set));
[hear] (element 6 (even-natural-set));
       # MATH introduce graph structures
[
hear] (define make-graph
         (lambda (nodes links) (pair (nodes) (links))));
[hear] (define test-graph
         (make-graph
           (vector 1 2 3 4)
           (vector (vector 1 2) (vector 2 3) (vector 1 4))));
[hear] (define graph-linked
         (lambda (g n1 n2)
           (exists
             (? idx
               (if (and (>= (idx) 0)
                        (< (idx) (list-length (list-ref (g) 1))))
                 (list= (list-ref (list-ref (g) 1) (idx))
                        (vector (n1) (n2)))
                 (false))))));
[hear] (= (graph-linked (test-graph) 1 2) (true));
[hear] (= (graph-linked (test-graph) 1 3) (false));
[hear] (= (graph-linked (test-graph) 2 4) (false));
       # 'if' is used a lot in the next definition in place of and/or
       # this is because I haven't established lazy evaluation forms for and/or
       # so this very inefficient algorithm completely bogs down when combined
       # ... during testing with a dumb implementation for 'exists'.
[hear] (define graph-linked*
         (lambda (g n1 n2)
           (if (= (n1) (n2))
             (true)
             (if (graph-linked (g) (n1) (n2))
               (true)
               (exists
                 (? n3
                   (if (graph-linked (g) (n1) (n3))
                     (graph-linked* (g) (n3) (n2))
                     (false))))))));
[hear] (= (graph-linked* (test-graph) 1 2) (true));
[hear] (= (graph-linked* (test-graph) 1 3) (true));
[hear] (= (graph-linked* (test-graph) 2 4) (false));
       # OBJECT introduce simple form of typing, for ease of documentation.
       # An object is simply a function that takes an argument.
       # The argument is the method to call on the object.
       # Types are here taken to be just the existence of a particular method,
       # with that method returning an object of the appropriate type.
[
hear] (define make-integer
         (lambda (v) (lambda (x) (if (= (x) int) (v) 0))));
[hear] (define objectify
         (? x (if (number? (x)) (make-integer (x)) (x))));
[hear] (define instanceof
         (lambda (t t)
           (if (number? (t))
             (= (t) int)
             (not (number? ((objectify (t)) (t)))))));
       # add version of lambda that allows types to be declared
[hear] (define prev-translate (translate));
[hear] (define translate
         (let ((prev (prev-translate)))
           (? x
             (if (number? (x))
               (prev (x))
               (if (= (head (x)) lambda)
                 (let ((formals (head (tail (x))))
                       (body (head (tail (tail (x))))))
                   (if (> (list-length (formals)) 0)
                     (if (number? (last (formals)))
                       (translate
                         (vector
                           lambda
                           (except-last (formals))
                           (vector ? (last (formals)) (body))))
                       (let ((formal-name (first (last (formals))))
                             (formal-type (second (last (formals)))))
                         (translate
                           (vector
                             lambda
                             (except-last (formals))
                             (vector
                               ?
                               (formal-name)
                               (vector
                                 let
                                 (vector
                                   (vector
                                     (formal-name)
                                     (vector
                                       (vector objectify (vector (formal-name)))
                                       (formal-type))))
                                 (body)))))))
                     (translate (body))))
                 (prev (x)))))));
       # add conditional form
[hear] (define prev-translate (translate));
[hear] (define translate
         (let ((prev (prev-translate)))
           (? x
             (if (number? (x))
               (prev (x))
               (if (= (head (x)) cond)
                 (let ((cnd (head (tail (x)))) (rem (tail (tail (x)))))
                   (if (> (list-length (rem)) 0)
                     (translate
                       (vector
                         if
                         (first (cnd))
                         (second (cnd))
                         (prepend cond (rem))))
                     (translate (cnd))))
                 (prev (x)))))));
[hear] (= 99 (cond 99));
[hear] (= 8 (cond ((true) 8) 11));
[hear] (= 11 (cond ((false) 8) 11));
[hear] (= 7 (cond ((false) 3) ((true) 7) 11));
[hear] (= 3 (cond ((true) 3) ((true) 7) 11));
[hear] (= 11 (cond ((false) 3) ((false) 7) 11));
[hear] (define remove-match
         (lambda (test lst)
           (if (> (list-length (lst)) 0)
             (if (test (head (lst)))
               (remove-match (test) (tail (lst)))
               (prepend
                 (head (lst))
                 (remove-match (test) (tail (lst)))))
             (lst))));
[hear] (define remove-element
         (lambda (x)
           (remove-match (lambda (y) (= (y) (x))))));
[hear] (list= (vector 1 2 3 5)
              (remove-element 4 (vector 1 2 3 4 5)));
[hear] (list= (vector 1 2 3 5)
              (remove-element 4 (vector 1 4 2 4 3 4 5)));
[hear] (define return
         (lambda (t t)
           (let ((obj (objectify (t)))) (obj (t)))));
[hear] (define tester
         (lambda ((x int) (y int))
           (return int (+ (x) (y)))));
[hear] (= 42
          (tester (make-integer 10) (make-integer 32)));
[hear] (= 42 (tester 10 32));
[hear] (define reflective
         (lambda (f)
           ((lambda (x) (f (lambda (y) ((x (x)) (y)))))
            (lambda (x) (f (lambda (y) ((x (x)) (y))))))));
       # OBJECT an example object -- a 2D point
[
hear] (define point
         (lambda (x y)
           (reflective
             (lambda (self msg)
               (cond ((= (msg) x) (x))
                     ((= (msg) y) (y))
                     ((= (msg) point) (self))
                     ((= (msg) +)
                      (lambda ((p point))
                        (point (+ (x) (p x)) (+ (y) (p y)))))
                     ((= (msg) =)
                      (lambda ((p point))
                        (and (= (x) (p x)) (= (y) (p y)))))
                     0)))));
[hear] (define point1 (point 1 11));
[hear] (define point2 (point 2 22));
[hear] (= 1 (point1 x));
[hear] (= 22 (point2 y));
[hear] (= 11 ((point 11 12) x));
[hear] (= 11 (((point 11 12) point) x));
[hear] (= 16 (((point 16 17) point) x));
[hear] (= 33 (point1 + (point2) y));
[hear] (point1 + (point2) = (point 3 33));
[hear] (point2 + (point1) = (point 3 33));
[hear] ((point 100 200)
        +
        (point 200 100)
        =
        (point 300 300));
[hear] (instanceof point (point1));
[hear] (not (instanceof int (point1)));
[hear] (instanceof int 5);
[hear] (not (instanceof point 5));
       # OBJECT an example object -- a container
[
hear] (define container
         (lambda (x)
           (let ((contents (make-cell (vector))))
             (reflective
               (lambda (self msg)
                 (cond ((= (msg) container) (self))
                       ((= (msg) inventory) (get! (contents)))
                       ((= (msg) add)
                        (lambda (x)
                          (if (not (element (x) (get! (contents))))
                            (set! (contents) (prepend (x) (get! (contents))))
                            (false))))
                       ((= (msg) remove)
                        (lambda (x)
                          (set! (contents)
                            (remove-element (x) (get! (contents))))))
                       ((= (msg) =)
                        (lambda ((c container))
                          (set= (self inventory) (c inventory))))
                       0))))));
       # Can pass anything to container function to create an object
       # Should eventually use a consistent protocol for all objects,
       # but all this stuff is still in flux
[hear] (define pocket (container new));
[hear] (pocket add 77);
[hear] (pocket add 88);
[hear] (pocket add 99);
[hear] (set= (pocket inventory) (vector 77 88 99));
[hear] (pocket remove 88);
[hear] (set= (pocket inventory) (vector 77 99));
[hear] (define pocket2 (container new));
[hear] (pocket2 add 77);
[hear] (pocket2 add 99);
[hear] (pocket2 = (pocket));
       # OBJECT expressing inheritance
       # counter-container adds one method to container: count
[
hear] (define counter-container
         (lambda (x)
           (let ((super (container new)))
             (reflective
               (lambda (self msg)
                 (cond ((= (msg) counter-container) (self))
                       ((= (msg) count) (list-length (super inventory)))
                       (super (msg))))))));
[hear] (define cc1 (counter-container new));
[hear] (= 0 (cc1 count));
[hear] (cc1 add 4);
[hear] (= 1 (cc1 count));
[hear] (cc1 add 5);
[hear] (= 2 (cc1 count));
       # OBJECT adding a special form for classes
       # need a bunch of extra machinery first, will push this
       # back into previous sections eventually, and simplify
[
hear] (define list-append
         (lambda (lst1 lst2)
           (if (> (list-length (lst1)) 0)
             (list-append
               (except-last (lst1))
               (prepend (last (lst1)) (lst2)))
             (lst2))));
[hear] (= (list-append (vector 1 2 3) (vector 4 5 6))
          (vector 1 2 3 4 5 6));
[hear] (define append
         (? x
           (? lst
             (if (> (list-length (lst)) 0)
               (prepend (head (lst)) (append (x) (tail (lst))))
               (vector (x))))));
[hear] (= (append 5 (vector 1 2)) (vector 1 2 5));
[hear] (define select-match
         (lambda (test lst)
           (if (> (list-length (lst)) 0)
             (if (test (head (lst)))
               (prepend
                 (head (lst))
                 (select-match (test) (tail (lst))))
               (select-match (test) (tail (lst))))
             (lst))));
[hear] (define unique
         (let ((store (make-cell 0)))
           (lambda (x)
             (let ((id (get! (store))))
               (begin (set! (store) (+ (id) 1)) (id))))));
[hear] (= (unique new) 0);
[hear] (= (unique new) 1);
[hear] (= (unique new) 2);
[hear] (not (= (unique new) (unique new)));
       # okay, here it comes. don't panic!
       # I need to split this up into helpers, and simplify.
       # It basically just writes code for classes like we saw in
       # a previous section.
[hear] (define prev-translate (translate));
[hear] (define translate
         (let ((prev (prev-translate)))
           (? x
             (if (number? (x))
               (prev (x))
               (if (= (head (x)) class)
                 (let ((name (list-ref (x) 1))
                       (args (list-ref (x) 2))
                       (fields (tail (tail (tail (x))))))
                   (translate
                     (vector
                       define
                       (name)
                       (vector
                         lambda
                         (prepend method (args))
                         (vector
                           let
                           (append
                             (vector unique-id (vector unique new))
                             (map (tail)
                                  (select-match
                                    (? x (= (first (x)) field))
                                    (fields))))
                           (vector
                             let
                             (vector
                               (vector
                                 self
                                 (vector
                                   reflective
                                   (vector
                                     lambda
                                     (vector self method)
                                     (list-append
                                       (prepend
                                         cond
                                         (list-append
                                           (map (? x
                                                  (vector
                                                    (vector
                                                      =
                                                      (vector method)
                                                      (first (x)))
                                                    (second (x))))
                                                (map (tail)
                                                     (select-match
                                                       (? x (= (first (x)) method))
                                                       (fields))))
                                           (map (? x
                                                  (vector
                                                    (vector = (vector method) (x))
                                                    (vector (x))))
                                                (map (second)
                                                     (select-match
                                                       (? x (= (first (x)) field))
                                                       (fields))))))
                                       (vector
                                         (vector
                                           (vector = (vector method) self)
                                           (vector self))
                                         (vector
                                           (vector = (vector method) (name))
                                           (vector self self))
                                         (vector
                                           (vector = (vector method) unknown)
                                           (vector lambda (vector x) 0))
                                         (vector (vector = (vector method) new) 0)
                                         (vector
                                           (vector = (vector method) unique-id)
                                           (vector unique-id))
                                         (vector
                                           (vector = (vector method) ==)
                                           (vector
                                             lambda
                                             (vector x)
                                             (vector
                                               =
                                               (vector unique-id)
                                               (vector x unique-id))))
                                         (vector self unknown (vector method))))))))
                             (vector
                               begin
                               (vector self (vector method))
                               (vector self))))))))
                 (prev (x)))))));
       # revisit the point class example
[hear] (class point
              (x y)
              (method x (x))
              (method y (y))
              (method
                +
                (lambda ((p point))
                  (point new (+ (x) (p x)) (+ (y) (p y)))))
              (method
                =
                (lambda ((p point))
                  (and (= (x) (p x)) (= (y) (p y))))));
       # note the appearance of new in the next line --
       # this is the only difference to previous version
[hear] (define point1 (point new 1 11));
[hear] (define point2 (point new 2 22));
[hear] (= 1 (point1 x));
[hear] (= 22 (point2 y));
[hear] (= 11 ((point new 11 12) x));
[hear] (= 11 (((point new 11 12) point) x));
[hear] (= 16 (((point new 16 17) point) x));
[hear] (= 33 (point1 + (point2) y));
[hear] (point1 + (point2) = (point new 3 33));
[hear] (point2 + (point1) = (point new 3 33));
[hear] ((point new 100 200)
        +
        (point new 200 100)
        =
        (point new 300 300));
[hear] (instanceof point (point1));
[hear] (not (instanceof int (point1)));
       # OBJECT wrapper class for cells
[
hear] (class cell
              (initial-value)
              (field content (make-cell (initial-value)))
              (method get (get! (content)))
              (method
                set
                (lambda (new-value) (set! (content) (new-value))))
              (method reset (self set (initial-value)))
              (method
                unknown
                (lambda (x) ((objectify (self get)) (x)))));
[hear] (define cell-test1 (cell new 15));
[hear] (= 15 (cell-test1 get));
[hear] (cell-test1 set 82);
[hear] (= 82 (cell-test1 get));
[hear] (define cell-test2
         (cell new (point new 120 150)));
[hear] (define cell-test3
         (cell new (point new 300 300)));
[hear] (cell-test2 + (cell-test3) = (point new 420 450));
[hear] (not (cell-test2 = (cell-test3)));
[hear] (cell-test3 set (cell-test2));
[hear] (cell-test2 = (cell-test3));
       # MUD playing around with doors and rooms
[
hear] (class door
              ((src room) (dest room))
              (method
                new
                (begin (src add (self)) (dest add (self))))
              (method
                access-from
                (lambda ((current room))
                  (cond ((current == (src)) (dest))
                        ((current == (dest)) (src))
                        0)))
              (method
                is-present
                (lambda ((current room))
                  (cond ((current == (src)) (true))
                        ((current == (dest)) (true))
                        (false)))));
[hear] (class room
              ()
              (field content (container new))
              (method unknown (lambda (x) (content (x)))));
       # need to fix up containers to use object equality
[hear] (define object-element
         (lambda (n lst)
           (> (list-length
                (select-match (lambda (x) (x == (n))) (lst)))
              0)));
[hear] (class container
              ()
              (field contents (cell new (vector)))
              (method inventory (contents get))
              (method
                add
                (lambda (x)
                  (if (not (object-element (x) (contents get)))
                    (contents set (prepend (x) (contents get)))
                    (false)))));
[hear] (define hall (room new));
[hear] (define kitchen (room new));
[hear] (define door1 (door new (hall) (kitchen)));
[hear] ((first (hall inventory)) == (door1));
[hear] ((first (kitchen inventory)) == (door1));
[hear] (door1 access-from (hall) == (kitchen));
[hear] (not (door1 access-from (hall) == (hall)));
[hear] (door1 access-from (kitchen) == (hall));
[hear] (define lawn (room new));
[hear] (define stairs (room new));
[hear] (define bedroom (room new));
[hear] (define nowhere (room new));
[hear] (define door2 (door new (hall) (lawn)));
[hear] (define door3 (door new (hall) (stairs)));
[hear] (define door4 (door new (stairs) (bedroom)));
[hear] (class character
              ()
              (field location (cell new (nowhere)))
              (method
                set-room
                (lambda ((r room)) (location set (r))))
              (method get-room (location get))
              (method update 0));
[hear] (define find-max-helper
         (lambda (test max idx n lst)
           (if (> (list-length (lst)) 0)
             (if (> (test (head (lst))) (max))
               (find-max-helper
                 (test)
                 (test (head (lst)))
                 (n)
                 (+ (n) 1)
                 (tail (lst)))
               (find-max-helper
                 (test)
                 (max)
                 (idx)
                 (+ (n) 1)
                 (tail (lst))))
             (idx))));
[hear] (define find-max-idx
         (lambda (test lst)
           (find-max-helper
             (test)
             (test (head (lst)))
             0
             0
             (lst))));
[hear] (define find-min-helper
         (lambda (test max idx n lst)
           (if (> (list-length (lst)) 0)
             (if (< (test (head (lst))) (max))
               (find-min-helper
                 (test)
                 (test (head (lst)))
                 (n)
                 (+ (n) 1)
                 (tail (lst)))
               (find-min-helper
                 (test)
                 (max)
                 (idx)
                 (+ (n) 1)
                 (tail (lst))))
             (idx))));
[hear] (define find-min-idx
         (lambda (test lst)
           (find-min-helper
             (test)
             (test (head (lst)))
             0
             0
             (lst))));
[hear] (= 2
          (find-max-idx (lambda (x) (x)) (vector 3 4 5 0)));
[hear] (= 1
          (find-max-idx (lambda (x) (x)) (vector 3 5 4 0)));
[hear] (= 0
          (find-max-idx (lambda (x) (x)) (vector 5 3 4 0)));
       # the robo class makes a character that patrols from room to room
[hear] (class robo
              ()
              (field super (character new))
              (field timestamp (cell new 0))
              (field timestamp-map (cell new (lambda (x) 0)))
              (method unknown (lambda (x) (super (x))))
              (method
                update
                (let ((exits (select-match
                               (lambda (x) (instanceof door (x)))
                               (self location inventory))))
                  (let ((timestamps
                          (map (lambda (x) (timestamp-map get (x)))
                               (exits))))
                    (let ((chosen-exit
                            (list-ref
                              (exits)
                              (find-min-idx (lambda (x) (x)) (timestamps))))
                          (current-tmap (timestamp-map get))
                          (current-t (timestamp get)))
                      (begin
                        (self location
                              set
                              (chosen-exit access-from (self location get)))
                        (timestamp-map
                          set
                          (lambda ((d door))
                            (if (d == (chosen-exit))
                              (current-t)
                              (current-tmap (d)))))
                        (timestamp set (+ (timestamp get) 1))))))));
[hear] (define myrobo (robo new));
[hear] (myrobo set-room (stairs));
[hear] (define which-room
         (lambda ((rr robo))
           (find-max-idx
             (lambda ((r room)) (if (r == (rr get-room)) 1 0))
             (vector
               (hall)
               (kitchen)
               (stairs)
               (lawn)
               (bedroom)))));
[hear] (define sequencer
         (lambda (n current lst)
           (if (< (current) (n))
             (begin
               (myrobo update)
               (sequencer
                 (n)
                 (+ (current) 1)
                 (append (which-room (myrobo)) (lst))))
             (lst))));
       # here is a list of the first 30 rooms the robot character visits
       # 0=hall, 1=kitchen, 2=stairs, 3=lawn, 4=bedroom
[hear] (list= (sequencer 30 0 (vector))
              (vector
                4
                2
                0
                3
                0
                1
                0
                2
                4
                2
                0
                3
                0
                1
                0
                2
                4
                2
                0
                3
                0
                1
                0
                2
                4
                2
                0
                3
                0
                1));
       # Now should start to introduce a language to talk about what is
       # going on in the simulated world, and start to move away from
       # detailed mechanism