Theory PhiSem_CF_Routine

theory PhiSem_CF_Routine
  imports PhiSem_CF_Break PhiSem_CF_Routine_Basic PhiSem_Void
begin

text ‹Based on the basic routine module, we provide the version that supports return statement.›

declare [[φhide_techinicals = false]]

definition RETURN_FRAME :: ‹'rets::FIX_ARITY_VALs itself ⇒ RES.brk_label ⇒ ('rets φarg ⇒ fiction BI) ⇒ bool›
  where ‹RETURN_FRAME _ label Y ⟷ True›

lemma RETURN_FRAME_I:
  ‹ RETURN_FRAME TY label Y ›
  unfolding RETURN_FRAME_def ..

lemma RETURN_FRAME_normal:
  ‹ RETURN_FRAME TYPE('rets) label Y
⟹ 𝗉𝗋𝗈𝖼 (op_break TYPE('any) TYPE('rets) label ret) ⦃ TECHNICAL Brk_Frame label❟ Y ret ⟼ 0 ⦄
    𝗍𝗁𝗋𝗈𝗐𝗌 (λ_. Brking_Frame label Y) ›
  for ret :: ‹'rets::FIX_ARITY_VALs φarg›
  using op_break_φapp .

lemma RETURN_FRAME_unit:
  ‹ RETURN_FRAME TYPE(unit) label Y
⟹ 𝗉𝗋𝗈𝖼 (op_break TYPE('any) TYPE(unit) label (φarg ())) ⦃ TECHNICAL Brk_Frame label❟ Y (φarg ()) ⟼ 0 ⦄
    𝗍𝗁𝗋𝗈𝗐𝗌 (λ_. Brking_Frame label Y) ›
  using op_break_φapp[where S=Y] .

(* TODO: suppress the Frame tailing in the above rules!!!!
lemma RETURN_FRAME_normal:
  ‹ RETURN_FRAME TYPE('rets) label Y
⟹ State 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y ret❟ TECHNICAL Brk_Frame label
⟹ 𝗉𝗋𝗈𝖼 (op_break TYPE('any) TYPE('rets) label ret) ⦃ State ⟼ 0 ⦄
    𝗍𝗁𝗋𝗈𝗐𝗌 (λ_. Brking_Frame label Y) ›
  for ret :: ‹'rets::FIX_ARITY_VALs φarg›
❴ premises _ and Tr 
  Tr
  op_break_φapp
❵ .

term ‹Identity_Elements›

lemma RETURN_FRAME_unit:
  ‹ RETURN_FRAME TYPE(unit) label Y
⟹ State 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y (φarg ())❟ TECHNICAL Brk_Frame label
⟹ 𝗉𝗋𝗈𝖼 (op_break TYPE('any) TYPE(unit) label (φarg ())) ⦃ State ⟼ 0 ⦄
    𝗍𝗁𝗋𝗈𝗐𝗌 (λ_. Brking_Frame label Y) ›
❴ premises _ and Tr
  Tr
  apply_rule op_break_φapp[where S=Y]
❵ .
*)

attribute_setup RETURN_FRAME = ‹Scan.succeed (Thm.rule_attribute [] (fn ctxt => fn th =>
                    th RS (Thm.transfer'' ctxt @{thm' RETURN_FRAME_unit})
    handle THM _ => th RS (Thm.transfer'' ctxt @{thm' RETURN_FRAME_normal})) )›

declare [[
  φpremise_attribute [RETURN_FRAME] for ‹RETURN_FRAME _ _ _›  (%φattr)
]]

(* RETURN_FRAME TYPE('rets::FIX_ARITY_VALs) label_ret *)

proc op_routine:
  requires Ty_X: ‹Semantic_Types X TY_ARGs›
      and  Ty_Y: ‹Semantic_Types Y TY_RETs›
      and  ‹𝗋Success›
      and  F: ‹(⋀(vs:: 'args::FIX_ARITY_VALs φarg <named> 'names) label_ret.
            return_φapp❙: TECHNICAL(RETURN_FRAME TYPE('rets::FIX_ARITY_VALs) label_ret Y)
            ⟹ 𝗉𝗋𝗈𝖼 F label_ret (case_named (λx. x) vs)
                   ⦃ TECHNICAL Brk_Frame label_ret❟ X (case_named id vs)
                 ⟼ λret. TECHNICAL Brk_Frame label_ret❟ Y ret
                   ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λe. 𝖻𝗋𝖾𝖺𝗄 label_ret 𝗐𝗂𝗍𝗁 Y 𝗈𝗋 E e))›
  input  ‹X vs›
  output ‹Y›
  throws ‹E›
❴
  apply_rule "__routine_basic__"[OF Ty_X Ty_Y 𝗋Success_I, where 'names='names,
                                 unfolded named_All, simplified]
  ❴ for vs 
    op_brk_scope ❴  for label_ret
      apply_rule F[of label_ret ‹tag vs›, unfolded Technical_def[where 'a=‹bool›], simplified, OF RETURN_FRAME_I]
    ❵
  ❵
❵ .

ML ‹Synchronized.change Phi_Syntax.semantic_oprs (Symtab.update (\<^const_name>‹op_routine›, 0))›


abbreviation
  ‹op_rec_routine argtys rettys F ≡ op_fix_point (λ𝖿.
        op_routine TYPE('ret::FIX_ARITY_VALs) TYPE('arg::FIX_ARITY_VALs) argtys rettys (F 𝖿))›


attribute_setup routine =
  ‹Scan.succeed (Phi_Modifier.wrap_to_attribute
      (PhiSem_Control_Flow.routine_mod
          (fn T => \<^typ>‹RES.brk_label› --> T)
          (fn N => fn wrap => fn Tm => Abs("label_ret", \<^typ>‹RES.brk_label›, wrap (Tm $ Bound N)))
          @{thm "op_routine_φapp"}))›

hide_fact RETURN_FRAME_normal RETURN_FRAME_unit


subsection ‹Syntax›

syntax "_routine_" :: ‹idt ⇒ logic ⇒ logic ⇒ do_binds ⇒ do_bind›
          ("((2𝗋𝗈𝗎𝗍𝗂𝗇𝖾 '(_ : _') : _ {//)(_)//})" [12,12,100,12] 13)
       "_recursive_routine_" :: ‹idt ⇒ idt ⇒ logic ⇒ logic ⇒ do_binds ⇒ do_bind›
          ("((2𝗋𝖾𝖼𝗎𝗋𝗌𝗂𝗏𝖾-𝗋𝗈𝗎𝗍𝗂𝗇𝖾 _ '(_ : _') : _ {//)(_)//})")

print_ast_translation ‹let open Ast
  fun get_label (Appl [Constant "_constrain", BV, _]) = get_label BV
    | get_label (Appl [Constant "_bound", Variable bv]) = bv
  fun is_label lb (Appl [Constant "_constrain", BV, _]) = is_label lb BV
    | is_label lb (Appl [Constant "_bound", Variable bv]) = bv = lb
  fun tr lret (tm as Appl [Constant \<^const_syntax>‹PhiSem_CF_Break.op_break›, _, _, BV, X]) =
        if is_label lret BV
        then Appl [Constant \<^const_syntax>‹Return›, X]
        else tm
    | tr lret (Appl aps) = Appl (map (tr lret) aps)
    | tr _ X = X
  fun tr0 cfg (Appl [Constant \<^syntax_const>‹_do_block›, X]) = tr cfg X
    | tr0 cfg X = tr cfg X
  fun strip_list (Appl [Constant \<^syntax_const>‹_list›, X]) = strip_list X
    | strip_list (Appl [Constant "_args", A, B]) =
        Appl [Constant "\<^const>Product_Type.Times", strip_list A, strip_list B]
    | strip_list (Constant \<^const_syntax>‹Nil›) =
        Constant \<^const_syntax>‹𝗏𝗈𝗂𝖽›
    | strip_list X = X
in [
  (\<^const_syntax>‹op_routine›, fn ctxt =>
    if Syntax_Group.is_enabled (Proof_Context.theory_of ctxt) @{syntax_group do_notation}
    then
      fn [_, _, TY1, TY2, Appl [Constant "_abs", lret, Appl [Constant "_abs", arg, X]]] =>
          Appl [Constant \<^syntax_const>‹_routine_›, arg,
                strip_list TY1, strip_list TY2, tr0 (get_label lret) X]
       | [_, _, TY1, TY2, Appl [Constant "_abs", lret, Appl [Constant "_abs", arg, X]], Y] =>
          Appl [
            Appl [Constant \<^syntax_const>‹_routine_›, arg,
                  strip_list TY1, strip_list TY2, tr0 (get_label lret) X],
            Y]
    else fn _ => raise Match),
  (\<^const_syntax>‹op_rec_routine›, fn ctxt =>
    if Syntax_Group.is_enabled (Proof_Context.theory_of ctxt) @{syntax_group do_notation}
    then
      fn [TY1, TY2, Appl [Constant "_abs", lf,
                              Appl [Constant "_abs", lret, Appl [Constant "_abs", arg, X]]]] =>
          Appl [Constant \<^syntax_const>‹_recursive_routine_›, lf, arg,
                strip_list TY1, strip_list TY2, tr0 (get_label lret) X]
       | [TY1, TY2, Appl [Constant "_abs", lf, 
                              Appl [Constant "_abs", lret, Appl [Constant "_abs", arg, X]], Y]] =>
          Appl [
            Appl [Constant \<^syntax_const>‹_routine_›, lf, arg,
                  strip_list TY1, strip_list TY2, tr0 (get_label lret) X],
            Y]
    else fn _ => raise Match)
] end›




end