(* CMSC 330 / Fall 2009 / Project 4 *)

(* NAME: *)

(* To load this file into the OCaml interpreter, type

   #use "boolean.ml"

   at the OCaml prompt
*)

type formula =
    False
  | True
  | Var of char
  | And of formula * formula
  | Or of formula * formula
  | Not of formula
  | Forall of char * formula
  | Exists of char * formula

type assignment = (char * bool) list

type vec = formula list

(*----------------------------------------------------------
  function f_to_str : formula -> string. 

	converts formula into a string 
*)

let rec f_to_str f = match f with
    False -> "F"
  | True -> "T"
  | Var x -> Char.escaped x
  | And (f1,f2) -> "(" ^ (f_to_str f1) ^ " && " ^ (f_to_str f2) ^ ")"
  | Or (f1,f2) -> "(" ^ (f_to_str f1) ^ " || " ^ (f_to_str f2) ^ ")"
  | Not f1 -> "(! " ^ (f_to_str f1) ^ ")"
  | Forall (x,f1) -> "(forall " ^ (Char.escaped x) ^ " : " ^ (f_to_str f1) ^ ")"
  | Exists (x,f1) -> "(exists " ^ (Char.escaped x) ^ " : " ^ (f_to_str f1) ^ ")"
;;

(*----------------------------------------------------------
  function eval : formula -> assignment -> bool. 

	evaluates the boolean formula on the given variable assignment 
	returns the result as an OCaml bool. 
*)

let rec eval f e = match f with 
    False -> false
  | True -> false
  | Var x -> false
  | And (f1,f2) -> false
  | Or (f1,f2) -> false
  | Not f1 -> false
  | Forall (x,f1) -> false
  | Exists (x,f1) -> false
;;

(*----------------------------------------------------------
  function vars_of : formula -> char list. 

	takes a formula and returns a list of the names of the 
	free variables of the formula. 
*)

let vars_of x = 
	[]
;;

(*----------------------------------------------------------
  function sat : formula -> assignment option. 

	function returns Some a, where a is a satisfying assignment, 
	if the formula is satisfiable, or None otherwise. 
*)

let sat x = 
	None
;;

(*----------------------------------------------------------
  function double : vec -> vec. 

	returns a vec representing twice its argument. 
*)

let double x = 
	[]
;;

(*----------------------------------------------------------
  function int_of_vec : vec -> int. 

	takes a vec composed solely of Trues and Falses 
	returns the integer equivalent. 
*)

let int_of_vec x = 
	0
;;

(*----------------------------------------------------------
  function vec_of_int : int -> vec. 

	takes a non-negative integer 
	returns the corresponding vec. 
*)

let vec_of_int x = 
	[]
;;

(*----------------------------------------------------------
  function subst : assignment -> vec -> vec. 

	reduces the vec argument to a vec of all Trues and Falses 
	by replacing the variables in the vec according to the 
	assignment and then evaluating each bit. 
*)

let subst x y = 
	[]
;;

(*----------------------------------------------------------
  function zero : vec -> formula. 

	returns a boolean formula representing whether vec represents zero, 
	i.e., is composed solely of False or formulae that are false. 
*)

let zero x = 
	True
;;

(*----------------------------------------------------------
  function bitand : vec -> vec -> vec. 

	returns a new vec representing the bitwise and of the two vectors. 
*)

let bitand x y =
	[]
;;

(*----------------------------------------------------------
  function eq : vec -> vec -> formula. 

	returns a formula representing whether the two bit vectors are equal. 
*)

let eq x y =
	(True)
;;

(*----------------------------------------------------------
  function add : vec -> vec -> vec. 

	returns a new vec representing the sum of the two vectors. 
*)

let add x y =
	[]
;;

(*----------------------------------------------------------
  function pad : vec -> int -> vec. 

	pad v i returns a new vec that is equal to v 
	but whose length is the greater of i and the length of v. 
*)

let pad x y =
	[]
;;

(*----------------------------------------------------------
  function mul : vec -> int -> vec. 

	mul a i returns a new vec representing the product of the a and i. 
*)

let mul x y =
	[]
;;

(*----------------------------------------------------------
  function add_three : vec -> vec -> vec -> vec. 

	returns a new vector that represents the sum of 
	the three input vectors. 
*)

let add_three x y z =
	[]
;;

(*----------------------------------------------------------
  function is_digit : vec -> formula. 

	input is a vec of length 4 (i.e., exactly 4 boolean formulae). 

	returns a formula that is true if and only if the vec is 
	greater than or equal to 1 and less than or equal to 9.
*)

let is_digit x =
	True	
;;

(*----------------------------------------------------------
  function disjoint : vec list -> formula. 

	takes a list of vecs and returns a formula representing whether 
	all the vecs are different from each other.
*)

let disjoint x =
	True	
;;

(*----------------------------------------------------------
  function is_magic : vec list -> formula. 

	takes a list of exactly nine vecs and returns a formula 
	representing whether the list is a magic square. 
*)

let is_magic x =
	True	
;;