Commit c38b56a562e3f888acf315d91d22cbafbd36534c - cafeobj

Code clean up, and supress sbcl's style-warnings. tswd 5 years ago

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

+48

-194

BigPink/codes/resolve.lisp less more

0	0	;;;--Mode:LISP; Package: CHAOS; Base:10; Syntax:Common-lisp --
1	1	;;;
2		;;; Copyright (c) 2000-2015, Toshimi Sawada. All rights reserved.
	2	;;; Copyright (c) 2000-2018, Toshimi Sawada. All rights reserved.
3	3	;;;
4	4	;;; Redistribution and use in source and binary forms, with or without
5	5	;;; modification, are permitted provided that the following conditions

79	79	(type clause new-clause)
80	80	(type list history subst)
81	81	(type (or null clash) clashes))
82		;;
83	82	(setq subst
84	83	(comb-clash-subst given-subst clash))
85		;;
86	84	(when (pn-flag debug-hyper-res)
87	85	(format t "~%build-hyper: clash =")
88	86	(prin1 clash)
89	87	(print-next)
90	88	(princ "givn-subst = ") (print-substitution given-subst)
91	89	(print-next)
92		(princ "cmb subst = ") (print-substitution subst)
93		)
94
	90	(princ "cmb subst = ") (print-substitution subst))
95	91	(when giv-sat
96	92	;; given clause is satellite
97		(push (clause-id giv-sat) history)
98		)
	93	(push (clause-id giv-sat) history))
99	94	(push (clause-id nucleus) history)
100
101	95	;; construct literals of resolvent
102
103	96	(dolist (lit giv-lits)
104	97	(declare (type literal lit))
105	98	(let ((new-literal (shallow-copy-literal lit new-clause)))

107	100	(setf (literal-atom new-literal)
108	101	(apply-subst subst (literal-atom lit)))
109	102	(push new-literal new-literals)))
110
111	103	(dolist (lit nuc-lits)
112	104	(declare (type literal lit))
113	105	(let ((new-literal (shallow-copy-literal lit new-clause)))

115	107	(setf (literal-atom new-literal)
116	108	(apply-subst subst (literal-atom lit)))
117	109	(push new-literal new-literals)))
118
119	110	(while clashes
120	111	(if (clash-evaluable clashes)
121	112	(push :eval history)

142	133	(delete-clause! junk-id current-psys))
143	134	)))
144	135	(setq clashes (clash-next clashes)))
145		;;
146	136	(setf (clause-literals new-clause)
147	137	(nreverse new-literals))
148	138

151	141	(when (pn-flag debug-hyper-res)
152	142	(format t "~%** build-hyper: new-clause =")
153	143	(print-clause new-clause))
154		;;
155		new-clause
156		))
	144	new-clause))
157	145
158	146	;;; HYPER-CLASH!
159	147	;;; - used by hyper and UR resolution to clash away the marked literals

219	207	(if (< p1 p2)
220	208	:less
221	209	nil)))))
222		;;
223	210	(let ((atom (literal-atom l1)))
224	211	(declare (type term atom))
225	212	(dolist (l2 (clause-literals (literal-clause l1)) t)

232	219	(if (and (eq (literal-sign l1)
233	220	(literal-sign l2))
234	221	(eq :less
235		#\|\|
236		(op-lex-compare (term-head atom)
237		(term-head (literal-atom l2)))
238		\|\|#
239	222	(opcompare (term-head atom)
240		(term-head (literal-atom l2)))
241		))
242		(return nil))))))
243		))
	223	(term-head (literal-atom l2)))))
	224	(return nil))))))))
244	225
245	226	(declaim (inline compose-subst2))
246	227

261	242	(t (cons (cons (caar s1)
262	243	(apply-subst s2 (cdar s1)))
263	244	(composel (cdr s1) s2))))))
264		;;
265	245	(if (car s2)
266	246	(add-new s2 (composel s1 s2))
267	247	s1)))

287	267	(type list given-subst)
288	268	(type symbol inf-id)
289	269	(type (or null clause) giv-sat))
290		#\|\|
291		(when (pn-flag debug-hyper-res)
292		(with-output-msg ()
293		(princ "clash-one:")
294		(print-next)
295		(format t "clash = ~S" clash)
296		(print-next)
297		(format t "clause-pred = ~s" clause-pred)
298		(print-next)
299		(princ "given-subst = ")
300		(print-substitution given-subst)
301		(print-next)
302		(format t "giv-sat = ~s" giv-sat)))
303		\|\|#
304	270	(let ((clashables (if (clash-clashables clash)
305	271	(cdr (clash-clashables clash))
306	272	(setf (clash-clashables clash)
307		#\|\|
308		(get-literal-entry-from-atom
309		(clash-db clash)
310		(literal-atom (clash-literal clash)))
311		\|\|#
312	273	(is-fetch-concat (literal-atom (clash-literal clash))
313		(clash-db clash))
314		)))
	274	(clash-db clash)))))
315	275	(atom (literal-atom (clash-literal clash)))
316	276	(subst (if (clash-prev clash)
317	277	(or (get-nsubst (clash-prev clash))
318	278	given-subst)
319		;; (or (clash-subst (clash-prev clash))
320		;; given-subst)
321	279	given-subst)))
322	280	(declare (type list clashables)
323	281	(type term atom)
324	282	(type list subst))
325		;;
326	283	(loop
327	284	(unless clashables
328	285	(return nil))
329	286	(block next
330		;;
331	287	(let* ((lit-data (car clashables))
332		;; (clash-lit (literal-entry-literal lit-data))
333	288	(clash-lit lit-data)
334	289	(clash-clause (literal-clause clash-lit))
335	290	(junk-cl-id nil))

343	298	(let (;; (clash-atom (literal-entry-atom clash-lit))
344	299	(clash-atom (literal-atom clash-lit))
345	300	(varmap nil)
346		(natom atom)
347		;; (renamed nil)
348		)
	301	(natom atom))
349	302	(declare (ignore varmap)
350	303	(type term clash-atom natom))
351		;;
352	304	(setq atom (apply-subst subst atom))
353	305	(when (or (eq giv-sat clash-clause)
354	306	(cl-occurs-in-clash clash-clause clash))

362	314	(setq junk-cl-id id)
363	315	(setq clash-lit tlit)
364	316	(setq clash-atom (literal-atom tlit))
365		(setq clash-clause dcl))
366		))
367		;;
	317	(setq clash-clause dcl))))
368	318	(when (pn-flag debug-hyper-res)
369	319	(with-output-msg ()
370	320	(princ "chash-one trying unify:")

375	325	(print-next)
376	326	(format t "target clause = ~s " clash-clause)
377	327	(print-next)
378		(princ "target atom = ") (term-print clash-atom)
379		))
380		;;
	328	(princ "target atom = ") (term-print clash-atom)))
381	329	(multiple-value-bind (new-subst no-match e-equal)
382	330	(unify clash-atom
383	331	atom
384		;; subst
385	332	nil)
386	333	(declare (type substitution new-subst)
387		(type (or null t) no-match e-equal))
	334	(type (or null t) no-match)
	335	(ignore e-equal))
388	336	(when no-match
389	337	(when junk-cl-id
390	338	(delete-clause! junk-cl-id current-psys))
391	339	(return-from next nil))
392		;;
393	340	(if new-subst
394	341	(progn
395		(setq new-subst (compose-subst subst new-subst))
396		;; (setq new-subst (compose-subst2 subst new-subst))
397		)
	342	(setq new-subst (compose-subst subst new-subst)))
398	343	(setq new-subst subst))
399	344	(when (pn-flag debug-hyper-res)
400	345	(with-output-simple-msg ()

418	363	(setf (clash-subst clash) new-subst)
419	364	(setf (clash-clashables clash) clashables)
420	365	(setf (clash-found-lit clash) clash-lit)
421		(return-from clash-one t))
422		)))
423		) ; block next
	366	(return-from clash-one t)))))) ; block next
424	367	;; try next clashable
425		(setq clashables (cdr clashables))
426		) ; end loop
	368	(setq clashables (cdr clashables))) ; end loop
427	369	nil))
428	370
429	371	(defun get-nsubst (clashes)

456	398	(declare (type (or null clash) clashes)
457	399	(type list list-resolvent)
458	400	(type (or null clash) c-end))
459		;;
460	401	(loop
461	402	(if (not backup)
462	403	(if (or (null c-start)

471	412	giv-lits
472	413	giv-sat
473	414	inf-id
474		nuc-pos
475		))
	415	nuc-pos))
476	416	(case inf-id
477	417	(:hyper-res-rule
478	418	(incf (pn-stat hyper-res-gen)))

484	424	;; pre-process the hyper-resolvent
485	425	(when (pre-process resolvent nil :sos)
486	426	(push resolvent list-resolvent))
487		;;
488	427	(setq backup t)
489	428	(setq c-end clashes) ; the last success clash
490		(setq clashes nil)
491		)
	429	(setq clashes nil))
492	430	;; else
493	431	(progn
494	432	(if (null clashes) ; just starting

496	434	;; try next clash
497	435	(setq clashes (clash-next clashes)))
498	436	(when (clash-evaluable clashes)
499		;; (setf (clash-subst clashes) nil)
500	437	(let* ((lit (clash-literal clashes))
501	438	(atom (literal-atom lit))
502	439	(subst (get-nsubst clashes))
503	440	(inst nil))
504		;; (setf (clash-subst clashes) subst)
505	441	(unless subst (setq subst given-subst))
506	442	(setq inst (demod-atom (apply-subst subst atom)))
507	443	(if (positive-literal? lit)

536	472	(unless (clash-evaluable clashes)
537	473	(setf (clash-subst clashes) nil))
538	474	(setq backup nil))))
539		;;
540	475	(unless backup
541	476	(if (clash-evaluable clashes)
542	477	(if (or (clash-already-evaluated clashes)

545	480	;; set flag and proceed
546	481	(setf (clash-already-evaluated clashes) t))
547	482	(unless (clash-one clashes sat-proc given-subst inf-id giv-sat)
548		(setq backup t))))
549		) ; loop end
	483	(setq backup t))))) ; loop end
550	484	;; done
551	485	list-resolvent))
552	486

