(* The data type of variable names (ie, strings) *)
type name = string

(* The data type of boolean expression:
   variables, negations, conjunctions and disjunctions *)
type bexp =
  | Var of name
  | Neg of bexp
  | Conj of bexp * bexp
  | Disj of bexp * bexp

(* The data type of truth value associations (ie, an environment) *)
type benv = (name * bool) list

(* lookup : name -> benv -> bool option *)
let rec lookup n env = match env with
  | [] ->
    None
  | (m, v) :: env' ->
    if m = n
    then Some v
    else lookup n env'

(* An exceptional state for evaluating an expression in an
   insufficient environment *)
exception UNBOUND_VARIABLE of name

(* eval : bexp -> benv -> bool *)
let eval e env =
  let rec visit e = match e with
    | Var n ->
      (match lookup n env with
        | None -> raise (UNBOUND_VARIABLE n)
        | Some v -> v)
    | Neg e ->
      not (visit e)
    | Conj (e1, e2) ->
      let v1 = visit e1 in
      let v2 = visit e2 in
      v1 && v2
    | Disj (e1, e2) ->
      let v1 = visit e1 in
      let v2 = visit e2 in
      v1 || v2
  in visit e


(* ex.4 *)
(* eval : bexp -> benv -> bool option *)
let eval' e env =
  let rec visit e = match e with
    | Var n ->
      lookup n env
    | Neg e ->
      (match visit e with
	| None -> None
	| Some v -> Some (not v))
    | Conj (e1, e2) ->
      (match visit e1 with
	| None -> None
	| Some v1 ->
	  (match visit e2 with
	    | None -> None
	    | Some v2 ->
	      Some (v1 && v2)))
    | Disj (e1, e2) ->
      (match visit e1 with
	| None -> None
	| Some v1 ->
	  (match visit e2 with
	    | None -> None
	    | Some v2 ->
	      Some (v1 || v2)))
  in visit e


(* ex.5 *)
(* The data type of boolean expression:
   variables, negations, conjunctions and disjunctions *)
type bexp_nnf =
  | PosVar of name
  | NegVar of name
  | ConjNnf of bexp_nnf * bexp_nnf
  | DisjNnf of bexp_nnf * bexp_nnf


(* ex.7 *)
(* eval_nnf : bexp_nnf -> env -> bool *)
let rec eval_nnf bexp env = match bexp with
  | PosVar x ->
    (match lookup x env with
      | None -> raise (UNBOUND_VARIABLE x)
      | Some v -> v)
  | NegVar x ->
    (match lookup x env with
      | None -> raise (UNBOUND_VARIABLE x)
      | Some v -> not v)
  | ConjNnf (e1,e2) ->
    (eval_nnf e1 env) && (eval_nnf e2 env)
  | DisjNnf (e1,e2) ->
    (eval_nnf e1 env) || (eval_nnf e2 env)


(* ex.8 *)
(* normalize_boolean_expression : bexp -> bexp_nnf *)
let normalize_boolean_expression bexp = 
  let rec visit b pos_context = match b with
    | Var x -> 
      if pos_context
      then PosVar x
      else NegVar x
    | Neg e ->
      visit e (not pos_context)
    | Conj (e1,e2) ->
      if pos_context
      then ConjNnf (visit e1 pos_context, visit e2 pos_context)
      else DisjNnf (visit e1 pos_context, visit e2 pos_context)
    | Disj (e1,e2) ->
      if pos_context
      then DisjNnf (visit e1 pos_context, visit e2 pos_context)
      else ConjNnf (visit e1 pos_context, visit e2 pos_context)
  in
  visit bexp true