exception Error of string
exception NotFound

type node =
  | Entail of node * node
  | Consistent of node * node
  | Inconsistent of node * node
  | Equivalent of node * node
  | Conjunct of node * node
  | Sum of node * node
  | NotEquivalent of node * node
  | Contradict of node
  | Terminal of char
(*
type subst = (char * node) list

type proof = (node * node * subst) list
*)

let rec print_node = function
  | Entail(a,b) ->
    print_string "(";
    print_node a;
    print_string " E ";
    print_node b;
    print_string ")";
  | Consistent(a,b) ->
    print_string "(";
    print_node a;
    print_string " o ";
    print_node b;
    print_string ")";
  | Inconsistent(a,b) ->
    print_string "(";
    print_node a;
    print_string " | ";
    print_node b;
    print_string ")";
  | Equivalent(a,b) ->
    print_string "(";
    print_node a;
    print_string " = ";
    print_node b;
    print_string ")";
  | Conjunct(a,b) ->
    print_string "(";
    print_node a;
    print_string " . ";
    print_node b;
    print_string ")";
  | Sum(a,b) ->
    print_string "(";
    print_node a;
    print_string " V ";
    print_node b;
    print_string ")";
  | NotEquivalent(a,b) ->
    print_string "(";
    print_node a;
    print_string " <> ";
    print_node b;
    print_string ")";
  | Contradict(a) ->
    print_string "-";
    print_node a;
  | Terminal(a) ->
    print_char a

let known_truths = [
  (* Definitions *)
  Equivalent(
    Inconsistent(Terminal 'p', Terminal 'q'),
    Contradict(Consistent(Terminal 'p', Terminal 'q')));

  Equivalent(
    Entail(Terminal 'p', Terminal 'q'),
    Inconsistent(Terminal 'p', Contradict(Terminal 'q')));

  Equivalent(
    Inconsistent(
      Contradict(Terminal 'p'),
      Contradict(Terminal 'q')),
    Sum(Terminal 'p', Terminal 'q'));

  Equivalent(
    Equivalent(Terminal 'p', Terminal 'q'),
    Conjunct(
      Entail(Terminal 'p', Terminal 'q'),
      Entail(Terminal 'q', Terminal 'p')));

  (* Postulates *)

  (* p entails itself *)
  Entail(Terminal 'p', Terminal 'p');

  (* If p is inconsistent with q then q is inconsistent with p *)
  Entail(
    Inconsistent(Terminal 'p', Terminal 'q'),
    Inconsistent(Terminal 'q', Terminal 'p'));

  (* p entails its double negation *)
  Entail(Terminal 'p', Contradict (Contradict (Terminal 'p')));

  (* If p entails q then p is consistent with q *)
  Entail(
    Entail(Terminal 'p', Terminal 'q'),
    Consistent(Terminal 'p', Terminal 'q'));

  (* The tricky one *)
  Entail(
    Conjunct(
      NotEquivalent(Terminal 'p', Terminal 'q'),
      Conjunct(
        NotEquivalent(Terminal 'p', Terminal 'r'),
        NotEquivalent(Terminal 'q', Terminal 'r'))),
    Entail(
      Conjunct(
        Entail(Terminal 'p', Terminal 'q'),
        Entail(Terminal 'q', Terminal 'r')),
      Entail(Terminal 'p', Terminal 'r')));

  (* commutative conjunction *)
  Equivalent(
    Conjunct(Terminal 'p', Terminal 'q'),
    Conjunct(Terminal 'q', Terminal 'p'));

  (* hm. *)
  Entail(
    Entail(
      Conjunct(Terminal 'p', Terminal 'q'),
      Terminal 'r'),
    Entail(
      Conjunct(Terminal 'p', Contradict(Contradict(Terminal 'q'))),
      Contradict(Terminal 'q')));

  Equivalent(
    Terminal 'p',
    Contradict( Contradict( Terminal 'p')));

  ]
  

let rec print_truths = function
  | [] -> 1
  | truth::tail ->
    print_node truth;
    print_newline();
    print_truths tail