560	494	(declare (type clause clause))
561	495	(when (= (the fixnum (num-literals clause)) 0)
562	496	(return-from hyper-resolution nil))
563		;;
564	497	(let ((resolvent-list nil)
565	498	(given-literals nil)
566	499	(clash-start nil)

586	519	last-clash nil
587	520	nuc-literals nil)
588	521	(dolist (lit (clause-literals clause))
589		b (cond ((or (positive-literal? lit) (answer-literal? lit))
	522	(cond ((or (positive-literal? lit) (answer-literal? lit))
590	523	(push lit nuc-literals))
591		;;
592	524	(t (let ((new-clash (make-clash :literal lit
593	525	:db clash-pos-literals)))
594	526	(declare (type clash new-clash))

600	532	(when (method-is-meta-demod (term-head (literal-atom lit)))
601	533	(setf (clash-evaluable new-clash) t))
602	534	(setq last-clash new-clash)))))
603		;;
604	535	(let ((res (hyper-clash! clash-start
605	536	nil ; subst
606	537	nuc-literals

612	543	nil)))
613	544	(when res
614	545	(setq resolvent-list (nconc res resolvent-list)))))
615		;;
616	546	(t
617		;;
618	547	;; given clause is a satellite.
619		;;
620	548	(dolist (l3 (clause-literals clause))
621	549	(declare (type literal l3))
622	550	(when (or (not (pn-flag order-hyper))

627	555	(unless (eq l3 lit)
628	556	(push lit given-literals)))
629	557	(let ((clashables
630		;; (get-literal-entry-from-atom clash-neg-literals
631		;; (literal-atom l3))
632		(is-fetch-concat (literal-atom l3) clash-neg-literals)
633		)
634		)
	558	(is-fetch-concat (literal-atom l3) clash-neg-literals)))
635	559	(dolist (lit-data clashables)
636	560	(block next
637		(let* (;; (nuc-lit (literal-entry-literal lit-data))
638		(nuc-lit lit-data)
	561	(let* ((nuc-lit lit-data)
639	562	(nuc (literal-clause (the literal nuc-lit))))
640	563	(when (not (positive-clause? nuc))
641	564	(multiple-value-bind (new-subst no-match e-equal)

644	567	nil)
645	568	(declare (ignore e-equal)
646	569	(type list new-subst))
647		;;
648	570	(when no-match (return-from next)) ; try next
649
650	571	;; found a nucleus
651	572	(setq nuc-literals nil)
652	573	(setq clash-start nil

691	612	resolvent-list)))
692	613	))))) ; block next
693	614	)) ; done for all possible clash
694		)
695		) ; done for all literals
696		)
697		)
	615	)) ; done for all literals
	616	)) ; end conditions
698	617	;; done
699	618	(when (pn-flag debug-hyper-res)
700	619	(with-output-simple-msg ()
701	620	(princ "End[hyper-res]")
702	621	(print-next)
703	622	(pr-clause-list resolvent-list)))
704		;;
705		(nreverse resolvent-list)
706		))
	623	(nreverse resolvent-list)))
707	624
708	625	;;; NEGATIVE HYPER RESOLUTION
709	626	;;; neg-hyper-resolution

716	633	(declare (type clause clause))
717	634	(when (= (the fixnum (num-literals clause)) 0)
718	635	(return-from neg-hyper-resolution nil))
719		;;
720	636	(let ((resolvent-list nil)
721	637	(given-literals nil)
722	638	(clash-start nil)

757	673	(when (method-is-meta-demod (term-head (literal-atom lit)))
758	674	(setf (clash-evaluable new-clash) t))
759	675	(setq last-clash new-clash)))))
760		;;
761	676	(let ((res (hyper-clash! clash-start
762	677	nil ; subst
763	678	nuc-literals

769	684	nil)))
770	685	(when res
771	686	(setq resolvent-list (nconc res resolvent-list)))))
772		;;
773	687	;; given clause is a sattelite.
774		;;
775	688	(t
776	689	(dolist (l3 (clause-literals clause))
777	690	(declare (type literal l3))

783	696	(unless (eq l3 lit)
784	697	(push lit given-literals)))
785	698	(let ((clashables
786		;; (get-literal-entry-from-atom clash-pos-literals
787		;; (literal-atom l3))
788		(is-fetch-concat (literal-atom l3) clash-pos-literals)
789		)
790		)
	699	(is-fetch-concat (literal-atom l3) clash-pos-literals)))
791	700	(dolist (lit-data clashables)
792	701	(block next
793	702	(let* (;; (nuc-lit (literal-entry-literal lit-data))

800	709	nil)
801	710	(declare (ignore e-equal)
802	711	(type list new-subst))
803		;;
804	712	(when no-match (return-from next)) ; try next
805
806	713	;; found a nucleus
807	714	(setq nuc-literals nil)
808	715	(setq clash-start nil

847	754	resolvent-list)))
848	755	))))) ; block next
849	756	)) ; done for all possible clash
850		)
851		) ; done for all literals
852		)
853		)
	757	)) ; done for all literals
	758	))
854	759	;; done
855	760	(when (pn-flag debug-hyper-res)
856	761	(with-output-simple-msg ()
857	762	(princ "End[neg-hyper-res]")
858	763	(print-next)
859	764	(pr-clause-list resolvent-list)))
860		;;
861		(nreverse resolvent-list)
862		))
	765	(nreverse resolvent-list)))
863	766
864	767	;;; UNIT RESULTING RESOLUTION
865	768	;;; ur-resolution

921	824	nil)))
922	825	(when res
923	826	(setq resolvent-list (nconc res resolvent-list))))
924		(pop nuc-literals))))
925		) ; end of case nucleus
926		;;
	827	(pop nuc-literals))))) ; end of case nucleus
927	828	(t ; given clause is satellite (unit).
928	829	;; collect any answer literal from given satellite
929	830	;; and get clashable literal (l3).

934	835	(progn
935	836	(push lit given-literals))))
936	837	(let ((clashables
937		#\|\|
938		(get-literal-entry-from-atom (if (positive-literal? l3)
939		clash-neg-literals
940		clash-pos-literals)
941		(literal-atom l3))
942		\|\|#
943	838	(is-fetch-concat (literal-atom l3)
944	839	(if (positive-literal? l3)
945	840	clash-neg-literals
946		clash-pos-literals))
947		))
	841	clash-pos-literals))))
948	842	(dolist (lit-data clashables)
949	843	(block next
950		(let* (;; (nuc-lit (literal-entry-literal lit-data))
951		(nuc-lit lit-data)
	844	(let* ((nuc-lit lit-data)
952	845	(nuc (literal-clause nuc-lit))
953	846	(nlits (num-literals nuc))
954	847	(new-subst nil)
955	848	(no-match nil)
956	849	(e-equal nil))
957		(declare (ignore e-equal))
958	850	(when (> nlits 1)
959	851	(multiple-value-setq (new-subst no-match e-equal)
960	852	(unify (literal-atom l3)

999	891	(setq c1 (clash-next c1))
1000	892	(incf j))
1001	893	(when (eq lit nuc-lit)
1002		(setq nuc-pos j))
1003		)
	894	(setq nuc-pos j)))
1004	895	(unless (null c1)
1005	896	(princ c1)
1006	897	(break "aho!")

1014	905	clause
1015	906	#'unit-clause?
1016	907	:ur-res
1017		nuc-pos))
1018		)
	908	nuc-pos)))
1019	909	(when res
1020	910	(setq resolvent-list
1021	911	(nconc res resolvent-list)))

1025	915	)) ; done for all possible clash
1026	916	) ; end case of satelite
1027	917	))
1028		(nreverse resolvent-list)
1029		))
	918	(nreverse resolvent-list)))
1030	919
1031	920
1032	921	;;; BUILD-BIN-RES : Literal1 Literal2 Subst -> Clause

1051	940	(setq new-literal (shallow-copy-literal lit new-clause))
1052	941	(setf (literal-atom new-literal)
1053	942	(apply-subst subst (literal-atom lit)))
1054		(push new-literal new-literals))))
1055		))
	943	(push new-literal new-literals))))))
1056	944	(make-bin-res l1)
1057	945	(make-bin-res l2)
1058	946	(setf (clause-literals new-clause) new-literals)

1062	950	:binary-res-rule)
1063	951	(clause-id (literal-clause l1))
1064	952	(clause-id (literal-clause l2)))))
1065		new-clause
1066		)))
	953	new-clause)))
1067	954
1068	955	;;; BINARY RESOLUTION
1069	956	;;; binary-resolution

1121	1008	(print-next)
1122	1009	(format t "clash = ")
1123	1010	(print-clause (literal-clause
1124		;; (literal-entry-literal lit-data)
1125	1011	lit-data
1126	1012	))
1127	1013	(print-next)
1128	1014	(princ "subst = ")
1129		(print-substitution new-subst)
1130		))
1131		;;
	1015	(print-substitution new-subst)))
1132	1016	(setq resolvent
1133	1017	(build-bin-res lit
1134	1018	;; (literal-entry-literal lit-data)

1146	1030	(let ((pre-res nil))
1147	1031	(setq pre-res (pre-process resolvent nil :sos))
1148	1032	(when pre-res
1149		(push resolvent resolvent-list)))
1150		))))
1151		))))
	1033	(push resolvent resolvent-list)))))))))))
1152	1034	) ; block next
1153	1035	) ; end do
1154	1036	;;

1157	1039	(princ "End[binary-res]")
1158	1040	(dolist (x (reverse resolvent-list))
1159	1041	(print-next)
1160		(print-clause x))
1161		))
1162		;;
	1042	(print-clause x))))
1163	1043	(nreverse resolvent-list)))
1164	1044
1165	1045	;;; =========

1206	1086	(return-from found t)))
1207	1087	(setf (factor-l2p f-struct)
1208	1088	(cdr (factor-l2p f-struct)))))
1209		;;
1210	1089	(setf (factor-l1p f-struct) (cdr (factor-l1p f-struct)))
1211	1090	(setf (factor-l2p f-struct) (factor-l1p f-struct)))
1212	1091	;; failed
1213		nil
1214		))
1215		;;
	1092	nil))
1216	1093	(when factored
1217	1094	(let* ((lit2 (car (factor-l2p f-struct))) ; clause to be excluded
1218		(clause (factor-clause f-struct))
1219		;;(new-vars-list (make-var-mapping (clause-variables clause)))
1220		)
	1095	(clause (factor-clause f-struct)))
1221	1096	(declare (type literal lit2)
1222	1097	(type clause clause))
1223	1098	(setq a-factor

1237	1112	oriented-eq-bit)
1238	1113	(set-bit (literal-stat-bits new-lit)
1239	1114	oriented-eq-bit))
1240		new-lit))
1241		)))
1242		))
1243		;;
	1115	new-lit)))))))
1244	1116	(when (pn-flag debug-infer)
1245	1117	(when a-factor
1246	1118	(with-output-simple-msg ()
1247	1119	(princ "*FACTOR: ")
1248	1120	(print-clause a-factor))))
1249		;;
1250	1121	a-factor))
1251	1122
1252	1123	;;; GET-FACTORS : Clause -> List[Clause]

1270	1141	(type list subst))
1271	1142	(unless no-match
1272	1143	(let ((a-factor (make-clause-shallow-copy clause
1273		(list lit2)))
1274		;; (new-vars-list (make-var-mapping (clause-variables clause)))
1275		)
	1144	(list lit2))))
1276	1145	(declare (type clause a-factor))
1277	1146	(setq a-factor (copy-clause
1278	1147	a-factor

1287	1156	oriented-eq-bit)
1288	1157	(set-bit (literal-stat-bits new-lit)
1289	1158	oriented-eq-bit))
1290		new-lit))
1291		))
	1159	new-lit))))
1292	1160	(push (cl-unique-variables a-factor) factors)))))))
1293	1161	(nreverse factors)))
1294	1162

1306	1174	(list (list :factor-rule (clause-id clause))))
1307	1175	(incf (pn-stat cl-generated))
1308	1176	(incf (pn-stat factor-gen))
1309		(pre-process a-factor nil list))
1310		))
	1177	(pre-process a-factor nil list))))
