author blanchet Tue Aug 30 16:07:45 2011 +0200 (2011-08-30) changeset 44593 ccf40af26ae9 parent 44592 54906b0337ab child 44594 ae82943481e9
implement more of the polymorphic simply typed format TFF(1)
```     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:07:45 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:07:45 2011 +0200
1.3 @@ -17,7 +17,9 @@
1.4      AConn of connective * ('a, 'b, 'c) formula list |
1.5      AAtom of 'c
1.6
1.7 -  datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
1.8 +  datatype 'a ho_type =
1.9 +    AType of 'a * 'a ho_type list |
1.10 +    AFun of 'a ho_type * 'a ho_type
1.11
1.12    datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
1.13    datatype tff_explicitness = TFF_Implicit | TFF_Explicit
1.14 @@ -118,7 +120,9 @@
1.15    AConn of connective * ('a, 'b, 'c) formula list |
1.16    AAtom of 'c
1.17
1.18 -datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
1.19 +datatype 'a ho_type =
1.20 +  AType of 'a * 'a ho_type list |
1.21 +  AFun of 'a ho_type * 'a ho_type
1.22
1.23  datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
1.24  datatype tff_explicitness = TFF_Implicit | TFF_Explicit
1.25 @@ -225,25 +229,29 @@
1.26    | string_for_kind Hypothesis = "hypothesis"
1.27    | string_for_kind Conjecture = "conjecture"
1.28
1.29 -fun strip_tff_type (AFun (AType s, ty)) = strip_tff_type ty |>> cons s
1.30 -  | strip_tff_type (AFun (AFun _, _)) =
1.31 +fun strip_tff_type (AFun (AFun _, _)) =
1.32      raise Fail "unexpected higher-order type in first-order format"
1.33 -  | strip_tff_type (AType s) = ([], s)
1.34 +  | strip_tff_type (AFun (ty1, ty2)) = strip_tff_type ty2 |>> cons ty1
1.35 +  | strip_tff_type ty = ([], ty)
1.36
1.37 -fun string_for_type (THF0 _) ty =
1.38 -    let
1.39 -      fun aux _ (AType s) = s
1.40 -        | aux rhs (AFun (ty1, ty2)) =
1.41 -          aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2
1.42 -          |> not rhs ? enclose "(" ")"
1.43 -    in aux true ty end
1.44 +fun general_string_for_type ty =
1.45 +  let
1.46 +    fun str _ (AType (s, [])) = s
1.47 +      | str _ (AType (s, tys)) = s ^ "(" ^ commas (map (str false) tys) ^ ")"
1.48 +      | str rhs (AFun (ty1, ty2)) =
1.49 +        str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
1.50 +        |> not rhs ? enclose "(" ")"
1.51 +  in str true ty end
1.52 +
1.53 +fun string_for_type (THF0 _) ty = general_string_for_type ty
1.54    | string_for_type (TFF _) ty =
1.55      (case strip_tff_type ty of
1.56 -       ([], s) => s
1.57 -     | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
1.58 -     | (ss, s) =>
1.59 -       "(" ^ space_implode (" " ^ tptp_product_type ^ " ") ss ^ ") " ^
1.60 -       tptp_fun_type ^ " " ^ s)
1.61 +       ([], ty) => general_string_for_type ty
1.62 +     | ([ty1], ty2) => general_string_for_type (AFun (ty1, ty2))
1.63 +     | (tys, ty) =>
1.64 +       "(" ^ space_implode (" " ^ tptp_product_type ^ " ")
1.65 +       (map general_string_for_type tys) ^ ") " ^ tptp_fun_type ^ " " ^
1.66 +       general_string_for_type ty)
1.67    | string_for_type _ _ = raise Fail "unexpected type in untyped format"
1.68
1.69  fun string_for_quantifier AForall = tptp_forall
1.70 @@ -256,11 +264,13 @@
1.71    | string_for_connective AIff = tptp_iff
1.72
1.73  fun string_for_bound_var format (s, ty) =
1.74 -  s ^ (if is_format_typed format then
1.75 -         " " ^ tptp_has_type ^ " " ^
1.76 -         string_for_type format (ty |> the_default (AType tptp_individual_type))
1.77 -       else
1.78 -         "")
1.79 +  s ^
1.80 +  (if is_format_typed format then
1.81 +     " " ^ tptp_has_type ^ " " ^
1.82 +     (ty |> the_default (AType (tptp_individual_type, []))
1.83 +         |> string_for_type format)
1.84 +   else
1.85 +     "")
1.86
1.87  fun string_for_term _ (ATerm (s, [])) = s
1.88    | string_for_term format (ATerm (s, ts)) =
1.89 @@ -440,9 +450,9 @@
1.90     symbols (with "\$i" as the type of individuals), but some provers (e.g.,
1.91     SNARK) require explicit declarations. The situation is similar for THF. *)
1.92
1.93 -val atype_of_types = AType (`I tptp_type_of_types)
1.94 -val bool_atype = AType (`I tptp_bool_type)
1.95 -val individual_atype = AType (`I tptp_individual_type)
1.96 +val atype_of_types = AType (`I tptp_type_of_types, [])
1.97 +val bool_atype = AType (`I tptp_bool_type, [])
1.98 +val individual_atype = AType (`I tptp_individual_type, [])
1.99
1.100  fun default_type pred_sym =
1.101    let
1.102 @@ -459,8 +469,9 @@
1.103    let
1.104      fun do_sym name ty =
1.105        if member (op =) declared name then I else AList.default (op =) (name, ty)
1.106 -    fun do_type (AFun (ty1, ty2)) = fold do_type [ty1, ty2]
1.107 -      | do_type (AType name) = do_sym name (K atype_of_types)
1.108 +    fun do_type (AType (name, tys)) =
1.109 +        do_sym name (K atype_of_types) #> fold do_type tys
1.110 +      | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
1.111      fun do_term pred_sym (ATerm (name as (s, _), tms)) =
1.112          is_tptp_user_symbol s
1.113          ? do_sym name (fn _ => default_type pred_sym (length tms))
1.114 @@ -557,7 +568,8 @@
1.115            end
1.116        in add 0 |> apsnd SOME end
1.117
1.118 -fun nice_type (AType name) = nice_name name #>> AType
1.119 +fun nice_type (AType (name, tys)) =
1.120 +    nice_name name ##>> pool_map nice_type tys #>> AType
1.121    | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
1.122  fun nice_term (ATerm (name, ts)) =
1.123      nice_name name ##>> pool_map nice_term ts #>> ATerm
```
```     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:45 2011 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:45 2011 +0200
2.3 @@ -763,11 +763,25 @@
2.4    | iterm_vars (IAbs (_, tm)) = iterm_vars tm
2.5  fun close_iformula_universally phi = close_universally iterm_vars phi
2.6
2.7 -fun term_vars bounds (ATerm (name as (s, _), tms)) =
2.8 -    (is_tptp_variable s andalso not (member (op =) bounds name))
2.9 -    ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms
2.10 -  | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm
2.11 -fun close_formula_universally phi = close_universally (term_vars []) phi
2.12 +fun term_vars type_enc =
2.13 +  let
2.14 +    fun vars bounds (ATerm (name as (s, _), tms)) =
2.15 +        (if is_tptp_variable s andalso not (member (op =) bounds name) then
2.16 +           (case type_enc of
2.17 +              Simple_Types (_, Polymorphic, _) =>
2.18 +              if String.isPrefix tvar_prefix s then
2.19 +                SOME (AType (`I tptp_type_of_types, []))
2.20 +              else
2.21 +                NONE
2.22 +            | _ => NONE)
2.23 +           |> pair name |> insert (op =)
2.24 +         else
2.25 +           I)
2.26 +        #> fold (vars bounds) tms
2.27 +      | vars bounds (AAbs ((name, _), tm)) = vars (name :: bounds) tm
2.28 +  in vars end
2.29 +fun close_formula_universally type_enc =
2.30 +  close_universally (term_vars type_enc [])
2.31
2.32  val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
2.33  val homo_infinite_type = Type (homo_infinite_type_name, [])
2.34 @@ -804,7 +818,7 @@
2.35  fun mangled_type format type_enc =
2.36    generic_mangled_type_name fst o ho_term_from_typ format type_enc
2.37
2.38 -val bool_atype = AType (`I tptp_bool_type)
2.39 +val bool_atype = AType (`I tptp_bool_type, [])
2.40
2.41  fun make_simple_type s =
2.42    if s = tptp_bool_type orelse s = tptp_fun_type orelse
2.43 @@ -815,9 +829,14 @@
2.44
2.45  fun ho_type_from_ho_term type_enc pred_sym ary =
2.46    let
2.47 -    fun to_atype ty =
2.48 +    fun to_mangled_atype ty =
2.49        AType ((make_simple_type (generic_mangled_type_name fst ty),
2.50 -              generic_mangled_type_name snd ty))
2.51 +              generic_mangled_type_name snd ty), [])
2.52 +    fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
2.53 +      | to_poly_atype _ = raise Fail "unexpected type abstraction"
2.54 +    val to_atype =
2.55 +      if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
2.56 +      else to_mangled_atype
2.57      fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
2.58      fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
2.59        | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
2.60 @@ -1454,7 +1473,7 @@
2.61    (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
2.62     else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
2.63    |> bound_tvars type_enc atomic_Ts
2.64 -  |> close_formula_universally
2.65 +  |> close_formula_universally type_enc
2.66
2.67  val type_tag = `(make_fixed_const NONE) type_tag_name
2.68
2.69 @@ -1717,7 +1736,7 @@
2.70                              should_guard_var_in_formula
2.71                              (if pos then SOME true else NONE)
2.72     |> bound_tvars type_enc atomic_types
2.73 -   |> close_formula_universally,
2.74 +   |> close_formula_universally type_enc,
2.75     NONE,
2.76     case locality of
2.77       Intro => isabelle_info introN
2.78 @@ -1726,13 +1745,13 @@
2.79     | _ => NONE)
2.80    |> Formula
2.81
2.82 -fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
2.83 -                                       : class_rel_clause) =
2.84 +fun formula_line_for_class_rel_clause type_enc
2.85 +        ({name, subclass, superclass, ...} : class_rel_clause) =
2.86    let val ty_arg = ATerm (`I "T", []) in
2.87      Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
2.88               AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
2.89                                 AAtom (ATerm (superclass, [ty_arg]))])
2.90 -             |> close_formula_universally, isabelle_info introN, NONE)
2.91 +             |> close_formula_universally type_enc, isabelle_info introN, NONE)
2.92    end
2.93
2.94  fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
2.95 @@ -1740,14 +1759,14 @@
2.96    | fo_literal_from_arity_literal (TVarLit (c, sort)) =
2.97      (false, ATerm (c, [ATerm (sort, [])]))
2.98
2.99 -fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
2.100 -                                   : arity_clause) =
2.101 +fun formula_line_for_arity_clause type_enc
2.102 +        ({name, prem_lits, concl_lits, ...} : arity_clause) =
2.103    Formula (arity_clause_prefix ^ name, Axiom,
2.104             mk_ahorn (map (formula_from_fo_literal o apfst not
2.105                            o fo_literal_from_arity_literal) prem_lits)
2.106                      (formula_from_fo_literal
2.107                           (fo_literal_from_arity_literal concl_lits))
2.108 -           |> close_formula_universally, isabelle_info introN, NONE)
2.109 +           |> close_formula_universally type_enc, isabelle_info introN, NONE)
2.110
2.111  fun formula_line_for_conjecture ctxt format mono type_enc
2.112          ({name, kind, iformula, atomic_types, ...} : translated_formula) =
2.113 @@ -1756,7 +1775,7 @@
2.114                 should_guard_var_in_formula (SOME false)
2.115                 (close_iformula_universally iformula)
2.116             |> bound_tvars type_enc atomic_types
2.117 -           |> close_formula_universally, NONE, NONE)
2.118 +           |> close_formula_universally type_enc, NONE, NONE)
2.119
2.120  fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
2.121    atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
2.122 @@ -1921,7 +1940,7 @@
2.123             |> formula_from_iformula ctxt format mono type_enc
2.124                                      (K (K (K (K true)))) (SOME true)
2.125             |> bound_tvars type_enc (atyps_of T)
2.126 -           |> close_formula_universally,
2.127 +           |> close_formula_universally type_enc,
2.128             isabelle_info introN, NONE)
2.129
2.130  fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
2.131 @@ -1983,7 +2002,7 @@
2.132               |> formula_from_iformula ctxt format mono type_enc
2.133                                        (K (K (K (K true)))) (SOME true)
2.134               |> n > 1 ? bound_tvars type_enc (atyps_of T)
2.135 -             |> close_formula_universally
2.136 +             |> close_formula_universally type_enc
2.137               |> maybe_negate,
2.138               isabelle_info introN, NONE)
2.139    end
2.140 @@ -2174,8 +2193,9 @@
2.141                                     (not exporter) (not exporter) mono
2.142                                     type_enc)
2.143              (0 upto length facts - 1 ~~ facts)),
2.144 -       (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
2.145 -       (aritiesN, map formula_line_for_arity_clause arity_clauses),
2.146 +       (class_relsN,
2.147 +        map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),
2.148 +       (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
2.149         (helpersN, helper_lines),
2.150         (conjsN,
2.151          map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
```