src/HOL/Tools/ATP/atp_proof_reconstruct.ML
changeset 57635 97adb86619a4
parent 57547 677b07d777c3
child 57697 44341963ade3
     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) =