author blanchet Thu Aug 25 23:38:09 2011 +0200 (2011-08-25) changeset 44501 5bde887b4785 parent 44500 dbd98b549597 child 44502 c537d5e5a365
make polymorphic encodings more complete
```     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 22:06:25 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 23:38:09 2011 +0200
1.3 @@ -202,10 +202,10 @@
1.4
1.5  fun formula_fold pos f =
1.6    let
1.7 -    fun aux pos (AQuant (_, _, phi)) = aux pos phi
1.8 -      | aux pos (AConn conn) = aconn_fold pos aux conn
1.9 -      | aux pos (AAtom tm) = f pos tm
1.10 -  in aux pos end
1.11 +    fun fld pos (AQuant (_, _, phi)) = fld pos phi
1.12 +      | fld pos (AConn conn) = aconn_fold pos fld conn
1.13 +      | fld pos (AAtom tm) = f pos tm
1.14 +  in fld pos end
1.15
1.16  fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
1.17    | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
```
```     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 22:06:25 2011 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 23:38:09 2011 +0200
2.3 @@ -1020,7 +1020,7 @@
2.4  fun preprocess_abstractions_in_terms trans_lambdas facts =
2.5    let
2.6      val (facts, lambda_ts) =
2.7 -      facts |> map (snd o snd) |> trans_lambdas
2.8 +      facts |> map (snd o snd) |> trans_lambdas
2.9              |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
2.10      val lambda_facts =
2.11        map2 (fn t => fn j =>
2.12 @@ -1246,8 +1246,8 @@
2.13        end
2.15  fun add_fact_syms_to_table ctxt explicit_apply =
2.16 -  formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply))
2.17 -  |> fact_lift
2.18 +  K (add_iterm_syms_to_table ctxt explicit_apply)
2.19 +  |> formula_fold NONE |> fact_lift
2.20
2.21  val tvar_a = TVar (("'a", 0), HOLogic.typeS)
2.22
2.23 @@ -1789,7 +1789,7 @@
2.24          #> fold (add_iterm_syms in_conj) args
2.25        end
2.27 -      fact_lift (formula_fold NONE (K (add_iterm_syms in_conj)))
2.28 +      K (add_iterm_syms in_conj) |> formula_fold NONE |> fact_lift
2.29      fun add_formula_var_types (AQuant (_, xs, phi)) =
2.30          fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
2.32 @@ -1885,6 +1885,22 @@
2.33         ? fold (add_fact_mononotonicity_info ctxt level) facts
2.34    end
2.35
2.36 +fun add_iformula_monotonic_types ctxt mono type_enc =
2.37 +  let
2.38 +    val level = level_of_type_enc type_enc
2.39 +    val should_encode = should_encode_type ctxt mono level
2.40 +    fun add_type T = should_encode T ? insert_type ctxt I T
2.41 +    fun add_term (tm as IApp (tm1, tm2)) =
2.44 +  in formula_fold NONE (K add_term) end
2.45 +fun add_fact_monotonic_types ctxt mono type_enc =
2.46 +  add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
2.47 +fun monotonic_types_for_facts ctxt mono type_enc facts =
2.48 +  [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
2.49 +         is_type_level_monotonicity_based (level_of_type_enc type_enc))
2.50 +        ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
2.51 +
2.52  fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
2.53    Formula (guards_sym_formula_prefix ^
2.54             ascii_of (mangled_type format type_enc T),
2.55 @@ -2046,17 +2062,9 @@
2.56         end)
2.57
2.58  fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
2.59 -                                     sym_decl_tab =
2.60 +                                     mono_Ts sym_decl_tab =
2.61    let
2.62      val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
2.63 -    val mono_Ts =
2.64 -      if polymorphism_of_type_enc type_enc = Polymorphic then
2.65 -        syms |> maps (map result_type_of_decl o snd)
2.66 -             |> filter_out (should_encode_type ctxt mono
2.67 -                                (level_of_type_enc type_enc))
2.68 -             |> rpair [] |-> fold (insert_type ctxt I)
2.69 -      else
2.70 -        []
2.71      val mono_lines =
2.72        problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
2.73      val decl_lines =
2.74 @@ -2131,11 +2139,14 @@
2.75      val helpers =
2.76        repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
2.77                         |> map repair
2.78 +    val mono_Ts =
2.79 +      helpers @ conjs @ facts
2.80 +      |> monotonic_types_for_facts ctxt mono type_enc
2.81      val sym_decl_lines =
2.82        (conjs, helpers @ facts)
2.83        |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
2.84        |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
2.85 -                                               type_enc
2.86 +                                               type_enc mono_Ts
2.87      val helper_lines =
2.88        0 upto length helpers - 1 ~~ helpers
2.89        |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
```