Theory Sepref_Snip_Combinator

section ‹Snippet to Define Custom Combinators›
theory Sepref_Snip_Combinator
imports "../../IICF/IICF"
begin

  subsection ‹Definition of the Combinator›
  
  text ‹
    Currently, when defining new combinators, you are largely on your own.
    If you can show your combinator equivalent to some other, already existing, 
    combinator, you should apply this equivalence in the monadify phase.

    In this example, we show the development of a map combinator from scratch.
    ›

  text ‹We set ourselves in to a context where we fix the abstract and concrete 
    arguments of the monadic map combinator, as well as the refinement assertions,
    and a frame, that represents the remaining heap content, and may be read by the map-function. ›
  context 
    fixes f :: "'a ⇒ 'b nres"
    fixes l :: "'a list"

    fixes fi :: "'ai ⇒ 'bi Heap"
    fixes li :: "'ai list"

    fixes A A' :: "'a ⇒ 'ai ⇒ assn" ― ‹Refinement for list elements before and after map-function. 
      Different, as map function may invalidate list elements!›
    fixes B :: "'b ⇒ 'bi ⇒ assn"

    fixes F :: assn ― ‹Symbolic frame, representing all heap content the map-function body may access›

    notes [[sepref_register_adhoc f l]] ― ‹Register for operation id›

    assumes f_rl: "hn_refine (hn_ctxt A x xi * F) (fi xi) (hn_ctxt A' x xi * F) B (f$x)"
      ― ‹Refinement for ‹f››

  begin  

    text ‹We implement our combinator using the monadic refinement framework.›
    definition "mmap ≡ RECT (λmmap. 
      λ[] ⇒ RETURN [] 
    | x#xs ⇒ do { x ← f x; xs ← mmap xs; RETURN (x#xs) }) l"

    subsection ‹Synthesis of Implementation›

    text ‹In order to propagate the frame ‹F› during synthesis, we use a trick: We wrap the
      frame into a dummy refinement assertion. This way, sepref recognizes the frame just as
      another context element, and does correct propagation.›
    definition "F_assn (x::unit) (y::unit) ≡ F"
    lemma F_unf: "hn_ctxt F_assn x y = F"
      by (auto simp: F_assn_def hn_ctxt_def)

    text ‹We build a combinator rule to refine ‹f›. We need a combinator rule here,
      because ‹f› does not only depend on its formal arguments, but also on the frame 
      (represented as dummy argument). ›  
    lemma f_rl': "hn_refine (hn_ctxt A x xi * hn_ctxt (F_assn) dx dxi) (fi xi) (hn_ctxt A' x xi * hn_ctxt (F_assn) dx dxi) B (f$x)" 
      unfolding F_unf by (rule f_rl)

    text ‹Then we use the Sepref tool to synthesize an implementation of ‹mmap›.›  
    schematic_goal mmap_impl:
      notes [sepref_comb_rules] = hn_refine_frame[OF f_rl']
      shows "hn_refine (hn_ctxt (list_assn A) l li * hn_ctxt (F_assn) dx dxi) (?c::?'c Heap) ?Γ' ?R mmap"
      unfolding mmap_def "HOL_list.fold_custom_empty"
      apply sepref_dbg_keep
      done

    text ‹We unfold the wrapped frame›  
    lemmas mmap_impl' = mmap_impl[unfolded F_unf]
  
  end

  subsection ‹Setup for Sepref›
  text ‹Outside the context, we extract the synthesized implementation as a new constant, and set up
    code theorems for the fixed-point combinators.›
  concrete_definition mmap_impl uses mmap_impl'
  prepare_code_thms mmap_impl_def

  text ‹Moreover, we have to manually declare arity and monadify theorems.
    The arity theorem ensures that we always have a constant number of operators, and 
    the monadify theorem determines an execution order: The list-argument is evaluated first.
    ›
  lemma mmap_arity[sepref_monadify_arity]: "mmap ≡ λ2f l. SP mmap$(λ2x. f$x)$l" by simp
  lemma mmap_mcomb[sepref_monadify_comb]: "mmap$f$x ≡ (⤜)$(EVAL$x)$(λ2x. SP mmap$f$x)" by simp

  text ‹We can massage the refinement theorem @{thm mmap_impl.refine} a bit, to get a valid 
    combinator rule›
  print_statement hn_refine_cons_pre[OF _ mmap_impl.refine, sepref_prep_comb_rule, no_vars]

  lemma mmap_comb_rl[sepref_comb_rules]:
    assumes "P ⟹t hn_ctxt (list_assn A) l li * F"
        ― ‹Initial frame›
      and "⋀x xi. hn_refine (hn_ctxt A x xi * F) (fi xi) (Q x xi) B (f x)"
        ― ‹Refinement of map-function›
      and "⋀x xi. Q x xi ⟹t hn_ctxt A' x xi * F"
        ― ‹Recover refinement for list-element and original frame from what map-function produced›
    shows "hn_refine P (mmap_impl fi li) (hn_ctxt (list_assn A') l li * F) (list_assn B) (mmap$(λ2x. f x)$l)"
    unfolding APP_def PROTECT2_def
    using hn_refine_cons_pre[OF _ mmap_impl.refine, sepref_prep_comb_rule, of P A l li F fi Q B f A']
    using assms
    by simp

  subsection ‹Example›  

  text ‹Finally, we can test our combinator. Note how the 
    map-function accesses the array on the heap, which is not among its arguments. 
    This is only possible as we passed around a frame. ›    

  sepref_thm test_mmap 
    is "λl. do { let a = op_array_of_list [True,True,False]; mmap (λx. do { mop_list_get a (x mod 3) }) l }"
    :: "(list_assn nat_assn)k →a list_assn bool_assn"
    unfolding HOL_list.fold_custom_empty
    by sepref

  subsection ‹Limitations›  
  text ‹
    Currently, the major limitation is that combinator rules are fixed to specific data types.
    In our example, we did an implementation for HOL lists. We cannot come up with an alternative implementation, 
    for, e.g., array-lists, but have to use a different abstract combinator.

    One workaround is to use some generic operations, as is done for foreach-loops, which require
    a generic to-list operation. However, in this case, we produce unwanted intermediate lists, and
    would have to add complicated a-posteriori deforestation optimizations.
    ›

end