# HG changeset patch # User wenzelm # Date 1422541649 -3600 # Node ID fb393ecde29d4ce3adcdca053ca3b2a915555937 # Parent fe665176064329aa4028b27744e8c4040cbf01b6 tuned; diff -r fe6651760643 -r fb393ecde29d src/HOL/Tools/ATP/atp_waldmeister.ML --- a/src/HOL/Tools/ATP/atp_waldmeister.ML Thu Jan 29 15:21:16 2015 +0100 +++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Thu Jan 29 15:27:29 2015 +0100 @@ -29,16 +29,16 @@ type 'a atp_proof = 'a ATP_Proof.atp_proof type stature = ATP_Problem_Generate.stature type waldmeister_info = (string * (term list * (term option * term))) list - + val waldmeister_skolemize_rule : string - + val generate_waldmeister_problem : Proof.context -> term list -> term -> ((string * stature) * term) list -> - string atp_problem * string Symtab.table * (string * term) list * int Symtab.table * + string atp_problem * string Symtab.table * (string * term) list * int Symtab.table * waldmeister_info val termify_waldmeister_proof : Proof.context -> string Symtab.table -> string atp_proof -> (term, string) atp_step list - val introduce_waldmeister_skolems : waldmeister_info -> (term, string) atp_step list -> + val introduce_waldmeister_skolems : waldmeister_info -> (term, string) atp_step list -> (term, string) atp_step list end; @@ -64,7 +64,7 @@ fun skolem_free ctxt1 ctxt2 vars (bound_name, ty, trm) = let - val (fun_trm, ctxt1_new, ctxt2_new) = + val (fun_trm, ctxt1_new, ctxt2_new) = mk_fun_for_bvar ctxt1 ctxt2 (List.rev vars) (bound_name,ty) in (Term.subst_bounds ([fun_trm], trm), ctxt1_new, ctxt2_new) @@ -81,7 +81,7 @@ fun skolem_bound is_free ctxt1 ctxt2 spets vars x = if is_free then - let + let val (trm', ctxt1', ctxt2') = skolem_free ctxt1 ctxt2 vars x in (ctxt1', ctxt2',spets, trm', vars) @@ -107,9 +107,9 @@ | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (name, _) $ Abs x)) = if name = @{const_name Ex} orelse name = @{const_name All} then let - val is_free = (name = @{const_name Ex} andalso pos) + val is_free = (name = @{const_name Ex} andalso pos) orelse (name = @{const_name All} andalso not pos) - val (ctxt1', ctxt2', spets', trm', vars') = + val (ctxt1', ctxt2', spets', trm', vars') = skolem_bound is_free ctxt1 ctxt2 (if is_free then trm :: spets else spets) vars x in skolemize' pos ctxt1' ctxt2' spets' vars' trm' @@ -117,7 +117,7 @@ else (ctxt1, ctxt2, spets, trm) | skolemize' pos ctxt1 ctxt2 spets vars ((c as Const (name, _)) $ a $ b) = - if name = @{const_name conj} orelse name = @{const_name disj} orelse + if name = @{const_name conj} orelse name = @{const_name disj} orelse name = @{const_name implies} then let val pos_a = if name = @{const_name implies} then not pos else pos @@ -131,11 +131,11 @@ else (ctxt1,ctxt2,spets,c $ a $ b) | skolemize' _ ctxt1 ctxt2 spets _ trm = (ctxt1, ctxt2, spets, trm) - + fun vars_of trm = rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t | _ => I) trm [])); - fun skolemize positve ctxt trm = + fun skolemize positve ctxt trm = let val (ctxt1, _, spets, skolemized_trm) = skolemize' positve ctxt ctxt [] (vars_of trm) trm in @@ -156,36 +156,36 @@ val identifier_character = not o member (op =) [delimiter, open_paranthesis, close_parathesis] -fun encode_type (Type (name, types)) = - type_prefix ^ open_paranthesis ^ name ^ delimiter ^ - (map encode_type types |> String.concatWith delimiter) ^ close_parathesis -| encode_type (TFree (name, sorts)) = - tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ (String.concatWith delimiter sorts) ^ +fun encode_type (Type (name, types)) = + type_prefix ^ open_paranthesis ^ name ^ delimiter ^ + (map encode_type types |> space_implode delimiter) ^ close_parathesis +| encode_type (TFree (name, sorts)) = + tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ space_implode delimiter sorts ^ close_parathesis | encode_type (TVar ((name, i), sorts)) = - tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^ - close_parathesis ^ delimiter ^ (String.concatWith delimiter sorts) ^ close_parathesis + tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^ + close_parathesis ^ delimiter ^ space_implode delimiter sorts ^ close_parathesis -fun encode_types types = (String.concatWith delimiter (map encode_type types)) +fun encode_types types = space_implode delimiter (map encode_type types) fun parse_identifier x = (Scan.many identifier_character >> implode) x - -fun parse_star delim scanner x = + +fun parse_star delim scanner x = (Scan.optional (scanner ::: Scan.repeat ($$ delim |-- scanner)) []) x - + fun parse_type x = (Scan.this_string type_prefix |-- $$ open_paranthesis |-- parse_identifier --| $$ delimiter -- parse_star delimiter parse_any_type --| $$ close_parathesis >> Type) x and parse_tfree x = (Scan.this_string tfree_prefix |-- $$ open_paranthesis |-- parse_identifier --| $$ delimiter -- parse_star delimiter parse_identifier --| $$ close_parathesis >> TFree) x and parse_tvar x = (Scan.this_string tvar_prefix |-- $$ open_paranthesis |-- $$ open_paranthesis - |-- parse_identifier --| $$ delimiter -- (parse_identifier >> (Int.fromString #> the)) --| $$ - close_parathesis --| $$ delimiter -- parse_star delimiter parse_identifier --| + |-- parse_identifier --| $$ delimiter -- (parse_identifier >> (Int.fromString #> the)) --| $$ + close_parathesis --| $$ delimiter -- parse_star delimiter parse_identifier --| $$ close_parathesis >> TVar) x and parse_any_type x = (parse_type || parse_tfree || parse_tvar) x fun parse_types x = parse_star delimiter parse_any_type x - + fun decode_type_string s = Scan.finite Symbol.stopper (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^ quote s)) parse_type)) (Symbol.explode s) |> fst @@ -253,7 +253,7 @@ val is_lambda_name = String.isPrefix lam_lifted_poly_prefix -fun lookup table k = +fun lookup table k = List.find (fn (key, _) => key = k) table fun dest_list' (f $ t) = @@ -286,7 +286,7 @@ val (function, trms) = dest_list trm val info' = map_minimal_app' info trms in - case function of + case function of (Const _) => list_update (function, length trms) info' | (Free _) => list_update (function, length trms) info' | _ => info @@ -300,14 +300,14 @@ fun map_minimal_app trms = map_minimal_app' [] trms fun mk_waldmeister_app function [] = function - | mk_waldmeister_app function (a :: args) = + | mk_waldmeister_app function (a :: args) = let val funT = type_of function val argT = type_of a val resT = dest_funT funT |> snd val newT = funT --> argT --> resT in - mk_waldmeister_app (Const (waldmeister_apply ^ "," ^ + mk_waldmeister_app (Const (waldmeister_apply ^ "," ^ encode_types [resT, argT], newT) $ function $ a) args end @@ -318,8 +318,8 @@ in case function of Var _ => mk_waldmeister_app function trms' | - _ => - let + _ => + let val min_args = lookup info function |> the |> snd val args0 = List.take (trms',min_args) val args1 = List.drop (trms',min_args) @@ -349,9 +349,9 @@ in [ATerm ((gen_ascii_tuple (String.str const_prefix ^ encode_const (x, ty_args)), []), args)] end - | trm_to_atp'' _ (Free (x, _)) args = + | trm_to_atp'' _ (Free (x, _)) args = [ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), args)] - | trm_to_atp'' _ (Var ((x, _), _)) args = + | trm_to_atp'' _ (Var ((x, _), _)) args = [ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), args)] | trm_to_atp'' thy (trm1 $ trm2) args = trm_to_atp'' thy trm1 (trm_to_atp'' thy trm2 [] @ args) | trm_to_atp'' _ _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Unexpected term") @@ -374,7 +374,7 @@ let val (const_name, ty_args) = if String.isPrefix waldmeister_apply encoded_name then (waldmeister_apply, []) else decode_const encoded_name - val const_trans_name = + val const_trans_name = if is_lambda_name const_name then lam_lift_waldmeister_prefix ^ (* ?? *) String.extract(const_name, size lam_lifted_poly_prefix, NONE) @@ -390,20 +390,20 @@ else if prefix = free_prefix then Free (encoded_name, dummy_fun_type ()) else if Char.isUpper prefix then - Var ((name, 0), dummy_fun_type ()) + Var ((name, 0), dummy_fun_type ()) (* Use name instead of encoded_name because Waldmeister renames free variables. *) else if name = waldmeister_equals then - (case args of + (case args of [_, _] => eq_const dummyT - | _ => raise FailureMessage - (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ + | _ => raise FailureMessage + (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ Int.toString (length args))) else if name = waldmeister_true then @{term True} else if name = waldmeister_false then @{term False} else - raise FailureMessage + raise FailureMessage (WM_ERROR_MSG ^ "Unknown name prefix when parsing Waldmeister proof: name = " ^ name) end @@ -421,7 +421,7 @@ fun formula_to_trm thy (AAtom aterm) = aterm |> atp_to_trm thy | formula_to_trm thy (AConn (ANot, [aterm])) = mk_not (formula_to_trm thy aterm) - | formula_to_trm _ _ = + | formula_to_trm _ _ = raise FailureMessage (WM_ERROR_MSG ^ "formula_to_trm expects AAtom or AConn") (* Abstract translation *) @@ -460,11 +460,11 @@ end fun map_ctxt f ctxt xs = map_ctxt' f ctxt xs [] - - fun skolemize_fact ctxt (name, trm) = - let - val (ctxt', (steps, trm')) = skolemize true ctxt trm - in + + fun skolemize_fact ctxt (name, trm) = + let + val (ctxt', (steps, trm')) = skolemize true ctxt trm + in (ctxt', (name, (steps, trm'))) end @@ -472,7 +472,7 @@ | name_list' prefix (x :: xs) i = (prefix ^ Int.toString i, x) :: name_list' prefix xs (i + 1) fun name_list prefix xs = name_list' prefix xs 0 - + (* Skolemization, hiding lambdas and translating formulas to equations *) val (ctxt', sko_facts) = map_ctxt skolemize_fact ctxt facts val (ctxt'', sko_conditions) = map_ctxt (skolemize true) ctxt' conditions @@ -486,13 +486,13 @@ skolemize false ctxt'' consequence |> apsnd (apsnd (mk_eq_true #> apsnd post_skolem)) val sko_eq_info = - (((conj_identifier, eq_conseq) :: sko_eq_conditions0) + (((conj_identifier, eq_conseq) :: sko_eq_conditions0) @ map (apfst (fn name => fact_prefix ^ "0_" ^ name)) sko_eq_facts0) (* Translation of partial function applications *) val fun_app_info = map_minimal_app (map (snd o snd o snd) sko_eq_info) - fun hide_partial_apps_in_last (x, (y, (z, term))) = + fun hide_partial_apps_in_last (x, (y, (z, term))) = (x, (y, (z, hide_partial_applications fun_app_info term))) val sko_eq_facts = map hide_partial_apps_in_last sko_eq_facts0 @@ -547,9 +547,9 @@ SOME x => x | NONE => NONE -fun fix_name name = +fun fix_name name = if String.isPrefix fact_prefix name andalso String.isSuffix "_J" name then - String.extract(name, size fact_prefix + 2,NONE) |> unascii_of |> + String.extract(name, size fact_prefix + 2,NONE) |> unascii_of |> (fn x => fact_prefix ^ "0_" ^ x) else name @@ -573,7 +573,7 @@ | mk_steps i (x :: xs) = (((waldmeister_name ^ "_" ^ Int.toString i),[]), Plain, mk_Trueprop ((is_conjecture ? mk_not) x), waldmeister_skolemize_rule, [(waldmeister_name ^ "_" ^ Int.toString (i-1), - if i = 1 then isabelle_names else [])]) + if i = 1 then isabelle_names else [])]) :: mk_steps (i+1) xs val first_step = ((waldmeister_name ^ "_0", isabelle_names), Unknown, @@ -584,13 +584,13 @@ val skolem_steps = first_step :: sub_steps val num_of_steps = length skolem_steps in - (skolem_steps @ + (skolem_steps @ [((waldmeister_name, []), Unknown, trm, waldmeister_skolemize_rule, [(waldmeister_name ^ "_" ^ Int.toString (num_of_steps - 1), if num_of_steps = 1 then isabelle_names else [])])]) end end - + fun introduce_waldmeister_skolems info proof_steps = proof_steps |> maps (skolemization_steps info) end; diff -r fe6651760643 -r fb393ecde29d src/Pure/library.ML --- a/src/Pure/library.ML Thu Jan 29 15:21:16 2015 +0100 +++ b/src/Pure/library.ML Thu Jan 29 15:27:29 2015 +0100 @@ -708,7 +708,7 @@ val cartouche = enclose "\\" "\\"; -fun space_implode a bs = implode (separate a bs); +val space_implode = String.concatWith; val commas = space_implode ", "; val commas_quote = commas o map quote;