Theory Eval

section "Standard semantics"

theory Eval
  imports HOLCF HOLCFUtils CPSScheme
begin

text ‹
We begin by giving the standard semantics for our language. Although this is not actually used to show any results, it is helpful to see that the later algorithms ``look similar'' to the evaluation code and the relation between calls done during evaluation and calls recorded by the control flow graph.
›

text ‹
We follow the definition in Figure 3.1 and 3.2 of Shivers' dissertation, with the clarifications from Section 4.1. As explained previously, our set of values encompasses just the integers, there is no separate value for \textit{false}. Also, values and procedures are not distinguished by the type system.

Due to recursion, one variable can have more than one currently valid binding, and due to closures all bindings can possibly be accessed. A simple call stack is therefore not sufficient. Instead we have a \textit{contour counter}, which is increased in each evaluation step. It can also be thought of as a time counter. The variable environment maps tuples of variables and contour counter to values, thus allowing a variable to have more than one active binding.  A contour environment lists the currently visible binding for each binding position and is preserved when a lambda expression is turned into a closure.
›

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

text ‹
The set of semantic values consist of the integers, closures, primitive operations and a special value ‹Stop›. This is passed as an argument to the program and represents the terminal continuation. When this value occurs in the first position of a call, the program terminates.
›

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

type_synonym venv = "var × contour ⇀ d"

text ‹
The function ‹𝒜› evaluates a syntactic value into a semantic datum. Constants and primitive operations are left untouched. Variable references are resolved in two stages: First the current binding contour is fetched from the binding environment ‹β›, then the stored value is fetched from the variable environment ‹ve›. A lambda expression is bundled with the current contour environment to form a closure.
›

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))"
  |     "𝒜 (L lam) β ve = DC (lam, β)"


text ‹
The answer domain of our semantics is the set of integers, lifted to obtain an additional element denoting bottom. Shivers distinguishes runtime errors from non-termination. Here, both are represented by ‹⊥›.
›

type_synonym ans = "int lift"

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 ‹
As usual, the semantics of a functional language is given as a denotational semantics. To that end, two functions are defined here: ‹ℱ› applies a procedure to a list of arguments. Here closures are unwrapped, the primitive operations are implemented and the terminal continuation ‹Stop› is handled. ‹𝒞› evaluates a call expression, either by evaluating procedure and arguments and passing them to ‹ℱ›, or by adding the bindings of a ‹Let› expression to the environment.

Note how the contour counter is incremented before each call to ‹ℱ› or when a ‹Let› expression is evaluated.

With mutually recursive equations, such as those given here, the existence of a function satisfying these is not obvious. Therefore, the ‹fixrec› command from the @{theory HOLCF} package is used. This takes a set of equations and builds a functional from that. It mechanically proofs that this functional is continuous and thus a least fixed point exists. This is then used to define ‹ℱ› and ‹𝒞› and proof the equations given here. To use the @{theory HOLCF} setup, the continuous function arrow ‹→› with application operator ‹⋅› is used and our types are wrapped in ‹discr› and ‹lift› to indicate which partial order is to be used.
›

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 "evalF⋅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) ⇒
                     let b' = Suc b;
                         β  = [c ↦ b]
                     in ℱ⋅(Discr (cnt,[DI (a1 + a2)],ve,b'))
            | (DP (prim.If ct cf),[DI v, contt, contf],ve,b) ⇒
                  (if v ≠ 0
                   then let b' = Suc b;
                            β = [ct ↦ b]
                        in ℱ⋅(Discr (contt,[],ve,b'))
                   else let b' = Suc b;
                            β = [cf ↦ b]
                        in ℱ⋅(Discr (contf,[],ve,b')))
            | (Stop,[DI i],_,_) ⇒ Def i
            | _ ⇒ ⊥
        )"
      | "𝒞⋅cstate = (case undiscr cstate of
             (App lab f vs,β,ve,b) ⇒
                 let f' = 𝒜 f β ve;
                     as = map (λv. 𝒜 v β ve) vs;
                     b' = Suc b
                  in ℱ⋅(Discr (f',as,ve,b'))
            | (Let lab ls c',β,ve,b) ⇒
                 let b' = Suc b;
                     β' = β (lab ↦ b');
                    ve' = ve ++ map_of (map (λ(v,l). ((v,b'), 𝒜 (L l) β' ve)) ls)
                 in 𝒞⋅(Discr (c',β',ve',b'))
        )"

text ‹
To evaluate a full program, it is passed to ‹ℱ› with proper initializations of the other arguments. We test our semantics function against two example programs and observe that the expected value is returned. 
›

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

lemma correct_ex1: "\<PR> ex1 = Def 0"
unfolding evalCPS_def
by simp

lemma correct_ex2: "\<PR> ex2 = Def 2"
unfolding evalCPS_def
by simp

(* (The third example takes long to finish, thus is it not ran by default.) 
lemma correct_ex3: "evalCPS ex3 = Def 55"
oops
unfolding evalCPS_def
by simp
*)

end