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.135  fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars;
   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.143                     if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
   1.144                     else (addtypes tvars funcs, addit preds)
   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;