# HG changeset patch # User paulson # Date 1138726108 -3600 # Node ID 00741f7280f7670a137df363a93e17b7d1674b43 # Parent 7cfc21ee0370a3f4cc5bb7c2e04dd4111d7b87f1 removal of ResClause.num_of_clauses and other simplifications diff -r 7cfc21ee0370 -r 00741f7280f7 src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue Jan 31 16:37:06 2006 +0100 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue Jan 31 17:48:28 2006 +0100 @@ -204,17 +204,6 @@ fun put_name_pair ("",th) = (fake_thm_name th, th) | put_name_pair (a,th) = (a,th); -(* outputs a list of (thm,clause) pairs *) - -fun multi x 0 xlist = xlist - |multi x n xlist = multi x (n-1) (x::xlist); - -fun clause_numbering ((clause, theorem), num_of_cls) = - let val numbers = 0 upto (num_of_cls - 1) - in - multi (clause, theorem) num_of_cls [] - end; - (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*) exception HASH_CLAUSE and HASH_STRING; @@ -263,17 +252,8 @@ val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (simpset_cls_thms@claset_cls_thms)) val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals - (* Identify the set of clauses to be written out *) - val clauses = map #1 (relevant_cls_thms_list); - val cls_nums = map ResClause.num_of_clauses clauses; - (*Note: in every case, cls_num = 1. I think that only conjecture clauses - can have any other value.*) - val whole_list = List.concat - (map clause_numbering (ListPair.zip (relevant_cls_thms_list, cls_nums))); in (* create array of put clausename, number pairs into it *) - assert (map #1 whole_list = clauses) "get_clasimp_lemmas"; - (*So get rid of cls_nums and clause_numbering; return simply cls_thms_list*) - (Array.fromList whole_list, clauses) + (Array.fromList relevant_cls_thms_list, map #1 (relevant_cls_thms_list)) end; diff -r 7cfc21ee0370 -r 00741f7280f7 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Tue Jan 31 16:37:06 2006 +0100 +++ b/src/HOL/Tools/res_clause.ML Tue Jan 31 17:48:28 2006 +0100 @@ -45,7 +45,6 @@ val make_type_class : string -> string val mk_fol_type: string * string * fol_type list -> fol_type val mk_typ_var_sort : Term.typ -> typ_var * sort - val num_of_clauses : clause -> int val paren_pack : string list -> string val schematic_var_prefix : string val special_equal : bool ref @@ -190,7 +189,7 @@ type polarity = bool; -(* "tag" is used for vampire specific syntax *) +(* "tag" is used for vampire specific syntax FIXME REMOVE *) type tag = bool; @@ -236,9 +235,9 @@ axiom_name: axiom_name, kind: kind, literals: literal list, - types_sorts: (typ_var * sort) list, - tvar_type_literals: type_literal list, - tfree_type_literals: type_literal list}; + types_sorts: (typ_var * sort) list}; + +fun get_axiomName (Clause cls) = #axiom_name cls; exception CLAUSE of string * term; @@ -254,24 +253,12 @@ fun isTaut (Clause {literals,...}) = exists isTrue literals; -fun make_clause (clause_id,axiom_name,kind,literals, - types_sorts,tvar_type_literals,tfree_type_literals) = +fun make_clause (clause_id, axiom_name, kind, literals, types_sorts) = if forall isFalse literals then error "Problem too trivial for resolution (empty clause)" else Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, - literals = literals, types_sorts = types_sorts, - tvar_type_literals = tvar_type_literals, - tfree_type_literals = tfree_type_literals}; - - -(** Some Clause destructor functions **) - -fun string_of_kind (Clause cls) = name_of_kind (#kind cls); - -fun get_axiomName (Clause cls) = #axiom_name cls; - -fun get_clause_id (Clause cls) = #clause_id cls; + literals = literals, types_sorts = types_sorts}; (*Declarations of the current theory--to allow suppressing types.*) @@ -588,10 +575,7 @@ end; -fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls) - - -(** make axiom clauses, hypothesis clauses and conjecture clauses. **) +(** make axiom and conjecture clauses. **) fun get_tvar_strs [] = [] | get_tvar_strs ((FOLTVar indx,s)::tss) = @@ -603,23 +587,18 @@ fun make_axiom_clause_thm thm (ax_name,cls_id) = let val (lits,types_sorts) = literals_of_term (prop_of thm) - val lits' = sort_lits lits - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts in - make_clause(cls_id,ax_name,Axiom, - lits',types_sorts,tvar_lits,tfree_lits) + make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts) end; -(* check if a clause is FOL first*) +(* check if a clause is first-order before making a conjecture clause*) fun make_conjecture_clause n t = let val _ = check_is_fol_term t handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t) val (lits,types_sorts) = literals_of_term t - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts in - make_clause(n,"conjecture",Conjecture, - lits,types_sorts,tvar_lits,tfree_lits) + make_clause(n, "conjecture", Conjecture, lits, types_sorts) end; fun make_conjecture_clauses_aux _ [] = [] @@ -635,10 +614,8 @@ handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) val (lits,types_sorts) = literals_of_term term val lits' = sort_lits lits - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts in - make_clause(cls_id,ax_name,Axiom, - lits',types_sorts,tvar_lits,tfree_lits) + make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts) end; @@ -684,14 +661,6 @@ conclLit = make_TConsLit(true, (res,tcons,tvars)), premLits = map make_TVarLit false_tvars_srts'} end; - -(*The number of clauses generated from cls, including type clauses. It's always 1 - except for conjecture clauses.*) -fun num_of_clauses (Clause cls) = - let val num_tfree_lits = - if !keep_types then length (#tfree_type_literals cls) - else 0 - in 1 + num_tfree_lits end; (**** Isabelle class relations ****) @@ -873,14 +842,13 @@ dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^ string_of_clausename (cls_id,ax_name) ^ ").\n\n"; -fun dfg_clause_aux (Clause{literals, tvar_type_literals, tfree_type_literals, ...}) = +fun dfg_clause_aux (Clause{literals, types_sorts, ...}) = let val lits = map dfg_literal literals + val (tvar_lits,tfree_lits) = add_typs_aux types_sorts val tvar_lits_strs = - if !keep_types then map dfg_of_typeLit tvar_type_literals - else [] + if !keep_types then map dfg_of_typeLit tvar_lits else [] val tfree_lits = - if !keep_types then map dfg_of_typeLit tfree_type_literals - else [] + if !keep_types then map dfg_of_typeLit tfree_lits else [] in (tvar_lits_strs @ lits, tfree_lits) end; @@ -985,10 +953,7 @@ end; -(********************************) -(* code to produce TPTP files *) -(********************************) - +(**** Produce TPTP files ****) (*Attach sign in TPTP syntax: false means negate.*) fun tptp_sign true s = "++" ^ s @@ -1006,7 +971,6 @@ fun tptp_of_typeLit (LTVar (s,ty)) = "--" ^ s ^ "(" ^ ty ^ ")" | tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")"; - fun gen_tptp_cls (cls_id,ax_name,knd,lits) = "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ knd ^ "," ^ lits ^ ").\n"; @@ -1015,53 +979,29 @@ "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ knd ^ ",[" ^ tfree_lit ^ "]).\n"; -fun tptp_type_lits (Clause cls) = - let val lits = map tptp_literal (#literals cls) - val tvar_lits_strs = - if !keep_types - then (map tptp_of_typeLit (#tvar_type_literals cls)) - else [] - val tfree_lits = - if !keep_types - then (map tptp_of_typeLit (#tfree_type_literals cls)) - else [] +fun tptp_type_lits (Clause {literals, types_sorts, ...}) = + let val lits = map tptp_literal literals + val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + val tvar_lits_strs = + if !keep_types then map tptp_of_typeLit tvar_lits else [] + val tfree_lits = + if !keep_types then map tptp_of_typeLit tfree_lits else [] in (tvar_lits_strs @ lits, tfree_lits) end; -fun tptp_clause cls = +fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) = let val (lits,tfree_lits) = tptp_type_lits cls (*"lits" includes the typing assumptions (TVars)*) - val cls_id = get_clause_id cls - val ax_name = get_axiomName cls - val knd = string_of_kind cls - val lits_str = bracket_pack lits - val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) - fun typ_clss k [] = [] - | typ_clss k (tfree :: tfrees) = - gen_tptp_type_cls(cls_id,ax_name,knd,tfree,k) :: - typ_clss (k+1) tfrees - in - cls_str :: (typ_clss 0 tfree_lits) - end; - -fun clause2tptp cls = - let val (lits,tfree_lits) = tptp_type_lits cls - (*"lits" includes the typing assumptions (TVars)*) - val cls_id = get_clause_id cls - val ax_name = get_axiomName cls - val knd = string_of_kind cls - val lits_str = bracket_pack lits - val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) + val knd = name_of_kind kind + val cls_str = gen_tptp_cls(clause_id, axiom_name, knd, bracket_pack lits) in (cls_str,tfree_lits) end; - fun tptp_tfree_clause tfree_lit = "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n"; - fun tptp_of_arLit (TConsLit(b,(c,t,args))) = tptp_sign b (c ^ "(" ^ t ^ paren_pack args ^ ")") | tptp_of_arLit (TVarLit(b,(c,str))) = @@ -1092,7 +1032,7 @@ val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss) val out = TextIO.openOut filename in - List.app (writeln_strs out o tptp_clause) axclauses; + List.app (curry TextIO.output out o #1 o clause2tptp) axclauses; writeln_strs out tfree_clss; writeln_strs out tptp_clss; List.app (curry TextIO.output out o tptp_classrelClause) classrel_clauses;