# HG changeset patch # User mengj # Date 1152102082 -7200 # Node ID 1ffcf4802802de277aa6f96014655ef11aefb9e1 # Parent 729a4553400188214590d39f45736fd0877c9414 Literals aren't sorted any more. Output overloaded constants' type var instantiations. diff -r 729a45534001 -r 1ffcf4802802 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Wed Jul 05 11:32:38 2006 +0200 +++ b/src/HOL/Tools/res_clause.ML Wed Jul 05 14:21:22 2006 +0200 @@ -17,9 +17,7 @@ val arity_clause_thy: theory -> arityClause list val ascii_of : string -> string val bracket_pack : string list -> string - val check_var_pairs: ''a * ''b -> (''a * ''b) list -> int val classrel_clauses_thy: theory -> classrelClause list - val clause_eq : clause * clause -> bool val clause_prefix : string val clause2tptp : clause -> string * string list val const_prefix : string @@ -28,7 +26,6 @@ val gen_tptp_cls : int * string * string * string -> string val gen_tptp_type_cls : int * string * string * string * int -> string val get_axiomName : clause -> string - val hash_clause : clause -> int val init : theory -> unit val isMeta : string -> bool val isTaut : clause -> bool @@ -57,8 +54,6 @@ val tptp_tfree_clause : string -> string val tptp_write_file: thm list -> string -> ((thm * (string * int)) list * classrelClause list * arityClause list) -> unit val tvar_prefix : string - val types_eq: fol_type list * fol_type list -> (string*string) list * (string*string) list -> bool * ((string*string) list * (string*string) list) - val types_ord : fol_type list * fol_type list -> order val union_all : ''a list list -> ''a list val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit val dfg_sign: bool -> string -> string @@ -270,14 +265,6 @@ fun isTaut (Clause {literals,...}) = exists isTrue literals; -fun make_clause (clause_id, axiom_name, th, kind, literals, types_sorts) = - if forall isFalse literals - then error "Problem too trivial for resolution (empty clause)" - else - Clause {clause_id = clause_id, axiom_name = axiom_name, - th = th, kind = kind, - literals = literals, types_sorts = types_sorts}; - (*Declarations of the current theory--to allow suppressing types.*) val const_typargs = ref (Library.K [] : (string*typ -> typ list)); @@ -393,161 +380,6 @@ (case ord(x,y) of EQUAL => list_ord ord (xs,ys) | xy_ord => xy_ord); -fun type_ord (AtomV(_),AtomV(_)) = EQUAL - | type_ord (AtomV(_),_) = LESS - | type_ord (AtomF(_),AtomV(_)) = GREATER - | type_ord (AtomF(f1),AtomF(f2)) = string_ord (f1,f2) - | type_ord (AtomF(_),_) = LESS - | type_ord (Comp(_,_),AtomV(_)) = GREATER - | type_ord (Comp(_,_),AtomF(_)) = GREATER - | type_ord (Comp(con1,args1),Comp(con2,args2)) = - (case string_ord(con1,con2) of EQUAL => types_ord (args1,args2) - | con_ord => con_ord) -and - types_ord ([],[]) = EQUAL - | types_ord (tps1,tps2) = list_ord type_ord (tps1,tps2); - - -fun term_ord (UVar _, UVar _) = EQUAL - | term_ord (UVar _, _) = LESS - | term_ord (Fun _, UVar _) = GREATER - | term_ord (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) = - (case string_ord (f1,f2) of - EQUAL => - (case terms_ord (tms1,tms2) of EQUAL => types_ord (tps1,tps2) - | tms_ord => tms_ord) - | fn_ord => fn_ord) - -and - terms_ord ([],[]) = EQUAL - | terms_ord (tms1,tms2) = list_ord term_ord (tms1,tms2); - - - -fun predicate_ord (Predicate(pname1,ftyps1,ftms1),Predicate(pname2,ftyps2,ftms2)) = - case string_ord (pname1,pname2) of - EQUAL => (case terms_ord(ftms1,ftms2) of EQUAL => types_ord(ftyps1,ftyps2) - | ftms_ord => ftms_ord) - | pname_ord => pname_ord - - -fun literal_ord (Literal(false,_,_),Literal(true,_,_)) = LESS - | literal_ord (Literal(true,_,_),Literal(false,_,_)) = GREATER - | literal_ord (Literal(_,pred1,_),Literal(_,pred2,_)) = predicate_ord(pred1,pred2); - -fun sort_lits lits = sort literal_ord lits; - - -(********** clause equivalence ******************) - -fun check_var_pairs (x,y) [] = 0 - | check_var_pairs (x,y) ((u,v)::w) = - if (x,y) = (u,v) then 1 - else - if x=u orelse y=v then 2 (*conflict*) - else check_var_pairs (x,y) w; - -fun type_eq (AtomV(v1),AtomV(v2)) (vars,tvars) = - (case check_var_pairs (v1,v2) tvars of 0 => (true,(vars,(v1,v2)::tvars)) - | 1 => (true,(vars,tvars)) - | 2 => (false,(vars,tvars))) - | type_eq (AtomV(_),_) vtvars = (false,vtvars) - | type_eq (AtomF(f1),AtomF(f2)) vtvars = (f1=f2,vtvars) - | type_eq (AtomF(_),_) vtvars = (false,vtvars) - | type_eq (Comp(con1,args1),Comp(con2,args2)) vtvars = - let val (eq1,vtvars1) = - if con1 = con2 then types_eq (args1,args2) vtvars - else (false,vtvars) - in - (eq1,vtvars1) - end - | type_eq (Comp(_,_),_) vtvars = (false,vtvars) - -and types_eq ([],[]) vtvars = (true,vtvars) - | types_eq (tp1::tps1,tp2::tps2) vtvars = - let val (eq1,vtvars1) = type_eq (tp1,tp2) vtvars - val (eq2,vtvars2) = if eq1 then types_eq (tps1,tps2) vtvars1 - else (eq1,vtvars1) - in - (eq2,vtvars2) - end; - - -fun term_eq (UVar(v1,tp1),UVar(v2,tp2)) (vars,tvars) = - (case check_var_pairs (v1,v2) vars of 0 => type_eq (tp1,tp2) (((v1,v2)::vars),tvars) - | 1 => type_eq (tp1,tp2) (vars,tvars) - | 2 => (false,(vars,tvars))) - | term_eq (UVar _,_) vtvars = (false,vtvars) - | term_eq (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) vtvars = - let val (eq1,vtvars1) = - if f1 = f2 then terms_eq (tms1,tms2) vtvars - else (false,vtvars) - val (eq2,vtvars2) = - if eq1 then types_eq (tps1,tps2) vtvars1 - else (eq1,vtvars1) - in - (eq2,vtvars2) - end - | term_eq (Fun(_,_,_),_) vtvars = (false,vtvars) - -and terms_eq ([],[]) vtvars = (true,vtvars) - | terms_eq (tm1::tms1,tm2::tms2) vtvars = - let val (eq1,vtvars1) = term_eq (tm1,tm2) vtvars - val (eq2,vtvars2) = if eq1 then terms_eq (tms1,tms2) vtvars1 - else (eq1,vtvars1) - in - (eq2,vtvars2) - end; - - -fun pred_eq (Predicate(pname1,tps1,tms1),Predicate(pname2,tps2,tms2)) vtvars = - let val (eq1,vtvars1) = - if pname1 = pname2 then terms_eq (tms1,tms2) vtvars - else (false,vtvars) - val (eq2,vtvars2) = - if eq1 then types_eq (tps1,tps2) vtvars1 - else (eq1,vtvars1) - in - (eq2,vtvars2) - end; - - -fun lit_eq (Literal(pol1,pred1,_),Literal(pol2,pred2,_)) vtvars = - if (pol1 = pol2) then pred_eq (pred1,pred2) vtvars - else (false,vtvars); - -fun lits_eq ([],[]) vtvars = (true,vtvars) - | lits_eq (l1::ls1,l2::ls2) vtvars = - let val (eq1,vtvars1) = lit_eq (l1,l2) vtvars - in - if eq1 then lits_eq (ls1,ls2) vtvars1 - else (false,vtvars1) - end - | lits_eq _ vtvars = (false,vtvars); - -(*Equality of two clauses up to variable renaming*) -fun clause_eq (Clause{literals=lits1,...}, Clause{literals=lits2,...}) = - #1 (lits_eq (lits1,lits2) ([],[])); - - -(*** Hash function for clauses ***) - -val xor_words = List.foldl Word.xorb 0w0; - -fun hashw_term (UVar _, w) = w - | hashw_term (Fun(f,tps,args), w) = - List.foldl hashw_term (Polyhash.hashw_string (f,w)) args; - -fun hashw_pred (Predicate(pn,_,args), w) = - List.foldl hashw_term (Polyhash.hashw_string (pn,w)) args; - -fun hash1_literal (Literal(true,pred,_)) = hashw_pred (pred, 0w0) - | hash1_literal (Literal(false,pred,_)) = Word.notb (hashw_pred (pred, 0w0)); - -fun hash_clause (Clause{literals,...}) = - Word.toIntX (xor_words (map hash1_literal literals)); - - (*Make literals for sorted type variables. FIXME: can it use map?*) fun sorts_on_typs (_, []) = ([]) | sorts_on_typs (v, "HOL.type" :: s) = @@ -579,30 +411,6 @@ (vss, fs union fss) end; - -(** make axiom and conjecture clauses. **) - -fun get_tvar_strs [] = [] - | get_tvar_strs ((FOLTVar indx,s)::tss) = - (make_schematic_type_var indx) ins (get_tvar_strs tss) - | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss - -(* check if a clause is first-order before making a conjecture clause*) -fun make_conjecture_clause n thm = - let val t = prop_of thm - val _ = check_is_fol_term t - handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t) - val (lits,types_sorts) = literals_of_term t - in - make_clause(n, "conjecture", thm, Conjecture, lits, types_sorts) - end; - -fun make_conjecture_clauses_aux _ [] = [] - | make_conjecture_clauses_aux n (t::ts) = - make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts - -val make_conjecture_clauses = make_conjecture_clauses_aux 0 - (** Too general means, positive equality literal with a variable X as one operand, when X does not occur properly in the other operand. This rules out clearly inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **) @@ -619,22 +427,57 @@ too_general_terms (x,y) orelse too_general_terms(y,x) | too_general_lit _ = false; + + +(** make axiom and conjecture clauses. **) + +exception MAKE_CLAUSE; +fun make_clause (clause_id, axiom_name, th, kind) = + let val term = prop_of th + val (lits,types_sorts) = literals_of_term term + in if forall isFalse lits + then error "Problem too trivial for resolution (empty clause)" + else + case kind of Axiom => + if forall too_general_lit lits then + (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); raise MAKE_CLAUSE) + else Clause {clause_id = clause_id, axiom_name = axiom_name,th = th, kind = kind, literals = lits, types_sorts = types_sorts} + | _ => Clause {clause_id = clause_id, axiom_name = axiom_name,th = th, kind = kind, literals = lits, types_sorts = types_sorts} + end; + +fun get_tvar_strs [] = [] + | get_tvar_strs ((FOLTVar indx,s)::tss) = + (make_schematic_type_var indx) ins (get_tvar_strs tss) + | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss + +(* check if a clause is first-order before making a conjecture clause*) +fun make_conjecture_clause n thm = + let val t = prop_of thm + val _ = check_is_fol_term t + handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t) + in + make_clause(n, "conjecture", thm, Conjecture) + end; + +fun make_conjecture_clauses_aux _ [] = [] + | make_conjecture_clauses_aux n (t::ts) = + make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts + +val make_conjecture_clauses = make_conjecture_clauses_aux 0 + + + (*before converting an axiom clause to "clause" format, check if it is FOL*) fun make_axiom_clause thm (ax_name,cls_id) = let val term = prop_of thm - val (lits,types_sorts) = literals_of_term term in if not (Meson.is_fol_term term) then - (Output.debug ("Omitting " ^ ax_name ^ ": Axiom is not FOL"); - NONE) - else if forall too_general_lit lits then - (Output.debug ("Omitting " ^ ax_name ^ ": equalities are too general"); - NONE) - else SOME (make_clause(cls_id, ax_name, thm, Axiom, sort_lits lits, types_sorts)) + (Output.debug ("Omitting " ^ ax_name ^ ": Axiom is not FOL"); + NONE) + else (SOME (make_clause(cls_id, ax_name, thm, Axiom)) handle MAKE_CLAUSE => NONE) end - handle CLAUSE _ => NONE; - - + handle CLAUSE _ => NONE; + fun make_axiom_clauses [] = [] | make_axiom_clauses ((thm,(name,id))::thms) = case make_axiom_clause thm (name,id) of SOME cls => if isTaut cls then make_axiom_clauses thms else cls :: make_axiom_clauses thms @@ -776,8 +619,7 @@ foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; fun add_folterm_funcs (UVar _, funcs) = funcs - | add_folterm_funcs (Fun(a,tys,[]), funcs) = Symtab.update (a,0) funcs - (*A constant is a special case: it has no type argument even if overloaded*) + | add_folterm_funcs (Fun(a,tys,[]), funcs) = Symtab.update (a,length tys) funcs | add_folterm_funcs (Fun(a,tys,tms), funcs) = foldl add_foltype_funcs (foldl add_folterm_funcs (Symtab.update (a, length tys + length tms) funcs) @@ -820,7 +662,7 @@ end and string_of_term (UVar(x,_)) = x | string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms) - | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*) + | string_of_term (Fun (name,typs,[])) = name ^ (paren_pack (map string_of_fol_type typs)) | string_of_term (Fun (name,typs,terms)) = let val terms_as_strings = map string_of_term terms val typs' = if !keep_types then map string_of_fol_type typs else []