Natural_deduction : Main.expand_and_validate

let expand_and_validate_file ?(options = default_options) (path : string) : unit =
        let exp_items : t_itm list = ITM_main.expand_file path in
        let map (item : t_itm) : string =
                match item with
                |Prf prf -> (
                        match validate_prf ~options:options 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 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
                                String.concat "\n" [ITM_main.string_of_item (Prf valid_prf);report_string]
                        |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 proves_string : string = String.concat " " [premises_string; turnstile_of_options options; conclusion_string] in
                                let report_string : string = String.concat "" [
                                        "\n"; "# Proof is NOT valid";qualification_of_options options;".";"\n";
                                        "# Does NOT prove "; proves_string; ".\n";
                                ]
                                in
                                String.concat "\n" [ITM_main.string_of_item (Prf prf);report_string]
                )       
                |Def_prf (p, prf) -> (
                        match validate_prf ~options:options 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 proves_string : string = String.concat " " [premises_string; turnstile_of_options options; conclusion_string] in
                                let report_string : string = String.concat "" [
                                        "\n"; "# ";string_of_prf p;" is VALID";qualification_of_options options;"."; "\n";
                                        "# PROVES "; proves_string; ".\n";
                                ] 
                                in
                                String.concat "\n" [ITM_main.string_of_item (Def_prf (p,valid_prf));report_string]
                        |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 proves_string : string = String.concat " " [premises_string; turnstile_of_options options; conclusion_string] in
                                let report_string : string = String.concat "" [
                                        "\n"; "# ";string_of_prf p;" is NOT valid";qualification_of_options options;".";"\n";
                                        "# Does NOT prove "; proves_string; ".\n";
                                ]
                                in
                                String.concat "\n" [ITM_main.string_of_item (Def_prf (p, prf));report_string]
                )
                |Def_fml _ | Comment _ -> ITM_main.string_of_item item
        in IO.print_to_stdout (String.concat "\n\n" (List.map map exp_items))