src/HOL/Tools/ATP/atp_translate.ML
changeset 44501 5bde887b4785
parent 44500 dbd98b549597
child 44502 c537d5e5a365
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 22:06:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 23:38:09 2011 +0200
     1.3 @@ -1020,7 +1020,7 @@
     1.4  fun preprocess_abstractions_in_terms trans_lambdas facts =
     1.5    let
     1.6      val (facts, lambda_ts) =
     1.7 -      facts |> map (snd o snd) |> trans_lambdas 
     1.8 +      facts |> map (snd o snd) |> trans_lambdas
     1.9              |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
    1.10      val lambda_facts =
    1.11        map2 (fn t => fn j =>
    1.12 @@ -1246,8 +1246,8 @@
    1.13        end
    1.14    in add true end
    1.15  fun add_fact_syms_to_table ctxt explicit_apply =
    1.16 -  formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply))
    1.17 -  |> fact_lift
    1.18 +  K (add_iterm_syms_to_table ctxt explicit_apply)
    1.19 +  |> formula_fold NONE |> fact_lift
    1.20  
    1.21  val tvar_a = TVar (("'a", 0), HOLogic.typeS)
    1.22  
    1.23 @@ -1789,7 +1789,7 @@
    1.24          #> fold (add_iterm_syms in_conj) args
    1.25        end
    1.26      fun add_fact_syms in_conj =
    1.27 -      fact_lift (formula_fold NONE (K (add_iterm_syms in_conj)))
    1.28 +      K (add_iterm_syms in_conj) |> formula_fold NONE |> fact_lift
    1.29      fun add_formula_var_types (AQuant (_, xs, phi)) =
    1.30          fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
    1.31          #> add_formula_var_types phi
    1.32 @@ -1885,6 +1885,22 @@
    1.33         ? fold (add_fact_mononotonicity_info ctxt level) facts
    1.34    end
    1.35  
    1.36 +fun add_iformula_monotonic_types ctxt mono type_enc =
    1.37 +  let
    1.38 +    val level = level_of_type_enc type_enc
    1.39 +    val should_encode = should_encode_type ctxt mono level
    1.40 +    fun add_type T = should_encode T ? insert_type ctxt I T
    1.41 +    fun add_term (tm as IApp (tm1, tm2)) =
    1.42 +        add_type (ityp_of tm) #> add_term tm1 #> add_term tm2
    1.43 +      | add_term tm = add_type (ityp_of tm)
    1.44 +  in formula_fold NONE (K add_term) end
    1.45 +fun add_fact_monotonic_types ctxt mono type_enc =
    1.46 +  add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
    1.47 +fun monotonic_types_for_facts ctxt mono type_enc facts =
    1.48 +  [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
    1.49 +         is_type_level_monotonicity_based (level_of_type_enc type_enc))
    1.50 +        ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
    1.51 +
    1.52  fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
    1.53    Formula (guards_sym_formula_prefix ^
    1.54             ascii_of (mangled_type format type_enc T),
    1.55 @@ -2046,17 +2062,9 @@
    1.56         end)
    1.57  
    1.58  fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
    1.59 -                                     sym_decl_tab =
    1.60 +                                     mono_Ts sym_decl_tab =
    1.61    let
    1.62      val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
    1.63 -    val mono_Ts =
    1.64 -      if polymorphism_of_type_enc type_enc = Polymorphic then
    1.65 -        syms |> maps (map result_type_of_decl o snd)
    1.66 -             |> filter_out (should_encode_type ctxt mono
    1.67 -                                (level_of_type_enc type_enc))
    1.68 -             |> rpair [] |-> fold (insert_type ctxt I)
    1.69 -      else
    1.70 -        []
    1.71      val mono_lines =
    1.72        problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
    1.73      val decl_lines =
    1.74 @@ -2131,11 +2139,14 @@
    1.75      val helpers =
    1.76        repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
    1.77                         |> map repair
    1.78 +    val mono_Ts =
    1.79 +      helpers @ conjs @ facts
    1.80 +      |> monotonic_types_for_facts ctxt mono type_enc
    1.81      val sym_decl_lines =
    1.82        (conjs, helpers @ facts)
    1.83        |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
    1.84        |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
    1.85 -                                               type_enc
    1.86 +                                               type_enc mono_Ts
    1.87      val helper_lines =
    1.88        0 upto length helpers - 1 ~~ helpers
    1.89        |> map (formula_line_for_fact ctxt format helper_prefix I false true mono