# HG changeset patch # User paulson # Date 1168765049 -3600 # Node ID 3d716cc9bd7adfdfc059264b9186a5acfcdada78 # Parent 71742560919279baeaa6eade105eb574ef2c9762 optimized translation of HO problems diff -r 717425609192 -r 3d716cc9bd7a src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Fri Jan 12 15:37:21 2007 +0100 +++ b/src/HOL/Tools/res_hol_clause.ML Sun Jan 14 09:57:29 2007 +0100 @@ -25,9 +25,25 @@ combinators appear to work best.*) val use_Turner = ref false; +(*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 const_typargs = ref (Library.K [] : (string*typ -> typ list)); -fun init thy = (const_typargs := Sign.const_typargs thy); +val const_min_arity = ref (Symtab.empty : int Symtab.table); + +val const_needs_hBOOL = ref (Symtab.empty : bool Symtab.table); + +fun min_arity_of c = getOpt (Symtab.lookup(!const_min_arity) c, 0); + +fun needs_hBOOL c = not (!minimize_applies) orelse + getOpt (Symtab.lookup(!const_needs_hBOOL) c, false); + +fun init thy = + (const_typargs := Sign.const_typargs thy; + const_min_arity := Symtab.empty; + const_needs_hBOOL := Symtab.empty); (**********************************************************************) (* convert a Term.term with lambdas into a Term.term with combinators *) @@ -38,14 +54,11 @@ | is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n)) | is_free _ _ = false; - -(*******************************************) fun mk_compact_comb (tm as (Const("ATP_Linkup.COMBB",_)$p) $ (Const("ATP_Linkup.COMBB",_)$q$r)) bnds = let val tp_p = Term.type_of1(bnds,p) val tp_q = Term.type_of1(bnds,q) val tp_r = Term.type_of1(bnds,r) - val typ = Term.type_of1(bnds,tm) - val typ_B' = [tp_p,tp_q,tp_r] ---> typ + val typ_B' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm) in Const("ATP_Linkup.COMBB'",typ_B') $ p $ q $ r end @@ -53,8 +66,7 @@ let val tp_p = Term.type_of1(bnds,p) val tp_q = Term.type_of1(bnds,q) val tp_r = Term.type_of1(bnds,r) - val typ = Term.type_of1(bnds,tm) - val typ_C' = [tp_p,tp_q,tp_r] ---> typ + val typ_C' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm) in Const("ATP_Linkup.COMBC'",typ_C') $ p $ q $ r end @@ -62,8 +74,7 @@ let val tp_p = Term.type_of1(bnds,p) val tp_q = Term.type_of1(bnds,q) val tp_r = Term.type_of1(bnds,r) - val typ = Term.type_of1(bnds,tm) - val typ_S' = [tp_p,tp_q,tp_r] ---> typ + val typ_S' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm) in Const("ATP_Linkup.COMBS'",typ_S') $ p $ q $ r end @@ -75,9 +86,7 @@ fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp-->tp) | lam2comb (Abs(x,tp,Bound n)) bnds = let val tb = List.nth(bnds,n-1) - in - Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ Bound (n-1) - end + in Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ Bound (n-1) end | lam2comb (Abs(x,t1,Const(c,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2) | lam2comb (Abs(x,t1,Free(v,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Free(v,t2) | lam2comb (Abs(x,t1,Var(ind,t2))) _ = Const("ATP_Linkup.COMBK", [t2,t1] ---> t2) $ Var(ind,t2) @@ -86,8 +95,7 @@ let val tI = [t1] ---> t1 val P' = lam2comb (Abs(x,t1,P)) bnds val tp' = Term.type_of1(bnds,P') - val tr = Term.type_of1(t1::bnds,P) - val tS = [tp',tI] ---> tr + val tS = [tp',tI] ---> Term.type_of1(t1::bnds,P) in compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Const("ATP_Linkup.COMBI",tI)) bnds @@ -101,44 +109,32 @@ if nfreeP andalso nfreeQ then let val tK = [tpq,t1] ---> tpq - val PQ' = incr_boundvars ~1 (P $ Q) - in - Const("ATP_Linkup.COMBK",tK) $ PQ' - end + in Const("ATP_Linkup.COMBK",tK) $ incr_boundvars ~1 (P $ Q) end else if nfreeP then let val Q' = lam2comb (Abs(x,t1,Q)) bnds val P' = incr_boundvars ~1 P val tp = Term.type_of1(bnds,P') val tq' = Term.type_of1(bnds, Q') val tB = [tp,tq',t1] ---> tpq - in - compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds - end + in compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds end else if nfreeQ then let val P' = lam2comb (Abs(x,t1,P)) bnds val Q' = incr_boundvars ~1 Q val tq = Term.type_of1(bnds,Q') val tp' = Term.type_of1(bnds, P') val tC = [tp',tq,t1] ---> tpq - in - compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds - end + in compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds end else let val P' = lam2comb (Abs(x,t1,P)) bnds val Q' = lam2comb (Abs(x,t1,Q)) bnds val tp' = Term.type_of1(bnds,P') val tq' = Term.type_of1(bnds,Q') val tS = [tp',tq',t1] ---> tpq - in - compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds - end + 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); -(*********************) - -fun to_comb (Abs(x,tp,b)) bnds = - lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds +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) | to_comb t _ = t; @@ -328,13 +324,17 @@ val app_str = "hAPP"; -val bool_str = "hBOOL"; - 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; +(*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) + | stripc x = x + in stripc(u,[]) end; + fun string_of_combterm1 (CombConst(c,tp,_)) = let val c' = if c = "equal" then "c_fequal" else c in wrap_type (c',tp) end @@ -355,25 +355,48 @@ | T_CONST => raise ERROR "string_of_combterm1" end; -fun string_of_combterm2 (CombConst(c,tp,tvars)) = - let val tvars' = map ResClause.string_of_fol_type tvars - val c' = if c = "equal" then "c_fequal" else c +fun rev_apply (v, []) = v + | rev_apply (v, arg::args) = app_str ^ ResClause.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) = + 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) + 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 - c' ^ ResClause.paren_pack tvars' + string_apply (c ^ ResClause.paren_pack args1, args2) end - | string_of_combterm2 (CombFree(v,tp)) = v - | string_of_combterm2 (CombVar(v,tp)) = v - | string_of_combterm2 (CombApp(t1,t2,_)) = - app_str ^ ResClause.paren_pack [string_of_combterm2 t1, string_of_combterm2 t2]; + | 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 _ = raise ERROR "string_of_applic"; + +fun string_of_combterm2 t = + let val (head, args) = strip_comb t + in string_of_applic (head, map string_of_combterm2 args) end; fun string_of_combterm t = case !typ_level of T_CONST => string_of_combterm2 t | _ => string_of_combterm1 t; - -fun string_of_predicate (CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)) = - ("equal" ^ ResClause.paren_pack [string_of_combterm t1, string_of_combterm t2]) - | string_of_predicate t = - bool_str ^ ResClause.paren_pack [string_of_combterm t] + +(*Boolean-valued terms are here converted to literals.*) +fun boolify t = "hBOOL" ^ ResClause.paren_pack [string_of_combterm t]; + +fun string_of_predicate t = + case t of + (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]) + | _ => + 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; @@ -393,6 +416,8 @@ | tptp_literal (Literal(pol,pred)) = ResClause.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.*) fun tptp_type_lits (Clause cls) = let val lits = map tptp_literal (#literals cls) val ctvar_lits_strs = @@ -405,7 +430,6 @@ (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) @@ -449,35 +473,43 @@ val cls_str = ResClause.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 init_funcs_tab funcs = - let val funcs1 = case !typ_level of T_PARTIAL => Symtab.update ("hAPP",3) funcs - | _ => Symtab.update ("hAPP",2) funcs - in - Symtab.update ("typeinfo",2) funcs1 - end; +fun addtypes tvars tab = foldl ResClause.add_foltype_funcs tab tvars; - -fun add_funcs (CombConst(c,_,tvars),funcs) = - if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars +fun add_decls (CombConst(c,_,tvars), (funcs,preds)) = + if c = "equal" then (addtypes tvars funcs, preds) else (case !typ_level of - T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars - | _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars) - | add_funcs (CombFree(v,ctp),funcs) = ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs) - | add_funcs (CombVar(_,ctp),funcs) = ResClause.add_foltype_funcs (ctp,funcs) - | add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs)); + T_CONST => + let val arity = min_arity_of c + length tvars + val addit = Symtab.update(c,arity) + in + if needs_hBOOL c then (addtypes tvars (addit funcs), preds) + else (addtypes tvars funcs, addit preds) + 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) + | 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)); -fun add_literal_funcs (Literal(_,c), funcs) = add_funcs (c,funcs); +fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls); -fun add_clause_funcs (Clause {literals, ...}, funcs) = - foldl add_literal_funcs funcs literals +fun add_clause_decls (Clause {literals, ...}, decls) = + foldl add_literal_decls decls literals handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities") -fun funcs_of_clauses clauses arity_clauses = - Symtab.dest (foldl ResClause.add_arityClause_funcs - (foldl add_clause_funcs (init_funcs_tab Symtab.empty) clauses) - arity_clauses) +fun decls_of_clauses clauses arity_clauses = + let val happ_ar = case !typ_level of T_PARTIAL => 3 | _ => 2 + val init_functab = Symtab.update ("typeinfo",2) (Symtab.update ("hAPP",happ_ar) Symtab.empty) + 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 predtab) + end; fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) = foldl ResClause.add_type_sort_preds preds ctypes_sorts @@ -488,8 +520,7 @@ Symtab.dest (foldl ResClause.add_classrelClause_preds (foldl ResClause.add_arityClause_preds - (Symtab.update ("hBOOL",1) - (foldl add_clause_preds Symtab.empty clauses)) + (foldl add_clause_preds Symtab.empty clauses) arity_clauses) clsrel_clauses) @@ -523,8 +554,10 @@ val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname) -fun get_helper_clauses ct = - let fun needed c = valOf (Symtab.lookup ct c) > 0 +fun get_helper_clauses (conjectures, axclauses, user_lemmas) = + let val ct0 = foldl count_clause init_counters conjectures + val ct = foldl (count_user_clause user_lemmas) ct0 axclauses + fun needed c = valOf (Symtab.lookup ct c) > 0 val IK = if needed "c_COMBI" orelse needed "c_COMBK" then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) else [] @@ -542,24 +575,57 @@ else [] val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal] in - make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') + map #2 (make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S')) end +(*Find the minimal arity of each function mentioned in the term. Also, note which uses + are not at top level, to see if hBOOL is needed.*) +fun count_constants_term toplev t = + let val (head, args) = strip_comb t + val n = length args + val _ = List.app (count_constants_term false) args + in + case head of + CombConst (a,_,_) => (*predicate or function version of "equal"?*) + let val a = if a="equal" andalso not toplev then "c_fequal" else a + in + const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity); + if toplev then () + else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL) + end + | ts => () + end; + +(*A literal is a top-level term*) +fun count_constants_lit (Literal (_,t)) = count_constants_term true t; + +fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals; + +fun display_arity (c,n) = + Output.debug ("Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ + (if needs_hBOOL c then " needs hBOOL" else "")); + +fun count_constants (conjectures, axclauses, helper_clauses) = + if !minimize_applies then + (List.app count_constants_clause conjectures; + List.app count_constants_clause axclauses; + List.app count_constants_clause helper_clauses; + List.app display_arity (Symtab.dest (!const_min_arity))) + else (); + (* tptp format *) (* write TPTP format to a single file *) -fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas = +fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas = let val conjectures = make_conjecture_clauses thms - val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses) + val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples) + 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 out = TextIO.openOut filename - val ct = foldl (count_user_clause user_lemmas) - (foldl count_clause init_counters conjectures) - axclauses' - val helper_clauses = map #2 (get_helper_clauses ct) + val out = TextIO.openOut filename in - List.app (curry TextIO.output out o #1 o clause2tptp) axclauses'; + 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; @@ -573,26 +639,25 @@ (* dfg format *) -fun dfg_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas = - let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) - val conjectures = make_conjecture_clauses thms - val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses) +fun dfg_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas = + let val conjectures = make_conjecture_clauses thms + val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples) + val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas) + val _ = count_constants (conjectures, axclauses, helper_clauses); 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 axstrs = map (#1 o clause2dfg) axclauses val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss) val out = TextIO.openOut filename - val ct = foldl (count_user_clause user_lemmas) - (foldl count_clause init_counters conjectures) - axclauses' - val helper_clauses = map #2 (get_helper_clauses ct) val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses - val funcs = funcs_of_clauses (helper_clauses @ conjectures @ axclauses') arity_clauses - and preds = preds_of_clauses axclauses' classrel_clauses arity_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 preds)); + TextIO.output (out, ResClause.string_of_symbols + (ResClause.string_of_funcs funcs) + (ResClause.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;