Theory AbsCF

section "Abstract nonstandard semantics"

theory AbsCF
  imports HOLCF HOLCFUtils CPSScheme Utils SetMap
begin

default_sort type

text ‹
After having defined the exact meaning of a control graph, we now alter the algorithm into a statically computable. We note that the contour pointer in the exact semantics is taken from an infinite set. This is unavoidable, as recursion depth is unbounded. But if this were not the case and the set were finite, the function would be calculable, having finite range and domain.

Therefore, we make the set of contour counter values finite and accept that this makes our result less exact, but calculable. We also do not work with values any more but only remember, for each variable, what possible lambdas can occur there. Because we do not have exact values any more, in a conditional expression, both branches are taken.

We want to leave the exact choice of the finite contour set open for now. Therefore, we define a type class capturing the relevant definitions and the fact that the set is finite. Isabelle expects type classes to be non-empty, so we show that the ‹unit› type is in this type class.
›

class contour = finite +
  fixes nb_a :: "'a ⇒ label ⇒ 'a" (‹\<anb>›)
    and a_initial_contour :: 'a (‹\<abinit>›)

instantiation unit :: contour
begin
definition "\<anb> _ _ = ()"
definition "\<abinit> = ()"
instance by standard auto
end

text ‹
Analogous to the previous section, we define types for binding environments, closures, procedures, semantic values (which are now sets of possible procedures) and variable environment. Their types are parametrized by the chosen set of abstract contours.

The abstract variable environment is a partial map to sets in Shivers' dissertation. As he does not need to distinguish between a key not in the map and a key mapped to the empty set, this presentation is redundant. Therefore, I encoded this as a function from keys to sets of values. The theory @{theory "Shivers-CFA.SetMap"} contains functions and lemmas to work with such maps, symbolized by an appended dot (e.g. ‹{}.›, ‹∪.›).
›

type_synonym 'c a_benv = "label ⇀ 'c" (‹_ \<abenv>› [1000])
type_synonym 'c a_closure = "lambda × 'c \<abenv>" (‹_ \<aclosure>› [1000])

datatype 'c proc (‹_ \<aproc>› [1000])
  = PC "'c \<aclosure>"
  | PP prim
  | AStop

type_synonym 'c a_d = "'c \<aproc> set" (‹_ \<ad>› [1000])

type_synonym 'c a_venv = "var × 'c ⇒ 'c \<ad>" (‹_ \<avenv>› [1000])

text ‹
The evaluation function now ignores constants and returns singletons for primitive operations and lambda expressions.
›

fun evalV_a :: "val ⇒ 'c \<abenv> ⇒ 'c \<avenv> ⇒ 'c \<ad>" (‹\<aA>›)
  where "\<aA> (C _ i) β ve = {}"
  |     "\<aA> (P prim) β ve = {PP prim}"
  |     "\<aA> (R _ var) β ve =
           (case β (binder var) of
              Some l ⇒ ve (var,l)
            | None ⇒ {})"
  |     "\<aA> (L lam) β ve = {PC (lam, β)}"

text ‹
The types of the calculated graph, the arguments to ‹\<aF>› and ‹\<aC>› resemble closely the types in the exact case, with each type replaced by its abstract counterpart.
›

type_synonym 'c a_ccache = "((label × 'c \<abenv>) × 'c \<aproc>) set" (‹_ \<accache>› [1000])
type_synonym 'c a_ans = "'c \<accache>" (‹_ \<aans>› [1000])

type_synonym 'c a_fstate = "('c \<aproc> × 'c \<ad> list × 'c \<avenv> × 'c)" (‹_ \<afstate>› [1000])
type_synonym 'c a_cstate = "(call × 'c \<abenv> × 'c \<avenv> × 'c)" (‹_ \<acstate>› [1000])

text ‹
And yet again, cont2cont results need to be shown for our custom data types.
›

lemma cont2cont_case_lambda [simp, cont2cont]:
  assumes "⋀a b c. cont (λx. f x a b c)"
  shows "cont (λx. case_lambda (f x) l)"
using assms
by (cases l) auto

lemma cont2cont_case_proc [simp, cont2cont]:
  assumes "⋀y. cont (λx. f1 x y)"
     and  "⋀y. cont (λx. f2 x y)"
     and  "cont (λx. f3 x)"
  shows "cont (λx. case_proc (f1 x) (f2 x) (f3 x) d)"
using assms
by (cases d) auto

lemma cont2cont_case_call [simp, cont2cont]:
  assumes "⋀a b c. cont (λx. f1 x a b c)"
     and  "⋀a b c. cont (λx. f2 x a b c)"
  shows "cont (λx. case_call (f1 x) (f2 x) c)"
using assms
by (cases c) auto

lemma cont2cont_case_prim [simp, cont2cont]:
  assumes "⋀y. cont (λx. f1 x y)"
     and  "⋀y z. cont (λx. f2 x y z)"
  shows "cont (λx. case_prim (f1 x) (f2 x) p)"
using assms
by (cases p) auto

text ‹
We can now define the abstract nonstandard semantics, based on the equations in Figure 4.5 and 4.6 of Shivers' dissertation. In the ‹AStop› case, ‹{}› is returned, while for wrong arguments, ‹⊥› is returned. Both actually represent the same value, the empty set, so this is just a aesthetic difference.
›

