# HG changeset patch # User paulson # Date 1129277990 -7200 # Node ID 1438291d57f0d912dbda2a4f7f899e31c05d23d2 # Parent d81057c3898734b3e2db385d814f330b1d719c7a deletion of Tools/res_types_sorts; removal of absolute numbering of clauses diff -r d81057c38987 -r 1438291d57f0 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Oct 13 11:58:22 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Oct 14 10:19:50 2005 +0200 @@ -67,7 +67,7 @@ (* write out a subgoal as tptp clauses to the file "xxxx_N"*) fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = let - val clss = map (ResClause.make_conjecture_clause_thm) thms + val clss = ResClause.make_conjecture_clauses thms val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss) val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses @@ -81,7 +81,7 @@ (* write out a subgoal in DFG format to the file "xxxx_N"*) fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = - let val clss = map (ResClause.make_conjecture_clause_thm) thms + let val clss = ResClause.make_conjecture_clauses thms (*FIXME: classrel_clauses and arity_clauses*) val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n) axclauses [] [] [] @@ -159,9 +159,9 @@ val _ = debug ("claset and simprules total clauses = " ^ Int.toString (Array.length clause_arr)) val thy = ProofContext.theory_of ctxt - val classrel_clauses = ResTypesSorts.classrel_clauses_thy thy + val classrel_clauses = ResClause.classrel_clauses_thy thy val _ = debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) - val arity_clauses = ResTypesSorts.arity_clause_thy thy + val arity_clauses = ResClause.arity_clause_thy thy val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses)) val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees fun writenext n = diff -r d81057c38987 -r 1438291d57f0 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Thu Oct 13 11:58:22 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Fri Oct 14 10:19:50 2005 +0200 @@ -18,16 +18,10 @@ exception CLAUSE of string * term type arityClause type classrelClause - val classrelClauses_of : string * string list -> classrelClause list type clause val init : theory -> unit - val make_axiom_arity_clause : - string * (string * string list list) -> arityClause - val make_axiom_classrelClause : string * string option -> classrelClause val make_axiom_clause : Term.term -> string * int -> clause - val make_conjecture_clause : Term.term -> clause - val make_conjecture_clause_thm : Thm.thm -> clause - val make_hypothesis_clause : Term.term -> clause + val make_conjecture_clauses : thm list -> clause list val get_axiomName : clause -> string val isTaut : clause -> bool val num_of_clauses : clause -> int @@ -37,6 +31,9 @@ (string * int) list -> (string * int) list -> string val tfree_dfg_clause : string -> string + val arity_clause_thy: theory -> arityClause list + val classrel_clauses_thy: theory -> classrelClause list + val tptp_arity_clause : arityClause -> string val tptp_classrelClause : classrelClause -> string val tptp_clause : clause -> string list @@ -182,14 +179,6 @@ type tag = bool; -val id_ref = ref 0; - -fun generate_id () = - let val id = !id_ref - in id_ref := id + 1; id end; - - - (**** Isabelle FOL clauses ****) val tagged = ref false; @@ -275,7 +264,7 @@ (*Initialize the type suppression mechanism with the current theory before producing any clauses!*) -fun init thy = (id_ref := 0; curr_defs := Theory.defs_of thy); +fun init thy = (curr_defs := Theory.defs_of thy); fun no_types_needed s = Defs.monomorphic (!curr_defs) s; @@ -526,16 +515,21 @@ -fun make_conjecture_clause_thm thm = +fun make_conjecture_clause n thm = let val (lits,types_sorts, preds, funcs) = literals_of_thm thm - val cls_id = generate_id() val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds val tvars = get_tvar_strs types_sorts in - make_clause(cls_id,"",Conjecture, + make_clause(n,"conjecture",Conjecture, lits,types_sorts,tvar_lits,tfree_lits, tvars, preds, funcs) end; + +fun make_conjecture_clauses_aux _ [] = [] + | make_conjecture_clauses_aux n (th::ths) = + make_conjecture_clause n th :: make_conjecture_clauses_aux (n+1) ths + +val make_conjecture_clauses = make_conjecture_clauses_aux 0 fun make_axiom_clause term (ax_name,cls_id) = @@ -549,28 +543,6 @@ end; -fun make_hypothesis_clause term = - let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) - val cls_id = generate_id() - val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds - val tvars = get_tvar_strs types_sorts - in - make_clause(cls_id,"",Hypothesis, - lits,types_sorts,tvar_lits,tfree_lits, - tvars, preds, funcs) - end; - -fun make_conjecture_clause term = - let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) - val cls_id = generate_id() - val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds - val tvars = get_tvar_strs types_sorts - in - make_clause(cls_id,"",Conjecture, - lits,types_sorts,tvar_lits,tfree_lits, - tvars, preds, funcs) - end; - (**** Isabelle arities ****) @@ -586,6 +558,7 @@ datatype arityClause = ArityClause of {clause_id: clause_id, + axiom_name: axiom_name, kind: kind, conclLit: arLit, premLits: arLit list}; @@ -604,23 +577,18 @@ fun make_TVarLit (b,(cls,str)) = TVarLit(b,(cls,str)); fun make_TConsLit (b,(cls,tcons,tvars)) = TConsLit(b,(make_type_class cls,make_fixed_type_const tcons,tvars)); - -fun make_arity_clause (clause_id,kind,conclLit,premLits) = - ArityClause {clause_id = clause_id, kind = kind, conclLit = conclLit, premLits = premLits}; - - -fun make_axiom_arity_clause (tcons,(res,args)) = - let val cls_id = generate_id() - val nargs = length args - val tvars = get_TVars nargs - val conclLit = make_TConsLit(true,(res,tcons,tvars)) - val tvars_srts = ListPair.zip (tvars,args) - val tvars_srts' = union_all(map pack_sort tvars_srts) - val false_tvars_srts' = map (pair false) tvars_srts' - val premLits = map make_TVarLit false_tvars_srts' - in - make_arity_clause (cls_id,Axiom,conclLit,premLits) - end; +fun make_axiom_arity_clause (tcons,n,(res,args)) = + let val nargs = length args + val tvars = get_TVars nargs + val tvars_srts = ListPair.zip (tvars,args) + val tvars_srts' = union_all(map pack_sort tvars_srts) + val false_tvars_srts' = map (pair false) tvars_srts' + in + ArityClause {clause_id = n, kind = Axiom, + axiom_name = tcons, + 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*) fun num_of_clauses (Clause cls) = @@ -638,28 +606,47 @@ subclass: class, superclass: class option}; -fun make_classrelClause (clause_id,subclass,superclass) = - ClassrelClause {clause_id = clause_id,subclass = subclass, superclass = superclass}; + +fun make_axiom_classrelClause n subclass superclass = + ClassrelClause {clause_id = n, + subclass = subclass, superclass = superclass}; -fun make_axiom_classrelClause (subclass,superclass) = - let val cls_id = generate_id() - val sub = make_type_class subclass - val sup = case superclass of NONE => NONE - | SOME s => SOME (make_type_class s) - in - make_classrelClause(cls_id,sub,sup) - end; - - - -fun classrelClauses_of_aux (sub,[]) = [] - | classrelClauses_of_aux (sub,(sup::sups)) = make_axiom_classrelClause(sub,SOME sup) :: (classrelClauses_of_aux (sub,sups)); +fun classrelClauses_of_aux n sub [] = [] + | classrelClauses_of_aux n sub (sup::sups) = + make_axiom_classrelClause n sub (SOME sup) :: classrelClauses_of_aux (n+1) sub sups; fun classrelClauses_of (sub,sups) = - case sups of [] => [make_axiom_classrelClause (sub,NONE)] - | _ => classrelClauses_of_aux (sub, sups); + case sups of [] => [make_axiom_classrelClause 0 sub NONE] + | _ => classrelClauses_of_aux 0 sub sups; + + +(***** Isabelle arities *****) + + +fun arity_clause _ (tcons, []) = [] + | arity_clause n (tcons, ar::ars) = + make_axiom_arity_clause (tcons,n,ar) :: + arity_clause (n+1) (tcons,ars); + +fun multi_arity_clause [] = [] + | multi_arity_clause (tcon_ar :: tcons_ars) = + arity_clause 0 tcon_ar @ multi_arity_clause tcons_ars + +fun arity_clause_thy thy = + let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy)) + in multi_arity_clause (Symtab.dest arities) end; + + +(* Isabelle classes *) + +type classrelClauses = classrelClause list Symtab.table; + +val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of; +fun classrel_clauses_classrel (C: Sorts.classes) = map classrelClauses_of (Graph.dest C); +val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of; + (****!!!! Changed for typed equality !!!!****) @@ -925,8 +912,8 @@ end; -fun string_of_arClauseID (ArityClause arcls) = - arclause_prefix ^ Int.toString(#clause_id arcls); +fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) = + arclause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id; fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); @@ -1075,13 +1062,15 @@ end; -fun tptp_classrelClause (ClassrelClause cls) = - let val relcls_id = clrelclause_prefix ^ Int.toString(#clause_id cls) - val sub = #subclass cls - val sup = #superclass cls - val lits = tptp_classrelLits sub sup +fun tptp_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) = + let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ + Int.toString clause_id + val lits = tptp_classrelLits (make_type_class subclass) + (Option.map make_type_class superclass) in "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." end; + + end; diff -r d81057c38987 -r 1438291d57f0 src/HOL/Tools/res_types_sorts.ML --- a/src/HOL/Tools/res_types_sorts.ML Thu Oct 13 11:58:22 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ -(* Author: Jia Meng, Cambridge University Computer Laboratory - ID: $Id$ - Copyright 2004 University of Cambridge - -Transformation of Isabelle arities and class relations into clauses -(defined in the structure Clause). -*) - -signature RES_TYPES_SORTS = -sig - exception ARITIES of string - val arity_clause: string * (string * string list list) list -> ResClause.arityClause list - val arity_clause_thy: theory -> ResClause.arityClause list - type classrelClauses - val classrel_clause: string * string list -> ResClause.classrelClause list - val classrel_clauses_classrel: Sorts.classes -> ResClause.classrelClause list list - val classrel_clauses_thy: theory -> ResClause.classrelClause list -end; - -structure ResTypesSorts: RES_TYPES_SORTS = -struct - -(* Isabelle arities *) - -exception ARITIES of string; - -fun arity_clause (tcons, []) = raise ARITIES tcons - | arity_clause (tcons, [ar]) = [ResClause.make_axiom_arity_clause (tcons, ar)] - | arity_clause (tcons, ar1 :: ars) = - ResClause.make_axiom_arity_clause (tcons, ar1) :: arity_clause (tcons, ars); - -fun multi_arity_clause [] expts = ([], expts) - | multi_arity_clause ((tcon, []) :: tcons_ars) expts = - multi_arity_clause tcons_ars ((tcon, []) :: expts) - | multi_arity_clause (tcon_ar :: tcons_ars) expts = - let val (cls,ary) = multi_arity_clause tcons_ars expts - in ((arity_clause tcon_ar @ cls), ary) end; - -fun arity_clause_thy thy = - let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy)) - in #1 (multi_arity_clause (Symtab.dest arities) []) end; - - -(* Isabelle classes *) - -type classrelClauses = ResClause.classrelClause list Symtab.table; - -val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of; -val classrel_clause = ResClause.classrelClauses_of; -fun classrel_clauses_classrel (C: Sorts.classes) = map classrel_clause (Graph.dest C); -val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of; - -end;