Commit 66520e525d2ec86c795e87321cbc42e5e306c903 - cafeobj

+10

-1

BigPink/codes/butils.lisp less more

89	89	(let ((var (find-if #'(lambda (x) (variable-eq term x)) variables)))
90	90	(if var
91	91	var
	92	#\|\|
92	93	(if variables
93	94	(with-output-panic-message-n (:p-pn-0010 (list (variable-name term)))
94	95	;; (format t "copying term, could not find var ~a"
95	96	;; (variable-name term))
96	97	(break "type in :q for returning to top-level.")
97	98	)
98		term))))
	99	term)
	100	\|\|#
	101	term )))
99	102	((term-is-application-form? term)
100	103	(@create-application-form-term
101	104	(term-head term)

988	991	;;;
989	992	(defun pn-automatic-settings-1 ()
990	993	;;
	994	#\|\|
991	995	(unless current-psys
992	996	(with-output-panic-message-n (:p-pn-0020)
993	997	;; (format t "system error, no context in PigNose environment.")
994	998	))
	999	\|\|#
995	1000	(move-axioms-to-usable current-psys)
996	1001	(setf usable (psystem-usable current-psys))
997	1002	(setf sos nil)

1170	1175
1171	1176	(defun pn-automatic-settings-2 ()
1172	1177	;;
	1178	#\|\|
1173	1179	(unless current-psys
1174	1180	(with-output-panic-message-n (:p-pn-0020)
1175	1181	;;(format t "system error, no context in PigNose env.")
1176	1182	))
	1183	\|\|#
1177	1184	(move-axioms-to-usable current-psys)
1178	1185	(setf usable (psystem-usable current-psys))
1179	1186	(setf sos nil)

1306	1313
1307	1314	(defun pn-automatic-settings-3 ()
1308	1315	;;
	1316	#\|\|
1309	1317	(unless current-psys
1310	1318	(with-output-panic-message-n (:p-pn-0020)
1311	1319	;; (format t "system error, no context in PigNose env.")
1312	1320	))
	1321	\|\|#
1313	1322	(move-axioms-to-usable current-psys)
1314	1323	(setf usable (psystem-usable current-psys))
1315	1324	(setf sos nil)

+6

-1

BigPink/codes/clause.lisp less more

408	408	(setq usable (list clause)))
409	409	(incf (pn-stat usable-size)))
410	410	(otherwise
	411	#\|\|
411	412	(with-output-panic-message-n (:p-gl-0010 (list 'append-clause list))
412	413	;; (format t "append-clause: not yet ~s" list)
413		)))
	414	)
	415	\|\|#
	416	))
414	417	(setf (clause-container clause) list)
415	418	)
416	419

431	434	(incf (pn-stat demodulators-size)))
432	435	\|\|#
433	436	)
	437	#\|\|
434	438	(unless real-list
435	439	(with-output-panic-message-n (:p-pn-0040)
436	440	;; (princ "prepend-clause: nil")
437	441	))
	442	\|\|#
438	443	(setf (cdr real-list) (cons (car real-list) (cdr real-list)))
439	444	(setf (car real-list) clause)
440	445	(setf (clause-container clause) list)))

+6

-7

Makefile less more

14	14	VERSION = 1.4
15	15	VMINOR = .9
16	16	VMEMO = PigNose0.99
17		PATCHLEVEL =
	17	PATCHLEVEL = 1
18	18
19	19	# Where to install the executables.
20	20	bindir = ${exec_prefix}/bin

43	43	GCL = no
44	44	CMU = no
45	45	ACL = no
46		LISP = no
47		BIN = .fasl
48		EXEC_SRC = cafeobj.acl.in
49		EXEC = cafeobj.acl
	46	LISP = /opt/local/bin/clisp
	47	BIN = .fas
	48	EXEC_SRC = cafeobj.clisp.in
	49	EXEC = cafeobj.mem
50	50
51	51	#### End of system configuration section. ####
52	52

61	61
62	62	DISTDIRTOP = $(PACKAGE)-$(VERSION)$(VMINOR)
63	63
64		DISTSUBDIRS = cafeobj clII comlib thstuff chaos win mac \
	64	DISTSUBDIRS = cafeobj clII comlib thstuff chaos \
65	65	chaos/boot chaos/cafein chaos/construct chaos/decafe chaos/e-match \
66	66	chaos/eval chaos/primitives chaos/term-parser chaos/tools \
67	67	chaos/tram chaos/psup \
68	68	elisp \
69		dist \
70	69	RefCard BigPink/codes BigPink/test
71	70
72	71	DISTBINSUBDIRS = bin/cafeobj bin/clII bin/comlib bin/obj3 bin/thstuff bin/chaos \

+1

-2

Makefile.in less more

61	61
62	62	DISTDIRTOP = $(PACKAGE)-$(VERSION)$(VMINOR)
63	63
64		DISTSUBDIRS = cafeobj clII comlib thstuff chaos win mac \
	64	DISTSUBDIRS = cafeobj clII comlib thstuff chaos \
65	65	chaos/boot chaos/cafein chaos/construct chaos/decafe chaos/e-match \
66	66	chaos/eval chaos/primitives chaos/term-parser chaos/tools \
67	67	chaos/tram chaos/psup \
68	68	elisp \
69		dist \
70	69	RefCard BigPink/codes BigPink/test
71	70
72	71	DISTBINSUBDIRS = bin/cafeobj bin/clII bin/comlib bin/obj3 bin/thstuff bin/chaos \

+2

-2

autom4te.cache/output.0 less more

1694	1694
1695	1695	PACKAGE=cafeobj
1696	1696	VERSION=1.4
1697		VMINOR=.9rc9
	1697	VMINOR=.9
1698	1698	VMEMO=PigNose0.99
1699		PATCHLEVEL=
	1699	PATCHLEVEL=1
1700	1700
1701	1701
1702	1702

+19

-19

autom4te.cache/requests less more

