Commit 299652d4d384ac653bf2cca8edf0fff0f06503ad - cafeobj

+5

-5

cafeobj/creader.lisp less more

85	85	'((:+ op ops) (:seq-of :opname) \|:\| :sorts -> :sort
86	86	(:if-present
87	87	\|{\| (:many-of
88		((:+ assoc comm idem associative commutative idempotent))
	88	((:+ assoc comm idem associative commutative idempotent demod))
89	89	(\|id:\| :chaos-item)
90	90	(\|identity:\| :chaos-item)
91	91	(\|idr:\| :chaos-item)

109	109	'((:+ bop bops) (:seq-of :opname) \|:\| :sorts -> :sort
110	110	(:if-present
111	111	\|{\| (:many-of
112		((:+ assoc comm idem associative commutative idempotent))
	112	((:+ assoc comm idem associative commutative idempotent demod))
113	113	(\|id:\| :chaos-item)
114	114	(\|identity:\| :chaos-item)
115	115	(\|idr:\| :chaos-item)

139	139	:sorts)
140	140	(:if-present
141	141	\|{\| (:many-of
142		((:+ assoc comm idem associative commutative idempotent))
	142	((:+ assoc comm idem associative commutative idempotent demod))
143	143	(\|id:\| :chaos-item)
144	144	(\|identity:\| :chaos-item)
145	145	(\|idr:\| :chaos-item)

169	169	:sorts)
170	170	(:if-present
171	171	\|{\| (:many-of
172		((:+ assoc comm idem associative commutative idempotent))
	172	((:+ assoc comm idem associative commutative idempotent demod))
173	173	(\|id:\| :chaos-item)
174	174	(\|identity:\| :chaos-item)
175	175	(\|idr:\| :chaos-item)

195	195	'((:+ attr attrs) (:seq-of :opname)
196	196	\|{\|
197	197	(:many-of
198		((:+ assoc comm idem associative commutative idempotent))
	198	((:+ assoc comm idem associative commutative idempotent demod))
199	199	(\|id:\| :chaos-item)
200	200	(\|identity:\| :chaos-item)
201	201	(\|idr:\| :chaos-item)

+2

-6

chaos/boot/preproc.lisp less more

151	151	(defun is-qId-token (token)
152	152	(and (stringp token)
153	153	(<= 2 (length token))
154		(eql #\' (char token 0))
155		(alpha-char-p (char token 1))))
	154	(eql #\' (char token 0))))
156	155
157	156	(defun create-qId (token)
158	157	(intern token))

175	174	(defun is-Sort-token (token)
176	175	(and (stringp token)
177	176	(<= 2 (length token))
178		(eql #\' (char token 0))
179		(alpha-char-p (char token 1))))
	177	(eql #\' (char token 0))))
180	178
181	179	(defun create-Sort-object (token)
182	180	(intern token))

194	192	(and (stringp token)
195	193	(<= 2 (length token))
196	194	(eql #\' (char token 0))
197		(alpha-char-p (char token 1))
198	195	(position #\. token :start 1)))
199	196
200	197	(defun create-constant-object (token)

213	210	(and (stringp token)
214	211	(<= 2 (length token))
215	212	(eql #\' (char token 0))
216		(alpha-char-p (char token 1))
217	213	(position #\: token :start 1)))
218	214
219	215	(defun create-variable-object (token)

+16

-16

chaos/construct/operator.lisp less more

109	109
110	110	;;; RESTRICTION: NOW IDENTITY TERM MUST BE A CONSTANT.
111	111	;;; TODO :
	112	#\|\|
112	113	(defun declare-operator-theory (operator theory &optional (module current-module))
113	114	(declare (type operator operator)
114	115	(type list theory)

119	120	(operator-theory operator)
120	121	module)))
121	122	(setf (operator-theory operator) theory) ))
122
123		(defun compute-theory-from-attr-decl (num-args theory-decl old-theory
124		&optional (module current-module))
125		(declare (type fixnum num-args)
	123	\|\|#
	124
	125	(defun compute-theory-from-attr-decl (arity theory-decl old-theory &optional (module current-module))
	126	(declare (type list arity)
126	127	(type list theory-decl)
127	128	(type (or null op-theory) old-theory)
128	129	(type module module)
129	130	(values op-theory))
130	131	(unless old-theory (setf old-theory the-empty-theory))
131		(let ((code (theory-code old-theory))
	132	(let ((num-args (length arity))
	133	(code (theory-code old-theory))
132	134	(t-code 0)
133	135	(is-iden-r nil)
134	136	(id nil))
135		(declare (type fixnum code)
	137	(declare (type fixnum num-args code)
136	138	(type (or null fixnum) t-code))
137	139	(dolist (theory-elt theory-decl)
138	140	(cond ((symbolp theory-elt)

149	151	(unless t-code
150	152	(with-output-chaos-error ('invalid-op-attribute)
151	153	(princ "invalid operator theory ")
152		(princ theory-elt)
153		))
	154	(princ theory-elt)))
154	155	(setq code (logior code t-code))
155	156	(setq id (if (consp (cadr theory-elt)) (cadr theory-elt)
156	157	(cdr theory-elt)))

162	163	;; identity
163	164	(when id
164	165	(prepare-for-parsing module)
165		(let ((trm (simple-parse module id)))
	166	(let ((trm (simple-parse module id (car (maximal-sorts arity current-sort-order)))))
166	167	(when (term-ill-defined trm)
167	168	(with-output-chaos-error ('invalid-op-attribute)
168		(format t "invalid identity term ~a" id)
169		))
170		;;
	169	(format t "invalid identity term ~a" id)))
171	170	(setq id trm)))
172	171
173	172	;; associativity

259	258	(type list attr)
260	259	(type hash-table info)
261	260	(values t))
262		(let ((theory (compute-theory-from-attr-decl
263		(length (method-arity method))
264		attr
265		(operator-theory (method-operator method info)))))
	261	(let ((theory (compute-theory-from-attr-decl (method-arity method)
	262	attr
	263	(operator-theory (method-operator method info)))))
266	264	(set-method-theory method theory info)))
267	265
268	266	(defun set-method-theory (method theory

836	834	(unless opinfo (return-from declare-operator-precedence-in-module nil))
837	835	(declare-operator-precedence (opinfo-operator opinfo) prec)))
838	836
	837	#\|\|
839	838	(defun declare-operator-theory-in-module (op-name number-of-args
840	839	theory
841	840	&optional

849	848	(let ((opinfo (find-operator-or-warn op-name number-of-args module)))
850	849	(unless opinfo (return-from declare-operator-theory-in-module nil))
851	850	(declare-operator-theory (opinfo-operator opinfo) theory)))
	851	\|\|#
852	852
853	853	(defun declare-operator-associativity-in-module (op-name number-of-args
854	854	assoc

+1

-1

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

0		;;--Mode:LISP; Package: CHAOS; Base:10; Syntax:Common-lisp --
	0	;;;--Mode:LISP; Package: CHAOS; Base:10; Syntax:Common-lisp --
1	1	;;; $Id: parse-engine.lisp,v 1.12 2010-07-20 06:59:37 sawada Exp $
2	2	(in-package :chaos)
3	3	#\|==============================================================================

+4

-4

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

611	611	(latefix (dictionary-add-info-on-token mod-dict
612	612	(cadr token-seq)
613	613	meth)
614		#\|\|
	614	;;#\|\|
615	615	(dictionary-add-info-on-token mod-dict
616	616	(token-seq-to-str token-seq)
617	617	meth)
618		\|\|#
	618	;;\|\|#
619	619	)
620	620	(juxtaposition
621		#\|\|
	621	;;#\|\|
622	622	(dictionary-add-info-on-token
623	623	mod-dict
624	624	(token-seq-to-str token-seq)
625	625	meth)
626		\|\|#
	626	;;\|\|#
627	627	(pushnew meth (module-juxtaposition module) :test #'eq))
628	628	(otherwise (break "SNARK: update-parse-information"))))
629	629	))

+20

-0

lib/lib/2tuple.cafe less more

	0	sys:mod! 2TUPLE (C1 :: TRIV, C2 :: TRIV)
	1	{
	2	signature {
	3	[ 2Tuple ]
	4	op << _ ; _ >> : Elt.C1 Elt.C2 -> 2Tuple { constr prec: 0 }
	5	op 1* _ : 2Tuple -> Elt.C1 { demod prec: 15 }
	6	op 2* _ : 2Tuple -> Elt.C2 { demod prec: 15 }
	7	}
	8	axioms {
	9	var e1 : Elt.C1
	10	var e2 : Elt.C2
	11	eq [:BDEMOD]: (1* (<< e1 ; e2 >>)) = e1 .
	12	eq [:BDEMOD]: (2* (<< e1 ; e2 >>)) = e2 .
	13	}
	14	}
	15
	16	provide 2tuple
	17	provide 2TUPLE
	18	--
	19	eof

+0

-73

~~lib/lib/3tuple.bin~~ less more

0		;CHAOS_BINS_____
1		;;;-- Mode:LISP: Package: CHAOS; Base:10: Syntax:Common-lisp --
2		;;; $Id: 3tuple.bin,v 1.2 2007-01-24 10:03:39 sawada Exp $
3		;;;
4		(in-package :chaos)
5		(defun chaos-install-3tuple ()
6		(let ((dribble-ast nil)
7		(ast-log nil)
8		(last-module nil)
9		(current-module nil)
10		(include-bool nil)
11		(include-rwl nil)
12		(regularize-signature nil))
13		(declare (special dribble-ast ast-log
14		last-module current-module
15		include-bool include-rwl
16		regularize-signature))
17		(eval-ast-if-need-no-error '(%module-decl "3TUPLE" :object :system
18		((%import :protecting "TRIV" "C1")
19		(%import :protecting "TRIV" "C2")
20		(%import :protecting "TRIV" "C3")
21		(%sort-decl (%sort-ref "3Tuple" nil)
22		nil)
23		(%op-decl
24		("<<" "_" ";" "_" ";" "_" ">>")
25		((%sort-ref "Elt" "C1")
26		(%sort-ref "Elt" "C2")
27		(%sort-ref "Elt" "C3"))
28		(%sort-ref "3Tuple" nil)
29		(%opattrs nil nil nil nil nil t nil)
30		nil)
31		(%op-decl ("1*" "_")
32		((%sort-ref "3Tuple" nil))
33		(%sort-ref "Elt" "C1")
34		(%opattrs nil nil nil nil nil nil nil t)
35		nil)
36		(%op-decl ("2*" "_")
37		((%sort-ref "3Tuple" nil))
38		(%sort-ref "Elt" "C2")
39		(%opattrs nil nil nil nil nil nil nil t)
40		nil)
41		(%op-decl ("3*" "_")
42		((%sort-ref "3Tuple" nil))
43		(%sort-ref "Elt" "C3")
44		(%opattrs nil nil nil nil nil nil nil t)
45		nil)
46		(%var-decl ("e1")
47		(%sort-ref "Elt" "C1"))
48		(%var-decl ("e2")
49		(%sort-ref "Elt" "C2"))
50		(%var-decl ("e3")
51		(%sort-ref "Elt" "C3"))
52		(%axiom-decl :equation (":BDEMOD")
53		("1*" "<<" "e1" ";" "e2" ";" "e3"
54		">>")
55		("e1") nil nil)
56		(%axiom-decl :equation (":BDEMOD")
57		("2*" "<<" "e1" ";" "e2" ";" "e3"
58		">>")
59		("e2") nil nil)
60		(%axiom-decl :equation (":BDEMOD")
61		("3*" "<<" "e1" ";" "e2" ";" "e3"
62		">>")
63		("e3") nil nil))))
64		(eval-ast-if-need-no-error '(%protect ("3TUPLE") :set))
65		(eval-ast-if-need-no-error '(%provide "3TUPLE"))
66		(eval-ast-if-need-no-error '(%provide "3tuple"))
67		))
68
69		(eval-when (:execute :load-toplevel)
70		(chaos-install-3tuple))
71
72		;;; EOF

+22

-0

lib/lib/3tuple.cafe less more

	0	sys:mod! 3TUPLE (C1 :: TRIV, C2 :: TRIV, C3 :: TRIV) {
	1	signature {
	2	[ 3Tuple ]
	3	op << _ ; _ ; _ >> : Elt.C1 Elt.C2 Elt.C3 -> 3Tuple { constr prec: 0 }
	4	op 1* _ : 3Tuple -> Elt.C1 { demod prec: 15 }
	5	op 2* _ : 3Tuple -> Elt.C2 { demod prec: 15 }
	6	op 3* _ : 3Tuple -> Elt.C3 { demod prec: 15 }
	7	}
	8	axioms {
	9	var e1 : Elt.C1
	10	var e2 : Elt.C2
	11	var e3 : Elt.C3
	12	eq [:BDEMOD]: (1* (<< e1 ; e2 ; e3 >>)) = e1 .
	13	eq [:BDEMOD]: (2* (<< e1 ; e2 ; e3 >>)) = e2 .
	14	eq [:BDEMOD]: (3* (<< e1 ; e2 ; e3 >>)) = e3 .
	15	}
	16	}
	17
	18	provide 3tuple
	19	provide 3TUPLE
	20	--
	21	eof

+0

-87

~~lib/lib/4tuple.bin~~ less more

0		;CHAOS_BINS_____
1		;;;-- Mode:LISP: Package: CHAOS; Base:10: Syntax:Common-lisp --
2		;;; $Id: 4tuple.bin,v 1.2 2007-01-24 10:03:39 sawada Exp $
3		;;;
4		(in-package :chaos)
5		(defun chaos-install-4tuple ()
6		(let ((dribble-ast nil)
7		(ast-log nil)
8		(last-module nil)
9		(current-module nil)
10		(include-bool nil)
11		(include-rwl nil)
12		(regularize-signature nil))
13		(declare (special dribble-ast ast-log
14		last-module current-module
15		include-bool include-rwl
16		regularize-signature))
17		(eval-ast-if-need-no-error '(%module-decl "4TUPLE" :object :system
18		((%import :protecting "TRIV" "C1")
19		(%import :protecting "TRIV" "C2")
20		(%import :protecting "TRIV" "C3")
21		(%import :protecting "TRIV" "C4")
22		(%sort-decl (%sort-ref "4Tuple" nil)
23		nil)
24		(%op-decl
25		("<<" "_" ";" "_" ";" "_" ";" "_"
26		">>")
27		((%sort-ref "Elt" "C1")
28		(%sort-ref "Elt" "C2")
29		(%sort-ref "Elt" "C3")
30		(%sort-ref "Elt" "C4"))
31		(%sort-ref "4Tuple" nil)
32		(%opattrs nil nil nil nil nil t nil)
33		nil)
34		(%op-decl ("1*" "_")
35		((%sort-ref "4Tuple" nil))
36		(%sort-ref "Elt" "C1")
37		(%opattrs nil nil nil nil nil nil nil t)
38		nil)
39		(%op-decl ("2*" "_")
40		((%sort-ref "4Tuple" nil))
41		(%sort-ref "Elt" "C2")
42		(%opattrs nil nil nil nil nil nil nil t)
43		nil)
44		(%op-decl ("3*" "_")
45		((%sort-ref "4Tuple" nil))
46		(%sort-ref "Elt" "C3")
47		(%opattrs nil nil nil nil nil nil nil t)
48		nil)
49		(%op-decl ("4*" "_")
50		((%sort-ref "4Tuple" nil))
51		(%sort-ref "Elt" "C4")
52		(%opattrs nil nil nil nil nil nil nil t)
53		nil)
54		(%var-decl ("e1")
55		(%sort-ref "Elt" "C1"))
56		(%var-decl ("e2")
57		(%sort-ref "Elt" "C2"))
58		(%var-decl ("e3")
59		(%sort-ref "Elt" "C3"))
60		(%var-decl ("e4")
61		(%sort-ref "Elt" "C4"))
62		(%axiom-decl :equation (":BDEMOD")
63		("1*" "<<" "e1" ";" "e2" ";" "e3"
64		";" "e4" ">>")
65		("e1") nil nil)
66		(%axiom-decl :equation (":BDEMOD")
67		("2*" "<<" "e1" ";" "e2" ";" "e3"
68		";" "e4" ">>")
69		("e2") nil nil)
70		(%axiom-decl :equation (":BDEMOD")
71		("3*" "<<" "e1" ";" "e2" ";" "e3"
72		";" "e4" ">>")
73		("e3") nil nil)
74		(%axiom-decl :equation (":BDEMOD")
75		("4*" "<<" "e1" ";" "e2" ";" "e3"
76		";" "e4" ">>")
77		("e4") nil nil))))
78		(eval-ast-if-need-no-error '(%protect ("4TUPLE") :set))
79		(eval-ast-if-need-no-error '(%provide "4TUPLE"))
80		(eval-ast-if-need-no-error '(%provide "4tuple"))
81		))
82
83		(eval-when (:execute :load-toplevel)
84		(chaos-install-4tuple))
85
86		;;; EOF

+26

-0

lib/lib/4tuple.cafe less more

	0	sys:mod! 4TUPLE (C1 :: TRIV, C2 :: TRIV, C3 :: TRIV, C4 :: TRIV)
	1	{
	2	signature {
	3	[ 4Tuple ]
	4	op << _ ; _ ; _ ; _ >> : Elt.C1 Elt.C2 Elt.C3 Elt.C4 -> 4Tuple { constr prec: 0 }
	5	op 1* _ : 4Tuple -> Elt.C1 { demod prec: 15 }
	6	op 2* _ : 4Tuple -> Elt.C2 { demod prec: 15 }
	7	op 3* _ : 4Tuple -> Elt.C3 { demod prec: 15 }
	8	op 4* _ : 4Tuple -> Elt.C4 { demod prec: 15 }
	9	}
	10	axioms {
	11	var e1 : Elt.C1
	12	var e2 : Elt.C2
	13	var e3 : Elt.C3
	14	var e4 : Elt.C4
	15	eq [:BDEMOD]: (1* (<< e1 ; e2 ; e3 ; e4 >>)) = e1 .
	16	eq [:BDEMOD]: (2* (<< e1 ; e2 ; e3 ; e4 >>)) = e2 .
	17	eq [:BDEMOD]: (3* (<< e1 ; e2 ; e3 ; e4 >>)) = e3 .
	18	eq [:BDEMOD]: (4* (<< e1 ; e2 ; e3 ; e4 >>)) = e4 .
	19	}
	20	}
	21
	22	provide 4tuple
	23	provide 4TUPLE
	24	--
	25	eof

+0

-172

~~lib/lib/character.bin~~ less more

0		;CHAOS_BINS_____
1		;;;-- Mode:LISP: Package: CHAOS; Base:10: Syntax:Common-lisp --
2		;;; $Id: character.bin,v 1.2 2007-01-24 10:03:39 sawada Exp $
3		;;;
4		(in-package :chaos)
5		(defun chaos-install-character ()
6		(let ((dribble-ast nil)
7		(ast-log nil)
8		(last-module nil)
9		(current-module nil)
10		(include-bool nil)
11		(include-rwl nil)
12		(regularize-signature nil))
13		(declare (special dribble-ast ast-log
14		last-module current-module
15		include-bool include-rwl
16		regularize-signature))
17		(eval-ast-if-need '(%module-decl "CHARACTER" :object :system
18		((%import :protecting "BOOL" nil)
19		(%import :protecting "NAT" nil)
20		(%import :protecting "CHAR-VALUE" nil)
21		(%psort-decl (%sort-ref "Character" nil))
22		(%op-decl ("char-code")
23		((%sort-ref "Character" nil))
24		(%sort-ref "Nat" nil)
25		(%opattrs nil nil nil nil nil nil nil t)
26		nil)
27		(%op-decl ("code-char") ((%sort-ref "Nat" nil))
28		(%sort-ref "Character" nil)
29		(%opattrs nil nil nil nil nil nil nil t)
30		nil)
31		(%op-decl ("upcase")
32		((%sort-ref "Character" nil))
33		(%sort-ref "Character" nil)
34		(%opattrs nil nil nil nil nil nil nil t)
35		nil)
36		(%op-decl ("downcase")
37		((%sort-ref "Character" nil))
38		(%sort-ref "Character" nil)
39		(%opattrs nil nil nil nil nil nil nil t)
40		nil)
41		(%op-decl ("graphic-char-p")
42		((%sort-ref "Character" nil))
43		(%sort-ref "Bool" nil)
44		(%opattrs nil nil nil nil nil nil nil t)
45		nil)
46		(%op-decl ("alpha-char-p")
47		((%sort-ref "Character" nil))
48		(%sort-ref "Bool" nil)
49		(%opattrs nil nil nil nil nil nil nil t)
50		nil)
51		(%op-decl ("upper-case-p")
52		((%sort-ref "Character" nil))
53		(%sort-ref "Bool" nil)
54		(%opattrs nil nil nil nil nil nil nil t)
55		nil)
56		(%op-decl ("lower-case-p")
57		((%sort-ref "Character" nil))
58		(%sort-ref "Bool" nil)
59		(%opattrs nil nil nil nil nil nil nil t)
60		nil)
61		(%op-decl ("both-case-p")
62		((%sort-ref "Character" nil))
63		(%sort-ref "Bool" nil)
64		(%opattrs nil nil nil nil nil nil nil t)
65		nil)
66		(%op-decl ("digit-char-p")
67		((%sort-ref "Character" nil))
68		(%sort-ref "Bool" nil)
69		(%opattrs nil nil nil nil nil nil nil t)
70		nil)
71		(%op-decl ("alphanumericp")
72		((%sort-ref "Character" nil))
73		(%sort-ref "Bool" nil)
74		(%opattrs nil nil nil nil nil nil nil t)
75		nil)
76		(%op-decl ("char<")
77		((%sort-ref "Character" nil)
78		(%sort-ref "Character" nil))
79		(%sort-ref "Bool" nil)
80		(%opattrs nil nil nil nil nil nil nil t)
81		nil)
82		(%op-decl ("char>")
83		((%sort-ref "Character" nil)
84		(%sort-ref "Character" nil))
85		(%sort-ref "Bool" nil)
86		(%opattrs nil nil nil nil nil nil nil t)
87		nil)
88		(%op-decl ("char<=")
89		((%sort-ref "Character" nil)
90		(%sort-ref "Character" nil))
91		(%sort-ref "Bool" nil)
92		(%opattrs nil nil nil nil nil nil nil t)
93		nil)
94		(%op-decl ("char>=")
95		((%sort-ref "Character" nil)
96		(%sort-ref "Character" nil))
97		(%sort-ref "Bool" nil)
98		(%opattrs nil nil nil nil nil nil nil t)
99		nil)
100		(%op-decl ("char=")
101		((%sort-ref "Character" nil)
102		(%sort-ref "Character" nil))
103		(%sort-ref "Bool" nil)
104		(%opattrs nil nil nil nil nil nil nil t)
105		nil)
106		(%var-decl ("C" "C2")
107		(%sort-ref "Character" nil))
108		(%var-decl ("N") (%sort-ref "Nat" nil))
109		(%axiom-decl :equation (":BDEMOD")
110		("char-code" "(" "C" ")")
111		((%slisp (char-code c))) nil nil)
112		(%axiom-decl :equation nil
113		("code-char" "(" "N" ")")
114		((%slisp (code-char n))) ("N" "<=" "255") nil)
115		(%axiom-decl :equation (":BDEMOD")
116		("upcase" "(" "C" ")")
117		((%slisp (char-upcase c))) nil nil)
118		(%axiom-decl :equation (":BDEMOD")
119		("downcase" "(" "C" ")")
120		((%slisp (char-downcase c))) nil nil)
121		(%axiom-decl :equation (":BDEMOD")
122		("graphic-char-p" "(" "C" ")")
123		((%slisp (graphic-char-p c))) nil nil)
124		(%axiom-decl :equation (":BDEMOD")
125		("alpha-char-p" "(" "C" ")")
126		((%slisp (alpha-char-p c))) nil nil)
127		(%axiom-decl :equation (":BDEMOD")
128		("upper-case-p" "(" "C" ")")
129		((%slisp (upper-case-p c))) nil nil)
130		(%axiom-decl :equation (":BDEMOD")
131		("lower-case-p" "(" "C" ")")
132		((%slisp (lower-case-p c))) nil nil)
133		(%axiom-decl :equation (":BDEMOD")
134		("both-case-p" "(" "C" ")")
135		((%slisp (both-case-p c))) nil nil)
136		(%axiom-decl :equation (":BDEMOD")
137		("digit-char-p" "(" "C" ")")
138		((%slisp (digit-char-p c))) nil nil)
139		(%axiom-decl :equation (":BDEMOD")
140		("alphanumericp" "(" "C" ")")
141		((%slisp (alphanumericp c))) nil nil)
142		(%axiom-decl :equation (":BDEMOD")
143		("char=" "(" "C" "," "C2" ")")
144		((%slisp (char= c c2))) nil nil)
145		(%axiom-decl :equation (":BDEMOD")
146		("char<" "(" "C" "," "C2" ")")
147		((%slisp (char< c c2))) nil nil)
148		(%axiom-decl :equation (":BDEMOD")
149		("char>" "(" "C" "," "C2" ")")
150		((%slisp (char> c c2))) nil nil)
151		(%axiom-decl :equation (":BDEMOD")
152		("char<=" "(" "C" "," "C2" ")")
153		((%slisp (char<= c c2))) nil nil)
154		(%axiom-decl :equation (":BDEMOD")
155		("char>=" "(" "C" "," "C2" ")")
156		((%slisp (char>= c c2))) nil nil))))
157		(eval-ast-if-need '(%protect ("CHARACTER") :set))
158		(eval-ast-if-need '(%provide "CHARACTER"))
159		(eval-ast-if-need '(%provide "character"))
160		))
161
162		(defun chaos-character-tram-interface ()
163		(setq z-char (get-z-module-or-panic "CHARACTER"))
164		(push z-char tram-builtin-modules)
165		)
166
167		(eval-when (:execute :load-toplevel)
168		(chaos-install-character)
169		(chaos-character-tram-interface))
170
171		;;; EOF

+63

-0

lib/lib/character.cafe less more

	0	sys:mod! CHARACTER
	1	principal-sort Character
	2	{
	3	imports {
	4	protecting (BOOL)
	5	protecting (NAT)
	6	protecting (CHAR-VALUE)
	7	}
	8	signature {
	9	op char-code : Character -> Nat { demod prec: 0 }
	10	op code-char : Nat -> Character { demod prec: 0 }
	11	op upcase : Character -> Character { demod prec: 0 }
	12	op downcase : Character -> Character { demod prec: 0 }
	13	pred graphic-char-p : Character { demod prec: 0 }
	14	pred alpha-char-p : Character { demod prec: 0 }
	15	pred upper-case-p : Character { demod prec: 0 }
	16	pred lower-case-p : Character { demod prec: 0 }
	17	pred both-case-p : Character { demod prec: 0 }
	18	pred digit-char-p : Character { demod prec: 0 }
	19	pred alphanumericp : Character { demod prec: 0 }
	20	pred char< : Character Character { demod prec: 0 }
	21	pred char> : Character Character { demod prec: 0 }
	22	pred char<= : Character Character { demod prec: 0 }
	23	pred char>= : Character Character { demod prec: 0 }
	24	pred char= : Character Character { demod prec: 0 }
	25	}
	26	axioms {
	27	var C : Character
	28	var C2 : Character
	29	var N : Nat
	30	eq [:BDEMOD]: char-code(C) = #! (char-code c) .
	31	ceq code-char(N) = #! (code-char n) if (N <= 255) .
	32	eq [:BDEMOD]: upcase(C) = #! (char-upcase c) .
	33	eq [:BDEMOD]: downcase(C) = #! (char-downcase c) .
	34	eq [:BDEMOD]: graphic-char-p(C) = #! (graphic-char-p c) .
	35	eq [:BDEMOD]: alpha-char-p(C) = #! (alpha-char-p c) .
	36	eq [:BDEMOD]: upper-case-p(C) = #! (upper-case-p c) .
	37	eq [:BDEMOD]: lower-case-p(C) = #! (lower-case-p c) .
	38	eq [:BDEMOD]: both-case-p(C) = #! (both-case-p c) .
	39	eq [:BDEMOD]: digit-char-p(C) = #! (digit-char-p c) .
	40	eq [:BDEMOD]: alphanumericp(C) = #! (alphanumericp c) .
	41	eq [:BDEMOD]: char=(C,C2) = #! (char= c c2) .
	42	eq [:BDEMOD]: char<(C,C2) = #! (char< c c2) .
	43	eq [:BDEMOD]: char>(C,C2) = #! (char> c c2) .
	44	eq [:BDEMOD]: char<=(C,C2) = #! (char<= c c2) .
	45	eq [:BDEMOD]: char>=(C,C2) = #! (char>= c c2) .
	46	}
	47	}
	48
	49	lispq
	50	(defun chaos-character-tram-interface ()
	51	(setq z-char (get-z-module-or-panic "CHARACTER"))
	52	(push z-char tram-builtin-modules))
	53
	54	lispq
	55	(eval-when (:execute :load-toplevel)
	56	(chaos-character-tram-interface))
	57
	58	provide character
	59	provide CHARACTER
	60	--
	61	eof
	62

+0

-191

~~lib/lib/float.bin~~ less more

0		;CHAOS_BINS_____
1		;;;-- Mode:LISP: Package: CHAOS; Base:10: Syntax:Common-lisp --
2		;;; $Id: float.bin,v 1.2 2007-01-24 10:03:39 sawada Exp $
3		;;;
4		(in-package :chaos)
5		(defun chaos-install-float ()
6		(let ((dribble-ast nil)
7		(ast-log nil)
8		(last-module nil)
9		(current-module nil)
10		(include-bool nil)
11		(include-rwl nil)
12		(regularize-signature nil))
13		(declare (special dribble-ast ast-log
14		last-module current-module
15		include-bool include-rwl
16		regularize-signature))
17		(eval-ast-if-need '(%module-decl "FLOAT" :object :system
18		((%import :protecting "FLOAT-VALUE" nil)
19		(%import :protecting "BOOL" nil)
20		(%psort-decl (%sort-ref "Float" nil))
21		(%op-decl ("_" "+" "_")
22		((%sort-ref "Float" nil)
23		(%sort-ref "Float" nil))
24		(%sort-ref "Float" nil)
25		(%opattrs nil nil nil nil nil nil nil t)
26		nil)
27		(%opattr-decl (%opref ("_" "+" "_") nil 2)
28		(%opattrs (:assoc :comm) nil 33 nil nil
29		nil nil t))
30		(%op-decl ("_" "-" "_")
31		((%sort-ref "Float" nil)
32		(%sort-ref "Float" nil))
33		(%sort-ref "Float" nil)
34		(%opattrs nil nil nil nil nil nil nil t)
35		nil)
36		(%opattr-decl (%opref ("_" "-" "_") nil 2)
37		(%opattrs nil :r-assoc 33 nil nil nil nil t))
38		(%op-decl ("_" "*" "_")
39		((%sort-ref "Float" nil)
40		(%sort-ref "Float" nil))
41		(%sort-ref "Float" nil)
42		(%opattrs nil nil nil nil nil nil nil t)
43		nil)
44		(%opattr-decl (%opref ("_" "*" "_") nil 2)
45		(%opattrs (:assoc :comm) nil 31 nil nil
46		nil nil t))
47		(%op-decl ("_" "/" "_")
48		((%sort-ref "Float" nil)
49		(%sort-ref "Float" nil))
50		(%sort-ref "Float" nil)
51		(%opattrs nil nil nil nil nil nil nil t)
52		nil)
53		(%opattr-decl (%opref ("_" "/" "_") nil 2)
54		(%opattrs nil :l-assoc 31 nil nil nil nil t))
55		(%op-decl ("_" "rem" "_")
56		((%sort-ref "Float" nil)
57		(%sort-ref "Float" nil))
58		(%sort-ref "Float" nil)
59		(%opattrs nil nil nil nil nil nil nil t)
60		nil)
61		(%opattr-decl (%opref ("_" "rem" "_") nil 2)
62		(%opattrs nil :l-assoc 31 nil nil nil nil t))
63		(%op-decl ("exp") ((%sort-ref "Float" nil))
64		(%sort-ref "Float" nil)
65		(%opattrs nil nil nil nil nil nil nil t)
66		nil)
67		(%op-decl ("log") ((%sort-ref "Float" nil))
68		(%sort-ref "Float" nil)
69		(%opattrs nil nil nil nil nil nil nil t)
70		nil)
71		(%op-decl ("sqrt") ((%sort-ref "Float" nil))
72		(%sort-ref "Float" nil)
73		(%opattrs nil nil nil nil nil nil nil t)
74		nil)
75		(%op-decl ("abs") ((%sort-ref "Float" nil))
76		(%sort-ref "Float" nil)
77		(%opattrs nil nil nil nil nil nil nil t)
78		nil)
79		(%op-decl ("sin") ((%sort-ref "Float" nil))
80		(%sort-ref "Float" nil)
81		(%opattrs nil nil nil nil nil nil nil t)
82		nil)
83		(%op-decl ("cos") ((%sort-ref "Float" nil))
84		(%sort-ref "Float" nil)
85		(%opattrs nil nil nil nil nil nil nil t)
86		nil)
87		(%op-decl ("atan") ((%sort-ref "Float" nil))
88		(%sort-ref "Float" nil)
89		(%opattrs nil nil nil nil nil nil nil t)
90		nil)
91		(%op-decl ("pi") nil (%sort-ref "Float" nil)
92		(%opattrs nil nil nil nil nil nil nil t)
93		nil)
94		(%op-decl ("_" "<" "_")
95		((%sort-ref "Float" nil)
96		(%sort-ref "Float" nil))
97		(%sort-ref "Bool" nil)
98		(%opattrs nil nil nil nil nil nil nil t)
99		nil)
100		(%opattr-decl (%opref ("_" "<" "_") nil 2)
101		(%opattrs nil nil 51 nil nil nil nil t))
102		(%op-decl ("_" "<=" "_")
103		((%sort-ref "Float" nil)
104		(%sort-ref "Float" nil))
105		(%sort-ref "Bool" nil)
106		(%opattrs nil nil nil nil nil nil nil t)
107		nil)
108		(%opattr-decl (%opref ("_" "<=" "_") nil 2)
109		(%opattrs nil nil 51 nil nil nil nil t))
110		(%op-decl ("_" ">" "_")
111		((%sort-ref "Float" nil)
112		(%sort-ref "Float" nil))
113		(%sort-ref "Bool" nil)
114		(%opattrs nil nil nil nil nil nil nil t)
115		nil)
116		(%opattr-decl (%opref ("_" ">" "_") nil 2)
117		(%opattrs nil nil 51 nil nil nil nil t))
118		(%op-decl ("_" ">=" "_")
119		((%sort-ref "Float" nil)
120		(%sort-ref "Float" nil))
121		(%sort-ref "Bool" nil)
122		(%opattrs nil nil nil nil nil nil nil t)
123		nil)
124		(%opattr-decl (%opref ("_" ">=" "_") nil 2)
125		(%opattrs nil nil 51 nil nil nil nil t))
126		(%op-decl ("_" "=" "[" "_" "]" "_")
127		((%sort-ref "Float" nil)
128		(%sort-ref "Float" nil)
129		(%sort-ref "Float" nil))
130		(%sort-ref "Bool" nil)
131		(%opattrs nil nil nil nil nil nil nil t)
132		nil)
133		(%opattr-decl
134		(%opref ("_" "=" "[" "_" "]" "_") nil 3)
135		(%opattrs nil nil 51 nil nil nil nil t))
136		(%var-decl ("X" "Y" "Z")
137		(%sort-ref "Float" nil))
138		(%axiom-decl :equation (":BDEMOD") ("X" "+" "Y")
139		((%slisp (+ x y))) nil nil)
140		(%axiom-decl :equation (":BDEMOD") ("X" "-" "Y")
141		((%slisp (- x y))) nil nil)
142		(%axiom-decl :equation (":BDEMOD") ("X" "*" "Y")
143		((%slisp (* x y))) nil nil)
144		(%axiom-decl :equation (":BDEMOD") ("X" "/" "Y")
145		((%slisp (/ x y))) nil nil)
146		(%axiom-decl :equation (":BDEMOD") ("X" "rem" "Y")
147		((%slisp (rem x y))) nil nil)
148		(%axiom-decl :equation (":BDEMOD") ("exp" "(" "X" ")")
149		((%slisp (exp x))) nil nil)
150		(%axiom-decl :equation (":BDEMOD") ("log" "(" "X" ")")
151		((%slisp (log x))) nil nil)
152		(%axiom-decl :equation (":BDEMOD") ("sqrt" "(" "X" ")")
153		((%slisp (sqrt x))) nil nil)
154		(%axiom-decl :equation (":BDEMOD") ("abs" "(" "X" ")")
155		((%slisp (abs x))) nil nil)
156		(%axiom-decl :equation (":BDEMOD") ("sin" "(" "X" ")")
157		((%slisp (sin x))) nil nil)
158		(%axiom-decl :equation (":BDEMOD") ("cos" "(" "X" ")")
159		((%slisp (cos x))) nil nil)
160		(%axiom-decl :equation (":BDEMOD") ("atan" "(" "X" ")")
161		((%slisp (atan x))) nil nil)
162		(%axiom-decl :equation (":BDEMOD") ("pi") ((%slisp pi))
163		nil nil)
164		(%axiom-decl :equation (":BDEMOD") ("X" "<" "Y")
165		((%slisp (< x y))) nil nil)
166		(%axiom-decl :equation (":BDEMOD") ("X" "<=" "Y")
167		((%slisp (<= x y))) nil nil)
168		(%axiom-decl :equation (":BDEMOD") ("X" ">" "Y")
169		((%slisp (> x y))) nil nil)
170		(%axiom-decl :equation (":BDEMOD") ("X" ">=" "Y")
171		((%slisp (>= x y))) nil nil)
172		(%axiom-decl :equation (":BDEMOD")
173		("(" "X" "=" "[" "Z" "]" "Y" ")")
174		((%slisp (< (abs (- x y)) z))) nil nil))))
175		(eval-ast-if-need '(%protect ("FLOAT") :set))
176		(eval-ast-if-need '(%provide "FLOAT"))
177		(eval-ast-if-need '(%provide "float"))
178		))
179
180		(defun chaos-float-tram-interface ()
181		(setq z-float (get-z-module-or-panic "FLOAT"))
182		(push z-float tram-builtin-modules)
183		)
184
185		(eval-when (:execute :load-toplevel)
186		(chaos-install-float)
187		(chaos-float-tram-interface)
188		)
189
190		;;; EOF

+65

-0

lib/lib/float.cafe less more

	0	sys:mod! FLOAT
	1	principal-sort Float
	2	{
	3	imports {
	4	protecting (FLOAT-VALUE)
	5	protecting (BOOL)
	6	}
	7	signature {
	8	op _ + _ : Float Float -> Float { assoc comm demod prec: 33 r-assoc }
	9	op _ - _ : Float Float -> Float { demod prec: 33 r-assoc }
	10	op _ * _ : Float Float -> Float { assoc comm demod prec: 31 r-assoc }
	11	op _ / _ : Float Float -> Float { demod prec: 31 l-assoc }
	12	op _ rem _ : Float Float -> Float { demod prec: 31 l-assoc }
	13	op exp : Float -> Float { demod prec: 0 }
	14	op log : Float -> Float { demod prec: 0 }
	15	op sqrt : Float -> Float { demod prec: 0 }
	16	op abs : Float -> Float { demod prec: 0 }
	17	op sin : Float -> Float { demod prec: 0 }
	18	op cos : Float -> Float { demod prec: 0 }
	19	op atan : Float -> Float { demod prec: 0 }
	20	op pi : -> Float { demod prec: 0 }
	21	pred _ < _ : Float Float { demod prec: 51 }
	22	pred _ <= _ : Float Float { demod prec: 51 }
	23	pred _ > _ : Float Float { demod prec: 51 }
	24	pred _ >= _ : Float Float { demod prec: 51 }
	25	pred _ = [ _ ] _ : Float Float Float { demod prec: 51 }
	26	}
	27	axioms {
	28	var X : Float
	29	var Y : Float
	30	var Z : Float
	31	eq [:BDEMOD]: (X + Y) = #! (+ x y) .
	32	eq [:BDEMOD]: (X - Y) = #! (- x y) .
	33	eq [:BDEMOD]: (X * Y) = #! (* x y) .
	34	eq [:BDEMOD]: (X / Y) = #! (/ x y) .
	35	eq [:BDEMOD]: (X rem Y) = #! (rem x y) .
	36	eq [:BDEMOD]: exp(X) = #! (exp x) .
	37	eq [:BDEMOD]: log(X) = #! (log x) .
	38	eq [:BDEMOD]: sqrt(X) = #! (sqrt x) .
	39	eq [:BDEMOD]: abs(X) = #! (abs x) .
	40	eq [:BDEMOD]: sin(X) = #! (sin x) .
	41	eq [:BDEMOD]: cos(X) = #! (cos x) .
	42	eq [:BDEMOD]: atan(X) = #! (atan x) .
	43	eq [:BDEMOD]: pi = #! pi .
	44	eq [:BDEMOD]: (X < Y) = #! (< x y) .
	45	eq [:BDEMOD]: (X <= Y) = #! (<= x y) .
	46	eq [:BDEMOD]: (X > Y) = #! (> x y) .
	47	eq [:BDEMOD]: (X >= Y) = #! (>= x y) .
	48	eq [:BDEMOD]: (X = [ Z ] Y) = #! (< (abs (- x y)) z) .
	49	}
	50	}
	51
	52	lispq
	53	(defun chaos-float-tram-interface ()
	54	(setq z-float (get-z-module-or-panic "FLOAT"))
	55	(push z-float tram-builtin-modules))
	56
	57	(eval-when (:execute :load-toplevel)
	58	(chaos-float-tram-interface))
	59
	60	provide float
	61	provide FLOAT
	62	--
	63	eof
	64

+0

-136

~~lib/lib/int.bin~~ less more

0		;CHAOS_BINS_____
1		;;;-- Mode:LISP: Package: CHAOS; Base:10: Syntax:Common-lisp --
2		;;; $Id: int.bin,v 1.2 2007-01-24 10:03:39 sawada Exp $
3		;;;
4		(in-package :chaos)
5		(defun chaos-install-int ()
6		(let ((dribble-ast nil)
7		(ast-log nil)
8		(last-module nil)
9		(current-module nil)
10		(include-bool nil)
11		(include-rwl nil)
12		(regularize-signature nil))
13		(declare (special dribble-ast ast-log
14		last-module current-module
15		include-bool include-rwl
16		regularize-signature))
17		(eval-ast-if-need '(%module-decl "INT" :object :system
18		((%import :protecting "NAT" nil)
19		(%import :protecting "INT-VALUE" nil)
20		(%psort-decl (%sort-ref "Int" nil))
21		(%op-decl ("_" "+" "_")
22		((%sort-ref "Int" nil)
23		(%sort-ref "Int" nil))
24		(%sort-ref "Int" nil)
25		(%opattrs ((:idr "0")) nil nil nil nil nil nil t)
26		nil)
27		(%op-decl ("_" "-" "_")
28		((%sort-ref "Int" nil)
29		(%sort-ref "Int" nil))
30		(%sort-ref "Int" nil)
31		(%opattrs nil nil nil nil nil nil nil t)
32		nil)
33		(%opattr-decl (%opref ("_" "-" "_") nil 2)
34		(%opattrs nil :r-assoc 33 nil nil nil nil t))
35		(%op-decl ("_" "*" "_")
36		((%sort-ref "Int" nil)
37		(%sort-ref "Int" nil))
38		(%sort-ref "Int" nil)
39		(%opattrs nil nil nil nil nil nil nil t)
40		nil)
41		(%op-decl ("_" "quo" "_")
42		((%sort-ref "Int" nil)
43		(%sort-ref "NzInt" nil))
44		(%sort-ref "Int" nil)
45		(%opattrs nil nil nil nil nil nil nil t)
46		nil)
47		(%op-decl ("_" "rem" "_")
48		((%sort-ref "Int" nil)
49		(%sort-ref "NzInt" nil))
50		(%sort-ref "Int" nil)
51		(%opattrs nil nil nil nil nil nil nil t)
52		nil)
53		(%op-decl ("_" "divides" "_")
54		((%sort-ref "NzInt" nil)
55		(%sort-ref "Int" nil))
56		(%sort-ref "Bool" nil)
57		(%opattrs nil nil nil nil nil nil nil t)
58		nil)
59		(%op-decl ("_" "<" "_")
60		((%sort-ref "Int" nil)
61		(%sort-ref "Int" nil))
62		(%sort-ref "Bool" nil)
63		(%opattrs nil nil nil nil nil nil nil t)
64		nil)
65		(%op-decl ("_" "<=" "_")
66		((%sort-ref "Int" nil)
67		(%sort-ref "Int" nil))
68		(%sort-ref "Bool" nil)
69		(%opattrs nil nil nil nil nil nil nil t)
70		nil)
71		(%op-decl ("_" ">" "_")
72		((%sort-ref "Int" nil)
73		(%sort-ref "Int" nil))
74		(%sort-ref "Bool" nil)
75		(%opattrs nil nil nil nil nil nil nil t)
76		nil)
77		(%op-decl ("_" ">=" "_")
78		((%sort-ref "Int" nil)
79		(%sort-ref "Int" nil))
80		(%sort-ref "Bool" nil)
81		(%opattrs nil nil nil nil nil nil nil t)
82		nil)
83		(%op-decl ("s" "_") ((%sort-ref "Int" nil))
84		(%sort-ref "Int" nil)
85		(%opattrs nil nil nil nil nil nil nil t)
86		nil)
87		(%op-decl ("-" "_") ((%sort-ref "Int" nil))
88		(%sort-ref "Int" nil)
89		(%opattrs nil nil 15 nil nil nil nil t)
90		nil)
91		(%op-decl ("-" "_") ((%sort-ref "NzInt" nil))
92		(%sort-ref "NzInt" nil)
93		(%opattrs nil nil 15 nil nil nil nil t)
94		nil)
95		(%var-decl ("I" "J") (%sort-ref "Int" nil))
96		(%var-decl ("NJ") (%sort-ref "NzInt" nil))
97		(%axiom-decl :equation (":BDEMOD") ("-" "I")
98		((%slisp (- i))) nil nil)
99		(%axiom-decl :equation (":BDEMOD") ("I" "+" "J")
100		((%slisp (+ i j))) nil nil)
101		(%axiom-decl :equation (":BDEMOD") ("I" "-" "J")
102		("I" "+" "(" "-" "J" ")") nil nil)
103		(%axiom-decl :equation (":BDEMOD") ("I" "*" "J")
104		((%slisp (* i j))) nil nil)
105		(%axiom-decl :equation (":BDEMOD") ("I" "quo" "NJ")
106		((%slisp (truncate i nj))) nil nil)
107		(%axiom-decl :equation (":BDEMOD") ("I" "rem" "NJ")
108		((%slisp (rem i nj))) nil nil)
109		(%axiom-decl :equation (":BDEMOD") ("NJ" "divides" "I")
110		((%slisp (= 0 (rem i nj)))) nil nil)
111		(%axiom-decl :equation (":BDEMOD") ("I" "<" "J")
112		((%slisp (< i j))) nil nil)
113		(%axiom-decl :equation (":BDEMOD") ("I" "<=" "J")
114		((%slisp (<= i j))) nil nil)
115		(%axiom-decl :equation (":BDEMOD") ("I" ">" "J")
116		((%slisp (> i j))) nil nil)
117		(%axiom-decl :equation (":BDEMOD") ("I" ">=" "J")
118		((%slisp (>= i j))) nil nil)
119		(%axiom-decl :equation (":BDEMOD") ("s" "I")
120		("1" "+" "I") nil nil))))
121		(eval-ast-if-need '(%protect "INT" :set))
122		(eval-ast-if-need '(%provide "INT"))
123		(eval-ast-if-need '(%provide "int"))
124		))
125
126		(defun chaos-int-tram-interface ()
127		(setq z-int (get-z-module-or-panic "INT"))
128		(push z-int tram-builtin-modules)
129		)
130
131		(eval-when (:execute :load-toplevel)
132		(chaos-install-int)
133		(chaos-int-tram-interface))
134
135		;;; EOF

+54

-0

lib/lib/int.cafe less more

	0	sys:mod! INT
	1	principal-sort Int
	2	{
	3	imports {
	4	protecting (NAT)
	5	protecting (INT-VALUE)
	6	}
	7	signature {
	8	pred _ divides _ : NzInt Int { demod prec: 41 }
	9	op _ rem _ : Int NzInt -> Int { demod prec: 41 }
	10	op _ quo _ : Int NzInt -> Int { demod prec: 41 }
	11	op _ + _ : Int Int -> Int { idr: 0 demod prec: 41 }
	12	op _ * _ : Int Int -> Int { demod prec: 41 }
	13	pred _ < _ : Int Int { demod prec: 41 }
	14	pred _ <= _ : Int Int { demod prec: 41 }
	15	pred _ > _ : Int Int { demod prec: 41 }
	16	pred _ >= _ : Int Int { demod prec: 41 }
	17	op s _ : Int -> Int { strat: (0 1) demod prec: 15 }
	18	op _ - _ : Int Int -> Int { strat: (0 1 2) demod prec: 33 r-assoc }
	19	op - _ : Int -> Int { demod prec: 15 }
	20	op - _ : NzInt -> NzInt { demod prec: 15 }
	21	}
	22	axioms {
	23	var I : Int
	24	var J : Int
	25	var NJ : NzInt
	26	eq [:BDEMOD]: (- I) = #! (- i) .
	27	eq [:BDEMOD]: (I + J) = #! (+ i j) .
	28	eq [:BDEMOD]: (I - J) = (I + (- J)) .
	29	eq [:BDEMOD]: (I * J) = #! (* i j) .
	30	eq [:BDEMOD]: (I quo NJ) = #! (truncate i nj) .
	31	eq [:BDEMOD]: (I rem NJ) = #! (rem i nj) .
	32	eq [:BDEMOD]: (NJ divides I) = #! (= 0 (rem i nj)) .
	33	eq [:BDEMOD]: (I < J) = #! (< i j) .
	34	eq [:BDEMOD]: (I <= J) = #! (<= i j) .
	35	eq [:BDEMOD]: (I > J) = #! (> i j) .
	36	eq [:BDEMOD]: (I >= J) = #! (>= i j) .
	37	eq [:BDEMOD]: (s I) = (1 + I) .
	38	}
	39	}
	40
	41	lispq
	42	(defun chaos-int-tram-interface ()
	43	(setq z-int (get-z-module-or-panic "INT"))
	44	(push z-int tram-builtin-modules)
	45
	46	lispq
	47	(eval-when (:execute :load-toplevel)
	48	(chaos-int-tram-interface))
	49
	50	provide int
	51	provide INT
	52	--
	53	eof

+32

-33

lib/lib/metalevel.cafe less more

124	124	}
125	125
126	126	mod! QID-LIST {
127		protecting (:LIST * {sort NeList -> NeQidList, sort List -> QidList})
	127	protecting (:LIST(QID) * {sort NeList -> NeQidList, sort List -> QidList})
128	128	}
129	129
130	130	mod! QID-SET {
131		protecting (:SET * {sort NeSet -> NeQidSet, sort Set -> QidSet})
	131	protecting (:SET(QID) * {sort NeSet -> NeQidSet, sort Set -> QidSet})
132	132	}
133	133
134	134	**

199	199	op [_<_] : Sort Sort -> SubsortDecl {ctor}
200	200	op none : -> SubsortDeclSet {ctor}
201	201	op __ : SubsortDeclSet SubsortDeclSet -> SubsortDeclSet {ctor assoc comm id: none}
202		eq S:SubsortDecl S:SubsortDecl = S:SubsortDecl
	202	eq S:SubsortDecl S:SubsortDecl = S:SubsortDecl .
203	203
204	204	** sort set
205	205	[ EmptySortSet < SortSet < QidSet]
206	206	[ Sort < NeSortSet < SortSet ]
207	207	[ NeSortSet < NeQidSet ]
208		op none : -> EmptyTypeSet {ctor}
	208	op none : -> EmptySortSet {ctor}
209	209	op _;_ : SortSet SortSet -> SortSet {ctor assoc comm id: none prec: 43}
210	210	op _;_ : NeSortSet SortSet -> NeSortSet {ctor assoc comm id: none prec: 43}
211		op _;_ : EmptySortSet EmptySortSet -> EmptyTypeSet {ctor assoc comm id: none prec: 43}
	211	op _;_ : EmptySortSet EmptySortSet -> EmptySortSet {ctor assoc comm id: none prec: 43}
212	212
213	213	** sort lists
214		[ NeTypeList TypeList ]
215		[ Type < NeTypeList < TypeList < QidList ]
216		-- subsorts NeTypeList < NeQidList .
217		op nil : -> TypeList [ctor] .
218		op __ : TypeList TypeList -> TypeList {ctor assoc comm id: none}
219		op __ : NeTypeList TypeList -> NeTypeList {ctor assoc comm id: none}
220		op __ : TypeList NeTypeList -> NeTypeList {ctor assoc comm id: none}
221		eq T:TypeList ; T:TypeList = T:TypeList .
	214	[ NeSortList SortList ]
	215	[ Sort < NeSortList < SortList < QidList ]
	216
	217	op nil : -> SortList {ctor}
	218	op __ : SortList SortList -> SortList {ctor assoc comm id: nil}
	219	op __ : NeSortList SortList -> NeSortList {ctor assoc comm id: nil}
	220	op __ : SortList NeSortList -> NeSortList {ctor assoc comm id: nil}
	221	eq T:SortList ; T:SortList = T:SortList .
222	222
223	223	** sets of sort lists
224		sort TypeListSet .
225		subsort TypeList TypeSet < TypeListSet .
226		op _;_ : TypeListSet TypeListSet -> TypeListSet {ctor assoc comm id: none prec: 43}
	224	[ SortList SortSet < SortListSet ]
	225	op none : -> SortListSet
	226	op _;_ : SortListSet SortListSet -> SortListSet {ctor assoc comm id: none prec: 43}
227	227
228	228	** attribute sets
229	229	[ Attr < AttrSet ]

233	233
234	234	** renamings
235	235	[ Renaming < RenamingSet ]
236		op sort_->_ : Qid Qid -> Renaming {ctor}
237		op op_->_{_} : Qid Qid AttrSet -> Renaming {ctor}
238		op op_:_->_to_{_} : Qid TypeList Type Qid AttrSet -> Renaming {ctor}
	236	op (sort_->_) : Qid Qid -> Renaming {ctor}
	237	op (op_->_) : Qid Qid -> Renaming {ctor}
	238	op (op_:_->_to_) : Qid SortList Sort Qid -> Renaming {ctor}
239	239	op label_->_ : Qid Qid -> Renaming {ctor}
240	240	op _,_ : RenamingSet RenamingSet -> RenamingSet {ctor assoc comm prec: 43}
241	241
242	242	** parameter lists
243		--sort EmptyCommaList NeParameterList ParameterList .
244	243	[ Sort < NeParameterList < ParameterList ]
245	244	[ EmptyCommaList < GroundTermList ParameterList ]
246	245	op empty : -> EmptyCommaList {ctor}

290	289
291	290	** operator declarations
292	291	[ OpDecl < OpDeclSet ]
293		op (op_:_->_[_].) : Qid TypeList Type AttrSet -> OpDecl {ctor}
	292	op (op_:_->_{_}) : Qid SortList Sort AttrSet -> OpDecl {ctor}
294	293	op none : -> OpDeclSet {ctor}
295	294	op __ : OpDeclSet OpDeclSet -> OpDeclSet {ctor assoc comm id: none}
296	295	eq O:OpDecl O:OpDecl = O:OpDecl .

307	306
308	307	** equations
309	308	[ Equation < EquationSet ]
310		op eq[_]:_=_. : AttrSet Term Term -> Equation {ctor}
311		op ceq[_]:_=_if_[_]. : AttrSet Term Term EqCondition -> Equation {ctor}
	309	op (eq[_]:_=_.) : AttrSet Term Term -> Equation {ctor}
	310	op (ceq[_]:_=_if_.) : AttrSet Term Term EqCondition -> Equation {ctor}
312	311	op none : -> EquationSet {ctor}
313	312	op __ : EquationSet EquationSet -> EquationSet{ctor assoc comm id: none}
314	313	eq E:Equation E:Equation = E:Equation .
315	314
316	315	** rules
317	316	[ Rule < RuleSet ]
318		op rl[_]:_=>_. : AttrSet Term Term AttrSet -> Rule {ctor}
319		op crl[_]:_=>_if_. : AttrSet Term Term Condition AttrSet -> Rule {ctor}
	317	op (tr[_]:_=>_.) : AttrSet Term Term -> Rule {ctor}
	318	op (ctr[_]:_=>_if_.) : AttrSet Term Term Condition -> Rule {ctor}
320	319	op none : -> RuleSet {ctor}
321	320	op __ : RuleSet RuleSet -> RuleSet {ctor assoc comm id: none}
322	321	eq R:Rule R:Rule = R:Rule .
323	322
324	323	** modules
325		sorts FModule SModule FTheory STheory Module .
326	324	[ FModule < SModule < Module ]
327	325	[ FTheory < STheory < Module ]
328	326	[ Qid < Header ]
329	327
330		op _{_} : Qid ParameterDeclList -> Header {ctor}
	328	op _[_] : Qid ParameterDeclList -> Header {ctor}
331	329	op module!_{_[_]__} : Header ImportList SubsortDeclSet OpDeclSet EquationSet
332	330	-> FModule {ctor}
333		format (d d s n++i ni d d ni ni ni ni n--i d)] .
	331
334	332	op module_{_[_]___} : Header ImportList SubsortDeclSet OpDeclSet EquationSet RuleSet
335	333	-> SModule {ctor}
336	334	op [_] : Qid -> Module .
337		eq [Q:Qid] = (th Q:Qid is including Q:Qid .
338		sorts none . none none none none none endth) .
	335	** eq [Q:Qid] = (module* Q:Qid { including(Q:Qid)
	336	** [ none ] none none none none none }) .
339	337
340	338	** projection functions
341	339	var Q : Qid .

346	344	var SS : SortSet .
347	345	var SSDS : SubsortDeclSet .
348	346	var OPDS : OpDeclSet .
349		var MAS : MembAxSet .
350	347	var EQS : EquationSet .
351	348	var RLS : RuleSet .
352
	349	}
	350
	351	eof
353	352	op getName : Module -> Qid .
354	353	eq getName(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = Q .
355	354	eq getName(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = Q .

382	381	eq getOps(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = OPDS .
383	382	eq getOps(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = OPDS .
384	383
385		op getMbs : Module -> MembAxSet .
	384	;; op getMbs : Module -> MembAxSet .
386	385	eq getMbs(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = MAS .
387	386	eq getMbs(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = MAS .
388	387	eq getMbs(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = MAS .

+0

-147

~~lib/lib/nat.bin~~ less more

0		;CHAOS_BINS_____
1		;;;-- Mode:LISP: Package: CHAOS; Base:10: Syntax:Common-lisp --
2		;;; $Id: nat.bin,v 1.2 2007-01-24 10:03:39 sawada Exp $
3		;;;
4		(in-package :chaos)
5
6		(defun chaos-install-nat ()
7		(let ((dribble-ast nil)
8		(ast-log nil)
9		(last-module nil)
10		(current-module nil)
11		(include-bool nil)
12		(include-rwl nil)
13		(regularize-signature nil))
14		(declare (special dribble-ast ast-log
15		last-module current-module
16		include-bool include-rwl
17		regularize-signature))
18		(eval-ast-if-need '(%module-decl "NAT" :object :system
19		((%import :protecting "NZNAT" nil)
20		(%import :protecting "NAT-VALUE" nil)
21		(%psort-decl (%sort-ref "Nat" nil))
22		(%op-decl ("_" "+" "_")
23		((%sort-ref "Nat" nil)
24		(%sort-ref "Nat" nil))
25		(%sort-ref "Nat" nil)
26		(%opattrs ((:idr "0")) nil nil nil nil nil nil t)
27		nil)
28		(%op-decl ("sd")
29		((%sort-ref "Nat" nil)
30		(%sort-ref "Nat" nil))
31		(%sort-ref "Nat" nil)
32		(%opattrs (:comm) nil nil nil nil nil nil t)
33		nil)
34		(%op-decl ("_" "*" "_")
35		((%sort-ref "Nat" nil)
36		(%sort-ref "Nat" nil))
37		(%sort-ref "Nat" nil)
38		(%opattrs nil nil nil nil nil nil nil t)
39		nil)
40		(%op-decl ("_" "quo" "_")
41		((%sort-ref "Nat" nil)
42		(%sort-ref "NzNat" nil))
43		(%sort-ref "Nat" nil)
44		(%opattrs nil nil nil nil nil nil nil t)
45		nil)
46		(%op-decl ("_" "rem" "_")
47		((%sort-ref "Nat" nil)
48		(%sort-ref "NzNat" nil))
49		(%sort-ref "Nat" nil)
50		(%opattrs nil nil nil nil nil nil nil t)
51		nil)
52		(%opattr-decl (%opref ("_" "rem" "_") nil 2)
53		(%opattrs nil :l-assoc 31 nil nil nil nil t))
54		(%op-decl ("_" "divides" "_")
55		((%sort-ref "NzNat" nil)
56		(%sort-ref "Nat" nil))
57		(%sort-ref "Bool" nil)
58		(%opattrs nil nil nil nil nil nil nil t)
59		nil)
60		(%opattr-decl
61		(%opref ("_" "divides" "_") nil 2)
62		(%opattrs nil nil 51 nil nil nil nil t))
63		(%op-decl ("_" "<" "_")
64		((%sort-ref "Nat" nil)
65		(%sort-ref "Nat" nil))
66		(%sort-ref "Bool" nil)
67		(%opattrs nil nil nil nil nil nil nil t)
68		nil)
69		(%op-decl ("_" "<=" "_")
70		((%sort-ref "Nat" nil)
71		(%sort-ref "Nat" nil))
72		(%sort-ref "Bool" nil)
73		(%opattrs nil nil nil nil nil nil nil t)
74		nil)
75		(%op-decl ("_" ">" "_")
76		((%sort-ref "Nat" nil)
77		(%sort-ref "Nat" nil))
78		(%sort-ref "Bool" nil)
79		(%opattrs nil nil nil nil nil nil nil t)
80		nil)
81		(%op-decl ("_" ">=" "_")
82		((%sort-ref "Nat" nil)
83		(%sort-ref "Nat" nil))
84		(%sort-ref "Bool" nil)
85		(%opattrs nil nil nil nil nil nil nil t)
86		nil)
87		(%op-decl ("s" "_") ((%sort-ref "Nat" nil))
88		(%sort-ref "NzNat" nil)
89		(%opattrs nil nil nil nil nil nil nil t)
90		nil)
91		(%op-decl ("p" "_") ((%sort-ref "NzNat" nil))
92		(%sort-ref "Nat" nil)
93		(%opattrs nil nil nil nil nil nil nil t)
94		nil)
95		(%opattr-decl (%opref ("p" "_") nil 1)
96		(%opattrs nil nil 15 nil nil nil nil t))
97		(%var-decl ("M" "N") (%sort-ref "Nat" nil))
98		(%var-decl ("NN") (%sort-ref "NzNat" nil))
99		(%axiom-decl :equation (":BDEMOD")
100		("sd" "(" "M" "," "N" ")")
101		((%slisp (abs (- m n)))) nil nil)
102		(%axiom-decl :equation (":BDEMOD") ("M" "+" "N")
103		((%slisp (+ m n))) nil nil)
104		(%axiom-decl :equation (":BDEMOD") ("N" "*" "0") ("0")
105		nil nil)
106		(%axiom-decl :equation (":BDEMOD") ("M" "quo" "NN")
107		((%slisp (truncate m nn))) nil nil)
108		(%axiom-decl :equation (":BDEMOD") ("M" "rem" "NN")
109		((%slisp (rem m nn))) nil nil)
110		(%axiom-decl :equation (":BDEMOD") ("NN" "divides" "M")
111		((%slisp (= 0 (rem m nn)))) nil nil)
112		(%axiom-decl :equation (":BDEMOD") ("N" "<" "0")
113		("false") nil nil)
114		(%axiom-decl :equation (":BDEMOD") ("0" "<" "NN")
115		("true") nil nil)
116		(%axiom-decl :equation (":BDEMOD") ("NN" "<=" "0")
117		("false") nil nil)
118		(%axiom-decl :equation (":BDEMOD") ("0" "<=" "N")
119		("true") nil nil)
120		(%axiom-decl :equation (":BDEMOD") ("0" ">" "N")
121		("false") nil nil)
122		(%axiom-decl :equation (":BDEMOD") ("NN" ">" "0")
123		("true") nil nil)
124		(%axiom-decl :equation (":BDEMOD") ("0" ">=" "NN")
125		("false") nil nil)
126		(%axiom-decl :equation (":BDEMOD") ("N" ">=" "0")
127		("true") nil nil)
128		(%axiom-decl :equation (":BDEMOD") ("s" "0") ("1") nil nil)
129		(%axiom-decl :equation (":BDEMOD") ("p" "NN")
130		((%slisp (- nn 1))) nil nil))))
131		(eval-ast-if-need '(%protect ("NAT") :set))
132		(eval-ast-if-need '(%provide "NAT"))
133		(eval-ast-if-need '(%provide "nat"))
134		))
135
136		(defun chaos-nat-tram-interface ()
137		(setq z-nat (get-z-module-or-panic "NAT"))
138		(push z-nat tram-builtin-modules)
139		)
140
141		(eval-when (:execute :load-toplevel)
142		(chaos-install-nat)
143		(chaos-nat-tram-interface))
144
145		;;; EOF
146

+57

-0

lib/lib/nat.cafe less more

	0	sys:mod! NAT
	1	principal-sort Nat
	2	{
	3	imports {
	4	protecting (NZNAT)
	5	protecting (NAT-VALUE)
	6	}
	7	signature {
	8	op s _ : Nat -> NzNat { demod prec: 15 }
	9	pred _ >= _ : Nat Nat { demod prec: 41 }
	10	pred _ > _ : Nat Nat { demod prec: 41 }
	11	pred _ <= _ : Nat Nat { demod prec: 41 }
	12	pred _ < _ : Nat Nat { demod prec: 41 }
	13	op _ * _ : Nat Nat -> Nat { strat: (2 0 1) demod prec: 41 }
	14	op _ + _ : Nat Nat -> Nat { idr: 0 demod prec: 41 }
	15	op sd : Nat Nat -> Nat { comm demod prec: 0 }
	16	op _ quo _ : Nat NzNat -> Nat { demod prec: 41 }
	17	op _ rem _ : Nat NzNat -> Nat { demod prec: 31 l-assoc }
	18	pred _ divides _ : NzNat Nat { demod prec: 51 }
	19	op p _ : NzNat -> Nat { demod prec: 15 }
	20	}
	21	axioms {
	22	var M : Nat
	23	var N : Nat
	24	var NN : NzNat
	25	eq [:BDEMOD]: sd(M,N) = #! (abs (- m n)) .
	26	eq [:BDEMOD]: (M + N) = #! (+ m n) .
	27	eq [:BDEMOD]: (N * 0) = 0 .
	28	eq [:BDEMOD]: (M quo NN) = #! (truncate m nn) .
	29	eq [:BDEMOD]: (M rem NN) = #! (rem m nn) .
	30	eq [:BDEMOD]: (NN divides M) = #! (= 0 (rem m nn)) .
	31	eq [:BDEMOD]: (N < 0) = false .
	32	eq [:BDEMOD]: (0 < NN) = true .
	33	eq [:BDEMOD]: (NN <= 0) = false .
	34	eq [:BDEMOD]: (0 <= N) = true .
	35	eq [:BDEMOD]: (0 > N) = false .
	36	eq [:BDEMOD]: (NN > 0) = true .
	37	eq [:BDEMOD]: (0 >= NN) = false .
	38	eq [:BDEMOD]: (N >= 0) = true .
	39	eq [:BDEMOD]: (s 0) = 1 .
	40	eq [:BDEMOD]: (p NN) = #! (- nn 1) .
	41	}
	42	}
	43
	44	lispq
	45	(defun chaos-nat-tram-interface ()
	46	(setq z-nat (get-z-module-or-panic "NAT"))
	47	(push z-nat tram-builtin-modules))
	48
	49	lispq
	50	(eval-when (:execute :load-toplevel)
	51	(chaos-nat-tram-interface))
	52
	53	provide nat
	54	provide NAT
	55	--
	56	eof

+0

-130

~~lib/lib/nznat.bin~~ less more

0		;CHAOS_BINS_____
1		;;;-- Mode:LISP: Package: CHAOS; Base:10: Syntax:Common-lisp --
2		;;; $Id: nznat.bin,v 1.2 2007-01-24 10:03:39 sawada Exp $
3		;;;
4		(in-package :chaos)
5		(defun chaos-install-nznat ()
6		(let ((dribble-ast nil)
7		(ast-log nil)
8		(last-module nil)
9		(current-module nil)
10		(include-bool nil)
11		(include-rwl nil)
12		(regularize-signature nil))
13		(declare (special dribble-ast ast-log
14		last-module current-module
15		include-bool include-rwl
16		regularize-signature))
17		(eval-ast-if-need '(%module-decl "NZNAT" :object :system
18		((%import :protecting "NZNAT-VALUE" nil)
19		(%import :protecting "BOOL" nil)
20		(%psort-decl (%sort-ref "NzNat" nil))
21		(%op-decl ("_" "+" "_")
22		((%sort-ref "NzNat" nil)
23		(%sort-ref "NzNat" nil))
24		(%sort-ref "NzNat" nil)
25		(%opattrs nil nil nil nil nil nil nil t)
26		nil)
27		(%opattr-decl (%opref ("_" "+" "_") nil 2)
28		(%opattrs (:assoc :comm) nil 33 nil nil
29		nil nil t))
30		(%op-decl ("d")
31		((%sort-ref "NzNat" nil)
32		(%sort-ref "NzNat" nil))
33		(%sort-ref "NzNat" nil)
34		(%opattrs nil nil nil nil nil nil nil t)
35		nil)
36		(%opattr-decl (%opref ("d") nil 2)
37		(%opattrs (:comm) nil nil nil nil nil nil t))
38		(%op-decl ("_" "*" "_")
39		((%sort-ref "NzNat" nil)
40		(%sort-ref "NzNat" nil))
41		(%sort-ref "NzNat" nil)
42		(%opattrs nil nil nil nil nil nil nil t)
43		nil)
44		(%opattr-decl (%opref ("_" "*" "_") nil 2)
45		(%opattrs (:assoc :comm (:idr "1")) nil 31
46		nil nil nil nil t))
47		(%op-decl ("_" "quot" "_")
48		((%sort-ref "NzNat" nil)
49		(%sort-ref "NzNat" nil))
50		(%sort-ref "NzNat" nil)
51		(%opattrs nil nil nil nil nil nil nil t)
52		nil)
53		(%opattr-decl (%opref ("_" "quot" "_") nil 2)
54		(%opattrs nil :l-assoc 31 nil nil nil nil t))
55		(%op-decl ("_" "<" "_")
56		((%sort-ref "NzNat" nil)
57		(%sort-ref "NzNat" nil))
58		(%sort-ref "Bool" nil)
59		(%opattrs nil nil nil nil nil nil nil t)
60		nil)
61		(%opattr-decl (%opref ("_" "<" "_") nil 2)
62		(%opattrs nil nil 51 nil nil nil nil t))
63		(%op-decl ("_" "<=" "_")
64		((%sort-ref "NzNat" nil)
65		(%sort-ref "NzNat" nil))
66		(%sort-ref "Bool" nil)
67		(%opattrs nil nil nil nil nil nil nil t)
68		nil)
69		(%opattr-decl (%opref ("_" "<=" "_") nil 2)
70		(%opattrs nil nil 51 nil nil nil nil t))
71		(%op-decl ("_" ">" "_")
72		((%sort-ref "NzNat" nil)
73		(%sort-ref "NzNat" nil))
74		(%sort-ref "Bool" nil)
75		(%opattrs nil nil nil nil nil nil nil t)
76		nil)
77		(%opattr-decl (%opref ("_" ">" "_") nil 2)
78		(%opattrs nil nil 51 nil nil nil nil t))
79		(%op-decl ("_" ">=" "_")
80		((%sort-ref "NzNat" nil)
81		(%sort-ref "NzNat" nil))
82		(%sort-ref "Bool" nil)
83		(%opattrs nil nil nil nil nil nil nil t)
84		nil)
85		(%opattr-decl (%opref ("_" ">=" "_") nil 2)
86		(%opattrs nil nil 51 nil nil nil nil t))
87		(%op-decl ("s" "_") ((%sort-ref "NzNat" nil))
88		(%sort-ref "NzNat" nil)
89		(%opattrs nil nil nil nil nil nil nil t)
90		nil)
91		(%opattr-decl (%opref ("s" "_") nil 1)
92		(%opattrs nil nil 15 nil nil nil nil t))
93		(%var-decl ("NN" "NM") (%sort-ref "NzNat" nil))
94		(%axiom-decl :equation (":BDEMOD") ("NN" "+" "NM")
95		((%slisp (+ nn nm))) nil nil)
96		(%axiom-decl :equation (":BDEMOD")
97		("d" "(" "NN" "," "NM" ")")
98		((%slisp (if (= nn nm) 1 (abs (- nn nm)))))
99		nil nil)
100		(%axiom-decl :equation (":BDEMOD") ("NN" "*" "NM")
101		((%slisp (* nn nm))) nil nil)
102		(%axiom-decl :equation (":BDEMOD") ("NN" "quot" "NM")
103		((%slisp (if (> nn nm) (truncate nn nm) 1)))
104		nil nil)
105		(%axiom-decl :equation (":BDEMOD") ("NN" "<" "NM")
106		((%slisp (< nn nm))) nil nil)
107		(%axiom-decl :equation (":BDEMOD") ("NN" "<=" "NM")
108		((%slisp (<= nn nm))) nil nil)
109		(%axiom-decl :equation (":BDEMOD") ("NN" ">" "NM")
110		((%slisp (> nn nm))) nil nil)
111		(%axiom-decl :equation (":BDEMOD") ("NN" ">=" "NM")
112		((%slisp (>= nn nm))) nil nil)
113		(%axiom-decl :equation (":BDEMOD") ("s" "NN")
114		((%slisp (1+ nn))) nil nil))))
115		(eval-ast-if-need '(%protect ("NZNAT") :set))
116		(eval-ast-if-need '(%provide "NZAT"))
117		(eval-ast-if-need '(%provide "nznat"))
118		))
119
120		(defun chaos-nznat-tram-interface ()
121		(setq z-nznat (get-z-module-or-panic "NZNAT"))
122		(pushnew z-nznat tram-builtin-modules))
123
124		(eval-when (:execute :load-toplevel)
125		(chaos-install-nznat)
126		(chaos-nznat-tram-interface)
127		)
128		;;; EOF
129

+51

-0

lib/lib/nznat.cafe less more

	0	**
	1	** NZNAT
	2	**
	3
	4	sys:mod! NZNAT
	5	principal-sort NzNat
	6	{
	7	imports {
	8	protecting (NZNAT-VALUE)
	9	protecting (BOOL)
	10	}
	11	signature {
	12	op _ + _ : NzNat NzNat -> NzNat { assoc comm demod prec: 33 r-assoc }
	13	op d : NzNat NzNat -> NzNat { comm demod prec: 0 }
	14	op _ * _ : NzNat NzNat -> NzNat { assoc comm idr: 1 demod prec: 31 r-assoc }
	15	op _ quot _ : NzNat NzNat -> NzNat { demod prec: 31 l-assoc }
	16	pred _ < _ : NzNat NzNat { demod prec: 51 }
	17	pred _ <= _ : NzNat NzNat { demod prec: 51 }
	18	pred _ > _ : NzNat NzNat { demod prec: 51 }
	19	pred _ >= _ : NzNat NzNat { demod prec: 51 }
	20	op s _ : NzNat -> NzNat { demod prec: 15 }
	21	}
	22	axioms {
	23	var NN : NzNat
	24	var NM : NzNat
	25	eq [:BDEMOD]: (NN + NM) = #! (+ nn nm) .
	26	eq [:BDEMOD]: d(NN,NM) = #! (if (= nn nm) 1 (abs (- nn nm))) .
	27	eq [:BDEMOD]: (NN * NM) = #! (* nn nm) .
	28	eq [:BDEMOD]: (NN quot NM) = #! (if (> nn nm) (truncate nn nm) 1) .
	29	eq [:BDEMOD]: (NN < NM) = #! (< nn nm) .
	30	eq [:BDEMOD]: (NN <= NM) = #! (<= nn nm) .
	31	eq [:BDEMOD]: (NN > NM) = #! (> nn nm) .
	32	eq [:BDEMOD]: (NN >= NM) = #! (>= nn nm) .
	33	eq [:BDEMOD]: (s NN) = #! (1+ nn) .
	34	eq [ident0]: (1 * X-ID:NzNat) = X-ID .
	35	}
	36	}
	37
	38	lispq
	39	(defun chaos-nznat-tram-interface ()
	40	(setq z-nznat (get-z-module-or-panic "NZNAT"))
	41	(pushnew z-nznat tram-builtin-modules))
	42
	43	lispq
	44	(eval-when (:execute :load-toplevel)
	45	(chaos-nznat-tram-interface))
	46
	47	provide nznat
	48	provide NZNAT
	49	--
	50	eof

+2

-1

lib/lib/qid.cafe less more

0		sys:mod! QID {
	0	sys:mod! QID psort Qid
	1	{
1	2	protecting (STRING)
2	3	bsort Qid (is-qid-token create-qid print-qid is-qid nil)
3	4	op string : Qid -> String

+0

-128

~~lib/lib/rat.bin~~ less more

0		;CHAOS_BINS_____
1		;;;-- Mode:LISP: Package: CHAOS; Base:10: Syntax:Common-lisp --
2		;;; $Id: rat.bin,v 1.2 2007-01-24 10:03:39 sawada Exp $
3		;;;
4		(in-package :chaos)
5		(defun chaos-install-rat ()
6		(let ((dribble-ast nil)
7		(ast-log nil)
8		(last-module nil)
9		(current-module nil)
10		(include-bool nil)
11		(include-rwl nil)
12		(regularize-signature nil))
13		(declare (special dribble-ast ast-log
14		last-module current-module
15		include-bool include-rwl
16		regularize-signature))
17		(eval-ast-if-need '(%module-decl "RAT" :object :system
18		((%import :protecting "INT" nil)
19		(%import :protecting "RAT-VALUE" nil)
20		(%psort-decl (%sort-ref "Rat" nil))
21		(%op-decl ("-" "_") ((%sort-ref "Rat" nil))
22		(%sort-ref "Rat" nil)
23		(%opattrs nil nil 15 nil nil nil nil t)
24		nil)
25		(%op-decl ("-" "_") ((%sort-ref "NzRat" nil))
26		(%sort-ref "NzRat" nil)
27		(%opattrs nil nil 15 nil nil nil nil t)
28		nil)
29		(%op-decl ("_" "+" "_")
30		((%sort-ref "Rat" nil)
31		(%sort-ref "Rat" nil))
32		(%sort-ref "Rat" nil)
33		(%opattrs ((:idr "0")) nil nil nil nil nil nil t)
34		nil)
35		(%op-decl ("_" "-" "_")
36		((%sort-ref "Rat" nil)
37		(%sort-ref "Rat" nil))
38		(%sort-ref "Rat" nil)
39		(%opattrs nil nil nil nil nil nil nil t)
40		nil)
41		(%op-decl ("_" "*" "_")
42		((%sort-ref "Rat" nil)
43		(%sort-ref "Rat" nil))
44		(%sort-ref "Rat" nil)
45		(%opattrs nil nil nil nil nil nil nil t)
46		nil)
47		(%op-decl ("_" "/" "_")
48		((%sort-ref "Rat" nil)
49		(%sort-ref "NzRat" nil))
50		(%sort-ref "Rat" nil)
51		(%opattrs nil nil nil nil nil nil nil t)
52		nil)
53		(%opattr-decl (%opref ("_" "/" "_") nil 2)
54		(%opattrs nil :l-assoc 31 nil nil nil nil t))
55		(%op-decl ("_" "/" "_")
56		((%sort-ref "NzRat" nil)
57		(%sort-ref "NzRat" nil))
58		(%sort-ref "NzRat" nil)
59		(%opattrs nil nil nil nil nil nil nil t)
60		nil)
61		(%op-decl ("_" "rem" "_")
62		((%sort-ref "Rat" nil)
63		(%sort-ref "NzRat" nil))
64		(%sort-ref "Rat" nil)
65		(%opattrs nil nil nil nil nil nil nil t)
66		nil)
67		(%op-decl ("_" "<" "_")
68		((%sort-ref "Rat" nil)
69		(%sort-ref "Rat" nil))
70		(%sort-ref "Bool" nil)
71		(%opattrs nil nil nil nil nil nil nil t)
72		nil)
73		(%op-decl ("_" "<=" "_")
74		((%sort-ref "Rat" nil)
75		(%sort-ref "Rat" nil))
76		(%sort-ref "Bool" nil)
77		(%opattrs nil nil nil nil nil nil nil t)
78		nil)
79		(%op-decl ("_" ">" "_")
80		((%sort-ref "Rat" nil)
81		(%sort-ref "Rat" nil))
82		(%sort-ref "Bool" nil)
83		(%opattrs nil nil nil nil nil nil nil t)
84		nil)
85		(%op-decl ("_" ">=" "_")
86		((%sort-ref "Rat" nil)
87		(%sort-ref "Rat" nil))
88		(%sort-ref "Bool" nil)
89		(%opattrs nil nil nil nil nil nil nil t)
90		nil)
91		(%var-decl ("R" "S") (%sort-ref "Rat" nil))
92		(%var-decl ("NS") (%sort-ref "NzRat" nil))
93		(%axiom-decl :equation (":BDEMOD") ("R" "+" "S")
94		((%slisp (+ r s))) nil nil)
95		(%axiom-decl :equation (":BDEMOD") ("-" "R")
96		((%slisp (- r))) nil nil)
97		(%axiom-decl :equation (":BDEMOD") ("R" "-" "S")
98		("R" "+" "(" "-" "S" ")") nil nil)
99		(%axiom-decl :equation (":BDEMOD") ("R" "*" "S")
100		((%slisp (* r s))) nil nil)
101		(%axiom-decl :equation (":BDEMOD") ("R" "/" "NS")
102		((%slisp (/ r ns))) nil nil)
103		(%axiom-decl :equation (":BDEMOD") ("R" "rem" "NS")
104		((%slisp (rem r ns))) nil nil)
105		(%axiom-decl :equation (":BDEMOD") ("R" "<" "S")
106		((%slisp (< r s))) nil nil)
107		(%axiom-decl :equation (":BDEMOD") ("R" "<=" "S")
108		((%slisp (<= r s))) nil nil)
109		(%axiom-decl :equation (":BDEMOD") ("R" ">" "S")
110		((%slisp (> r s))) nil nil)
111		(%axiom-decl :equation (":BDEMOD") ("R" ">=" "S")
112		((%slisp (>= r s))) nil nil))))
113		(eval-ast-if-need '(%protect ("RAT") :set))
114		(eval-ast-if-need '(%provide "RAT"))
115		(eval-ast-if-need '(%provide "rat"))
116		))
117
118		(defun chaos-rat-tram-interface ()
119		(setq z-rat (get-z-module-or-panic "RAT"))
120		(push z-rat tram-builtin-modules)
121		)
122
123		(eval-when (:execute :load-toplevel)
124		(chaos-install-rat)
125		(chaos-rat-tram-interface))
126
127		;;; EOF

+53

-0

lib/lib/rat.cafe less more

	0	sys:mod! RAT
	1	principal-sort Rat
	2	{
	3	imports {
	4	protecting (INT)
	5	protecting (RAT-VALUE)
	6	}
	7	signature {
	8	op - _ : Rat -> Rat { demod prec: 15 }
	9	op - _ : NzRat -> NzRat { demod prec: 15 }
	10	op _ - _ : Rat Rat -> Rat { strat: (0 1 2) demod prec: 33 r-assoc }
	11	pred _ >= _ : Rat Rat { demod prec: 41 }
	12	pred _ > _ : Rat Rat { demod prec: 41 }
	13	pred _ <= _ : Rat Rat { demod prec: 41 }
	14	pred _ < _ : Rat Rat { demod prec: 41 }
	15	op _ * _ : Rat Rat -> Rat { demod prec: 41 }
	16	op _ + _ : Rat Rat -> Rat { idr: 0 demod prec: 41 }
	17	op _ rem _ : Rat NzRat -> Rat { demod prec: 41 }
	18	op _ / _ : Rat NzRat -> Rat { demod prec: 31 l-assoc }
	19	op _ / _ : NzRat NzRat -> NzRat { demod prec: 31 l-assoc }
	20	}
	21	axioms {
	22	var R : Rat
	23	var S : Rat
	24	var NS : NzRat
	25	eq [:BDEMOD]: (R + S) = #! (+ r s) .
	26	eq [:BDEMOD]: (- R) = #! (- r) .
	27	eq [:BDEMOD]: (R - S) = (R + (- S)) .
	28	eq [:BDEMOD]: (R * S) = #! (* r s) .
	29	eq [:BDEMOD]: (R / NS) = #! (/ r ns) .
	30	eq [:BDEMOD]: (R rem NS) = #! (rem r ns) .
	31	eq [:BDEMOD]: (R < S) = #! (< r s) .
	32	eq [:BDEMOD]: (R <= S) = #! (<= r s) .
	33	eq [:BDEMOD]: (R > S) = #! (> r s) .
	34	eq [:BDEMOD]: (R >= S) = #! (>= r s) .
	35	}
	36	}
	37
	38	lispq
	39	(defun chaos-rat-tram-interface ()
	40	(setq z-rat (get-z-module-or-panic "RAT"))
	41	(push z-rat tram-builtin-modules))
	42
	43	lispq
	44	(eval-when (:execute :load-toplevel)
	45	(chaos-rat-tram-interface))
	46
	47	provide rat
	48	provide RAT
	49	--
	50	eof
	51
	52

+1

-1

lib/lib/reobject.bin less more

166	166	(eval-ast-if-need '(%provide "reobject"))
167	167	))
168	168
169		(eval-when (execute :load-toplevel)
	169	(eval-when (:execute :load-toplevel)
170	170	(let ((chaos-quiet t))
171	171	(chaos-install-record-object))
172	172	)

+2

-1

lib/lib/string.cafe less more

0		sys:mod! STRING {
	0	sys:mod! STRING psort String
	1	{
1	2	protecting (NAT)
2	3	protecting (CHARACTER)
3	4	protecting (STRING-VALUE)

+0

-58

~~lib/lib/tuple.bin~~ less more

0		;CHAOS_BINS_____
1		;;;-- Mode:LISP: Package: CHAOS; Base:10: Syntax:Common-lisp --
2		;;; $Id: tuple.bin,v 1.2 2007-01-24 10:03:39 sawada Exp $
3		;;;
4		(in-package :chaos)
5		(defun chaos-install-2tuple ()
6		(let ((dribble-ast nil)
7		(ast-log nil)
8		(last-module nil)
9		(current-module nil)
10		(include-bool nil)
11		(include-rwl nil)
12		(regularize-signature nil))
13		(declare (special dribble-ast ast-log
14		last-module current-module
15		include-bool include-rwl
16		regularize-signature))
17
18		(eval-ast-if-need-no-error '(%module-decl "2TUPLE" :object :system
19		((%import :protecting "TRIV" "C1")
20		(%import :protecting "TRIV" "C2")
21		(%sort-decl (%sort-ref "2Tuple" nil)
22		nil)
23		(%op-decl ("<<" "_" ";" "_" ">>")
24		((%sort-ref "Elt" "C1")
25		(%sort-ref "Elt" "C2"))
26		(%sort-ref "2Tuple" nil)
27		(%opattrs nil nil nil nil nil t nil)
28		nil)
29		(%op-decl ("1*" "_")
30		((%sort-ref "2Tuple" nil))
31		(%sort-ref "Elt" "C1")
32		(%opattrs nil nil nil nil nil nil nil t)
33		nil)
34		(%op-decl ("2*" "_")
35		((%sort-ref "2Tuple" nil))
36		(%sort-ref "Elt" "C2")
37		(%opattrs nil nil nil nil nil nil nil t)
38		nil)
39		(%var-decl ("e1")
40		(%sort-ref "Elt" "C1"))
41		(%var-decl ("e2")
42		(%sort-ref "Elt" "C2"))
43		(%axiom-decl :equation (":BDEMOD")
44		("1*" "<<" "e1" ";" "e2" ">>")
45		("e1") nil nil)
46		(%axiom-decl :equation (":BDEMOD")
47		("2*" "<<" "e1" ";" "e2" ">>")
48		("e2") nil nil))))
49		(eval-ast-if-need-no-error '(%protect ("2TUPLE") :set))
50		(eval-ast-if-need-no-error '(%provide "2TUPLE"))
51		(eval-ast-if-need-no-error '(%provide "tuple"))
52		))
53
54		(eval-when (:execute :load-toplevel)
55		(chaos-install-2tuple))
56
57		;;; EOF

+6

-16

lib/prelude/std.bin less more

0	0	;CHAOS_BINS_____
1	1	#\|\| -- Mode: LISP --
2	2	-- Chaos internal file --
3		chaos version: 1.4.7
	3	chaos version: 1.4.13
4	4	file: lib/prelude/std.bin
5		Wed Jan 24 12:41:58 JST 2007
	5	Wed March 5 18:28:14: JST 2014
6	6	* NOTE : DO NOT MODIFY THIS FILE ULESS YOU REALLY KNOW WHAT YOU ARE DOING!.
7	7	\|\|#
8	8	(in-package :CHAOS)

18	18	(setq autoload-alist
19	19	'(("TRUTH" . "truth")
20	20	("BOOL" . "bool")
21		("IDENTICAL" . "identical")
22	21	("RWL" . "rwl")
23	22	("NZNAT" . "nznat")
24	23	("NAT" . "nat")

29	28	("FOPL-CLAUSE" . "fopl")
30	29	("PROPC" . "propc")
31	30	("STRING" . "string")
32		("2TUPLE" . "tuple")
	31	("2TUPLE" . "2tuple")
33	32	("3TUPLE" . "3tuple")
34	33	("4TUPLE" . "4tuple")
35	34	("EQL" . "eql")

40	39	("STATE-CONFIGURATION" . "reobject")
41	40	("ACZ-CONFIGURATION" . "reobject")
42	41	("QID" . "qid")
43		("META-LEVEL" . "meta")
	42	("META-LEVEL" . "metalevel")
44	43	))
45		#\|\| --- no more depends : important intitializations are
46		moved to the introduction of TRUTH-VALUE.
47		;; we need TRUTH at start up
48		(chaos-input-file :file "truth"
49		:proc 'process-cafeobj-input
50		:suffix '(".mod" ".bin")
51		:load-path chaos-libpath
52		:args nil
53		:errorp t)
54		\|\|#
55		)⏎
	44	)
	45	;;; EOF⏎

0		;;--Mode:LISP; Package: CHAOS; Base:10; Syntax:Common-lisp --
	0	;;;--Mode:LISP; Package: CHAOS; Base:10; Syntax:Common-lisp --
1	1	;;; $Id: parse-engine.lisp,v 1.12 2010-07-20 06:59:37 sawada Exp $
2	2	(in-package :chaos)
3	3	#\|==============================================================================