(*: John Silvela
	jcsilvel@syr.edu
	CIS473 - Wang's Algorithm Programming Assignment
	(Implemented using CAML)
	DUE: Wednesday, March 1, 2000
	[Extended until Friday, March 3]    *)



(*:----------------------------------------- *)
(*:  N O T E S   &   D E S C R I P T I O N   *)
(*:----------------------------------------- *)

(*: 
	I implemented wang's algorithm through a CAML function.  My function to perform 
	wang's algorithm requires the logic_expr type definitions, and 2 helper functions -  
	check (to check if a formula occurs in both the left & right hand sides of the 
	turnstile) and reduced (to check if a list (one side of the turnstile) contains 
	just single variables)
	
	
	I "ran" my program by using the free CAML Light Interpreter for Macintosh.
	It can be found at 
	http://caml.inria.fr/distrib-caml-light-eng.html
	
	
	To use my wang's algorithm function, you would call the function and pass it two 
	lists (of logic expressions).  Each list represents one side of the turnstile, so the
	first list would be the left hand side of the turnstile, and the second list would 
	be the right hand side of the turnstile. 	

	My function will then return a boolean value (true / false) corresponding to
	whether or not the expression was a tautology.
	
	
	REPRESENTATION OF LOGIC EXPRESSIONS :
	
	(PVar "x")  =>			   x   (the logic variable x)
	(Not exp1)  =>             ~ exp1
	(And (exp1,exp2))  =>      exp1 & exp2
	(Or (exp1,exp2))  =>       exp1 v exp2
	(Implies (exp1,exp2))  =>  exp1 -> exp2
	
	
	
	
	SOME EXAMPLES TO TRY :
	
	wangs_alg [(PVar "p")] [(PVar "p")];; 
	
	REPRESENTS   --->   p |- p
	SHOULD RETURN  --->  true
	----------------------------------------------
	
	wangs_alg [(PVar "p")] [(PVar "r"); (PVar "q")];;
	
	REPRESENTS   --->   p  |-  r, q
	SHOULD RETURN  --->  false
	----------------------------------------------
	
	wangs_alg [(PVar "p")] [(Or ((PVar "r"), (PVar "p"))); (Not (PVar "s"))];;
	
	REPRESENTS   --->   p  |-  (r v p), ~s
	SHOULD RETURN  --->  true
	----------------------------------------------
	
	wangs_alg [(PVar "p")] [(Or ((PVar "r"), (PVar "p"))); (Not (PVar "s")); (PVar "s")];;
	
	REPRESENTS   --->   p  |-  (r v p), ~s, s
	SHOULD RETURN  --->  true
	----------------------------------------------
	
	wangs_alg 
	[(Implies ((PVar "p"), (PVar "q"))); (Implies ((PVar "q"), (PVar "r"))); (Not (PVar "r"))] 
	[Not (PVar "p")];;
	
	REPRESENTS   --->   (p -> q), (q -> r), ~r  |-  ~p
	SHOULD RETURN  --->  true
	----------------------------------------------
	
	wangs_alg 
	[] 
	[(Implies ((Implies ( (And ((PVar "p"), (PVar "q"))) , (PVar "r"))),  
			  (Implies ( (Or ((PVar "p"), (PVar "q"))) , (PVar "r")))))];;
			  
	REPRESENTS   --->     |-  ( (p & q) -> r )  ->  ( (p v q) -> r )
	SHOULD RETURN  --->  false
	----------------------------------------------

	wangs_alg 
	[] 
	[(Implies ( (Implies ((PVar "a"), (PVar "b"))) , 
			  (Implies ( (Implies ((Not(PVar "a")), (PVar "b"))) , (PVar "b")))))];;
			  
	REPRESENTS   --->     |-  (a -> b)  ->  ( (~a -> b)  ->  b)
	SHOULD RETURN  --->  true
	----------------------------------------------
	



*)

(*:---------------------------------------- *)



	
(*:----------------------------------------------------------- *)
(*: L O G I C  EXPRESSION  T Y P E S  created for this program *)
(*:----------------------------------------------------------- *)

type logic_expr = PVar of string
				| Or of logic_expr * logic_expr
				| And of logic_expr * logic_expr
				| Implies of logic_expr * logic_expr
				| Not of logic_expr;;

(*:----------------------------------------------------------- *)





(*:----------------------------------------------------------------------------------------- *)
(*: C H E C K -  Checks if a formula occurs on both the left & right hand sides (in 2 lists) *)
(*:----------------------------------------------------------------------------------------- *)

let rec check = 
	fun [] [] -> true
	 |  [PVar x] [PVar y] -> if (x=y) then true else false
	 |  ls [] -> false
	 |  [] ls -> false
	 
	 |  ((PVar x)::ls1) [PVar y] -> if (x=y) then true else (false or (check ls1 [PVar y]))
	 
	 |  [PVar x] ((PVar y)::ls2) -> if (x=y) then true else (check [PVar x] ls2)
	 
	 |  ((PVar x)::ls1) ((PVar y)::ls2) -> 
	 		if (x=y) then true
	 			else ( (check [PVar x] ls2) or (check ls1 ((PVar y)::ls2) ) );;
	 			
(*:----------------------------------------------------------------------------------------- *)





(*: --------------------------------------------------------------- *)		
(*: R E D U C E D - Checks if a list contains just single variables *)
(*: --------------------------------------------------------------- *)	

let rec reduced = 
	fun ((PVar x)::ls) -> (true & (reduced ls))
	 |  []  -> true
	 |  ls -> false;;
	 
(*: --------------------------------------------------------------- *)	






(*:----------------------------------------------------------- *)
(*:  I M P L E M E N T A T I O N   of Wang's Algorithm in caml *)
(*:----------------------------------------------------------- *)

let rec  wangs_alg = 
	fun  (Implies (e1, e2)::ls1) ls2 -> (wangs_alg  (((Or ((Not e1), e2))::ls1))  ls2)	 
	 |   ls1 ((Implies (e1, e2))::ls2) -> (wangs_alg ls1  ((Or ((Not e1), e2))::ls2))
	 
	 
	 |   ((Not e1)::ls1) ls2 -> wangs_alg ls1 (e1::ls2)
	 |   ls1 ((Not e1)::ls2) -> wangs_alg (e1::ls1) ls2

	 
	 |  ((And (e1, e2))::ls1) ls2 -> (wangs_alg (e1::e2::ls1) ls2) 
	 |  ls1  ((Or (e1, e2))::ls2) -> (wangs_alg ls1 (e1::e2::ls2))


	 |  ((Or (e1, e2))::ls1) ls2 -> ((wangs_alg (e1::ls1) ls2) & (wangs_alg (e2::ls1) ls2)) 
	 |  ls1  ((And (e1, e2))::ls2) -> ((wangs_alg ls1 (e1::ls2)) & (wangs_alg ls1 (e2::ls2)))
	 
	 |  [PVar x] [PVar y] -> if (x=y) then true else false
	 
	 |  ((PVar x)::ls1) ((PVar y)::ls2)  -> 
	 		if ( (reduced ls1)&(reduced ls2) ) then (check ((PVar x)::ls1) ((PVar y)::ls2)) 
	 			else (wangs_alg  (ls1@[(PVar x)])  (ls2@[(PVar y)]) )
	 			
	 | [] ((PVar y)::ls2) -> 
	 		if (reduced ls2) then false
	 			else (wangs_alg []  (ls2@[(PVar y)]) )

	 			
	 | ((PVar x)::ls1) [] ->
			if (reduced ls1) then false
				else (wangs_alg (ls1@[(PVar x)]) [])
	 
	 
	 | [] [] -> true;;


(*:----------------------------------------------------------- *)