Natural_deduction : Main.validate

let validate_prf ?(options = default_options) (prf : t_prf) : t_prf option =
        let dischargeable (fml : t_fml) : int option = None in
        match validate options 0 0 dischargeable [] prf with
        |Some valid_prf ->
                let premises : t_fml list = premises_of_prf [] valid_prf in
                let conclusion : t_fml = conclusion_of_prf valid_prf in
                let premises_string : string = string_of_premises premises in
                let conclusion_string : string = string_of_fml conclusion in
                let proof_string : string = string_of_prf valid_prf in
                let proves_string : string = String.concat " " [premises_string; turnstile_of_options options; conclusion_string] in
                let report_string : string = String.concat "" [
                        "\n"; "Proof is VALID";qualification_of_options options;"."; "\n";
                        "PROVES "; proves_string; ".\n";
                ] 
                in
                let _ : unit = if not options.quiet then IO.print_to_stderr report_string else () in
                let _ : unit = if not options.quiet then IO.print_to_stdout proof_string else () in
                Some valid_prf
        |None ->
                let premises : t_fml list = premises_of_prf [] prf in
                let conclusion : t_fml = conclusion_of_prf prf in
                let premises_string : string = string_of_premises premises in
                let conclusion_string : string = string_of_fml conclusion in
                let proof_string : string = string_of_prf prf in
                let proves_string : string = String.concat " " [premises_string; turnstile_of_options options; conclusion_string] in
                let report_string : string = String.concat "" [
                        proof_string;"\n";
                        "\n"; "Proof is NOT valid";qualification_of_options options;".";"\n";
                        "Does NOT prove "; proves_string; ".\n";
                ]
                in
                let _ : unit = if not options.quiet then IO.print_to_stderr report_string else () in
                None