src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42534 46e690db16b8
parent 42533 dc81fe6b7a87
child 42538 9e3e45636459
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -55,6 +55,9 @@
     1.4  
     1.5  fun make_type ty = type_prefix ^ ascii_of ty
     1.6  
     1.7 +(* official TPTP TFF syntax *)
     1.8 +val tff_bool_type = "$o"
     1.9 +
    1.10  (* Freshness almost guaranteed! *)
    1.11  val sledgehammer_weak_prefix = "Sledgehammer:"
    1.12  
    1.13 @@ -117,9 +120,12 @@
    1.14  
    1.15  fun mk_anot phi = AConn (ANot, [phi])
    1.16  fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    1.17 +fun mk_aconns c phis =
    1.18 +  let val (phis', phi') = split_last phis in
    1.19 +    fold_rev (mk_aconn c) phis' phi'
    1.20 +  end
    1.21  fun mk_ahorn [] phi = phi
    1.22 -  | mk_ahorn (phi :: phis) psi =
    1.23 -    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
    1.24 +  | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
    1.25  fun mk_aquant _ [] phi = phi
    1.26    | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
    1.27      if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
    1.28 @@ -440,9 +446,10 @@
    1.29    fold_rev (curry (op ^) o g o prefix mangled_type_sep
    1.30              o mangled_combtyp_component f) tys ""
    1.31  
    1.32 -fun mangled_const (s, s') ty_args =
    1.33 -  (s ^ mangled_type_suffix fst ascii_of ty_args,
    1.34 -   s' ^ mangled_type_suffix snd I ty_args)
    1.35 +fun mangled_const_fst ty_args s = s ^ mangled_type_suffix fst ascii_of ty_args
    1.36 +fun mangled_const_snd ty_args s' = s' ^ mangled_type_suffix snd I ty_args
    1.37 +fun mangled_const ty_args (s, s') =
    1.38 +  (mangled_const_fst ty_args s, mangled_const_snd ty_args s')
    1.39  
    1.40  val parse_mangled_ident =
    1.41    Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
    1.42 @@ -471,6 +478,11 @@
    1.43      CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty])
    1.44    | _ => raise Fail "expected two-argument type constructor"
    1.45  
    1.46 +fun has_type_combatom ty tm =
    1.47 +  CombApp (CombConst ((const_prefix ^ is_base, is_base), pred_combtyp ty, [ty]),
    1.48 +           tm)
    1.49 +  |> AAtom
    1.50 +
    1.51  fun formula_for_combformula ctxt type_sys =
    1.52    let
    1.53      fun do_term top_level u =
    1.54 @@ -496,7 +508,7 @@
    1.55                     case type_arg_policy type_sys s'' of
    1.56                       No_Type_Args => (name, [])
    1.57                     | Explicit_Type_Args => (name, ty_args)
    1.58 -                   | Mangled_Types => (mangled_const name ty_args, [])
    1.59 +                   | Mangled_Types => (mangled_const ty_args name, [])
    1.60                   end)
    1.61            | CombVar (name, _) => (name, [])
    1.62            | CombApp _ => raise Fail "impossible \"CombApp\""
    1.63 @@ -514,16 +526,14 @@
    1.64      val do_out_of_bound_type =
    1.65        if member (op =) [Args true, Mangled true] type_sys then
    1.66          (fn (s, ty) =>
    1.67 -            CombApp (CombConst ((const_prefix ^ is_base, is_base),
    1.68 -                                pred_combtyp ty, [ty]),
    1.69 -                     CombVar (s, ty))
    1.70 -            |> AAtom |> formula_for_combformula ctxt type_sys |> SOME)
    1.71 +            has_type_combatom ty (CombVar (s, ty))
    1.72 +            |> formula_for_combformula ctxt type_sys |> SOME)
    1.73        else
    1.74          K NONE
    1.75      fun do_formula (AQuant (q, xs, phi)) =
    1.76          AQuant (q, xs |> map (apsnd (fn NONE => NONE
    1.77                                        | SOME ty => do_bound_type ty)),
    1.78 -                (if q = AForall then mk_ahorn else fold (mk_aconn AAnd))
    1.79 +                (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
    1.80                      (map_filter
    1.81                           (fn (_, NONE) => NONE
    1.82                             | (s, SOME ty) => do_out_of_bound_type (s, ty)) xs)
    1.83 @@ -710,43 +720,67 @@
    1.84    | repair_problem_line _ _ _ _ = raise Fail "unexpected non-formula"
    1.85  fun repair_problem thy = map o apsnd o map oo repair_problem_line thy
    1.86  
    1.87 -fun is_const_relevant s =
    1.88 -  case strip_prefix_and_unascii const_prefix s of
    1.89 -    SOME @{const_name HOL.eq} => false
    1.90 -  | opt => is_some opt
    1.91 +fun is_const_relevant type_sys sym_tab unmangled_s s =
    1.92 +  not (String.isPrefix bound_var_prefix unmangled_s) andalso
    1.93 +  unmangled_s <> "equal" andalso
    1.94 +  (type_sys = Many_Typed orelse not (is_pred_sym sym_tab s))
    1.95  
    1.96 -fun consider_combterm_consts sym_tab (*FIXME: use*) tm =
    1.97 +fun consider_combterm_consts type_sys sym_tab tm =
    1.98    let val (head, args) = strip_combterm_comb tm in
    1.99      (case head of
   1.100         CombConst ((s, s'), ty, ty_args) =>
   1.101         (* FIXME: exploit type subsumption *)
   1.102 -       is_const_relevant s ? Symtab.insert_list (op =) (s, (s', ty_args, ty))
   1.103 +       is_const_relevant type_sys sym_tab s
   1.104 +                         (s |> member (op =) [Many_Typed, Mangled true] type_sys
   1.105 +                               ? mangled_const_fst ty_args)
   1.106 +       ? Symtab.insert_list (op =) (s, (s', ty_args, ty))
   1.107       | _ => I) (* FIXME: hAPP on var *)
   1.108 -    #> fold (consider_combterm_consts sym_tab) args
   1.109 +    #> fold (consider_combterm_consts type_sys sym_tab) args
   1.110    end
   1.111  
   1.112 -fun consider_fact_consts sym_tab ({combformula, ...} : translated_formula) =
   1.113 -  fold_formula (consider_combterm_consts sym_tab) combformula
   1.114 +fun consider_fact_consts type_sys sym_tab
   1.115 +                         ({combformula, ...} : translated_formula) =
   1.116 +  fold_formula (consider_combterm_consts type_sys sym_tab) combformula
   1.117  
   1.118  fun const_table_for_facts type_sys sym_tab facts =
   1.119    Symtab.empty |> member (op =) [Many_Typed, Args true, Mangled true] type_sys
   1.120 -                  ? fold (consider_fact_consts sym_tab) facts
   1.121 +                  ? fold (consider_fact_consts type_sys sym_tab) facts
   1.122  
   1.123 -fun fo_type_from_combtyp (ty as CombType ((s, _), tys)) =
   1.124 +fun strip_and_map_combtyp f (ty as CombType ((s, _), tys)) =
   1.125      (case (strip_prefix_and_unascii type_const_prefix s, tys) of
   1.126         (SOME @{type_name fun}, [dom_ty, ran_ty]) =>
   1.127 -       fo_type_from_combtyp ran_ty |>> cons (mangled_combtyp dom_ty)
   1.128 -     | _ => ([], mangled_combtyp ty))
   1.129 -  | fo_type_from_combtyp ty = ([], mangled_combtyp ty)
   1.130 +       strip_and_map_combtyp f ran_ty |>> cons (f dom_ty)
   1.131 +     | _ => ([], f ty))
   1.132 +  | strip_and_map_combtyp f ty = ([], f ty)
   1.133  
   1.134 -fun type_decl_line_for_const_entry Many_Typed s (s', ty_args, ty) =
   1.135 +fun type_decl_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) =
   1.136 +  if type_sys = Many_Typed then
   1.137 +    let
   1.138 +      val (arg_tys, res_ty) = strip_and_map_combtyp mangled_combtyp ty
   1.139 +      val (s, s') = (s, s') |> mangled_const ty_args
   1.140 +    in
   1.141 +      Type_Decl (type_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
   1.142 +                 if is_pred_sym sym_tab s then `I tff_bool_type else res_ty)
   1.143 +    end
   1.144 +  else
   1.145      let
   1.146 -      val (s, s') = mangled_const (s, s') ty_args
   1.147 -      val (arg_tys, res_ty) = fo_type_from_combtyp ty
   1.148 -    in Type_Decl (type_decl_prefix ^ ascii_of s, (s, s'), arg_tys, res_ty) end
   1.149 -  | type_decl_line_for_const_entry _ _ _ = raise Fail "not implemented yet"
   1.150 -fun type_decl_lines_for_const type_sys (s, xs) =
   1.151 -  map (type_decl_line_for_const_entry type_sys s) xs
   1.152 +      val (arg_tys, res_ty) = strip_and_map_combtyp I ty
   1.153 +      val bounds =
   1.154 +        map (`I o make_bound_var o string_of_int) (1 upto length arg_tys)
   1.155 +        ~~ map SOME arg_tys
   1.156 +      val bound_tms =
   1.157 +        map (fn (name, ty) => CombConst (name, the ty, [])) bounds
   1.158 +    in
   1.159 +      Formula (type_decl_prefix ^ ascii_of s, Axiom,
   1.160 +               mk_aquant AForall bounds
   1.161 +                         (has_type_combatom res_ty
   1.162 +                              (fold (curry (CombApp o swap)) bound_tms
   1.163 +                                    (CombConst ((s, s'), ty, ty_args))))
   1.164 +               |> formula_for_combformula ctxt type_sys,
   1.165 +               NONE, NONE)
   1.166 +    end
   1.167 +fun type_decl_lines_for_const ctxt type_sys sym_tab (s, xs) =
   1.168 +  map (type_decl_line_for_const_entry ctxt type_sys sym_tab s) xs
   1.169  
   1.170  val factsN = "Relevant facts"
   1.171  val class_relsN = "Class relationships"
   1.172 @@ -786,7 +820,8 @@
   1.173                |> get_helper_facts ctxt type_sys
   1.174      val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts)
   1.175      val type_decl_lines =
   1.176 -      Symtab.fold_rev (append o type_decl_lines_for_const type_sys) const_tab []
   1.177 +      Symtab.fold_rev (append o type_decl_lines_for_const ctxt type_sys sym_tab)
   1.178 +                      const_tab []
   1.179      val helper_lines =
   1.180        helper_facts
   1.181        |>> map (pair 0