1311	1178
1312	1179	;;; FACTOR-SIMPLIFY : Clause -> fixnum
1313	1180	;;;
1314
1315	1181	(defun factor-simplify (clause)
1316	1182	(declare (type clause clause)
1317	1183	(values (or null fixnum)))

1319	1185	:l1p (clause-literals clause)
1320	1186	:l2p (clause-literals clause)))
1321	1187	(num 0)
1322		(a-factor nil)
1323		)
	1188	(a-factor nil))
1324	1189	(declare (type fixnum num)
1325	1190	(type factor f-struct)
1326	1191	(type (or null clause) a-factor))

1338	1203	(setf (literal-clause l) a-factor))
1339	1204	(dolist (l (clause-literals clause))
1340	1205	(setf (literal-clause l) clause))
1341		#\|\|
1342		(setf (clause-parents clause)
1343		(nconc (clause-parents clause)
1344		(list (list :factor-simp-rule (clause-id a-factor)))))
1345		\|\|#
1346	1206	(setf (clause-parents clause)
1347	1207	(nconc (clause-parents clause)
1348	1208	(list (list :factor-simp-rule))))
1349		;;
1350	1209	(delete-clause a-factor current-psys)
1351		;;
1352	1210	(setf (factor-l1p f-struct) (clause-literals clause)
1353	1211	(factor-l2p f-struct) (clause-literals clause))
1354		(setq a-factor (next-factor f-struct))
1355		)
1356		;; cl_del_non(factor)
	1212	(setq a-factor (next-factor f-struct)))
1357	1213	(progn
1358	1214	(delete-clause a-factor current-psys)
1359		(setq a-factor (next-factor f-struct)))
1360		))
1361		;;
	1215	(setq a-factor (next-factor f-struct)))))
1362	1216	num ))
1363	1217
1364	1218

+56

-56

cafeobj/oldoc.lisp less more

