--- a/src/HOL/Tools/ATP/res_clasimpset.ML Sun May 22 19:26:18 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Mon May 23 00:18:51 2005 +0200
@@ -1,4 +1,6 @@
+
(* ID: $Id$
+
Author: Claire Quigley
Copyright 2004 University of Cambridge
*)
@@ -10,32 +12,56 @@
structure ResClasimp : RES_CLASIMP =
struct
-
+fun has_name th = not((Thm.name_of_thm th )= "")
fun has_name_pair (a,b) = not_equal a "";
fun stick [] = []
| stick (x::xs) = x@(stick xs )
+fun filterlist p [] = []
+| filterlist p (x::xs) = if p x
+ then
+ (x::(filterlist p xs))
+ else
+ filterlist p xs
+
+
(* changed, now it also finds out the name of the theorem. *)
(* convert a theorem into CNF and then into Clause.clause format. *)
-fun clausify_axiom_pairs thm =
- let val thm_name = Thm.name_of_thm thm
- val isa_clauses = ResAxioms.cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
- val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses
- val clauses_n = length isa_clauses
- fun make_axiom_clauses _ [] []= []
- | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss'
- in
- make_axiom_clauses 0 isa_clauses' isa_clauses
- end;
+
+(* outputs a list of (thm,clause) pairs *)
-fun clausify_rules_pairs [] err_list = ([],err_list)
- | clausify_rules_pairs (thm::thms) err_list =
- let val (ts,es) = clausify_rules_pairs thms err_list
- in
- ((clausify_axiom_pairs thm)::ts,es) handle _ => (ts,(thm::es))
- end;
+(* for tracing: encloses each string element in brackets. *)
+fun concat_with_stop [] = ""
+ | concat_with_stop [x] = x
+ | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs;
+
+fun remove_symb str = if String.isPrefix "List.op @." str
+ then
+ ((String.substring(str,0,5))^(String.extract (str, 10, NONE)))
+ else
+ str
+
+fun remove_spaces str = let val strlist = String.tokens Char.isSpace str
+ val spaceless = concat strlist
+ val strlist' = String.tokens Char.isPunct spaceless
+ in
+ concat_with_stop strlist'
+ end
+
+fun remove_symb_pair (str, thm) = let val newstr = remove_symb str
+ in
+ (newstr, thm)
+ end
+
+
+fun remove_spaces_pair (str, thm) = let val newstr = remove_spaces str
+ in
+ (newstr, thm)
+ end
+
+
(*Insert th into the result provided the name is not "".*)
@@ -44,12 +70,14 @@
fun write_out_clasimp filename = let
val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
- val named_claset = List.foldr add_nonempty [] claset_rules;
- val claset_cls_thms = #1( clausify_rules_pairs named_claset []);
+ val named_claset = filterlist has_name_pair claset_rules;
+ val claset_names = map remove_spaces_pair (named_claset)
+ val claset_cls_thms = #1( ResAxioms.clausify_rules_pairs named_claset []);
+
val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
- val named_simpset = map #2(List.filter has_name_pair simpset_rules);
- val simpset_cls_thms = #1 (clausify_rules_pairs named_simpset []);
+ val named_simpset = map remove_spaces_pair (filterlist has_name_pair simpset_rules);
+ val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
val cls_thms = (claset_cls_thms@simpset_cls_thms);
val cls_thms_list = stick cls_thms;
@@ -79,3 +107,4 @@
end;
+