13	13	'configure.in'
14	14	],
15	15	{
	16	'_LT_AC_TAGCONFIG' => 1,
16	17	'AM_PROG_F77_C_O' => 1,
17		'_LT_AC_TAGCONFIG' => 1,
	18	'AC_INIT' => 1,
18	19	'm4_pattern_forbid' => 1,
19		'AC_INIT' => 1,
	20	'_AM_COND_IF' => 1,
20	21	'AC_CANONICAL_TARGET' => 1,
21		'_AM_COND_IF' => 1,
	22	'AC_SUBST' => 1,
22	23	'AC_CONFIG_LIBOBJ_DIR' => 1,
23		'AC_SUBST' => 1,
	24	'AC_FC_SRCEXT' => 1,
24	25	'AC_CANONICAL_HOST' => 1,
25		'AC_FC_SRCEXT' => 1,
26	26	'AC_PROG_LIBTOOL' => 1,
27	27	'AM_INIT_AUTOMAKE' => 1,
	28	'AM_PATH_GUILE' => 1,
28	29	'AC_CONFIG_SUBDIRS' => 1,
29		'AM_PATH_GUILE' => 1,
30	30	'AM_AUTOMAKE_VERSION' => 1,
31	31	'LT_CONFIG_LTDL_DIR' => 1,
	32	'AC_REQUIRE_AUX_FILE' => 1,
32	33	'AC_CONFIG_LINKS' => 1,
33		'AC_REQUIRE_AUX_FILE' => 1,
	34	'm4_sinclude' => 1,
34	35	'LT_SUPPORTED_TAG' => 1,
35		'm4_sinclude' => 1,
36	36	'AM_MAINTAINER_MODE' => 1,
37	37	'AM_NLS' => 1,
38	38	'AC_FC_PP_DEFINE' => 1,
39	39	'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
	40	'AM_MAKEFILE_INCLUDE' => 1,
40	41	'_m4_warn' => 1,
41		'AM_MAKEFILE_INCLUDE' => 1,
42	42	'AM_PROG_CXX_C_O' => 1,
	43	'_AM_COND_ENDIF' => 1,
43	44	'_AM_MAKEFILE_INCLUDE' => 1,
44		'_AM_COND_ENDIF' => 1,
45	45	'AM_ENABLE_MULTILIB' => 1,
46	46	'AM_SILENT_RULES' => 1,
47	47	'AM_PROG_MOC' => 1,
48	48	'AC_CONFIG_FILES' => 1,
	49	'include' => 1,
49	50	'LT_INIT' => 1,
50		'include' => 1,
	51	'AM_PROG_AR' => 1,
51	52	'AM_GNU_GETTEXT' => 1,
52		'AM_PROG_AR' => 1,
53	53	'AC_LIBSOURCE' => 1,
	54	'AM_PROG_FC_C_O' => 1,
54	55	'AC_CANONICAL_BUILD' => 1,
55		'AM_PROG_FC_C_O' => 1,
56	56	'AC_FC_FREEFORM' => 1,
	57	'AH_OUTPUT' => 1,
57	58	'AC_FC_PP_SRCEXT' => 1,
58		'AH_OUTPUT' => 1,
	59	'_AM_SUBST_NOTMAKE' => 1,
59	60	'AC_CONFIG_AUX_DIR' => 1,
60		'_AM_SUBST_NOTMAKE' => 1,
	61	'sinclude' => 1,
	62	'AM_PROG_CC_C_O' => 1,
61	63	'm4_pattern_allow' => 1,
62		'AM_PROG_CC_C_O' => 1,
63		'sinclude' => 1,
	64	'AM_XGETTEXT_OPTION' => 1,
	65	'AC_CANONICAL_SYSTEM' => 1,
64	66	'AM_CONDITIONAL' => 1,
65		'AC_CANONICAL_SYSTEM' => 1,
66		'AM_XGETTEXT_OPTION' => 1,
67	67	'AC_CONFIG_HEADERS' => 1,
68	68	'AC_DEFINE_TRACE_LITERAL' => 1,
69	69	'AM_POT_TOOLS' => 1,

+4

-1

cafeobj/cafeobj-top.lisp less more

211	211	))
212	212	(setq chaos-vergine nil)))
213	213	;; message DB
	214	#+:Allegro
214	215	(setup-message-db)
215	216	;; help DB
216		(setup-help-db))
	217	#+:Allegro
	218	(setup-help-db)
	219	)
217	220
218	221	;;; **********************
219	222	;;; THE TOP LEVEL FUNCTION

+1

-1

chaos/construct/module.lisp less more

221	221
222	222	;; for simple-parser.
223	223	;; (check-polimorphic-overloading-in module)
224		(propagate-attributes module)
	224	;; (propagate-attributes module)
225	225	(set-operator-syntactic-properties module)
226	226	(update-parse-information module)
227	227	;;

+7

-7

chaos/e-match/match-system.lisp less more

251	251	;; the different top level
252	252	;; possibly maches only when zero case...
253	253	;;
254		#\|\|
	254	;; #\|\|
255	255	(if (or (test-theory .Z. (theory-info-code th-info))
256	256	(test-theory .Z. (theory-info-code
257	257	(method-theory-info-for-matching!

260	260	nil)
261	261	;; will never match
262	262	t)
263		\|\|#
264		t
	263	;;\|\|#
	264	;;t
265	265	)
266	266	))))
267	267

340	340	;; the different top level
341	341	;; possibly maches only when zero case or on-demand.
342	342	;;
343		#\|\| too danderous: many cases of rewriting rush into infinite loop.
	343	;; #\|\| too danderous: many cases of rewriting rush into infinite loop.
344	344	(if (term-is-on-demand? t2)
345	345	(progn
346	346	(mark-term-as-not-on-demand t2)

365	365	nil)
366	366	;; will never match
367	367	t))
368		\|\|#
369		;; #\|\|
	368	;; \|\|#
	369	#\|\|
370	370	(if (term-is-on-demand? t2)
371	371	(progn
372	372	(mark-term-as-not-on-demand t2)

376	376	(!match-decompose t1 t2 res)))
377	377	;; never ...
378	378	t)
379		;; \|\|#
	379	\|\|#
380	380	)))
381	381	))
382	382

+58

-0

chaos/primitives/boperator.lisp less more

1680	1680	(return-from lowest-method
1681	1681	(or (choose-lowest-op cand) method))))
1682	1682
	1683	(defun lowest-method! (method lower-bound &optional (module current-module))
	1684	(declare (type method method)
	1685	(type list lower-bound)
	1686	(type module module)
	1687	(values (or null method)))
	1688	(flet ((select-one-method (method-list)
	1689	;; select arbitrary one if every has the same rank
	1690	(let* ((cand (car method-list))
	1691	(coar (method-coarity cand))
	1692	(arity (method-arity cand)))
	1693	(dolist (m (cdr method-list) cand)
	1694	(unless (sort= coar (method-coarity m))
	1695	(return-from select-one-method nil))
	1696	(unless (sort-list= arity (method-arity m))
	1697	(return-from select-one-method nil))))))
	1698	(let ((current-sort-order (module-sort-order module))
	1699	(current-opinfo-table (module-opinfo-table module))
	1700	(res nil))
	1701	(declare (type hash-table current-sort-order current-opinfo-table))
	1702	(let ((over-methods (method-overloaded-methods
	1703	method
	1704	(module-opinfo-table module))))
	1705
	1706	(declare (type list over-methods))
	1707	(when on-debug
	1708	(format t "~%* lowest-method! : over-methods =")
	1709	(dolist (m over-methods)
	1710	(terpri)
	1711	(princ " ")
	1712	(print-chaos-object m)))
	1713	;;
	1714	(if over-methods
	1715	(progn
	1716	(dolist (meth over-methods)
	1717	(declare (type method meth))
	1718	(when (and (sort-list<= lower-bound (method-arity meth))
	1719	(not (member
	1720	meth
	1721	res
	1722	:test #'(lambda (x y)
	1723	(method-is-instance-of y
	1724	x
	1725	current-sort-order)))
	1726	))
	1727	(push meth res)))
	1728	(when on-debug
	1729	(format t "~%lowest-method! res=")
	1730	(print-chaos-object res)
	1731	)
	1732	(if (cdr res)
	1733	;; was method
	1734	(or (select-one-method res)
	1735	method)
	1736	(car res)))
	1737	(return-from lowest-method! method))))))
	1738
	1739	#\|\|
1683	1740	(defun lowest-method! (method lower-bound &optional (module current-module))
1684	1741	(declare (type method method)
1685	1742	(type list lower-bound)

1714	1771	(or (choose-lowest-op res)
1715	1772	method))
1716	1773	(return-from lowest-method! method)))))
	1774	\|\|#
1717	1775
1718	1776	(defun lowest-method* (method &optional lower-bound (module current-module))
1719	1777	(declare (type method method)

+16

-16

chaos/term-parser/parse-engine.lisp less more

1548	1548	(let ((token-list (cdr arg-acc)) )
1549	1549	(if (null token-list)
1550	1550	nil ;this iteration is finished
1551		(let* ((arg-list (car arg-acc))
1552		(terletox-list (parse-term token-list
1553		module
1554		level-constraint
1555		sort-constraint)))
1556		;; notice that parser is not called with
1557		;; token-list empty
1558		(dolist (terletox terletox-list)
1559		;; if terletox-list empty, no effect
1560		(let* ((arg-prime (caar terletox))
1561		(token-list-prime (cdr terletox))
1562		(arg-list-prime (cons arg-prime arg-list))
1563		;; notice that we accumulate arguments in reverse order
1564		(arg-acc-prime (cons arg-list-prime token-list-prime)))
1565		(setq arg-acc-list-prime
1566		(cons arg-acc-prime arg-acc-list-prime))))))))))
	1551	(let* ((arg-list (car arg-acc))
	1552	(terletox-list (parse-term token-list
	1553	module
	1554	level-constraint
	1555	sort-constraint)))
	1556	;; notice that parser is not called with
	1557	;; token-list empty
	1558	(dolist (terletox terletox-list)
	1559	;; if terletox-list empty, no effect
	1560	(let* ((arg-prime (caar terletox))
	1561	(token-list-prime (cdr terletox))
	1562	(arg-list-prime (cons arg-prime arg-list))
	1563	;; notice that we accumulate arguments in reverse order
	1564	(arg-acc-prime (cons arg-list-prime token-list-prime)))
	1565	(setq arg-acc-list-prime
	1566	(cons arg-acc-prime arg-acc-list-prime))))))))))
1567	1567
1568	1568	;;; op parser-scan-token :
1569	1569	;;; LIST[ ( ChaosTermList . TokenList ) ] -- not empty !

+4

-5

chaos/term-parser/parse-top.lisp less more

208	208	;; if there are some remaining terms serviving these
209	209	;; hard checks, they can be the result.
210	210	pres
211		;; OK, we failed in a test. let ask users which we should
212		;; take as a result.
213		res))
	211	;; OK, we failed in a test. let ask users which we should
	212	;; take as a result.
	213	res))
