Theory Transform_Cmd

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} ""
    (Transform_Parser.dp_fun_part1_parser >> Transform_DP.dp_fun_part1_cmd)

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

val _ =
  Outer_Syntax.local_theory_to_proof @{command_keyword memoize_correct} ""
    (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