Commit 19e73e9a9373f4f76ba0f203c2430128c7a37cf5 - cafeobj

* Adding support for a metalevel core part. tswd 10 years ago

9 changed file(s) with 496 addition(s) and 183 deletion(s). Raw diff Collapse all Expand all

-1

cafeobj/trans-com.lisp less more

558	558	(defun cafeobj-eval-module-element-proc (inp)
559	559	(if open-module
560	560	(with-in-module (last-module)
561		(let ((ast (parse-module-element inp)))
	561	(multiple-value-bind (type ast)
	562	(parse-module-element inp)
	563	(declare (ignore type))
562	564	(dolist (a ast)
563	565	(eval-ast a))))
564	566	(with-output-chaos-warning ()

+64

-39

cafeobj/trans-decl.lisp less more

374	374	(with-output-chaos-warning ()
375	375	(format t "# of arguments mismatch for mixfix operator `~{~a~}', ignored."
376	376	pat)
	377	(format t "~% arity = ~a, coarity=~a" arity coarity)
	378	;;
377	379	(return-from process-operator-declaration-form nil))
378	380	)
379	381	)

718	720	;;;
719	721	(defun parse-module-elements (s &rest ignore)
720	722	(declare (ignore ignore))
721		(let ((body nil))
	723	(let ((body nil)
	724	(sig nil)
	725	(ax nil))
722	726	(dolist (e s)
723		(setf body (nconc body (parse-module-element e))))
	727	(multiple-value-bind (kind elt)
	728	(parse-module-element e)
	729	(case kind
	730	(:misc nil)
	731	(:sig (setq sig (nconc sig elt)))
	732	(:ax (setq ax (nconc ax elt))))))
	733	(setf body (append sig ax))
724	734	body))
725	735
726	736	(defun parse-module-element (e &rest ignore)
727	737	(declare (ignore ignore))
728	738	(case-equal (car e)
729		;; SORT & Subsort Declaration.
730		("bsort" (list (process-bsort-declaration e)))
731		("[" (process-sort-and-subsort-form e))
732		(("hidden" "*") (process-hidden-sort-form e))
	739	;; SORT & Subsort Declaration.
	740	("bsort" (values :sig (list (process-bsort-declaration e))))
	741	("[" (values :sig (process-sort-and-subsort-form e)))
	742	(("hidden" "*") (values :sig (process-hidden-sort-form e)))
733	743
734	744	;; OPERATOR DECLARATION.
735	745	("op"
736		(list (process-operator-declaration-form e)))
	746	(values :sig (list (process-operator-declaration-form e))))
737	747	("ops"
738		(process-operators-declaration-form e))
	748	(values :sig (process-operators-declaration-form e)))
739	749	("bop"
740		(list (process-operator-declaration-form e)))
	750	(values :sig (list (process-operator-declaration-form e))))
741	751	("bops"
742		(process-boperators-declaration-form e))
	752	(values :sig (process-boperators-declaration-form e)))
743	753
744	754	;; predicate
745	755	("pred"
746		(list (process-predicate-declaration-form e)))
	756	(values :sig (list (process-predicate-declaration-form e))))
747	757
748	758	;; meta-demod predicate
749	759	("dpred"
750		(list (process-predicate-declaration-form e)))
	760	(values :sig (list (process-predicate-declaration-form e))))
751	761
752	762	;; behavioural
753	763	("bpred"
754		(list (process-predicate-declaration-form e)))
	764	(values :sig (list (process-predicate-declaration-form e))))
755	765
756	766	;; meta-demod behavioural predicate
757	767	("dbpred"
758		(list (process-predicate-declaration-form e)))
	768	(values :sig (list (process-predicate-declaration-form e))))
759	769
760	770	;; OPERATOR-ATTRIBUTES.
761	771	(("opattr" "attr" "attrs")
762		(list (process-opattr-declaration-form e)))
	772	(values :sig (list (process-opattr-declaration-form e))))
763	773
764	774	;; RECORD DECLARATION.
765	775	(("rec" "record")
766		(list (process-record-declaration-form e)))
	776	(values :sig (list (process-record-declaration-form e))))
767	777
768	778	;; CLASS DECLARATION.
769	779	(("cls" "class")
770		(list (process-class-declaration-form e)))
	780	(values :sig (list (process-class-declaration-form e))))
771	781
772	782	;; LET Construct.
773		("let" (list (process-let-declaration-form e)))
	783	("let" (values :ax (list (process-let-declaration-form e))))
774	784
775	785	;; Macro
776		("#define" (list (process-macro-declaration-form e)))
	786	("#define" (values :ax (list (process-macro-declaration-form e))))
777	787
778	788	;; Axioms
779	789	(("eq" "cq" "ceq" "rule" "rl" "crl" "crule" "trans" "ctrans" "trns" "ctrns"
780	790	"beq" "bceq" "brule" "brl" "bcrule" "bcrl" "btrans" "btrns"
781	791	"bctrans" "bctrns")
782		(list (process-axiom-form e)))
	792	(values :ax (list (process-axiom-form e))))
783	793
784	794	;; VARIABLE declaration.
785	795	(("var" "vars")
786		(list (process-variable-declaration-form e)))
	796	(values :ax (list (process-variable-declaration-form e))))
787	797
788	798	(("pvar" "pvars")
789		(list (process-pseud-variable-declaration-form e)))
	799	(values :ax (list (process-pseud-variable-declaration-form e))))
790	800
791	801	#+:bigpink
792	802	;; FOPL
793	803	(("fax" "bfax" "ax" "bax" "frm" "bfrm")
794		(list (pignose-process-fax-proc e)))
	804	(values :ax (list (pignose-process-fax-proc e))))
795	805	#+:bigpink
796	806	(("goal" "bgoal")
797		(list (pignose-process-goal-proc e)))
	807	(values :ax (list (pignose-process-goal-proc e))))
798	808
799	809	#\|\|
800	810	("vars-of" ; NOT YET
801		(list (process-vars-of-declaration-form e)))
	811	(values :ax (list (process-vars-of-declaration-form e))))
802	812	\|\|#
803	813	;; IMPORTATIONS.
804	814	(("imports" "import")

816	826	(nconc body (list
817	827	(%dyna-comment* (cons "**" (cdr elt)))))))
818	828	(t (setf body (nconc body (process-importation-form elt))))))))
819		body))
	829	(values :sig body)))
820	830
821	831	(("pr" "protecting" "ex" "extending" "us" "using" "inc" "including")
822		(process-importation-form e))
	832	(values :sig (process-importation-form e)))
823	833
824	834	;; Comments.
825	835	;; must prepare ....
826		(("--" "**") nil) ; do nothing
	836	(("--" "**") (values :misc nil)) ; do nothing
827	837	;; should delay the output.
828		("-->" (list (%dyna-comment* (cons "--" (cdr e)))))
829		("*>" (list (%dyna-comment (cons "**" (cdr e)))))
	838	("-->" (let ((comm (%dyna-comment* (cons "--" (cdr e)))))
	839	(eval-ast comm)
	840	(values :misc nil)))
	841	("*>" (let ((comm (%dyna-comment (cons "**" (cdr e)))))
	842	(eval-ast comm)
	843	(values :misc nil)))
830	844
831	845	;; AS -- not yet
832	846	;; ("as" (list (process-as-form e)))

835	849
836	850	;; MISC ..
837	851	(("ev" "lisp" "evq" "lispq")
838		(list (%lisp-eval* (cadr e))))
	852	(let ((form (%lisp-eval* (cadr e))))
	853	(eval-ast form)
	854	(values :misc nil)))
839	855
840	856	(("eval")
841		(list (%eval* (cadr e))))
	857	(list (values :misc (%eval* (cadr e)))))
842	858
843	859	;; SIG, AX
844	860	(("sig" "signature")

847	863	(unless (equal s-body "}")
848	864	(dolist (elt s-body)
849	865	(unless (equal elt "}")
850		(setf body (nconc body (parse-module-element elt))))))
851		body))
	866	(multiple-value-bind (type sig)
	867	(parse-module-element elt)
	868	(declare (ignore type))
	869	(setf body (nconc body sig))))))
	870	(values :sig body)))
852	871
853	872	(("axioms" "axiom" "axs")
854	873	(let ((body nil)

856	875	(unless (equal a-body "}")
857	876	(dolist (elt a-body)
858	877	(unless (equal elt "}" )
859		(setf body (nconc body (parse-module-element elt))))))
860		body))
	878	(multiple-value-bind (type ax)
	879	(parse-module-element elt)
	880	(declare (ignore type))
	881	(setf body (nconc body ax))))))
	882	(values :sig body)))
861	883
862	884	((".") ; sole dots
863		nil)
	885	(values :misc nil))
864	886	;; Unknown...
865	887	(t (format t "~&Processing module elements : unknown form: ~a, ignored." e)
866		nil)))
	888	(values :misc nil))))
867	889
868	890	(defun parse-module-element-1 (e &rest ignore)
869		(car (parse-module-element e ignore)))
	891	(multiple-value-bind (type elt)
	892	(parse-module-element e ignore)
	893	(declare (ignore type))
	894	(car elt)))
870	895
871	896	;;; ********************
872	897	;;; VIEW DECLARTION FORM _______________________________________________________

-2

chaos/boot/builtins.lisp less more

229	229	((%psort-decl (%sort-ref "Float" nil))
230	230	(%bsort-decl "Float" is-float-token
231	231	create-float print-float is-float nil))))
232		#\|\|
233	232	(eval-ast-if-need '(%module-decl "ID" :object :hard
234	233	((%psort-decl (%sort-ref "Id" nil))
235	234	(%bsort-decl "Id" is-id-token create-id
236	235	print-id is-id nil))))
237	236	(setup-id)
238
	237	#\|\|
