order LEO-II/Satallax definitions so that they build on each other (cf. Satallax's THF policy)
authorblanchet
Wed May 23 21:19:48 2012 +0200 (2012-05-23)
changeset 47975adc977fec17e
parent 47974 08d2dcc2dab9
child 47976 6b13451135a9
order LEO-II/Satallax definitions so that they build on each other (cf. Satallax's THF policy)
src/HOL/Tools/ATP/atp_problem_generate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 23 21:19:48 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 23 21:19:48 2012 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    type connective = ATP_Problem.connective
     1.5    type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
     1.6    type atp_format = ATP_Problem.atp_format
     1.7 -  type formula_kind = ATP_Problem.formula_kind
     1.8 +  type formula_role = ATP_Problem.formula_role
     1.9    type 'a problem = 'a ATP_Problem.problem
    1.10  
    1.11    datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter
    1.12 @@ -102,7 +102,7 @@
    1.13      Proof.context -> type_enc -> string -> term list -> term list * term list
    1.14    val factsN : string
    1.15    val prepare_atp_problem :
    1.16 -    Proof.context -> atp_format -> formula_kind -> type_enc -> mode -> string
    1.17 +    Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string
    1.18      -> bool -> bool -> bool -> term list -> term
    1.19      -> ((string * stature) * term) list
    1.20      -> string problem * string Symtab.table * (string * stature) list vector
    1.21 @@ -267,7 +267,7 @@
    1.22     thread. Also, the errors are impossible. *)
    1.23  val unascii_of =
    1.24    let
    1.25 -    fun un rcs [] = String.implode(rev rcs)
    1.26 +    fun un rcs [] = String.implode (rev rcs)
    1.27        | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
    1.28          (* Three types of _ escapes: __, _A to _P, _nnn *)
    1.29        | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
    1.30 @@ -822,13 +822,13 @@
    1.31  type translated_formula =
    1.32    {name : string,
    1.33     stature : stature,
    1.34 -   kind : formula_kind,
    1.35 +   role : formula_role,
    1.36     iformula : (name, typ, iterm) formula,
    1.37     atomic_types : typ list}
    1.38  
    1.39 -fun update_iformula f ({name, stature, kind, iformula, atomic_types}
    1.40 +fun update_iformula f ({name, stature, role, iformula, atomic_types}
    1.41                         : translated_formula) =
    1.42 -  {name = name, stature = stature, kind = kind, iformula = f iformula,
    1.43 +  {name = name, stature = stature, role = role, iformula = f iformula,
    1.44     atomic_types = atomic_types} : translated_formula
    1.45  
    1.46  fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
    1.47 @@ -1230,7 +1230,7 @@
    1.48    let
    1.49      val (facts, lambda_ts) =
    1.50        facts |> map (snd o snd) |> trans_lams
    1.51 -            |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
    1.52 +            |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
    1.53      val lam_facts =
    1.54        map2 (fn t => fn j =>
    1.55                 ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t)))
    1.56 @@ -1285,15 +1285,15 @@
    1.57    | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
    1.58    | should_use_iff_for_eq _ _ = true
    1.59  
    1.60 -fun make_formula ctxt format type_enc iff_for_eq name stature kind t =
    1.61 +fun make_formula ctxt format type_enc iff_for_eq name stature role t =
    1.62    let
    1.63      val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc
    1.64      val (iformula, atomic_Ts) =
    1.65 -      iformula_from_prop ctxt type_enc iff_for_eq (SOME (kind <> Conjecture)) t
    1.66 +      iformula_from_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t
    1.67                           []
    1.68        |>> close_iformula_universally
    1.69    in
    1.70 -    {name = name, stature = stature, kind = kind, iformula = iformula,
    1.71 +    {name = name, stature = stature, role = role, iformula = iformula,
    1.72       atomic_types = atomic_Ts}
    1.73    end
    1.74  
    1.75 @@ -1326,9 +1326,9 @@
    1.76  *)
    1.77  
    1.78  fun make_conjecture ctxt format type_enc =
    1.79 -  map (fn ((name, stature), (kind, t)) =>
    1.80 -          t |> kind = Conjecture ? s_not
    1.81 -            |> make_formula ctxt format type_enc true name stature kind)
    1.82 +  map (fn ((name, stature), (role, t)) =>
    1.83 +          t |> role = Conjecture ? s_not
    1.84 +            |> make_formula ctxt format type_enc true name stature role)
    1.85  
    1.86  (** Finite and infinite type inference **)
    1.87  
    1.88 @@ -1893,7 +1893,31 @@
    1.89    else
    1.90      error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
    1.91  
    1.92 -fun translate_formulas ctxt prem_kind format type_enc lam_trans presimp hyp_ts
    1.93 +fun order_definitions facts =
    1.94 +  let
    1.95 +    fun add_consts (IApp (t, u)) = fold add_consts [t, u]
    1.96 +      | add_consts (IAbs (_, t)) = add_consts t
    1.97 +      | add_consts (IConst (name, _, _)) = insert (op =) name
    1.98 +      | add_consts (IVar _) = I
    1.99 +    fun consts_of_hs l_or_r (_, {iformula, ...} : translated_formula) =
   1.100 +      case iformula of
   1.101 +        AAtom (IApp (IApp (IConst _, t), u)) => add_consts (l_or_r (t, u)) []
   1.102 +      | _ => []
   1.103 +    (* Quadratic, but usually OK. *)
   1.104 +    fun order [] [] = []
   1.105 +      | order (fact :: skipped) [] = fact :: order [] skipped (* break cycle *)
   1.106 +      | order skipped (fact :: facts) =
   1.107 +        let val rhs_consts = consts_of_hs snd fact in
   1.108 +          if exists (exists (member (op =) rhs_consts o the_single
   1.109 +                     o consts_of_hs fst))
   1.110 +                    [skipped, facts] then
   1.111 +            order (fact :: skipped) facts
   1.112 +          else
   1.113 +            fact :: order [] (facts @ skipped)
   1.114 +        end
   1.115 +  in order [] facts end
   1.116 +
   1.117 +fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
   1.118                         concl_t facts =
   1.119    let
   1.120      val thy = Proof_Context.theory_of ctxt
   1.121 @@ -1906,7 +1930,7 @@
   1.122        |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
   1.123      val facts = facts |> map (apsnd (pair Axiom))
   1.124      val conjs =
   1.125 -      map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
   1.126 +      map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
   1.127        |> map (apsnd freeze_term)
   1.128        |> map2 (pair o rpair (Local, General) o string_of_int)
   1.129                (0 upto length hyp_ts)
   1.130 @@ -1925,7 +1949,9 @@
   1.131        |> map_filter (fn (name, (_, t)) =>
   1.132                          make_fact ctxt format type_enc true (name, t)
   1.133                          |> Option.map (pair name))
   1.134 -      |> ListPair.unzip
   1.135 +      |> List.partition (fn (_, {role, ...}) => role = Definition)
   1.136 +      |>> order_definitions
   1.137 +      |> op @ |> ListPair.unzip
   1.138      val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
   1.139      val lam_facts =
   1.140        lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
   1.141 @@ -2086,8 +2112,8 @@
   1.142     of monomorphization). The TPTP explicitly forbids name clashes, and some of
   1.143     the remote provers might care. *)
   1.144  fun formula_line_for_fact ctxt polym_constrs prefix encode freshen pos
   1.145 -        mono type_enc rank (j, {name, stature, kind, iformula, atomic_types}) =
   1.146 -  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
   1.147 +        mono type_enc rank (j, {name, stature, role, iformula, atomic_types}) =
   1.148 +  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role,
   1.149     iformula
   1.150     |> formula_from_iformula ctxt polym_constrs mono type_enc
   1.151            should_guard_var_in_formula (if pos then SOME true else NONE)
   1.152 @@ -2131,8 +2157,8 @@
   1.153             NONE, isabelle_info inductiveN helper_rank)
   1.154  
   1.155  fun formula_line_for_conjecture ctxt polym_constrs mono type_enc
   1.156 -        ({name, kind, iformula, atomic_types, ...} : translated_formula) =
   1.157 -  Formula (conjecture_prefix ^ name, kind,
   1.158 +        ({name, role, iformula, atomic_types, ...} : translated_formula) =
   1.159 +  Formula (conjecture_prefix ^ name, role,
   1.160             iformula
   1.161             |> formula_from_iformula ctxt polym_constrs mono type_enc
   1.162                    should_guard_var_in_formula (SOME false)
   1.163 @@ -2304,8 +2330,8 @@
   1.164      end
   1.165    | add_iterm_mononotonicity_info _ _ _ _ mono = mono
   1.166  fun add_fact_mononotonicity_info ctxt level
   1.167 -        ({kind, iformula, ...} : translated_formula) =
   1.168 -  formula_fold (SOME (kind <> Conjecture))
   1.169 +        ({role, iformula, ...} : translated_formula) =
   1.170 +  formula_fold (SOME (role <> Conjecture))
   1.171                 (add_iterm_mononotonicity_info ctxt level) iformula
   1.172  fun mononotonicity_info_for_facts ctxt type_enc facts =
   1.173    let val level = level_of_type_enc type_enc in
   1.174 @@ -2385,14 +2411,14 @@
   1.175                 ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
   1.176    end
   1.177  
   1.178 -fun honor_conj_sym_kind in_conj =
   1.179 +fun honor_conj_sym_role in_conj =
   1.180    if in_conj then (Hypothesis, I) else (Axiom, I)
   1.181  
   1.182  fun formula_line_for_guards_sym_decl ctxt mono type_enc n s j
   1.183                                       (s', T_args, T, _, ary, in_conj) =
   1.184    let
   1.185      val thy = Proof_Context.theory_of ctxt
   1.186 -    val (kind, maybe_negate) = honor_conj_sym_kind in_conj
   1.187 +    val (role, maybe_negate) = honor_conj_sym_role in_conj
   1.188      val (arg_Ts, res_T) = chop_fun ary T
   1.189      val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
   1.190      val bounds =
   1.191 @@ -2413,7 +2439,7 @@
   1.192          replicate ary NONE
   1.193    in
   1.194      Formula (guards_sym_formula_prefix ^ s ^
   1.195 -             (if n > 1 then "_" ^ string_of_int j else ""), kind,
   1.196 +             (if n > 1 then "_" ^ string_of_int j else ""), role,
   1.197               IConst ((s, s'), T, T_args)
   1.198               |> fold (curry (IApp o swap)) bounds
   1.199               |> type_guard_iterm type_enc res_T
   1.200 @@ -2435,7 +2461,7 @@
   1.201      val ident_base =
   1.202        tags_sym_formula_prefix ^ s ^
   1.203        (if n > 1 then "_" ^ string_of_int j else "")
   1.204 -    val (kind, maybe_negate) = honor_conj_sym_kind in_conj
   1.205 +    val (role, maybe_negate) = honor_conj_sym_role in_conj
   1.206      val (arg_Ts, res_T) = chop_fun ary T
   1.207      val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
   1.208      val bounds = bound_names |> map (fn name => ATerm (name, []))
   1.209 @@ -2455,7 +2481,7 @@
   1.210              else
   1.211                bounds
   1.212          in
   1.213 -          cons (Formula (ident_base ^ "_res", kind,
   1.214 +          cons (Formula (ident_base ^ "_res", role,
   1.215                           eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
   1.216                           NONE, isabelle_info defN helper_rank))
   1.217          end
   1.218 @@ -2517,7 +2543,7 @@
   1.219      fun do_alias ary =
   1.220        let
   1.221          val thy = Proof_Context.theory_of ctxt
   1.222 -        val (kind, maybe_negate) = honor_conj_sym_kind in_conj
   1.223 +        val (role, maybe_negate) = honor_conj_sym_role in_conj
   1.224          val base_name = base_s0 |> `(make_fixed_const (SOME type_enc))
   1.225          val T = case types of [T] => T | _ => robust_const_type thy base_s0
   1.226          val T_args = robust_const_typargs thy (base_s0, T)
   1.227 @@ -2550,7 +2576,7 @@
   1.228                       (ho_term_of tm1) (ho_term_of tm2)
   1.229        in
   1.230          ([tm1, tm2],
   1.231 -         [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,
   1.232 +         [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate,
   1.233                     NONE, isabelle_info defN helper_rank)])
   1.234          |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
   1.235              else pair_append (do_alias (ary - 1)))
   1.236 @@ -2670,7 +2696,7 @@
   1.237  
   1.238  val app_op_and_predicator_threshold = 50
   1.239  
   1.240 -fun prepare_atp_problem ctxt format prem_kind type_enc mode lam_trans
   1.241 +fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans
   1.242                          uncurried_aliases readable_names preproc hyp_ts concl_t
   1.243                          facts =
   1.244    let
   1.245 @@ -2700,7 +2726,7 @@
   1.246          lam_trans
   1.247      val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
   1.248           lifted) =
   1.249 -      translate_formulas ctxt prem_kind format type_enc lam_trans preproc hyp_ts
   1.250 +      translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts
   1.251                           concl_t facts
   1.252      val (_, sym_tab0) =
   1.253        sym_table_for_facts ctxt type_enc app_op_level conjs facts