TFF: declare free types as types
authorblanchet
Tue Mar 27 16:59:13 2012 +0300 (2012-03-27)
changeset 47145ffc6d6267a88
parent 47144 9bfc32fc7ced
child 47146 7276f2b12ff7
TFF: declare free types as types
src/HOL/Tools/ATP/atp_problem_generate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 15:34:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -2035,14 +2035,21 @@
     1.4             |> close_formula_universally
     1.5             |> bound_tvars type_enc true atomic_types, NONE, [])
     1.6  
     1.7 +fun type_enc_needs_free_types (Simple_Types (_, Polymorphic, _)) = true
     1.8 +  | type_enc_needs_free_types (Simple_Types _) = false
     1.9 +  | type_enc_needs_free_types _ = true
    1.10 +
    1.11  fun formula_line_for_free_type j phi =
    1.12    Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
    1.13  fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
    1.14 -  let
    1.15 -    val phis =
    1.16 -      fold (union (op =)) (map #atomic_types facts) []
    1.17 -      |> formulas_for_types type_enc add_sorts_on_tfree
    1.18 -  in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
    1.19 +  if type_enc_needs_free_types type_enc then
    1.20 +    let
    1.21 +      val phis =
    1.22 +        fold (union (op =)) (map #atomic_types facts) []
    1.23 +        |> formulas_for_types type_enc add_sorts_on_tfree
    1.24 +    in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
    1.25 +  else
    1.26 +    []
    1.27  
    1.28  (** Symbol declarations **)
    1.29  
    1.30 @@ -2497,8 +2504,11 @@
    1.31      val ind =
    1.32        case type_enc of
    1.33          Simple_Types _ =>
    1.34 -        if String.isPrefix type_const_prefix s then atype_of_types
    1.35 -        else individual_atype
    1.36 +        if String.isPrefix type_const_prefix s orelse
    1.37 +           String.isPrefix tfree_prefix s then
    1.38 +          atype_of_types
    1.39 +        else
    1.40 +          individual_atype
    1.41        | _ => individual_atype
    1.42      fun typ 0 = if pred_sym then bool_atype else ind
    1.43        | typ ary = AFun (ind, typ (ary - 1))