Theory ExCF

section "Exact nonstandard semantics"

theory ExCF
  imports HOLCF HOLCFUtils CPSScheme Utils
begin

text ‹
We now alter the standard semantics given in the previous section to calculate a control flow graph instead of the return value. At this point, we still ``run'' the program in full, so this is not yet the static analysis that we aim for. Instead, this is the reference for the correctness proof of the static analysis: If an edge is recorded here, we expect it to be found by the static analysis as well.
›

text ‹
In preparation of the correctness proof we change the type of the contour counters. Instead of plain natural numbers as in the previous sections we use lists of labels, remembering at each step which part of the program was just evaluated.

Note that for the exact semantics, this is information is not used in any way and it would have been possible to just use natural numbers again. This is reflected by the preorder instance for the contours which only look at the length of the list, but not the entries.
›

definition "contour = (UNIV::label list set)"

typedef contour = contour
  unfolding contour_def by auto

definition initial_contour ("\<binit>")
  where "\<binit> = Abs_contour []"

definition nb 
  where "nb b c = Abs_contour (c # Rep_contour b)"

instantiation contour :: preorder
begin
definition le_contour_def: "b ≤ b' ⟷ length (Rep_contour b) ≤ length (Rep_contour b')"
definition less_contour_def: "b < b' ⟷ length (Rep_contour b) < length (Rep_contour b')"
instance proof
qed(auto simp add:le_contour_def less_contour_def Rep_contour_inverse Abs_contour_inverse contour_def)
end

text ‹
Three simple lemmas helping Isabelle to automatically prove statements about contour numbers.
›

lemma nb_le_less[iff]: "nb b c ≤ b' ⟷ b < b'"
  unfolding nb_def
  by (auto simp add:le_contour_def less_contour_def Rep_contour_inverse Abs_contour_inverse contour_def)

lemma nb_less[iff]: "b' < nb b c ⟷ b' ≤ b"
  unfolding nb_def
  by (auto simp add:le_contour_def less_contour_def Rep_contour_inverse Abs_contour_inverse contour_def)

