more robust handling of types for skolems (modeled as Frees)
authorblanchet
Thu Jul 24 00:24:00 2014 +0200 (2014-07-24)
changeset 5763597adb86619a4
parent 57634 efc00b9b8680
child 57636 3ab503b04bdb
more robust handling of types for skolems (modeled as Frees)
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/ATP/atp_waldmeister.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jul 24 00:24:00 2014 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jul 24 00:24:00 2014 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4      ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
     1.5      int Symtab.table -> string atp_proof -> (term, string) atp_step list
     1.6    val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list
     1.7 -  val infer_formula_types : Proof.context -> term -> term
     1.8 +  val infer_formula_types : Proof.context -> term list -> term list
     1.9    val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list
    1.10    val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list ->
    1.11      (term, string) atp_step list
    1.12 @@ -530,9 +530,12 @@
    1.13      else
    1.14        s
    1.15  
    1.16 +fun set_var_index j = map_aterms (fn Var ((s, _), T) => Var ((s, j), T) | t => t)
    1.17 +
    1.18  fun infer_formula_types ctxt =
    1.19 -  Type.constraint HOLogic.boolT
    1.20 -  #> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
    1.21 +  map_index (uncurry (fn j => set_var_index j #> Type.constraint HOLogic.boolT))
    1.22 +  #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
    1.23 +  #> map (set_var_index 0)
    1.24  
    1.25  val combinator_table =
    1.26    [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
    1.27 @@ -571,8 +574,6 @@
    1.28          |> prop_of_atp ctxt format type_enc true sym_tab
    1.29          |> uncombine_term thy
    1.30          |> unlift_term lifted
    1.31 -        |> infer_formula_types ctxt
    1.32 -        |> HOLogic.mk_Trueprop
    1.33      in
    1.34        SOME (name, role, t, rule, deps)
    1.35      end
    1.36 @@ -591,10 +592,14 @@
    1.37      repair_body proof
    1.38    end
    1.39  
    1.40 +fun map_proof_terms f (lines : ('a * 'b * 'c * 'd * 'e) list) =
    1.41 +  map2 (fn c => fn (a, b, _, d, e) => (a, b, c, d, e)) (f (map #3 lines)) lines
    1.42 +
    1.43  fun termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab =
    1.44    nasty_atp_proof pool
    1.45    #> map_term_names_in_atp_proof repair_name
    1.46    #> map_filter (termify_line ctxt format type_enc lifted sym_tab)
    1.47 +  #> map_proof_terms (infer_formula_types ctxt #> map HOLogic.mk_Trueprop)
    1.48    #> local_prover = waldmeisterN ? repair_waldmeister_endgame
    1.49  
    1.50  fun take_distinct_vars seen ((t as Var _) :: ts) =
     2.1 --- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Thu Jul 24 00:24:00 2014 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Thu Jul 24 00:24:00 2014 +0200
     2.3 @@ -181,7 +181,7 @@
     2.4      val thy = Proof_Context.theory_of ctxt
     2.5      val t = u
     2.6        |> atp_to_trm
     2.7 -      |> infer_formula_types ctxt
     2.8 +      |> singleton (infer_formula_types ctxt)
     2.9        |> HOLogic.mk_Trueprop
    2.10    in
    2.11      (name, role, t, rule, deps)