open Syntax
open Printf


let rec proof_checker tree lst =
  match tree with
  | Ax(p) -> if List.mem p lst
             then p
             else failwith "Not on list"
  | TopI -> Top
  | ConjI(p1, p2) -> Conj((proof_checker p1 lst), (proof_checker p2 lst))
  | DisjIL(p1, prop) -> Disj((proof_checker p1 lst) , prop)
  | DisjIR(prop, p2) -> Disj(prop, (proof_checker p2 lst))
  | ImplI((prop, pt)) -> Impl(prop, proof_checker pt (prop::lst))
  | BotE(prop) -> prop
  | ConjEL(pt) -> let assump = proof_checker pt lst in
                  begin
                  match assump with
                  | Conj(p1, p2) -> p1
                  | _ -> failwith "Not a conjuction"
                  end
  | ConjER(pt) -> let assump = proof_checker pt lst in
                  begin
                  match assump with
                  | Conj(p1, p2) -> p2
                  | _ -> failwith "Not a conjuction"
                  end
  | DisjE(pt, (prop1, hpt1), (prop2, hpt2)) ->
              let assump = proof_checker pt lst in
                  begin
                  match assump with
                  | Disj(p1, p2) -> if (p1 = prop1) && (p2 = prop2)
                                    then let proof1 = proof_checker hpt1 (p1::lst)
                                    in let proof2 = proof_checker hpt2 (p2::lst)
                                    in if proof1 = proof2
                                       then proof1
                                       else failwith "Proposals not equal"
                                    else failwith "Wrong hypothesis"
                  | _ -> failwith "Not a disjunction"
                  end
  |ImplE(pt1, pt2) -> let alpha = proof_checker pt1 lst
                          in let impli = proof_checker pt2 lst
                            in begin match impli with
                               | Impl(p1, p2) -> if p1 = alpha
                                                 then p2
                                                 else failwith "Wrong implication"
                               | _ -> failwith "Not an implication"  end



let is_in prop lst =
  List.mem prop lst;;

let intro prop lst =
  match prop with
  | Conj(p1, p2) -> (is_in p1 lst) && (is_in p2 lst)
  | Disj(p1, p2) -> (is_in p1 lst) || (is_in p2 lst)
  | _ -> false

let elim prop lst =
  let aux axiom =
    match prop with
    | Conj(p1, p2) -> (prop = p1) || (prop = p2)
    | Impl(p1, p2) -> (is_in p1 lst) && (prop = p2)
    | Disj(p1, p2) -> is_in (Impl(p1, prop)) lst && is_in (Impl(p2, prop)) lst
    | Bot -> true
    | _ -> false
  in List.exists aux lst

let check prop lst =
  is_in prop lst ||
  intro prop lst ||
  elim prop lst;;

let rec proof_checker_s script lst =
  match script with
  | PDone(prop) ->
    if (check prop lst)
    then prop
    else failwith "Pdone error"
  | PConc(prop, ps) ->
    if (check prop lst)
    then proof_checker_s ps (prop::lst)
    else failwith "PConc error"
  | PHyp((hprop, hps1), ps) ->
    let temp = proof_checker_s hps1 (hprop::lst)
      in proof_checker_s ps (Impl(hprop, temp)::lst)

let proofs_checker proofs =
  let aux proof =
    try
    begin
    match proof with
    | TGoal(name, prop, pt) ->
      if prop = proof_checker pt []
      then printf "%s OK\n" name
      else printf "%s FAIL\n" name
    | SGoal(name, prop, ps) ->
      if prop = proof_checker_s ps []
      then printf "%s OK\n" name
      else printf "%s FAIL\n" name
    end
    with (Failure msg) ->
      printf "EXCEPTION: %s\n" msg
  in List.map aux proofs

let _ =
  let lexbuf = Lexing.from_channel stdin in
  let proofs = Parser.file Lexer.token lexbuf
  (* powyższe wiersze wczytują listę dowodów ze standardowego wejścia
     i parsują ją do postaci zdefiniowanej w module Syntax *)
  in proofs_checker proofs