webertj@14350: (* Title: HOL/Tools/refute_isar.ML webertj@14350: ID: $Id$ webertj@14350: Author: Tjark Weber webertj@22092: Copyright 2003-2007 webertj@14350: webertj@14350: Adds the 'refute' and 'refute_params' commands to Isabelle/Isar's outer webertj@14350: syntax. webertj@14350: *) webertj@14350: wenzelm@24867: structure RefuteIsar: sig end = webertj@14350: struct webertj@14350: webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: (* common functions for argument parsing/scanning *) webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: (* both 'refute' and 'refute_params' take an optional list of arguments of *) webertj@14350: (* the form [name1=value1, name2=value2, ...] *) webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: webertj@22092: fun repeatd delim scan = scan -- Scan.repeat (OuterParse.$$$ delim |-- scan) webertj@22092: >> op :: || Scan.succeed []; webertj@14350: webertj@22092: val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name); webertj@14350: webertj@22092: val scan_parms = Scan.option webertj@22092: (OuterParse.$$$ "[" |-- (repeatd "," scan_parm) --| OuterParse.$$$ "]"); webertj@14350: webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: (* set up the 'refute' command *) webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: (* 'refute' takes an optional list of parameters, followed by an optional *) webertj@14350: (* subgoal number *) webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: webertj@14350: val refute_scan_args = scan_parms -- (Scan.option OuterParse.nat); webertj@14350: webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: (* the 'refute' command is mapped to 'Refute.refute_subgoal' *) webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: webertj@14350: fun refute_trans args = webertj@22092: Toplevel.keep (fn state => webertj@22092: let webertj@22092: val (parms_opt, subgoal_opt) = args webertj@22092: val parms = Option.getOpt (parms_opt, []) webertj@22092: val subgoal = Option.getOpt (subgoal_opt, 1) - 1 webertj@22092: val thy = Toplevel.theory_of state webertj@22092: val thm = (snd o snd) (Proof.get_goal (Toplevel.proof_of state)) webertj@22092: in webertj@22092: Refute.refute_subgoal thy parms thm subgoal webertj@22092: end); webertj@14350: webertj@14350: fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans; webertj@14350: wenzelm@24867: val _ = OuterSyntax.improper_command "refute" webertj@22092: "try to find a model that refutes a given subgoal" webertj@22092: OuterKeyword.diag refute_parser; webertj@14350: webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: (* set up the 'refute_params' command *) webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: (* 'refute_params' takes an optional list of parameters *) webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: webertj@14350: val refute_params_scan_args = scan_parms; webertj@14350: webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: (* the 'refute_params' command is mapped to (multiple calls of) *) webertj@14350: (* 'Refute.set_default_param'; then the (new) default parameters are *) webertj@14350: (* displayed *) webertj@14350: (* ------------------------------------------------------------------------- *) webertj@14350: webertj@14350: fun refute_params_trans args = webertj@14350: let webertj@22092: fun add_params thy [] = webertj@22092: thy webertj@22092: | add_params thy (p::ps) = webertj@22092: add_params (Refute.set_default_param p thy) ps webertj@14350: in webertj@14350: Toplevel.theory (fn thy => webertj@14350: let webertj@22092: val thy' = add_params thy (getOpt (args, [])) webertj@14350: val new_default_params = Refute.get_default_params thy' webertj@22092: val output = if new_default_params=[] then webertj@22092: "none" webertj@22092: else webertj@22092: space_implode "\n" (map (fn (name, value) => name ^ "=" ^ value) webertj@22092: new_default_params) webertj@14350: in webertj@14350: writeln ("Default parameters for 'refute':\n" ^ output); webertj@14350: thy' webertj@14350: end) webertj@14350: end; webertj@14350: webertj@22092: fun refute_params_parser tokens = webertj@22092: (refute_params_scan_args tokens) |>> refute_params_trans; webertj@14350: wenzelm@24867: val _ = OuterSyntax.command "refute_params" webertj@22092: "show/store default parameters for the 'refute' command" webertj@22092: OuterKeyword.thy_decl refute_params_parser; webertj@14350: webertj@14350: end; webertj@14350: