387 else if Char.isUpper prefix then |
387 else if Char.isUpper prefix then |
388 Var ((name, 0), dummy_fun_type ()) |
388 Var ((name, 0), dummy_fun_type ()) |
389 (* Use name instead of encoded_name because Waldmeister renames free variables. *) |
389 (* Use name instead of encoded_name because Waldmeister renames free variables. *) |
390 else if name = waldmeister_equals then |
390 else if name = waldmeister_equals then |
391 (case args of |
391 (case args of |
392 [_, _] => eq_const @{typ bool} |
392 [_, _] => eq_const dummyT |
393 | _ => raise FailureMessage |
393 | _ => raise FailureMessage |
394 (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ |
394 (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ |
395 Int.toString (length args))) |
395 Int.toString (length args))) |
396 else if name = waldmeister_true then |
396 else if name = waldmeister_true then |
397 @{term True} |
397 @{term True} |
539 #> repair_waldmeister_endgame |
539 #> repair_waldmeister_endgame |
540 |
540 |
541 fun get_skolem_info info names = case map (lookup info) names |> List.find is_some of |
541 fun get_skolem_info info names = case map (lookup info) names |> List.find is_some of |
542 SOME x => x | |
542 SOME x => x | |
543 NONE => NONE |
543 NONE => NONE |
544 |
544 |
545 fun fix_name name = (* fixme *) |
545 fun fix_name name = |
546 if String.isPrefix fact_prefix name then |
546 let |
547 String.extract(name,7,NONE) |> unascii_of |> curry (op ^) "fact_0_" |
547 fun drop_digits' xs [] = (xs, []) |
548 else |
548 | drop_digits' xs (c :: cs) = if Char.isDigit c then drop_digits' (c :: xs) cs else |
549 name |
549 (xs, (c :: cs)) |
|
550 fun drop_digits xs = drop_digits' [] xs |
|
551 in |
|
552 if String.isPrefix fact_prefix name then |
|
553 String.extract(name,size fact_prefix,NONE) |> String.explode |> drop_digits ||> tl |
|
554 ||> String.implode ||> unascii_of |> (fn (x,y) => fact_prefix ^ String.implode x ^ "_" ^ y) |
|
555 else |
|
556 name |
|
557 end |
550 |
558 |
551 fun skolemization_steps info |
559 fun skolemization_steps info |
552 (proof_step as ((waldmeister_name, isabelle_names), _, trm, rule, _)) = |
560 (proof_step as ((waldmeister_name, isabelle_names), _, trm, rule, _)) = |
553 case get_skolem_info info (map fix_name isabelle_names) of |
561 case get_skolem_info info (map fix_name isabelle_names) of |
554 NONE => [proof_step] | |
562 NONE => [proof_step] | |