Theory Transform_Cmd

theory Transform_Cmd
imports DP_CRelVH
subsection ‹Tool Setup›

theory Transform_Cmd
  imports
    "../Pure_Monad"
    "../state_monad/DP_CRelVS"
    "../heap_monad/DP_CRelVH"
  keywords
    "memoize_fun" :: thy_decl
    and "monadifies" :: thy_decl
    and "memoize_correct" :: thy_goal
    and "with_memory" :: quasi_command
    and "default_proof" :: quasi_command
begin

ML_file ‹../transform/Transform_Misc.ML›
ML_file ‹../transform/Transform_Const.ML›
ML_file ‹../transform/Transform_Data.ML›
ML_file ‹../transform/Transform_Tactic.ML›
ML_file ‹../transform/Transform_Term.ML›
ML_file ‹../transform/Transform.ML›
ML_file ‹../transform/Transform_Parser.ML›

ML ‹
val _ =
  Outer_Syntax.local_theory @{command_keyword memoize_fun} "whatever"
    (Transform_Parser.dp_fun_part1_parser >> Transform_DP.dp_fun_part1_cmd)

val _ =
  Outer_Syntax.local_theory @{command_keyword monadifies} "whatever"
    (Transform_Parser.dp_fun_part2_parser >> Transform_DP.dp_fun_part2_cmd)
›

ML ‹
val _ =
  Outer_Syntax.local_theory_to_proof @{command_keyword memoize_correct} "whatever"
    (Scan.succeed Transform_DP.dp_correct_cmd)
›

method_setup memoize_prover = ‹
Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
  Transform_Data.get_last_cmd_info ctxt
  |> Transform_Tactic.solve_consistentDP_tac ctxt)))
›

method_setup memoize_prover_init = ‹
Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
  Transform_Data.get_last_cmd_info ctxt
  |> Transform_Tactic.prepare_consistentDP_tac ctxt)))
›

method_setup memoize_prover_case_init = ‹
Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
  Transform_Data.get_last_cmd_info ctxt
  |> Transform_Tactic.prepare_case_tac ctxt)))
›

method_setup memoize_prover_match_step = ‹
Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
  Transform_Data.get_last_cmd_info ctxt
  |> Transform_Tactic.step_tac ctxt)))
›

method_setup memoize_unfold_defs  = ‹
Scan.option (Scan.lift (Args.parens Args.name) -- Args.term) >> (fn tm_opt => fn ctxt => (SIMPLE_METHOD' (
  Transform_Data.get_or_last_cmd_info ctxt tm_opt
  |> Transform_Tactic.dp_unfold_defs_tac ctxt)))
›

method_setup memoize_combinator_init  = ‹
Scan.option (Scan.lift (Args.parens Args.name) -- Args.term) >> (fn tm_opt => fn ctxt => (SIMPLE_METHOD' (
  Transform_Data.get_or_last_cmd_info ctxt tm_opt
  |> Transform_Tactic.prepare_combinator_tac ctxt)))
›
end (* theory *)