deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
authorpaulson
Fri Oct 14 10:19:50 2005 +0200 (2005-10-14 ago)
changeset 178451438291d57f0
parent 17844 d81057c38987
child 17846 6fd3261a1be0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_types_sorts.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Oct 13 11:58:22 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 14 10:19:50 2005 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
     1.5  fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
     1.6    let
     1.7 -    val clss = map (ResClause.make_conjecture_clause_thm) thms
     1.8 +    val clss = ResClause.make_conjecture_clauses thms
     1.9      val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    1.10      val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss)
    1.11      val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
    1.12 @@ -81,7 +81,7 @@
    1.13  
    1.14  (* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.15  fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = 
    1.16 -    let val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.17 +    let val clss = ResClause.make_conjecture_clauses thms
    1.18          (*FIXME: classrel_clauses and arity_clauses*)
    1.19          val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n)
    1.20                          axclauses [] [] []    
    1.21 @@ -159,9 +159,9 @@
    1.22        val _ = debug ("claset and simprules total clauses = " ^ 
    1.23                       Int.toString (Array.length clause_arr))
    1.24        val thy = ProofContext.theory_of ctxt
    1.25 -      val classrel_clauses = ResTypesSorts.classrel_clauses_thy thy
    1.26 +      val classrel_clauses = ResClause.classrel_clauses_thy thy
    1.27        val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.28 -      val arity_clauses = ResTypesSorts.arity_clause_thy thy
    1.29 +      val arity_clauses = ResClause.arity_clause_thy thy
    1.30        val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.31        val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
    1.32        fun writenext n =
     2.1 --- a/src/HOL/Tools/res_clause.ML	Thu Oct 13 11:58:22 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Oct 14 10:19:50 2005 +0200
     2.3 @@ -18,16 +18,10 @@
     2.4    exception CLAUSE of string * term
     2.5    type arityClause 
     2.6    type classrelClause
     2.7 -  val classrelClauses_of : string * string list -> classrelClause list
     2.8    type clause
     2.9    val init : theory -> unit
    2.10 -  val make_axiom_arity_clause :
    2.11 -     string * (string * string list list) -> arityClause
    2.12 -  val make_axiom_classrelClause :  string * string option -> classrelClause
    2.13    val make_axiom_clause : Term.term -> string * int -> clause
    2.14 -  val make_conjecture_clause : Term.term -> clause
    2.15 -  val make_conjecture_clause_thm : Thm.thm -> clause
    2.16 -  val make_hypothesis_clause : Term.term -> clause
    2.17 +  val make_conjecture_clauses : thm list -> clause list
    2.18    val get_axiomName : clause ->  string
    2.19    val isTaut : clause -> bool
    2.20    val num_of_clauses : clause -> int
    2.21 @@ -37,6 +31,9 @@
    2.22  	   (string * int) list -> (string * int) list -> string
    2.23    val tfree_dfg_clause : string -> string
    2.24  
    2.25 +  val arity_clause_thy: theory -> arityClause list 
    2.26 +  val classrel_clauses_thy: theory -> classrelClause list 
    2.27 +
    2.28    val tptp_arity_clause : arityClause -> string
    2.29    val tptp_classrelClause : classrelClause -> string
    2.30    val tptp_clause : clause -> string list
    2.31 @@ -182,14 +179,6 @@
    2.32  type tag = bool; 
    2.33  
    2.34  
    2.35 -val id_ref = ref 0;
    2.36 -
    2.37 -fun generate_id () = 
    2.38 -  let val id = !id_ref
    2.39 -  in id_ref := id + 1; id end;
    2.40 -
    2.41 -
    2.42 -
    2.43  (**** Isabelle FOL clauses ****)
    2.44  
    2.45  val tagged = ref false;
    2.46 @@ -275,7 +264,7 @@
    2.47  
    2.48  (*Initialize the type suppression mechanism with the current theory before
    2.49      producing any clauses!*)
    2.50 -fun init thy = (id_ref := 0; curr_defs := Theory.defs_of thy);
    2.51 +fun init thy = (curr_defs := Theory.defs_of thy);
    2.52  
    2.53  fun no_types_needed s = Defs.monomorphic (!curr_defs) s;
    2.54      
    2.55 @@ -526,16 +515,21 @@
    2.56  
    2.57  
    2.58  
    2.59 -fun make_conjecture_clause_thm thm =
    2.60 +fun make_conjecture_clause n thm =
    2.61      let val (lits,types_sorts, preds, funcs) = literals_of_thm thm
    2.62 -	val cls_id = generate_id()
    2.63  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
    2.64          val tvars = get_tvar_strs types_sorts
    2.65      in
    2.66 -	make_clause(cls_id,"",Conjecture,
    2.67 +	make_clause(n,"conjecture",Conjecture,
    2.68  	            lits,types_sorts,tvar_lits,tfree_lits,
    2.69  	            tvars, preds, funcs)
    2.70      end;
    2.71 +    
    2.72 +fun make_conjecture_clauses_aux _ [] = []
    2.73 +  | make_conjecture_clauses_aux n (th::ths) =
    2.74 +      make_conjecture_clause n th :: make_conjecture_clauses_aux (n+1) ths
    2.75 +
    2.76 +val make_conjecture_clauses = make_conjecture_clauses_aux 0
    2.77  
    2.78  
    2.79  fun make_axiom_clause term (ax_name,cls_id) =
    2.80 @@ -549,28 +543,6 @@
    2.81      end;
    2.82  
    2.83  
    2.84 -fun make_hypothesis_clause term =
    2.85 -    let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[])
    2.86 -	val cls_id = generate_id()
    2.87 -	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts  preds 
    2.88 -        val tvars = get_tvar_strs types_sorts
    2.89 -    in
    2.90 -	make_clause(cls_id,"",Hypothesis,
    2.91 -	            lits,types_sorts,tvar_lits,tfree_lits,
    2.92 -	            tvars, preds, funcs)
    2.93 -    end;
    2.94 - 
    2.95 -fun make_conjecture_clause term =
    2.96 -    let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[])
    2.97 -	val cls_id = generate_id()
    2.98 -	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
    2.99 -        val tvars = get_tvar_strs types_sorts	
   2.100 -    in
   2.101 -	make_clause(cls_id,"",Conjecture,
   2.102 -	            lits,types_sorts,tvar_lits,tfree_lits,
   2.103 -	            tvars, preds, funcs)
   2.104 -    end;
   2.105 - 
   2.106  
   2.107   
   2.108  (**** Isabelle arities ****)
   2.109 @@ -586,6 +558,7 @@
   2.110   
   2.111  datatype arityClause =  
   2.112  	 ArityClause of {clause_id: clause_id,
   2.113 +	  	         axiom_name: axiom_name,
   2.114  			 kind: kind,
   2.115  			 conclLit: arLit,
   2.116  			 premLits: arLit list};
   2.117 @@ -604,23 +577,18 @@
   2.118  fun make_TVarLit (b,(cls,str)) = TVarLit(b,(cls,str));
   2.119  fun make_TConsLit (b,(cls,tcons,tvars)) = TConsLit(b,(make_type_class cls,make_fixed_type_const tcons,tvars));
   2.120  
   2.121 -
   2.122 -fun make_arity_clause (clause_id,kind,conclLit,premLits) =
   2.123 -    ArityClause {clause_id = clause_id, kind = kind, conclLit = conclLit, premLits = premLits};
   2.124 -
   2.125 -
   2.126 -fun make_axiom_arity_clause (tcons,(res,args)) =
   2.127 -     let val cls_id = generate_id()
   2.128 -	 val nargs = length args
   2.129 -	 val tvars = get_TVars nargs
   2.130 -	 val conclLit = make_TConsLit(true,(res,tcons,tvars))
   2.131 -         val tvars_srts = ListPair.zip (tvars,args)
   2.132 -	 val tvars_srts' = union_all(map pack_sort tvars_srts)
   2.133 -         val false_tvars_srts' = map (pair false) tvars_srts'
   2.134 -	 val premLits = map make_TVarLit false_tvars_srts'
   2.135 -     in
   2.136 -	 make_arity_clause (cls_id,Axiom,conclLit,premLits)
   2.137 -     end;
   2.138 +fun make_axiom_arity_clause (tcons,n,(res,args)) =
   2.139 +   let val nargs = length args
   2.140 +       val tvars = get_TVars nargs
   2.141 +       val tvars_srts = ListPair.zip (tvars,args)
   2.142 +       val tvars_srts' = union_all(map pack_sort tvars_srts)
   2.143 +       val false_tvars_srts' = map (pair false) tvars_srts'
   2.144 +   in
   2.145 +      ArityClause {clause_id = n, kind = Axiom, 
   2.146 +                   axiom_name = tcons,
   2.147 +                   conclLit = make_TConsLit(true,(res,tcons,tvars)), 
   2.148 +                   premLits = map make_TVarLit false_tvars_srts'}
   2.149 +   end;
   2.150      
   2.151  (*The number of clauses generated from cls, including type clauses*)
   2.152  fun num_of_clauses (Clause cls) =
   2.153 @@ -638,28 +606,47 @@
   2.154  			    subclass: class,
   2.155  			    superclass: class option};
   2.156  
   2.157 -fun make_classrelClause (clause_id,subclass,superclass) =
   2.158 -    ClassrelClause {clause_id = clause_id,subclass = subclass, superclass = superclass};
   2.159 +
   2.160 +fun make_axiom_classrelClause n subclass superclass =
   2.161 +  ClassrelClause {clause_id = n,
   2.162 +                  subclass = subclass, superclass = superclass};
   2.163  
   2.164  
   2.165 -fun make_axiom_classrelClause (subclass,superclass) =
   2.166 -    let val cls_id = generate_id()
   2.167 -	val sub = make_type_class subclass
   2.168 -	val sup = case superclass of NONE => NONE 
   2.169 -				   | SOME s => SOME (make_type_class s)
   2.170 -    in
   2.171 -	make_classrelClause(cls_id,sub,sup)
   2.172 -    end;
   2.173 -
   2.174 -
   2.175 -
   2.176 -fun classrelClauses_of_aux (sub,[]) = []
   2.177 -  | classrelClauses_of_aux (sub,(sup::sups)) = make_axiom_classrelClause(sub,SOME sup) :: (classrelClauses_of_aux (sub,sups));
   2.178 +fun classrelClauses_of_aux n sub [] = []
   2.179 +  | classrelClauses_of_aux n sub (sup::sups) =
   2.180 +      make_axiom_classrelClause n sub (SOME sup) :: classrelClauses_of_aux (n+1) sub sups;
   2.181  
   2.182  
   2.183  fun classrelClauses_of (sub,sups) = 
   2.184 -    case sups of [] => [make_axiom_classrelClause (sub,NONE)]
   2.185 -	       | _ => classrelClauses_of_aux (sub, sups);
   2.186 +    case sups of [] => [make_axiom_classrelClause 0 sub NONE]
   2.187 +	       | _ => classrelClauses_of_aux 0 sub sups;
   2.188 +
   2.189 +
   2.190 +(***** Isabelle arities *****)
   2.191 +
   2.192 +
   2.193 +fun arity_clause _ (tcons, []) = []
   2.194 +  | arity_clause n (tcons, ar::ars) =
   2.195 +      make_axiom_arity_clause (tcons,n,ar) :: 
   2.196 +      arity_clause (n+1) (tcons,ars);
   2.197 +
   2.198 +fun multi_arity_clause [] = []
   2.199 +  | multi_arity_clause (tcon_ar :: tcons_ars)  =
   2.200 +      arity_clause 0 tcon_ar  @  multi_arity_clause tcons_ars 
   2.201 +
   2.202 +fun arity_clause_thy thy =
   2.203 +  let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy))
   2.204 +  in multi_arity_clause (Symtab.dest arities) end;
   2.205 +
   2.206 +
   2.207 +(* Isabelle classes *)
   2.208 +
   2.209 +type classrelClauses = classrelClause list Symtab.table;
   2.210 +
   2.211 +val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
   2.212 +fun classrel_clauses_classrel (C: Sorts.classes) = map classrelClauses_of (Graph.dest C);
   2.213 +val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of;
   2.214 +
   2.215  
   2.216  
   2.217  (****!!!! Changed for typed equality !!!!****)
   2.218 @@ -925,8 +912,8 @@
   2.219       end;
   2.220  
   2.221  
   2.222 -fun string_of_arClauseID (ArityClause arcls) =
   2.223 -    arclause_prefix ^ Int.toString(#clause_id arcls);
   2.224 +fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) =
   2.225 +    arclause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id;
   2.226  
   2.227  fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
   2.228  
   2.229 @@ -1075,13 +1062,15 @@
   2.230      end;
   2.231  
   2.232  
   2.233 -fun tptp_classrelClause (ClassrelClause cls) =
   2.234 -    let val relcls_id = clrelclause_prefix ^ Int.toString(#clause_id cls)
   2.235 -	val sub = #subclass cls
   2.236 -	val sup = #superclass cls
   2.237 -	val lits = tptp_classrelLits sub sup
   2.238 +fun tptp_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) =
   2.239 +    let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ 
   2.240 +                        Int.toString clause_id
   2.241 +	val lits = tptp_classrelLits (make_type_class subclass) 
   2.242 +	                (Option.map make_type_class superclass)
   2.243      in
   2.244  	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
   2.245      end; 
   2.246  
   2.247 +
   2.248 +
   2.249  end;
     3.1 --- a/src/HOL/Tools/res_types_sorts.ML	Thu Oct 13 11:58:22 2005 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,53 +0,0 @@
     3.4 -(*  Author:     Jia Meng, Cambridge University Computer Laboratory
     3.5 -    ID:         $Id$
     3.6 -    Copyright 2004 University of Cambridge
     3.7 -
     3.8 -Transformation of Isabelle arities and class relations into clauses
     3.9 -(defined in the structure Clause).
    3.10 -*)
    3.11 -
    3.12 -signature RES_TYPES_SORTS =
    3.13 -sig
    3.14 -  exception ARITIES of string
    3.15 -  val arity_clause: string * (string * string list list) list -> ResClause.arityClause list
    3.16 -  val arity_clause_thy: theory -> ResClause.arityClause list 
    3.17 -  type classrelClauses
    3.18 -  val classrel_clause: string * string list -> ResClause.classrelClause list
    3.19 -  val classrel_clauses_classrel: Sorts.classes -> ResClause.classrelClause list list
    3.20 -  val classrel_clauses_thy: theory -> ResClause.classrelClause list 
    3.21 -end;
    3.22 -
    3.23 -structure ResTypesSorts: RES_TYPES_SORTS =
    3.24 -struct
    3.25 -
    3.26 -(* Isabelle arities *)
    3.27 -
    3.28 -exception ARITIES of string;
    3.29 -
    3.30 -fun arity_clause (tcons, []) = raise ARITIES tcons
    3.31 -  | arity_clause (tcons, [ar]) = [ResClause.make_axiom_arity_clause (tcons, ar)]
    3.32 -  | arity_clause (tcons, ar1 :: ars) =
    3.33 -      ResClause.make_axiom_arity_clause (tcons, ar1) :: arity_clause (tcons, ars);
    3.34 -
    3.35 -fun multi_arity_clause [] expts = ([], expts)
    3.36 -  | multi_arity_clause ((tcon, []) :: tcons_ars) expts =
    3.37 -      multi_arity_clause tcons_ars ((tcon, []) :: expts)
    3.38 -  | multi_arity_clause (tcon_ar :: tcons_ars) expts =
    3.39 -      let val (cls,ary) = multi_arity_clause tcons_ars expts
    3.40 -      in ((arity_clause tcon_ar @ cls), ary) end;
    3.41 -
    3.42 -fun arity_clause_thy thy =
    3.43 -  let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy))
    3.44 -  in #1 (multi_arity_clause (Symtab.dest arities) []) end;
    3.45 -
    3.46 -
    3.47 -(* Isabelle classes *)
    3.48 -
    3.49 -type classrelClauses = ResClause.classrelClause list Symtab.table;
    3.50 -
    3.51 -val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
    3.52 -val classrel_clause = ResClause.classrelClauses_of;
    3.53 -fun classrel_clauses_classrel (C: Sorts.classes) = map classrel_clause (Graph.dest C);
    3.54 -val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of;
    3.55 -
    3.56 -end;