# HG changeset patch # User mengj # Date 1159619556 -7200 # Node ID 497e1c9d4a9f23cbc25635c2b5d86b0fbb8b64b4 # Parent a9595fdc02b1bfb6d13b6d5b479ab5578a427139 Combinator axioms are now from Isabelle theorems, no need to use helper files. Removed LAM2COMB exception. diff -r a9595fdc02b1 -r 497e1c9d4a9f src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Sat Sep 30 14:31:41 2006 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Sat Sep 30 14:32:36 2006 +0200 @@ -9,6 +9,20 @@ struct +(* theorems for combinators and function extensionality *) +val ext = thm "HOL.ext"; +val comb_I = thm "Reconstruction.COMBI_def"; +val comb_K = thm "Reconstruction.COMBK_def"; +val comb_B = thm "Reconstruction.COMBB_def"; +val comb_C = thm "Reconstruction.COMBC_def"; +val comb_S = thm "Reconstruction.COMBS_def"; +val comb_B' = thm "Reconstruction.COMBB'_def"; +val comb_C' = thm "Reconstruction.COMBC'_def"; +val comb_S' = thm "Reconstruction.COMBS'_def"; +val fequal_imp_equal = thm "Reconstruction.fequal_imp_equal"; +val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal"; + + (* a flag to set if we use extra combinators B',C',S' *) val use_combB'C'S' = ref true; @@ -56,8 +70,6 @@ | is_free _ _ = false; -exception LAM2COMB of term; - exception BND of term; fun decre_bndVar (Bound n) = Bound (n-1) @@ -202,7 +214,7 @@ compact_comb (Const("COMBS",tS) $ P' $ Q') Bnds count_comb end))) end - | lam2comb (t as (Abs(x,t1,_))) _ _ = raise LAM2COMB (t); + | lam2comb (t as (Abs(x,t1,_))) _ _ = raise ResClause.CLAUSE("HOL CLAUSE",t); (*********************) @@ -841,37 +853,26 @@ (* write clauses to files *) (**********************************************************************) -(* tptp format *) - -fun read_in fs = map (File.read o File.unpack_platform_path) fs; +local -fun get_helper_tptp () = - let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K";["combIK.tptp"]) else [] - val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C";["combBC.tptp"]) else [] - val S = if !combS_count > 0 then (Output.debug "Include combinator S";["combS.tptp"]) else [] - val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; ["combBC_e.tptp"]) else [] - val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'";["combS_e.tptp"]) else [] - in - ("helper1.tptp") :: (IK @ BC @ S @ B'C' @ S') - end; +val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname) +in -fun get_helper_clauses_tptp () = - let val tlevel = case !typ_level of - T_FULL => (Output.debug "Fully-typed HOL"; - "~~/src/HOL/Tools/atp-inputs/full_") - | T_PARTIAL => (Output.debug "Partially-typed HOL"; - "~~/src/HOL/Tools/atp-inputs/par_") - | T_CONST => (Output.debug "Const-only-typed HOL"; - "~~/src/HOL/Tools/atp-inputs/const_") - | T_NONE => (Output.debug "Untyped HOL"; - "~~/src/HOL/Tools/atp-inputs/u_") - val helpers = get_helper_tptp () - val t_helpers = map (curry (op ^) tlevel) helpers - in - read_in t_helpers - end; - +fun get_helper_clauses () = + let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) else [] + val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C"; cnf_helper_thms [comb_B,comb_C]) else [] + val S = if !combS_count > 0 then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) else [] + val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; cnf_helper_thms [comb_B', comb_C']) else [] + val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) else [] + val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal] + in + make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') [] + end + +end + +(* tptp format *) (* write TPTP format to a single file *) (* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *) @@ -881,47 +882,21 @@ val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss) val out = TextIO.openOut filename - val helper_clauses = get_helper_clauses_tptp () + val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) () in List.app (curry TextIO.output out o #1 o clause2tptp) axclauses'; ResClause.writeln_strs out tfree_clss; ResClause.writeln_strs out tptp_clss; List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses; List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses; - List.app (curry TextIO.output out) helper_clauses; + List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses; TextIO.closeOut out; clnames end; -fun get_helper_dfg () = - let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K";["combIK.dfg"]) else [] - val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C";["combBC.dfg"]) else [] - val S = if !combS_count > 0 then (Output.debug "Include combinator S";["combS.dfg"]) else [] - val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; ["combBC_e.dfg"]) else [] - val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'";["combS_e.dfg"]) else [] - in - ("helper1.dfg") :: (IK @ BC @ S @ B'C' @ S') - end; - (* dfg format *) -fun get_helper_clauses_dfg () = - let val tlevel = case !typ_level of - T_FULL => (Output.debug "Fully-typed HOL"; - "~~/src/HOL/Tools/atp-inputs/full_") - | T_PARTIAL => (Output.debug "Partially-typed HOL"; - "~~/src/HOL/Tools/atp-inputs/par_") - | T_CONST => (Output.debug "Const-only-typed HOL"; - "~~/src/HOL/Tools/atp-inputs/const_") - | T_NONE => (Output.debug "Untyped HOL"; - "~~/src/HOL/Tools/atp-inputs/u_") - val helpers = get_helper_dfg () - val t_helpers = map (curry (op ^) tlevel) helpers - in - read_in t_helpers - end; - fun dfg_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas = let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) @@ -935,7 +910,8 @@ val (axstrs,_) = ListPair.unzip (map clause2dfg axclauses') val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss) val out = TextIO.openOut filename - val helper_clauses = get_helper_clauses_dfg () + val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) () + val helper_clauses_strs = (#1 o ListPair.unzip o (map clause2dfg)) helper_clauses in TextIO.output (out, ResClause.string_of_start probname); TextIO.output (out, ResClause.string_of_descrip probname); @@ -944,7 +920,7 @@ ResClause.writeln_strs out axstrs; List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses; List.app (curry TextIO.output out o ResClause.dfg_arity_clause) arity_clauses; - ResClause.writeln_strs out helper_clauses; + ResClause.writeln_strs out helper_clauses_strs; TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); ResClause.writeln_strs out tfree_clss; ResClause.writeln_strs out dfg_clss;