239	238	(eval-ast-if-need '(%module-decl "QID" :object :hard
240	239	((%psort-decl (%sort-ref "QId" nil))
241	240	(%bsort-decl "QId" is-qid-token create-qid

+17

-23

chaos/boot/preproc.lisp less more

155	155	(alpha-char-p (char token 1))))
156	156
157	157	(defun create-qId (token)
158		(if (eql #\' (char token 0))
159		(intern (subseq token 1))
160		(intern token)))
161
162		(defun print-qId (x) (format t "'~a" (string x)))
	158	(intern token))
	159
	160	(defun print-qId (x) (format t "~a" (string x)))
163	161
164	162	(defun is-qId (x)
165	163	(and (symbolp x)

181	179	(alpha-char-p (char token 1))))
182	180
183	181	(defun create-Sort-object (token)
184		(if (eql #\' (char token 0))
185		(intern (subseq token 1))
186		(intern token)))
187
188		(defun print-meta-sort-object (x) (format t "'~a" (string x)))
	182	(intern token))
	183
	184	(defun print-meta-sort-object (x) (format t "~a" (string x)))
189	185
190	186	(defun is-sort-object (x)
191	187	(and (symbolp x)

202	198	(position #\. token :start 1)))
203	199
204	200	(defun create-constant-object (token)
205		(if (eql #\' (char token 0))
206		(intern (subseq token 1))
207		(intern token)))
208
209		(defun print-constant-object (x) (format t "'~a" (string x)))
	201	(intern token))
	202
	203	(defun print-constant-object (x) (format t "~a" (string x)))
210	204
211	205	(defun is-constant-object (x)
212	206	(and (symbolp x)

536	530	(break)))))
537	531
538	532	(defun s-find (Char Str Num)
539		(let ((C (term-builtin-value char))
	533	(let ((C (term-builtin-value Char))
540	534	(S (term-builtin-value Str))
541	535	(N (term-builtin-value Num)))
542		(let ((pos (position C S :start N)))
543		(if pos
544		(simple-parse-from-string (format nil "~s" pos))
545		string-not-found))))
546
547		(defun s-rfind (C S N)
	536	(let ((pos (position C S :start N)))
	537	(if pos
	538	(simple-parse-from-string (format nil "~s" pos))
	539	(simple-parse-from-string "notFound")))))
	540
	541	(defun s-rfind (Char Str Num)
548	542	(let ((C (term-builtin-value char))
549	543	(S (term-builtin-value Str))
550	544	(N (term-builtin-value Num)))
551	545	(let ((pos (position C S :start N :from-end t)))
552	546	(if pos
553	547	(simple-parse-from-string (format nil "~s" pos))
554		string-not-found))))
	548	(simple-parse-from-string "notFound")))))
555	549
556	550	; ;;;-----------------------------------------------------------------------------
557	551	; ;;; module CHAOS:EXPR

-4

chaos/construct/operator.lisp less more

