src/HOL/Tools/ATP/atp_proof_reconstruct.ML
changeset 57256 cf43583f9bb9
parent 57255 488046fdda59
child 57257 0d5e34ba4d28
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jun 16 16:18:15 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jun 16 16:18:34 2014 +0200
@@ -130,6 +130,8 @@
           Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
             (if null clss then @{sort type} else map class_of_atp_class clss))))
   end
+  | typ_of_atp_type ctxt (ty as AFun (a, tys)) =
+    (typ_of_atp_type ctxt a) --> (typ_of_atp_type ctxt tys)
 
 fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
 
@@ -188,46 +190,24 @@
 
 
 (* Higher-order translation. Variables are typed (although we don't use that information). Lambdas
-   are typed. *)
+   are typed.
+
+  The code is similar to term_of_atp_fo. *)
 fun term_of_atp_ho ctxt textual sym_tab =
   let
     val thy = Proof_Context.theory_of ctxt
-    fun norm_var_types var T' t =
-      let
-        fun norm_term (ATerm ((x, ty), l)) =
-            ATerm((x, if x = var then [T'] else ty), List.map norm_term l)
-          | norm_term (AAbs(((x, ty), term), l)) = AAbs(((x, ty), term), List.map norm_term l)
-      in
-        norm_term t
-      end
-    fun mk_op_of_tptp_operator s =
-      if s = tptp_or then HOLogic.mk_disj
-      else if s = tptp_and then HOLogic.mk_conj
-      else if s = tptp_implies then HOLogic.mk_imp
-      else if s = tptp_iff orelse s = tptp_equal then HOLogic.mk_eq
-      else if s = tptp_not_iff orelse s = tptp_not_equal then HOLogic.mk_eq #> HOLogic.mk_not
-      else if s = tptp_if then HOLogic.mk_imp #> HOLogic.mk_not
-      else if s = tptp_not_and then HOLogic.mk_conj #> HOLogic.mk_not
-      else if s = tptp_not_or then HOLogic.mk_disj #> HOLogic.mk_not
-      else raise Fail ("unknown operator: " ^ s)
-    fun mk_quant_of_tptp_quant s =
-      if s = tptp_ho_exists then HOLogic.mk_exists
-      else if s = tptp_ho_forall then HOLogic.mk_all
-      else raise Fail ("unknown quantifier: " ^ s)
     val var_index = if textual then 0 else 1
 
     fun do_term opt_T u =
       (case u of
         AAbs(((var, ty), term), []) =>
         let val typ = typ_of_atp_type ctxt ty in
-          absfree (repair_var_name textual var, typ) (do_term NONE (norm_var_types var ty term))
+          absfree (repair_var_name textual var, typ) (do_term NONE term)
         end
       | ATerm ((s, tys), us) =>
         if s = ""
         then error "Isar proof reconstruction failed because the ATP proof \
                      \contains unparsable material."
-        else if String.isPrefix native_type_prefix s then
-          @{const True} (* ignore TPTP type information *)
         else if s = tptp_equal then
           let val ts = map (do_term NONE) us in
             if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
@@ -235,90 +215,65 @@
             else
               list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
           end
-        else if s = tptp_app then
-          let val ts = map (do_term NONE) us in
-            hd ts $ List.last ts
-          end
-        else if s = tptp_not then
-          let val ts = map (do_term NONE) us in
-            List.last ts |> HOLogic.mk_not
-          end
-        else if s = tptp_ho_forall orelse s = tptp_ho_exists then
-          (case us of
-            [AAbs (((var, ty), term), [])] =>
-            let val typ = typ_of_atp_type ctxt ty in
-              (repair_var_name textual var, typ , do_term NONE (norm_var_types var ty term))
-                |> mk_quant_of_tptp_quant s
-            end
-          | [] => if s = tptp_ho_exists then HOLogic.exists_const dummyT
-                  else HOLogic.all_const dummyT)
-        else if List.exists (curry (op=) s) tptp_binary_op_list then
-          let val ts = map (do_term NONE) us in
-            (mk_op_of_tptp_operator s) (hd ts, List.last ts)
-          end
+        else if not (null us) then
+          let
+            val args = List.map (do_term NONE) us
+            val opt_T' = SOME (map slack_fastype_of args ---> the_default dummyT opt_T)
+            val func = do_term opt_T' (ATerm ((s, tys), []))
+          in foldl1 (op $) (func :: args) end
+        else if s = tptp_or then HOLogic.disj
+        else if s = tptp_and then HOLogic.conj
+        else if s = tptp_implies then HOLogic.imp
+        else if s = tptp_iff orelse s = tptp_equal then HOLogic.eq_const dummyT
+        else if s = tptp_not_iff orelse s = tptp_not_equal then @{term "% P Q. Q ~= P"}
+        else if s = tptp_if then @{term "% P Q. Q --> P"}
+        else if s = tptp_not_and then @{term "% P Q. ~ (P & Q)"}
+        else if s = tptp_not_or then @{term "% P Q. ~ (P | Q)"}
+        else if s = tptp_not then HOLogic.Not
+        else if s = tptp_ho_forall then HOLogic.all_const dummyT
+        else if s = tptp_ho_exists then HOLogic.exists_const dummyT
         else
-          if us <> [] then
+          (case unprefix_and_unascii const_prefix s of
+            SOME s' =>
             let
-              val applicant_list = List.map (do_term NONE) us
-              val opt_typ = SOME (fold_rev
-                                    (fn t1 => fn t2 => slack_fastype_of t1 --> t2)
-                                    applicant_list (the_default dummyT opt_T))
-              val func_name = do_term opt_typ (ATerm ((s, tys), []))
-            in
-              foldl1 (op$) (func_name :: applicant_list) end
-          else (*FIXME: clean (remove stuff related to vampire and other provers)*)
-            (case unprefix_and_unascii const_prefix s of
-              SOME s' =>
-              let
-                val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const
-                val new_skolem = String.isPrefix new_skolem_const_prefix s''
-                val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s)
-                val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
-                val term_ts = map (do_term NONE) term_us
-                val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us
-                val T =
-                    (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then
-                       if new_skolem then
-                         SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
-                       else if textual then
-                         try (Sign.const_instance thy) (s', Ts)
-                       else
-                         NONE
-                     else
-                       NONE)
-                       |> (fn SOME T => T
-                            | NONE =>
-                              map slack_fastype_of term_ts --->
-                                the_default (Type_Infer.anyT @{sort type}) opt_T)
-                val t =
-                    if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
-                    else Const (unproxify_const s', T)
-              in list_comb (t, term_ts) end
-            | NONE => (* a free or schematic variable *)
-              let
-                (* This assumes that distinct names are mapped to distinct names by
-                   "Variable.variant_frees". This does not hold in general but should hold for
-                   ATP-generated Skolem function names, since these end with a digit and
-                   "variant_frees" appends letters. *)
-                fun fresh_up s =
-                  [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
-                val ts = map (do_term NONE) us
-                val T =
-                  (case opt_T of
-                    SOME T => map slack_fastype_of ts ---> T
-                  | NONE =>
-                    map slack_fastype_of ts --->
-                      (case tys of [ty] => typ_of_atp_type ctxt ty | _ => Type_Infer.anyT
-                        @{sort type}))
-                val t =
-                  (case unprefix_and_unascii fixed_var_prefix s of
-                    SOME s => Free (s, T)
-                  | NONE =>
-                    if textual andalso not (is_tptp_variable s) then
-                      Free (s |> textual ? (repair_var_name_raw #> fresh_up), T)
-                    else
-                      Var ((repair_var_name textual s, var_index), T))
-              in list_comb (t, ts) end))
+              val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const
+              val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s)
+              val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
+              val term_ts = map (do_term NONE) term_us
+              val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us
+              val T =
+                (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then
+                   if textual then try (Sign.const_instance thy) (s', Ts) else NONE
+                 else
+                   NONE)
+                |> (fn SOME T => T
+                     | NONE =>
+                       map slack_fastype_of term_ts --->
+                       the_default (Type_Infer.anyT @{sort type}) opt_T)
+              val t = Const (unproxify_const s', T)
+            in list_comb (t, term_ts) end
+          | NONE => (* a free or schematic variable *)
+            let
+              fun fresh_up s =
+                [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
+              val ts = map (do_term NONE) us
+              val T =
+                (case opt_T of
+                  SOME T => map slack_fastype_of ts ---> T
+                | NONE =>
+                  map slack_fastype_of ts --->
+                    (case tys of
+                      [ty] => typ_of_atp_type ctxt ty
+                    | _ => Type_Infer.anyT @{sort type}))
+              val t =
+                (case unprefix_and_unascii fixed_var_prefix s of
+                  SOME s => Free (s, T)
+                | NONE =>
+                  if textual andalso not (is_tptp_variable s) then
+                    Free (s |> textual ? (repair_var_name_raw #> fresh_up), T)
+                  else
+                    Var ((repair_var_name textual s, var_index), T))
+            in list_comb (t, ts) end))
   in do_term end
 
 (* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}"
@@ -459,7 +414,7 @@
     val vars = filter (fn ((s, _), _) => s = var_s) (Term.add_vars t [])
     val normTs = vars |> AList.group (op =) |> map (apsnd hd)
     fun norm_var_types (Var (x, T)) =
-        Var (x, (case AList.lookup (op =) normTs x of NONE => T | SOME T' => T'))
+        Var (x, the_default T (AList.lookup (op =) normTs x))
       | norm_var_types t = t
   in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
 
@@ -623,7 +578,7 @@
                    t
                | t => t)
 
-fun termify_line _ _ _ _ _ (_, Type_Role, _, _, _) =  NONE
+fun termify_line _ _ _ _ _ (_, Type_Role, _, _, _) = NONE
   | termify_line ctxt format type_enc lifted sym_tab (name, role, u, rule, deps) =
     let
       val thy = Proof_Context.theory_of ctxt
@@ -656,7 +611,7 @@
   #> nasty_atp_proof pool
   #> map_term_names_in_atp_proof repair_name
   #> map_filter (termify_line ctxt format type_enc lifted sym_tab)
-  #> prover = waldmeisterN ? repair_waldmeister_endgame
+  #> perhaps (try (unprefix remote_prefix)) prover = waldmeisterN ? repair_waldmeister_endgame
 
 fun take_distinct_vars seen ((t as Var _) :: ts) =
     if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts