510 |
510 |
511 val type_wrapper = "typeinfo"; |
511 val type_wrapper = "typeinfo"; |
512 |
512 |
513 datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE; |
513 datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE; |
514 |
514 |
515 val typ_level = ref T_FULL; |
515 val typ_level = ref T_CONST; |
516 |
516 |
517 fun full_types () = (typ_level:=T_FULL); |
517 fun full_types () = (typ_level:=T_FULL); |
518 fun partial_types () = (typ_level:=T_PARTIAL); |
518 fun partial_types () = (typ_level:=T_PARTIAL); |
519 fun const_types_only () = (typ_level:=T_CONST); |
519 fun const_types_only () = (typ_level:=T_CONST); |
520 fun no_types () = (typ_level:=T_NONE); |
520 fun no_types () = (typ_level:=T_NONE); |
828 (* tptp format *) |
828 (* tptp format *) |
829 |
829 |
830 fun read_in fs = map (File.read o File.unpack_platform_path) fs; |
830 fun read_in fs = map (File.read o File.unpack_platform_path) fs; |
831 |
831 |
832 fun get_helper_clauses_tptp () = |
832 fun get_helper_clauses_tptp () = |
833 let val tlevel = case !typ_level of T_FULL => (warning "Fully-typed HOL"; "~~/src/HOL/Tools/atp-inputs/full_") |
833 let val tlevel = case !typ_level of |
834 | T_PARTIAL => (warning "Partially-typed HOL"; "~~/src/HOL/Tools/atp-inputs/par_") |
834 T_FULL => (Output.debug "Fully-typed HOL"; |
835 | T_CONST => (warning "Const-only-typed HOL"; "~~/src/HOL/Tools/atp-inputs/const_") |
835 "~~/src/HOL/Tools/atp-inputs/full_") |
836 | T_NONE => (warning "Untyped HOL"; "~~/src/HOL/Tools/atp-inputs/u_") |
836 | T_PARTIAL => (Output.debug "Partially-typed HOL"; |
837 val helpers = if !include_combS then (warning "Include combinator S"; ["helper1.tptp","comb_inclS.tptp"]) else |
837 "~~/src/HOL/Tools/atp-inputs/par_") |
838 if !include_min_comb then (warning "Include min combinators"; ["helper1.tptp","comb_noS.tptp"]) |
838 | T_CONST => (Output.debug "Const-only-typed HOL"; |
839 else (warning "No combinator is used"; ["helper1.tptp"]) |
839 "~~/src/HOL/Tools/atp-inputs/const_") |
840 val t_helpers = map (curry (op ^) tlevel) helpers |
840 | T_NONE => (Output.debug "Untyped HOL"; |
841 in |
841 "~~/src/HOL/Tools/atp-inputs/u_") |
842 read_in t_helpers |
842 val helpers = if !include_combS |
843 end; |
843 then (Output.debug "Include combinator S"; |
|
844 ["helper1.tptp","comb_inclS.tptp"]) |
|
845 else if !include_min_comb |
|
846 then (Output.debug "Include min combinators"; |
|
847 ["helper1.tptp","comb_noS.tptp"]) |
|
848 else (Output.debug "No combinator is used"; ["helper1.tptp"]) |
|
849 val t_helpers = map (curry (op ^) tlevel) helpers |
|
850 in |
|
851 read_in t_helpers |
|
852 end; |
844 |
853 |
845 |
854 |
846 (* write TPTP format to a single file *) |
855 (* write TPTP format to a single file *) |
847 (* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *) |
856 (* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *) |
848 fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) = |
857 fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) = |
863 end; |
872 end; |
864 |
873 |
865 |
874 |
866 (* dfg format *) |
875 (* dfg format *) |
867 fun get_helper_clauses_dfg () = |
876 fun get_helper_clauses_dfg () = |
868 let val tlevel = case !typ_level of T_FULL => (warning "Fully-typed HOL"; "~~/src/HOL/Tools/atp-inputs/full_") |
877 let val tlevel = case !typ_level of |
869 | T_PARTIAL => (warning "Partially-typed HOL"; "~~/src/HOL/Tools/atp-inputs/par_") |
878 T_FULL => (Output.debug "Fully-typed HOL"; |
870 | T_CONST => (warning "Const-only-typed HOL"; "~~/src/HOL/Tools/atp-inputs/const_") |
879 "~~/src/HOL/Tools/atp-inputs/full_") |
871 | T_NONE => (warning "Untyped HOL"; "~~/src/HOL/Tools/atp-inputs/u_") |
880 | T_PARTIAL => (Output.debug "Partially-typed HOL"; |
872 val helpers = if !include_combS then (warning "Include combinator S"; ["helper1.dfg","comb_inclS.dfg"]) else |
881 "~~/src/HOL/Tools/atp-inputs/par_") |
873 if !include_min_comb then (warning "Include min combinators"; ["helper1.dfg","comb_noS.dfg"]) |
882 | T_CONST => (Output.debug "Const-only-typed HOL"; |
874 else (warning "No combinator is used"; ["helper1.dfg"]) |
883 "~~/src/HOL/Tools/atp-inputs/const_") |
875 val t_helpers = map (curry (op ^) tlevel) helpers |
884 | T_NONE => (Output.debug "Untyped HOL"; |
876 in |
885 "~~/src/HOL/Tools/atp-inputs/u_") |
877 read_in t_helpers |
886 val helpers = if !include_combS |
878 end; |
887 then (Output.debug "Include combinator S"; |
|
888 ["helper1.dfg","comb_inclS.dfg"]) else |
|
889 if !include_min_comb |
|
890 then (Output.debug "Include min combinators"; |
|
891 ["helper1.dfg","comb_noS.dfg"]) |
|
892 else (Output.debug "No combinator is used"; ["helper1.dfg"]) |
|
893 val t_helpers = map (curry (op ^) tlevel) helpers |
|
894 in |
|
895 read_in t_helpers |
|
896 end; |
879 |
897 |
880 |
898 |
881 fun dfg_write_file thms filename (axclauses,classrel_clauses,arity_clauses) = |
899 fun dfg_write_file thms filename (axclauses,classrel_clauses,arity_clauses) = |
882 let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) |
900 let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) |
883 val conjectures = make_conjecture_clauses thms |
901 val conjectures = make_conjecture_clauses thms |