# 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 (unary 0));
(intro (unary 1 0));
(intro (unary 1 1 0));
(intro (unary 1 1 1 0));
(intro (unary 1 1 1 1 0));
(intro (unary 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(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));
(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));
(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));
(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));
(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));
(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));
(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));
(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));
(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));
(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));
(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));
(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));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 0));
(intro (unary 1 1 1 1 0));
(intro (unary 1 1 1 0));
(intro (unary 1 1 0));
(intro (unary 1 0));
(intro (unary 0));
(intro (unary 0));
(intro (unary 1 0));
(intro (unary 1 1 0));
(intro (unary 1 1 1 0));
(intro (unary 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(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));
(intro (unary 0));
(intro (unary 1 0));
(intro (unary 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 0));
(intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(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));
(intro (unary 0));
(intro (unary 1 0));
(intro (unary 1 1 1 1 1 1 1 1 0));
(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
(intro =);
(= (unary 0) (unary 0));
(= (unary 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));
(= (unary 1 1 0) (unary 1 1 0));
(= (unary 1 1 1 0) (unary 1 1 1 0));
# MATH now show other relational operators
(intro >);
(> (unary 1 1 1 0) (unary 1 0));
(> (unary 1 0) (unary 0));
(> (unary 1 1 1 1 1 1 0) (unary 0));
(> (unary 1 1 1 1 0) (unary 0));
(> (unary 1 1 1 1 1 0) (unary 0));
(> (unary 1 1 1 1 0) (unary 0));
(> (unary 1 0) (unary 0));
(> (unary 1 1 1 1 1 1 0) (unary 1 0));
(> (unary 1 1 1 1 1 1 0) (unary 1 1 0));
(> (unary 1 1 1 0) (unary 1 0));
(> (unary 1 1 1 1 1 0) (unary 0));
(intro <);
(< (unary 0) (unary 1 1 1 1 1 1 0));
(< (unary 0) (unary 1 0));
(< (unary 0) (unary 1 0));
(< (unary 0) (unary 1 1 0));
(< (unary 1 0) (unary 1 1 1 0));
(< (unary 0) (unary 1 1 0));
(< (unary 1 1 0) (unary 1 1 1 1 0));
(< (unary 1 1 1 0) (unary 1 1 1 1 1 0));
(< (unary 0) (unary 1 1 0));
(< (unary 0) (unary 1 1 1 1 1 0));
(< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0));
(< (unary 1 1 0) (unary 1 1 1 0));
(> (unary 1 1 0) (unary 1 0));
(> (unary 1 1 1 1 1 0) (unary 1 0));
(= (unary 1 1 1 0) (unary 1 1 1 0));
(= (unary 1 1 1 0) (unary 1 1 1 0));
(> (unary 1 0) (unary 0));
(< (unary 1 0) (unary 1 1 1 1 0));
(= (unary 1 1 1 1 0) (unary 1 1 1 1 0));
(> (unary 1 1 1 0) (unary 1 1 0));
(= (unary 1 1 1 0) (unary 1 1 1 0));
(< (unary 1 1 1 0) (unary 1 1 1 1 1 0));
# MATH introduce the NOT logical operator
(intro not);
(= (unary 1 0) (unary 1 0));
(not (< (unary 1 0) (unary 1 0)));
(not (> (unary 1 0) (unary 1 0)));
(= (unary 1 1 1 0) (unary 1 1 1 0));
(not (< (unary 1 1 1 0) (unary 1 1 1 0)));
(not (> (unary 1 1 1 0) (unary 1 1 1 0)));
(= (unary 0) (unary 0));
(not (< (unary 0) (unary 0)));
(not (> (unary 0) (unary 0)));
(= (unary 1 1 1 0) (unary 1 1 1 0));
(not (< (unary 1 1 1 0) (unary 1 1 1 0)));
(not (> (unary 1 1 1 0) (unary 1 1 1 0)));
(= (unary 1 0) (unary 1 0));
(not (< (unary 1 0) (unary 1 0)));
(not (> (unary 1 0) (unary 1 0)));
(= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
(not (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
(not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
(not (= (unary 1 0) (unary 1 1 1 1 0)));
(< (unary 1 0) (unary 1 1 1 1 0));
(not (> (unary 1 0) (unary 1 1 1 1 0)));
(not (= (unary 1 1 0) (unary 1 1 1 1 0)));
(< (unary 1 1 0) (unary 1 1 1 1 0));
(not (> (unary 1 1 0) (unary 1 1 1 1 0)));
(not (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
(< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0));
(not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
(not (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
(< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0));
(not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
(not (= (unary 1 0) (unary 1 1 1 0)));
(< (unary 1 0) (unary 1 1 1 0));
(not (> (unary 1 0) (unary 1 1 1 0)));
(not (= (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 1 0));
(not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
(not (= (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 0));
(not (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)));
(not (= (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
(> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
(not (< (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
(not (= (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
(> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
(not (< (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
(not (= (unary 1 1 1 0) (unary 1 0)));
(> (unary 1 1 1 0) (unary 1 0));
(not (< (unary 1 1 1 0) (unary 1 0)));
(not (= (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
(> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
(not (< (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
(not (= (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)));
(> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0));
(not (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)));
# MATH introduce the AND logical operator
(intro and);
(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)));
(and (= (unary 1 0) (unary 1 0))
(= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
(and (> (unary 1 1 1 1 0) (unary 1 1 1 0))
(> (unary 1 1 1 1 0) (unary 1 0)));
(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)));
(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)));
(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)));
(and (= (unary 1 1 0) (unary 1 1 0))
(< (unary 0) (unary 1 1 0)));
(and (> (unary 1 1 1 1 1 0) (unary 1 1 0))
(= (unary 1 1 0) (unary 1 1 0)));
(and (< (unary 1 0) (unary 1 1 1 1 0))
(= (unary 1 1 1 1 0) (unary 1 1 1 1 0)));
(and (< (unary 1 0) (unary 1 1 0))
(= (unary 1 1 0) (unary 1 1 0)));
(not (and (> (unary 1 1 1 1 0) (unary 1 1 1 0)) (> (unary 0) (unary 1 0))));
(not
(and (< (unary 1 1 1 0) (unary 1 1 1 1 1 0))
(= (unary 1 1 0) (unary 1 1 1 1 0))));
(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))));
(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))));
(not (and (= (unary 1 0) (unary 1 0)) (< (unary 1 1 1 1 1 0) (unary 1 1 0))));
(not (and (> (unary 1 1 0) (unary 1 1 1 0)) (< (unary 1 0) (unary 1 1 1 0))));
(not
(and (< (unary 1 1 1 1 1 1 0) (unary 1 0))
(> (unary 1 1 1 0) (unary 1 1 0))));
(not
(and (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))
(> (unary 1 1 0) (unary 0))));
(not
(and (= (unary 1 0) (unary 0))
(> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0))));
(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))));
(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))));
(not (and (= (unary 1 1 1 1 0) (unary 0)) (> (unary 0) (unary 1 1 1 0))));
(not
(and (= (unary 1 1 1 1 1 0) (unary 0))
(> (unary 1 1 1 0) (unary 1 1 1 0))));
(not (and (> (unary 0) (unary 1 1 1 1 0)) (> (unary 1 1 0) (unary 1 1 0))));
(not (and (= (unary 0) (unary 1 1 1 1 0)) (= (unary 1 1 1 1 1 0) (unary 1 0))));
(not (and (< (unary 1 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 1 0) (unary 1 0))));
(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)));
(not
(and (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0))
(> (unary 1 1 0) (unary 1 1 1 0))));
(not (and (> (unary 1 0) (unary 0)) (< (unary 1 1 1 0) (unary 1 1 0))));
(and (< (unary 0) (unary 1 1 0))
(> (unary 1 0) (unary 0)));
(not (and (= (unary 1 1 1 1 0) (unary 1 0)) (> (unary 0) (unary 1 1 1 0))));
(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))));
(not (and (= (unary 1 1 0) (unary 1 0)) (> (unary 1 0) (unary 1 1 1 0))));
(not (and (> (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 1 0) (unary 1 0))));
(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
(intro or);
(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)));
(or (< (unary 1 0) (unary 1 1 0))
(> (unary 1 1 0) (unary 0)));
(or (> (unary 1 1 1 1 0) (unary 1 0))
(< (unary 1 1 0) (unary 1 1 1 1 0)));
(or (< (unary 1 0) (unary 1 1 1 1 0))
(> (unary 1 0) (unary 0)));
(or (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0))
(= (unary 0) (unary 0)));
(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)));
(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)));
(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)));
(or (= (unary 0) (unary 0))
(= (unary 1 1 0) (unary 1 1 0)));
(or (< (unary 0) (unary 1 1 1 0))
(= (unary 0) (unary 0)));
(or (< (unary 0) (unary 1 1 0))
(= (unary 1 1 1 1 0) (unary 1 1 0)));
(or (> (unary 1 1 1 0) (unary 1 0))
(= (unary 0) (unary 1 1 0)));
(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)));
(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)));
(or (> (unary 1 1 1 1 1 0) (unary 1 1 1 0))
(> (unary 1 1 0) (unary 1 1 1 1 0)));
(or (> (unary 0) (unary 1 1 1 1 0))
(= (unary 0) (unary 0)));
(or (= (unary 1 1 0) (unary 0))
(< (unary 0) (unary 1 1 0)));
(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)));
(or (= (unary 1 1 0) (unary 0))
(= (unary 0) (unary 0)));
(or (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
(< (unary 1 0) (unary 1 1 0)));
(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))));
(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))));
(not (or (> (unary 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 1 0) (unary 0))));
(not
(or (> (unary 1 1 1 0) (unary 1 1 1 0))
(< (unary 1 1 1 1 1 0) (unary 1 1 1 0))));
(not (or (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)) (> (unary 0) (unary 0))));
(not (or (> (unary 0) (unary 1 0)) (< (unary 1 1 1 1 1 0) (unary 1 1 0))));
(not (or (> (unary 1 0) (unary 1 1 1 1 1 1 0)) (< (unary 1 1 0) (unary 0))));
(or (> (unary 0) (unary 1 1 1 0))
(> (unary 1 1 1 1 0) (unary 1 1 1 0)));
(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)));
(or (= (unary 1 1 1 0) (unary 1 1 1 0))
(= (unary 1 1 0) (unary 1 1 0)));
(not
(or (< (unary 1 1 1 1 1 0) (unary 1 1 1 0))
(< (unary 1 1 0) (unary 1 0))));
(or (> (unary 1 1 1 1 0) (unary 1 0))
(> (unary 1 0) (unary 1 1 1 1 1 1 0)));
(or (< (unary 1 1 1 1 0) (unary 1 1 1 0))
(= (unary 1 1 1 1 0) (unary 1 1 1 1 0)));
(not (or (> (unary 0) (unary 0)) (= (unary 1 1 0) (unary 1 1 1 0))));
(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
(= (> (unary 1 1 1 1 0) (unary 1 1 0))
(> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)));
(= (= (unary 1 1 0) (unary 1 1 0))
(< (unary 1 1 1 1 0) (unary 1 1 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 0) (unary 1 0)));
(= (> (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)));
(= (= (unary 1 1 0) (unary 1 1 0)) (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
(= (= (unary 1 1 1 0) (unary 1 1 0)) (= (unary 1 0) (unary 0)));
(= (> (unary 0) (unary 1 0)) (< (unary 1 1 1 1 0) (unary 1 0)));
(= (> (unary 1 0) (unary 1 1 1 1 1 0)) (> (unary 1 1 1 0) (unary 1 1 1 0)));
(= (> (unary 1 1 0) (unary 1 1 1 1 1 0)) (< (unary 1 0) (unary 0)));
(= (= (unary 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 0) (unary 1 1 1 1 0)));
(not
(= (= (unary 1 0) (unary 0)) (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))));
(not (= (= (unary 1 1 1 1 1 0) (unary 1 1 0)) (= (unary 0) (unary 0))));
(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))));
(not (= (= (unary 0) (unary 1 0)) (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))));
(not
(= (> (unary 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 1 0) (unary 1 1 1 1 0))));
(not
(= (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0))
(= (unary 1 1 1 1 0) (unary 1 0))));
(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))));
(not (= (< (unary 0) (unary 1 1 0)) (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))));
(not
(= (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 0) (unary 0))));
(not
(= (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0)) (= (unary 1 1 1 0) (unary 0))));
(intro true);
(intro false);
(= (true) (= (unary 1 1 1 0) (unary 1 1 1 0)));
(= (true) (= (unary 0) (unary 0)));
(= (true) (> (unary 1 1 1 1 1 0) (unary 1 1 0)));
(= (true) (< (unary 1 1 1 0) (unary 1 1 1 1 0)));
(= (true) (> (unary 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
(= (< (unary 1 0) (unary 1 1 1 1 0)) (true));
(= (< (unary 1 1 1 0) (unary 1 1 1 1 0)) (true));
(= (= (unary 1 1 1 0) (unary 1 1 1 0)) (true));
(= (< (unary 1 1 1 0) (unary 1 1 1 1 0)) (true));
(= (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (true));
(= (false) (> (unary 1 1 0) (unary 1 1 1 1 1 1 0)));
(= (false) (= (unary 1 1 0) (unary 1 1 1 1 0)));
(= (false) (< (unary 1 1 0) (unary 0)));
(= (false) (> (unary 1 1 1 0) (unary 1 1 1 1 1 1 0)));
(= (false) (< (unary 1 1 1 1 0) (unary 1 1 1 0)));
(= (> (unary 1 1 0) (unary 1 1 1 1 1 0)) (false));
(= (= (unary 1 1 0) (unary 1 0)) (false));
(= (= (unary 1 1 0) (unary 1 1 1 1 1 0)) (false));
(= (< (unary 1 1 1 1 1 1 0) (unary 1 1 0)) (false));
(= (< (unary 1 1 1 0) (unary 1 0)) (false));
(= (true) (true));
(= (false) (false));
(not (= (true) (false)));
(not (= (false) (true)));
# MATH introduce addition
(intro +);
(= (+ (unary 1 1 1 0) (unary 1 1 1 1 0)) (unary 1 1 1 1 1 1 1 0));
(= (+ (unary 0) (unary 1 1 1 0)) (unary 1 1 1 0));
(= (+ (unary 0) (unary 1 1 1 0)) (unary 1 1 1 0));
(= (+ (unary 1 0) (unary 0)) (unary 1 0));
(= (+ (unary 0) (unary 0)) (unary 0));
(= (+ (unary 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 0));
(= (+ (unary 1 0) (unary 0)) (unary 1 0));
(= (+ (unary 1 0) (unary 0)) (unary 1 0));
(= (+ (unary 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 0));
(= (+ (unary 0) (unary 0)) (unary 0));
# MATH introduce subtraction
(intro -);
(= (- (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 0));
(= (- (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 0)) (unary 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));
(= (- (unary 1 1 1 1 1 0) (unary 1 1 0)) (unary 1 1 1 0));
(= (- (unary 1 0) (unary 1 0)) (unary 0));
(= (- (unary 0) (unary 0)) (unary 0));
(= (- (unary 1 1 0) (unary 0)) (unary 1 1 0));
(= (- (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 0));
(= (- (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (unary 0));
(= (- (unary 1 1 1 0) (unary 0)) (unary 1 1 1 0));
# MATH introduce multiplication
(intro *);
(= (* (unary 0) (unary 0)) (unary 0));
(= (* (unary 0) (unary 1 0)) (unary 0));
(= (* (unary 0) (unary 1 1 0)) (unary 0));
(= (* (unary 0) (unary 1 1 1 0)) (unary 0));
(= (* (unary 1 0) (unary 0)) (unary 0));
(= (* (unary 1 0) (unary 1 0)) (unary 1 0));
(= (* (unary 1 0) (unary 1 1 0)) (unary 1 1 0));
(= (* (unary 1 0) (unary 1 1 1 0)) (unary 1 1 1 0));
(= (* (unary 1 1 0) (unary 0)) (unary 0));
(= (* (unary 1 1 0) (unary 1 0)) (unary 1 1 0));
(= (* (unary 1 1 0) (unary 1 1 0)) (unary 1 1 1 1 0));
(= (* (unary 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 1 0));
(= (* (unary 1 1 1 0) (unary 0)) (unary 0));
(= (* (unary 1 1 1 0) (unary 1 0)) (unary 1 1 1 0));
(= (* (unary 1 1 1 0) (unary 1 1 0)) (unary 1 1 1 1 1 1 0));
(= (* (unary 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 1 1 1 1 0));
(= (* (unary 1 1 1 0) (unary 0)) (unary 0));
(= (* (unary 0) (unary 1 0)) (unary 0));
(= (* (unary 0) (unary 1 0)) (unary 0));
(= (* (unary 0) (unary 1 0)) (unary 0));
(= (* (unary 0) (unary 1 1 0)) (unary 0));
(= (* (unary 1 1 1 0) (unary 1 0)) (unary 1 1 1 0));
(= (* (unary 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 1 1 1 1 0));
(= (* (unary 1 0) (unary 1 1 0)) (unary 1 1 0));
(= (* (unary 0) (unary 1 0)) (unary 0));
(= (* (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.
(= (unary 0) (.));
(= (unary 1 0) (:));
(= (unary 1 1 0) (:.));
(= (unary 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) (::.));
(= (unary 1 1 1 1 1 1 1 0) (:::));
(= (unary 1 1 1 1 1 1 1 1 0) (:...));
(= (unary 1 1 1 1 1 1 1 1 1 0) (:..:));
(= (unary 1 1 1 1 1 1 1 1 1 1 0) (:.:.));
(= (unary 1 1 1 1 1 1 1 1 1 1 1 0) (:.::));
(= (unary 1 1 1 1 1 1 1 1 1 1 1 1 0) (::..));
(= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (::.:));
(= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (:::.));
(= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (::::));
(= (::.:) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(= (::) (unary 1 1 1 0));
(= (::.:) (unary 1 1 1 1 1 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 1 0));
(= (::.:) (unary 1 1 1 1 1 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 1 1 1 1 1 1 1 0));
(= (:..:) (unary 1 1 1 1 1 1 1 1 1 0));
(= (::.) (unary 1 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 1 1 1 1 1 1 1 1 1 1 0));
(= (:::) (unary 1 1 1 1 1 1 1 0));
(= (:::.) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
(= (:.:) (unary 1 1 1 1 1 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);
((((? z (? x (? y (= (* (x) (y)) (z))))) 11) 1)
11);
((((? z (? x (? y (= (* (x) (y)) (z))))) 121) 11)
11);
((((? z (? x (? y (= (* (x) (y)) (z))))) 156) 12)
13);
((((? z (? x (? y (= (* (x) (y)) (z))))) 16) 2)
8);
((((? z (? x (? y (= (* (x) (y)) (z))))) 0) 4) 0);
((((? z (? x (? y (= (* (x) (y)) (z))))) 108) 12)
9);
((((? z (? x (? y (= (* (x) (y)) (z))))) 80) 10)
8);
((((? z (? x (? y (= (* (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 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
(define pure-if (? x (? y (? z (x (y) (z))))));
(define pure-true (? y (? z (y))));
(define pure-false (? y (? z (z))));
(define pure-cons
(? x (? y (? z (pure-if (z) (x) (y))))));
(define pure-car (? x (x (pure-true))));
(define pure-cdr (? x (x (pure-false))));
(define zero (? f (? x (x))));
(define one (? f (? x (f (x)))));
(define two (? f (? x (f (f (x))))));
(define succ (? n (? f (? x (f ((n (f)) (x)))))));
(define add (? a (? b ((a (succ)) (b)))));
(define mult (? a (? b ((a (add (b))) (zero)))));
(define pred
(? n
(pure-cdr
((n (? p
(pure-cons (succ (pure-car (p))) (pure-car (p)))))
(pure-cons (zero) (zero))))));
(define is-zero
(? n ((n (? dummy (pure-false)) (pure-true)))));
(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
(define unchurch (? c (c (? x (+ (x) 1)) 0)));
(= 0 (unchurch (zero)));
(= 1 (unchurch (one)));
(= 2 (unchurch (two)));
(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
(define easy-factorial
(? f
(? x (if (> (x) 0) (* (x) (f (f) (- (x) 1))) 1))));
(define factorial
(? x
(if (> (x) 0) (* (x) (factorial (- (x) 1))) 1)));
(= (easy-factorial (easy-factorial) 0) 1);
(= (easy-factorial (easy-factorial) 1) 1);
(= (easy-factorial (easy-factorial) 2) 2);
(= (easy-factorial (easy-factorial) 3) 6);
(= (easy-factorial (easy-factorial) 4) 24);
(= (easy-factorial (easy-factorial) 5) 120);
(= (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 =>);
(define => (? x (? y (not (and (x) (not (y)))))));
(=> (true) (true));
(not (=> (true) (false)));
(=> (false) (true));
(=> (false) (false));
(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
#
(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)))))));
(define list
(? n
(if (= (n) 0)
(cons 0 0)
(list-helper (n) (? y (? z (cons (y) (z))))))));
(define head
(? lst
(if (= (car (lst)) 0)
(undefined)
(if (= (car (lst)) 1)
(cdr (lst))
(car (cdr (lst)))))));
(define tail
(? lst
(if (= (car (lst)) 0)
(undefined)
(if (= (car (lst)) 1)
(cons 0 0)
(cons (- (car (lst)) 1) (cdr (cdr (lst))))))));
(define list-length (? lst (car (lst))));
(define list-ref
(? lst
(? n
(if (= (list-ref (lst)) 0)
(undefined)
(if (= (n) 0)
(head (lst))
(list-ref (tail (lst)) (- (n) 1)))))));
(define prepend
(? x
(? lst
(if (= (list-length (lst)) 0)
(cons 1 (x))
(cons (+ (list-length (lst)) 1)
(cons (x) (cdr (lst))))))));
(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)))));
(= (list-length ((list 1) 3)) 1);
(= (list-length ((list 8) 9 8 0 4 7 3 6 5)) 8);
(= (list-length ((list 5) 8 6 4 2 5)) 5);
(= (list-length ((list 9) 5 8 4 3 9 6 1 7 2)) 9);
(= (list-length ((list 7) 2 4 9 6 5 0 8)) 7);
(= (head ((list 8) 12 1 4 13 17 3 10 4)) 12);
(list= (tail ((list 8) 12 1 4 13 17 3 10 4))
((list 7) 1 4 13 17 3 10 4));
(= (head ((list 9) 6 13 15 4 12 1 0 5 6)) 6);
(list= (tail ((list 9) 6 13 15 4 12 1 0 5 6))
((list 8) 13 15 4 12 1 0 5 6));
(= (head ((list 6) 19 4 12 2 15 12)) 19);
(list= (tail ((list 6) 19 4 12 2 15 12))
((list 5) 4 12 2 15 12));
(= (head ((list 10) 3 4 4 2 15 3 17 6 11 3)) 3);
(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));
(= (head ((list 2) 15 2)) 15);
(list= (tail ((list 2) 15 2)) ((list 1) 2));
(= (head ((list 10) 15 12 17 11 0 12 14 8 17 5))
15);
(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));
(= (head ((list 5) 11 1 10 7 9)) 11);
(list= (tail ((list 5) 11 1 10 7 9))
((list 4) 1 10 7 9));
(= (head ((list 3) 19 10 14)) 19);
(list= (tail ((list 3) 19 10 14))
((list 2) 10 14));
(= (head ((list 5) 4 2 7 12 18)) 4);
(list= (tail ((list 5) 4 2 7 12 18))
((list 4) 2 7 12 18));
(= (head ((list 5) 13 1 0 5 10)) 13);
(list= (tail ((list 5) 13 1 0 5 10))
((list 4) 1 0 5 10));
(= (list-ref ((list 1) 9) 0) 9);
(= (list-ref ((list 10) 4 4 14 0 14 4 17 7 3 17) 0)
4);
(= (list-ref ((list 8) 10 13 6 14 3 13 9 18) 0)
10);
(= (list-ref ((list 4) 3 1 0 2) 2) 0);
(= (list-ref ((list 5) 13 7 18 13 12) 1) 7);
(= (list-ref ((list 3) 19 16 9) 2) 9);
(= (list-ref ((list 5) 12 14 5 14 4) 4) 4);
(= (list-ref ((list 2) 10 17) 1) 17);
(= (list-ref ((list 4) 1 12 10 18) 3) 18);
(= (list-ref ((list 8) 17 7 2 4 19 15 4 9) 0) 17);
(list= ((list 0)) ((list 0)));
(list= ((list 1) 7) ((list 1) 7));
(list= ((list 2) 1 19) ((list 2) 1 19));
(list= ((list 3) 18 1 18) ((list 3) 18 1 18));
(list= ((list 4) 13 15 10 6)
((list 4) 13 15 10 6));
# this next batch of examples are a bit misleading, should streamline
(not (list= ((list 0)) ((list 1) 0)));
(not (list= ((list 0)) ((list 1) 6)));
(not (list= ((list 1) 9) ((list 2) 6 9)));
(not (list= ((list 1) 9) ((list 2) 9 7)));
(not (list= ((list 2) 1 6) ((list 3) 2 1 6)));
(not (list= ((list 2) 1 6) ((list 3) 1 6 0)));
(not (list= ((list 3) 10 9 12) ((list 4) 5 10 9 12)));
(not (list= ((list 3) 10 9 12) ((list 4) 10 9 12 3)));
(not (list= ((list 4) 17 9 1 0) ((list 5) 4 17 9 1 0)));
(not (list= ((list 4) 17 9 1 0) ((list 5) 17 9 1 0 4)));
# some helpful functions
(list= (prepend 12 ((list 0))) ((list 1) 12));
(list= (prepend 0 ((list 1) 14)) ((list 2) 0 14));
(list= (prepend 10 ((list 2) 8 19))
((list 3) 10 8 19));
(list= (prepend 12 ((list 3) 10 2 1))
((list 4) 12 10 2 1));
(list= (prepend 14 ((list 4) 6 16 14 5))
((list 5) 14 6 16 14 5));
(list= (prepend 4 ((list 5) 15 2 3 11 8))
((list 6) 4 15 2 3 11 8));
(list= (prepend 12 ((list 6) 9 2 19 7 2 0))
((list 7) 12 9 2 19 7 2 0));
(list= (prepend 11 ((list 7) 17 17 2 4 16 5 14))
((list 8) 11 17 17 2 4 16 5 14));
(define pair (? x (? y ((list 2) (x) (y)))));
(define first (? lst (head (lst))));
(define second (? lst (head (tail (lst)))));
(list= (pair 3 6) ((list 2) 3 6));
(= (first (pair 3 6)) 3);
(= (second (pair 3 6)) 6);
(list= (pair 8 8) ((list 2) 8 8));
(= (first (pair 8 8)) 8);
(= (second (pair 8 8)) 8);
(list= (pair 9 2) ((list 2) 9 2));
(= (first (pair 9 2)) 9);
(= (second (pair 9 2)) 2);
(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)))))))));
(define list-find
(? lst
(? key
(? fail (list-find-helper (lst) (key) (fail) 0)))));
(define example-fail (? x 100));
(= (list-find ((list 1) 15) 15 (example-fail)) 0);
(= (list-find ((list 2) 9 6) 9 (example-fail)) 0);
(= (list-find
((list 4) 19 7 14 6)
19
(example-fail))
0);
(= (list-find
((list 8) 10 0 6 9 5 10 2 2)
5
(example-fail))
4);
(= (list-find ((list 4) 14 5 7 6) 6 (example-fail))
3);
(= (list-find ((list 1) 2) 2 (example-fail)) 0);
(= (list-find
((list 7) 19 7 12 4 18 8 7)
4
(example-fail))
3);
(= (list-find ((list 1) 2) 2 (example-fail)) 0);
(= (list-find
((list 4) 5 19 13 13)
19
(example-fail))
1);
(= (list-find
((list 10) 17 14 17 8 6 1 2 12 10 4)
1
(example-fail))
5);
(= (list-find
((list 4) 15 13 6 17)
14
(example-fail))
100);
(= (list-find
((list 6) 16 13 10 3 0 19)
2
(example-fail))
100);
(= (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
(define base-translate (translate));
(define translate
(? x (if (= (x) 10) 15 (base-translate (x)))));
(= 10 15);
(= (+ 10 15) 30);
(define translate (base-translate));
(not (= 10 15));
(= (+ 10 15) 25);
# now can create a special form for lists
(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))))));
(= (vector 1 2 3) ((list 3) 1 2 3));
# now to desugar let expressions
(define translate-with-vector (translate));
(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))))))))));
(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))))));
(let ((x 20)) (= (x) 20));
(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
(define is-list (? x (not (number? (x)))));
(is-list ((list 2) 1 3));
(is-list ((list 0)));
(not (is-list 23));
(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
(intro let);
(= (let ((x 10)) (+ (x) 5)) ((? x (+ (x) 5)) 10));
(= (let ((x 10) (y 5)) (+ (x) (y)))
(((? x (? y (+ (x) (y)))) 10) 5));
# MATH build up functions of several variables
(= ((? x (? y (- (x) (y)))) 12 6) 6);
(= ((? x (? y (- (x) (y)))) 3 0) 3);
(= ((? x (? y (- (x) (y)))) 8 7) 1);
(= ((? x (? y (- (x) (y)))) 7 6) 1);
(= ((? x (? y (- (x) (y)))) 7 6) 1);
(define last
(? x (list-ref (x) (- (list-length (x)) 1))));
(define except-last
(? x
(if (> (list-length (x)) 1)
(prepend (head (x)) (except-last (tail (x))))
(vector))));
# test last and except-last
(= 15 (last (vector 4 5 15)));
(list= (vector 4 5)
(except-last (vector 4 5 15)));
(intro lambda);
(define prev-translate (translate));
(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
(= (? x (- (x) 5)) (lambda (x) (- (x) 5)));
(= (? x (? y (- (x) (y))))
(lambda (x y) (- (x) (y))));
(= ((lambda (x y) (- (x) (y))) 17 9) 8);
(= ((lambda (x y) (- (x) (y))) 9 2) 7);
(= ((lambda (x y) (- (x) (y))) 13 8) 5);
(= ((lambda (x y) (- (x) (y))) 8 6) 2);
(= ((lambda (x y) (- (x) (y))) 3 3) 0);
(define apply
(lambda (x y)
(if (list= (y) (vector))
(x)
(apply ((x) (head (y))) (tail (y))))));
(= (apply (lambda (x y) (- (x) (y))) (vector 12 6))
6);
(= (apply (lambda (x y) (- (x) (y))) (vector 10 7))
3);
(= (apply (lambda (x y) (- (x) (y))) (vector 12 3))
9);
(= (apply (lambda (x y) (- (x) (y))) (vector 6 5))
1);
(= (apply (lambda (x y) (- (x) (y))) (vector 0 0))
0);
# MATH show map function for applying a function across the elements of a list
(define map
(lambda (p lst)
(if (> (list-length (lst)) 0)
(prepend (p (head (lst))) (map (p) (tail (lst))))
(vector))));
(= (map (? x (* (x) 2)) (vector 3 18 17))
(vector 6 36 34));
(= (map (? x (* (x) 2)) (vector 6 11 7 9))
(vector 12 22 14 18));
(= (map (? x (* (x) 2)) (vector 6 14 16 1 11))
(vector 12 28 32 2 22));
(= (map (? x (* (x) 2)) (vector 13 11 19 9 7 16))
(vector 26 22 38 18 14 32));
(= (map (? x 42) (vector 15 3 19))
(vector 42 42 42));
(= (map (? x 42) (vector 2 15 6 19))
(vector 42 42 42 42));
(= (map (? x 42) (vector 2 9 11 5 13))
(vector 42 42 42 42 42));
(= (map (? x 42) (vector 19 12 17 18 5 8))
(vector 42 42 42 42 42 42));
(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)))));
(= (crunch (+) (vector 17 7 18)) 42);
(= (crunch (+) (vector 19 10 0 11)) 40);
(= (crunch (+) (vector 7 16 11 8 19)) 61);
(= (crunch (+) (vector 1 5 14 16 15 19)) 70);
# 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);
# MATH show how to execute a sequence of instructions
(intro begin);
(define prev-translate (translate));
(define reverse
(? x
(if (>= (list-length (x)) 1)
(prepend (last (x)) (reverse (except-last (x))))
(x))));
# test reverse
(list= (vector 1 2 3) (reverse (vector 3 2 1)));
(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)))))));
(= (begin 1 7 2 4) 4);
(= (begin
(set! (demo-mut1) 88)
(set! (demo-mut1) 6)
(get! (demo-mut1)))
6);
(= (begin
(set! (demo-mut2) 88)
(set! (demo-mut1) 6)
(get! (demo-mut2)))
88);
(= (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)
(define hash-add
(lambda (h x y z) (if (= (z) (x)) (y) (h (z)))));
(define hash-ref (lambda (h x) (h (x))));
(define hash-null (? x (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
(if (list= (x) (vector))
(hash-null)
(hash-add
(make-hash (tail (x)))
(first (head (x)))
(second (head (x)))))));
(= (hash-ref
(make-hash
(vector (pair 3 10) (pair 2 20) (pair 1 30)))
3)
10);
(= (hash-ref
(make-hash
(vector (pair 3 10) (pair 2 20) (pair 1 30)))
1)
30);
# OBJECT introduce simple mutable structures
(define mutable-struct
(? lst
(let ((data (map (? x (make-cell 0)) (lst))))
(? key
(list-ref (data) (list-find (lst) (key) (? x 0)))))));
(define test-struct1
(mutable-struct (vector item1 item2 item3)));
(set! (test-struct1 item1) 15);
(= (get! (test-struct1 item1)) 15);
# OBJECT introduce method handler wrappers
(define add-method
(lambda (object name method)
(hash-add
(object)
(name)
(? dummy (method (object))))));
(define call (? x (x 0)));
(define test-struct2
(mutable-struct (vector x y)));
(set! (test-struct2 x) 10);
(set! (test-struct2 y) 20);
(= (get! (test-struct2 x)) 10);
(= (get! (test-struct2 y)) 20);
(define test-struct3
(add-method
(test-struct2)
sum
(? self (+ (get! (self x)) (get! (self y))))));
(= (get! (test-struct3 x)) 10);
(= (get! (test-struct3 y)) 20);
(= (call (test-struct3 sum)) 30);
(set! (test-struct3 y) 10);
(= (call (test-struct3 sum)) 20);
(set! (test-struct2 y) 5);
(= (call (test-struct3 sum)) 15);
# TURING introduce turing machine model
# just for fun!
(define safe-tail
(? x
(if (> (list-length (x)) 0)
(if (> (list-length (x)) 1)
(tail (x))
(vector (false)))
(? vector (false)))));
(define safe-head
(? x
(if (> (list-length (x)) 0) (head (x)) (false))));
(define tape-read
(? tape
(let ((x (second (tape))))
(if (> (list-length (x)) 0) (head (x)) (false)))));
(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)))))))));
(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)))))));
(define make-tape (? x (pair (vector) (x))));
(define remove-trail
(? x
(? lst
(if (> (list-length (lst)) 0)
(if (= (last (lst)) (x))
(remove-trail (x) (except-last (lst)))
(lst))
(lst)))));
(define extract-tape
(? x (remove-trail (false) (second (x)))));
(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))))));
(= (extract-tape
(turing
(tm-binary-increment)
right
halt
(make-tape (vector 1 0 0 1))))
(vector 1 0 1 0));
(= (extract-tape
(turing
(tm-binary-increment)
right
halt
(make-tape (vector 1 1 1))))
(vector 1 0 0 0));
(= (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
(intro element);
(define element
(? x
(? lst
(not (= (list-find (lst) (x) (? y (false))) (false))))));
(element 9 (vector 7 9 5 6));
(element 6 (vector 7 9 5 6));
(element 7 (vector 7 9 5 6));
(element 9 (vector 7 1 9 2 4));
(element 1 (vector 7 1 9 2 4));
(element 9 (vector 7 1 9 2 4));
(element 2 (vector 7 8 0 9 2 6));
(element 9 (vector 7 8 0 9 2 6));
(element 0 (vector 7 8 0 9 2 6));
(element 1 (vector 9 1 3 6));
(element 1 (vector 9 1 3 6));
(element 1 (vector 9 1 3 6));
(element 4 (vector 8 1 2 3 4));
(element 8 (vector 8 1 2 3 4));
(element 1 (vector 8 1 2 3 4));
(not (element 0 (vector 8 2 3 5)));
(not (element 8 (vector 0 1 3 5)));
(not (element 0 (vector 8 3 4)));
(not (element 7 (vector 8 4 5 6)));
(not (element 7 (vector 0 9 2 3)));
# rules for set equality
(define set-subset
(? x
(? y
(if (> (list-length (x)) 0)
(and (element (head (x)) (y))
(set-subset (tail (x)) (y)))
(true)))));
(define set=
(? x
(? y
(and (set-subset (x) (y)) (set-subset (y) (x))))));
(set= (vector 1 5 9) (vector 5 1 9));
(set= (vector 1 5 9) (vector 9 1 5));
(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
(element 5 (all (? x (= (+ (x) 10) 15))));
(element 3 (all (? x (= (* (x) 3) (+ (x) 6)))));
(define empty-set (vector));
(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 (vector (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))
(= (* 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 introduce graph structures
(define make-graph
(lambda (nodes links) (pair (nodes) (links))));
(define test-graph
(make-graph
(vector 1 2 3 4)
(vector (vector 1 2) (vector 2 3) (vector 1 4))));
(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))))));
(= (graph-linked (test-graph) 1 2) (true));
(= (graph-linked (test-graph) 1 3) (false));
(= (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'.
(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))))))));
(= (graph-linked* (test-graph) 1 2) (true));
(= (graph-linked* (test-graph) 1 3) (true));
(= (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.
(define make-integer
(lambda (v) (lambda (x) (if (= (x) int) (v) 0))));
(define objectify
(? x (if (number? (x)) (make-integer (x)) (x))));
(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
(define prev-translate (translate));
(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
(define prev-translate (translate));
(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)))))));
(= 99 (cond 99));
(= 8 (cond ((true) 8) 11));
(= 11 (cond ((false) 8) 11));
(= 7 (cond ((false) 3) ((true) 7) 11));
(= 3 (cond ((true) 3) ((true) 7) 11));
(= 11 (cond ((false) 3) ((false) 7) 11));
(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))));
(define remove-element
(lambda (x)
(remove-match (lambda (y) (= (y) (x))))));
(list= (vector 1 2 3 5)
(remove-element 4 (vector 1 2 3 4 5)));
(list= (vector 1 2 3 5)
(remove-element 4 (vector 1 4 2 4 3 4 5)));
(define return
(lambda (t t)
(let ((obj (objectify (t)))) (obj (t)))));
(define tester
(lambda ((x int) (y int))
(return int (+ (x) (y)))));
(= 42
(tester (make-integer 10) (make-integer 32)));
(= 42 (tester 10 32));
(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
(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)))));
(define point1 (point 1 11));
(define point2 (point 2 22));
(= 1 (point1 x));
(= 22 (point2 y));
(= 11 ((point 11 12) x));
(= 11 (((point 11 12) point) x));
(= 16 (((point 16 17) point) x));
(= 33 (point1 + (point2) y));
(point1 + (point2) = (point 3 33));
(point2 + (point1) = (point 3 33));
((point 100 200)
+
(point 200 100)
=
(point 300 300));
(instanceof point (point1));
(not (instanceof int (point1)));
(instanceof int 5);
(not (instanceof point 5));
# OBJECT an example object -- a container
(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
(define pocket (container new));
(pocket add 77);
(pocket add 88);
(pocket add 99);
(set= (pocket inventory) (vector 77 88 99));
(pocket remove 88);
(set= (pocket inventory) (vector 77 99));
(define pocket2 (container new));
(pocket2 add 77);
(pocket2 add 99);
(pocket2 = (pocket));
# OBJECT expressing inheritance
# counter-container adds one method to container: count
(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))))))));
(define cc1 (counter-container new));
(= 0 (cc1 count));
(cc1 add 4);
(= 1 (cc1 count));
(cc1 add 5);
(= 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
(define list-append
(lambda (lst1 lst2)
(if (> (list-length (lst1)) 0)
(list-append
(except-last (lst1))
(prepend (last (lst1)) (lst2)))
(lst2))));
(= (list-append (vector 1 2 3) (vector 4 5 6))
(vector 1 2 3 4 5 6));
(define append
(? x
(? lst
(if (> (list-length (lst)) 0)
(prepend (head (lst)) (append (x) (tail (lst))))
(vector (x))))));
(= (append 5 (vector 1 2)) (vector 1 2 5));
(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))));
(define unique
(let ((store (make-cell 0)))
(lambda (x)
(let ((id (get! (store))))
(begin (set! (store) (+ (id) 1)) (id))))));
(= (unique new) 0);
(= (unique new) 1);
(= (unique new) 2);
(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.
(define prev-translate (translate));
(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
(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
(define point1 (point new 1 11));
(define point2 (point new 2 22));
(= 1 (point1 x));
(= 22 (point2 y));
(= 11 ((point new 11 12) x));
(= 11 (((point new 11 12) point) x));
(= 16 (((point new 16 17) point) x));
(= 33 (point1 + (point2) y));
(point1 + (point2) = (point new 3 33));
(point2 + (point1) = (point new 3 33));
((point new 100 200)
+
(point new 200 100)
=
(point new 300 300));
(instanceof point (point1));
(not (instanceof int (point1)));
# OBJECT wrapper class for cells
(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)))));
(define cell-test1 (cell new 15));
(= 15 (cell-test1 get));
(cell-test1 set 82);
(= 82 (cell-test1 get));
(define cell-test2
(cell new (point new 120 150)));
(define cell-test3
(cell new (point new 300 300)));
(cell-test2 + (cell-test3) = (point new 420 450));
(not (cell-test2 = (cell-test3)));
(cell-test3 set (cell-test2));
(cell-test2 = (cell-test3));
# MUD playing around with doors and rooms
(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)))));
(class room
()
(field content (container new))
(method unknown (lambda (x) (content (x)))));
# need to fix up containers to use object equality
(define object-element
(lambda (n lst)
(> (list-length
(select-match (lambda (x) (x == (n))) (lst)))
0)));
(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)))));
(define hall (room new));
(define kitchen (room new));
(define door1 (door new (hall) (kitchen)));
((first (hall inventory)) == (door1));
((first (kitchen inventory)) == (door1));
(door1 access-from (hall) == (kitchen));
(not (door1 access-from (hall) == (hall)));
(door1 access-from (kitchen) == (hall));
(define lawn (room new));
(define stairs (room new));
(define bedroom (room new));
(define nowhere (room new));
(define door2 (door new (hall) (lawn)));
(define door3 (door new (hall) (stairs)));
(define door4 (door new (stairs) (bedroom)));
(class character
()
(field location (cell new (nowhere)))
(method
set-room
(lambda ((r room)) (location set (r))))
(method get-room (location get))
(method update 0));
(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))));
(define find-max-idx
(lambda (test lst)
(find-max-helper
(test)
(test (head (lst)))
0
0
(lst))));
(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))));
(define find-min-idx
(lambda (test lst)
(find-min-helper
(test)
(test (head (lst)))
0
0
(lst))));
(= 2
(find-max-idx (lambda (x) (x)) (vector 3 4 5 0)));
(= 1
(find-max-idx (lambda (x) (x)) (vector 3 5 4 0)));
(= 0
(find-max-idx (lambda (x) (x)) (vector 5 3 4 0)));
# the robo class makes a character that patrols from room to room
(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))))))));
(define myrobo (robo new));
(myrobo set-room (stairs));
(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)))));
(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
(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