Commit 7a03ee2212657e19a95aa5ce3ef6ee159d4103d9 - cafeobj

+16

-14

cafeobj/creader.lisp less more

328	328	\|}\|))
329	329
330	330	(defparameter INIT
331		'((:+ \|:init\| init \|:init!\| init!)
	331	'(\|:init\|
332	332	(:if-present as :symbol)
333		(:one-of (\( (:one-of #.EqDeclaration
334		#.CeqDeclaration
335		#.RlDeclaration
336		#.CRlDeclaration
337		#.BeqDeclaration
338		#.BCeqDeclaration
339		#.BRLDeclaration
340		#.BCRLDeclaration
341		#.FoplAXDeclaration)
342		\))
343		(\[ (:symbol) \]))
344		\|by\| \|{\| ((:! SubstList)) \|}\|))
	333	(:one-of ((:+ \|{\| \() (:one-of #.EqDeclaration
	334	#.CeqDeclaration
	335	#.RlDeclaration
	336	#.CRlDeclaration
	337	#.BeqDeclaration
	338	#.BCeqDeclaration
	339	#.BRLDeclaration
	340	#.BCRLDeclaration
	341	#.FoplAXDeclaration)
	342	(:+ \|}\| \)))
	343	(\[ :symbol \]))
	344	(:if-present by \|{\| ((:! SubstList)) \|}\|)))
	345
345	346	(defparameter USE
346	347	'(\|:use\|
347	348	(:one-of (\( (:seq-of :symbol) \))

350	351	(\|id:\| :chaos-item)
351	352	(\|identity:\| :chaos-item))
352	353	\|}\|))))
	354
353	355	(defparameter EMBED
354	356	'(\|:embed\|
355	357	(:one-of (\( (:seq-of :symbol) \) (:+ as into) :symbol)

901	903	;; Substitution
902	904	;; variable-1 <- term-1; ... variable-n <- term-n;
903	905	(SubstList ((:! Subst) :append (:seq-of (:! Subst))))
904		(Subst ((:symbol <- :term) \;))
	906	(Subst ((:symbol <- :term) (:+ \|,\| \;)))
905	907	)) ; end of cafeobj-scheme
906	908	) ; end eval-when
907	909

+1

-0

thstuff/apply-tactic.lisp less more

2186	2186	;;; resolve-subst-form
2187	2187	;;;
2188	2188	(defun resolve-subst-form (context subst-forms &optional (normalize nil))
	2189	(unless subst-forms (return-from resolve-subst-form nil))
2189	2190	(with-in-module (context)
2190	2191	(let ((subst nil)
2191	2192	(parse-variables nil))

+12

-7

thstuff/citp.lisp less more

159	159	;;;
160	160	;;; :init {[<label>] \| (<axiom>)} by { <var> <- <term>; ...<var> <- <term>; }
161	161	;;;
	162	;;; first second third four fifth
162	163	;;; (":init" ("[" ("test1") "]") "by" "{" (("X:S" "<-" ("X#S")) ";") "}"))
	164	;;; first second third fourth
	165	;;; (":init" ("as" "ts-ss-1") (#1="{" ("eq" ("ts.." "(" "SS:SeqSym" ")") "=" ("true") ".") #3="}") ("by" #1# (("SS:SeqSym" "<-" ("ss")) #2=";" ("XX:Bar" "<-" ("bb")) #2#) #3#)))
	166	;;; (":init" ("as" "ts-ss-1") (#1="(" ("eq" ("ts.." #1# "SS:SeqSym" #2=")") "=" ("true") ".") #2#) "by" ("{" ("SS:SeqSym" "<-" ("ss")) ";" "}"))
163	167	;;;
164	168	(defun make-axiom-pattern (target)
165		(if (equal (first target) "[")
166		(cons :label (second target))
167		(cons :axiom (second target))))
	169	(if (stringp target)
	170	(cons :label (list target))
	171	(cons :axiom target)))
168	172
169	173	(defun citp-parse-init (args)
170	174	(let ((name (if (equal (first (second args)) "as")
171	175	(second (second args))
172	176	nil)))
173	177	(let ((target-form (make-axiom-pattern (if name
174		(third args)
175		(second args))))
	178	(second (third args))
	179	(second (second args)))))
176	180	(subst-list (if name
177		(sixth args)
178		(fifth args)))
	181	(third (fourth args))
	182	(third (third args))))
179	183	(subst-pairs nil))
180	184	(dolist (subst-form subst-list)
181	185	(unless (atom subst-form)

297	301	;;; (":def" "tactic-1" "=" ("(" ("si" "rd" "tc") ")"))
298	302	;;; ==> (:seq "tactic-1" ("si" "rd" "tc"))
299	303	;;; (":define" "disr" "=" (":init" ("[" ("disr") "]") "by" "{" (("X:PNat.PNAT" "<-" ("X#PNat")) #1=";" ("Y:PNat.PNAT" "<-" ("Y@PNat")) #1# ("Z:PNat.PNAT" "<-" ("Z@PNat")) #1#) "}"))
	304	;;; (":define" "ts-ss2" "="(":init" ("as" "ts-ss-1") (#1="(" ("eq" ("ts.." #1# "SS:SeqSym" #2=")") "=" ("true") ".") #2#) "by" ("{" ("SS:SeqSym" "<-" ("ss")) ";" "}")))
300	305	;;; ==> (:init "disr" nil (":init" ("[" ("disr") "]") "by" "{" (("X:PNat.PNAT" "<-" #) #1=";" ("Y:PNat.PNAT" "<-" #) #1# ("Z:PNat.PNAT" "<-" #) #1#) "}"))
301	306
302	307	(defun citp-parse-define (args)

+8

-5

thstuff/proof-struct.lisp less more

211	211	(if (eq (first (tactic-init-kind obj)) :label)
212	212	(format stream "[~a]" (second (tactic-init-kind obj)))
213	213	(progn
214		(princ "(")
	214	(princ "{")
215	215	(print-axiom-brief (tactic-init-axiom obj))
216		(princ " .)")))
217		(print-next)
218		(princ "by subst form: ")
219		(princ (tactic-init-subst obj)))))
	216	(princ " .}")))
	217	(if (tactic-init-subst obj)
	218	(progn
	219	(print-next)
	220	(princ "by subst form: ")
	221	(princ (tactic-init-subst obj)))
	222	(princ ".")))))
220	223
221	224	;;; :ind as tactic
222	225	;;;