A. First Edition

This little problem is part of assignment of comp472 and it is a group assignment which means I owe credit from members in

our group. However, I keep a version for my personal reference later. (I already suffer the pain of losing my assignment of

comp348 in Haskell which is another dialect of Lisp.

B.The problem

　

C.The idea of program

　

I think I already explained very clearly about the purpose of this simple program.

D.The major functions

To run them, you need only (load "flatten_final.txt") at command line of Gambit or other Scheme prgram. then (convert test** 'dnf)

or (convert test** 'cnf)

E.Further improvement

The next step?

F.File listing

1. utility.txt

2. nnf.txt

3. mergebracket.txt

4. dfs.txt

5. clausesort.txt

6. testcases.txt

7. flatten_final.txt

file name: utility.txt

;this is supposed to be our small library where all common utility
;function are stored in this file and all other module will load this
;module by (load "utility.txt")

;some functions here are simply some simplified version of Scheme built-in 
;functions. However, we prefer our own version.

;there is subtle difference between these contradictive predicate
;cannot simply negate them
(define not_symbol
	(lambda (x)
		(if (symbol? x)
			#f
			(if (is_not x)
				#f
				#t
			)
		)
	)
)

(define is_symbol
	(lambda (x)
		(or (symbol? x)(is_not x))
	)
)

(define is_not
	(lambda (ls)
		(if (symbol? ls)
			#f
			(eq? (car ls) 'NOT)
		)
	)
)

(define is_or
	(lambda (ls)
		(if (symbol? ls)
			#f
			 (eq? (car ls) 'OR)	
		)		
	)
)

(define is_and
	(lambda (ls)
		(if (symbol? ls)
			#f
			(eq? (car ls) 'AND)
		)
	)
)

;this is my own limited version of "map"
(define foreach
	(lambda (f)
		(lambda (ls)
			(if   (null? ls)
				'()
				(cons (f (car ls)) ((foreach f) (cdr ls)))
			)
		)
	)
)

;"this is my own limited version of "append"
(define concat 
	(lambda (ls1 ls2)
		(if (null? ls1)
			ls2
			(cons (car ls1) (concat (cdr ls1) ls2))
		)
	)
)

(define concatlist
	(lambda (ls)
		(if (null? ls)
			'()
			(concat (car ls) (concatlist (cdr ls)))
		)
	)
)




(define generic_insert
	(lambda (f)
		(lambda (x ls)
			(if (null? ls)
				(list x)
				(if (f x (car ls))
					(cons x ls)
					(cons (car ls) ((generic_insert f) x (cdr ls)))
				)
			)
		)
	)
)		


; a general purpose sorting algorithm which is a bubble sort with user defined compare method
; as parameter f. 
(define generic_sort
	(lambda (f)
		(lambda (ls)
			(if (null? (cdr ls))
				ls
				((generic_insert f) (car ls) ((generic_sort f) (cdr ls)))
			)
		)
	)
)

file name: nnf.txt

(load "utility.txt")
(load "testcases.txt")

;this is to convert input to be "nnf" format in which all "NOT" are before the
;single symbol instead of a sublist
;i.e. (NOT (AND A B) ===>(OR (NOT A)(NOT B))
;usage: (mergebracket input)
;input is assumed in WFF format

(define nnf_op
	(lambda (ls)		
		(if (null? ls)
			'()
			(if (symbol? (car ls))
				(cond
					((eq? (car ls) 'AND) (cons 'OR (nnf_op (cdr ls))))
					((eq? (car ls) 'OR) (cons 'AND (nnf_op (cdr ls))))
					((and (eq? (car ls) 'NOT) (symbol? (cadr ls)))  (cadr ls))		
					((and (eq? (car ls) 'NOT) (not(symbol? (cadr ls))))  (nnf (cadr ls)))		
					(else (cons (list 'NOT (car ls)) (nnf_op (cdr ls))))
				)
				(cons (nnf_op (car ls)) (nnf_op (cdr ls)))
			)
			
		)
	)
)






(define nnf
	(lambda (expr)
		(if (null? expr)
			'()
			(if (symbol? (car expr))
				(if (eq? (car expr) 'NOT)
					(if (symbol? (cadr expr))
						;(cons (list 'NOT (cadr expr)) (nnf (cddr expr)))
						(list 'NOT (cadr expr))
						;we need to 'float' up a level since NOT is unary operator
						;(cons (nnf_op (cadr expr)) (nnf (cddr expr)))						
						(nnf_op (cadr expr))
					)
					(cons (car expr) (nnf (cdr expr)))
				)
				(cons (nnf (car expr)) (nnf (cdr expr)))
			)
		)
	)
)
					

file name: mergebracket.txt

(load "utility.txt")
(load "testcases.txt")

;remove redundant parenthese. ie (AND(AND A B) C) has redundant parenthese
;usage: (mergebracket input)
;input is assumed in "nnf" format

(define domerge
	(lambda (ls1 ls2)
		(if (null? ls2)
			ls1
			(if (is_symbol (car ls2))
				(domerge (append ls1 (list (car ls2))) (cdr ls2))
				(if (eq? (car ls1)(car (car ls2)))
					(domerge (append ls1 (cdr (mergebracket (car ls2)))) (cdr ls2))
					(domerge(append ls1 (list(mergebracket (car ls2)))) (cdr ls2))
				)
			)
		)
	)
)

(define mergebracket
	(lambda (ls)
		(domerge '() ls)
	)
)

file name: dfs.txt

(load "utility.txt")
(load "testcases.txt")

;this is the "distribution function which assume input has been converted to
;"nnf" format, redundant parenthese has been removed, input has been sorted by 
;alphabetic order in case of symbol, in length ascending order in case of sub-;list. 
;usage: (dfs input)
;it must be sorted such that all single term (including "NOT" term) are at 
;left hand side and all elements which are actually a sublist must be at right
;hand side.


(define combine
	(lambda (f x y)
		(cond
			((and (is_symbol x)(is_symbol y))
				(list f x y))
			((and (not_symbol x)(is_symbol y))
				(cons f (cons y (cdr x))))
			((and (not_symbol x)(not_symbol y))
				(cons f (concat (cdr x) (cdr y))))
			((and (is_symbol x)(not_symbol y))
				(cons f (cons x (cdr y))))		
		)
	)
)


(define is_simple
	(lambda (ls)
		(if (is_symbol ls)
			#t
			(is_symbol (car ls))				
		)
	)
)

(define single_op
	(lambda (ls)
		(< (length ls) 2)
	)
)

(define same_op
	(lambda (ls1 ls2)
		(eq? (car ls1)(car ls2))
	)
)

(define combine_op
	(lambda(f)
		(lambda (x)
			(lambda (y)
				(combine f x y)
			)
		)
	)
)

(define map_op
	(lambda (f ls)
		(lambda (x)
			(map (f x) ls)
		)
	)
)



	
(define foreachlist2list
	(lambda (f)
		(lambda (ls1 ls2)
			;(begin (pp (list "foreachlist2list ls1=" ls1 "ls2=" ls2))

;			(map (map_op f ls1) ls2)
			(if (null? ls1)
				'()
				(concat (map (f (car ls1)) ls2) ((foreachlist2list f) (cdr ls1) ls2))
;				(map (f (car ls1)) ((foreachlist2list f) (cdr ls1) ls2))
;				((foreachlist2list f) (cdr ls1) (map (f (car ls1)) ls2))
;				(map (map f ls1)
			)
			;)
		)
	)
)








(define dodistribute
	(lambda (op ls1 ls2)
		;(begin (pp (list "dodistribute ls1=" ls1 "ls2=" ls2))
		(if (or (single_op ls1)(single_op ls2))
			'()
			(cons (swap_op op) ((foreachlist2list (combine_op op))(cdr ls1)(cdr ls2)))
		)
		;)
	)
)

(define mymap
	(lambda (op ls1 ls2)
		;(begin (pp (list "mymap op=" op "ls1=" ls1 "ls2=" ls2))
		(if (single_op ls2)
			ls1
			(if (and (same_op ls1 ls2)(eq? op (car ls1)))

;			(if (same_op ls1 ls2)
;				(if (eq? op (car ls1))
					(concat ls1 (cdr ls2))
					(dodistribute op ls1 ls2)
;				)
			)
		)
		;)
	)
)	


;(define test1 '(AND X A (OR B (AND C (OR M N) F) D) (OR W(AND P (OR Q (AND X Y))))))
;(define test2 '(AND X (OR Y Z)))
;(define test13 '(AND (OR B C D) A B))
;(define test4 '(AND X Z (OR A B C)))
;(define test5 '(AND (OR X Y) (OR W Z) ))
;(define test6 '(OR (AND X Y (OR A B)) U))
;(define test7 '(AND (OR X Y N Z) (OR U W M)))

(define swap_op
	(lambda (x)
		(if (eq? x 'AND)
			'OR
			'AND
		)
	)
)

(define distribute
	(lambda (ls)
		;(begin (pp (list "distribute ls=" ls))
		(if (single_op ls)
			'()
			(if (is_symbol (cadr ls))
				(mymap (car ls)(cons (car ls) (list (cadr ls))) (distribute (cons (car ls)(cddr ls))))
				(mymap (car ls)(distribute  (cadr ls)) (distribute (cons (car ls)(cddr ls))))
			)
		)
		;)
	)
)


(define dfs
	(lambda (ls)
		(if (is_symbol ls)
			ls
			(distribute ls)
		)
	)
)

file name: clausesort.txt

(load "utility.txt")
(load "testcases.txt")

;this is the sorting module. It uses bubble sort algorithm to sort input
;such that all single term (including "NOT" term) are in left hand side and 
;all terms which are sublist are in right-hand-side
;usage: (dfs_sort input)
;input are assumed to be in "nnf" format with redundant parenthese are removed.




(define symbol_length
	(lambda (ls)
		(if (symbol? ls)
			0
			(length ls)
		)
	)
)

(define symbolcomp
	(lambda (sym1 sym2)
		(if (and (is_symbol sym1)(is_symbol sym2))
			(string<? (symbol->string sym1) (symbol->string sym2))
			(listcomparison sym1 sym2)
		)
	)
)


(define term2string
	(lambda (ls)
		(if (is_not ls)
			(symbol->string (cadr ls))
			(symbol->string ls)
		)
	)
)
;
(define termcomp
	(lambda (ls1 ls2)
		(if (string=? (term2string ls1)(term2string ls2))
			(if (and (is_not ls1)(symbol? ls2));  define "not A" < "A"
				#t
				#f ;all other cases assume they are not ls1<ls2
			)
			(string<? (term2string ls1)(term2string ls2))
		)
	)
)

(define clausesort
	(lambda (ls)
		((generic_sort clausecomp) ls)
	)
)				

(define clauselength
	(lambda (ls)
		(if (is_symbol ls)
			0
			(- (length ls) 1)
		)
	)
)

;already tested length of ls1 and ls2, they must be equal!
(define termbyterm
	(lambda (ls1 ls2)
		(if (null? ls1)
			#f
			(let ((n1 (clauselength ls1))(n2 (clauselength ls2)))
				(if (and (= n1 n2)(= n1 0));single term
					(termcomp (car ls1)(car ls2))
					(if (= n1 n2)
						(termbyterm (cdr ls1)(cdr ls2))
						(< n1 n2)
					)
				)
			)
		)
	)
)

(define clausecomp
	(lambda (ls1 ls2)
		(if (and (is_symbol ls1)(is_symbol ls2))
			(termcomp ls1 ls2)
			(let ((n1 (clauselength ls1))(n2 (clauselength ls2)))
				(if (= n1 n2)
					(termbyterm ls1 ls2)
					(< n1 n2)
				)
			)
		)
	)
)

(define dfs_sort
	(lambda (lst)
		(if (is_symbol lst)
			lst
			(cons (car lst) (clausesort (map dfs_sort (cdr lst))))
		)
	)
)

(define contraterm
	(lambda (x y)
		(cond
			((or(not_symbol x)(not_symbol y)) #f)
			((and (is_not x)(is_not y))  #f)
			((and (symbol? x)(symbol? y)) #f)
			(else (string=? (term2string x)(term2string y)))
		)
	)
)

			

;find mutual-negate pairs; return true or false
(define findcontra
	(lambda (ls)
		(if (or (null? ls)(null? (cdr ls)))
			#f
			(if (contraterm (car ls) (cadr ls))
				#t
				(findcontra (cdr ls))
			)
		)
	)
)

;assumed already assorted
(define evalclause
	(lambda (ls)
		(if (or(eq? ls 'TRUE)(eq? ls 'OR))
			ls
			(if (findcontra (cdr ls))
				(if (eq? (car ls) 'AND)
					'FALSE
					'TRUE
				)
				ls
			)
		)
	)
)

(define doshrinkclause
	(lambda (ls1 ls2)
		(if (null? ls2)
			ls1			
			(if (and(is_symbol (car ls2))(not(eq?(car ls2)'TRUE))(not(eq?(car ls2)'FALSE)))				
				(doshrinkclause (concat ls1 (list (car ls2))) (cdr ls2))
				(cond
					((and (eq? (evalclause (car ls2)) 'TRUE) (eq? (car ls1) 'AND))
						(doshrinkclause ls1 (cdr ls2)));ignore the term
					((and (eq? (evalclause (car ls2)) 'FALSE) (eq? (car ls1) 'AND))
						'FALSE)
					((and (eq? (evalclause (car ls2)) 'FALSE) (eq? (car ls1) 'OR))
						(doshrinkclause ls1 (cdr ls2))); ignore the term
					((and (eq? (evalclause (car ls2)) 'TRUE) (eq? (car ls1) 'OR))
						'TRUE)
					(else (doshrinkclause (concat ls1 (list(car ls2))) (cdr ls2)))
				)
			)
		)
	)
)

					

(define shrinkclause
	(lambda (ls)
		(let ((lst (evalclause ls)))
			(if (or(eq? lst 'TRUE)(eq? lst 'FALSE))
				lst
				(doshrinkclause (list (car lst)) (cdr lst))
			)
		)
	)
)
		

;(define absorb
;	(lambda ls)
;		(if 



file name: testcases.txt

;NNF + merge bracket checks
(define test01 '(NOT (NOT (NOT (NOT (AND B C))))))
(define test02 '(NOT (AND (NOT A) (NOT B))))
(define test03 '(NOT (AND (OR X Y (AND A B)) U)))
(define test04 '(NOT (OR (AND X Y (OR A B)) U)))
(define test05 '(NOT (AND A (NOT (NOT C)) D (OR E (NOT F)))))
(define test06 '(NOT (AND A (OR B C) (AND D E))))
(define test07 '(NOT (AND (NOT B) (OR (NOT A) (NOT B)))))
(define test08 '(NOT (AND (AND A B) (AND C D))))

;simple convert tests
(define test09 '(OR (NOT A) B C))
(define test10 '(AND X (OR Y Z)))
(define test11 '(AND A B))
(define test12 '(AND (OR B C D) A B))
(define test13 '(OR (AND A B C) X Z))
(define test14 '(AND (OR X Y) (OR W Z) ))
(define test15 '(OR (AND D A) (AND C B) D))
(define test16 '(NOT (AND (OR (AND A B) (OR C D)) E)))

; does order matter?
(define test17 '(AND A D (OR B C)))
(define test18 '(AND (OR B C) A D))
(define test19 '(AND D (OR B C) A))
(define test20 '(AND A B C (OR P Q R) (OR X Y Z))) ; 'cnf may take a while, as the complexity increases exponentially
(define test21 '(AND (OR P Q R) A B C (OR X Y Z))) ; 'cnf may take a while, as the complexity increases exponentially
(define test22 '(AND (OR P Q R) (OR X Y Z) A B C)) ; 'cnf may take a while, as the complexity increases exponentially

; complexity tests: WARNING works for 'dnf, 'cnf may "explode"
(define test23 '(AND (OR B (AND C (OR M N) F) D) (OR W(AND P (OR Q(AND X Y) X A)))))
(define test24 '(AND X A (OR B (AND C (OR M N) F) D) (OR W(AND P (OR Q(AND X Y))))))

file name: flatten_final.txt

(load "utility.txt")
(load "nnf.txt")
(load "dfs.txt")
(load "clausesort.txt")
(load "mergebracket.txt")
(load "testcases.txt")

;this module acts as a "main" with function "flatten" to flatten
;input to be either "cnf"or "dnf". It first check if output is matched or 
;not after first "flatten" operation, if yes, return the result. if no, 
;flatten again. 
;usage: (convert input indicator)
;input must be WFF and single term or '(AND A B) are considered as
;natural "cnf" or "dnf" format
;this module will load all other module. So to invoke whole project, just 
;(load flatten_final.txt)
;(convert input indicator)

(define flatten
	(lambda (ls)
		(dfs (dfs_sort ( mergebracket (nnf ls))))
	)

)

;this function test if output is what we need
(define term_match
	(lambda (indicator ls)
		(or     (and (eq? indicator 'cnf)(is_and ls)) 
			(and (eq? indicator 'dnf)(is_or ls))
		)
	)

)


(define convert
	(lambda (ls indicator)
		(let ((lst (flatten ls)))
			(if (term_match indicator lst)
				lst
                                     (flatten lst)

			)
		)
	)
)