type formula =
    | Var of string
    | Bot
    | Top
    | Neg of formula
    | And of formula * formula
    | Or of formula * formula

type env = string -> bool

let rec string_of_formula = function
    | Var(v) -> v
    | Bot -> "_|_"
    | Top -> "T"
    | Neg(f) -> "( - "^(string_of_formula f)^" )"
    | And(f1, f2) -> "( "^(string_of_formula f1)^" /\\ "^(string_of_formula f2)^" )"
    | Or(f1, f2) -> "( "^(string_of_formula f1)^" \\/ "^(string_of_formula f2)^" )"

let rec eval = function
    | Var(v) -> fun (s:env) -> s v
    | Bot -> fun _ -> false
    | Top -> fun _ -> true
    | Neg(f) -> fun s -> not (eval f s)
    | And(f1, f2) -> fun s -> (eval f1 s && eval f2 s)
    | Or(f1, f2) -> fun s -> (eval f1 s || eval f2 s)

let rec size = function
    | Var(_) | Bot | Top -> 1
    | Neg(f) -> 1 + size f
    | And(f1, f2) | Or(f1, f2) -> 1 + max (size f1) (size f2)

module VarSet = Set.Make(struct type t=string let compare = compare end)

let rec var = function
    | Var(v) -> VarSet.add v VarSet.empty
    | Top | Bot -> VarSet.empty
    | Neg(f) -> var f
    | Or(f1, f2) | And(f1, f2) -> VarSet.union (var f1) (var f2)


let rec random_tree h v =
    let random_var v =
        v.(Random.int (Array.length v))
    in
    if h = 1 then
      begin
        match Random.int 5 with
        | 0 | 1 | 2-> Var(random_var v)
        | 3 -> Top
        | _ -> Bot
      end
    else
        match Random.int 13 with
        | 0 | 1 -> Var(random_var v)
        | 2 -> Top
        | 3 -> Bot
        | 4 | 5 | 6 -> Neg(random_tree (h-1) v)
        | 7 | 8 | 9 -> And(random_tree (h-1) v, random_tree (h-1) v)
        | _ -> Or(random_tree (h-1) v, random_tree (h-1) v)

let valuation_to_function vars a = 
  let l = Array.length a in
  let rec valuation_to_function f n a =
    match n with
    | 0 -> f
    | n -> valuation_to_function (fun x -> if x == vars.(l-n) then a.(l-n) else f x) (n-1) a
  in
  valuation_to_function (fun _ -> false) l a

let enumerate v =
  let l = Array.length v in
  let next a =
    let rec aux i =
      if i == l then
        false
      else if not a.(i) then
        let () = a.(i) <- true in
        true
      else
        let () = a.(i) <- false in
        aux (i+1)
    in
    aux 0
  in
  let init = Array.init l (fun _ -> false) in
  let rec list_valuation a =
    let b = Array.copy a in
    a::(if next b then list_valuation b else [])
  in
  list_valuation init

let print_table formula =
  let vars = formula |> var |> VarSet.elements |> ArrayLabels.of_list in
  Array.iter
    (fun var ->
       Printf.printf "%s     | " var;
    )
    vars;
  Printf.printf "\n";
  List.iter
    (fun env -> Array.iter (fun b -> Printf.printf "%s | " (if b then "true " else "false")) env; Printf.printf "%b\n" (eval formula (valuation_to_function vars env)))
    (vars |> enumerate)

let () =
  Random.self_init();
  let vars = [|"A"; "B"; "C"|] in
  let rec f = function
      | 0 -> ()
      | n ->
        let formula = random_tree 5 vars in
        Printf.printf "%s\n" (string_of_formula formula);
        print_table formula;
        f (n-1)
  in
  f 1