added type abstractions (for declaring polymorphic constants) to TFF syntax
authorblanchet
Tue Aug 30 16:07:45 2011 +0200 (2011-08-30)
changeset 44594ae82943481e9
parent 44593 ccf40af26ae9
child 44595 444d111bde7d
added type abstractions (for declaring polymorphic constants) to TFF syntax
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 @@ -19,7 +19,8 @@
     1.4  
     1.5    datatype 'a ho_type =
     1.6      AType of 'a * 'a ho_type list |
     1.7 -    AFun of 'a ho_type * 'a ho_type
     1.8 +    AFun of 'a ho_type * 'a ho_type |
     1.9 +    ATyAbs of 'a list * 'a ho_type
    1.10  
    1.11    datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
    1.12    datatype tff_explicitness = TFF_Implicit | TFF_Explicit
    1.13 @@ -122,7 +123,8 @@
    1.14  
    1.15  datatype 'a ho_type =
    1.16    AType of 'a * 'a ho_type list |
    1.17 -  AFun of 'a ho_type * 'a ho_type
    1.18 +  AFun of 'a ho_type * 'a ho_type |
    1.19 +  ATyAbs of 'a list * 'a ho_type
    1.20  
    1.21  datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
    1.22  datatype tff_explicitness = TFF_Implicit | TFF_Explicit
    1.23 @@ -229,29 +231,38 @@
    1.24    | string_for_kind Hypothesis = "hypothesis"
    1.25    | string_for_kind Conjecture = "conjecture"
    1.26  
    1.27 -fun strip_tff_type (AFun (AFun _, _)) =
    1.28 +fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)
    1.29 +  | flatten_type (ty as AFun (ty1 as AType _, ty2)) =
    1.30 +    (case flatten_type ty2 of
    1.31 +       AFun (ty' as AType (s, tys), ty) =>
    1.32 +       AFun (AType (tptp_product_type,
    1.33 +                    ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)
    1.34 +     | _ => ty)
    1.35 +  | flatten_type (ty as AType _) = ty
    1.36 +  | flatten_type _ =
    1.37      raise Fail "unexpected higher-order type in first-order format"
    1.38 -  | strip_tff_type (AFun (ty1, ty2)) = strip_tff_type ty2 |>> cons ty1
    1.39 -  | strip_tff_type ty = ([], ty)
    1.40  
    1.41 -fun general_string_for_type ty =
    1.42 +fun str_for_type ty =
    1.43    let
    1.44      fun str _ (AType (s, [])) = s
    1.45 -      | str _ (AType (s, tys)) = s ^ "(" ^ commas (map (str false) tys) ^ ")"
    1.46 +      | str _ (AType (s, tys)) =
    1.47 +        tys |> map (str false) 
    1.48 +            |> (if s = tptp_product_type then
    1.49 +                  space_implode (" " ^ tptp_product_type ^ " ")
    1.50 +                  #> length tys > 1 ? enclose "(" ")"
    1.51 +                else
    1.52 +                  commas #> enclose "(" ")" #> prefix s)
    1.53        | str rhs (AFun (ty1, ty2)) =
    1.54          str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
    1.55          |> not rhs ? enclose "(" ")"
    1.56 +      | str _ (ATyAbs (ss, ty)) =
    1.57 +        tptp_forall ^ "[" ^
    1.58 +        commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
    1.59 +                    ss) ^ "] : " ^ str false ty
    1.60    in str true ty end
    1.61  
    1.62 -fun string_for_type (THF0 _) ty = general_string_for_type ty
    1.63 -  | string_for_type (TFF _) ty =
    1.64 -    (case strip_tff_type ty of
    1.65 -       ([], ty) => general_string_for_type ty
    1.66 -     | ([ty1], ty2) => general_string_for_type (AFun (ty1, ty2))
    1.67 -     | (tys, ty) =>
    1.68 -       "(" ^ space_implode (" " ^ tptp_product_type ^ " ")
    1.69 -       (map general_string_for_type tys) ^ ") " ^ tptp_fun_type ^ " " ^
    1.70 -       general_string_for_type ty)
    1.71 +fun string_for_type (THF0 _) ty = str_for_type ty
    1.72 +  | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
    1.73    | string_for_type _ _ = raise Fail "unexpected type in untyped format"
    1.74  
    1.75  fun string_for_quantifier AForall = tptp_forall
    1.76 @@ -469,9 +480,10 @@
    1.77    let
    1.78      fun do_sym name ty =
    1.79        if member (op =) declared name then I else AList.default (op =) (name, ty)
    1.80 -    fun do_type (AType (name, tys)) =
    1.81 -        do_sym name (K atype_of_types) #> fold do_type tys
    1.82 +    fun do_type_name name = do_sym name (K atype_of_types)
    1.83 +    fun do_type (AType (name, tys)) = do_type_name name #> fold do_type tys
    1.84        | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
    1.85 +      | do_type (ATyAbs (names, ty)) = fold do_type_name names #> do_type ty
    1.86      fun do_term pred_sym (ATerm (name as (s, _), tms)) =
    1.87          is_tptp_user_symbol s
    1.88          ? do_sym name (fn _ => default_type pred_sym (length tms))
    1.89 @@ -571,6 +583,8 @@
    1.90  fun nice_type (AType (name, tys)) =
    1.91      nice_name name ##>> pool_map nice_type tys #>> AType
    1.92    | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
    1.93 +  | nice_type (ATyAbs (names, ty)) =
    1.94 +    pool_map nice_name names ##>> nice_type ty #>> ATyAbs
    1.95  fun nice_term (ATerm (name, ts)) =
    1.96      nice_name name ##>> pool_map nice_term ts #>> ATerm
    1.97    | nice_term (AAbs ((name, ty), tm)) =
     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 @@ -495,6 +495,15 @@
     2.4    [new_skolem_const_prefix, s, string_of_int num_T_args]
     2.5    |> space_implode Long_Name.separator
     2.6  
     2.7 +fun robust_const_type thy s =
     2.8 +  if s = app_op_name then Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
     2.9 +  else s |> Sign.the_const_type thy
    2.10 +
    2.11 +(* This function only makes sense if "T" is as general as possible. *)
    2.12 +fun robust_const_typargs thy (s, T) =
    2.13 +  (s, T) |> Sign.const_typargs thy
    2.14 +  handle TYPE _ => [] |> Term.add_tvarsT T |> rev |> map TVar
    2.15 +
    2.16  (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
    2.17     Also accumulates sort infomation. *)
    2.18  fun iterm_from_term thy format bs (P $ Q) =
    2.19 @@ -504,10 +513,7 @@
    2.20      in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
    2.21    | iterm_from_term thy format _ (Const (c, T)) =
    2.22      (IConst (`(make_fixed_const (SOME format)) c, T,
    2.23 -             if String.isPrefix old_skolem_const_prefix c then
    2.24 -               [] |> Term.add_tvarsT T |> map TVar
    2.25 -             else
    2.26 -               (c, T) |> Sign.const_typargs thy),
    2.27 +             robust_const_typargs thy (c, T)),
    2.28       atyps_of T)
    2.29    | iterm_from_term _ _ _ (Free (s, T)) =
    2.30      (IConst (`make_fixed_var s, T,
    2.31 @@ -690,8 +696,7 @@
    2.32    Mangled_Type_Args of bool |
    2.33    No_Type_Args
    2.34  
    2.35 -fun should_drop_arg_type_args (Simple_Types _) =
    2.36 -    false (* since TFF doesn't support overloading *)
    2.37 +fun should_drop_arg_type_args (Simple_Types _) = false
    2.38    | should_drop_arg_type_args type_enc =
    2.39      level_of_type_enc type_enc = All_Types andalso
    2.40      uniformity_of_type_enc type_enc = Uniform
    2.41 @@ -783,8 +788,10 @@
    2.42  fun close_formula_universally type_enc =
    2.43    close_universally (term_vars type_enc [])
    2.44  
    2.45 -val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
    2.46 -val homo_infinite_type = Type (homo_infinite_type_name, [])
    2.47 +val fused_infinite_type_name = @{type_name ind} (* any infinite type *)
    2.48 +val fused_infinite_type = Type (fused_infinite_type_name, [])
    2.49 +
    2.50 +fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
    2.51  
    2.52  fun ho_term_from_typ format type_enc =
    2.53    let
    2.54 @@ -792,15 +799,14 @@
    2.55        ATerm (case (is_type_enc_higher_order type_enc, s) of
    2.56                 (true, @{type_name bool}) => `I tptp_bool_type
    2.57               | (true, @{type_name fun}) => `I tptp_fun_type
    2.58 -             | _ => if s = homo_infinite_type_name andalso
    2.59 +             | _ => if s = fused_infinite_type_name andalso
    2.60                         is_format_typed format then
    2.61                        `I tptp_individual_type
    2.62                      else
    2.63                        `make_fixed_type_const s,
    2.64               map term Ts)
    2.65      | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
    2.66 -    | term (TVar ((x as (s, _)), _)) =
    2.67 -      ATerm ((make_schematic_type_var x, s), [])
    2.68 +    | term (TVar (x, _)) = ATerm (tvar_name x, [])
    2.69    in term end
    2.70  
    2.71  fun ho_term_for_type_arg format type_enc T =
    2.72 @@ -1177,14 +1183,14 @@
    2.73         | _ => false)
    2.74    | should_tag_with_type _ _ _ _ _ _ = false
    2.75  
    2.76 -fun homogenized_type ctxt mono level =
    2.77 +fun fused_type ctxt mono level =
    2.78    let
    2.79      val should_encode = should_encode_type ctxt mono level
    2.80 -    fun homo 0 T = if should_encode T then T else homo_infinite_type
    2.81 -      | homo ary (Type (@{type_name fun}, [T1, T2])) =
    2.82 -        homo 0 T1 --> homo (ary - 1) T2
    2.83 -      | homo _ _ = raise Fail "expected function type"
    2.84 -  in homo end
    2.85 +    fun fuse 0 T = if should_encode T then T else fused_infinite_type
    2.86 +      | fuse ary (Type (@{type_name fun}, [T1, T2])) =
    2.87 +        fuse 0 T1 --> fuse (ary - 1) T2
    2.88 +      | fuse _ _ = raise Fail "expected function type"
    2.89 +  in fuse end
    2.90  
    2.91  (** predicators and application operators **)
    2.92  
    2.93 @@ -1361,13 +1367,7 @@
    2.94  
    2.95  fun filter_type_args _ _ _ [] = []
    2.96    | filter_type_args thy s arity T_args =
    2.97 -    let
    2.98 -      (* will throw "TYPE" for pseudo-constants *)
    2.99 -      val U = if s = app_op_name then
   2.100 -                @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
   2.101 -              else
   2.102 -                s |> Sign.the_const_type thy
   2.103 -    in
   2.104 +    let val U = robust_const_type thy s in
   2.105        case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
   2.106          [] => []
   2.107        | res_U_vars =>
   2.108 @@ -1688,8 +1688,7 @@
   2.109      val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
   2.110      val do_bound_type =
   2.111        case type_enc of
   2.112 -        Simple_Types (_, _, level) =>
   2.113 -        homogenized_type ctxt mono level 0
   2.114 +        Simple_Types (_, _, level) => fused_type ctxt mono level 0
   2.115          #> ho_type_from_typ format type_enc false 0 #> SOME
   2.116        | _ => K NONE
   2.117      fun do_out_of_bound_type pos phi universal (name, T) =
   2.118 @@ -1792,12 +1791,6 @@
   2.119  
   2.120  (** Symbol declarations **)
   2.121  
   2.122 -fun should_declare_sym type_enc pred_sym s =
   2.123 -  (case type_enc of
   2.124 -     Guards _ => not pred_sym
   2.125 -   | _ => true) andalso
   2.126 -  is_tptp_user_symbol s
   2.127 -
   2.128  fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
   2.129                               (conjs, facts) =
   2.130    let
   2.131 @@ -1805,8 +1798,15 @@
   2.132        let val (head, args) = strip_iterm_comb tm in
   2.133          (case head of
   2.134             IConst ((s, s'), T, T_args) =>
   2.135 -           let val pred_sym = is_pred_sym repaired_sym_tab s in
   2.136 -             if should_declare_sym type_enc pred_sym s then
   2.137 +           let
   2.138 +             val pred_sym = is_pred_sym repaired_sym_tab s
   2.139 +             val decl_sym =
   2.140 +               (case type_enc of
   2.141 +                  Guards _ => not pred_sym
   2.142 +                | _ => true) andalso
   2.143 +               is_tptp_user_symbol s
   2.144 +           in
   2.145 +             if decl_sym then
   2.146                 Symtab.map_default (s, [])
   2.147                     (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
   2.148                                           in_conj))
   2.149 @@ -1964,14 +1964,28 @@
   2.150  fun decl_line_for_sym ctxt format mono type_enc s
   2.151                        (s', T_args, T, pred_sym, ary, _) =
   2.152    let
   2.153 -    val (T_arg_Ts, level) =
   2.154 -      case type_enc of
   2.155 -        Simple_Types (_, _, level) => ([], level)
   2.156 -      | _ => (replicate (length T_args) homo_infinite_type, No_Types)
   2.157 +    val thy = Proof_Context.theory_of ctxt
   2.158 +    val (T, T_args) =
   2.159 +      if null T_args then
   2.160 +        (T, [])
   2.161 +      else case strip_prefix_and_unascii const_prefix s of
   2.162 +        SOME s' =>
   2.163 +        let
   2.164 +          val s' = s' |> invert_const
   2.165 +          val T = s' |> robust_const_type thy
   2.166 +        in (T, robust_const_typargs thy (s', T)) end
   2.167 +      | NONE =>
   2.168 +        case strip_prefix_and_unascii fixed_var_prefix s of
   2.169 +          SOME s' =>
   2.170 +          if String.isPrefix polymorphic_free_prefix s' then (tvar_a, [tvar_a])
   2.171 +          else raise Fail "unexpected type arguments to free variable"
   2.172 +        | NONE => raise Fail "unexpected type arguments"
   2.173    in
   2.174      Decl (sym_decl_prefix ^ s, (s, s'),
   2.175 -          (T_arg_Ts ---> (T |> homogenized_type ctxt mono level ary))
   2.176 -          |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
   2.177 +          T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
   2.178 +            |> ho_type_from_typ format type_enc pred_sym ary
   2.179 +            |> not (null T_args)
   2.180 +               ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
   2.181    end
   2.182  
   2.183  fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s