Commit 6f133ad860fed4bd3135ebc514b76802198cd45c - cafeobj

1. Optimized term parser for not accumulate same forms for possible arguments. 2. Modified old examples for adapting the current syntax. tswd 11 years ago

17 changed file(s) with 272 addition(s) and 258 deletion(s). Raw diff Collapse all Expand all

-1

Makefile less more

12	12
13	13	PACKAGE = cafeobj
14	14	VERSION = 1.4
15		VMINOR = .9rc8
	15	VMINOR = .9rc9
16	16	VMEMO = PigNose0.99
17	17	PATCHLEVEL =
18	18

-1

autom4te.cache/output.0 less more

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

+19

-19

autom4te.cache/requests less more

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

+193

-193

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

216	216	(format t "~&dictionary info token = ~s" token))
217	217	(let ((res nil)
218	218	(mod-token nil))
219		(cond ((consp token)
220		;; special builtin tokens
221		(setq res (list (info-for-special-builtins token))))
222		;; normal token
223		(t (setq res (dictionary-get-token-info (dictionary-table dictionary)
	219	(block collect
	220	(cond ((consp token)
	221	;; special builtin tokens
	222	(setq res (list (info-for-special-builtins token))))
	223	;; normal token
	224	(t (setq res (dictionary-get-token-info (dictionary-table dictionary)
224	225	token))
225		;; blocked let variable?
226		;; TODO
	226	;; blocked let variable?
	227	;; TODO
227	228
228		;; bound variable?
229		(catch 'term-context-error
230		(let ((val (get-bound-value token)))
231		(when val
232		(if (is-special-let-variable? token)
233		(push val res)
	229	;; bound variable?
	230	(catch 'term-context-error
	231	(let ((val (get-bound-value token)))
	232	(when val
	233	(if (is-special-let-variable? token)
	234	(push val res)
234	235	(push (simple-copy-term-sharing-variables
235	236	val dictionary)
236	237	res)))))
237
238		;; try other possiblities.
239		;; variable ?
240		(let ((res2 (assoc (intern token) parse-variables)))
241		(cond
242		(res2
243		;; there's a registered variable with name 'token', accumlate
244		;; it. now that vars are left in modules want
245		;; parser-variables to replace.
246		(when on-parse-debug
247		(format t "~&found var : ~s" (car res2)))
248		(setq res (cons (cdr res2) (dictionary-delete-vars res)))
249		)
250		(t
251		;; check sort qualified variable reference
252		;; = on-the-fly (dynamic) variable declaration.
253		;;
254		(let ((q-pos (position #\: (the simple-string token)
255		:from-end t)))
256		(declare (type (or null fixnum) q-pos))
257		(cond ((and q-pos
258		(not (zerop (the fixnum q-pos)))
259		(not (= (the fixnum q-pos)
260		(the fixnum
261		(1- (length
262		(the simple-string token)))))))
263		(let ((sort nil)
264		(var-name nil)
265		(var nil))
266		;; assumes the token is qualified vriable
267		;; declaration.
268		(setq var-name (subseq (the simple-string token)
269		0
270		(the fixnum q-pos)))
271		;;; (setf var-name (intern var-name))
272		(setf sort (find-sort-in current-module
273		(subseq
274		(the simple-string token)
275		(1+ (the fixnum q-pos)))))
276		(unless sort
277		(with-output-chaos-error ('no-such-sort)
278		(format t "unknown sort ~a for variable form ~a."
279		(subseq token (1+ q-pos))
280		token)
281		))
282		(let ((bi (check-var-name-overloading-with-builtin
283		var-name sort current-module)))
284		(when bi
285		(with-output-chaos-warning ()
286		(format t "declaring variable ~s on the fly,"
287		var-name)
288		(print-next)
289		(princ "the name is conflicting with built-in constant of sort ")
290		(print-sort-name bi current-module)
291		(princ ".")
292		(terpri)
293		)))
294		;;
295		(let ((gv (dictionary-get-token-info
296		(dictionary-table dictionary)
297		var-name)))
298		(when gv
299		(dolist (op-v gv)
300		(when (eq (object-syntactic-type op-v)
301		'variable)
302		(with-output-chaos-error ('already-used-name)
303		(format t "~&on the fly variable name ~A is already used for static variable declaration..." var-name))))))
304		;; OK
305		(setq var-name (intern var-name))
306		;; success parsing it as a variable declaration.
307		;; checks if there alredy a variable with the same
308		;; name.
309		(when on-parse-debug
310		(format t "~&on-the-fly var decl: ~A" var-name)
311		(format t "... ~A" parse-variables))
312		(let ((old-var (assoc var-name parse-variables)))
313		(if old-var
314		(unless (sort= (variable-sort (cdr old-var))
315		sort)
316		(with-output-chaos-error ()
317		(format t "on the fly variable ~A has been declared as sort ~A, but now being redefined as sort ~A.~%"
318		(string var-name)
319		(string (sort-id
320		(variable-sort (cdr
321		old-var))))
322		(string (sort-id sort))))
323		;;(setf (cdr old-var)
324		;; (make-variable-term sort var-name))
325		)
326		(progn
327		;; check name, if it start with `, we make
328		;; pseudo variable
329		(if (eql #\` (char (the simple-string
330		(string var-name))
331		0))
332		(setf var (make-pvariable-term sort
333		var-name))
334		(setf var (make-variable-term sort
335		var-name)))
336		(push (cons var-name var) parse-variables)))
337		(if old-var
338		(progn
339		(push (cdr old-var) res)
340		#\|\|
341		(when (err-sort-p (variable-sort
342		(cdr old-var)))
343		(pushew (cdr old-var)
344		(module-error-variables
345		current-module)))
346		\|\|#
347		)
348		(progn
349		(push var res)
350		#\|\|
351		(when (err-sort-p (variable-sort var))
352		(pushnew var (module-error-variables
353		current-module)))
354		\|\|#
355		)))))
356
357		;; must not be a variable declaration.
358		;; try yet other possibilities.
359		(t (let ((pos nil))
360		;; builtin constant tokens?
361		(dolist (bi (dictionary-builtins dictionary))
362		(let ((token-pred (bsort-token-predicate bi)))
363		(when (and token-pred
364		(funcall token-pred token))
365		(push bi pos))))
366		(if pos
367		;; may be builtin constant.
368		(if (cdr pos)
369		(let ((so (module-sort-order
370		current-module)))
371		(dolist (bi pos)
372		(unless (some #'(lambda (x)
373		(sort< x bi so))
374		pos)
375		(push
376		(dictionary-make-builtin-constant
377		token bi)
378		res))))
379		(push (dictionary-make-builtin-constant
380		token
381		(car pos))
382		res))
383
384		;; no possibility for vairable nor builtin
385		;; constant.
386		(let ((ast (gethash token builtin-ast-dict)))
387		(if ast
388		;; abstract syntax tree.
389		(setf res ast))
390		(unless res
391		(multiple-value-setq (res mod-token)
392		(get-qualified-op-pattern token)))
393		;;
394		(when (and (null res)
395		(memq identifier-sort
396		(module-all-sorts
397		current-module)))
398		(let ((ident (intern token)))
399		(unless (member ident '(\|.\| \|,\|
400		\|(\| \|)\|
401		\|{\| \|}\|
402		\|[\| \|]\|))
403		(push (make-bconst-term
404		identifier-sort ident)
405		res))))))))
406		)))))
407		;; #\|\|
408		;;; final possibility
409		(unless res
410		(multiple-value-setq (res mod-token)
411		(get-qualified-op-pattern token)))
412		;; \|\|#
413		))
	238	;;----
	239	;; (when res (return-from collect nil))
	240	;;----
	241
	242	;; try other possiblities.
	243	;; variable ?
	244	(let ((res2 (assoc (intern token) parse-variables)))
	245	(cond (res2
	246	;; there's a registered variable with name 'token', accumlate
	247	;; it. now that vars are left in modules want
	248	;; parser-variables to replace.
	249	(when on-parse-debug
	250	(format t "~&found var : ~s" (car res2)))
	251	(setq res (cons (cdr res2) (dictionary-delete-vars res))))
	252	(t
	253	;; check sort qualified variable reference
	254	;; = on-the-fly (dynamic) variable declaration.
	255	;;
	256	(let ((q-pos (position #\: (the simple-string token)
	257	:from-end t)))
	258	(declare (type (or null fixnum) q-pos))
	259	(cond ((and q-pos
	260	(not (zerop (the fixnum q-pos)))
	261	(not (= (the fixnum q-pos)
	262	(the fixnum
	263	(1- (length
	264	(the simple-string token)))))))
	265	(let ((sort nil)
	266	(var-name nil)
	267	(var nil))
	268	;; assumes the token is qualified vriable
	269	;; declaration.
	270	(setq var-name (subseq (the simple-string token)
	271	0
	272	(the fixnum q-pos)))
	273	;; (setf var-name (intern var-name))
	274	(setf sort (find-sort-in current-module
	275	(subseq
	276	(the simple-string token)
	277	(1+ (the fixnum q-pos)))))
	278	(unless sort
	279	(when res (return-from collect nil))
	280	(with-output-chaos-error ('no-such-sort)
	281	(format t "unknown sort ~a for variable form ~a."
	282	(subseq token (1+ q-pos))
	283	token)))
	284	(let ((bi (check-var-name-overloading-with-builtin
	285	var-name sort current-module)))
	286	(when bi
	287	(with-output-chaos-warning ()
	288	(format t "declaring variable ~s on the fly,"
	289	var-name)
	290	(print-next)
	291	(princ "the name is conflicting with built-in constant of sort ")
	292	(print-sort-name bi current-module)
	293	(princ ".")
	294	(terpri))))
	295	;;
	296	(let ((gv (dictionary-get-token-info
	297	(dictionary-table dictionary)
	298	var-name)))
	299	(when gv
	300	(dolist (op-v gv)
	301	(when (eq (object-syntactic-type op-v)
	302	'variable)
	303	(with-output-chaos-error ('already-used-name)
	304	(format t "~&on the fly variable name ~A is already used for static variable declaration..." var-name))))))
	305	;; OK
	306	(setq var-name (intern var-name))
	307	;; success parsing it as a variable declaration.
	308	;; checks if there alredy a variable with the same
	309	;; name.
	310	(when on-parse-debug
	311	(format t "~&on-the-fly var decl: ~A" var-name)
	312	(format t "... ~A" parse-variables))
	313	(let ((old-var (assoc var-name parse-variables)))
	314	(if old-var
	315	(unless (sort= (variable-sort (cdr old-var))
	316	sort)
	317	(with-output-chaos-error ()
	318	(format t "on the fly variable ~A has been declared as sort ~A, but now being redefined as sort ~A.~%"
	319	(string var-name)
	320	(string (sort-id
	321	(variable-sort (cdr
	322	old-var))))
	323	(string (sort-id sort))))
	324	;;(setf (cdr old-var)
	325	;; (make-variable-term sort var-name))
	326	)
	327	(progn
	328	;; check name, if it start with `, we make
	329	;; pseudo variable
	330	(if (eql #\` (char (the simple-string
	331	(string var-name))
	332	0))
	333	(setf var (make-pvariable-term sort
	334	var-name))
	335	(setf var (make-variable-term sort
	336	var-name)))
	337	(push (cons var-name var) parse-variables)))
	338	(if old-var
	339	(progn
	340	(push (cdr old-var) res)
	341	#\|\|
	342	(when (err-sort-p (variable-sort
	343	(cdr old-var)))
	344	(pushew (cdr old-var)
	345	(module-error-variables
	346	current-module)))
	347	\|\|#
	348	)
	349	(progn
	350	(push var res)
	351	#\|\|
	352	(when (err-sort-p (variable-sort var))
	353	(pushnew var (module-error-variables
	354	current-module)))
	355	\|\|#
	356	)))))
	357
	358	;; must not be a variable declaration.
	359	;; try yet other possibilities.
	360	(t (let ((pos nil))
	361	;; builtin constant tokens?
	362	(dolist (bi (dictionary-builtins dictionary))
	363	(let ((token-pred (bsort-token-predicate bi)))
	364	(when (and token-pred
	365	(funcall token-pred token))
	366	(push bi pos))))
	367	(if pos
	368	;; may be builtin constant.
	369	(if (cdr pos)
	370	(let ((so (module-sort-order
	371	current-module)))
	372	(dolist (bi pos)
	373	(unless (some #'(lambda (x)
	374	(sort< x bi so))
	375	pos)
	376	(push
	377	(dictionary-make-builtin-constant
	378	token bi)
	379	res))))
	380	(push (dictionary-make-builtin-constant
	381	token
	382	(car pos))
	383	res))
	384
	385	;; no possibilities of vairable nor builtin
	386	;; constant.
	387	(let ((ast (gethash token builtin-ast-dict)))
	388	(if ast
	389	;; abstract syntax tree.
	390	(setf res ast))
	391	(unless res
	392	(multiple-value-setq (res mod-token)
	393	(get-qualified-op-pattern token)))
	394	;;
	395	(when (and (null res)
	396	(memq identifier-sort
	397	(module-all-sorts
	398	current-module)))
	399	(let ((ident (intern token)))
	400	(unless (member ident '(\|.\| \|,\|
	401	\|(\| \|)\|
	402	\|{\| \|}\|
	403	\|[\| \|]\|))
	404	(push (make-bconst-term
	405	identifier-sort ident)
	406	res))))))))
	407	)))))
	408	;; #\|\|
	409	;; final possibility
	410	(unless res
	411	(multiple-value-setq (res mod-token)
	412	(get-qualified-op-pattern token)))
	413	;; \|\|#
	414	)))
414	415	;;
415	416	(when sort-constraint
416	417	(let ((real-res nil))

1526	1527	(print-in-progress "!"))
1527	1528	(or res arg-acc-list-prime))
1528	1529	\|\|#
1529		arg-acc-list-prime
1530		))
	1530	arg-acc-list-prime))
1531	1531
1532	1532	;;; op parser-collect-one-argument :
1533	1533	;;; LIST[ ( ChaosTermList . TokenList ) ] -- not empty !

1544	1544	(type fixnum level-constraint)
1545	1545	(type sort* sort-constraint))
1546	1546	(let ((arg-acc-list-prime nil))
1547		(dolist (arg-acc arg-acc-list arg-acc-list-prime)
	1547	(dolist (arg-acc arg-acc-list (delete-duplicates arg-acc-list-prime :test #'equal))
1548	1548	(let ((token-list (cdr arg-acc)) )
1549	1549	(if (null token-list)
1550	1550	nil ;this iteration is finished

-1

configure less more

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

-1

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=.9rc8
	8	VMINOR=.9rc9
9	9	VMEMO=PigNose0.99
10	10	PATCHLEVEL=
11	11	AC_SUBST(PACKAGE)

-3

exs/sorting.mod less more

35	35
36	36	set exec normalize on
37	37
38		select SORTING-STRG(NAT)
	38	open SORTING-STRG(NAT) .
39	39	exec (4 3 5 3 1) .
40	40	-- fast execution by brute engine
41	41	set tram path brute .
42	42	-- tram exec (40 39 38 37 36 35 34 33 32 31 30 29 28 27 26 25 24 23 22 21 20 19 18 17 16 15 14 13 12 11 10 9 8 7 6 5 4 3 2 1) .
	43	close
43	44
44	45	-- functions for proving the generic termination of the sorting algorithm
45	46	mod! SORTING-STRG-PROOF {

77	78	** hypothesis
78	79	eq e' <= e = true .
79	80	** conclusion
80		red disorder(e' e s) < disorder(e e' s) .
	81	-- red disorder(e' e s) < disorder(e e' s) .
81	82	close
82	83
83	84	**> LEMMA2: disorder(e s) < disorder(e s')

92	93	eq (e >> s) = (e >> s') .
93	94	eq disorder(s) < disorder(s') = true .
94	95	** conclusion
95		red disorder(e s) < disorder(e s') .
	96	red disorder(e s) < disorder(e s') .
96	97	close
97	98
98	99	-- proof of (generic) local confluence for the sorting algorithm

-2

exs-old/2-exs.mod less more

21	21	reduce xx(3) .
22	22	**> should be 256
23	23	reduce xx(4) .
24		select 2(F <= view to FNS { op f -> dbl_ })
	24	**> does not work select 2(F <= view to FNS { op f -> dbl_ })
	25	-- select 2(F <= view to FNS { op f -> dbl_ })
	26	open 2(F <= view to FNS { op f -> dbl_ }) .
25	27	**> should be 12
26	28	reduce xx(3) .
27		select 2((2(FNS { op f -> sq_ })*{ op xx -> f }){ sort S -> Int, op f -> f })
	29	close
	30
	31	-- select 2((2(FNS { op f -> sq_ })*{ op xx -> f }){ sort S -> Int, op f -> f })
	32	open 2((2(FNS { op f -> sq_ })*{ op xx -> f }){ sort S -> Int, op f -> f }) .
28	33	**> should be 65536
29	34	reduce xx(2) .
30	35	**> should be 43046721
31	36	reduce xx(3) .
	37
	38	close
32	39	--
33	40	eof
34	41	--

-3

exs-old/bubbles.mod less more

39	39	op L1 < L2 -> L1 divides L2 and L1 =/= L2
40	40	}
41	41
42		select BUBBLES[NAT]
	42	open BUBBLES[NAT] .
43	43	reduce sorting(18 5 6 3) . **> should be: 3 5 6 18
44	44	reduce sorting(8 5 4 2) . **> should be: 2 4 5 8
45		select BUBBLES[NATD]
	45	close
	46	open BUBBLES[NATD] .
46	47	reduce sorting(18 5 6 3) . **> mightnt contain: 3 6 18
47	48	reduce sorting(8 5 4 2) . **> mightnt contain: 2 4 8
48
	49	close
49	50	--
50	51	eof
51	52	**

-5

exs-old/combinators.mod less more

1	1	** was combinators.obj(in OBJ3 distribution) translated to CafeOBJ.
2	2	--
3	3	module! COMBINATORS {
4		protecting (CHAOS) -- to import Identifier, should be used with care.
	4	-- protecting (CHAOS) -- to import Identifier, should be used with care.
5	5	signature {
6	6	[ Identifier < T ]
7	7	op __ : T T -> T {l-assoc strat: (1 2 0)}

15	15	}
16	16	}
17	17
18		select COMBINATORS
	18	open COMBINATORS .
	19	ops m n p : -> Identifier .
19	20	red S K K m == I m .
20	21	red S K S m == I m .
21	22	red S I I I m == I m .
22	23
23		red K m n == S(S(K S)(S(K K)K))(K(S K K))m n .
24		red S m n p == S(S(K S)(S(K(S(K S)))(S(K(S(K K)))S)))(K(K(S K K)))m n p .
	24	red K m n == S(S(K S)(S(K K)K))(K(S K K)) m n .
	25	--
	26	red S m n p == S(S(K S)(S(K(S(K S)))(S(K(S(K K)))S)))(K(K(S K K))) m n p .
25	27	red S(K K) m n p == S(S(K S)(S(K K)(S(K S)K)))(K K) m n p .
26
	28	--
	29	close
27	30	--
28	31	eof
29	32	**

+17

-17

exs-old/fun.mod less more

47	47	signature {
48	48	[ Stmt ]
49	49	op _;_ : Stmt Stmt -> Stmt {assoc}
50		op _:=_ : Id IntExp -> Stmt
	50	op _::=_ : Id IntExp -> Stmt
51	51	op while_do_od : BoolExp Stmt -> Stmt
52	52	op [[_]]_ : Stmt Env -> Env
53	53	}

56	56	var E : IntExp var B : BoolExp
57	57	var I : Id
58	58	-- -----------------------------------------
59		eq [[ I := E ]] V = put(I,[[ E ]] V, V) .
	59	eq [[ I ::= E ]] V = put(I,[[ E ]] V, V) .
60	60	eq [[ S ; S' ]] V = [[ S' ]] [[ S ]] V .
61	61	eq [[ while B do S od ]] V
62	62	= if [[ B ]] V then

82	82	signature {
83	83	[ Fun ]
84	84	op fun _ _ is vars _ body: _ : Id IdList InitList Stmt -> Fun
85		op [[_:=_]]_ : IdList IntList Env -> Env
	85	op [[_::=_]]_ : IdList IntList Env -> Env
86	86	op [[_]]_ : InitList Env -> Env
87	87	op [[_]][_]_ : Fun Env IntList -> Env
88	88	op [[_]]_ : Fun IntList -> Int

95	95	var S : Stmt var V : Env
96	96	-- -------------------------------------
97	97	eq [[ nil-init ]] V = V .
98		eq [[(I initially E); INs ]] V = [[ INs ]] [[ I := E ]] V .
99		eq [[ I Is := N Ns ]] V = [[ (I := N) ]] ([[ Is := Ns ]] V) .
100		eq [[(nil):IdList := (nil):IntList ]] V = V .
	98	eq [[(I initially E); INs ]] V = [[ INs ]] [[ I ::= E ]] V .
	99	eq [[ I Is ::= N Ns ]] V = [[ (I ::= N) ]] ([[ Is ::= Ns ]] V) .
	100	eq [[(nil):IdList ::= (nil):IntList ]] V = V .
101	101	eq [[ fun F(Is) is vars nil-init body: S ]][ V ](Ns) = [[ S ]] V .
102	102	eq [[ fun F(Is) is vars INs body: S ]][ V ](Ns) =
103		[[ S ]] [[ INs ]] [[ Is := Ns ]] V .
	103	[[ S ]] [[ INs ]] [[ Is ::= Ns ]] V .
104	104	eq [[ fun F(Is) is vars INs body: S ]](Ns) =
105	105	[[ fun F(Is) is vars INs body: S ]][ nilArr ](Ns) [ F ] .
106		cq [[ Is := Ns ]] V = wrong#args if \| Is \| =/= \| Ns \| . ** err-qn
	106	cq [[ Is ::= Ns ]] V = wrong#args if \| Is \| =/= \| Ns \| . ** err-qn
107	107	}
108	108	}
109	109

111	111	select FUN
112	112	**> pow(n m) finds the nth power of m for positive n or 0
113	113	reduce [[ fun 'pow('n 'm) is vars 'pow initially 1 body:
114		while 0 < 'n do ('pow := 'pow * 'm);('n := 'n - 1) od ]](4 2) .
	114	while 0 < 'n do ('pow ::= 'pow * 'm);('n ::= 'n - 1) od ]](4 2) .
115	115	-- tram reduce [[ fun 'pow('n 'm) is vars 'pow initially 1 body:
116		-- while 0 < 'n do ('pow := 'pow * 'm);('n := 'n - 1) od ]](4 2) .
	116	-- while 0 < 'n do ('pow ::= 'pow * 'm);('n ::= 'n - 1) od ]](4 2) .
117	117	reduce [[ fun 'pow('n 'm) is vars 'pow initially 1 body:
118		while 0 < 'n do ('pow := 'pow * 'm);('n := 'n - 1) od ]](4 2) .
	118	while 0 < 'n do ('pow ::= 'pow * 'm);('n ::= 'n - 1) od ]](4 2) .
119	119	**> should be: 16
120	120
121	121	**> factorial of n
122	122	reduce [[ fun 'fac('n) is vars ('fac initially 1);('i initially 0) body:
123		while 'i < 'n do ('i := 'i + 1); ('fac := 'i * 'fac) od ]](5) .
	123	while 'i < 'n do ('i ::= 'i + 1); ('fac ::= 'i * 'fac) od ]](5) .
124	124	-- tram reduce [[ fun 'fac('n) is vars ('fac initially 1);('i initially 0) body:
125		-- while 'i < 'n do ('i := 'i + 1); ('fac := 'i * 'fac) od ]](5) .
	125	-- while 'i < 'n do ('i ::= 'i + 1); ('fac ::= 'i * 'fac) od ]](5) .
126	126	**> should be: 120
127	127
128	128	**> max finds the maximum of a list of three numbers
129	129	reduce [[ fun 'max('a 'b 'c) is vars ('n initially 2);('max initially 'a) body:
130	130	while 0 < 'n do
131		('n := 'n - 1); ('x := 'b); ('b := 'c);
132		('max := if 'x < 'max then 'max else 'x endif) od ]](3 123 32) .
	131	('n ::= 'n - 1); ('x ::= 'b); ('b ::= 'c);
	132	('max ::= if 'x < 'max then 'max else 'x endif) od ]](3 123 32) .
133	133	-- tram reduce [[ fun 'max('a 'b 'c) is vars ('n initially 2);('max initially 'a) body:
134	134	-- while 0 < 'n do
135		-- ('n := 'n - 1); ('x := 'b); ('b := 'c);
136		-- ('max := if 'x < 'max then 'max else 'x endif) od ]](3 123 32) .
	135	-- ('n ::= 'n - 1); ('x ::= 'b); ('b ::= 'c);
	136	-- ('max ::= if 'x < 'max then 'max else 'x endif) od ]](3 123 32) .
137	137	**> should be: 123
138	138	--
139	139	eof

-1

exs-old/groupl.mod less more

11	11	eq [las]: A * (B * C) = (A * B) * C .
12	12	}
13	13
14		open GROUPL
	14	open GROUPL .
15	15	op a : -> Elt .
16	16
17	17	** first, prove the right inverse law:

-1

exs-old/groupla.mod less more

11	11	eq [linv]: A -1 * A = e .
12	12	}
13	13
14		open GROUPLA
	14	open GROUPLA .
15	15	op a : -> Elt .
16	16
17	17	** first, prove the right inverse law:

-3

exs-old/implang.mod less more

44	44	op inc : expr -> expr { prec: 8 }
45	45	-- statements ----------------------------------------
46	46	-- assignment
47		op (_:=_) : var expr -> assignment { prec: 20 }
	47	op (_::=_) : var expr -> assignment { prec: 20 }
48	48	-- conditional
49	49	op if : expr program program -> conditional { prec: 20 }
50	50	-- loop

76	76	-- expression
77	77	op evale : expr env -> nat
78	78
79		eq [assignment]: evalp((X:var := E:expr), C:env)
	79	eq [assignment]: evalp((X:var ::= E:expr), C:env)
80	80	= update(C,X,evale(E,C)) .
81	81	eq [if]: evalp((if(E:expr, P:program, P':program)), C:env)
82	82	= if evale(E,C) == 0 then evalp(P',C)

107	107
108	108
109	109	red in TINY-IPL :
110		evalp((v(0) := 0, while le(v(0), s(s(s(s(s(0)))))) { v(0) := inc(v(0)) }), empty) .
	110	evalp((v(0) ::= 0, while le(v(0), s(s(s(s(s(0)))))) { v(0) ::= inc(v(0)) }), empty) .
111	111
112	112	--
113	113	eof

-1

exs-old/osa.mod less more

90	90	eq pop push(N,S) = S .
91	91	}
92	92
93		open BSTACK
	93	open BSTACK .
94	94	eq length push(N,S) = 1 + length S .
95	95
96	96	red length(empty) .

-3

exs-old/sorting.mod less more

4	4	require lexl
5	5
6	6	module! SORTING(X :: POSET) {
7		protecting (LIST[X])
	7	protecting (LIST(X))
8	8	op sorting_ : List -> List
9	9	op unsorted_ : List -> Bool
10	10	vars L L' L'' : List

14	14	cq unsorted L E L' E' L'' = true if E' < E .
15	15	}
16	16
17		select SORTING[NATD]
	17	open SORTING(NATD) .
18	18	reduce sorting(18 5 6 3) . **> should contain: 3 6 18
19	19	reduce sorting(8 5 4 2) . **> should contain: 2 4 8
20	20	reduce sorting(6 3 1) . **> should be: 1 3 6
21	21	reduce sorting(18 6 5 3 1) . **> should contain: 1 3 6 18
	22	close
22	23
23		select SORTING[INT]
	24	open SORTING(INT) .
24	25	reduce unsorted 1 2 3 4 . **> should not be: true
25	26	reduce unsorted 4 1 2 3 . **> should be: true
26	27	reduce sorting 1 4 2 3 . **> should be: 1 2 3 4
	28	close
27	29
28	30	make SORTING-PH-LIST (SORTING[(LEXL[QIDL]*{op __ -> _._})
29	31	{sort Elt -> List,

-3

version.lisp less more

12	12	(if (not (equal "" cafeobj-version-memo))
13	13	(if (not (equal "" patch-level))
14	14	(setq cafeobj-version-minor
15		(format nil ".9rc8(~a,~A)"
	15	(format nil ".9rc9(~a,~A)"
16	16	cafeobj-version-memo
17	17	patch-level))
18	18	(setq cafeobj-version-minor
19		(format nil ".9rc8(~a)" cafeobj-version-memo)))
20		(setq cafeobj-version-minor ".9rc8"))
	19	(format nil ".9rc9(~a)" cafeobj-version-memo)))
	20	(setq cafeobj-version-minor ".9rc9"))
21	21	(setq cafeobj-version (concatenate 'string
22	22	cafeobj-version-major
23	23	cafeobj-version-minor))