# HG changeset patch # User blanchet # Date 1406918669 -7200 # Node ID f1108245ba117551d1d4702770168fc8d8270037 # Parent cac309e2b1f7a82920b7e65c9a793773c0330855 better handling of variable names diff -r cac309e2b1f7 -r f1108245ba11 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Aug 01 20:15:41 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Aug 01 20:44:29 2014 +0200 @@ -30,6 +30,7 @@ val forall_of : term -> term -> term val exists_of : term -> term -> term + val rename_bound_vars : term -> term val type_enc_aliases : (string * string list) list val unalias_type_enc : string -> string list val term_of_atp : Proof.context -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc -> @@ -101,6 +102,24 @@ TFree (ww, the_default @{sort type} (Variable.def_sort ctxt (ww, ~1))) end +fun single_letter upper s = + let val s' = if String.isPrefix "o" s orelse String.isPrefix "O" s then "z" else s in + String.extract (Name.desymbolize (SOME upper) (Long_Name.base_name s'), 0, SOME 1) + end + +fun var_name_of_typ (Type (@{type_name fun}, [_, T])) = + if body_type T = HOLogic.boolT then "p" else "f" + | var_name_of_typ (Type (@{type_name set}, [T])) = single_letter true (var_name_of_typ T) + | var_name_of_typ (Type (s, Ts)) = + if String.isSuffix "list" s then var_name_of_typ (the_single Ts) ^ "s" + else single_letter false (Long_Name.base_name s) + | var_name_of_typ (TFree (s, _)) = single_letter false (perhaps (try (unprefix "'")) s) + | var_name_of_typ (TVar ((s, _), T)) = var_name_of_typ (TFree (s, T)) + +fun rename_bound_vars (t $ u) = rename_bound_vars t $ rename_bound_vars u + | rename_bound_vars (Abs (_, T, t)) = Abs (var_name_of_typ T, T, rename_bound_vars t) + | rename_bound_vars t = t + exception ATP_CLASS of string list exception ATP_TYPE of string atp_type list exception ATP_TERM of (string, string atp_type) atp_term list diff -r cac309e2b1f7 -r f1108245ba11 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 20:15:41 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 20:44:29 2014 +0200 @@ -210,18 +210,20 @@ val rule_of_clause_id = fst o the o Symtab.lookup steps o fst - fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form + val close_form_etc = rename_bound_vars o close_form + + fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form_etc | prop_of_clause names = let - val lits = map (HOLogic.dest_Trueprop o snd) - (map_filter (Symtab.lookup steps o fst) names) + val lits = + map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) in (case List.partition (can HOLogic.dest_not) lits of (negs as _ :: _, pos as _ :: _) => s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) | _ => fold (curry s_disj) lits @{term False}) end - |> HOLogic.mk_Trueprop |> close_form + |> HOLogic.mk_Trueprop |> close_form_etc fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show @@ -350,8 +352,7 @@ ||> (comment_isar_proof comment_of #> chain_isar_proof #> kill_useless_labels_in_isar_proof - #> relabel_isar_proof_nicely - #> rename_bound_vars_in_isar_proof) + #> relabel_isar_proof_nicely) in (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of 1 => diff -r cac309e2b1f7 -r f1108245ba11 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Aug 01 20:15:41 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Aug 01 20:44:29 2014 +0200 @@ -46,7 +46,6 @@ val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof val relabel_isar_proof_canonically : isar_proof -> isar_proof val relabel_isar_proof_nicely : isar_proof -> isar_proof - val rename_bound_vars_in_isar_proof : isar_proof -> isar_proof val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string end; @@ -207,34 +206,6 @@ relabel_proof [] 0 end -val Type (listT_name, _) = HOLogic.listT dummyT - -fun var_name_of_typ (Type (@{type_name fun}, [_, T])) = - if body_type T = HOLogic.boolT then "p" else "f" - | var_name_of_typ (Type (@{type_name set}, [T])) = - Name.desymbolize (SOME true) (var_name_of_typ T) - | var_name_of_typ (Type (s, _)) = - if s = listT_name then "xs" - else String.extract (Name.desymbolize (SOME false) (Long_Name.base_name s), 0, SOME 1) - | var_name_of_typ (TFree (s, _)) = - String.extract (Name.desymbolize (SOME false) (perhaps (try (unprefix "'")) s), 0, SOME 1) - | var_name_of_typ (TVar ((s, _), T)) = var_name_of_typ (TFree (s, T)) - -fun rename_bound_vars (t $ u) = rename_bound_vars t $ rename_bound_vars u - | rename_bound_vars (Abs (_, T, t)) = Abs (var_name_of_typ T, T, rename_bound_vars t) - | rename_bound_vars t = t - -val rename_bound_vars_in_isar_proof = - let - fun rename_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) = - Prove (qs, xs, l, rename_bound_vars t, map rename_proof subs, facts, meths, comment) - | rename_step step = step - and rename_proof (Proof (fix, assms, steps)) = - Proof (fix, map (apsnd rename_bound_vars) assms, map rename_step steps) - in - rename_proof - end - val indent_size = 2 fun string_of_isar_proof ctxt0 i n proof =