author | wenzelm |
Wed, 28 Oct 2009 22:04:57 +0100 | |
changeset 33291 | 93f0238151f6 |
parent 32857 | 394d37f19e0a |
child 34120 | f9920a3ddf50 |
permissions | -rw-r--r-- |
14350 | 1 |
(* Title: HOL/Tools/refute_isar.ML |
2 |
Author: Tjark Weber |
|
22092 | 3 |
Copyright 2003-2007 |
14350 | 4 |
|
32855 | 5 |
Outer syntax commands 'refute' and 'refute_params'. |
14350 | 6 |
*) |
7 |
||
32855 | 8 |
structure Refute_Isar: sig end = |
14350 | 9 |
struct |
10 |
||
32855 | 11 |
(* argument parsing *) |
14350 | 12 |
|
32855 | 13 |
(*optional list of arguments of the form [name1=value1, name2=value2, ...]*) |
14350 | 14 |
|
32855 | 15 |
val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name); |
14350 | 16 |
|
32855 | 17 |
val scan_parms = Scan.optional |
18 |
(OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") []; |
|
14350 | 19 |
|
20 |
||
32855 | 21 |
(* 'refute' command *) |
14350 | 22 |
|
32855 | 23 |
val _ = |
24 |
OuterSyntax.improper_command "refute" |
|
25 |
"try to find a model that refutes a given subgoal" OuterKeyword.diag |
|
32857
394d37f19e0a
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents:
32855
diff
changeset
|
26 |
(scan_parms -- Scan.optional OuterParse.nat 1 >> |
394d37f19e0a
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents:
32855
diff
changeset
|
27 |
(fn (parms, i) => |
394d37f19e0a
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents:
32855
diff
changeset
|
28 |
Toplevel.keep (fn state => |
394d37f19e0a
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents:
32855
diff
changeset
|
29 |
let |
394d37f19e0a
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents:
32855
diff
changeset
|
30 |
val thy = Toplevel.theory_of state; |
33291 | 31 |
val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state); |
32857
394d37f19e0a
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents:
32855
diff
changeset
|
32 |
in Refute.refute_goal thy parms st i end))); |
14350 | 33 |
|
34 |
||
32855 | 35 |
(* 'refute_params' command *) |
14350 | 36 |
|
32855 | 37 |
val _ = |
38 |
OuterSyntax.command "refute_params" |
|
39 |
"show/store default parameters for the 'refute' command" OuterKeyword.thy_decl |
|
40 |
(scan_parms >> (fn parms => |
|
41 |
Toplevel.theory (fn thy => |
|
42 |
let |
|
32857
394d37f19e0a
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents:
32855
diff
changeset
|
43 |
val thy' = fold Refute.set_default_param parms thy; |
32855 | 44 |
val output = |
45 |
(case Refute.get_default_params thy' of |
|
46 |
[] => "none" |
|
32857
394d37f19e0a
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents:
32855
diff
changeset
|
47 |
| new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults)); |
32855 | 48 |
val _ = writeln ("Default parameters for 'refute':\n" ^ output); |
32857
394d37f19e0a
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
wenzelm
parents:
32855
diff
changeset
|
49 |
in thy' end))); |
14350 | 50 |
|
51 |
end; |
|
52 |