implement more of the polymorphic simply typed format TFF(1)
authorblanchet
Tue Aug 30 16:07:45 2011 +0200 (2011-08-30)
changeset 44593ccf40af26ae9
parent 44592 54906b0337ab
child 44594 ae82943481e9
implement more of the polymorphic simply typed format TFF(1)
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_translate.ML
     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),