let rec equivalent x y =
  match x, y with
  | Entail(a,b), Entail(c,d)
  | Consistent(a,b), Consistent(c,d)
  | Inconsistent(a,b), Inconsistent(c,d)
  | Equivalent(a,b), Equivalent(c,d)
  | Conjunct(a,b), Conjunct(c,d)
  | NotEquivalent(a,b), NotEquivalent(c,d)
  | Sum(a,b), Sum(c,d) ->
    (equivalent a c) && (equivalent b d)
  | Contradict(a), Contradict(b) ->
    equivalent a b
  | Terminal(a), Terminal(b) -> a == b
  | _ -> false

let rec similar' x y env =
  match x, y with
  | Entail(a,b), Entail(c,d)
  | Consistent(a,b), Consistent(c,d)
  | Inconsistent(a,b), Inconsistent(c,d)
  | Equivalent(a,b), Equivalent(c,d)
  | Conjunct(a,b), Conjunct(c,d)
  | NotEquivalent(a,b), NotEquivalent(c,d)
  | Sum(a,b), Sum(c,d) ->
    (similar' a c env) && (similar' b d env)
  | Contradict(a), Contradict(b) ->
    similar' a b env
  | Terminal(a), Terminal(b) ->
    if (List.mem_assoc a env) then
      let assoc = List.assoc a env in
      assoc == b
    else
      let new_env = (a, b) :: env in
      true
  | _ -> false

let similar x y = similar' x y []

