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;