src/HOL/Tools/res_hol_clause.ML
 changeset 22825 bd774e01d6d5 parent 22130 0906fd95e0b5 child 22851 7b7d6e1c70b6
```     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Mon Apr 30 13:22:15 2007 +0200
1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Mon Apr 30 13:22:35 2007 +0200
1.3 @@ -1,7 +1,11 @@
1.4  (* ID: \$Id\$
1.5     Author: Jia Meng, NICTA
1.6
1.7 -FOL clauses translated from HOL formulae.  Combinators are used to represent lambda terms.
1.8 +FOL clauses translated from HOL formulae.
1.9 +
1.10 +The combinator code needs to be deleted after the translation paper has been published.
1.11 +It cannot be used with proof reconstruction because combinators are not introduced by proof.
1.12 +The Turner combinators (B', C', S') yield no improvement and should be deleted.
1.13  *)
1.14
1.15  structure ResHolClause =
1.16 @@ -23,12 +27,23 @@
1.17  val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
1.18  val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
1.19
1.20 +
1.21 +(*The different translations of types*)
1.22 +datatype type_level = T_FULL | T_PARTIAL | T_CONST;
1.23 +
1.24 +val typ_level = ref T_CONST;
1.25 +
1.26 +fun full_types () = (typ_level:=T_FULL);
1.27 +fun partial_types () = (typ_level:=T_PARTIAL);
1.28 +fun const_types_only () = (typ_level:=T_CONST);
1.29 +
1.30  (*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard
1.31    combinators appear to work best.*)
1.32  val use_Turner = ref false;
1.33
1.34  (*If true, each function will be directly applied to as many arguments as possible, avoiding
1.35 -  use of the "apply" operator. Use of hBOOL is also minimized.*)
1.36 +  use of the "apply" operator. Use of hBOOL is also minimized. It only works for the
1.37 +  constant-typed translation, though it could be tried for the partially-typed one.*)
1.38  val minimize_applies = ref true;
1.39
1.40  val const_typargs = ref (Library.K [] : (string*typ -> typ list));
1.41 @@ -39,7 +54,9 @@
1.42
1.43  fun min_arity_of c = getOpt (Symtab.lookup(!const_min_arity) c, 0);
1.44
1.45 -fun needs_hBOOL c = not (!minimize_applies) orelse
1.46 +(*True if the constant ever appears outside of the top-level position in literals.
1.47 +  If false, the constant always receives all of its arguments and is used as a predicate.*)
1.48 +fun needs_hBOOL c = not (!minimize_applies) orelse !typ_level<>T_CONST orelse
1.49                      getOpt (Symtab.lookup(!const_needs_hBOOL) c, false);
1.50
1.51  fun init thy =
1.52 @@ -145,17 +162,6 @@
1.53  (* data types for typed combinator expressions        *)
1.54  (******************************************************)
1.55
1.56 -datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE;
1.57 -
1.58 -val typ_level = ref T_CONST;
1.59 -
1.60 -fun full_types () = (typ_level:=T_FULL);
1.61 -fun partial_types () = (typ_level:=T_PARTIAL);
1.62 -fun const_types_only () = (typ_level:=T_CONST);
1.63 -fun no_types () = (typ_level:=T_NONE);
1.64 -
1.65 -fun find_typ_level () = !typ_level;
1.66 -
1.67  type axiom_name = string;
1.68  type polarity = bool;
1.69  type clause_id = int;
1.70 @@ -286,7 +292,7 @@
1.71  (* DFG used by SPASS                                                  *)
1.72  (**********************************************************************)
1.73
1.74 -val type_wrapper = "typeinfo";
1.75 +val type_wrapper = "ti";
1.76
1.77  fun wrap_type (c,tp) = case !typ_level of
1.78  	T_FULL => type_wrapper ^ RC.paren_pack [c, RC.string_of_fol_type tp]
1.79 @@ -312,6 +318,7 @@
1.80          |   stripc  x =  x
1.81      in  stripc(u,[])  end;
1.82
1.83 +(*Full and partial-typed transations*)
1.84  fun string_of_combterm1 (CombConst(c,tp,_)) =
1.85        let val c' = if c = "equal" then "c_fequal" else c
1.86        in  wrap_type (c',tp)  end
1.87 @@ -328,7 +335,6 @@
1.88  	                   RC.string_of_fol_type (result_type (type_of_combterm t1))]
1.89  	    | T_PARTIAL => app_str ^ RC.paren_pack
1.90  	                     [s1,s2, RC.string_of_fol_type (type_of_combterm t1)]
1.91 -	    | T_NONE => app_str ^ RC.paren_pack [s1,s2]
1.92  	    | T_CONST => raise ERROR "string_of_combterm1"
1.93        end;
1.94
1.95 @@ -354,6 +360,7 @@
1.96    | string_of_applic (CombVar(v,_), args) = string_apply (v, args)
1.97    | string_of_applic _ = raise ERROR "string_of_applic";
1.98
1.99 +(*Constant-typed transation*)
1.100  fun string_of_combterm2 t =
1.101    let val (head, args) = strip_comb t
1.102    in  string_of_applic (head, map string_of_combterm2 args)  end;
1.103 @@ -397,12 +404,8 @@
1.104    the latter should only occur in conjecture clauses.*)
1.105  fun tptp_type_lits (Clause cls) =
1.106      let val lits = map tptp_literal (#literals cls)
1.107 -	val ctvar_lits_strs =
1.108 -	    case !typ_level of T_NONE => []
1.109 -	      | _ => map RC.tptp_of_typeLit (#ctvar_type_literals cls)
1.110 -	val ctfree_lits =
1.111 -	    case !typ_level of T_NONE => []
1.112 -	      | _ => map RC.tptp_of_typeLit (#ctfree_type_literals cls)
1.113 +	val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls)
1.114 +	val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls)
1.115      in
1.116  	(ctvar_lits_strs @ lits, ctfree_lits)
1.117      end;
1.118 @@ -422,12 +425,8 @@
1.119  fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) =
1.120    let val lits = map dfg_literal literals
1.121        val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts
1.122 -      val tvar_lits_strs =
1.123 -	  case !typ_level of T_NONE => []
1.124 -	      | _ => map RC.dfg_of_typeLit tvar_lits
1.125 -      val tfree_lits =
1.126 -          case !typ_level of T_NONE => []
1.127 -	      | _ => map RC.dfg_of_typeLit tfree_lits
1.128 +      val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits
1.129 +      val tfree_lits = map RC.dfg_of_typeLit tfree_lits
1.130    in
1.131        (tvar_lits_strs @ lits, tfree_lits)
1.132    end;
1.133 @@ -454,7 +453,7 @@
1.134
1.136
1.137 -fun add_decls (CombConst(c,_,tvars), (funcs,preds)) =
1.138 +fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) =
1.139        if c = "equal" then (addtypes tvars funcs, preds)
1.140        else
1.141  	(case !typ_level of
1.142 @@ -465,7 +464,7 @@
1.145                 end
1.146 -           | _ => (addtypes tvars (Symtab.update(c,0) funcs), preds))
1.147 +           | _ => (RC.add_foltype_funcs (tp, Symtab.update(c,0) funcs), preds))
1.148    | add_decls (CombFree(v,ctp), (funcs,preds)) =
1.149        (RC.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds)
1.150    | add_decls (CombVar(_,ctp), (funcs,preds)) =
1.151 @@ -480,7 +479,7 @@
1.152
1.153  fun decls_of_clauses clauses arity_clauses =
1.154    let val happ_ar = case !typ_level of T_PARTIAL => 3 | _ => 2
1.155 -      val init_functab = Symtab.update ("typeinfo",2) (Symtab.update ("hAPP",happ_ar) Symtab.empty)
1.156 +      val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",happ_ar) Symtab.empty)
1.157        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
1.158        val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
1.159    in
1.160 @@ -583,7 +582,7 @@
1.161                  (if needs_hBOOL c then " needs hBOOL" else ""));
1.162
1.163  fun count_constants (conjectures, axclauses, helper_clauses) =
1.164 -  if !minimize_applies then
1.165 +  if !minimize_applies andalso !typ_level=T_CONST then
1.166      (List.app count_constants_clause conjectures;
1.167       List.app count_constants_clause axclauses;
1.168       List.app count_constants_clause helper_clauses;
```