more tuning
authorblanchet
Wed Aug 31 11:23:16 2011 +0200 (2011-08-31)
changeset 44624b82085db501f
parent 44623 1e2d5cdef3d0
child 44625 4a1132815a70
more tuning
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 11:14:53 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 11:23:16 2011 +0200
     1.3 @@ -367,19 +367,17 @@
     1.4  
     1.5  (** Isabelle arities **)
     1.6  
     1.7 -datatype arity_literal =
     1.8 -  AryLitConst of name * name * name list |
     1.9 -  AryLitVar of name * name
    1.10 +type arity_literal = name * name * name list
    1.11  
    1.12  val type_class = the_single @{sort type}
    1.13  
    1.14  fun add_packed_sort tvar =
    1.15 -  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
    1.16 +  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
    1.17  
    1.18  type arity_clause =
    1.19    {name : string,
    1.20     prem_lits : arity_literal list,
    1.21 -   concl_lits : arity_literal}
    1.22 +   concl_lit : arity_literal}
    1.23  
    1.24  (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
    1.25  fun make_axiom_arity_clause (tcons, name, (cls, args)) =
    1.26 @@ -388,11 +386,9 @@
    1.27      val tvars_srts = ListPair.zip (tvars, args)
    1.28    in
    1.29      {name = name,
    1.30 -     prem_lits =
    1.31 -       [] |> fold (uncurry add_packed_sort) tvars_srts |> map AryLitVar,
    1.32 -     concl_lits =
    1.33 -       AryLitConst (`make_type_class cls, `make_fixed_type_const tcons,
    1.34 -                    tvars ~~ tvars)}
    1.35 +     prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts,
    1.36 +     concl_lit = (`make_type_class cls, `make_fixed_type_const tcons,
    1.37 +                  tvars ~~ tvars)}
    1.38    end
    1.39  
    1.40  fun arity_clause _ _ (_, []) = []
    1.41 @@ -1759,19 +1755,17 @@
    1.42               |> close_formula_universally type_enc, isabelle_info introN, NONE)
    1.43    end
    1.44  
    1.45 -fun fo_literal_from_arity_literal type_enc (AryLitConst (class, t, args)) =
    1.46 -    (true, type_class_aterm type_enc class
    1.47 -                            (ATerm (t, map (fn arg => ATerm (arg, [])) args)))
    1.48 -  | fo_literal_from_arity_literal type_enc (AryLitVar (class, var)) =
    1.49 -    (false, type_class_aterm type_enc class (ATerm (var, [])))
    1.50 +fun fo_literal_from_arity_literal type_enc (class, t, args) =
    1.51 +  (true, type_class_aterm type_enc class
    1.52 +                          (ATerm (t, map (fn arg => ATerm (arg, [])) args)))
    1.53  
    1.54  fun formula_line_for_arity_clause type_enc
    1.55 -        ({name, prem_lits, concl_lits, ...} : arity_clause) =
    1.56 +        ({name, prem_lits, concl_lit, ...} : arity_clause) =
    1.57    Formula (arity_clause_prefix ^ name, Axiom,
    1.58 -           mk_ahorn (map (formula_from_fo_literal o apfst not
    1.59 +           mk_ahorn (map (formula_from_fo_literal
    1.60                            o fo_literal_from_arity_literal type_enc) prem_lits)
    1.61                      (formula_from_fo_literal
    1.62 -                         (fo_literal_from_arity_literal type_enc concl_lits))
    1.63 +                         (fo_literal_from_arity_literal type_enc concl_lit))
    1.64             |> close_formula_universally type_enc, isabelle_info introN, NONE)
    1.65  
    1.66  fun formula_line_for_conjecture ctxt format mono type_enc