214	214	res)))
215		\|\|#
216	215
217	216	(defun pre-choose-final (module final)
218	217	(declare (type module module)
219	218	(type list final))
220		(when (every #'term-is-application-form? final)
	219	(when (every #'(lambda(x) (term-is-application-form? x)) final)
221	220	(let ((mslist (mapcar #'(lambda (x) (term-head x)) final))
222	221	(least-op nil)
223	222	(gen-op nil)

+0

-8

~~chaos/tools/patch.lisp~~ less more

0		;;;-- Mode:LISP; Package:CHAOS; Base:10; Syntax:Common-lisp --
1		;;; $Id: patch.lisp,v 1.1.1.1 2003-06-19 08:29:39 sawada Exp $
2
3		;;; PATCH
4		(defvar patch-level 0)
5
6		(defun apply-patch (patch-file target)
7		⏎

+2

-0

comlib/message.lisp less more

37	37	(defun register-message (type msg)
38	38	(setf (gethash (car msg) Message-DB) (cons type (cdr msg))))
39	39
	40	#+:Allegro
40	41	(defun read-message-db (path)
41	42	(clrhash Message-DB)
42	43	(flet ((regme (type msgs)

55	56	(otherwise
56	57	(error "Internal error, invalid message type ~s" type)))))))
57	58
	59	#+:Allegro
58	60	(defun setup-message-db ()
59	61	(let ((fname (chaos-probe-file "messagesDB" chaos-libpath '(".msg"))))
60	62	(unless fname

+2

-2

configure less more

1694	1694
1695	1695	PACKAGE=cafeobj
1696	1696	VERSION=1.4
1697		VMINOR=.9rc9
	1697	VMINOR=.9
1698	1698	VMEMO=PigNose0.99
1699		PATCHLEVEL=
	1699	PATCHLEVEL=1
1700	1700
1701	1701
1702	1702

+2

-2

configure.in less more

5	5	AC_PREREQ(2.4)dnl Required Autoconf version.
6	6	PACKAGE=cafeobj
7	7	VERSION=1.4
8		VMINOR=.9rc9
	8	VMINOR=.9
9	9	VMEMO=PigNose0.99
10		PATCHLEVEL=
	10	PATCHLEVEL=1
11	11	AC_SUBST(PACKAGE)
12	12	AC_SUBST(VERSION)
13	13	AC_SUBST(VMINOR)

+0

-51

~~deliver.cl-~~ less more

0		;;; -- Mode: LISP; Syntax: Common-Lisp --
1		;;; $Id: deliver.cl,v 1.4 2007-09-14 08:55:28 sawada Exp $
2		(in-package :common-lisp-user)
3		(eval-when (eval load)
4		(load "chaos-package.fasl")
5		)
6		(defun make-app (path)
7		(generate-application "CafeOBJ"
8		#-:mswindows
9		"dist/cafeobj-1.4/lisp/"
10		#+:mswindows
11		"dist/cafeobj-1.4/"
12		'("pignose.fasl" :emacs :eli
13		:sock :process
14		:acldns :collate :euc :ffcompat :list2
15		:fileutil :foreign :trace
16		:hmac :locale :regexp2 #-:mswindows :sigio
17		;; #-:mswindows :ssl
18		:ssl
19		:streama)
20		:application-type :exe
21		:print-startup-message nil
22		:allow-existing-directory t
23		:copy-shared-libraries t
24		:read-init-files nil
25		:restart-app-function 'chaos::cafeobj-top-level
26		;; :restart-init-function 'chaos::chaos-init-fun
27		:runtime :standard
28		:suppress-allegro-cl-banner t
29		:runtime-bundle t
30		:include-compiler nil
31		;; :record-source-file-info nil
32		;; :record-xref-info nil
33		;; :load-source-file-info nil
34		;; :load-xref-info nil
35		;; :load-local-names-info nil
36		:autoload-warning t
37		:discard-local-name-info t
38		:discard-source-file-info t
39		;; :discard-xref-into t
40		:discard-arglists t
41		:application-administration
42		'(#+:mswindows
43		(:batch-file "cafeobj.bat")
44		)
45		))
46
47		(eval-when (eval load)
48		(make-app nil))
49
50		;;; EOF

+2

-2

exs/debt-red.mod less more

93	93	exec B .
94	94	--> this needs much time to perform ... please be patient
95	95	clean memo
96		eof
	96	-- eof
97	97	red B ==> 'c 2 'd .
98	98	**
99		eof
	99	-- eof
100	100
101	101	-- -------------------------------
102	102	--> the problem is NOT confluent: both of the following are normal forms

+3

-1

exs/sorting.mod less more

93	93	eq (e >> s) = (e >> s') .
94	94	eq disorder(s) < disorder(s') = true .
95	95	** conclusion
96		red disorder(e s) < disorder(e s') .
	96	--> the reduction causes stack overflow!
	97	--> red disorder(e s) < disorder(e s') .
97	98	close
	99	eof
98	100
99	101	-- proof of (generic) local confluence for the sorting algorithm
100	102	** case 1 for local confluence

+0

-1

exs/watch.mod less more

179	179	}
180	180
181	181	-- tram red in PROOF : RESULT .
182		red in PROOF : RESULT .
183	182	--
184	183	eof
185	184	--

+1

-1

lib/lib/bool.mod less more

23	23	(unless bootstrapping-bool
24	24	(setf bootstrapping-bool t)
25	25	(unless (modexp-is-error (eval-modexp "BOOL"))
26		(with-outout-chaos-error ('more-than-one-bool)
	26	(with-output-chaos-error ('more-than-one-bool)
27	27	(format t "You cann not define BOOL module more than once in a session.")))
28	28	(if (and user-bool (not (equal "" user-bool)))
29	29	(cafeobj-input user-bool)

+1

-1

lib/lib/eql.mod less more

33	33	(prepare-for-parsing eql-module)
34	34	(with-in-module (eql-module)
35	35	(let* ((eq-op (find-operator '("_" "=" "_") 2 eql-module))
36		(eq-meth (lowest-method (car (opinfo-methods eq-op)))))
	36	(eq-meth (lowest-method* (car (opinfo-methods eq-op)))))
37	37	(setq eql-op eq-meth))))
38	38
39	39	lispq

+4

-4

lib/lib/fopl.mod less more

150	150	-- (a) op P : ... Bool ... -> Bool
151	151	-- (b) op Q : ... Bool ... -> S -- S is not Bool
152	152	--
153		-- ¡ú Basically, if one want to use PigNose system, one cannot
	153	-- Basically, if one want to use PigNose system, one cannot
154	154	-- define such operators, otherwise the result is unknown.
155	155	-- System (may) warn if it found such operations.
156	156	--
157		-- ¡ú But, built-in module BOOL does define such operators,
	157	-- But, built-in module BOOL does define such operators,
158	158	-- and how about equality operators?
159	159	--
160	160	-- One of the reason we adopt sort Bool as truth value is

164	164	-- And Bool-valued terms are used as the condition part of axioms,
165	165	-- this is rather ungly, but its too late for now.
166	166	--
167		-- ¡ü "Here is the way we took:"
	167	-- "Here is the way we took:"
168	168	-- Lift up (partially) operations of BOOL to FOPL level.
169	169	-- * "and" ---> &
170	170	-- * "or" ---> \|

180	180	-- in automatic manner.
181	181	-- * Axioms of above operators are "not" used in inference.
182	182	--
183		-- ¡ü "if_then_else_fi"
	183	-- "if_then_else_fi"
184	184	-- Users "cannot" use if_then_else_fi. We don't provide any
185	185	-- support for this operator. Also the following operators
186	186	-- has no support:

manual/manual.pdf less more

Binary diff not shown

+5

-241

manual/manual.sty less more

19	19	{\end{minipage}\end{Sbox}\fbox{\TheSbox}}
20	20	%%%%%
21	21	\usepackage{graphicx}
22		%%%%%%%%%%%%%%%%%% plainmarkruled pagestyle
	22	%%%%% plainmarkruled pagestyle
23	23	\makepagestyle{plainmarkruled}
24	24	\makeheadrule{plainmarkruled}{\textwidth}{\normalrulethickness}
25	25	\makeevenhead{plainmarkruled}{\scshape\leftmark}{}{}

28	28	\makeoddfoot{plainmarkruled}{}{}{\thepage}
29	29	\makepsmarks{plainmarkruled}{\@ruledmarks}
30	30
31		%%%%%%%%%%%%%%%%%% index pagestyle
	31	%%%%% index pagestyle
32	32	\makepagestyle{index}
33	33	\makeheadrule{index}{\textwidth}{\normalrulethickness}
34	34	\makeevenhead{index}{\rightmark}{}{\leftmark}

38	38
39	39	\makeindex
40	40
41		%%%%%%%%%%%%%%%%%%%%%%% glossary
	41	%%%%% glossary
42	42	\makeglossary
43	43	\changeglossactual{?}
44	44	\changeglossnum{\@currentlabel}

56	56	\fi}
57	57	\renewcommand*{\glossarymark}{\markboth{\glossaryname}{\glossaryname}}
58	58
59		%%%%%%%%%%%%%%%%%%%%%%%%%%%% endnotes
60		% \makepagenote
61		% \notepageref% use page numbers
62		% \newcommand*{\notemark}{\markboth{\notesname}{\notesname}}
63		% \renewcommand*{\notedivision}{\chapter{\notesname}\notemark}
64		% \renewcommand*{\notenumintext}[1]{}% no number marks in main text
65		% \renewcommand*{\notenuminnotes}[1]{}% no number marks in listing
66		% \renewcommand*{\idtextinnotes}[1]{\vspace{-0.5\onelineskip}
67		% \par [#1]\space}
68		% \renewcommand*{\notemark}{\markboth{{\scshape \notesname}}{{\scshape \notesname}}}
69		% \renewcommand*{\pagenotesubhead}[3]{%
70		% \section{#1 #2 #3}}
71		%%\renewcommand*{\notemark}{\markboth{\notesname}{\notesname}}
72
73		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
74		%%%% Short and long ToC
75
76		% \newcommand*{\setupshorttoc}{%
77		% \renewcommand*{\contentsname}{Short contents}
78		% \let\oldchangetocdepth\changetocdepth
79		% \let\oldprecistoctext\precistoctext
80		% \renewcommand{\precistoctext}[1]{}
81		% \let\oldcftchapterfillnum\cftchapterfillnum
82		% \renewcommand*{\changetocdepth}[1]{}
83		% \setcounter{tocdepth}{0}% chapters
84		% \renewcommand*{\cftchapterfont}{\hfill\sffamily}
85		% \renewcommand*{\cftchapterpagefont}{\normalfont}
86		% \renewcommand*{\cftchapterleader}{ \textperiodcentered\space}
87		% \renewcommand*{\cftchapterafterpnum}{\cftparfillskip}
88		% %% \setpnumwidth{0em}
89		% %% \setpnumwidth{1.5em}
90		% \renewcommand*{\cftchapterfillnum}[1]{%
91		% {\cftchapterleader}\nobreak
92		% \hbox to 1.5em{\cftchapterpagefont ##1\hfil}\cftchapterafterpnum\par}
93		% \setrmarg{0.3\textwidth}
94		% \setlength{\unitlength}{\@tocrmarg}
95		% \addtolength{\unitlength}{1.5em}
96		% \let\oldcftpartformatpnum\cftpartformatpnum
97		% \renewcommand*{\cftpartformatpnum}[1]{%
98		% \hbox to\unitlength{{\cftpartpagefont ##1}}}
99		% \let\oldcftbookformatpnum\cftbookformatpnum
100		% \renewcommand*{\cftbookformatpnum}[1]{%
101		% \hbox to\unitlength{{\cftbookpagefont ##1}}}}
102
103		% \newcommand*{\setupparasubsecs}{%
104		% \let\oldnumberline\numberline
105		% \renewcommand*{\cftsubsectionfont}{\itshape}
106		% \renewcommand*{\cftsubsectionpagefont}{\itshape}
107		% \renewcommand{\l@subsection}[2]{
108		% \ifnum\c@tocdepth > 1\relax
109		% \def\numberline####1{\textit{####1}~}%
110		% \leftskip=\cftsubsectionindent
111		% \rightskip=\@tocrmarg
112		% %% \advance\rightskip 0pt plus \hsize % uncomment this for raggedright
113		% %% \advance\rightskip 0pt plus 2em % uncomment this for semi-ragged
114		% \parfillskip=\fill
115		% \ifhmode ,\ \else\noindent\fi
116		% \ignorespaces
117		% {\cftsubsectionfont ##1}~{\cftsubsectionpagefont##2}%
118		% \let\numberline\oldnumberline\ignorespaces
119		% \fi}}
120
121		% \AtEndDocument{\addtocontents{toc}{\par}}%%% OK
122
123		% \newcommand*{\setupmaintoc}{%
124		% \renewcommand{\contentsname}{Contents}
125		% \let\changetocdepth\oldchangetocdepth
126		% \let\precistoctext\oldprecistoctext
127		% \let\cftchapterfillnum\oldcftchapterfillnum
128		% \addtodef{\cftchapterbreak}{\par}{}
129		% \renewcommand*{\cftchapterfont}{\normalfont\sffamily}
130		% \renewcommand*{\cftchapterleader}{\sffamily\cftdotfill{\cftchapterdotsep}}
131		% \renewcommand*{\cftchapterafterpnum}{}
132		% \renewcommand{\cftchapterbreak}{\par\addpenalty{-\@highpenalty}}
133		% \setpnumwidth{2.55em}
134		% \setrmarg{3.55em}
135		% \setcounter{tocdepth}{2}
136		% \let\cftpartformatpnum\oldcftpartformatpnum
137		% \addtodef{\cftpartbreak}{\par}{}
138		% \let\cftbookformatpnum\oldcftbookformatpnum
139		% \addtodef{\cftbookbreak}{\par}{}
140		% }
141
142		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
143
144		% \newcommand*{\theclass}{memoir}
145
146		% %%% Print and Index macros
147		% \newcommand*{\noidxnum}[1]{}
148
149		% %% index @ in macrocode
150		% \newcommand*{\idxatincode}{\index{@?\texttt{@}!in macro code}}
151		% \newcommand*{\seeatincode}{see \Sref{sec:alltexcommands}}
152
153		% % index marking
	59
	60	%%%% index marking
154	61	\newcommand{\idxmark}[1]{#1\markboth{#1}{#1}}
155	62	% %%%% index sup/sub and sub \indexsupsubmain{main}{sub}
156	63	\newcommand*{\indexsupsubmain}[2]{\index{#1!#2}\index{#2}}

229	136	\newcommand*{\Icrep}[1]{\texttt{#1}\index{#1 tt?\texttt{#1}}}% % counter representation
230	137	\renewcommand*{\Icrep}[1]{\pcrep{#1}\ixcrep{#1}}% % print & index counter rep
231	138	\newcommand*{\pixcrep}[1]{\pcrep{#1}\ixcrep{#1}} % print & index counter rep
232
233		% print (and index) TeX keywords
234		%\newcommand*{\pkey}[1]{\texttt{#1}} % TeX keywords
235		% \newcommand*{\pixkey}[1]{\pkey{#1}\index{#1 key?\pkey{#1} (keyword)}%
236		% \index{keyword!#1?\pkey{#1}}}
237
238		% \newcommand*{\patexp}{@-expression} % print @-expression
239		% \newcommand*{\ixatexp}{%
240		% \index{@-expression?\patexp}} % index @-expression
241		% \newcommand*{\pixatexp}{\patexp\ixatexp} % print & index @-expression
242
243		% \newcommand*{\Pprog}[1]{\textsf{#1}} % print program name
244		% \newcommand*{\Iprog}[1]{\index{#1 prog?\Pprog{#1} (program)}%
245		% \index{program!#1?\Pprog{#1}}} % index program name
246		% \newcommand*{\Iprogsub}[2]{\index{#1 prog?\Pprog{#1} (program)!#2}}
247		% \newcommand*{\Lprog}[1]{\Pprog{#1}\Iprog{#1}} % print & index program name
248		% \DeclareRobustCommand{\Pmakeindex}{\Pprog{MakeIndex}}
249		% \DeclareRobustCommand{\Imakeindex}{\Iprog{MakeIndex}}
250		% \DeclareRobustCommand{\Lmakeindex}{\Lprog{MakeIndex}}
251		% \DeclareRobustCommand{\Pbibtex}{\Pprog{BibTeX}}
252		% \DeclareRobustCommand{\Ibibtex}{\Iprog{BibTeX}}
253		% \DeclareRobustCommand{\Lbibtex}{\Lprog{BibTeX}}
254
255		% % print and index an \if... \piif{if...}
256		% \newcommand*{\piif}[1]{\cs{#1}\index{#1?\cs{#1}}}
257
258		% % index command \!
259		% \newcommand*{\iexcl}{\index{"!?\cs{!}}}
260		% % print and index \!
261		% \newcommand*{\pixabang}{\cmdprint{\!}\index{"!?\string\cs{}\texttt{"!}}}
262		% % print and index \\!
263		% \newcommand*{\pixslashbang}{\cmdprint{\\!}\index{"\"\"!?\string\cmdprint{\\}\texttt{"!}}}
264
265		% \DeclareRobustCommand{\senv}[1]{\texttt{\bs begin\{#1\}}} % print \begin{env}
266		% \DeclareRobustCommand{\eenv}[1]{\texttt{\bs end\{#1\}}} % print \end{env}
267
268		% \newcommand*{\listofx}{`List of\ldots'}
269
270		% \newcommand*{\Note}{\textbf{NOTE:}}
271
272		% \newcommand*{\ptrue}{\texttt{true}} % print TRUE
273		% \newcommand*{\pfalse}{\texttt{false}} % print FALSE
274		% \DeclareRobustCommand{\btitle}[1]{\textit{#1}} % print a book/article/etc title
275
276
277		% %%% numbers
278		% \let\Mfrac\slashfrac
279		% \newcommand*{\ratio}[2]{{\ensuremath #1 \raise0.2ex\hbox{:} #2}}% or perhaps 0.15ex
280		% \providecommand*{\abyb}[2]{\ensuremath{#1 \times #2}} % e.g., 3 x 4
281		% \providecommand*{\abybm}[3]{\ensuremath{#1 \times #2}\:#3} % e.g., 3 x 4 cm
282		% \providecommand*{\atob}[2]{\ensuremath{#1\!:\!#2}} % e.g., 3:4
283
284
285		% \DeclareRobustCommand*{\lb}{\texttt{\char`\{}} % prints {
286		% \DeclareRobustCommand*{\rb}{\texttt{\char`\}}} % prints }
287
288		% %% A couple of shorthands
289		% \newcommand*{\tmri}{\mathrm{i}}
290		% \newcommand*{\tmrx}{\mathrm{x}}
291
292		% \newcommand*{\foredge}{fore-edge}
293		% \newlength{\pwlayi}\setlength{\pwlayi}{0.45\textwidth} %
294		% \newlength{\pwlayii}\setlength{\pwlayii}{0.45\pwlayi}
295
296		% \DeclareRobustCommand{\Vprint}[1]{\texttt{\string#1}}
297
298		% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% stuff for demoing fonts
299		% \DeclareFontFamily{T1}{bodoni}{}
300		% \DeclareFontShape{T1}{bodoni}{m}{n}{ <-> bodonirg9a }{}
301		% %% \usethisfont[encoding]{size}{baselineskip}{family}{series}{shape}
302		% \newcommand*{\usethisfont}[6][T1]{%
303		% \fontencoding{#1}\fontsize{#2}{#3}\fontfamily{#4}\fontseries{#5}%
304		% \fontshape{#6}\selectfont}
305		% \newcommand*{\termfont}[3]{%
306		% \usethisfont{25}{30}{#1}{#2}{#3}}
307		% \newcommand*{\UCalphabet}{A B C D E F G H I J K L M N O P Q R S T U V W X Y Z \&}
308		% \newcommand*{\LCalphabet}{a b c d e f g h i j k l m n o p q r s t u v w x y z
309		% 1 2 3 4 5 6 7 8 9 0 ! ? fi fl}
310		% \newcommand*{\fox}{It was a dark and stormy night.
311		% While all the good men were coming to the aid of the
312		% party, the quick brown dog had jumped over the fast red fox
313		% to its great surprise. The cattle had wound slowly
314		% o'er the lea and I was in the dark.}
315		% \newcommand*{\Kafka}{`But aren't Kafka's Schlo{\ss} and {\AE}sop's
316		% {\OE}uvres often na{\"\i}ve vis-\`a-vis the d{\ae}monic ph{\oe}nix's
317		% official r\^ole in fluffy souffl\'es?' }
318		% \newcommand*{\namesAZ}{ {\AA}ngel\aa\ Beatrice Claire
319		% Diana \'Erica Fran\c{c}oise Ginette H\'el\`ene Iris
320		% Jackie K\=aren {\L}au\.ra Mar{\'\i}a N\H{a}ta{\l}{\u\i}e {\O}ctave
321		% Pauline Qu\^eneau Roxanne Sabine
322		% %% T\~a{\'\j}a
323		% T\~aja
324		% Ur\v{s}ula Vivian Wendy Xanthippe Yv{\o}nne Z\"azilie }
325
326
327
328		% %% sans label for labelled list
329		% \newcommand*{\sflabel}[1]{\hspace\labelsep \normalfont\sffamily #1}
330		% %% italic label for labelled list
331		% \newcommand*{\itlabel}[1]{\hspace\labelsep \normalfont\itshape #1}
332
333
334		% %%%%%% stuff for new LaTeX code environment
335
336		% % \zeroseps sets list before/after skips to minimum values
337		% \newcommand*{\@zeroseps}{\setlength{\topsep}{\z@}
338		% \setlength{\partopsep}{\z@}
339		% \setlength{\parskip}{\z@}}
340		% \newlength{\gparindent} \setlength{\gparindent}{\parindent}
341		% \setlength{\gparindent}{0.5\parindent}
342		% % now we can do the new environment. This has no extra before/after spacing.
343		% \newenvironment{lcode}{\@zeroseps
344		% \renewcommand{\verbatim@startline}{\verbatim@line{\hskip\gparindent}}
345		% \small\setlength{\baselineskip}{\onelineskip}\verbatim}%
346		% {\endverbatim
347		% \vspace{-\baselineskip}%
348		% \noindent}
349
350		% %%%%% for demoing chapterstyles
351		% \newcommand*{\chaptext}[1]{The above is a demonstration of the \textit{#1}
352		% chapterstyle. It is one of several styles that come as part of the
353		% \Pclass{memoir} class.}
354
355		% %%%\renewcommand*{\theHchapter}{\thesheetsequence.\arabic{chapter}}
356
357		% \newcount\savechapcnt
358		% \newcount\demochapcnt
359		% \newcount\saveseccnt
360		% \newcount\savesubseccnt
361		% \demochapcnt=0
362		% %%\newcommand*{\theHc@demochapcnt}{\thefigure.\arabic{\c@demochapcnt}}
363		% \newcount\savefigcnt
364		% \newcount\saveftncnt
365
366
367		% %%% comma separated in-line items
368		% \let\litemize\itemize \let\endlitemize\enditemize
369		% \renewenvironment{litemize}{\renewcommand{\item}{\unskip, }}{}
370		% \newenvironment{lineitems}{\litemize\renewcommand{\item}{\unskip, }}%
371		% {\endlitemize\unskip }
372	139
373	140	%%%%%% for FontSite fonts
374	141	\newcommand*{\FSfont}[1]{%

447	214	\centering\begin{vplace}\begin{minipage}[c][\txtheight]{\txtwidth}}%
448	215	{\end{minipage}\end{vplace}\end{boxminipage}}
449	216
450		%%%%%%%%%%%%%%%%%%
451
452
453	217	%%%%%%%%% section head designs
454	218	\newcommand*{\defaultsecheads}{
455	219	\setsecheadstyle{\normalfont\Large\bfseries\raggedright}

manual/manual.synctex.gz less more

Binary diff not shown

+6

-5

manual/manual.tex less more

20	20	%%
21	21	\title{\cafeobj~User's Manual \\ --- ver.1.4.9 ---}
22	22	\author{Ataru T. Nakagawa \and Toshimi Sawada \and Kokichi Futatsugi}
23		\date{\today}
	23	%\date{\today}
	24	\date{2013/3/1}
24	25	\bibliographystyle{plain}
25	26
26	27	\maketitle

29	30	\includegraphics[scale=0.2]{cafe-logo.pdf}
30	31	\end{center}
31	32	\vfill
32		\Hline
33		\begin{center}
34		\footnotesize{Revised on 2012/3 by Kosakusha}
35		\end{center}
	33	%% \Hline
	34	%% \begin{center}
	35	%% \footnotesize{Revised on 2012/3 by Kosakusha}
	36	%% \end{center}
36	37	\thispagestyle{empty}
37	38	%% \Hline
38	39	%% %%%%

+1

-1

mksrc.sh less more

0	0	#!/bin/sh
1		VERSION=1.4.8rc4
	1	VERSION=1.4.9rc9
2	2	DISTDIR=dist/cafeobj-$VERSION
3	3	DISTFILE=cafeobj-$VERSION.tgz
4	4

+2

-2

todo/2010/aexpCompBadRed101226.cafe less more

210	210	-- may be because of a conflict of the declarations of
211	211	-- _=_ in EQL and _=_ declared in PNAT
212	212	-- and LHS of the equation declared does not match
213		open THEOREM-COMPILER
	213	open THEOREM-COMPILER .
214	214	-- assumptions
215	215	eq ((if 0 = interpret(e) then 0
216	216	else (if interpret(e) < sq(pivot(0,interpret(e)))

225	225	red th1(/ e,n) .
226	226	close
227	227	-- BUT the following works!
228		open THEOREM-COMPILER
	228	open THEOREM-COMPILER .
229	229	-- assumptions
230	230	eq ((if 0 = interpret(e) then 0
231	231	else (if interpret(e) < sq(pivot(0,interpret(e)))

+2

-2

todo/2010/bad-match.cafe less more

26	26	-- " eq[exMid]: P or not P = true ." and
27	27	-- "P:BoolBa" may
28	28	-- interact in a bad manner!
29		open BOOLba
	29	open BOOLba .
30	30	set trace on
31	31	red not P:BoolBa or false .
32	32	set trace off
33	33	close
34	34
35	35	-- (2) works properly
36		open BOOLba
	36	open BOOLba .
37	37	set trace on
38	38	red not Q:BoolBa or false .
39	39	set trace off

+2

-2

todo/2010/bad-reduction.cafe less more

80	80	singleton('a,0)))) .
81	81	}
82	82
83		open TEST
	83	open TEST .
84	84	--
85	85	red update('c,10,t) .
86	86	red insert('c,10,t) .

97	97	valOfT(someT(((< 'd , 3 >) \|
98	98	((< 'e , 10 >) \| empty))))))))))))):?TOption"
99	99
100		eof
	100	-- eof
101	101	**
102	102	close
103	103

+1

-1

todo/2010/infSearchQlock/qlock.mod less more

56	56	-- get
57	57	op get : QueueErr -> QueueErr
58	58	eq get((Q,X)) = Q .
59		eq (get(empty) = Q:Queue) = false .
	59	eq (get(empty) = Q) = false .
60	60
61	61	-- top
62	62	op top : QueueErr -> EltErr.D

+2

-2

todo/2010/infSearchQlock/verificationBySearchWithObEq-ijkl.cafe less more

2	2	-- ==========================================================
3	3
4	4	set always memo on
5		clean memo
	5	set clean memo on
6	6
7	7	-- "set clean memo on" makes litte differences
8	8	-- is it contradicts to the general rule? 110228

20	20
21	21	-- verification of non existence of counter examples
22	22	-- for 2 agents case
23		open (QLOCKijklTrans + QLOCKobEq + MEX)
	23	open (QLOCKijklTrans + QLOCKobEq + MEX) .
24	24
25	25	-- defining observational/behavioral equivalence
26	26	pred _=ob=_ : Config Config {memo} .

+2

-2

todo/2010/infSearchQlock/verificationBySearchWithObEq.mod less more

14	14
15	15	-- verification of non existence of counter examples
16	16	-- for 2 agents case
17		open (QLOCKijTrans + QLOCKobEq + MEX)
	17	open (QLOCKijTrans + QLOCKobEq + MEX) .
18	18
19	19	-- defining observational/behavioral equivalence
20	20	pred _=ob=_ : Config Config {memo} .

68	68
69	69	-- verification of non existence of counter examples
70	70	-- for 3 agents case
71		open (QLOCKijkTrans + QLOCKobEq + MEX)
	71	open (QLOCKijkTrans + QLOCKobEq + MEX) .
72	72
73	73	-- defining observational/behavioral equivalence
74	74	pred _=ob=_ : Config Config {memo} .

+11

-11

todo/2010/modexp.cafe less more

33	33	show op (_ + _)
34	34	describe op (_ + _)
35	35
36		open NAT
	36	open NAT .
37	37	show
38	38	show ops
39	39	show sorts

123	123	-- module in the module LIST(TRIV=>PNAT=) to NatList
124	124
125	125	--> testing PNAT=LIST
126		open PNAT=LIST
	126	open PNAT=LIST .
127	127	parse (s 0 \| nil) .
128	128	ops a b : -> Nat .
129	129	red (0 \| s 0 \| nil) = (0 \| s 0 \| nil) .

268	268	make NAT==LIST (LIST(TRIV=>NAT==))
269	269
270	270	--> testing the NAT==LIST
271		open NAT==LIST
	271	open NAT==LIST .
272	272	ops a b : -> Nat .
273	273	red (0 \| 1 \| nil) = (0 \| 1 \| nil) .
274	274	red (0 \| 1 \| nil) = (0 \| 2 \| nil) .

310	310	(E1:Nat >= E2:Nat))}))
311	311
312	312	--> testing the NAT<=>LIST
313		open NAT<=>LIST
	313	open NAT<=>LIST .
314	314	ops a b : -> Nat .
315	315	red (0 \| 1 \| nil) = (0 \| 1 \| nil) .
316	316	red (0 \| 1 \| nil) = (0 \| 2 \| nil) .

515	515	}
516	516
517	517	-- testing LISTord
518		open LISTord
	518	open LISTord .
519	519	parse hd nil .
520	520	parse tl nil .
521	521	ops a b : -> Elt .

549	549	}
550	550
551	551	--> testing
552		open (LIST@(PNAT))
	552	open (LIST@(PNAT)) .
553	553	ops a b : -> Nat .
554	554	red (0 \| s 0 \| nil) @ (0 \| s 0 \| nil) .
555	555	red (a \| b \| nil) @ (a \| b \| nil) .
556	556	close
557	557
558	558	--> using trace command
559		open LIST@
	559	open LIST@ .
560	560	ops a b c : -> Elt .
561	561
562	562	set trace on

591	591	--> (i.e. @ri(L:Nat) = true)
592	592	-- Proof: By induction on L1.
593	593	-- I Base case
594		open PRED-LIST@
	594	open PRED-LIST@ .
595	595	-- check
596	596	red @ri(nil) .
597	597	close
598	598	-- II Induction case
599		open PRED-LIST@
	599	open PRED-LIST@ .
600	600	-- arbitrary values
601	601	op e : -> Elt.X .
602	602	op l1 : -> List .

613	613	-- (i.e. @assoc(L1:List,L2:List,L3:List) = true)
614	614	-- Proof: By induction on L1.
615	615	-- I Base case
616		open PRED-LIST@
	616	open PRED-LIST@ .
617	617	-- arbitrary values
618	618	ops l2 l3 : -> List .
619	619	-- check
620	620	red @assoc(nil,l2,l3) .
621	621	close
622	622	-- II Induction case
623		open PRED-LIST@
	623	open PRED-LIST@ .
624	624	-- arbitrary values
625	625	op e : -> Elt.X .
626	626	op l1 : -> List .

+2

-2

todo/2010/parseErrorOnTwo=110105.cafe less more

24	24	eq s(X) * Y = Y + (X * Y) .
25	25
26	26	-- _*_ distributes on _+_
27		eq X:Nat * (Y:Nat + Z:Nat) = (X * Y) + (X * Z) .
	27	eq x:Nat * (y:Nat + z:Nat) = (x * y) + (x * z) .
28	28
29	29	}
30	30

54	54	-- instead of "open (FACT + FACT2) <CR> inc(EQL)"
55	55	-- ****************************************************
56	56	-- open (FACT + FACT2 + EQL)
57		open (FACT + FACT2)
	57	open (FACT + FACT2) .
58	58	inc(EQL)
59	59	-- eof
60	60	-- induction base M = 0

+2

-2

todo/2010/parseErrorOnTwo=110223.cafe less more

24	24	eq s(X) * Y = Y + (X * Y) .
25	25
26	26	-- _*_ distributes on _+_
27		eq X:Nat * (Y:Nat + Z:Nat) = (X * Y) + (X * Z) .
	27	eq x:Nat * (y:Nat + z:Nat) = (x * y) + (x * z) .
28	28
29	29	}
30	30

58	58	-- open (FACT + FACT2 + EQL)
59	59	-- but
60	60	-- the following two lines causes error; this is fixed at 148p23
61		open (FACT + FACT2)
	61	open (FACT + FACT2) .
62	62	inc(EQL)
63	63
64	64	--> induction base M = 0

+8

-8

todo/2010/prExIncUsTests110308.cafe less more

17	17	op f : S.M1 S.M2 -> S5
18	18	}
19	19
20		open M3
	20	open M3 .
21	21	red a.M1 .
22	22	red a.M2 .
23	23	red f(a.M1,a.M2) .

30	30	op f : S.M1 S.M2 -> S6
31	31	}
32	32
33		open M4
	33	open M4 .
34	34	red a.M1 .
35	35	red a.M2 .
36	36	red f(a.M1,a.M2) .

43	43	op f : S.M1 S.M2 -> S3
44	44	}
45	45
46		open M5
	46	open M5 .
47	47	red a.M1 .
48	48	red a.M2 .
49	49	red f(a.M1,a.M2) .

56	56	op f : S.M1 S.M2 -> S4
57	57	}
58	58
59		open M6
	59	open M6 .
60	60	--> the three commented red commands
61	61	--> make the system down to CHAOS level
62		-- red a.M1 .
63		-- red a.M2 .
64		-- red f(a.M1,a.M2) .
	62	red a.M1 .
	63	red a.M2 .
	64	red f(a.M1,a.M2) .
65	65	close
66	66
67	67	sh M6
68	68	parse in M6 : a .
69	69	sh op f
70	70	--> the following does not return the expected result
71		parse in M6 : f(a,a) .⏎
	71	parse in M6 : f(a,a) .

+2

-1

todo/2010/rename.cafe less more

3	3	op f : S -> S
4	4	}
5	5
6		open M * {op f -> _@}
	6	open M * {op f -> _@} .
	7

+12

-3

todo/2010/simp/smpi.mod less more

168	168	}
169	169	) .
170	170	}
171		select TEST .
	171
	172	set clean memo on
	173	open TEST .
172	174
173	175	--> (1) exec test
174	176
175		-- exec input .
	177	exec input .
176	178
177	179	--> (2) red _==>!_ test
178	180	--> This search should find the normal form of the above execution (1).
179	181
180		-- red input ==>! L:List .
	182	red input ==>! L:List .
181	183
	184	close
	185	set clean memo off
	186
	187	--
	188	eof
	189
	190

+1

-1

todo/2012/prtime.cafe less more

684	684
685	685	-- (ss ; drSr ; duSr ; rr ; rs ; drRs ; duRs ; sr)
686	686
687		eof
	687	-- eof
688	688
689	689	-- (0.000 sec for parse, 2717438 rewrites(205.180 sec), 64516479 matches) with cafeobj149rc6 130101
690	690	-- (1.250 sec for parse, 2854107 rewrites(401.330 sec), 79646800 matches) with cafeobj149rc9 130101

+4

-4

version.lisp less more

8	8	(eval-when (eval load compile)
9	9	(setq cafeobj-version-major "1.4")
10	10	(setq cafeobj-version-memo (format nil "~a" "PigNose0.99"))
11		(setq patch-level (format nil "~a" ""))
	11	(setq patch-level (format nil "~a" "1"))
12	12	(if (not (equal "" cafeobj-version-memo))
13	13	(if (not (equal "" patch-level))
14	14	(setq cafeobj-version-minor
15		(format nil ".9rc9(~a,~A)"
	15	(format nil ".9(~a,~A)"
16	16	cafeobj-version-memo
17	17	patch-level))
18	18	(setq cafeobj-version-minor
19		(format nil ".9rc9(~a)" cafeobj-version-memo)))
20		(setq cafeobj-version-minor ".9rc9"))
	19	(format nil ".9(~a)" cafeobj-version-memo)))
	20	(setq cafeobj-version-minor ".9"))
21	21	(setq cafeobj-version (concatenate 'string
22	22	cafeobj-version-major
23	23	cafeobj-version-minor))