# HG changeset patch # User paulson # Date 1177932155 -7200 # Node ID bd774e01d6d5773573130642d4c1b4d90308b979 # Parent 51bb2f6ecc4a98f7300b28a851f2a43de30f8230 Fixing bugs in the partial-typed and fully-typed translations diff -r 51bb2f6ecc4a -r bd774e01d6d5 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Mon Apr 30 13:22:15 2007 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Mon Apr 30 13:22:35 2007 +0200 @@ -1,7 +1,11 @@ (* ID: $Id$ Author: Jia Meng, NICTA -FOL clauses translated from HOL formulae. Combinators are used to represent lambda terms. +FOL clauses translated from HOL formulae. + +The combinator code needs to be deleted after the translation paper has been published. +It cannot be used with proof reconstruction because combinators are not introduced by proof. +The Turner combinators (B', C', S') yield no improvement and should be deleted. *) structure ResHolClause = @@ -23,12 +27,23 @@ val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal"; val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal"; + +(*The different translations of types*) +datatype type_level = T_FULL | T_PARTIAL | T_CONST; + +val typ_level = ref T_CONST; + +fun full_types () = (typ_level:=T_FULL); +fun partial_types () = (typ_level:=T_PARTIAL); +fun const_types_only () = (typ_level:=T_CONST); + (*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard 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.*) + use of the "apply" operator. Use of hBOOL is also minimized. It only works for the + constant-typed translation, though it could be tried for the partially-typed one.*) val minimize_applies = ref true; val const_typargs = ref (Library.K [] : (string*typ -> typ list)); @@ -39,7 +54,9 @@ fun min_arity_of c = getOpt (Symtab.lookup(!const_min_arity) c, 0); -fun needs_hBOOL c = not (!minimize_applies) orelse +(*True if the constant ever appears outside of the top-level position in literals. + If false, the constant always receives all of its arguments and is used as a predicate.*) +fun needs_hBOOL c = not (!minimize_applies) orelse !typ_level<>T_CONST orelse getOpt (Symtab.lookup(!const_needs_hBOOL) c, false); fun init thy = @@ -145,17 +162,6 @@ (* data types for typed combinator expressions *) (******************************************************) -datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE; - -val typ_level = ref T_CONST; - -fun full_types () = (typ_level:=T_FULL); -fun partial_types () = (typ_level:=T_PARTIAL); -fun const_types_only () = (typ_level:=T_CONST); -fun no_types () = (typ_level:=T_NONE); - -fun find_typ_level () = !typ_level; - type axiom_name = string; type polarity = bool; type clause_id = int; @@ -286,7 +292,7 @@ (* DFG used by SPASS *) (**********************************************************************) -val type_wrapper = "typeinfo"; +val type_wrapper = "ti"; fun wrap_type (c,tp) = case !typ_level of T_FULL => type_wrapper ^ RC.paren_pack [c, RC.string_of_fol_type tp] @@ -312,6 +318,7 @@ | stripc x = x in stripc(u,[]) end; +(*Full and partial-typed transations*) fun string_of_combterm1 (CombConst(c,tp,_)) = let val c' = if c = "equal" then "c_fequal" else c in wrap_type (c',tp) end @@ -328,7 +335,6 @@ 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; @@ -354,6 +360,7 @@ | string_of_applic (CombVar(v,_), args) = string_apply (v, args) | string_of_applic _ = raise ERROR "string_of_applic"; +(*Constant-typed transation*) fun string_of_combterm2 t = let val (head, args) = strip_comb t in string_of_applic (head, map string_of_combterm2 args) end; @@ -397,12 +404,8 @@ 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 = - case !typ_level of T_NONE => [] - | _ => map RC.tptp_of_typeLit (#ctvar_type_literals cls) - val ctfree_lits = - case !typ_level of T_NONE => [] - | _ => map RC.tptp_of_typeLit (#ctfree_type_literals cls) + val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls) + val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls) in (ctvar_lits_strs @ lits, ctfree_lits) end; @@ -422,12 +425,8 @@ fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = let val lits = map dfg_literal literals val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts - val tvar_lits_strs = - case !typ_level of T_NONE => [] - | _ => map RC.dfg_of_typeLit tvar_lits - val tfree_lits = - case !typ_level of T_NONE => [] - | _ => map RC.dfg_of_typeLit tfree_lits + val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits + val tfree_lits = map RC.dfg_of_typeLit tfree_lits in (tvar_lits_strs @ lits, tfree_lits) end; @@ -454,7 +453,7 @@ fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars; -fun add_decls (CombConst(c,_,tvars), (funcs,preds)) = +fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) = if c = "equal" then (addtypes tvars funcs, preds) else (case !typ_level of @@ -465,7 +464,7 @@ 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)) + | _ => (RC.add_foltype_funcs (tp, Symtab.update(c,0) funcs), preds)) | add_decls (CombFree(v,ctp), (funcs,preds)) = (RC.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds) | add_decls (CombVar(_,ctp), (funcs,preds)) = @@ -480,7 +479,7 @@ 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_functab = Symtab.update (type_wrapper,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 @@ -583,7 +582,7 @@ (if needs_hBOOL c then " needs hBOOL" else "")); fun count_constants (conjectures, axclauses, helper_clauses) = - if !minimize_applies then + if !minimize_applies andalso !typ_level=T_CONST then (List.app count_constants_clause conjectures; List.app count_constants_clause axclauses; List.app count_constants_clause helper_clauses;