(FILECREATED " 3-MAR-83 12:57:19" {PHYLUM}<FIKES>LISP>PROCESSWFFS.;13 19803  

      changes to:  (FNS EvalAtom)

      previous date: " 3-FEB-83 13:27:46" {PHYLUM}<BLUEBONNET>PROCESSWFFS.;4)


(PRETTYCOMPRINT PROCESSWFFSCOMS)

(RPAQQ PROCESSWFFSCOMS [(FNS * PROCESSWFFSFNS)
			(RECORDS * PROCESSWFFSRECORDS)
			(VARS * PROCESSWFFSVARS)
			(DECLARE: EVAL@COMPILE (P (LOADCOMP? 'LOADBLUEBONNET])

(RPAQQ PROCESSWFFSFNS (CombineSupports CompactNormalForm CreateWff EvalAndWff EvalAtom EvalCompactOr 
				       EvalDividesWff EvalEqualWff EvalEval EvalGtWff EvalIfWff 
				       EvalImpliesWff EvalNotWff EvalOrWff EvalQuoteWff EvalTimesWff 
				       EvalWff FieldsInWff NormalizeSubWff NormalizeWff 
				       ShortestSupport WffEqual WffToList))
(DEFINEQ

(CombineSupports
  [LAMBDA (supportList)                                      (* edited: "20-JAN-83 10:19")
                                                             (* supportLIst is a list of supports as returned from 
							     EvalWff. Produce a support list that is the AND of those
							     supports.)
    (for sList in supportList::1 bind (support ← supportList:1) when sList
       do [support←(for s1 in sList join (for s2 in support collect (UNION s1 s2]
	  (support←(for s1 on support unless (for s2 on support unless s1=s2
						thereis (Subset? s2:1 s1:1)
							  and (s2:1 MEMB s1::1
								      or (LENGTH s1:1)
									 ~=(LENGTH s2:1)))
		      collect s1:1))
       finally (RETURN support])

(CompactNormalForm
  [LAMBDA (wff)                                              (* ref: " 4-JUN-82 14:15")

          (* Return the compact conjunctive normal form of wff. The compact form is a list of lists.
	  Elements of the top level list represent conjuncts in the normal form. Elements of the second level lists 
	  represent disjuncts in the normal form.)


    (PROG ((normal (NormalizeWff wff)))
          (RETURN (for c in (if (type? Wff normal) and normal:operator='AND
				then normal:operands
			      else <normal>)
		     collect (if (type? Wff c) and c:operator='OR
				 then c:operands
			       else <c>])

(CreateWff
  [LAMBDA (wffExp)                                           (* ref: " 4-JUN-82 11:21")
                                                             (* Create a wff from an s-expression form.)
    (if (LISTP wffExp)
	then (create Wff
		     operator ← wffExp:1
		     operands ←(for rand in wffExp::1 collect (CreateWff rand)))
      else wffExp])

(EvalAndWff
  [LAMBDA (operands context supportFlg)                      (* edited: " 3-FEB-83 11:58")
                                                             (* Evaluator for conjunctions.)
    (if supportFlg
	then (for rand on operands bind (support val)
		do (val←(EvalWff rand:1 context T))
		   (if val:1
		       then (push support val::1)
		     else support←val::1
			  (for r in rand::1 unless (CAR (val←(EvalWff r context T)))
			     do (pushlist support val::1))
			  (RETURN <NIL ! support>))
		finally (RETURN <T !(CombineSupports support)
				  >))
      else (for rand in operands always (EvalWff rand context])

(EvalAtom
  [LAMBDA (wff context supportFlg)                           (* edited: " 3-MAR-83 12:56")
                                                             (* Evaluator for an atom.)
    (if supportFlg
	then <(if (type? CopyJob context)
		  then (JobFieldValue wff context)
		else (RECORDACCESS wff context (if (type? JobState context)
						   then JobStateRecord)))
	       <wff>>
      else (if (type? CopyJob context)
	       then (JobFieldValue wff context)
	     else (RECORDACCESS wff context (if (type? JobState context)
						then JobStateRecord])

(EvalCompactOr
  [LAMBDA (constraint context supportFlg)                    (* edited: "19-JAN-83 14:44")
                                                             (* Evaluate a disjunction represented as a list of 
							     disjuncts.)
    (if supportFlg
	then (for d on constraint bind (support val)
		do (val←(EvalWff d:1 context T))
		   (if val:1
		       then support←val::1
			    (for r in d::1 when (CAR (val←(EvalWff r context T)))
			       do (pushlist support val::1))
			    (RETURN <T ! support>)
		     else (push support val::1))
		finally (RETURN <NIL !(CombineSupports support)
				  >))
      else (for d in constraint thereis (EvalWff d context])

(EvalDividesWff
  [LAMBDA (operand1 operand2 context supportFlg)             (* edited: " 3-FEB-83 12:00")
                                                             (* Evaluator for TIMES.)
    (if supportFlg
	then (PROG ((r1 (EvalWff operand1 context T))
		    (r2 (EvalWff operand2 context T)))
	           (RETURN <(r1:1 or 0)/r2:1 !(CombineSupports <r1::1 r2::1>)
			     >))
      else ((EvalWff operand1 context) or 0)/(EvalWff operand2 context])

(EvalEqualWff
  [LAMBDA (operand1 operand2 context supportFlg)             (* edited: " 3-FEB-83 12:01")
                                                             (* Evaluator for =.)
    (if supportFlg
	then (PROG ((r1 (EvalWff operand1 context T))
		    (r2 (EvalWff operand2 context T)))
	           (RETURN <(EQUAL r1:1 r2:1) !(CombineSupports <r1::1 r2::1>)
			     >))
      else (EQUAL (EvalWff operand1 context)
		  (EvalWff operand2 context])

(EvalEval
  [LAMBDA (operand context supportFlg)                       (* edited: " 3-FEB-83 12:02")
                                                             (* Evaluator for Eval.)
    (APPLY* operand context supportFlg])

(EvalGtWff
  [LAMBDA (operand1 operand2 context supportFlg)             (* edited: " 3-FEB-83 12:02")
                                                             (* Evaluator for >.)
    (if supportFlg
	then (PROG ((r1 (EvalWff operand1 context T))
		    (r2 (EvalWff operand2 context T)))
	           (RETURN <(GREATERP (OR r1:1 0)
				      (OR r2:1 0))
			     !(CombineSupports <r1::1 r2::1>)
			     >))
      else (GREATERP (OR (EvalWff operand1 context)
			 0)
		     (OR (EvalWff operand2 context)
			 0])

(EvalIfWff
  [LAMBDA (operand1 operand2 operand3 context supportFlg)    (* edited: " 3-FEB-83 12:03")
                                                             (* Evaluator for IF.)
    (if supportFlg
	then (PROG (r2 (r1 (EvalWff operand1 context T)))
	           (r2 ←(EvalWff (if r1:1
				     then operand2
				   else operand3)
				 context T))
	           (RETURN <r2:1 !(CombineSupports <r1::1 r2::1>)
			     >))
      elseif (EvalWff operand1 context)
	then (EvalWff operand2 context)
      else (EvalWff operand3 context])

(EvalImpliesWff
  [LAMBDA (operand1 operand2 context supportFlg)             (* edited: " 3-FEB-83 12:04")
                                                             (* Evaluator for IMPLIES.)
    (if supportFlg
	then (PROG ((r1 (EvalWff operand1 context T))
		    (r2 (EvalWff operand2 context T)))
	           (RETURN (if r1:1
			       then (if r2:1
					then <T ! r2::1 >
				      else <NIL !(CombineSupports <r1::1 r2::1>)
					     >)
			     elseif r2:1
			       then <T r1::1 r2::1>
			     else <T ! r1::1>)))
      else ~(EvalWff operand1 context) or (EvalWff operand2 context])

(EvalNotWff
  [LAMBDA (operand context supportFlg)                       (* edited: " 3-FEB-83 12:04")
                                                             (* Evaluator for ~.)
    (if supportFlg
	then (PROG ((val (EvalWff operand context T)))
	           (RETURN <~(val : 1) ! val::1>))
      else ~(EvalWff operand context])

(EvalOrWff
  [LAMBDA (operands context supportFlg)                      (* edited: " 3-FEB-83 12:04")
                                                             (* Evaluate a disjunction.)
    (if supportFlg
	then (for rand on operands bind (support val)
		do (val←(EvalWff rand:1 context T))
		   (if val:1
		       then support←val::1
			    (for r in rand::1 when (CAR (val←(EvalWff r context T)))
			       do (pushlist support val::1))
			    (RETURN <T ! support>)
		     else (push support val::1))
		finally (RETURN <NIL !(CombineSupports support)
				  >))
      else (for rand in operands thereis (EvalWff rand context])

(EvalQuoteWff
  [LAMBDA (operand context supportFlg)                       (* edited: " 3-FEB-83 12:05")
                                                             (* Evaluator for quoted values.)
    (if supportFlg
	then <operand>
      else operand])

(EvalTimesWff
  [LAMBDA (operand1 operand2 context supportFlg)             (* edited: " 3-FEB-83 12:06")
                                                             (* Evaluator for TIMES.)
    (if supportFlg
	then (PROG ((r1 (EvalWff operand1 context T))
		    (r2 (EvalWff operand2 context T)))
	           (RETURN <(r1:1 or 0)*(r2:1 or 0) !(CombineSupports <r1::1 r2::1>)
			     >))
      else ((EvalWff operand1 context) or 0)*((EvalWff operand2 context) or 0])

(EvalWff
  [LAMBDA (wff context supportFlg)                           (* edited: " 3-FEB-83 12:17")

          (* Evaluate the wff wff in the given context. If supportFlg is non-NIL, then return a dotted pair, the first 
	  element of which is the value of the wff, the second is a list of fields whose values were used to determine the 
	  value.)


    (if (LITATOM wff)
	then (EvalAtom wff context supportFlg)
      elseif (NUMBERP wff)
	then (if supportFlg
		 then <wff>
	       else wff)
      else (SELECTQ wff:operator
		    (= (EvalEqualWff wff:operands:1 wff:operands:2 context supportFlg))
		    (~ (EvalNotWff wff:operands:1 context supportFlg))
		    (AND (EvalAndWff wff:operands context supportFlg))
		    (QUOTE (EvalQuoteWff wff:operands:1 context supportFlg))
		    (OR (EvalOrWff wff:operands context supportFlg))
		    (IF (EvalIfWff wff:operands:1 wff:operands:2 wff:operands:3 context supportFlg))
		    (> (EvalGtWff wff:operands:1 wff:operands:2 context supportFlg))
		    (Eval (EvalEval wff:operands:1 context supportFlg))
		    (TIMES (EvalTimesWff wff:operands:1 wff:operands:2 context supportFlg))
		    (/ (EvalDividesWff wff:operands:1 wff:operands:2 context supportFlg))
		    (HELP "Unrecognized Wff operator" wff:operator])

(FieldsInWff
  [LAMBDA (wff)                                              (* ref: " 4-JUN-82 12:48")
                                                             (* Return a list of the fields mentioned in wff.)
    (if (LITATOM wff)
	then <wff>
      elseif (type? Wff wff) and wff:operator~='QUOTE
	then (for rand in wff:operands join (FieldsInWff rand])

(NormalizeSubWff
  [LAMBDA (wff)                                              (* ref: "22-NOV-82 12:49")
                                                             (* Convert wff to conjunctive wff form.
							     Each of wff's operands have already been normalized.
							     IMPLIES and IFF have already been removed.)
    (PROG (conjunction disjuncts)                            (* ~~x -> x)
          [COND
	    ((AND (EQ (fetch operator of wff)
		      (QUOTE ~))
		  (type? Wff (CAR (fetch operands of wff)))
		  (EQ (fetch operator of (CAR (fetch operands of wff)))
		      (QUOTE ~)))
	      (RETURN (CAR (fetch operands of (CAR (fetch operands of wff]
                                                             (* or and -> and)
          [COND
	    ([AND (EQ (fetch operator of wff)
		      (QUOTE OR))
		  (SETQ conjunction (for d in (fetch operands of wff) when (type? Wff d)
				       thereis (EQ (fetch operator of d)
						   (QUOTE AND]
	      (SETQ disjuncts (for d in (fetch operands of wff) unless (EQ d conjunction)
				 collect d))
	      (SETQ wff (create Wff
				operator ←(QUOTE AND)
				operands ←(for c in (fetch operands of conjunction)
					     collect (NormalizeSubWff (create Wff
									      operator ←(QUOTE
										  OR)
									      operands ←(CONS c 
											disjuncts]
                                                             (* or or -> or)
          [COND
	    ([AND (EQ (fetch operator of wff)
		      (QUOTE OR))
		  (for rand in (fetch operands of wff) thereis (AND (type? Wff rand)
								    (EQ (fetch operator of rand)
									(QUOTE OR]
	      (SETQ wff (create Wff
				operator ←(QUOTE OR)
				operands ←(for d in (fetch operands of wff)
					     join (COND
						    ((AND (type? Wff d)
							  (EQ (fetch operator of d)
							      (QUOTE OR)))
						      (APPEND (fetch operands of d)))
						    (T (LIST d]
                                                             (* and and -> and)
          [COND
	    ([AND (EQ (fetch operator of wff)
		      (QUOTE AND))
		  (for rand in (fetch operands of wff) thereis (AND (type? Wff rand)
								    (EQ (fetch operator of rand)
									(QUOTE AND]
	      (SETQ wff (create Wff
				operator ←(QUOTE AND)
				operands ←(for c in (fetch operands of wff)
					     join (COND
						    ((AND (type? Wff c)
							  (EQ (fetch operator of c)
							      (QUOTE AND)))
						      (APPEND (fetch operands of c)))
						    (T (LIST c]
                                                             (* (OR a b a) -> (OR a b) and 
							     (AND a b a) -> (AND a b))
                                                             (* (OR x) -> x and (AND x) -> x)
          [COND
	    ((OR (EQ (fetch operator of wff)
		     (QUOTE OR))
		 (EQ (fetch operator of wff)
		     (QUOTE AND)))
	      [SETQ wff (create Wff
				operator ←(fetch operator of wff)
				operands ←(for randLoc on (fetch operands of wff)
					     unless (for rand in (CDR randLoc)
						       thereis (WffEqual (CAR randLoc)
									 rand))
					     collect (CAR randLoc]
	      (COND
		((EQ (LENGTH (fetch operands of wff))
		     1)
		  (SETQ wff (CAR (fetch operands of wff]
          (RETURN wff])

(NormalizeWff
  [LAMBDA (wff)                                              (* edited: "31-JAN-83 14:47")
                                                             (* Convert wff to conjunctive normal form.)
    (if (type? Wff wff)
	then [if wff:operator=(QUOTE IMPLIES)
		 then                                        (* implies -> or)
		      (NormalizeWff (create Wff
					    operator ←(QUOTE OR)
					    operands ←(<(create Wff
								operator ←(QUOTE ~)
								operands ←(<wff:operands:1>))
					      wff:operands:2>)))
	       elseif wff:operator=(QUOTE IFF)
		 then                                        (* iff -> and)
		      (NormalizeWff (create Wff
					    operator ←(QUOTE AND)
					    operands ←(<(create Wff
								operator ←(QUOTE IMPLIES)
								operands ← wff:operands)
					      (create Wff
						      operator ←(QUOTE IMPLIES)
						      operands ←(<wff:operands:2 wff:operands:1>))
					      >)))
	       elseif wff:operator=(QUOTE ~) and (type? Wff wff:operands:1) and 
									 wff:operands:1:operator=(
										  QUOTE
										    AND)
		 then                                        (* ~and -> or)
		      [NormalizeWff (create Wff
					    operator ←(QUOTE OR)
					    operands ←(for c in wff:operands:1:operands
							 collect (create Wff
									 operator ←(QUOTE ~)
									 operands ←(<c>]
	       elseif wff:operator=(QUOTE ~) and (type? Wff wff:operands:1) and 
									 wff:operands:1:operator=(
										  QUOTE
										    OR)
		 then                                        (* ~or -> and)
		      [NormalizeWff (create Wff
					    operator ←(QUOTE AND)
					    operands ←(for d in wff:operands:1:operands
							 collect (create Wff
									 operator ←(QUOTE ~)
									 operands ←(<d>]
	       elseif wff:operator=(QUOTE IF)
		 then                                        (* if -> 'and' of 2 'or's)
		      (NormalizeWff (create Wff
					    operator ←(QUOTE AND)
					    operands ←(<(create Wff
								operator ←(QUOTE OR)
								operands ←(<(create Wff
										    operator ←(QUOTE
										      ~)
										    operands ←(
										 <wff:operands:1>))
								  wff:operands:2>))
					      (create Wff
						      operator ←(QUOTE OR)
						      operands ←(<wff:operands:1 wff:operands:3>))
					      >)))
	       else (NormalizeSubWff (create Wff
					     operator ← wff:operator
					     operands ←(for rand in wff:operands collect
										  (NormalizeWff
										    rand]
      else wff])

(ShortestSupport
  [LAMBDA (supportList)                                      (* edited: "19-JAN-83 13:40")
                                                             (* supportList is a list of lists.
							     Return the shortest list that is an element of 
							     supportList.)
    (for s in supportList::1 bind (support ← supportList:1)
       when (LENGTH s) lt (LENGTH support) do support←s finally (RETURN support])

(WffEqual
  [LAMBDA (w1 w2)                                            (* edited: "21-NOV-82 13:20")
                                                             (* Test whether w1 and w2 are equivalent wffs.)
    (OR w1=w2 (AND (type? Wff w1)
		   (type? Wff w2)
		   w1:operator=w2:operator
		   (LENGTH w1:operands)=(LENGTH w2:operands)
		   (for rand1 in w1:operands as rand2 in w2:operands always (WffEqual rand1 rand2])

(WffToList
  [LAMBDA (wff)                                              (* ref: " 1-JUN-82 15:53")
                                                             (* Produce a list structure form of wff acceptable by 
							     CreateWff.)
    (if (ATOM wff)
	then wff
      else <wff:operator !(for rand in wff:operands collect (WffToList rand))
	     >])
)

(RPAQQ PROCESSWFFSRECORDS (Wff))
[DECLARE: EVAL@COMPILE 

(DATATYPE Wff (operator operands))
]
(/DECLAREDATATYPE (QUOTE Wff)
		  (QUOTE (POINTER POINTER)))

(RPAQQ PROCESSWFFSVARS [(CopyJobRecord (RECLOOK (QUOTE CopyJob)))
			(JobStateRecord (RECLOOK (QUOTE JobState])

(RPAQ CopyJobRecord (RECLOOK (QUOTE CopyJob)))

(RPAQ JobStateRecord (RECLOOK (QUOTE JobState)))
(DECLARE: EVAL@COMPILE 
(LOADCOMP? 'LOADBLUEBONNET)
)
(DECLARE: DONTCOPY
  (FILEMAP (NIL (762 19339 (CombineSupports 772 . 1597) (CompactNormalForm 1599 . 2298) (CreateWff 2300
 . 2702) (EvalAndWff 2704 . 3444) (EvalAtom 3446 . 4088) (EvalCompactOr 4090 . 4875) (EvalDividesWff 
4877 . 5376) (EvalEqualWff 5378 . 5876) (EvalEval 5878 . 6116) (EvalGtWff 6118 . 6676) (EvalIfWff 6678
 . 7280) (EvalImpliesWff 7282 . 7950) (EvalNotWff 7952 . 8318) (EvalOrWff 8320 . 9060) (EvalQuoteWff 
9062 . 9340) (EvalTimesWff 9342 . 9853) (EvalWff 9855 . 11207) (FieldsInWff 11209 . 11617) (
NormalizeSubWff 11619 . 15267) (NormalizeWff 15269 . 17984) (ShortestSupport 17986 . 18465) (WffEqual 
18467 . 18936) (WffToList 18938 . 19337)))))
STOP