# HG changeset patch # User paulson # Date 1169023926 -3600 # Node ID 5084f53cef39801c17d8fe17bc872fd7f2577967 # Parent 2882d9cc5e75c558a9e0eac43ce432e33f15b275 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC minimize_applies is now by default TRUE! diff -r 2882d9cc5e75 -r 5084f53cef39 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Tue Jan 16 14:11:25 2007 +0100 +++ b/src/HOL/Tools/res_hol_clause.ML Wed Jan 17 09:52:06 2007 +0100 @@ -8,6 +8,8 @@ struct +structure RC = ResClause; + (* theorems for combinators and function extensionality *) val ext = thm "HOL.ext"; val comb_I = thm "ATP_Linkup.COMBI_def"; @@ -27,7 +29,7 @@ (*If true, each function will be directly applied to as many arguments as possible, avoiding use of the "apply" operator. Use of hBOOL is also minimized.*) -val minimize_applies = ref false; +val minimize_applies = ref true; val const_typargs = ref (Library.K [] : (string*typ -> typ list)); @@ -132,7 +134,7 @@ val tS = [tp',tq',t1] ---> tpq in compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds end end - | lam2comb (t as (Abs(x,t1,_))) _ = raise ResClause.CLAUSE("HOL CLAUSE",t); + | lam2comb (t as (Abs(x,t1,_))) _ = raise RC.CLAUSE("HOL CLAUSE",t); fun to_comb (Abs(x,tp,b)) bnds = lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds | to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds) @@ -158,10 +160,10 @@ type polarity = bool; type clause_id = int; -datatype combterm = CombConst of string * ResClause.fol_type * ResClause.fol_type list - | CombFree of string * ResClause.fol_type - | CombVar of string * ResClause.fol_type - | CombApp of combterm * combterm * ResClause.fol_type +datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list + | CombFree of string * RC.fol_type + | CombVar of string * RC.fol_type + | CombApp of combterm * combterm datatype literal = Literal of polarity * combterm; @@ -169,11 +171,11 @@ Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm, - kind: ResClause.kind, + kind: RC.kind, literals: literal list, - ctypes_sorts: (ResClause.typ_var * Term.sort) list, - ctvar_type_literals: ResClause.type_literal list, - ctfree_type_literals: ResClause.type_literal list}; + ctypes_sorts: (RC.typ_var * Term.sort) list, + ctvar_type_literals: RC.type_literal list, + ctfree_type_literals: RC.type_literal list}; (*********************************************************************) @@ -194,73 +196,44 @@ fun type_of (Type (a, Ts)) = let val (folTypes,ts) = types_of Ts - val t = ResClause.make_fixed_type_const a - in - (ResClause.mk_fol_type("Comp",t,folTypes), ts) - end + in (RC.Comp(RC.make_fixed_type_const a, 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 + (RC.AtomF (RC.make_fixed_type_var a), [RC.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 + (RC.AtomV (RC.make_schematic_type_var v), [RC.mk_typ_var_sort tp]) 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; + let val (folTyps,ts) = ListPair.unzip (map type_of Ts) + in (folTyps, RC.union_all ts) end; (* same as above, but no gathering of sort information *) fun simp_type_of (Type (a, Ts)) = - let val typs = map simp_type_of Ts - val t = ResClause.make_fixed_type_const a - in - ResClause.mk_fol_type("Comp",t,typs) - end - | 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,[]); + RC.Comp(RC.make_fixed_type_const a, map simp_type_of Ts) + | simp_type_of (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a) + | simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v); fun const_type_of (c,t) = - let val (tp,ts) = type_of t - val tvars = !const_typargs(c,t) - in - (tp, ts, map simp_type_of tvars) - end; + let val (tp,ts) = type_of t + in (tp, ts, map simp_type_of (!const_typargs(c,t))) end; (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) fun combterm_of (Const(c,t)) = let val (tp,ts,tvar_list) = const_type_of (c,t) - val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_list) - in - (c',ts) - end + val c' = CombConst(RC.make_fixed_const c, tp, tvar_list) + in (c',ts) end | combterm_of (Free(v,t)) = let val (tp,ts) = type_of t - val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp) - else CombFree(ResClause.make_fixed_var v,tp) - in - (v',ts) - end + val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp) + else CombFree(RC.make_fixed_var v,tp) + in (v',ts) end | combterm_of (Var(v,t)) = let val (tp,ts) = type_of t - val v' = CombVar(ResClause.make_schematic_var v,tp) - in - (v',ts) - end + val v' = CombVar(RC.make_schematic_var v,tp) + in (v',ts) end | combterm_of (t as (P $ Q)) = let val (P',tsP) = combterm_of P val (Q',tsQ) = combterm_of Q - val tp = Term.type_of t - val t' = CombApp(P',Q', simp_type_of tp) - in - (t',tsP union tsQ) - end; + in (CombApp(P',Q'), tsP union tsQ) end; fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity) | predicate_of (t,polarity) = (combterm_of t, polarity); @@ -279,7 +252,7 @@ (* making axiom and conjecture clauses *) fun make_clause(clause_id,axiom_name,kind,th) = let val (lits,ctypes_sorts) = literals_of_term (to_comb (prop_of th) []) - val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts + val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts in if forall isFalse lits then error "Problem too trivial for resolution (empty clause)" @@ -292,7 +265,7 @@ fun add_axiom_clause ((th,(name,id)), pairs) = - let val cls = make_clause(id, name, ResClause.Axiom, th) + let val cls = make_clause(id, name, RC.Axiom, th) in if isTaut cls then pairs else (name,cls)::pairs end; @@ -301,7 +274,7 @@ fun make_conjecture_clauses_aux _ [] = [] | make_conjecture_clauses_aux n (th::ths) = - make_clause(n,"conjecture", ResClause.Conjecture, th) :: + make_clause(n,"conjecture", RC.Conjecture, th) :: make_conjecture_clauses_aux (n+1) ths; val make_conjecture_clauses = make_conjecture_clauses_aux 0; @@ -316,22 +289,26 @@ val type_wrapper = "typeinfo"; fun wrap_type (c,tp) = case !typ_level of - T_FULL => type_wrapper ^ ResClause.paren_pack [c, ResClause.string_of_fol_type tp] + T_FULL => type_wrapper ^ RC.paren_pack [c, RC.string_of_fol_type tp] | _ => c; -val bool_tp = ResClause.make_fixed_type_const "bool"; +val bool_tp = RC.make_fixed_type_const "bool"; val app_str = "hAPP"; +(*Result of a function type; no need to check that the argument type matches.*) +fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2 + | result_type _ = raise ERROR "result_type" + fun type_of_combterm (CombConst(c,tp,_)) = tp | type_of_combterm (CombFree(v,tp)) = tp | type_of_combterm (CombVar(v,tp)) = tp - | type_of_combterm (CombApp(t1,t2,tp)) = tp; + | type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1); (*gets the head of a combinator application, along with the list of arguments*) fun strip_comb u = - let fun stripc (CombApp(t,u,_), ts) = stripc (t, u::ts) + let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) | stripc x = x in stripc(u,[]) end; @@ -340,41 +317,41 @@ in wrap_type (c',tp) end | string_of_combterm1 (CombFree(v,tp)) = wrap_type (v,tp) | string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp) - | string_of_combterm1 (CombApp(t1,t2,tp)) = + | string_of_combterm1 (CombApp(t1,t2)) = let val s1 = string_of_combterm1 t1 - val s2 = string_of_combterm1 t2 + and s2 = string_of_combterm1 t2 in case !typ_level of T_FULL => type_wrapper ^ - ResClause.paren_pack - [app_str ^ ResClause.paren_pack [s1,s2], - ResClause.string_of_fol_type tp] - | T_PARTIAL => app_str ^ ResClause.paren_pack - [s1,s2, ResClause.string_of_fol_type (type_of_combterm t1)] - | T_NONE => app_str ^ ResClause.paren_pack [s1,s2] + RC.paren_pack + [app_str ^ RC.paren_pack [s1,s2], + RC.string_of_fol_type (result_type (type_of_combterm t1))] + | T_PARTIAL => app_str ^ RC.paren_pack + [s1,s2, RC.string_of_fol_type (type_of_combterm t1)] + | T_NONE => app_str ^ RC.paren_pack [s1,s2] | T_CONST => raise ERROR "string_of_combterm1" end; fun rev_apply (v, []) = v - | rev_apply (v, arg::args) = app_str ^ ResClause.paren_pack [rev_apply (v, args), arg]; + | rev_apply (v, arg::args) = app_str ^ RC.paren_pack [rev_apply (v, args), arg]; fun string_apply (v, args) = rev_apply (v, rev args); (*Apply an operator to the argument strings, using either the "apply" operator or direct function application.*) -fun string_of_applic (CombConst(c,tp,tvars), args) = +fun string_of_applic (CombConst(c,_,tvars), args) = let val c = if c = "equal" then "c_fequal" else c val nargs = min_arity_of c - val args1 = List.take(args, nargs) @ (map ResClause.string_of_fol_type tvars) + val args1 = List.take(args, nargs) @ (map RC.string_of_fol_type tvars) handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^ Int.toString nargs ^ " but is applied to " ^ space_implode ", " args) val args2 = List.drop(args, nargs) in - string_apply (c ^ ResClause.paren_pack args1, args2) + string_apply (c ^ RC.paren_pack args1, args2) end - | string_of_applic (CombFree(v,tp), args) = string_apply (v, args) - | string_of_applic (CombVar(v,tp), args) = string_apply (v, args) + | string_of_applic (CombFree(v,_), args) = string_apply (v, args) + | string_of_applic (CombVar(v,_), args) = string_apply (v, args) | string_of_applic _ = raise ERROR "string_of_applic"; fun string_of_combterm2 t = @@ -386,20 +363,20 @@ | _ => string_of_combterm1 t; (*Boolean-valued terms are here converted to literals.*) -fun boolify t = "hBOOL" ^ ResClause.paren_pack [string_of_combterm t]; +fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t]; fun string_of_predicate t = case t of - (CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)) => + (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) => (*DFG only: new TPTP prefers infix equality*) - ("equal" ^ ResClause.paren_pack [string_of_combterm t1, string_of_combterm t2]) + ("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2]) | _ => case #1 (strip_comb t) of CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t | _ => boolify t; fun string_of_clausename (cls_id,ax_name) = - ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id; + RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id; fun string_of_type_clsname (cls_id,ax_name,idx) = string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); @@ -411,10 +388,10 @@ let val eqop = if pol then " = " else " != " in string_of_combterm t1 ^ eqop ^ string_of_combterm t2 end; -fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_))) = +fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) = tptp_of_equality pol (t1,t2) | tptp_literal (Literal(pol,pred)) = - ResClause.tptp_sign pol (string_of_predicate pred); + RC.tptp_sign pol (string_of_predicate pred); (*Given a clause, returns its literals paired with a list of literals concerning TFrees; the latter should only occur in conjecture clauses.*) @@ -422,17 +399,17 @@ let val lits = map tptp_literal (#literals cls) val ctvar_lits_strs = case !typ_level of T_NONE => [] - | _ => map ResClause.tptp_of_typeLit (#ctvar_type_literals cls) + | _ => map RC.tptp_of_typeLit (#ctvar_type_literals cls) val ctfree_lits = case !typ_level of T_NONE => [] - | _ => map ResClause.tptp_of_typeLit (#ctfree_type_literals cls) + | _ => map RC.tptp_of_typeLit (#ctfree_type_literals cls) in (ctvar_lits_strs @ lits, ctfree_lits) end; fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = let val (lits,ctfree_lits) = tptp_type_lits cls - val cls_str = ResClause.gen_tptp_cls(clause_id,axiom_name,kind,lits) + val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits) in (cls_str,ctfree_lits) end; @@ -440,42 +417,42 @@ (*** dfg format ***) -fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_predicate pred); +fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred); fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = let val lits = map dfg_literal literals - val (tvar_lits,tfree_lits) = ResClause.add_typs_aux ctypes_sorts + val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts val tvar_lits_strs = case !typ_level of T_NONE => [] - | _ => map ResClause.dfg_of_typeLit tvar_lits + | _ => map RC.dfg_of_typeLit tvar_lits val tfree_lits = case !typ_level of T_NONE => [] - | _ => map ResClause.dfg_of_typeLit tfree_lits + | _ => map RC.dfg_of_typeLit tfree_lits in (tvar_lits_strs @ lits, tfree_lits) end; -fun get_uvars (CombConst(_,_,_)) vars = vars - | get_uvars (CombFree(_,_)) vars = vars - | get_uvars (CombVar(v,tp)) vars = (v::vars) - | get_uvars (CombApp(P,Q,tp)) vars = get_uvars P (get_uvars Q vars); +fun get_uvars (CombConst _) vars = vars + | get_uvars (CombFree _) vars = vars + | get_uvars (CombVar(v,_)) vars = (v::vars) + | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars); fun get_uvars_l (Literal(_,c)) = get_uvars c []; -fun dfg_vars (Clause {literals,...}) = ResClause.union_all (map get_uvars_l literals); +fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals); fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = let val (lits,tfree_lits) = dfg_clause_aux cls val vars = dfg_vars cls - val tvars = ResClause.get_tvar_strs ctypes_sorts - val knd = ResClause.name_of_kind kind + val tvars = RC.get_tvar_strs ctypes_sorts + val knd = RC.name_of_kind kind val lits_str = commas lits - val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) + val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) in (cls_str, tfree_lits) end; (** For DFG format: accumulate function and predicate declarations **) -fun addtypes tvars tab = foldl ResClause.add_foltype_funcs tab tvars; +fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars; fun add_decls (CombConst(c,_,tvars), (funcs,preds)) = if c = "equal" then (addtypes tvars funcs, preds) @@ -490,10 +467,10 @@ end | _ => (addtypes tvars (Symtab.update(c,0) funcs), preds)) | add_decls (CombFree(v,ctp), (funcs,preds)) = - (ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds) + (RC.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds) | add_decls (CombVar(_,ctp), (funcs,preds)) = - (ResClause.add_foltype_funcs (ctp,funcs), preds) - | add_decls (CombApp(P,Q,_),decls) = add_decls(P,add_decls (Q,decls)); + (RC.add_foltype_funcs (ctp,funcs), preds) + | add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls)); fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls); @@ -507,19 +484,19 @@ val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses) in - (Symtab.dest (foldl ResClause.add_arityClause_funcs functab arity_clauses), + (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses), Symtab.dest predtab) end; fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) = - foldl ResClause.add_type_sort_preds preds ctypes_sorts + foldl RC.add_type_sort_preds preds ctypes_sorts handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities") (*Higher-order clauses have only the predicates hBOOL and type classes.*) fun preds_of_clauses clauses clsrel_clauses arity_clauses = Symtab.dest - (foldl ResClause.add_classrelClause_preds - (foldl ResClause.add_arityClause_preds + (foldl RC.add_classrelClause_preds + (foldl RC.add_arityClause_preds (foldl add_clause_preds Symtab.empty clauses) arity_clauses) clsrel_clauses) @@ -542,7 +519,7 @@ | SOME n => Symtab.update (c,n+1) ct) | count_combterm (CombFree(v,tp), ct) = ct | count_combterm (CombVar(v,tp), ct) = ct - | count_combterm (CombApp(t1,t2,tp), ct) = count_combterm(t1, count_combterm(t2, ct)); + | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct)); fun count_literal (Literal(_,t), ct) = count_combterm(t,ct); @@ -622,14 +599,14 @@ val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas) val _ = count_constants (conjectures, axclauses, helper_clauses); val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures) - val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss) + val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss) val out = TextIO.openOut filename in List.app (curry TextIO.output out o #1 o clause2tptp) axclauses; - ResClause.writeln_strs out tfree_clss; - ResClause.writeln_strs out tptp_clss; - List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses; - List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses; + RC.writeln_strs out tfree_clss; + RC.writeln_strs out tptp_clss; + List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses; + List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses; List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses; TextIO.closeOut out; clnames @@ -647,25 +624,25 @@ val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures) and probname = Path.implode (Path.base (Path.explode filename)) val axstrs = map (#1 o clause2dfg) axclauses - val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss) + val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss) val out = TextIO.openOut filename val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses in - TextIO.output (out, ResClause.string_of_start probname); - TextIO.output (out, ResClause.string_of_descrip probname); - TextIO.output (out, ResClause.string_of_symbols - (ResClause.string_of_funcs funcs) - (ResClause.string_of_preds (cl_preds @ ty_preds))); + TextIO.output (out, RC.string_of_start probname); + TextIO.output (out, RC.string_of_descrip probname); + TextIO.output (out, RC.string_of_symbols + (RC.string_of_funcs funcs) + (RC.string_of_preds (cl_preds @ ty_preds))); TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); - ResClause.writeln_strs out axstrs; - List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses; - List.app (curry TextIO.output out o ResClause.dfg_arity_clause) arity_clauses; - ResClause.writeln_strs out helper_clauses_strs; + RC.writeln_strs out axstrs; + List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses; + List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses; + RC.writeln_strs out helper_clauses_strs; TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); - ResClause.writeln_strs out tfree_clss; - ResClause.writeln_strs out dfg_clss; + RC.writeln_strs out tfree_clss; + RC.writeln_strs out dfg_clss; TextIO.output (out, "end_of_list.\n\n"); (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");