fixrec   a_evalF :: "'c::contour \<afstate> discr → 'c \<aans>" (‹\<aF>›)
     and a_evalC :: "'c::contour \<acstate> discr → 'c \<aans>" (‹\<aC>›)
  where "\<aF>⋅fstate = (case undiscr fstate of
             (PC (Lambda lab vs c, β), as, ve, b) ⇒
               (if length vs = length as
                then let β' = β (lab ↦ b);
                         ve' = ve ∪. (⋃. (map (λ(v,a). {(v,b) := a}.) (zip vs as)))
                     in \<aC>⋅(Discr (c,β',ve',b))
                else ⊥)
            | (PP (Plus c),[_,_,cnts],ve,b) ⇒
                     let b' = \<anb> b c;
                         β  = [c ↦ b]
                     in (⋃cnt∈cnts. \<aF>⋅(Discr (cnt,[{}],ve,b')))
                        ∪
                        {((c, β), cont) | cont . cont ∈ cnts}
            | (PP (prim.If ct cf),[_, cntts, cntfs],ve,b) ⇒
                  ((   let b' = \<anb> b ct;
                            β = [ct ↦ b]
                        in (⋃cnt∈cntts . \<aF>⋅(Discr (cnt,[],ve,b')))
                           ∪{((ct, β), cnt) | cnt . cnt ∈ cntts}
                   )∪(
                       let b' = \<anb> b cf;
                            β = [cf ↦ b]
                        in (⋃cnt∈cntfs . \<aF>⋅(Discr (cnt,[],ve,b')))
                           ∪{((cf, β), cnt) | cnt . cnt ∈ cntfs}
                   ))
            | (AStop,[_],_,_) ⇒ {}
            | _ ⇒ ⊥
        )"
      | "\<aC>⋅cstate = (case undiscr cstate of
             (App lab f vs,β,ve,b) ⇒
                 let fs = \<aA> f β ve;
                     as = map (λv. \<aA> v β ve) vs;
                     b' = \<anb> b lab
                  in (⋃f' ∈ fs. \<aF>⋅(Discr (f',as,ve,b')))
                     ∪{((lab, β),f') | f' . f'∈ fs}
            | (Let lab ls c',β,ve,b) ⇒
                 let b' = \<anb> b lab;
                     β' = β (lab ↦ b');
                     ve' = ve ∪. (⋃. (map (λ(v,l). {(v,b') := (\<aA> (L l) β' ve)}.) ls))
                 in \<aC>⋅(Discr (c',β',ve',b'))
        )"

text ‹
Again, we name the cases of the induction rule and build a nicer case analysis rule for arguments of type ‹\<afstate>›.
›

lemmas a_evalF_evalC_induct = a_evalF_a_evalC.induct[case_names Admissibility Bottom Next]

fun a_evalF_cases
 where "a_evalF_cases (PC (Lambda lab vs c, β)) as ve b = undefined"
     | "a_evalF_cases (PP (Plus cp)) [a1, a2, cnt] ve b = undefined"
     | "a_evalF_cases (PP (prim.If cp1 cp2)) [v,cntt,cntf] ve b = undefined"
     | "a_evalF_cases AStop [v] ve b = undefined"

lemmas a_fstate_case_x = a_evalF_cases.cases[
  OF case_split, of _ "λ_ vs _ _ as _ _ . length vs = length as",
  case_names "Closure" "Closure_inv" "Plus" "If" "Stop"]

lemmas a_cl_cases = prod.exhaust[OF lambda.exhaust, of _ "λ a _ . a"]
lemmas a_ds_cases = list.exhaust[
  OF _ list.exhaust,  of _ _ "λ_ x. x",
  OF _ _ list.exhaust  ,of _ _ "λ_ _ _ x. x" , 
  OF _ _ _ list.exhaust,of _ _ "λ_ _ _ _ _ x. x"
  ] 
lemmas a_ds_cases_stop = list.exhaust[OF _ list.exhaust, of _ _ "λ_ x. x"]
lemmas a_fstate_case = prod_cases4[OF proc.exhaust, of _ "λx _ _ _ . x",
  OF a_cl_cases prim.exhaust, of _ "λ _ _ _ _ a . a" _ "λ _ _ _ _ a. a",
  OF case_split a_ds_cases a_ds_cases a_ds_cases_stop,
  of _ "λ_ as _ _ _ _ _ _ vs _ . length vs = length as" _ "λ _ ds _ _ _ _ . ds" "λ _ ds _ _ _ _ _. ds" "λ _ ds _ _. ds"]

text ‹
Not surprisingly, the abstract semantics of a whole program is defined using ‹\<aF>› with suitably initialized arguments. The function ‹the_elem› extracts a value from a singleton set. This works because we know that ‹\<aA>› returns such a set when given a lambda expression.
›

definition evalCPS_a :: "prog ⇒ ('c::contour) \<aans>" (‹\<aPR>›)
  where "\<aPR> l = (let ve = {}.;
                          β = Map.empty;
                          f = \<aA> (L l) β ve
                      in  \<aF>⋅(Discr (the_elem f,[{AStop}],ve,\<abinit>)))"

end