src/HOL/Tools/refute_isar.ML
author paulson
Tue May 22 17:56:06 2007 +0200 (2007-05-22)
changeset 23075 69e30a7e8880
parent 22092 ab3dfcef6489
child 24867 e5b55d7be9bb
permissions -rw-r--r--
Some hacks for SPASS format
     1 (*  Title:      HOL/Tools/refute_isar.ML
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2003-2007
     5 
     6 Adds the 'refute' and 'refute_params' commands to Isabelle/Isar's outer
     7 syntax.
     8 *)
     9 
    10 structure RefuteIsar =
    11 struct
    12 
    13 (* ------------------------------------------------------------------------- *)
    14 (* common functions for argument parsing/scanning                            *)
    15 (* ------------------------------------------------------------------------- *)
    16 
    17 (* ------------------------------------------------------------------------- *)
    18 (* both 'refute' and 'refute_params' take an optional list of arguments of   *)
    19 (* the form [name1=value1, name2=value2, ...]                                *)
    20 (* ------------------------------------------------------------------------- *)
    21 
    22 	fun repeatd delim scan = scan -- Scan.repeat (OuterParse.$$$ delim |-- scan)
    23 		>> op :: || Scan.succeed [];
    24 
    25 	val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
    26 
    27 	val scan_parms = Scan.option
    28 		(OuterParse.$$$ "[" |-- (repeatd "," scan_parm) --| OuterParse.$$$ "]");
    29 
    30 (* ------------------------------------------------------------------------- *)
    31 (* set up the 'refute' command                                               *)
    32 (* ------------------------------------------------------------------------- *)
    33 
    34 (* ------------------------------------------------------------------------- *)
    35 (* 'refute' takes an optional list of parameters, followed by an optional    *)
    36 (* subgoal number                                                            *)
    37 (* ------------------------------------------------------------------------- *)
    38 
    39 	val refute_scan_args = scan_parms -- (Scan.option OuterParse.nat);
    40 
    41 (* ------------------------------------------------------------------------- *)
    42 (* the 'refute' command is mapped to 'Refute.refute_subgoal'                 *)
    43 (* ------------------------------------------------------------------------- *)
    44 
    45 	fun refute_trans args =
    46 		Toplevel.keep (fn state =>
    47 			let
    48 				val (parms_opt, subgoal_opt) = args
    49 				val parms   = Option.getOpt (parms_opt, [])
    50 				val subgoal = Option.getOpt (subgoal_opt, 1) - 1
    51 				val thy     = Toplevel.theory_of state
    52 				val thm     = (snd o snd) (Proof.get_goal (Toplevel.proof_of state))
    53 			in
    54 				Refute.refute_subgoal thy parms thm subgoal
    55 			end);
    56 
    57 	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
    58 
    59 	val refute_cmd = OuterSyntax.improper_command "refute"
    60 		"try to find a model that refutes a given subgoal"
    61 		OuterKeyword.diag refute_parser;
    62 
    63 (* ------------------------------------------------------------------------- *)
    64 (* set up the 'refute_params' command                                        *)
    65 (* ------------------------------------------------------------------------- *)
    66 
    67 (* ------------------------------------------------------------------------- *)
    68 (* 'refute_params' takes an optional list of parameters                      *)
    69 (* ------------------------------------------------------------------------- *)
    70 
    71 	val refute_params_scan_args = scan_parms;
    72 
    73 (* ------------------------------------------------------------------------- *)
    74 (* the 'refute_params' command is mapped to (multiple calls of)              *)
    75 (* 'Refute.set_default_param'; then the (new) default parameters are         *)
    76 (* displayed                                                                 *)
    77 (* ------------------------------------------------------------------------- *)
    78 
    79 	fun refute_params_trans args =
    80 		let
    81 			fun add_params thy [] =
    82 				thy
    83 			  | add_params thy (p::ps) =
    84 				add_params (Refute.set_default_param p thy) ps
    85 		in
    86 			Toplevel.theory (fn thy =>
    87 				let
    88 					val thy'               = add_params thy (getOpt (args, []))
    89 					val new_default_params = Refute.get_default_params thy'
    90 					val output             = if new_default_params=[] then
    91 							"none"
    92 						else
    93 							space_implode "\n" (map (fn (name, value) => name ^ "=" ^ value)
    94 								new_default_params)
    95 				in
    96 					writeln ("Default parameters for 'refute':\n" ^ output);
    97 					thy'
    98 				end)
    99 		end;
   100 
   101 	fun refute_params_parser tokens =
   102 		(refute_params_scan_args tokens) |>> refute_params_trans;
   103 
   104 	val refute_params_cmd = OuterSyntax.command "refute_params"
   105 		"show/store default parameters for the 'refute' command"
   106 		OuterKeyword.thy_decl refute_params_parser;
   107 
   108 end;
   109 
   110 (* ------------------------------------------------------------------------- *)
   111 (* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's  *)
   112 (* outer syntax                                                              *)
   113 (* ------------------------------------------------------------------------- *)
   114 
   115 OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];