# HG changeset patch # User mengj # Date 1135049365 -3600 # Node ID 72ee07f4b56b77a4cba81ed19826656f922e8ccf # Parent 4b517881ac7ecb4f9676dac4dc6c4ef347cbf53e Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words. diff -r 4b517881ac7e -r 72ee07f4b56b src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Tue Dec 20 04:27:46 2005 +0100 +++ b/src/HOL/Tools/res_hol_clause.ML Tue Dec 20 04:29:25 2005 +0100 @@ -181,7 +181,9 @@ type indexname = Term.indexname; type clause_id = int; type csort = Term.sort; -type ctyp = string; +type ctyp = ResClause.fol_type; + +val string_of_ctyp = ResClause.string_of_fol_type; type ctyp_var = ResClause.typ_var; @@ -213,8 +215,58 @@ fun get_axiomName (Clause cls) = #axiom_name cls; fun get_clause_id (Clause cls) = #clause_id cls; +fun get_literals (c as Clause(cls)) = #literals cls; + +exception TERM_ORD of string + +fun term_ord (CombVar(_,_),CombVar(_,_)) = EQUAL + | term_ord (CombVar(_,_),_) = LESS + | term_ord (CombFree(_,_),CombVar(_,_)) = GREATER + | term_ord (CombFree(f1,tp1),CombFree(f2,tp2)) = + let val ord1 = string_ord(f1,f2) + in + case ord1 of EQUAL => ResClause.types_ord ([tp1],[tp2]) + | _ => ord1 + end + | term_ord (CombFree(_,_),_) = LESS + | term_ord (CombConst(_,_,_),CombVar(_,_)) = GREATER + | term_ord (CombConst(_,_,_),CombFree(_,_)) = GREATER + | term_ord (CombConst(c1,tp1,_),CombConst(c2,tp2,_)) = + let val ord1 = string_ord (c1,c2) + in + case ord1 of EQUAL => ResClause.types_ord ([tp1],[tp2]) + | _ => ord1 + end + | term_ord (CombConst(_,_,_),_) = LESS + | term_ord (CombApp(_,_,_),Bool(_)) = raise TERM_ORD("bool") + | term_ord (CombApp(_,_,_),Equal(_,_)) = LESS + | term_ord (CombApp(f1,arg1,tp1),CombApp(f2,arg2,tp2)) = + let val ord1 = term_ord (f1,f2) + val ord2 = case ord1 of EQUAL => term_ord (arg1,arg2) + | _ => ord1 + in + case ord2 of EQUAL => ResClause.types_ord ([tp1],[tp2]) + | _ => ord2 + end + | term_ord (CombApp(_,_,_),_) = GREATER + | term_ord (Bool(_),_) = raise TERM_ORD("bool") + | term_ord (Equal(t1,t2),Equal(t3,t4)) = ResClause.list_ord term_ord ([t1,t2],[t3,t4]) + | term_ord (Equal(_,_),_) = GREATER; + +fun predicate_ord (Equal(_,_),Bool(_)) = LESS + | predicate_ord (Equal(t1,t2),Equal(t3,t4)) = + ResClause.list_ord term_ord ([t1,t2],[t3,t4]) + | predicate_ord (Bool(_),Equal(_,_)) = GREATER + | predicate_ord (Bool(t1),Bool(t2)) = term_ord (t1,t2) + + +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; (*********************************************************************) (* convert a clause with type Term.term to a clause with type clause *) @@ -244,31 +296,40 @@ ctvar_type_literals = ctvar_type_literals, ctfree_type_literals = ctfree_type_literals}; -(* convert a Term.type to a string; gather sort information of type variables *) -fun type_of (Type (a, [])) = (ResClause.make_fixed_type_const a,[]) - | type_of (Type (a, Ts)) = - let val typ_ts = map type_of Ts - val (typs,tsorts) = ListPair.unzip typ_ts - val ts = ResClause.union_all tsorts +fun type_of (Type (a, Ts)) = + let val (folTypes,ts) = types_of Ts val t = ResClause.make_fixed_type_const a in - (t ^ (ResClause.paren_pack typs),ts) + (ResClause.mk_fol_type("Comp",t,folTypes),ts) + end + | type_of (tp as (TFree(a,s))) = + let val t = ResClause.make_fixed_type_var a + in + (ResClause.mk_fol_type("Fixed",t,[]),[ResClause.mk_typ_var_sort tp]) end - | type_of (tp as (TFree (a,s))) = (ResClause.make_fixed_type_var a,[ResClause.mk_typ_var_sort tp]) - | type_of (tp as (TVar (v,s))) = (ResClause.make_schematic_type_var v,[ResClause.mk_typ_var_sort tp]); + | type_of (tp as (TVar(v,s))) = + let val t = ResClause.make_schematic_type_var v + in + (ResClause.mk_fol_type("Var",t,[]),[ResClause.mk_typ_var_sort tp]) + end - +and types_of Ts = + let val foltyps_ts = map type_of Ts + val (folTyps,ts) = ListPair.unzip foltyps_ts + in + (folTyps,ResClause.union_all ts) + end; (* same as above, but no gathering of sort information *) -fun simp_type_of (Type (a, [])) = ResClause.make_fixed_type_const a - | simp_type_of (Type (a, Ts)) = +fun simp_type_of (Type (a, Ts)) = let val typs = map simp_type_of Ts val t = ResClause.make_fixed_type_const a in - t ^ ResClause.paren_pack typs + ResClause.mk_fol_type("Comp",t,typs) end - | simp_type_of (TFree (a,s)) = ResClause.make_fixed_type_var a - | simp_type_of (TVar (v,s)) = ResClause.make_schematic_type_var v; + | simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[]) + | simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]); + fun comb_typ ("COMBI",t) = @@ -412,10 +473,11 @@ fun make_axiom_clause term (ax_name,cls_id) = let val term' = comb_of term val (lits,ctypes_sorts) = literals_of_term term' + val lits' = sort_lits lits val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux2 ctypes_sorts in make_clause(cls_id,ax_name,Axiom, - lits,ctypes_sorts,ctvar_lits,ctfree_lits) + lits',ctypes_sorts,ctvar_lits,ctfree_lits) end; @@ -469,18 +531,30 @@ exception STRING_OF_COMBTERM of int; (* convert literals of clauses into strings *) -fun string_of_combterm1_aux _ (CombConst(c,tp,_)) = (wrap_type (c,tp),tp) - | string_of_combterm1_aux _ (CombFree(v,tp)) = (wrap_type (v,tp),tp) - | string_of_combterm1_aux _ (CombVar(v,tp)) = (wrap_type (v,tp),tp) +fun string_of_combterm1_aux _ (CombConst(c,tp,_)) = + let val tp' = string_of_ctyp tp + in + (wrap_type (c,tp'),tp') + end + | string_of_combterm1_aux _ (CombFree(v,tp)) = + let val tp' = string_of_ctyp tp + in + (wrap_type (v,tp'),tp') + end + | string_of_combterm1_aux _ (CombVar(v,tp)) = + let val tp' = string_of_ctyp tp + in + (wrap_type (v,tp'),tp') + end | string_of_combterm1_aux is_pred (CombApp(t1,t2,tp)) = let val (s1,tp1) = string_of_combterm1_aux is_pred t1 val (s2,tp2) = string_of_combterm1_aux is_pred t2 - val r = case !typ_level of T_FULL => type_wrapper ^ (ResClause.paren_pack [(app_str ^ (ResClause.paren_pack [s1,s2])),tp]) + val tp' = ResClause.string_of_fol_type tp + val r = case !typ_level of T_FULL => type_wrapper ^ (ResClause.paren_pack [(app_str ^ (ResClause.paren_pack [s1,s2])),tp']) | T_PARTIAL => app_str ^ (ResClause.paren_pack [s1,s2,tp1]) | T_NONE => app_str ^ (ResClause.paren_pack [s1,s2]) | T_CONST => raise STRING_OF_COMBTERM (1) (*should not happen, if happened may be a bug*) - in - (r,tp) + in (r,tp') end | string_of_combterm1_aux is_pred (Bool(t)) = @@ -499,7 +573,11 @@ fun string_of_combterm1 is_pred term = fst (string_of_combterm1_aux is_pred term); -fun string_of_combterm2 _ (CombConst(c,tp,tvars)) = c ^ (ResClause.paren_pack tvars) +fun string_of_combterm2 _ (CombConst(c,tp,tvars)) = + let val tvars' = map string_of_ctyp tvars + in + c ^ (ResClause.paren_pack tvars') + end | string_of_combterm2 _ (CombFree(v,tp)) = v | string_of_combterm2 _ (CombVar(v,tp)) = v | string_of_combterm2 is_pred (CombApp(t1,t2,tp)) = @@ -568,4 +646,80 @@ end; + +(**********************************************************************) +(* clause equalities and hashing functions *) +(**********************************************************************) + + +fun combterm_eq (CombConst(c1,tp1,tps1),CombConst(c2,tp2,tps2)) vtvars = + let val (eq1,vtvars1) = if c1 = c2 then ResClause.types_eq (tps1,tps2) vtvars + else (false,vtvars) + in + (eq1,vtvars1) + end + | combterm_eq (CombConst(_,_,_),_) vtvars = (false,vtvars) + | combterm_eq (CombFree(a1,tp1),CombFree(a2,tp2)) vtvars = + if a1 = a2 then ResClause.types_eq ([tp1],[tp2]) vtvars + else (false,vtvars) + | combterm_eq (CombFree(_,_),_) vtvars = (false,vtvars) + | combterm_eq (CombVar(v1,tp1),CombVar(v2,tp2)) (vars,tvars) = + (case ResClause.check_var_pairs(v1,v2) vars of 0 => ResClause.types_eq ([tp1],[tp2]) ((v1,v2)::vars,tvars) + | 1 => ResClause.types_eq ([tp1],[tp2]) (vars,tvars) + | 2 => (false,(vars,tvars))) + | combterm_eq (CombVar(_,_),_) vtvars = (false,vtvars) + | combterm_eq (CombApp(f1,arg1,tp1),CombApp(f2,arg2,tp2)) vtvars = + let val (eq1,vtvars1) = combterm_eq (f1,f2) vtvars + val (eq2,vtvars2) = if eq1 then combterm_eq (arg1,arg2) vtvars1 + else (eq1,vtvars1) + in + if eq2 then ResClause.types_eq ([tp1],[tp2]) vtvars2 + else (eq2,vtvars2) + end + | combterm_eq (CombApp(_,_,_),_) vtvars = (false,vtvars) + | combterm_eq (Bool(t1),Bool(t2)) vtvars = combterm_eq (t1,t2) vtvars + | combterm_eq (Bool(_),_) vtvars = (false,vtvars) + | combterm_eq (Equal(t1,t2),Equal(t3,t4)) vtvars = + let val (eq1,vtvars1) = combterm_eq (t1,t3) vtvars + in + if eq1 then combterm_eq (t2,t4) vtvars1 + else (eq1,vtvars1) + end + | combterm_eq (Equal(t1,t2),_) vtvars = (false,vtvars); + +fun lit_eq (Literal(pol1,pred1),Literal(pol2,pred2)) vtvars = + if (pol1 = pol2) then combterm_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; + +fun clause_eq (cls1,cls2) = + let val lits1 = get_literals cls1 + val lits2 = get_literals cls2 + in + length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[])) + end; + +val xor_words = List.foldl Word.xorb 0w0; + +fun hash_combterm (CombVar(_,_),w) = w + | hash_combterm (CombFree(f,_),w) = Hashtable.hash_string(f,w) + | hash_combterm (CombConst(c,tp,tps),w) = Hashtable.hash_string(c,w) + | hash_combterm (CombApp(f,arg,tp),w) = + hash_combterm (arg, (hash_combterm (f,w))) + | hash_combterm (Bool(t),w) = hash_combterm (t,w) + | hash_combterm (Equal(t1,t2),w) = + List.foldl hash_combterm (Hashtable.hash_string ("equal",w)) [t1,t2] + +fun hash_literal (Literal(true,pred)) = hash_combterm(pred,0w0) + | hash_literal (Literal(false,pred)) = Word.notb(hash_combterm(pred,0w0)); + +fun hash_clause clause = xor_words (map hash_literal (get_literals clause)); + end \ No newline at end of file