135	135	;; . otherwise do substring matching
136	136	;; . if all the matches in the previous loop returned true, flag it
137	137	;; . list all the flagged functions, or say no match
138
139		;;
140		;; TOPLEVEL entry functions
141		;;
142		;; the following functions are called from the toplevel evaluation loop
143		;; in particular when one of the ? commands, and gendoc is called.
144		;
145		; oldoc-get-documentation
146		; returns the formatted string for display on the console
147		; returns nil if nothing found
148		(defun oldoc-get-documentation (question &key (main t) (example nil) (apropos nil) (related t))
149		(if apropos
150		(oldoc-search-all question)
151		(let ((doc (oldoc-find-doc-entry question)))
152		(if (not (listp doc))
153		(oldoc-format-documentation doc :raw nil :main main :example example :related related)
154		(progn
155		(if doc
156		(format t "Did you mean one of ~a~%" doc))
157		nil)))))
158
159		;; oldoc-list-categories
160		;;
161		(declaim (special .category-descriptions. .valid-com-categories.))
162
163		(defun oldoc-list-categories (cat)
164		(unless cat
165		(format t "** ======================================================================~%")
166		(format t "COMMAND CLASSES:~%")
167		(format t "'?com <class>' shows the list of commands classified by <class>.~2%")
168		(format t "class~10Tdescription~%")
169		(format t "-------------------------------------------------------------------------~%")
170		(dolist (entry .category-descriptions.)
171		(format t "~a~10T~a~%" (first entry) (second entry)))
172		(return-from oldoc-list-categories nil))
173		;; gather commands
174		(unless (member (car cat) .valid-com-categories.
175		:test #'(lambda (x y) (string-equal x (symbol-name y))))
176		(with-output-chaos-error ('invalid-category)
177		(format t "System does not know the command class '~a'.~%" (car cat))
178		(format t "Type '?cat' for the list of available class names.")))
179		(let ((docs (oldoc-get-documents-by-category (car cat))))
180		(unless docs
181		(with-output-chaos-warning ()
182		(format t "Sorry, the commands classified as '~a' not found." (car cat)))
183		(return-from oldoc-list-categories nil))
184		(format t "The list of commands classified as '~a'.~%" (car cat))
185		(format t "Type '? <command-name>' for the online document of <command-name>.~%")
186		(format t "==========================================================================")
187		(do* ((dl docs (cdr dl))
188		(doc (car dl) (car dl))
189		(n 0 (1+ n)))
190		((endp dl))
191		(let ((key (car doc))
192		(desc (cdr doc)))
193		(format t "~%~a~% ~a" key (format-markdown (oldoc-title desc)))))))
194	138
195	139	;;
196	140	;; INTERNAL functioons

537	481	cafeobj-doc-db)
538	482	(sort coms #'ob< :key #'car)))
539	483
	484	;;
	485	;; TOPLEVEL entry functions
	486	;;
	487	;; the following functions are called from the toplevel evaluation loop
	488	;; in particular when one of the ? commands, and gendoc is called.
	489	;
	490	; oldoc-get-documentation
	491	; returns the formatted string for display on the console
	492	; returns nil if nothing found
	493	(defun oldoc-get-documentation (question &key (main t) (example nil) (apropos nil) (related t))
	494	(if apropos
	495	(oldoc-search-all question)
	496	(let ((doc (oldoc-find-doc-entry question)))
	497	(if (not (listp doc))
	498	(oldoc-format-documentation doc :raw nil :main main :example example :related related)
	499	(progn
	500	(if doc
	501	(format t "Did you mean one of ~a~%" doc))
	502	nil)))))
	503
	504	;; oldoc-list-categories
	505	;;
	506	(declaim (special .category-descriptions. .valid-com-categories.))
	507
	508	(defun oldoc-list-categories (cat)
	509	(unless cat
	510	(format t "** ======================================================================~%")
	511	(format t "COMMAND CLASSES:~%")
	512	(format t "'?com <class>' shows the list of commands classified by <class>.~2%")
	513	(format t "class~10Tdescription~%")
	514	(format t "-------------------------------------------------------------------------~%")
	515	(dolist (entry .category-descriptions.)
	516	(format t "~a~10T~a~%" (first entry) (second entry)))
	517	(return-from oldoc-list-categories nil))
	518	;; gather commands
	519	(unless (member (car cat) .valid-com-categories.
	520	:test #'(lambda (x y) (string-equal x (symbol-name y))))
	521	(with-output-chaos-error ('invalid-category)
	522	(format t "System does not know the command class '~a'.~%" (car cat))
	523	(format t "Type '?cat' for the list of available class names.")))
	524	(let ((docs (oldoc-get-documents-by-category (car cat))))
	525	(unless docs
	526	(with-output-chaos-warning ()
	527	(format t "Sorry, the commands classified as '~a' not found." (car cat)))
	528	(return-from oldoc-list-categories nil))
	529	(format t "The list of commands classified as '~a'.~%" (car cat))
	530	(format t "Type '? <command-name>' for the online document of <command-name>.~%")
	531	(format t "==========================================================================")
	532	(do* ((dl docs (cdr dl))
	533	(doc (car dl) (car dl))
	534	(n 0 (1+ n)))
	535	((endp dl))
	536	(let ((key (car doc))
	537	(desc (cdr doc)))
	538	(format t "~%~a~% ~a" key (format-markdown (oldoc-title desc)))))))
	539
540	540	;;; EOF

-26

chaos/cafein/reducer.lisp less more

41	41	;;; REDUCER
42	42	;;; provides term rewriting eclosed within computing environment.
43	43	;;; ========
44		(declaim (inline begin-parse end-parse time-for-parsing-in-seconds
45		begin-rewrite end-rewrite time-for-rewriting-in-seconds
46		number-metches number-rewritings number-memo-hits
47		clear-rewriting-fc prepare-term reset-rewrite-counters
48		prepare-reduction-env reducer reducer-no-stat
49		number-hash-size))
50
51
52	44	(let ((m-pattern-subst nil)
53	45	(.rwl-context-stack. nil)
54	46	(.rwl-states-so-far. 0)

96	88	(type integer parse-begin-time rewrite-begin-time)
97	89	(type float time-for-parsing time-for-rewriting))
98	90
99		(declaim (inline reset-parse-time))
100	91	(defun reset-parse-time ()
101	92	(setf time-for-parsing 0.0))
102	93
103		(declaim (inline bgin-parse))
104	94	(defun begin-parse ()
105	95	(setf parse-begin-time (get-internal-run-time)))
106	96
107		(declaim (inline end-parse))
108	97	(defun end-parse ()
109	98	(setf time-for-parsing (elapsed-time-in-seconds parse-begin-time
110	99	(get-internal-run-time))))
111	100
112		(declaim (inline time-for-parsing-in-seconds))
113	101	(defun time-for-parsing-in-seconds ()
114	102	time-for-parsing)
115	103
116		(declaim (inline begin-rewrite))
117	104	(defun begin-rewrite ()
118	105	(setf rewrite-begin-time (get-internal-run-time)))
119	106
120		(declaim (inline end-rewrite))
121	107	(defun end-rewrite ()
122	108	(setf time-for-rewriting (elapsed-time-in-seconds rewrite-begin-time
123	109	(get-internal-run-time))))
124	110
125		(declaim (inline time-for-rewriting-in-seconds))
126	111	(defun time-for-rewriting-in-seconds ()
127	112	time-for-rewriting)
128	113
129		(declaim (inline number-matches))
130	114	(defun number-matches ()
131	115	$$matches)
132	116
133		(declaim (inline number-rewritings))
134	117	(defun number-rewritings ()
135	118	rule-count)
136	119
137		(declaim (inline number-memo-hits))
138	120	(defun number-memo-hits ()
139	121	term-memo-hash-hit)
140	122
141		(declaim (inline number-hash-size))
142	123	(defun number-hash-size ()
143	124	(declare (inline hash-table-count))
144	125	;; .hash-size.
145	126	(hash-table-count term-memo-table))
146		;;
147		(declaim (inline clear-rewriting-fc))
	127
148	128	(defun clear-rewriting-fc (module mode)
149	129	(setf m-pattern-subst nil
150	130	.rwl-context-stack. nil

183	163
184	164	;; reset-rewrite-counters
185	165	;; initialize rewriting counters.
186		(declaim (inline reset-rewrite-counters))
187	166	(defun reset-rewrite-counters ()
188	167	(setf $$matches 0
189	168	rule-count 0
190	169	term-memo-hash-hit 0))
191	170
192	171	;; reset-term-memo-table
193		(declaim (inline reset-term-memo-table))
194	172	(defun reset-term-memo-table (module)
195	173	(when (or clean-memo-in-normalize
196	174	(not (eq module memoized-module)))

200	178	;; prepare-reduction-env
201	179	;; all-in-one proc for setting up environment variables for rewriting,
202	180	;; returns evaluated 'context-module'.
203		(declaim (inline prepare-reduction-env))
204	181	(defun prepare-reduction-env (term context-module mode stat-reset)
205	182	(let ((module (if (module-p context-module)
206	183	context-module

221	198	module))
222	199
223	200	;; generate-statistics-form
224		(declaim (inline geneate-statistics-form))
225	201	(defun generate-statistics-form ()
226	202	(let ((stat-form ""))
227	203	(declare (type string stat-form))

239	215	;; (number-hash-size)
240	216	)))))
241	217
242		(declaim (inline generate-statistics-form-rewriting-only))
243	218	(defun generate-statistics-form-rewriting-only ()
244	219	(let ((stat-form ""))
245	220	(declare (type string stat-form))

-1

chaos/primitives/bsort.lisp less more

186	186	(stream stream)
187	187	(ignore ignore))
188	188	(if (sort-is-hidden obj)
189		(format stream ":hsort[~a.a]" (sort-id obj) (module-print-name (object-context-mod obj)))
	189	(format stream ":hsort[~a.~a]" (sort-id obj) (module-print-name (object-context-mod obj)))
190	190	(format stream ":sort[~a.~a]" (sort-id obj) (module-print-name (object-context-mod obj)))))
191	191
192	192	;;; Constructor ----------------------------------------------------------------

-610

~~chaos/primitives/substitution.lisp~~ less more

0		;;;-- Mode:LISP; Package:CHAOS; Base:10; Syntax:Common-lisp --
1		;;;
2		;;; Copyright (c) 2000-2015, Toshimi Sawada. All rights reserved.
3		;;;
4		;;; Redistribution and use in source and binary forms, with or without
5		;;; modification, are permitted provided that the following conditions
6		;;; are met:
7		;;;
8		;;; * Redistributions of source code must retain the above copyright
9		;;; notice, this list of conditions and the following disclaimer.
10		;;;
11		;;; * Redistributions in binary form must reproduce the above
12		;;; copyright notice, this list of conditions and the following
13		;;; disclaimer in the documentation and/or other materials
14		;;; provided with the distribution.
15		;;;
16		;;; THIS SOFTWARE IS PROVIDED BY THE AUTHOR 'AS IS' AND ANY EXPRESSED
17		;;; OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
18		;;; WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
19		;;; ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
20		;;; DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
21		;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
22		;;; GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
23		;;; INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
24		;;; WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
25		;;; NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
26		;;; SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27		;;;
28		(in-package :chaos)
29		#\|==============================================================================
30		System: Chaos
31		Module: primitives
32		File: substitution.lisp
33		==============================================================================\|#
34		#-:chaos-debug
35		(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
36		#+:chaos-debug
37		(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
38
39		#\|
40		SUBSTITUTION
41		--------------------------------------------------------------------------------
42		A substitution is a map from variables to terms. Any mapping \sigma of variables
43		to terms extends to a substitution by defining \sigma(f(t1,...,tn)) to be
44		f(\sigma(t1), ... , \sigma(tn)).
45
46		IMPLEMENTATION:
47		this is naturally an association list of (varible . term) pair, and we want it
48		to be mutable, then we implemented as a structure of type list.
49		--------------------------------------------------------------------------------
50		\|#
51
52		(deftype substitution () 'list)
53		(defmacro substitution-create (_bind) _bind)
54		(defmacro substitution-bindings (_sub) _sub)
55		(defmacro assoc-in-substitution (_key _sub &optional (_test '#'variable-eq))
56		`(assoc ,_key ,_sub :test ,_test))
57
58		;;; CREATE-EMPTY-SUBSTITUTION
59		;;; Creates new empty substitution
60		;;;
61		(defmacro create-empty-substitution () `())
62		(declaim (inline new-substitution))
63		(defun new-substitution () ())
64
65		;;; SUBSTITUTION-COPY sigma
66		;;; Returns a copy of sigma.
67		;;;
68		(defmacro substitution-copy (_sigma)
69		` (mapcar #'(lambda (map)
70		(cons (car map) (cdr map)))
71		,_sigma))
72
73		;;; SUBSTITUTION-IS-EMPTY sigma
74		;;; Returns t iff \sigma is an empty substitution-
75		;;;
76		(defmacro substitution-is-empty (sigma_) `(null ,sigma_))
77
78		;;; SUBSTITUTION-DOMAIN sigma
79		;;; Returns the domain of sigma
80		;;;
81		(defmacro substitution-domain (_sigma_) `(mapcar #'car ,_sigma_))
82
83		;;; VARIABLE-IMAGE
84		;;; returns the image of variable under sigma.
85		;;;
86		(defmacro variable-image (_sigma _variable)
87		`(cdr (assoc ,_variable ,_sigma :test #'variable-eq)))
88
89		(defmacro variable-image-fast (_sigma _variable)
90		`(cdr (assoc ,_variable ,_sigma :test #'eq)))
91
92		(defmacro variable-image-slow (_sigma _variable)
93		`(cdr (assoc ,_variable ,_sigma :test #'variable-equal)))
94
95		;;; SUBSTITUTION-LIST-OF-PAIRS sigma
96		;;; returns the list of pair in substitution-
97		;;;
98		(defmacro substitution-list-of-pairs (_sigma_) _sigma_)
99
100		;;; SUBSTITUTION-ADD sigma variable term
101		;;; adds the new map variable -> term to sigma.
102		;;;
103		(defmacro substitution-add (sigma_* variable_* term_*)
104		`(cons (cons ,variable_* ,term_) ,sigma_))
105
106		;;; SUBSTITUTION-DELETE sigma variable
107		;;; deletes the map for variable from sigma.
108		;;; NOTE: sigma is modified.
109		;;;
110		(defmacro substitution-delete (sigma!_ variable!_)
111		(once-only (sigma!_)
112		` (progn (setf ,sigma!_
113		(delete ,variable!_ ,sigma!_ :test #'variable-eq))
114		,sigma!_)))
115
116		;;; SUBSTITUTION-CHANGE sigma variable term
117		;;; change the mapping of variable to term.
118		;;; if the variable is not in the domain of sigma, add the new binding.
119		;;; NOTE: sigma is modified.
120		;;;
121		(defmacro substitution-change (?__sigma ?__variable ?__term)
122		(once-only (?__sigma ?__variable ?__term)
123		` (let ((binding (assoc-in-substitution ,?__variable ,?__sigma)))
124		(if binding
125		(setf (cdr binding) ,?__term)
126		(push (cons variable ,?__term) ?__sigma))
127		,?__sigma)))
128
129		;;; SUBSTITUTION-SET sigma variable term
130		;;; Changes sigma to map v to term.
131		;;;
132		(defmacro substitution-set (?_?sigma ?_?v ?_?term)
133		(once-only (?_?sigma ?_?v ?_?term)
134		`(progn
135		(if (variable-eq ,?_?v ,?_?term)
136		(substitution-delete ,?_?sigma ,?_?v)
137		(substitution-change ,?_?sigma ,?_?v ,?_?term))
138		,?_?sigma)))
139
140		;;; CANONICALIZE-SUBSTITUTION : substitution -> substitution
141		;;;
142		(defun canonicalize-substitution (s)
143		(declare (type list s)
144		(optimize (speed 3) (safety 0))
145		(values list))
146		(sort (copy-list s) ; (substitution-copy s)
147		#'(lambda (x y) ; two substitution items (var . term)
148		(string< (the simple-string (string (variable-name (car x))))
149		(the simple-string (string (variable-name (car y))))))))
150
151
152		;;; SUBSTITUTION-EQUAL : substitution1 substitution2 -> Bool
153		;;;
154		(defun substitution-equal (s1 s2)
155		(declare (type list s1 s2)
156		(optimize (speed 3) (safety 0))
157		(values (or null t)))
158		(every2len #'(lambda (x y)
159		(and (variable= (the term (car x)) (the term (car y)))
160		(term-is-similar? (the term (cdr x)) (the term (cdr y)))))
161		s1 s2))
162
163		;;; SUBSTITUTION-RESTRICT : list-of-variables substitution -> substitution
164		;;;
165		(defun substitution-restrict (vars sub)
166		(declare (type list vars sub)
167		(optimize (speed 3) (safety 0))
168		(values list))
169		(let ((res nil))
170		(dolist (s sub)
171		(when (member (car s) vars)
172		(push s res)))
173		res))
174
175		;;; SUBSTITUTION-SUBSET substitution-1 substitution-2 : -> bool
176		;;; subset when viewed as a set of (mapping) pairs
177		;;; assumed canonicalized
178		;;;
179		(defun substitution-subset (s1 s2)
180		(declare (type list s1 s2)
181		(optimize (speed 3) (safety 0)))
182		(substitution-subset-list (substitution-list-of-pairs s1)
183		(substitution-list-of-pairs s2)))
184		(defun substitution-subset-list (s1 s2)
185		(declare (type list s1 s2)
186		(optimize (speed 3) (safety 0))
187		(values (or null t)))
188		(let ((s1x s1)
189		(s2x s2)
190		(res t))
191		(loop (when (null s1x) (return))
192		(let ((v1 (the term (caar s1x)))
193		(t1 (the term (cdar s1x))))
194		(loop (when (null s2x) (setq res nil) (return))
195		(when (variable-eq v1 (caar s2x))
196		(if (term-is-similar? t1 (cdar s2x))
197		(progn (setq s2x (cdr s2x)) (return))
198		(progn (setq res nil) (return))))
199		(setq s2x (cdr s2x)))
200		(when (null res) (return))
201		(setq s1x (cdr s1x))))
202		res))
203
204
205		;;; SUBSTITUTION-DOMAIN-RESTRICTION sigma domain
206		;;; Restricts the domain of sigma to dom and renames in a canonical fashion all
207		;;; variables in the range of sigma, but not in domain. More precisely, returns
208		;;; a substitution sigma2 with domain a subset of domain such that, for any
209		;;; variable v in domain, \sigma2(v) = \rho(\sigma(v)), where \rho is a substitution
210		;;; that renames variables.
211		;;;
212		;;; TODO
213		(defun substitution-domain-restriction (sigma domain)
214		sigma domain
215		)
216
217		;;; SUBSTITUTION-UNION sigma1 sigma2
218		;;; Returns the union of \sigma1 nd \sigma2. Returns 'incompatible if
219		;;; \sigma1(v) differs from \sigma2(v) for some v in the intersection of their
220		;;; domains.
221		;;;
222		;;; TODO
223		(defun substitution-union (sigma1 sigma2)
224		sigma1 sigma2
225		)
226
227		;;; SUBSTITUTION-COMPOSIT sigma1 sigma2
228		;;; Returns the composition of \sigma1 and \sigma2. The result of applying this
229		;;; composition to a term t is \sigma1(\sigma2(t)).
230		;;; NOTE: This operation is NOT commutative,
231		;;; i,e. substitution-composit(sigma, sigma) =/= sigma.
232		;;;
233		(defun substitution-composit (sigma1 sigma2)
234		sigma1 sigma2
235		)
236
237		;;; SUBSTITUTION-FOREACH (element sigma) body
238		;;; Yields the variable-term pairs in sigma
239		;;;
240		(defmacro substitution-foreach ((?_??element ?_??sigma) &body ?_??body)
241		`(dolist (,?_??element (substitution-bindings ,?_??sigma))
242		,@?_??body)
243		)
244
245		;;; SUBSTITUTION-IMAGE
246		;;; Returns sigma(t) and "true" iff the sort of "t" and "sigma(t)" are the same.
247		;;; A COPY of the term "t" is done and the sort information is updated.
248		;;;
249		(defun substitution-image (sigma term)
250		(declare (type list sigma)
251		(optimize (speed 3) (safety 0))
252		(type term term))
253		(let ((consider-object t))
254		(cond ((term-is-variable? term)
255		(let ((im (variable-image sigma term)))
256		(if im;; i.e. im = sigma(term)
257		(values im nil)
258		(values term t))))
259		((term-is-lisp-form? term)
260		(multiple-value-bind (new-term success)
261		(funcall (lisp-form-function term) sigma)
262		(if success
263		new-term
264		(throw 'rule-failure :fail-builtin))))
265		((term-is-chaos-expr? term)
266		(multiple-value-bind (new-term success)
267		(funcall (chaos-form-expr term) sigma)
268		(if success
269		new-term
270		(throw 'fule-failure :fail-builtin))))
271		((term-is-builtin-constant? term)
272		term) ; shold we copy?
273		(t (let ((l-result nil)
274		(modif-sort nil))
275		(dolist (s-t (term-subterms term))
276		(multiple-value-bind (image-s-t same-sort)
277		(substitution-image sigma s-t)
278		(unless same-sort (setq modif-sort t))
279		(push image-s-t l-result)))
280		(setq l-result (nreverse l-result))
281		(if modif-sort
282		(let ((term-image (make-term-with-sort-check (term-head term)
283		l-result)))
284		(values term-image
285		(sort= (term-sort term)
286		(term-sort term-image))))
287		(values (make-applform (term-sort term)
288		(term-head term)
289		l-result)
290		t)))))))
291
292		(defun substitution-image! (sigma term)
293		(declare (type list sigma)
294		(optimize (speed 3) (safety 0))
295		(type term term))
296		(let ((consider-object t))
297		(cond ((term-is-variable? term)
298		(let ((im (variable-image-slow sigma term)))
299		(if im;; i.e. im = sigma(term)
300		(values im nil)
301		(values term t))))
302		((term-is-lisp-form? term)
303		(multiple-value-bind (new-term success)
304		(funcall (lisp-form-function term) sigma)
305		(if success
306		new-term
307		(throw 'rule-failure :fail-builtin))))
308		((term-is-chaos-expr? term)
309		(multiple-value-bind (new-term success)
310		(funcall (chaos-form-expr term) sigma)
311		(if success
312		new-term
313		(throw 'fule-failure :fail-builtin))))
314		((term-is-builtin-constant? term) term) ; shold we copy?
315		(t (let ((l-result nil)
316		(modif-sort nil))
317		(dolist (s-t (term-subterms term))
318		(multiple-value-bind (image-s-t same-sort)
319		(substitution-image! sigma s-t)
320		(unless same-sort (setq modif-sort t))
321		(push image-s-t l-result)))
322		(setq l-result (nreverse l-result))
323		(if modif-sort
324		(let ((term-image (make-term-with-sort-check (term-head term)
325		l-result)))
326		(values term-image
327		(sort= (term-sort term)
328		(term-sort term-image))))
329		(values (make-applform (term-sort term)
330		(term-head term)
331		l-result)
332		t)))))))
333
334		(defun substitution-image-cp (sigma term)
335		(declare (type list sigma)
336		(optimize (speed 3) (safety 0))
337		(type term term))
338		(let ((consider-object t))
339		(cond ((term-is-variable? term)
340		(let ((im (variable-image sigma term)))
341		(if im;; i.e. im = sigma(term)
342		;; (values (simple-copy-term im) nil)
343		(values im nil)
344		(values term t))))
345		((term-is-lisp-form? term)
346		(multiple-value-bind (new-term success)
347		(funcall (lisp-form-function term) sigma)
348		(if success
349		new-term
350		(throw 'rule-failure :fail-builtin))))
351		((term-is-chaos-expr? term)
352		(multiple-value-bind (new-term success)
353		(funcall (chaos-form-expr term) sigma)
354		(if success
355		new-term
356		(throw 'fule-failure :fail-builtin))))
357		((term-is-builtin-constant? term) term) ; shold we copy?
358		(t (let ((l-result nil)
359		(modif-sort nil))
360		(dolist (s-t (term-subterms term))
361		(multiple-value-bind (image-s-t same-sort)
362		(substitution-image-cp sigma s-t)
363		(unless same-sort (setq modif-sort t))
364		(push image-s-t l-result)))
365		(setq l-result (nreverse l-result))
366		(if modif-sort
367		(let ((term-image (make-term-with-sort-check (term-head term)
368		l-result)))
369		(values term-image
370		(sort= (term-sort term)
371		(term-sort term-image))))
372		(values (make-applform (term-sort term)
373		(term-head term)
374		l-result)
375		t)))))))
376
377		(defun substitution-check-built-in (trm) trm)
378
379		;;; SUBSTITUTION-COMPOSE
380
381		(defun substitution-compose (teta lisp-term)
382		(declare (type list teta lisp-term)
383		(optimize (speed 3) (safety 0)))
384		(let ((fcn (lisp-form-function lisp-term))
385		(new-fun nil)
386		(new-term nil))
387		(if (or #-CMU(typep fcn 'compiled-function)
388		#+CMU(typep fcn 'function)
389		(not (and (consp fcn) (eq 'lambda (car fcn))
390		(equal '(compn) (cadr fcn)))))
391		(setf new-fun
392		`(lambda (compn) (funcall ',fcn (append ',teta compn))))
393		(let ((oldteta (cadr (nth 1 (nth 2 (nth 2 fcn)))))
394		(realfcn (cadr (nth 1 (nth 2 fcn)))))
395		(setf new-fun
396		`(lambda (compn)
397		(funcall ',realfcn (append ',(append teta oldteta) compn))))))
398		(if (term-is-simple-lisp-form? lisp-term)
399		(setf new-term (make-simple-lisp-form-term (lisp-form-original-form lisp-term)))
400		(setf new-term (make-general-lisp-form-term (lisp-form-original-form lisp-term))))
401		(setf (lisp-form-function new-term) new-fun)
402		new-term))
403
404		(defun substitution-compose-chaos (teta chaos-expr)
405		(declare (type list teta chaos-expr)
406		(optimize (speed 3) (safety 0)))
407		(let ((fcn (chaos-form-expr chaos-expr))
408		(new-fun nil)
409		(new-term nil))
410		(if (or #-CMU(typep fcn 'compiled-function)
411		#+CMU(typep fcn 'function)
412		(not (and (consp fcn) (eq 'lambda (car fcn))
413		(equal '(compn) (cadr fcn)))))
414		(setf new-fun
415		`(lambda (compn) (funcall ',fcn (append ',teta compn))))
416		(let ((oldteta (cadr (nth 1 (nth 2 (nth 2 fcn)))))
417		(realfcn (cadr (nth 1 (nth 2 fcn)))))
418		(setf new-fun
419		`(lambda (compn)
420		(funcall ',realfcn (append ',(append teta oldteta) compn))))))
421		(setf new-term (make-bconst-term chaos-value-sort
422		(list '\|%Chaos\|
423		new-fun
424		(chaos-original-expr chaos-expr))))
425		new-term))
426
427		;;; SUBSTITUTION-IMAGE* sigma term
428		;;; Returns the image of term under sigma. Like substitution-image, but
429		;;; changing bound variables as necessary in the result to prevent variables in the
430		;;; range of sigma from being captured by a quantifier in term. Also renames all bound
431		;;; variables in the image of term under sigma (by replacing them by constants).
432		;;; To preserve shared subterms, returns t itself, and not a copy, if the image is the
433		;;; same as t.
434		;;; * TODO *
435		;;;
436
437		;; NO COPY of Term is done.
438		(defun substitution-image-no-copy (sigma term &optional (subst-pconst nil))
439		(declare (type list sigma)
440		(type term term)
441		(optimize (speed 3) (safety 0))
442		(values t))
443		(let ((im nil))
444		;; '-image-slow' because the use case often distructively changes terms.
445		(cond ((term-is-variable? term)
446		(when (setq im (variable-image-slow sigma term))
447		(term-replace term im)))
448		((term-is-constant? term)
449		(when subst-pconst
450		(when (setq im (variable-image-slow sigma term))
451		(term-replace term im))))
452		(t (dolist (s-t (term-subterms term))
453		(substitution-image-no-copy sigma s-t subst-pconst))))
454		term))
455
456		(defun substitution-partial-image (sigma term)
457		(declare (type list sigma)
458		(type term term)
459		(optimize (speed 3) (safety 0)))
460		(let ((consider-object t))
461		(cond ((term-is-variable? term)
462		(let ((im (variable-image sigma term)))
463		(if im
464		(values im nil)
465		(values term t))))
466		((term-is-lisp-form? term)
467		(substitution-compose sigma term)
468		)
469		((term-is-chaos-expr? term)
470		(substitution-compose-chaos sigma term))
471		((term-is-builtin-constant? term) term)
472		((term-is-applform? term)
473		(let ((l-result nil) (modif-sort nil))
474		(dolist (s-t (term-subterms term))
475		(multiple-value-bind (image-s-t same-sort)
476		(substitution-partial-image sigma s-t)
477		(unless same-sort (setq modif-sort t))
478		(push image-s-t l-result)))
479		(setq l-result (nreverse l-result))
480		(if modif-sort
481		(let ((term-image (make-term-with-sort-check
482		(term-head term)
483		l-result)))
484		(values term-image
485		(sort= (term-sort term)
486		(term-sort term-image))))
487		(values (make-applform (term-sort term) (term-head term) l-result)
488		t))))
489		(t (break "substution-partial-image : not implemented ~s" term))
490		)))
491
492		(defun substitution-image-simplifying (sigma term &optional (cp nil) (slow-map nil))
493		(declare (type list sigma)
494		(type term)
495		(optimize (speed 3) (safety 0)))
496		(let ((consider-object t))
497		;; (setq subst-debug-term term)
498		(cond ((term-is-variable? term)
499		(let ((im (if slow-map
500		(variable-image-slow sigma term)
501		(variable-image sigma term))))
502		(if im
503		(values (if cp
504		(progn
505		;; debug
506		;; (format t "~&copying " (term-print im))
507		(simple-copy-term im))
508		im)
509		(sort= (variable-sort term)
510		(term-sort im)))
511		(values term t))))
512		((term-is-chaos-expr? term)
513		(when rewrite-debug
514		(format t "CHAOS: ~S" (chaos-form-expr term)))
515		(multiple-value-bind (new-term success)
516		(funcall (chaos-form-expr term) sigma)
517		(if success
518		new-term
519		(throw 'fule-failure :fail-builtin))))
520		((term-is-builtin-constant? term) term)
521		((term-is-lisp-form? term)
522		(multiple-value-bind (new success)
523		(funcall (lisp-form-function term) sigma)
524		(if success
525		new
526		(throw 'rule-failure :fail-builtin))))
527		((term-is-applform? term)
528		(let ((l-result nil)
529		(modif-sort nil))
530		(dolist (s-t (term-subterms term))
531		(multiple-value-bind (image-s-t same-sort)
532		(substitution-image-simplifying sigma s-t cp)
533		(unless same-sort (setq modif-sort t))
534		(push image-s-t l-result)))
535		(setq l-result (nreverse l-result))
536		(let ((method (term-head term)))
537		(if (and (cdr l-result)
538		(null (cddr l-result))
539		(method-is-identity method))
540		;; head operator is binary & has identity theory
541		(if (term-is-zero-for-method (car l-result) method)
542		;; ID * X --> X
543		;; simplify for left identity.
544		(values (cadr l-result)
545		(sort= (term-sort term)
546		(term-sort (cadr l-result))))
547		;; X * ID --> X
548		(if (term-is-zero-for-method (cadr l-result) method)
549		(values (car l-result)
550		(sort= (term-sort term)
551		(term-sort (car l-result))))
552		;; X * Y
553		(if modif-sort
554		(let ((term-image (make-term-with-sort-check
555		method l-result)))
556		(values term-image
557		(sort= (term-sort term)
558		(term-sort term-image))))
559		(values (make-applform (term-sort term)
560		method l-result)
561		t) ; sort not changed
562		))) ; done for zero cases
563		;; This is the same as the previous bit of code
564		(if modif-sort
565		(let ((term-image (make-term-with-sort-check method
566		l-result)))
567		(values term-image
568		(sort= (term-sort term) (term-sort term-image))))
569		(values (make-applform (method-coarity method)
570		method l-result)
571		t))))))
572		(t (break "not implemented yet")) )))
573
574		;;; CANONICALIZE-SUBSTITUTION
575		;;;
576		(defun substitution-can (s)
577		(declare (type list s)
578		(optimize (speed 3) (safety 0))
579		(values list))
580		(sort (copy-list s)
581		#'(lambda (x y) ;two substitution items (var . term)
582		(declare (type list x y))
583		(string< (the simple-string (string (variable-name (car x))))
584		(the simple-string (string (variable-name (car y)))))
585		)))
586
587		;;;
588		(defun substitution-simple-image (teta term)
589		(declare (type list teta)
590		(type term term)
591		(optimize (speed 3) (safety 0)))
592		(macrolet ((assoc% (_?x _?y)
593		`(let ((lst$$ ,_?y))
594		(loop
595		(when (null lst$$) (return nil))
596		(when (eq ,_?x (caar lst$$)) (return (car lst$$)))
597		(setq lst$$ (cdr lst$$))))))
598		(cond ((term-is-variable? term)
599		(let ((im (cdr (assoc% term teta))))
600		(if im im term)))
601		((term-is-builtin-constant? term)
602		(make-bconst-term (term-sort term)
603		(term-builtin-value term)))
604		(t (make-applform (method-coarity (term-head term))
605		(term-head term)
606		(mapcar #'(lambda (stm)
607		(substitution-simple-image teta stm))
608		(term-subterms term)))))))
609		;;; EOF

+606

-35

chaos/primitives/term-utils.lisp less more

47	47	;;; APPLICATION FORM CONSTRUTORS
48	48	;;; with some additional works ________________________________________________
49	49	;;; ****************************
50
51		;;; op make-term-check-op : method {subterms}list[term] -> term
52		;;;
53		(declaim (inline make-term-check-op))
54		(defun make-term-check-op (f subterms &optional module)
55		(declare (type method f)
56		(type list subterms)
57		(type (or null module) module)
58		(optimize (speed 3) (safety 0))
59		(inline make-term-with-sort-check))
60		(make-term-with-sort-check f subterms module))
61
62		;;; op make-term-check-op-with-sort-check :
63		;;; operator {subterms}list[term] -> term
64		;;; check if f is a built-in-constant-op
65		;;;
66		(defun make-term-check-op-with-sort-check (f subterms &optional module)
67		(declare (type method f)
68		(type list subterms)
69		(type (or null module) module)
70		(optimize (safety 0) (speed 3))
71		(inline make-term-with-sort-check))
72		(make-term-with-sort-check f subterms module))
73	50
74	51	;;; MAKE-TERM-WITH-SORT-CHECK : METHOD SUBTERMS -> TERM
75	52	;;; construct application form from given method & subterms.

131	108	(force-output))
132	109	res))
133	110
	111	;;; op make-term-check-op : method {subterms}list[term] -> term
	112	;;;
	113	(declaim (inline make-term-check-op))
	114	(defun make-term-check-op (f subterms &optional module)
	115	(declare (type method f)
	116	(type list subterms)
	117	(type (or null module) module)
	118	(optimize (speed 3) (safety 0))
	119	(inline make-term-with-sort-check))
	120	(make-term-with-sort-check f subterms module))
	121
	122	;;; op make-term-check-op-with-sort-check :
	123	;;; operator {subterms}list[term] -> term
	124	;;; check if f is a built-in-constant-op
	125	;;;
	126	(defun make-term-check-op-with-sort-check (f subterms &optional module)
	127	(declare (type method f)
	128	(type list subterms)
	129	(type (or null module) module)
	130	(optimize (safety 0) (speed 3))
	131	(inline make-term-with-sort-check))
	132	(make-term-with-sort-check f subterms module))
	133
134	134	;;;*****************************
135	135	;;; Application form constructor________________________________________________
136	136	;;;*****************************

153	153	(dolist (sub (term-subterms term))
154	154	(reset-reduced-flag sub)))
155	155	term)
	156
	157	#\|
	158	SUBSTITUTION
	159	--------------------------------------------------------------------------------
	160	A substitution is a map from variables to terms. Any mapping \sigma of variables
	161	to terms extends to a substitution by defining \sigma(f(t1,...,tn)) to be
	162	f(\sigma(t1), ... , \sigma(tn)).
	163
	164	IMPLEMENTATION:
	165	this is naturally an association list of (varible . term) pair, and we want it
	166	to be mutable, then we implemented as a structure of type list.
	167	--------------------------------------------------------------------------------
	168	\|#
	169
	170	(deftype substitution () 'list)
	171	(defmacro substitution-create (_bind) _bind)
	172	(defmacro substitution-bindings (_sub) _sub)
	173	(defmacro assoc-in-substitution (_key _sub &optional (_test '#'variable-eq))
	174	`(assoc ,_key ,_sub :test ,_test))
	175
	176	;;; CREATE-EMPTY-SUBSTITUTION
	177	;;; Creates new empty substitution
	178	;;;
	179	(defmacro create-empty-substitution () `())
	180	(declaim (inline new-substitution))
	181	(defun new-substitution () ())
	182
	183	;;; SUBSTITUTION-COPY sigma
	184	;;; Returns a copy of sigma.
	185	;;;
	186	(defmacro substitution-copy (_sigma)
	187	` (mapcar #'(lambda (map)
	188	(cons (car map) (cdr map)))
	189	,_sigma))
	190
	191	;;; SUBSTITUTION-IS-EMPTY sigma
	192	;;; Returns t iff \sigma is an empty substitution-
	193	;;;
	194	(defmacro substitution-is-empty (sigma_) `(null ,sigma_))
	195
	196	;;; SUBSTITUTION-DOMAIN sigma
	197	;;; Returns the domain of sigma
	198	;;;
	199	(defmacro substitution-domain (_sigma_) `(mapcar #'car ,_sigma_))
	200
	201	;;; VARIABLE-IMAGE
	202	;;; returns the image of variable under sigma.
	203	;;;
	204	(defmacro variable-image (_sigma _variable)
	205	`(cdr (assoc ,_variable ,_sigma :test #'variable-eq)))
	206
	207	(defmacro variable-image-fast (_sigma _variable)
	208	`(cdr (assoc ,_variable ,_sigma :test #'eq)))
	209
	210	(defmacro variable-image-slow (_sigma _variable)
	211	`(cdr (assoc ,_variable ,_sigma :test #'variable-equal)))
	212
	213	;;; SUBSTITUTION-LIST-OF-PAIRS sigma
	214	;;; returns the list of pair in substitution-
	215	;;;
	216	(defmacro substitution-list-of-pairs (_sigma_) _sigma_)
	217
	218	;;; SUBSTITUTION-ADD sigma variable term
	219	;;; adds the new map variable -> term to sigma.
	220	;;;
	221	(defmacro substitution-add (sigma_* variable_* term_*)
	222	`(cons (cons ,variable_* ,term_) ,sigma_))
	223
	224	;;; SUBSTITUTION-DELETE sigma variable
	225	;;; deletes the map for variable from sigma.
	226	;;; NOTE: sigma is modified.
	227	;;;
	228	(defmacro substitution-delete (sigma!_ variable!_)
	229	(once-only (sigma!_)
	230	` (progn (setf ,sigma!_
	231	(delete ,variable!_ ,sigma!_ :test #'variable-eq))
	232	,sigma!_)))
	233
	234	;;; SUBSTITUTION-CHANGE sigma variable term
	235	;;; change the mapping of variable to term.
	236	;;; if the variable is not in the domain of sigma, add the new binding.
	237	;;; NOTE: sigma is modified.
	238	;;;
	239	(defmacro substitution-change (?__sigma ?__variable ?__term)
	240	(once-only (?__sigma ?__variable ?__term)
	241	` (let ((binding (assoc-in-substitution ,?__variable ,?__sigma)))
	242	(if binding
	243	(setf (cdr binding) ,?__term)
	244	(push (cons variable ,?__term) ?__sigma))
	245	,?__sigma)))
	246
	247	;;; SUBSTITUTION-SET sigma variable term
	248	;;; Changes sigma to map v to term.
	249	;;;
	250	(defmacro substitution-set (?_?sigma ?_?v ?_?term)
	251	(once-only (?_?sigma ?_?v ?_?term)
	252	`(progn
	253	(if (variable-eq ,?_?v ,?_?term)
	254	(substitution-delete ,?_?sigma ,?_?v)
	255	(substitution-change ,?_?sigma ,?_?v ,?_?term))
	256	,?_?sigma)))
	257
	258	;;; CANONICALIZE-SUBSTITUTION : substitution -> substitution
	259	;;;
	260	(defun canonicalize-substitution (s)
	261	(declare (type list s)
	262	(optimize (speed 3) (safety 0))
	263	(values list))
	264	(sort (copy-list s) ; (substitution-copy s)
	265	#'(lambda (x y) ; two substitution items (var . term)
	266	(string< (the simple-string (string (variable-name (car x))))
	267	(the simple-string (string (variable-name (car y))))))))
	268
	269
	270	;;; SUBSTITUTION-EQUAL : substitution1 substitution2 -> Bool
	271	;;;
	272	(defun substitution-equal (s1 s2)
	273	(declare (type list s1 s2)
	274	(optimize (speed 3) (safety 0))
	275	(values (or null t)))
	276	(every2len #'(lambda (x y)
	277	(and (variable= (the term (car x)) (the term (car y)))
	278	(term-is-similar? (the term (cdr x)) (the term (cdr y)))))
	279	s1 s2))
	280
	281	;;; SUBSTITUTION-RESTRICT : list-of-variables substitution -> substitution
	282	;;;
	283	(defun substitution-restrict (vars sub)
	284	(declare (type list vars sub)
	285	(optimize (speed 3) (safety 0))
	286	(values list))
	287	(let ((res nil))
	288	(dolist (s sub)
	289	(when (member (car s) vars)
	290	(push s res)))
	291	res))
	292
	293	;;; SUBSTITUTION-SUBSET substitution-1 substitution-2 : -> bool
	294	;;; subset when viewed as a set of (mapping) pairs
	295	;;; assumed canonicalized
	296	;;;
	297	(defun substitution-subset (s1 s2)
	298	(declare (type list s1 s2)
	299	(optimize (speed 3) (safety 0)))
	300	(substitution-subset-list (substitution-list-of-pairs s1)
	301	(substitution-list-of-pairs s2)))
	302	(defun substitution-subset-list (s1 s2)
	303	(declare (type list s1 s2)
	304	(optimize (speed 3) (safety 0))
	305	(values (or null t)))
	306	(let ((s1x s1)
	307	(s2x s2)
	308	(res t))
	309	(loop (when (null s1x) (return))
	310	(let ((v1 (the term (caar s1x)))
	311	(t1 (the term (cdar s1x))))
	312	(loop (when (null s2x) (setq res nil) (return))
	313	(when (variable-eq v1 (caar s2x))
	314	(if (term-is-similar? t1 (cdar s2x))
	315	(progn (setq s2x (cdr s2x)) (return))
	316	(progn (setq res nil) (return))))
	317	(setq s2x (cdr s2x)))
	318	(when (null res) (return))
	319	(setq s1x (cdr s1x))))
	320	res))
	321
	322
	323	;;; SUBSTITUTION-DOMAIN-RESTRICTION sigma domain
	324	;;; Restricts the domain of sigma to dom and renames in a canonical fashion all
	325	;;; variables in the range of sigma, but not in domain. More precisely, returns
	326	;;; a substitution sigma2 with domain a subset of domain such that, for any
	327	;;; variable v in domain, \sigma2(v) = \rho(\sigma(v)), where \rho is a substitution
	328	;;; that renames variables.
	329	;;;
	330	;;; TODO
	331	(defun substitution-domain-restriction (sigma domain)
	332	sigma domain
	333	)
	334
	335	;;; SUBSTITUTION-UNION sigma1 sigma2
	336	;;; Returns the union of \sigma1 nd \sigma2. Returns 'incompatible if
	337	;;; \sigma1(v) differs from \sigma2(v) for some v in the intersection of their
	338	;;; domains.
	339	;;;
	340	;;; TODO
	341	(defun substitution-union (sigma1 sigma2)
	342	sigma1 sigma2
	343	)
	344
	345	;;; SUBSTITUTION-COMPOSIT sigma1 sigma2
	346	;;; Returns the composition of \sigma1 and \sigma2. The result of applying this
	347	;;; composition to a term t is \sigma1(\sigma2(t)).
	348	;;; NOTE: This operation is NOT commutative,
	349	;;; i,e. substitution-composit(sigma, sigma) =/= sigma.
	350	;;;
	351	(defun substitution-composit (sigma1 sigma2)
	352	sigma1 sigma2
	353	)
	354
	355	;;; SUBSTITUTION-FOREACH (element sigma) body
	356	;;; Yields the variable-term pairs in sigma
	357	;;;
	358	(defmacro substitution-foreach ((?_??element ?_??sigma) &body ?_??body)
	359	`(dolist (,?_??element (substitution-bindings ,?_??sigma))
	360	,@?_??body)
	361	)
	362
	363
	364	(defun substitution-check-built-in (trm) trm)
	365
	366	;;; SUBSTITUTION-COMPOSE
	367
	368	(defun substitution-compose (teta lisp-term)
	369	(declare (type list teta lisp-term)
	370	(optimize (speed 3) (safety 0)))
	371	(let ((fcn (lisp-form-function lisp-term))
	372	(new-fun nil)
	373	(new-term nil))
	374	(if (or #-CMU(typep fcn 'compiled-function)
	375	#+CMU(typep fcn 'function)
	376	(not (and (consp fcn) (eq 'lambda (car fcn))
	377	(equal '(compn) (cadr fcn)))))
	378	(setf new-fun
	379	`(lambda (compn) (funcall ',fcn (append ',teta compn))))
	380	(let ((oldteta (cadr (nth 1 (nth 2 (nth 2 fcn)))))
	381	(realfcn (cadr (nth 1 (nth 2 fcn)))))
	382	(setf new-fun
	383	`(lambda (compn)
	384	(funcall ',realfcn (append ',(append teta oldteta) compn))))))
	385	(if (term-is-simple-lisp-form? lisp-term)
	386	(setf new-term (make-simple-lisp-form-term (lisp-form-original-form lisp-term)))
	387	(setf new-term (make-general-lisp-form-term (lisp-form-original-form lisp-term))))
	388	(setf (lisp-form-function new-term) new-fun)
	389	new-term))
	390
	391	(defun substitution-compose-chaos (teta chaos-expr)
	392	(declare (type list teta chaos-expr)
	393	(optimize (speed 3) (safety 0)))
	394	(let ((fcn (chaos-form-expr chaos-expr))
	395	(new-fun nil)
	396	(new-term nil))
	397	(if (or #-CMU(typep fcn 'compiled-function)
	398	#+CMU(typep fcn 'function)
	399	(not (and (consp fcn) (eq 'lambda (car fcn))
	400	(equal '(compn) (cadr fcn)))))
	401	(setf new-fun
	402	`(lambda (compn) (funcall ',fcn (append ',teta compn))))
	403	(let ((oldteta (cadr (nth 1 (nth 2 (nth 2 fcn)))))
	404	(realfcn (cadr (nth 1 (nth 2 fcn)))))
	405	(setf new-fun
	406	`(lambda (compn)
	407	(funcall ',realfcn (append ',(append teta oldteta) compn))))))
	408	(setf new-term (make-bconst-term chaos-value-sort
	409	(list '\|%Chaos\|
	410	new-fun
	411	(chaos-original-expr chaos-expr))))
	412	new-term))
	413
	414	;;; SUBSTITUTION-IMAGE* sigma term
	415	;;; Returns the image of term under sigma. Like substitution-image, but
	416	;;; changing bound variables as necessary in the result to prevent variables in the
	417	;;; range of sigma from being captured by a quantifier in term. Also renames all bound
	418	;;; variables in the image of term under sigma (by replacing them by constants).
	419	;;; To preserve shared subterms, returns t itself, and not a copy, if the image is the
	420	;;; same as t.
	421	;;; * TODO *
	422	;;;
	423
	424	;; NO COPY of Term is done.
	425	(defun substitution-image-no-copy (sigma term &optional (subst-pconst nil))
	426	(declare (type list sigma)
	427	(type term term)
	428	(optimize (speed 3) (safety 0))
	429	(values t))
	430	(let ((im nil))
	431	;; '-image-slow' because the use case often distructively changes terms.
	432	(cond ((term-is-variable? term)
	433	(when (setq im (variable-image-slow sigma term))
	434	(term-replace term im)))
	435	((term-is-constant? term)
	436	(when subst-pconst
	437	(when (setq im (variable-image-slow sigma term))
	438	(term-replace term im))))
	439	(t (dolist (s-t (term-subterms term))
	440	(substitution-image-no-copy sigma s-t subst-pconst))))
	441	term))
	442
	443	;;; CANONICALIZE-SUBSTITUTION
	444	;;;
	445	(defun substitution-can (s)
	446	(declare (type list s)
	447	(optimize (speed 3) (safety 0))
	448	(values list))
	449	(sort (copy-list s)
	450	#'(lambda (x y) ;two substitution items (var . term)
	451	(declare (type list x y))
	452	(string< (the simple-string (string (variable-name (car x))))
	453	(the simple-string (string (variable-name (car y))))))))
	454
	455	(defun substitution-simple-image (teta term)
	456	(declare (type list teta)
	457	(type term term)
	458	(optimize (speed 3) (safety 0)))
	459	(macrolet ((assoc% (_?x _?y)
	460	`(let ((lst$$ ,_?y))
	461	(loop
	462	(when (null lst$$) (return nil))
	463	(when (eq ,_?x (caar lst$$)) (return (car lst$$)))
	464	(setq lst$$ (cdr lst$$))))))
	465	(cond ((term-is-variable? term)
	466	(let ((im (cdr (assoc% term teta))))
	467	(if im im term)))
	468	((term-is-builtin-constant? term)
	469	(make-bconst-term (term-sort term)
	470	(term-builtin-value term)))
	471	(t (make-applform (method-coarity (term-head term))
	472	(term-head term)
	473	(mapcar #'(lambda (stm)
	474	(substitution-simple-image teta stm))
	475	(term-subterms term)))))))
156	476
157	477	;;; **************************
158	478	;;; WITH-VARIABLE-AS-CONSTANT------------------------------------------------

178	498	(make-pconst-term sort pc-name pc-pname)))
179	499
180	500	(defun variables->pconstants (term)
181		(declare (optimize (speed 3) (safety 0)))
182		(let ((vars (term-variables term))
183		(subst (new-substitution))
184		(rsubst (new-substitution)))
185		(dolist (var vars)
186		(let ((pc (make-pconst-from-var var)))
187		(setq subst (substitution-add subst var pc))
188		(setq rsubst (substitution-add rsubst pc var))))
189		(setq rsubst (copy-tree rsubst)) ; because substitution-image-no-copy
	501	(declare (type term term)
	502	(optimize (speed 3) (safety 0)))
	503	(macrolet ((substitution-add (_sigma _var _term)
	504	`(cons (cons ,_var ,_term) ,_sigma)))
	505	(let ((vars (term-variables term))
	506	(subst nil)
	507	(rsubst nil))
	508	(dolist (var vars)
	509	(let ((pc (make-pconst-from-var var)))
	510	(setq subst (substitution-add subst var pc))
	511	(setq rsubst (substitution-add rsubst pc var))))
	512	(setq rsubst (copy-tree rsubst)) ; because substitution-image-no-copy
190	513	; destructively changes given term
191		(substitution-image-no-copy subst term)
192		rsubst))
	514	(substitution-image-no-copy subst term)
	515	rsubst)))
193	516
194	517	(defun revert-pconstants (term rsubst)
195		(declare (optimize (speed 3) (safety 0)))
	518	(declare (type term term)
	519	(optimize (speed 3) (safety 0)))
196	520	(substitution-image-no-copy rsubst term :subst-pconstance)
197	521	term)
198	522

1498	1822	(term-print term))
1499	1823	(t (print-chaos-object term))))))
1500	1824
	1825	;;; SUBSTITUTION-IMAGE
	1826	;;; Returns sigma(t) and "true" iff the sort of "t" and "sigma(t)" are the same.
	1827	;;; A COPY of the term "t" is done and the sort information is updated.
	1828	;;;
	1829	(defun substitution-image (sigma term)
	1830	(declare (type list sigma)
	1831	(optimize (speed 3) (safety 0))
	1832	(type term term))
	1833	(let ((consider-object t))
	1834	(cond ((term-is-variable? term)
	1835	(let ((im (variable-image sigma term)))
	1836	(if im;; i.e. im = sigma(term)
	1837	(values im nil)
	1838	(values term t))))
	1839	((term-is-lisp-form? term)
	1840	(multiple-value-bind (new-term success)
	1841	(funcall (lisp-form-function term) sigma)
	1842	(if success
	1843	new-term
	1844	(throw 'rule-failure :fail-builtin))))
	1845	((term-is-chaos-expr? term)
	1846	(multiple-value-bind (new-term success)
	1847	(funcall (chaos-form-expr term) sigma)
	1848	(if success
	1849	new-term
	1850	(throw 'fule-failure :fail-builtin))))
	1851	((term-is-builtin-constant? term)
	1852	term) ; shold we copy?
	1853	(t (let ((l-result nil)
	1854	(modif-sort nil))
	1855	(dolist (s-t (term-subterms term))
	1856	(multiple-value-bind (image-s-t same-sort)
	1857	(substitution-image sigma s-t)
	1858	(unless same-sort (setq modif-sort t))
	1859	(push image-s-t l-result)))
	1860	(setq l-result (nreverse l-result))
	1861	(if modif-sort
	1862	(let ((term-image (make-term-with-sort-check (term-head term)
	1863	l-result)))
	1864	(values term-image
	1865	(sort= (term-sort term)
	1866	(term-sort term-image))))
	1867	(values (make-applform (term-sort term)
	1868	(term-head term)
	1869	l-result)
	1870	t)))))))
	1871
	1872	(defun substitution-image! (sigma term)
	1873	(declare (type list sigma)
	1874	(optimize (speed 3) (safety 0))
	1875	(type term term))
	1876	(let ((consider-object t))
	1877	(cond ((term-is-variable? term)
	1878	(let ((im (variable-image-slow sigma term)))
	1879	(if im;; i.e. im = sigma(term)
	1880	(values im nil)
	1881	(values term t))))
	1882	((term-is-lisp-form? term)
	1883	(multiple-value-bind (new-term success)
	1884	(funcall (lisp-form-function term) sigma)
	1885	(if success
	1886	new-term
	1887	(throw 'rule-failure :fail-builtin))))
	1888	((term-is-chaos-expr? term)
	1889	(multiple-value-bind (new-term success)
	1890	(funcall (chaos-form-expr term) sigma)
	1891	(if success
	1892	new-term
	1893	(throw 'fule-failure :fail-builtin))))
	1894	((term-is-builtin-constant? term) term) ; shold we copy?
	1895	(t (let ((l-result nil)
	1896	(modif-sort nil))
	1897	(dolist (s-t (term-subterms term))
	1898	(multiple-value-bind (image-s-t same-sort)
	1899	(substitution-image! sigma s-t)
	1900	(unless same-sort (setq modif-sort t))
	1901	(push image-s-t l-result)))
	1902	(setq l-result (nreverse l-result))
	1903	(if modif-sort
	1904	(let ((term-image (make-term-with-sort-check (term-head term)
	1905	l-result)))
	1906	(values term-image
	1907	(sort= (term-sort term)
	1908	(term-sort term-image))))
	1909	(values (make-applform (term-sort term)
	1910	(term-head term)
	1911	l-result)
	1912	t)))))))
	1913
	1914	(defun substitution-image-cp (sigma term)
	1915	(declare (type list sigma)
	1916	(optimize (speed 3) (safety 0))
	1917	(type term term))
	1918	(let ((consider-object t))
	1919	(cond ((term-is-variable? term)
	1920	(let ((im (variable-image sigma term)))
	1921	(if im;; i.e. im = sigma(term)
	1922	;; (values (simple-copy-term im) nil)
	1923	(values im nil)
	1924	(values term t))))
	1925	((term-is-lisp-form? term)
	1926	(multiple-value-bind (new-term success)
	1927	(funcall (lisp-form-function term) sigma)
	1928	(if success
	1929	new-term
	1930	(throw 'rule-failure :fail-builtin))))
	1931	((term-is-chaos-expr? term)
	1932	(multiple-value-bind (new-term success)
	1933	(funcall (chaos-form-expr term) sigma)
	1934	(if success
	1935	new-term
	1936	(throw 'fule-failure :fail-builtin))))
	1937	((term-is-builtin-constant? term) term) ; shold we copy?
	1938	(t (let ((l-result nil)
	1939	(modif-sort nil))
	1940	(dolist (s-t (term-subterms term))
	1941	(multiple-value-bind (image-s-t same-sort)
	1942	(substitution-image-cp sigma s-t)
	1943	(unless same-sort (setq modif-sort t))
	1944	(push image-s-t l-result)))
	1945	(setq l-result (nreverse l-result))
	1946	(if modif-sort
	1947	(let ((term-image (make-term-with-sort-check (term-head term)
	1948	l-result)))
	1949	(values term-image
	1950	(sort= (term-sort term)
	1951	(term-sort term-image))))
	1952	(values (make-applform (term-sort term)
	1953	(term-head term)
	1954	l-result)
	1955	t)))))))
	1956
	1957	(defun substitution-partial-image (sigma term)
	1958	(declare (type list sigma)
	1959	(type term term)
	1960	(optimize (speed 3) (safety 0)))
	1961	(let ((consider-object t))
	1962	(cond ((term-is-variable? term)
	1963	(let ((im (variable-image sigma term)))
	1964	(if im
	1965	(values im nil)
	1966	(values term t))))
	1967	((term-is-lisp-form? term)
	1968	(substitution-compose sigma term)
	1969	)
	1970	((term-is-chaos-expr? term)
	1971	(substitution-compose-chaos sigma term))
	1972	((term-is-builtin-constant? term) term)
	1973	((term-is-applform? term)
	1974	(let ((l-result nil) (modif-sort nil))
	1975	(dolist (s-t (term-subterms term))
	1976	(multiple-value-bind (image-s-t same-sort)
	1977	(substitution-partial-image sigma s-t)
	1978	(unless same-sort (setq modif-sort t))
	1979	(push image-s-t l-result)))
	1980	(setq l-result (nreverse l-result))
	1981	(if modif-sort
	1982	(let ((term-image (make-term-with-sort-check
	1983	(term-head term)
	1984	l-result)))
	1985	(values term-image
	1986	(sort= (term-sort term)
	1987	(term-sort term-image))))
	1988	(values (make-applform (term-sort term) (term-head term) l-result)
	1989	t))))
	1990	(t (break "substution-partial-image : not implemented ~s" term)))))
	1991
	1992	(defun substitution-image-simplifying (sigma term &optional (cp nil) (slow-map nil))
	1993	(declare (type list sigma)
	1994	(type term)
	1995	(optimize (speed 3) (safety 0)))
	1996	(let ((consider-object t))
	1997	;; (setq subst-debug-term term)
	1998	(cond ((term-is-variable? term)
	1999	(let ((im (if slow-map
	2000	(variable-image-slow sigma term)
	2001	(variable-image sigma term))))
	2002	(if im
	2003	(values (if cp
	2004	(progn
	2005	(simple-copy-term im))
	2006	im)
	2007	(sort= (variable-sort term)
	2008	(term-sort im)))
	2009	(values term t))))
	2010	((term-is-chaos-expr? term)
	2011	(when rewrite-debug
	2012	(format t "CHAOS: ~S" (chaos-form-expr term)))
	2013	(multiple-value-bind (new-term success)
	2014	(funcall (chaos-form-expr term) sigma)
	2015	(if success
	2016	new-term
	2017	(throw 'fule-failure :fail-builtin))))
	2018	((term-is-builtin-constant? term) term)
	2019	((term-is-lisp-form? term)
	2020	(multiple-value-bind (new success)
	2021	(funcall (lisp-form-function term) sigma)
	2022	(if success
	2023	new
	2024	(throw 'rule-failure :fail-builtin))))
	2025	((term-is-applform? term)
	2026	(let ((l-result nil)
	2027	(modif-sort nil))
	2028	(dolist (s-t (term-subterms term))
	2029	(multiple-value-bind (image-s-t same-sort)
	2030	(substitution-image-simplifying sigma s-t cp)
	2031	(unless same-sort (setq modif-sort t))
	2032	(push image-s-t l-result)))
	2033	(setq l-result (nreverse l-result))
	2034	(let ((method (term-head term)))
	2035	(if (and (cdr l-result)
	2036	(null (cddr l-result))
	2037	(method-is-identity method))
	2038	;; head operator is binary & has identity theory
	2039	(if (term-is-zero-for-method (car l-result) method)
	2040	;; ID * X --> X
	2041	;; simplify for left identity.
	2042	(values (cadr l-result)
	2043	(sort= (term-sort term)
	2044	(term-sort (cadr l-result))))
	2045	;; X * ID --> X
	2046	(if (term-is-zero-for-method (cadr l-result) method)
	2047	(values (car l-result)
	2048	(sort= (term-sort term)
	2049	(term-sort (car l-result))))
	2050	;; X * Y
	2051	(if modif-sort
	2052	(let ((term-image (make-term-with-sort-check
	2053	method l-result)))
	2054	(values term-image
	2055	(sort= (term-sort term)
	2056	(term-sort term-image))))
	2057	(values (make-applform (term-sort term)
	2058	method l-result)
	2059	t) ; sort not changed
	2060	))) ; done for zero cases
	2061	;; This is the same as the previous bit of code
	2062	(if modif-sort
	2063	(let ((term-image (make-term-with-sort-check method
	2064	l-result)))
	2065	(values term-image
	2066	(sort= (term-sort term) (term-sort term-image))))
	2067	(values (make-applform (method-coarity method)
	2068	method l-result)
	2069	t))))))
	2070	(t (break "not implemented yet")) )))
	2071
1501	2072	;;; EOF

-1

sysdef.asd less more

90	90	(:file "gen-print")
91	91	(:file "context")
92	92	(:file "term-utils")
93		(:file "substitution")
94	93	(:file "find")
95	94	(:file "print-object")
96	95	))

-3

thstuff/apply-tactic.lisp less more

185	185	;;;
186	186	(defun normalize-term-in (module term &optional (reduction-mode :red) var-is-const)
187	187	(let ((applied? nil)
188		(targets nil)
189	188	(rule-count-save (number-rewritings))
190	189	(variable-as-constant var-is-const))
	190	(declare (type fixnum rule-count-save)
	191	(optimize (speed 3) (safety 0)))
191	192	(reducer-no-stat term module reduction-mode)
192		(unless (= rule-count-save (number-rewritings))
	193	(unless (= rule-count-save (the fixnum (number-rewritings)))
193	194	(setq applied? t))
194	195	(values term applied?)))
195	196

198	199	;;; NOTE: given axiom is preserved (not changed).
199	200	;;;
200	201	(defun normalize-sentence (ax module &optional lhs-only variable-is-constant)
	202	(declare (type rewrite-rule ax)
	203	(type module module)
	204	(type (or null t) lhs-only variable-is-constant)
	205	(optimize (speed 3) (safety 0)))
201	206	(if-spoiler-on
202	207	;; normalize sentence only if :spoiler is on
203	208	:then (let ((target (rule-copy-canonicalized ax module)))

1606	1611	(step-goals nil)
1607	1612	(remainings nil))
1608	1613	;; just for now
1609		(declare (ignore given-hypos targets))
	1614	(declare (ignore given-hypos))
1610	1615	;; base cases
1611	1616	(dolist (target targets)
1612	1617	(if (not (set-base-cases base-goal target (get-ind-substitutions indvars (goal-bases goal))))

-0

thstuff/proof-struct.lisp less more

1090	1090	;;; :order (<op>, ..., <op>)
1091	1091	;;;
1092	1092	(defun citp-eval-order (ast)
	1093	(declare (notinline %pn-lex-ops))
1093	1094	(check-context-module-and-ptree)
1094	1095	(with-in-module ((get-context-module))
1095	1096	(let ((optokens (%pn-lex-ops ast)))