src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
changeset 35963 943e2582dc87
parent 35865 2f8fb5242799
child 36167 c1a35be8e476
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Mar 22 15:23:18 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Mar 23 11:39:21 2010 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4  open Sledgehammer_FOL_Clause
     1.5  open Sledgehammer_Fact_Preprocessor
     1.6  
     1.7 -(* Parameter t_full below indicates that full type information is to be
     1.8 +(* Parameter "full_types" below indicates that full type information is to be
     1.9  exported *)
    1.10  
    1.11  (* If true, each function will be directly applied to as many arguments as
    1.12 @@ -210,10 +210,8 @@
    1.13  fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
    1.14    | head_needs_hBOOL _ _ = true;
    1.15  
    1.16 -fun wrap_type t_full (s, tp) =
    1.17 -  if t_full then
    1.18 -      type_wrapper ^ paren_pack [s, string_of_fol_type tp]
    1.19 -  else s;
    1.20 +fun wrap_type full_types (s, tp) =
    1.21 +  if full_types then type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s;
    1.22  
    1.23  fun apply ss = "hAPP" ^ paren_pack ss;
    1.24  
    1.25 @@ -224,7 +222,7 @@
    1.26  
    1.27  (*Apply an operator to the argument strings, using either the "apply" operator or
    1.28    direct function application.*)
    1.29 -fun string_of_applic t_full cma (CombConst (c, _, tvars), args) =
    1.30 +fun string_of_applic full_types cma (CombConst (c, _, tvars), args) =
    1.31        let val c = if c = "equal" then "c_fequal" else c
    1.32            val nargs = min_arity_of cma c
    1.33            val args1 = List.take(args, nargs)
    1.34 @@ -232,21 +230,22 @@
    1.35                                           Int.toString nargs ^ " but is applied to " ^
    1.36                                           space_implode ", " args)
    1.37            val args2 = List.drop(args, nargs)
    1.38 -          val targs = if not t_full then map string_of_fol_type tvars else []
    1.39 +          val targs = if full_types then [] else map string_of_fol_type tvars
    1.40        in
    1.41            string_apply (c ^ paren_pack (args1@targs), args2)
    1.42        end
    1.43    | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
    1.44    | string_of_applic _ _ _ = error "string_of_applic";
    1.45  
    1.46 -fun wrap_type_if t_full cnh (head, s, tp) =
    1.47 -  if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
    1.48 +fun wrap_type_if full_types cnh (head, s, tp) =
    1.49 +  if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else s;
    1.50  
    1.51 -fun string_of_combterm (params as (t_full, cma, cnh)) t =
    1.52 +fun string_of_combterm (params as (full_types, cma, cnh)) t =
    1.53    let val (head, args) = strip_combterm_comb t
    1.54 -  in  wrap_type_if t_full cnh (head,
    1.55 -                    string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
    1.56 -                    type_of_combterm t)
    1.57 +  in  wrap_type_if full_types cnh (head,
    1.58 +          string_of_applic full_types cma
    1.59 +                           (head, map (string_of_combterm (params)) args),
    1.60 +          type_of_combterm t)
    1.61    end;
    1.62  
    1.63  (*Boolean-valued terms are here converted to literals.*)
    1.64 @@ -318,11 +317,11 @@
    1.65  
    1.66  fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
    1.67  
    1.68 -fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
    1.69 +fun add_decls (full_types, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
    1.70        if c = "equal" then (addtypes tvars funcs, preds)
    1.71        else
    1.72          let val arity = min_arity_of cma c
    1.73 -            val ntys = if not t_full then length tvars else 0
    1.74 +            val ntys = if not full_types then length tvars else 0
    1.75              val addit = Symtab.update(c, arity+ntys)
    1.76          in
    1.77              if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
    1.78 @@ -452,12 +451,12 @@
    1.79  
    1.80  (* TPTP format *)
    1.81  
    1.82 -fun write_tptp_file t_full file clauses =
    1.83 +fun write_tptp_file full_types file clauses =
    1.84    let
    1.85      val (conjectures, axclauses, _, helper_clauses,
    1.86        classrel_clauses, arity_clauses) = clauses
    1.87      val (cma, cnh) = count_constants clauses
    1.88 -    val params = (t_full, cma, cnh)
    1.89 +    val params = (full_types, cma, cnh)
    1.90      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
    1.91      val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
    1.92      val _ =
    1.93 @@ -474,12 +473,12 @@
    1.94  
    1.95  (* DFG format *)
    1.96  
    1.97 -fun write_dfg_file t_full file clauses =
    1.98 +fun write_dfg_file full_types file clauses =
    1.99    let
   1.100      val (conjectures, axclauses, _, helper_clauses,
   1.101        classrel_clauses, arity_clauses) = clauses
   1.102      val (cma, cnh) = count_constants clauses
   1.103 -    val params = (t_full, cma, cnh)
   1.104 +    val params = (full_types, cma, cnh)
   1.105      val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
   1.106      and probname = Path.implode (Path.base file)
   1.107      val axstrs = map (#1 o (clause2dfg params)) axclauses