(* A is the base *)
let rec check_match' a b env = match a,b  with
  | Terminal(p), _ ->
    if (List.mem_assoc p env) then
      let assoc = List.assoc p env in
      env, equivalent assoc b
    else
      let new_env = (p, b) :: env in
      new_env, true
    (* Any of these *)
  | Entail(a,b), Entail(c,d)
  | Consistent(a,b), Consistent(c,d)
  | Inconsistent(a,b), Inconsistent(c,d)
  | Equivalent(a,b), Equivalent(c,d)
  | Conjunct(a,b), Conjunct(c,d)
  | NotEquivalent(a,b), NotEquivalent(c,d)
  | Sum(a,b), Sum(c,d) ->
    let (newenv, result) = (check_match' a c env) in
    let (newenv, result2) = (check_match' b d newenv) in
    (newenv, result && result2)
  | Contradict(a), Contradict(b) ->
    check_match' a b env
  | _ -> env, false

let check_match a b =
  let (newenv, result) = check_match' a b [] in
  result

let rec apply env = function
  | Entail(a,b) -> Entail(apply env a, apply env b)
  | Consistent(a,b) -> Consistent(apply env a, apply env b)
  | Inconsistent(a,b) -> Inconsistent(apply env a, apply env b)
  | Equivalent(a,b) -> Equivalent(apply env a, apply env b)
  | Conjunct(a,b) -> Conjunct(apply env a, apply env b)
  | NotEquivalent(a,b) -> NotEquivalent(apply env a, apply env b)
  | Sum(a,b) -> Sum(apply env a, apply env b)
  | Contradict(a) -> Contradict(apply env a)
  | Terminal(a) -> List.assoc a env

let print_env = function
  | [] -> ()
  | (a, b) :: t ->
    print_char a;
    print_char '/';
    print_node b;
    print_char ';'

let rec match_backward goal = function
  | [] -> []
  | truth::tail ->
    let env, result = check_match' truth goal [] in
    if result then
      (apply env truth, truth, env) :: match_backward goal tail
    else try begin
      match truth with
      | Entail(a, b) as rule ->
        let env, result = check_match' b goal [] in
        if result then
          (apply env a, rule, env) :: match_backward goal tail
        else raise NotFound
      | Equivalent(a, b) as rule ->
        let env, result = check_match' a goal [] in
        if result then
          (apply env b, rule, env) :: (match_backward goal tail)
        else
          let env, result = check_match' b goal [] in
          if result then
            (apply env a, rule, env) :: match_backward goal tail
          else raise NotFound
      | _ -> raise (Error "DEATH!")
    end with
      | NotFound -> match_backward goal tail

let rec print_deriv' prev_rule prev_env line = function
  | [] -> print_newline()
  | (result, rule, env)::t ->
    print_string "(";
    print_int line;
    print_string ") ";
    print_node result;
    print_string "\t\t";
    print_node prev_rule;
    print_string "\t";
    print_env prev_env;
    print_newline();
    print_deriv' rule env (line + 1) t

let print_deriv = function
  | [] -> print_newline()
  | (result, rule, env)::t as n->
    print_deriv' result [] 1 n

let rec no_duplication primary = function
  | [] -> true
  | (move, rule, subs)::rest ->
    if (equivalent primary move) then
      false
    else no_duplication primary rest

let rec is_member move = function
  | [] -> false
  (* | h::t -> (similar move h) or (is_member move t) *)
  | h::t -> (check_match h move) or (is_member move t)

let rec subproof truths move attempt =
  match move with
  | Conjunct(a, b) ->
    print_string "Trying subproofs of: ";
    print_node move;
    print_newline();
    let proof1 = prove truths a in
    let proof2 = prove truths b in
    if ((proof1 == []) or (proof2 == [])) then
      false, []
    else true, proof1 @ proof2 @ attempt
  | _ -> false, []

and prove' truths queue =
  try begin
    let attempt = Queue.take queue in
    match attempt with
    | [] -> raise NotFound
    | (move, rule, subs)::rest ->
      if (no_duplication move rest) then begin
        print_string "Testing: ";
        print_node move;
        print_newline();
        (* Check to see if this move reaches a truth *)
        if (is_member move truths) then
          attempt
        else
          let (gotone, proof) = subproof truths move attempt in
          if gotone then proof else
          (* Build list of legal moves from here *)
          let legal_moves = match_backward move truths in
          (* Mangle the list and add each to the queue *)
          let queue_move move =
            Queue.add (move :: attempt) queue in
          let _ = List.iter queue_move legal_moves in
          prove' truths queue
      end else
        (* Duplication found, skip this one *)
        prove' truths queue
  end with Queue.Empty -> print_string "EMPTY QUEUE!\n"; []

(* Wrapper to prove a theorm *)
and prove truths theorm =
  let base = [(theorm, theorm, [])] in
  let queue = Queue.create() in
  Queue.add base queue;
  prove' truths queue

let wanted_proofs = [
  (* Part of Lemma 1: --pEp *)
  Entail ((Contradict (Contradict (Terminal 'p'))), Terminal 'p');

  (* Lemma 1: p = --p *)
  Equivalent (
    Contradict (Contradict (Terminal 'p')), Terminal 'p');

  (* (a) p|-p *)
  Inconsistent (Terminal 'p', Contradict (Terminal 'p'));

  (* (b) pV-p *)
  Sum (Terminal 'p', Contradict(Terminal 'p'));

  (* (c) pop *)
  Consistent (Terminal 'p', Terminal 'p');

  (* (d) pEq . = . -pVq *)
  Equivalent (
    Entail (Terminal 'p', Terminal 'q'),
    Sum (Contradict (Terminal 'p'), Terminal 'q'));

  (* (e) pEq . = . -qE-p *)
  Equivalent (
    Entail (Terminal 'p', Terminal 'q'),
    Entail (Contradict (Terminal 'q'), Contradict (Terminal 'p')));

  (* (f) poq . E . -(pE-q) *)
  Entail (
    Consistent (Terminal 'p', Terminal 'q'),
    Contradict (
      Entail (Terminal 'p', Contradict (Terminal 'q'))));

  (* (g) -(pE-p) *)
  Contradict (
    Entail (Terminal 'p', Contradict (Terminal 'p')));

  (* (h) p|q . E . po-q *)
  Entail (
    Inconsistent (Terminal 'p', Terminal 'q'),
    Consistent (Terminal 'p', Contradict (Terminal 'q')));

  (* (i) pEq . E . -(pE-q) *)
  Entail (
    Entail (Terminal 'p', Terminal 'q'),
    Contradict (
      Entail (Terminal 'p', Contradict (Terminal 'q'))));

  (* (j) pqEr . = . p-rE-q . = . q-rE-p *)
  (* (k) pqor . = . proq . = . qrop *)
]


let rec many_proofs = function
  | [] -> print_newline()
  | h::t ->
    print_string "Trying to prove: ";
    print_node h;
    print_newline();
    let proof = prove known_truths h in
    print_string "Proof:\n";
    print_deriv proof;
    print_newline();
    many_proofs t


let _ = many_proofs wanted_proofs