removal of ResClause.num_of_clauses and other simplifications
authorpaulson
Tue Jan 31 17:48:28 2006 +0100 (2006-01-31)
changeset 1886900741f7280f7
parent 18868 7cfc21ee0370
child 18870 020e242c02a0
removal of ResClause.num_of_clauses and other simplifications
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Jan 31 16:37:06 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Jan 31 17:48:28 2006 +0100
     1.3 @@ -204,17 +204,6 @@
     1.4  fun put_name_pair ("",th) = (fake_thm_name th, th)
     1.5    | put_name_pair (a,th)  = (a,th);
     1.6  
     1.7 -(* outputs a list of (thm,clause) pairs *)
     1.8 -
     1.9 -fun multi x 0 xlist = xlist
    1.10 -   |multi x n xlist = multi x (n-1) (x::xlist);
    1.11 -
    1.12 -fun clause_numbering ((clause, theorem), num_of_cls) = 
    1.13 -    let val numbers = 0 upto (num_of_cls - 1)
    1.14 -    in 
    1.15 -	multi (clause, theorem) num_of_cls []
    1.16 -    end;
    1.17 -    
    1.18  (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
    1.19  
    1.20  exception HASH_CLAUSE and HASH_STRING;
    1.21 @@ -263,17 +252,8 @@
    1.22        val cls_thms_list = make_unique (mk_clause_table 2200) 
    1.23                                        (List.concat (simpset_cls_thms@claset_cls_thms))
    1.24        val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter cls_thms_list goals
    1.25 -      (* Identify the set of clauses to be written out *)
    1.26 -      val clauses = map #1 (relevant_cls_thms_list);
    1.27 -      val cls_nums = map ResClause.num_of_clauses clauses;
    1.28 -      (*Note: in every case, cls_num = 1.  I think that only conjecture clauses
    1.29 -	can have any other value.*)
    1.30 -      val whole_list = List.concat 
    1.31 -	    (map clause_numbering (ListPair.zip (relevant_cls_thms_list, cls_nums)));
    1.32    in  (* create array of put clausename, number pairs into it *)
    1.33 -      assert (map #1 whole_list = clauses) "get_clasimp_lemmas";
    1.34 -      (*So get rid of cls_nums and clause_numbering; return simply cls_thms_list*)
    1.35 -      (Array.fromList whole_list, clauses)
    1.36 +      (Array.fromList relevant_cls_thms_list, map #1 (relevant_cls_thms_list))
    1.37    end;
    1.38  
    1.39  
     2.1 --- a/src/HOL/Tools/res_clause.ML	Tue Jan 31 16:37:06 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Jan 31 17:48:28 2006 +0100
     2.3 @@ -45,7 +45,6 @@
     2.4    val make_type_class : string -> string
     2.5    val mk_fol_type: string * string * fol_type list -> fol_type
     2.6    val mk_typ_var_sort : Term.typ -> typ_var * sort
     2.7 -  val num_of_clauses : clause -> int
     2.8    val paren_pack : string list -> string
     2.9    val schematic_var_prefix : string
    2.10    val special_equal : bool ref
    2.11 @@ -190,7 +189,7 @@
    2.12  
    2.13  type polarity = bool;
    2.14  
    2.15 -(* "tag" is used for vampire specific syntax  *)
    2.16 +(* "tag" is used for vampire specific syntax FIXME REMOVE *)
    2.17  type tag = bool; 
    2.18  
    2.19  
    2.20 @@ -236,9 +235,9 @@
    2.21  		    axiom_name: axiom_name,
    2.22  		    kind: kind,
    2.23  		    literals: literal list,
    2.24 -		    types_sorts: (typ_var * sort) list, 
    2.25 -                    tvar_type_literals: type_literal list, 
    2.26 -                    tfree_type_literals: type_literal list};
    2.27 +		    types_sorts: (typ_var * sort) list};
    2.28 +
    2.29 +fun get_axiomName (Clause cls) = #axiom_name cls;
    2.30  
    2.31  exception CLAUSE of string * term;
    2.32  
    2.33 @@ -254,24 +253,12 @@
    2.34    
    2.35  fun isTaut (Clause {literals,...}) = exists isTrue literals;  
    2.36  
    2.37 -fun make_clause (clause_id,axiom_name,kind,literals,
    2.38 -                 types_sorts,tvar_type_literals,tfree_type_literals) =
    2.39 +fun make_clause (clause_id, axiom_name, kind, literals, types_sorts) =
    2.40    if forall isFalse literals 
    2.41    then error "Problem too trivial for resolution (empty clause)"
    2.42    else
    2.43       Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, 
    2.44 -             literals = literals, types_sorts = types_sorts,
    2.45 -             tvar_type_literals = tvar_type_literals,
    2.46 -             tfree_type_literals = tfree_type_literals};
    2.47 -
    2.48 -
    2.49 -(** Some Clause destructor functions **)
    2.50 -
    2.51 -fun string_of_kind (Clause cls) = name_of_kind (#kind cls);
    2.52 -
    2.53 -fun get_axiomName (Clause cls) = #axiom_name cls;
    2.54 -
    2.55 -fun get_clause_id (Clause cls) = #clause_id cls;
    2.56 +             literals = literals, types_sorts = types_sorts};
    2.57  
    2.58  
    2.59  (*Declarations of the current theory--to allow suppressing types.*)
    2.60 @@ -588,10 +575,7 @@
    2.61        end;
    2.62  
    2.63  
    2.64 -fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls)  
    2.65 -
    2.66 -
    2.67 -(** make axiom clauses, hypothesis clauses and conjecture clauses. **)
    2.68 +(** make axiom and conjecture clauses. **)
    2.69  
    2.70  fun get_tvar_strs [] = []
    2.71    | get_tvar_strs ((FOLTVar indx,s)::tss) = 
    2.72 @@ -603,23 +587,18 @@
    2.73  
    2.74  fun make_axiom_clause_thm thm (ax_name,cls_id) =
    2.75      let val (lits,types_sorts) = literals_of_term (prop_of thm)
    2.76 -	val lits' = sort_lits lits
    2.77 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts  
    2.78      in 
    2.79 -	make_clause(cls_id,ax_name,Axiom,
    2.80 -	            lits',types_sorts,tvar_lits,tfree_lits)
    2.81 +	make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)
    2.82      end;
    2.83  
    2.84  
    2.85 -(* check if a clause is FOL first*)
    2.86 +(* check if a clause is first-order before making a conjecture clause*)
    2.87  fun make_conjecture_clause n t =
    2.88      let val _ = check_is_fol_term t
    2.89  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t)
    2.90  	val (lits,types_sorts) = literals_of_term t
    2.91 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts 
    2.92      in
    2.93 -	make_clause(n,"conjecture",Conjecture,
    2.94 -	            lits,types_sorts,tvar_lits,tfree_lits)
    2.95 +	make_clause(n, "conjecture", Conjecture, lits, types_sorts)
    2.96      end;
    2.97      
    2.98  fun make_conjecture_clauses_aux _ [] = []
    2.99 @@ -635,10 +614,8 @@
   2.100  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
   2.101  	val (lits,types_sorts) = literals_of_term term
   2.102  	val lits' = sort_lits lits
   2.103 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   2.104      in 
   2.105 -	make_clause(cls_id,ax_name,Axiom,
   2.106 -	            lits',types_sorts,tvar_lits,tfree_lits)
   2.107 +	make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)
   2.108      end;
   2.109  
   2.110  
   2.111 @@ -684,14 +661,6 @@
   2.112                     conclLit = make_TConsLit(true, (res,tcons,tvars)), 
   2.113                     premLits = map make_TVarLit false_tvars_srts'}
   2.114     end;
   2.115 -    
   2.116 -(*The number of clauses generated from cls, including type clauses. It's always 1
   2.117 -  except for conjecture clauses.*)
   2.118 -fun num_of_clauses (Clause cls) =
   2.119 -    let val num_tfree_lits = 
   2.120 -	      if !keep_types then length (#tfree_type_literals cls)
   2.121 -	      else 0
   2.122 -    in 	1 + num_tfree_lits  end;
   2.123  
   2.124  
   2.125  (**** Isabelle class relations ****)
   2.126 @@ -873,14 +842,13 @@
   2.127      dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^ 
   2.128      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   2.129  
   2.130 -fun dfg_clause_aux (Clause{literals, tvar_type_literals, tfree_type_literals, ...}) = 
   2.131 +fun dfg_clause_aux (Clause{literals, types_sorts, ...}) = 
   2.132    let val lits = map dfg_literal literals
   2.133 +      val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   2.134        val tvar_lits_strs = 
   2.135 -	  if !keep_types then map dfg_of_typeLit tvar_type_literals
   2.136 -	  else []
   2.137 +	  if !keep_types then map dfg_of_typeLit tvar_lits else []
   2.138        val tfree_lits =
   2.139 -          if !keep_types then map dfg_of_typeLit tfree_type_literals
   2.140 -          else []
   2.141 +          if !keep_types then map dfg_of_typeLit tfree_lits else []
   2.142    in
   2.143        (tvar_lits_strs @ lits, tfree_lits)
   2.144    end; 
   2.145 @@ -985,10 +953,7 @@
   2.146    end;
   2.147  
   2.148  
   2.149 -(********************************)
   2.150 -(* code to produce TPTP files   *)
   2.151 -(********************************)
   2.152 -
   2.153 +(**** Produce TPTP files ****)
   2.154  
   2.155  (*Attach sign in TPTP syntax: false means negate.*)
   2.156  fun tptp_sign true s = "++" ^ s
   2.157 @@ -1006,7 +971,6 @@
   2.158  fun tptp_of_typeLit (LTVar (s,ty)) = "--" ^ s ^ "(" ^ ty ^ ")"
   2.159    | tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")";
   2.160   
   2.161 -
   2.162  fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 
   2.163      "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   2.164      knd ^ "," ^ lits ^ ").\n";
   2.165 @@ -1015,53 +979,29 @@
   2.166      "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
   2.167      knd ^ ",[" ^ tfree_lit ^ "]).\n";
   2.168  
   2.169 -fun tptp_type_lits (Clause cls) = 
   2.170 -    let val lits = map tptp_literal (#literals cls)
   2.171 -	val tvar_lits_strs =
   2.172 -	      if !keep_types 
   2.173 -	      then (map tptp_of_typeLit (#tvar_type_literals cls)) 
   2.174 -	      else []
   2.175 -	val tfree_lits = 
   2.176 -	      if !keep_types
   2.177 -	      then (map tptp_of_typeLit (#tfree_type_literals cls)) 
   2.178 -	      else []
   2.179 +fun tptp_type_lits (Clause {literals, types_sorts, ...}) = 
   2.180 +    let val lits = map tptp_literal literals
   2.181 +	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   2.182 +        val tvar_lits_strs =
   2.183 +            if !keep_types then map tptp_of_typeLit tvar_lits else []
   2.184 +	val tfree_lits =
   2.185 +	    if !keep_types then map tptp_of_typeLit tfree_lits else []
   2.186      in
   2.187  	(tvar_lits_strs @ lits, tfree_lits)
   2.188      end; 
   2.189  
   2.190 -fun tptp_clause cls =
   2.191 +fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) =
   2.192      let val (lits,tfree_lits) = tptp_type_lits cls 
   2.193              (*"lits" includes the typing assumptions (TVars)*)
   2.194 -	val cls_id = get_clause_id cls
   2.195 -	val ax_name = get_axiomName cls
   2.196 -	val knd = string_of_kind cls
   2.197 -	val lits_str = bracket_pack lits
   2.198 -	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 			 
   2.199 -	fun typ_clss k [] = []
   2.200 -          | typ_clss k (tfree :: tfrees) = 
   2.201 -              gen_tptp_type_cls(cls_id,ax_name,knd,tfree,k) :: 
   2.202 -              typ_clss (k+1) tfrees
   2.203 -    in 
   2.204 -	cls_str :: (typ_clss 0 tfree_lits)
   2.205 -    end;
   2.206 -
   2.207 -fun clause2tptp cls =
   2.208 -    let val (lits,tfree_lits) = tptp_type_lits cls 
   2.209 -            (*"lits" includes the typing assumptions (TVars)*)
   2.210 -	val cls_id = get_clause_id cls
   2.211 -	val ax_name = get_axiomName cls
   2.212 -	val knd = string_of_kind cls
   2.213 -	val lits_str = bracket_pack lits
   2.214 -	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
   2.215 +	val knd = name_of_kind kind
   2.216 +	val cls_str = gen_tptp_cls(clause_id, axiom_name, knd, bracket_pack lits) 
   2.217      in
   2.218  	(cls_str,tfree_lits) 
   2.219      end;
   2.220  
   2.221 -
   2.222  fun tptp_tfree_clause tfree_lit =
   2.223      "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n";
   2.224  
   2.225 -
   2.226  fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
   2.227        tptp_sign b (c ^ "(" ^ t ^ paren_pack args ^ ")")
   2.228    | tptp_of_arLit (TVarLit(b,(c,str))) =
   2.229 @@ -1092,7 +1032,7 @@
   2.230      val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   2.231      val out = TextIO.openOut filename
   2.232    in
   2.233 -    List.app (writeln_strs out o tptp_clause) axclauses;
   2.234 +    List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
   2.235      writeln_strs out tfree_clss;
   2.236      writeln_strs out tptp_clss;
   2.237      List.app (curry TextIO.output out o tptp_classrelClause) classrel_clauses;