3255 add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #> |
3255 add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #> |
3256 add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #> |
3256 add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #> |
3257 add_printer "stlc" stlc_printer #> |
3257 add_printer "stlc" stlc_printer #> |
3258 add_printer "IDT" IDT_printer; |
3258 add_printer "IDT" IDT_printer; |
3259 |
3259 |
|
3260 |
|
3261 |
|
3262 (** outer syntax commands 'refute' and 'refute_params' **) |
|
3263 |
|
3264 (* argument parsing *) |
|
3265 |
|
3266 (*optional list of arguments of the form [name1=value1, name2=value2, ...]*) |
|
3267 |
|
3268 val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true") |
|
3269 val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") []; |
|
3270 |
|
3271 |
|
3272 (* 'refute' command *) |
|
3273 |
|
3274 val _ = |
|
3275 Outer_Syntax.improper_command "refute" |
|
3276 "try to find a model that refutes a given subgoal" Keyword.diag |
|
3277 (scan_parms -- Scan.optional Parse.nat 1 >> |
|
3278 (fn (parms, i) => |
|
3279 Toplevel.keep (fn state => |
|
3280 let |
|
3281 val ctxt = Toplevel.context_of state; |
|
3282 val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state); |
|
3283 in refute_goal ctxt parms st i end))); |
|
3284 |
|
3285 |
|
3286 (* 'refute_params' command *) |
|
3287 |
|
3288 val _ = |
|
3289 Outer_Syntax.command "refute_params" |
|
3290 "show/store default parameters for the 'refute' command" Keyword.thy_decl |
|
3291 (scan_parms >> (fn parms => |
|
3292 Toplevel.theory (fn thy => |
|
3293 let |
|
3294 val thy' = fold set_default_param parms thy; |
|
3295 val output = |
|
3296 (case get_default_params thy' of |
|
3297 [] => "none" |
|
3298 | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults)); |
|
3299 val _ = writeln ("Default parameters for 'refute':\n" ^ output); |
|
3300 in thy' end))); |
|
3301 |
3260 end; |
3302 end; |
3261 |
3303 |