323	323	;; commutativity
324	324	;;
325	325	(when (theory-contains-commutativity theory)
326		(unless (sort= (car arity) (cadr arity))
	326	(unless (is-in-same-connected-component (car arity) (cadr arity) current-sort-order)
327	327	;;
328	328	(unless inherit
329	329	(with-output-chaos-warning ()
330		(princ "the current implementation requires a STRONG condition for")
331		(print-next)
332		(princ "commutative operations, their arguments must be of the SAME sort,")
	330	(princ "commutative operations, their arguments must be of the same connected component.")
333	331	(print-next)
334	332	(princ "`comm' attribute of operation ")
335	333	(print-chaos-object method)

+41

-57

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

223	223	;; normal token
224	224	(t (setq res (dictionary-get-token-info (dictionary-table dictionary)
225	225	token))
	226	;; check builtin constant
	227	(let (pos)
	228	(dolist (bi (dictionary-builtins dictionary))
	229	(let ((token-pred (bsort-token-predicate bi)))
	230	(when (and token-pred
	231	(funcall token-pred token))
	232	(push bi pos))))
	233	(if pos
	234	;; may be builtin constant.
	235	(if (cdr pos)
	236	(let ((so (module-sort-order
	237	current-module)))
	238	(dolist (bi pos)
	239	(unless (some #'(lambda (x) (sort< x bi so)) pos)
	240	(push (dictionary-make-builtin-constant token bi) res))))
	241	(push (dictionary-make-builtin-constant token (car pos)) res))))
	242
226	243	;; blocked let variable?
227	244	;; TODO
228	245

232	249	(when val
233	250	(if (is-special-let-variable? token)
234	251	(push val res)
235		(push (simple-copy-term-sharing-variables
236		val dictionary)
	252	(push (simple-copy-term-sharing-variables val dictionary)
237	253	res)))))
238	254	;; try other possiblities.
239	255	;; variable ?

265	281	(setq var-name (subseq (the simple-string token)
266	282	0
267	283	(the fixnum q-pos)))
268		;; (setf var-name (intern var-name))
269	284	(setf sort (find-sort-in current-module
270	285	(subseq
271	286	(the simple-string token)

360	375
361	376	;; must not be a variable declaration.
362	377	;; try yet other possibilities.
363		(t (let ((pos nil))
364		;; builtin constant tokens?
365		(dolist (bi (dictionary-builtins dictionary))
366		(let ((token-pred (bsort-token-predicate bi)))
367		(when (and token-pred
368		(funcall token-pred token))
369		(push bi pos))))
370		(if pos
371		;; may be builtin constant.
372		(if (cdr pos)
373		(let ((so (module-sort-order
374		current-module)))
375		(dolist (bi pos)
376		(unless (some #'(lambda (x)
377		(sort< x bi so))
378		pos)
379		(push
380		(dictionary-make-builtin-constant
381		token bi)
382		res))))
383		(push (dictionary-make-builtin-constant
384		token
385		(car pos))
386		res))
387
388		;; no possibilities of vairable nor builtin
389		;; constant.
390		(let ((ast (gethash token builtin-ast-dict)))
391		(if ast
392		;; abstract syntax tree.
393		(setf res ast))
394		(unless res
395		(multiple-value-setq (res mod-token)
396		(get-qualified-op-pattern token)))
397		;;
398		(when (and (null res)
399		(memq identifier-sort
400		(module-all-sorts
401		current-module)))
402		(let ((ident (intern token)))
403		(unless (member ident '(\|.\| \|,\|
404		\|(\| \|)\|
405		\|{\| \|}\|
406		\|[\| \|]\|))
407		(push (make-bconst-term
408		identifier-sort ident)
409		res))))))))
410		)))))
411		;; #\|\|
	378	(t
	379	;; no possibilities of vairable nor builtin
	380	;; constant.
	381	(let ((ast (gethash token builtin-ast-dict)))
	382	(if ast
	383	;; abstract syntax tree.
	384	(setf res ast))
	385	(unless res
	386	(multiple-value-setq (res mod-token)
	387	(get-qualified-op-pattern token)))
	388	;;
	389	(when (and (null res)
	390	(memq identifier-sort
	391	(module-all-sorts
	392	current-module)))
	393	(let ((ident (intern token)))
	394	(unless (member ident '(\|.\| \|,\|
	395	\|(\| \|)\|
	396	\|{\| \|}\|
	397	\|[\| \|]\|))
	398	(push (make-bconst-term identifier-sort ident) res)))))))))))
412	399	;; final possibility
413	400	(unless res
414	401	(multiple-value-setq (res mod-token)
415		(get-qualified-op-pattern token)))
416		;; \|\|#
417		)))
418		;;
	402	(get-qualified-op-pattern token))))))
	403	;; end collect
419	404	(when sort-constraint
420	405	(let ((real-res nil))
421	406	(dolist (r res)

448	433	(print-chaos-object sort-constraint)
449	434	(format t "~& : result info = ~s" res)
450	435	(print-chaos-object res))
451		;; (values (delete-duplicates res :test #'equal) (car mod-token))
452	436	(values res (car mod-token))
453	437	))
454	438

+363

-13

lib/lib/metalevel.cafe less more

	0	**
	1	** CafeOBJ MetaLevel Core
	2	**
	3	module! :SET(X :: TRIV) {
	4	protecting (BOOL)
	5	protecting (NAT)
	6	[ Elt.X < NeSet < Set ]
	7
	8	op empty : -> Set {ctor}
	9	op _;_ : Set Set -> Set {ctor assoc comm id: empty prec: 43}
	10	op _;_ : NeSet Set -> NeSet {ctor assoc comm id: empty prec: 43}
	11
	12	var E : Elt.X
	13	var N : NeSet
	14	vars A S S' : Set
	15	var C : Nat
	16
	17	op !espattern : Elt.X Set -> Bool
	18	eq !espattern(E, (N ; S)) = true .
	19
	20	eq N, N = N .
	21
	22	op insert : Elt.X Set -> Set
	23	eq insert(E ; S) = E, S .
	24
	25	op delete : Elt.X Set -> Set
	26	eq delete(E, (E ; S)) = delete(E, S) .
	27	ceq delete(E ; S) = S if !espattern(E, S) =/= true .
	28
	29	op _in_ : Elt.X Set -> Bool
	30	eq E in (E ; S) = true .
	31	ceq E in S = false if !espattern(E,S) =/= true .
	32
	33	op \|_\| : Set -> Nat
	34	op \|_\| : NeSet -> NzNat
	35	eq \| S \| = $card(S, 0) .
	36
	37	op $card : Set Nat -> Nat
	38	eq $card(empty, C) = C .
	39	eq $card((N ; N ; S), C) = $card((N ; S), C) .
	40	ceq $card((E ; S), C) = $card(S, C + 1) if !espattern(E, S) =/= true .
	41
	42	op union : Set Set -> Set
	43	op union : NeSet Set -> NeSet
	44	op union : Set NeSet -> NeSet
	45	eq union(S, S') = S, S' .
	46
	47	op intersection : Set Set -> Set
	48	eq intersection(S, empty) = empty .
	49	eq intersection(S, N) = $intersect(S, N, empty) .
	50
	51	op $intersect : Set Set Set -> Set
	52	eq $intersect(empty, S', A) = A .
	53	eq $intersect((E ; S), S', A) = $intersect(S, S', if E in S' then E ; A else A fi) .
	54
	55	op _\_ : Set Set -> Set
	56	eq S \ empty = S .
	57	eq S \ N = $diff(S; N, empty) .
	58
	59	op $diff : Set Set Set -> Set
	60	eq $diff(empty, S', A) = A .
	61	eq $diff((E; S), S', A) = $diff(S, S', if E in S' then A else E ; A fi) .
	62
	63	op _subset_ : Set Set -> Bool .
	64	eq empty subset S' = true .
	65	eq (E, S) subset S' = E in S' and-also S subset S' .
	66
	67	op _psubset_ : Set Set -> Bool .
	68	eq S psubset S' = S =/= S' and-also S subset S' .
	69	}
	70
	71	module! :LIST(X :: TRIV) {
	72	protecting (NAT)
	73	[ Elt.X < NeList < List ]
	74
	75	op nil : -> List {ctor}
	76	op __ : List List -> List {ctor assoc id: nil prec: 25}
	77	op __ : NeList List -> NeList {ctor assoc id: nil prec: 25}
	78	op __ : List NeList -> NeList {ctor assoc id: nil prec: 25}
	79
	80	vars E E' : Elt.X
	81	vars A L : List
	82	var C : Nat
	83
	84	op append : List List -> List
	85	op append : NeList List -> NeList
	86	op append : List NeList -> NeList
	87	eq append(A, L) = A L .
	88
	89	op head : NeList -> Elt.X
	90	eq head(E L) = E .
	91
	92	op tail : NeList -> List
	93	eq tail(E L) = L .
	94
	95	op last : NeList -> Elt.X
	96	eq last(L E) = E .
	97
	98	op front : NeList -> List
	99	eq front(L E) = L .
	100
	101	op occurs : Elt.X List -> Bool
	102	eq occurs(E, nil) = false .
	103	eq occurs(E, E' L) = if E == E' then true else occurs(E, L) fi .
	104
	105	op reverse : List -> List
	106	op reverse : NeList -> NeList
	107	eq reverse(L) = $reverse(L, nil) .
	108
	109	op $reverse : List List -> List
	110	eq $reverse(nil, A) = A .
	111	eq $reverse(E L, A) = $reverse(L, E A).
	112
	113	op size : List -> Nat .
	114	op size : NeList -> NzNat
	115	eq size(L) = $size(L, 0) .
	116
	117	op $size : List Nat -> Nat
	118	eq $size(nil, C) = C .
	119	eq $size(E L, C) = $size(L, C + 1) .
	120	}
	121
	122	module! NAT-LIST {
	123	protecting (:LIST(NAT) * {sort NeList -> NeNatList, sort List -> NatList})
	124	}
	125
	126	module! QID-LIST {
	127	protecting (:LIST * {sort NeList -> NeQidList, sort List -> QidList})
	128	}
	129
	130	module! QID-SET {
	131	protecting (:SET * {sort NeSet -> NeQidSet, sort Set -> QidSet})
	132	}
	133
	134	**
	135	** META-TERM
	136	**
0	137	module! META-TERM {
1	138	protecting (QID)
2	139

20	157	op _[_] : Qid NeGroundTermList -> GroundTerm {ctor}
21	158	op _[_] : Qid NeTermList -> Term {ctor}
22	159
	160	** contexts (terms with a single hole)
	161	[ Context < NeCTermList < GTermList,
	162	TermList < GTermList ]
	163
	164	op [] : -> Context {ctor}
	165	op _,_ : TermList NeCTermList -> NeCTermList {ctor assoc id: empty prec 121}
	166	op _,_ : NeCTermList TermList -> NeCTermList {ctor assoc id: empty prec 121}
	167	op _,_ : GTermList GTermList -> GTermList {ctor assoc id: empty prec 121}
	168	op _[_] : Qid NeCTermList -> Context {ctor}
	169
23	170	** extraction of names and types
24	171	op getName : Constant -> Qid
25	172	op getType : Constant -> Sort
26	173	var C : Constant
27	174	eq getName(C) = qid(substring(string(C), 0, rfind('.', string(C), 0))) .
28		eq getType(C) = qid(substring(string(C), rfind('.', string(C), 0))) .
	175	eq getType(C) = qid(substring(string(C), rfind('.', string(C), 0) + 1)) .
29	176
30	177	op getName : Variable -> Qid
31	178	op getType : Variable -> Sort
32	179	var V : Variable
33	180	eq getName(V) = qid(substring(string(V), 0, rfind(':', string(V), 0))) .
34		eq getType(V) = qid(substring(string(V), rfind(':', string(V), 0))) .
	181	eq getType(V) = qid(substring(string(V), rfind(':', string(V), 0) + 1)) .
35	182
36	183	** substitutions
37	184	[ Assignment < Substitution ]

40	187	op _;_ : Substitution Substitution -> Substitution
41	188	{ctor assoc comm id: none prec 65}
42	189	eq A:Assignment ; A:Assignment = A:Assignment .
43
44		** contexts (terms with a single hole)
45		[ Context < NeCTermList < GTermList,
46		TermList < GTermList ]
47
48		op [] : -> Context {ctor}
49		op _,_ : TermList NeCTermList -> NeCTermList {ctor assoc id: empty prec 121}
50		op _,_ : NeCTermList TermList -> NeCTermList {ctor assoc id: empty prec 121}
51		op _,_ : GTermList GTermList -> GTermList {ctor assoc id: empty prec 121}
52		op _[_] : Qid NeCTermList -> Context {ctor}
53		}
	190	}
	191
	192	module! META-MODULE {
	193	protecting (META-TERM)
	194	protecting (NAT-LIST)
	195	protecting (QID-LIST)
	196	protecting (QID-SET * {op empty -> none})
	197
	198	** subsort declarations
	199	[ SubsortDecl < SubsortDeclSet ]
	200	op [_<_] : Sort Sort -> SubsortDecl {ctor}
	201	op none : -> SubsortDeclSet {ctor}
	202	op __ : SubsortDeclSet SubsortDeclSet -> SubsortDeclSet {ctor assoc comm id: none}
	203	eq S:SubsortDecl S:SubsortDecl = S:SubsortDecl
	204
	205	** sort set
	206	[ EmptySortSet < SortSet < QidSet]
	207	[ Sort < NeSortSet < SortSet ]
	208	[ NeSortSet < NeQidSet ]
	209	op none : -> EmptyTypeSet {ctor}
	210	op _;_ : SortSet SortSet -> SortSet {ctor assoc comm id: none prec: 43}
	211	op _;_ : NeSortSet SortSet -> NeSortSet {ctor assoc comm id: none prec: 43}
	212	op _;_ : EmptySortSet EmptySortSet -> EmptyTypeSet {ctor assoc comm id: none prec: 43}
	213
	214	** sort lists
	215	[ NeTypeList TypeList ]
	216	[ Type < NeTypeList < TypeList < QidList ]
	217	-- subsorts NeTypeList < NeQidList .
	218	op nil : -> TypeList [ctor] .
	219	op __ : TypeList TypeList -> TypeList {ctor ditto}
	220	op __ : NeTypeList TypeList -> NeTypeList {ctor ditto}
	221	op __ : TypeList NeTypeList -> NeTypeList {ctor ditto}
	222	eq T:TypeList ; T:TypeList = T:TypeList .
	223
	224	** sets of sort lists
	225	sort TypeListSet .
	226	subsort TypeList TypeSet < TypeListSet .
	227	op _;_ : TypeListSet TypeListSet -> TypeListSet {ctor assoc comm id: none prec: 43}
	228
	229	** attribute sets
	230	[ Attr < AttrSet ]
	231	op none : -> AttrSet {ctor}
	232	op __ : AttrSet AttrSet -> AttrSet {ctor assoc comm id: none}
	233	eq A:Attr A:Attr = A:Attr .
	234
	235	** renamings
	236	[ Renaming < RenamingSet ]
	237	op sort_->_ : Qid Qid -> Renaming {ctor}
	238	op op_->_{_} : Qid Qid AttrSet -> Renaming {ctor}
	239	op op_:_->_to_{_} : Qid TypeList Type Qid AttrSet -> Renaming {ctor}
	240	op label_->_ : Qid Qid -> Renaming {ctor}
	241	op _,_ : RenamingSet RenamingSet -> RenamingSet {ctor assoc comm prec: 43}
	242
	243	** parameter lists
	244	--sort EmptyCommaList NeParameterList ParameterList .
	245	[ Sort < NeParameterList < ParameterList ]
	246	[ EmptyCommaList < GroundTermList ParameterList ]
	247	op empty : -> EmptyCommaList {ctor}
	248	op _,_ : ParameterList ParameterList -> ParameterList {ctor ditto}
	249	op _,_ : NeParameterList ParameterList -> NeParameterList {ctor ditto}
	250	op _,_ : ParameterList NeParameterList -> NeParameterList {ctor ditto}
	251	op _,_ : EmptyCommaList EmptyCommaList -> EmptyCommaList {ctor ditto}
	252
	253	** module expressions
	254	[ Qid < ModuleExpression ]
	255	op _+_ : ModuleExpression ModuleExpression -> ModuleExpression {ctor assoc comm}
	256	op _*{_} : ModuleExpression RenamingSet -> ModuleExpression {ctor prec: 39}
	257	op _(_) : ModuleExpression ParameterList -> ModuleExpression {ctor prec: 37}
	258
	259	** parameter declarations
	260	[ ParameterDecl < NeParameterDeclList < ParameterDeclList ]
	261	op _::_ : Sort ModuleExpression -> ParameterDecl .
	262	op nil : -> ParameterDeclList [ctor] .
	263	op _,_ : ParameterDeclList ParameterDeclList -> ParameterDeclList {ctor
	264	op _,_ : NeParameterDeclList ParameterDeclList -> NeParameterDeclList {ctor assoc id: nil prec: 121}
	265	op _,_ : ParameterDeclList NeParameterDeclList -> NeParameterDeclList {ctor assoc id: nil prec: 121}
	266
	267	** importations
	268	[ Import < ImportList ]
	269	op protecting : ModuleExpression -> Import {ctor}
	270	op extending : ModuleExpression -> Import {ctor}
	271	op including : ModuleExpression -> Import {ctor}
	272	op nil : -> ImportList {ctor}
	273	op __ : ImportList ImportList -> ImportList {ctor assoc id: nil}
	274
	275	** operator attributes
	276	op assoc : -> Attr {ctor}
	277	op comm : -> Attr {ctor}
	278	op idem : -> Attr [ctor]
	279	op (id:) : Term -> Attr {ctor}
	280	op (idr:) : Term -> Attr {ctor}
	281	op l-assoc : -> Attr {ctor}
	282	op r-assoc : -> Attr {ctor}
	283	op (strat:) : NeNatList -> Attr {ctor}
	284	op memo : -> Attr {ctor}
	285	op (prec:) : Nat -> Attr {ctor}
	286	op ctor : -> Attr {ctor}
	287
	288	** statement attributes
	289	op label : Qid -> Attr {ctor}
	290	op :nonexec : -> Attr {ctor}
	291
	292	** operator declarations
	293	[ OpDecl < OpDeclSet ]
	294	op (op_:_->_[_].) : Qid TypeList Type AttrSet -> OpDecl {ctor}
	295	op none : -> OpDeclSet {ctor}
	296	op __ : OpDeclSet OpDeclSet -> OpDeclSet {ctor assoc comm id: none}
	297	eq O:OpDecl O:OpDecl = O:OpDecl .
	298
	299	** conditions
	300	[ EqCondition < Condition ]
	301	op nil : -> EqCondition {ctor}
	302	op _=_ : Term Term -> EqCondition {ctor prec: 71}
	303	op _:_ : Term Sort -> EqCondition {ctor prec: 71}
	304	op _:=_ : Term Term -> EqCondition {ctor prec: 71}
	305	op _=>_ : Term Term -> Condition {ctor prec: 71}
	306	op _/\_ : EqCondition EqCondition -> EqCondition {ctor assoc id: nil prec: 73}
	307	op _/\_ : Condition Condition -> Condition {ctor assoc id: nil prec: 73}
	308
	309	** equations
	310	[ Equation < EquationSet ]
	311	op eq[_]:_=_. : AttrSet Term Term -> Equation {ctor}
	312	op ceq[_]:_=_if_[_]. : AttrSet Term Term EqCondition -> Equation {ctor}
	313	op none : -> EquationSet {ctor}
	314	op __ : EquationSet EquationSet -> EquationSet{ctor assoc comm id: none}
	315	eq E:Equation E:Equation = E:Equation .
	316
	317	** rules
	318	[ Rule < RuleSet ]
	319	op rl[_]:_=>_. : AttrSet Term Term AttrSet -> Rule {ctor}
	320	op crl[_]:_=>_if_. : AttrSet Term Term Condition AttrSet -> Rule {ctor}
	321	op none : -> RuleSet {ctor}
	322	op __ : RuleSet RuleSet -> RuleSet {ctor assoc comm id: none}
	323	eq R:Rule R:Rule = R:Rule .
	324
	325	** modules
	326	sorts FModule SModule FTheory STheory Module .
	327	[ FModule < SModule < Module ]
	328	[ FTheory < STheory < Module ]
	329	[ Qid < Header ]
	330
	331	op _{_} : Qid ParameterDeclList -> Header {ctor}
	332	op module!_{_[_]__} : Header ImportList SubsortDeclSet OpDeclSet EquationSet
	333	-> FModule {ctor}
	334	format (d d s n++i ni d d ni ni ni ni n--i d)] .
	335	op module_{_[_]___} : Header ImportList SubsortDeclSet OpDeclSet EquationSet RuleSet
	336	-> SModule {ctor}
	337	op [_] : Qid -> Module .
	338	eq [Q:Qid] = (th Q:Qid is including Q:Qid .
	339	sorts none . none none none none none endth) .
	340
	341	** projection functions
	342	var Q : Qid .
	343	var PDL : ParameterDeclList .
	344	var H : Header .
	345	var M : Module .
	346	var IL : ImportList .
	347	var SS : SortSet .
	348	var SSDS : SubsortDeclSet .
	349	var OPDS : OpDeclSet .
	350	var MAS : MembAxSet .
	351	var EQS : EquationSet .
	352	var RLS : RuleSet .
	353
	354	op getName : Module -> Qid .
	355	eq getName(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = Q .
	356	eq getName(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = Q .
	357	eq getName(fmod Q{PDL} is IL sorts SS . SSDS OPDS MAS EQS endfm) = Q .
	358	eq getName(mod Q{PDL} is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = Q .
	359	eq getName(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = Q .
	360	eq getName(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = Q .
	361
	362	op getImports : Module -> ImportList .
	363	eq getImports(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = IL .
	364	eq getImports(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = IL .
	365	eq getImports(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = IL .
	366	eq getImports(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = IL .
	367
	368	op getSorts : Module -> SortSet .
	369	eq getSorts(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = SS .
	370	eq getSorts(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = SS .
	371	eq getSorts(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = SS .
	372	eq getSorts(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = SS .
	373
	374	op getSubsorts : Module -> SubsortDeclSet .
	375	eq getSubsorts(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = SSDS .
	376	eq getSubsorts(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = SSDS .
	377	eq getSubsorts(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = SSDS .
	378	eq getSubsorts(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = SSDS .
	379
	380	op getOps : Module -> OpDeclSet .
	381	eq getOps(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = OPDS .
	382	eq getOps(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = OPDS .
	383	eq getOps(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = OPDS .
	384	eq getOps(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = OPDS .
	385
	386	op getMbs : Module -> MembAxSet .
	387	eq getMbs(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = MAS .
	388	eq getMbs(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = MAS .
	389	eq getMbs(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = MAS .
	390	eq getMbs(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = MAS .
	391
	392	op getEqs : Module -> EquationSet .
	393	eq getEqs(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = EQS .
	394	eq getEqs(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = EQS .
	395	eq getEqs(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = EQS .
	396	eq getEqs(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = EQS .
	397
	398	op getRls : Module -> RuleSet .
	399	eq getRls(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = none .
	400	eq getRls(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = RLS .
	401	eq getRls(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = none .
	402	eq getRls(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = RLS .
	403	}

-23

lib/lib/string.cafe less more

44	44	eq [:BDEMOD]: string>(S1,S2) = #! (string> s1 s2) .
45	45	eq [:BDEMOD]: string<=(S1,S2) = #! (string<= s1 s2) .
46	46	eq [:BDEMOD]: string>=(S1,S2) = #! (string>= s1 s2) .
47		eq find(C, S, N) = #! (s-find C S N) .
48		eq rfind(C, S, N) = #! (s-rfind C S N) .
	47	eq find(C, S, N) = #!! (s-find C S N) .
	48	eq rfind(C, S, N) = #!! (s-rfind C S N) .
49	49	}
50	50
51		evq (setq x_current current-module)
52		select STRING
53		let notFound = notFound .
54		evq (setq string-not-found (simple-copy-term (get-bound-value "notFound" current-module)))
55		evq (register-metalevel-sort (term-sort string-not-found))
56		evq (when x_current (eval-mod-ext x_current t))
	51	lispq (setq _string_mod_ (eval-modexp "STRING"))
	52	lispq (with-in-module (_string_mod_)
	53	(setq strig-not-found (simple-parse-from-string "notFound")))
57	54
58	55	lispq
59	56	(defun chaos-install-string ()

74	71	(chaos-install-string)
75	72	(chaos-string-tram-interface))
76	73
77		lispq
78		(defun s-find (C S N)
79		(let ((pos (position C S :start N)))
80		(if pos
81		pos
82		string-not-found)))
83
84		lispq
85		(defun s-rfind (C S N)
86		(let ((pos (position C S :start N :from-end t)))
87		(if pos
88		pos
89		string-not-found)))
90
91		;;; EOF

-21

~~lib/mel.mod~~ less more

0		**
1		** MEL sort constraint support
2		**
3		evq
4		(defun sort-match (x s &optional (module (or current-module
5		last-module)))
6		(unless module (return-from sort-match nil))
7		(let ((so (module-sort-order module))
8		(sort (find-sort-in module (string (term-builtin-value s)))))
9		(unless sort (return-from sort-match nil))
10		(sort<= (term-sort x) sort so)))
11
12		module! MEL
13		{
14		protecting (CHAOS:IDENTIFIER)
15		[ Identifier < SortName ]
16		pred (_::_) : Universal SortName
17		eq (X:Universal :: S:SortName) = #!!(coerce-to-Bool
18		(sort-match X S)) .
19		}
20