src/HOL/Tools/ATP/atp_translate.ML
changeset 44772 60ac7b56296a
parent 44771 0e5d4388bbac
child 44773 e701dabbfe37
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
     1.3 @@ -408,7 +408,7 @@
     1.4  
     1.5  fun multi_arity_clause [] = []
     1.6    | multi_arity_clause ((tcons, ars) :: tc_arlists) =
     1.7 -      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
     1.8 +    arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
     1.9  
    1.10  (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
    1.11     theory thy provided its arguments have the corresponding sorts. *)
    1.12 @@ -1215,7 +1215,7 @@
    1.13  
    1.14  fun add_iterm_syms_to_table ctxt explicit_apply =
    1.15    let
    1.16 -    fun consider_var_arity const_T var_T max_ary =
    1.17 +    fun consider_var_ary const_T var_T max_ary =
    1.18        let
    1.19          fun iter ary T =
    1.20            if ary = max_ary orelse type_instance ctxt var_T T orelse
    1.21 @@ -1229,9 +1229,9 @@
    1.22           (can dest_funT T orelse T = @{typ bool}) then
    1.23          let
    1.24            val bool_vars' = bool_vars orelse body_type T = @{typ bool}
    1.25 -          fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
    1.26 +          fun repair_min_ary {pred_sym, min_ary, max_ary, types} =
    1.27              {pred_sym = pred_sym andalso not bool_vars',
    1.28 -             min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
    1.29 +             min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
    1.30               max_ary = max_ary, types = types}
    1.31            val fun_var_Ts' =
    1.32              fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
    1.33 @@ -1240,7 +1240,7 @@
    1.34               pointer_eq (fun_var_Ts', fun_var_Ts) then
    1.35              accum
    1.36            else
    1.37 -            ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
    1.38 +            ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
    1.39          end
    1.40        else
    1.41          accum
    1.42 @@ -1267,7 +1267,7 @@
    1.43                           pointer_eq (types', types) then
    1.44                          min_ary
    1.45                        else
    1.46 -                        fold (consider_var_arity T) fun_var_Ts min_ary
    1.47 +                        fold (consider_var_ary T) fun_var_Ts min_ary
    1.48                    in
    1.49                      Symtab.update (s, {pred_sym = pred_sym,
    1.50                                         min_ary = Int.min (ary, min_ary),
    1.51 @@ -1282,7 +1282,7 @@
    1.52                        case explicit_apply of
    1.53                          SOME true => 0
    1.54                        | SOME false => ary
    1.55 -                      | NONE => fold (consider_var_arity T) fun_var_Ts ary
    1.56 +                      | NONE => fold (consider_var_ary T) fun_var_Ts ary
    1.57                    in
    1.58                      Symtab.update_new (s, {pred_sym = pred_sym,
    1.59                                             min_ary = min_ary, max_ary = ary,
    1.60 @@ -1316,7 +1316,7 @@
    1.61    |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
    1.62    |> fold Symtab.update default_sym_tab_entries
    1.63  
    1.64 -fun min_arity_of sym_tab s =
    1.65 +fun min_ary_of sym_tab s =
    1.66    case Symtab.lookup sym_tab s of
    1.67      SOME ({min_ary, ...} : sym_info) => min_ary
    1.68    | NONE =>
    1.69 @@ -1368,7 +1368,7 @@
    1.70        case strip_iterm_comb tm of
    1.71          (head as IConst ((s, _), _, _), args) =>
    1.72          args |> map aux
    1.73 -             |> chop (min_arity_of sym_tab s)
    1.74 +             |> chop (min_ary_of sym_tab s)
    1.75               |>> list_app head
    1.76               |-> list_explicit_app
    1.77        | (head, args) => list_explicit_app head (map aux args)
    1.78 @@ -1380,10 +1380,10 @@
    1.79    | chop_fun _ T = ([], T)
    1.80  
    1.81  fun filter_type_args _ _ _ [] = []
    1.82 -  | filter_type_args thy s arity T_args =
    1.83 +  | filter_type_args thy s ary T_args =
    1.84      let
    1.85        val U = robust_const_type thy s
    1.86 -      val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun arity |> fst) []
    1.87 +      val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
    1.88        val U_args = (s, U) |> robust_const_typargs thy
    1.89      in
    1.90        U_args ~~ T_args
    1.91 @@ -1395,8 +1395,8 @@
    1.92  fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
    1.93    let
    1.94      val thy = Proof_Context.theory_of ctxt
    1.95 -    fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
    1.96 -      | aux arity (IConst (name as (s, _), T, T_args)) =
    1.97 +    fun aux ary (IApp (tm1, tm2)) = IApp (aux (ary + 1) tm1, aux 0 tm2)
    1.98 +      | aux ary (IConst (name as (s, _), T, T_args)) =
    1.99          (case strip_prefix_and_unascii const_prefix s of
   1.100             NONE =>
   1.101             (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
   1.102 @@ -1405,7 +1405,7 @@
   1.103             let
   1.104               val s'' = invert_const s''
   1.105               fun filter_T_args false = T_args
   1.106 -               | filter_T_args true = filter_type_args thy s'' arity T_args
   1.107 +               | filter_T_args true = filter_type_args thy s'' ary T_args
   1.108             in
   1.109               case type_arg_policy type_enc s'' of
   1.110                 Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
   1.111 @@ -2251,7 +2251,7 @@
   1.112                       else NONE)
   1.113                   ((helpers_offset + 1 upto helpers_offset + length helpers)
   1.114                    ~~ helpers)
   1.115 -    fun add_sym_arity (s, {min_ary, ...} : sym_info) =
   1.116 +    fun add_sym_ary (s, {min_ary, ...} : sym_info) =
   1.117        if min_ary > 0 then
   1.118          case strip_prefix_and_unascii const_prefix s of
   1.119            SOME s => Symtab.insert (op =) (s, min_ary)
   1.120 @@ -2265,7 +2265,7 @@
   1.121       offset_of_heading_in_problem factsN problem 0,
   1.122       fact_names |> Vector.fromList,
   1.123       typed_helpers,
   1.124 -     Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
   1.125 +     Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
   1.126    end
   1.127  
   1.128  (* FUDGE *)