make polymorphic encodings more complete
authorblanchet
Thu Aug 25 23:38:09 2011 +0200 (2011-08-25)
changeset 445015bde887b4785
parent 44500 dbd98b549597
child 44502 c537d5e5a365
make polymorphic encodings more complete
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_translate.ML
     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.14    in add true 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.26      fun add_fact_syms in_conj =
    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.31          #> add_formula_var_types phi
    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.42 +        add_type (ityp_of tm) #> add_term tm1 #> add_term tm2
    2.43 +      | add_term tm = add_type (ityp_of tm)
    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