declare less_imp_le[where 'a = contour, intro]


text ‹
The other types used in our semantics functions have not changed.
›

type_synonym benv = "label ⇀ contour"
type_synonym closure = "lambda × benv"

datatype d = DI int
           | DC closure
           | DP prim
           | Stop

type_synonym venv = "var × contour ⇀ d"

text ‹
As we do not use the type system to distinguish procedural from non-procedural values, we define a predicate for that.
›

primrec isProc 
  where "isProc (DI _) = False"
      | "isProc (DC _) = True"
      | "isProc (DP _) = True"
      | "isProc Stop   = True"

text ‹
To please @{theory HOLCF}, we declare the discrete partial order for our types:
›

instantiation contour :: discrete_cpo
begin
definition [simp]: "(x::contour) ⊑ y ⟷ x = y"
instance by standard simp
end
instantiation d :: discrete_cpo begin
definition  [simp]: "(x::d) ⊑ y ⟷ x = y"
instance by standard simp
end

instantiation call :: discrete_cpo begin
definition  [simp]: "(x::call) ⊑ y ⟷ x = y"
instance by standard simp
end

text ‹
The evaluation function for values has only changed slightly: To avoid worrying about incorrect programs, we return zero when a variable lookup fails. If the labels in the program given are correct, this will not happen. Shivers makes this explicit in Section 4.1.3 by restricting the function domains to the valid programs. This is omitted here.
›


fun evalV :: "val ⇒ benv ⇒ venv ⇒ d" ("𝒜")
  where "𝒜 (C _ i) β ve = DI i"
  |     "𝒜 (P prim) β ve = DP prim"
  |     "𝒜 (R _ var) β ve =
           (case β (binder var) of
              Some l ⇒ (case ve (var,l) of Some d ⇒ d | None ⇒ DI 0)
             | None ⇒ DI 0)"
  |     "𝒜 (L lam) β ve = DC (lam, β)"


text ‹
To be able to do case analysis on the custom datatypes ‹lambda›, ‹d›, ‹call› and ‹prim› inside a function defined with ‹fixrec›, we need continuity results for them. These are all of the same shape and proven by case analysis on the discriminator.
›

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_d [simp, cont2cont]:
  assumes "⋀y. cont (λx. f1 x y)"
     and  "⋀y. cont (λx. f2 x y)"
     and  "⋀y. cont (λx. f3 x y)"
    and   "cont (λx. f4 x)"
  shows "cont (λx. case_d (f1 x) (f2 x) (f3 x) (f4 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 ‹
Now, our answer domain is not any more the integers, but rather call caches. These are represented as sets containing tuples of call sites (given by their label) and binding environments to the called value. The argument types are unaltered.

In the functions ‹ℱ› and ‹𝒞›, upon every call, a new element is added to the resulting set. The ‹STOP› continuation now ignores its argument and retuns the empty set instead. This corresponds to Figure 4.2 and 4.3 in Shivers' dissertation.
›

type_synonym ccache = "((label × benv) × d) set"
type_synonym ans = ccache

type_synonym fstate = "(d × d list × venv × contour)"
type_synonym cstate = "(call × benv × venv × contour)"


fixrec   evalF :: "fstate discr → ans" ("ℱ")
     and evalC :: "cstate discr → ans" ("𝒞")
  where "ℱ⋅fstate = (case undiscr fstate of
             (DC (Lambda lab vs c, β), as, ve, b) ⇒
               (if length vs = length as
                then let β' = β (lab ↦ b);
                         ve' = map_upds ve (map (λv.(v,b)) vs) as
                     in 𝒞⋅(Discr (c,β',ve',b))
                else ⊥)
            | (DP (Plus c),[DI a1, DI a2, cnt],ve,b) ⇒
                (if isProc cnt
                 then let b' = nb b c;
                          β  = [c ↦ b]
                      in ℱ⋅(Discr (cnt,[DI (a1 + a2)],ve,b'))
                        ∪ {((c, β),cnt)}
                 else ⊥)
            | (DP (prim.If ct cf),[DI v, contt, contf],ve,b) ⇒
                (if isProc contt ∧ isProc contf
                 then
                  (if v ≠ 0
                   then let b' = nb b ct;
                            β = [ct ↦ b]
                        in (ℱ⋅(Discr (contt,[],ve,b'))
                            ∪ {((ct, β),contt)})
                   else let b' = nb b cf;
                            β = [cf ↦ b]
                        in (ℱ⋅(Discr (contf,[],ve,b')))
                            ∪ {((cf, β),contf)})
                 else ⊥)
            | (Stop,[DI i],_,_) ⇒ {}
            | _ ⇒ ⊥
        )"
      | "𝒞⋅cstate = (case undiscr cstate of
             (App lab f vs,β,ve,b) ⇒
                 let f' = 𝒜 f β ve;
                     as = map (λv. 𝒜 v β ve) vs;
                     b' = nb b lab
                  in if isProc f'
                     then ℱ⋅(Discr (f',as,ve,b')) ∪ {((lab, β),f')}
                     else ⊥
            | (Let lab ls c',β,ve,b) ⇒
                 let b' = nb b lab;
                     β' = β (lab ↦ b');
                    ve' = ve ++ map_of (map (λ(v,l). ((v,b'), 𝒜 (L l) β' ve)) ls)
                 in 𝒞⋅(Discr (c',β',ve',b'))
        )"

text ‹
In preparation of later proofs, we give the cases of the generated induction rule names and also create a large rule to deconstruct the an value of type ‹fstate› into the various cases that were used in the definition of ‹ℱ›.
›

lemmas evalF_evalC_induct = evalF_evalC.induct[case_names Admissibility Bottom Next]

lemmas cl_cases = prod.exhaust[OF lambda.exhaust, of _ "λ a _ . a"]
lemmas ds_cases_plus = list.exhaust[
  OF _ d.exhaust, of _ _ "λa _. a",
  OF _ list.exhaust, of _ _ "λ_ x _. x",
  OF _ _ d.exhaust, of _ _ "λ_ _ _ a _. a",
  OF _ _ list.exhaust,of _ _ "λ_ _ _ _ x _. x",
  OF _ _ _ list.exhaust,of _ _ "λ_ _ _ _ _ _ _ x. x"
  ]
lemmas ds_cases_if = list.exhaust[OF _ d.exhaust, of _ _ "λa _. a",
  OF _ list.exhaust[OF _ list.exhaust[OF _ list.exhaust, of _ _ "λ_ x. x"], of _ _ "λ_ x. x"], of _ _ "λ_ x _. x"]
lemmas ds_cases_stop = list.exhaust[OF _ d.exhaust, of _ _ "λa _. a",
  OF _ list.exhaust, of _ _ "λ_ x _. x"]
lemmas fstate_case = prod_cases4[OF d.exhaust, of _ "λx _ _ _ . x",
  OF _ cl_cases prim.exhaust, of _ _ "λ _ _ _ _ a . a" "λ _ _ _ _ a. a",
  OF _ case_split ds_cases_plus ds_cases_if ds_cases_stop,
  of _ _ "λ_ as _ _ _ _ _ _ vs _ . length vs = length as" "λ _ ds _ _ _ _ . ds" "λ _ ds _ _ _ _ _. ds" "λ _ ds _ _. ds",
  case_names "x" "Closure" "x" "x"  "x" "x" "Plus" "x" "x" "x" "x" "x" "x" "x" "x"   "x" "x" "If_True" "If_False" "x" "x" "x" "x" "x" "Stop"  "x" "x" "x" "x" "x"]


text ‹
The exact semantics of a program again uses ‹ℱ› with properly initialized arguments. For the first two examples, we see that the function works as expected.
›

definition evalCPS :: "prog ⇒ ans" ("\<PR>")
  where "\<PR> l = (let ve = Map.empty;
                          β = Map.empty;
                          f = 𝒜 (L l) β ve
                      in  ℱ⋅(Discr (f,[Stop],ve,\<binit>)))"

lemma correct_ex1: "\<PR> ex1 = {((2,[1 ↦ \<binit>]), Stop)}"
unfolding evalCPS_def
by simp

lemma correct_ex2: "\<PR> ex2 = {((2, [1 ↦ \<binit>]), DP (Plus 3)),
                                   ((3, [3 ↦ nb \<binit> 2]),  Stop)}"
unfolding evalCPS_def
by simp


end