make sure typing fact names are unique (needed e.g. by SNARK)
authorblanchet
Sun May 01 18:37:24 2011 +0200 (2011-05-01)
changeset 425468591fcc56c34
parent 42545 a14b602fb3d5
child 42547 b5eec0c99528
make sure typing fact names are unique (needed e.g. by SNARK)
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
     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 @@ -102,7 +102,7 @@
     1.4       Many_Typed => false
     1.5     | Tags full_types => full_types orelse s = explicit_app_base
     1.6     | Args _ => s = explicit_app_base
     1.7 -   | Mangled _ => s = explicit_app_base
     1.8 +   | Mangled _ => false
     1.9     | No_Types => true)
    1.10  
    1.11  datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
    1.12 @@ -776,7 +776,7 @@
    1.13       | _ => ([], f ty))
    1.14    | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function"
    1.15  
    1.16 -fun problem_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) =
    1.17 +fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, ty) =
    1.18    let
    1.19      val thy = Proof_Context.theory_of ctxt
    1.20      val arity = min_arity_of thy type_sys sym_tab s
    1.21 @@ -786,7 +786,8 @@
    1.22          val (arg_tys, res_ty) = strip_and_map_combtyp arity mangled_combtyp ty
    1.23          val (s, s') = (s, s') |> mangled_const_name ty_args
    1.24        in
    1.25 -        Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
    1.26 +        Decl (sym_decl_prefix ^ ascii_of s, (s, s'),
    1.27 +              arg_tys,
    1.28                if is_pred_sym sym_tab s then `I tff_bool_type else res_ty)
    1.29        end
    1.30      else
    1.31 @@ -797,8 +798,10 @@
    1.32            ~~ map SOME arg_tys
    1.33          val bound_tms =
    1.34            map (fn (name, ty) => CombConst (name, the ty, [])) bounds
    1.35 +        val freshener =
    1.36 +          case type_sys of Args _ => string_of_int j ^ "_" | _ => ""
    1.37        in
    1.38 -        Formula (Fof, sym_decl_prefix ^ ascii_of s, Axiom,
    1.39 +        Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom,
    1.40                   CombConst ((s, s'), ty, ty_args)
    1.41                   |> fold (curry (CombApp o swap)) bound_tms
    1.42                   |> type_pred_combatom type_sys res_ty
    1.43 @@ -808,7 +811,8 @@
    1.44        end
    1.45    end
    1.46  fun problem_lines_for_const ctxt type_sys sym_tab (s, xs) =
    1.47 -  map (problem_line_for_const_entry ctxt type_sys sym_tab s) xs
    1.48 +  map2 (problem_line_for_typed_const ctxt type_sys sym_tab s)
    1.49 +       (0 upto length xs - 1) xs
    1.50  
    1.51  fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
    1.52      union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi