theory a2
  imports Main
begin

datatype val =
  Boolv bool | Intv int

datatype exp =
  Bool bool
  | Integer int
  | Var string
  | Add exp exp
  | And exp exp
  | Le exp exp

primrec eval :: "exp \<Rightarrow> val option" where
  "eval (Bool b) = Some(Boolv b)"
| "eval (Integer i) = Some(Intv i)"
| "eval (Var x) = None"
| "eval (Add e1 e2) =
   (case eval e1 of
      Some(Intv i1) \<Rightarrow>
      (case eval e2 of
         Some(Intv i2) \<Rightarrow> Some(Intv(i1 + i2))
       | _ \<Rightarrow> None)
    | _ \<Rightarrow> None
   )"
| "eval (And e1 e2) =
   (case eval e1 of
      Some(Boolv False) \<Rightarrow> Some(Boolv False)
    | Some(Boolv True) \<Rightarrow>
      (case eval e2 of
        Some(Boolv b2) \<Rightarrow> Some(Boolv b2)
       | _ \<Rightarrow> None)
    | _ \<Rightarrow> None
   )"
| "eval (Le e1 e2) =
   (case eval e1 of
      Some(Intv i1) \<Rightarrow>
      (case eval e2 of
         Some(Intv i2) \<Rightarrow> Some(Boolv(i1 \<le> i2))
       | _ \<Rightarrow> None)
    | _ \<Rightarrow> None
   )"

primrec subst_exp :: "exp \<Rightarrow> string \<Rightarrow> val \<Rightarrow> exp" where
  "subst_exp (Bool b) x e = Bool b"
| "subst_exp (Integer i) x e = Integer i"
| "subst_exp (Var y) x e =
   (if x = y then
      (case e of
           Boolv b \<Rightarrow> Bool b
         | Intv  n \<Rightarrow> Integer n)
    else Var y)"
| "subst_exp (Add e1 e2) x e =
   Add (subst_exp e1 x e) (subst_exp e2 x e)"
| "subst_exp (And e1 e2) x e =
   And (subst_exp e1 x e) (subst_exp e2 x e)"
| "subst_exp (Le e1 e2) x e =
   Le (subst_exp e1 x e) (subst_exp e2 x e)"

primrec vars :: "exp \<Rightarrow> string set" where
  "vars (Bool b) = {}"
| "vars (Integer i) = {}"
| "vars (Var y) = {y}"
| "vars (Add e1 e2) = (vars e1 \<union> vars e2)"
| "vars (And e1 e2) = (vars e1 \<union> vars e2)"
| "vars (Le e1 e2) = (vars e1 \<union> vars e2)"

section "Q1. Expressions and Types (28 marks)"

lemma subst_not_free:
  "\<lbrakk>x \<notin> vars e\<rbrakk> \<Longrightarrow> subst_exp e x d = e"
  oops

lemma subst_fresh:
  "x \<notin> vars(subst_exp e x v)"
  oops

lemma subst_commute:
  "x \<noteq> y \<Longrightarrow> subst_exp (subst_exp e x v) y v' = subst_exp (subst_exp e y v') x v"
  oops

lemma subst_idem:
  "subst_exp (subst_exp e x v) x v' = subst_exp e x v"
  oops

datatype vtype = BoolT | IntT

inductive type_exp :: "(string \<rightharpoonup> vtype) \<Rightarrow> exp \<Rightarrow> vtype \<Rightarrow> bool" where
  "type_exp \<Gamma> (Bool b) BoolT"
| "type_exp \<Gamma> (Integer i) IntT"
|  "\<Gamma> x = Some ty \<Longrightarrow> type_exp \<Gamma> (Var x) ty"
| "\<lbrakk>type_exp \<Gamma> e1 IntT; type_exp \<Gamma> e2 IntT\<rbrakk> \<Longrightarrow> type_exp \<Gamma> (Add e1 e2) IntT"
| "\<lbrakk>type_exp \<Gamma> e1 BoolT; type_exp \<Gamma> e2 BoolT\<rbrakk> \<Longrightarrow> type_exp \<Gamma> (And e1 e2) BoolT"
| "\<lbrakk>type_exp \<Gamma> e1 IntT; type_exp \<Gamma> e2 IntT\<rbrakk> \<Longrightarrow> type_exp \<Gamma> (Le e1 e2) BoolT"

primrec type_v :: "val \<Rightarrow> vtype" where 
  "type_v (Boolv b) = BoolT" 
| "type_v (Intv t) = IntT"

lemma type_exp_subst:
  assumes "type_exp \<Gamma> e ty"
      and "\<Gamma> x = Some(type_v v)"
    shows "type_exp \<Gamma> (subst_exp e x v) ty"
 oops

lemma type_exp_drop:
  assumes "type_exp \<Gamma> e ty"
      and "x \<notin> vars e"
    shows "type_exp (\<Gamma>(x := t)) e ty"
  oops

lemma type_exp_subst':
  assumes "type_exp (\<Gamma>(x \<mapsto> type_v v)) e ty"
    shows "type_exp \<Gamma> (subst_exp e x v) ty"
  oops

lemma type_exp_eval:
  shows "type_exp Map.empty e ty \<Longrightarrow> \<exists>v. eval e = Some v \<and> type_v v = ty"
  oops

text \<open>
Is it the case that every expression that evaluates successfully has a type? 
i.e., is the following true: \<close>

term  "eval e = Some v \<Longrightarrow> type_exp Map.empty e (type_v v)"

text \<open> If you answer yes, explain why (informally). 
   If you answer no, give a counterexample. (4 marks)
\<close>

text \<open>
Your answer including an explanation or a counterexample.

\<close>

section "Q2. Processes and Session Types (29 marks)"

datatype process =
   Done
   | Send exp process
   | Receive string process
   | IfThen exp process process
   | ExtChoice process process

primrec subst_proc :: "process \<Rightarrow> char list \<Rightarrow> val \<Rightarrow> process" where
  "subst_proc Done x e = Done"
| "subst_proc (Send exp p) x e =
   Send (subst_exp exp x e) (subst_proc p x e)"
| "subst_proc (Receive y p) x e =
   (if x = y then
      Receive y p
    else
      Receive y (subst_proc p x e))
  "
| "subst_proc (IfThen exp p q) x e =
   IfThen (subst_exp exp x e) (subst_proc p x e) (subst_proc q x e)
  "
| "subst_proc (ExtChoice p q) x e =
   ExtChoice (subst_proc p x e) (subst_proc q x e)
  "

primrec varsp :: "process \<Rightarrow> string set" where
  "varsp Done = {}"
| "varsp (Send exp e) = (vars exp \<union> varsp e)"
| "varsp (Receive s e) = (varsp e \<union> {s})"
| "varsp (IfThen exp e1 e2) =
   (vars exp \<union> varsp e1 \<union> varsp e2)"
| "varsp (ExtChoice e1 e2) =
   (varsp e1 \<union> varsp e2)"

inductive semantics :: "process \<times> process \<Rightarrow> process \<times> process \<Rightarrow> bool" where
   com_l:
   "\<lbrakk>eval exp = Some d; q' = (subst_proc q x d)\<rbrakk> \<Longrightarrow>
     semantics (Send exp p,Receive x q) (p, q')"
 | com_r:
   "\<lbrakk>eval exp = Some d; p' = (subst_proc p x d)\<rbrakk> \<Longrightarrow>
     semantics (Receive x p,Send exp q) (p', q)"
 | choice_l:
   "\<lbrakk>eval exp = Some(Boolv b); 
     p' = (if b then p else q); 
     q' = (if b then r else s)\<rbrakk> \<Longrightarrow>
     semantics (IfThen exp p q, ExtChoice r s) (p', q')"
 | choice_r:
   "\<lbrakk>eval exp = Some(Boolv b); 
     p' = (if b then p else q); 
     q' = (if b then r else s)\<rbrakk> \<Longrightarrow>
     semantics (ExtChoice p q,IfThen exp r s) (p', q')"


text \<open>Consider a pair of processes: one that sends the integer 5 and
        then successfully terminates, and another that receives a message
        and then successfully terminates.
        Formulate and prove a lemma stating that the @{term semantics} relates
        this pair of processes to a pair of successfully terminated processes. \<close>

lemma example1:
  "first example"
  oops

text \<open>Consider another pair of processes:
        one waits for an external choice, and then terminates regardless of
        branch choice. Another chooses a branch based on the value of a boolean expression,
        then terminates regardless of branch choice.
        Formulate and prove a lemma 
        stating that the @{term semantics} relates
        this pair of processes to a pair of successfully terminated processes. \<close>

lemma example2:
  "second example"
oops


datatype stype = 
  DoneT
  | SendT vtype stype
  | ReceiveT vtype stype
  | IntChoiceT stype stype
  | ExtChoiceT stype stype

inductive type_proc :: "(string \<rightharpoonup> vtype) \<Rightarrow> process \<Rightarrow> stype \<Rightarrow> bool" where
  "type_proc \<Gamma> Done DoneT"
| "\<lbrakk>type_exp \<Gamma> exp vty; type_proc \<Gamma> e ety\<rbrakk> \<Longrightarrow>
   type_proc \<Gamma> (Send exp e) (SendT vty ety)"
| "\<lbrakk>type_proc (\<Gamma>(x := Some vty)) e ety\<rbrakk> \<Longrightarrow>
   type_proc \<Gamma> (Receive x e) (ReceiveT vty ety)"
| "\<lbrakk>type_exp \<Gamma> exp BoolT;
    type_proc \<Gamma> e ety;
    type_proc \<Gamma> e' ety'\<rbrakk> \<Longrightarrow>
   type_proc \<Gamma> (IfThen exp e e') (IntChoiceT ety ety')"
| "\<lbrakk>type_proc \<Gamma> e ety;
    type_proc \<Gamma> e' ety'\<rbrakk> \<Longrightarrow>
   type_proc \<Gamma> (ExtChoice e e') (IntChoiceT ety ety')"

text \<open> Formulate and prove a lemma listing a type and typing environment under which the process that 
        sends the integer 5 then directly terminates (from question 2a) is well-typed through the @{term type_proc} 
        typing relation. \<close>

lemma example_type:
  "type example"
  oops

lemma type_proc_subst':
  assumes "type_proc (\<Gamma>(x \<mapsto> type_v v)) e ty"
      shows "type_proc \<Gamma> (subst_proc e x v) ty"
  oops

lemma type_proc_drop:
  assumes "type_proc \<Gamma> p ty"
      and "x \<notin> varsp p"
    shows "type_proc (\<Gamma>(x := t)) p ty"
  oops
  
primrec dual :: "stype \<Rightarrow> stype" where
  "dual DoneT = DoneT"
| "dual (SendT vt et) = ReceiveT vt (dual et)"
| "dual (ReceiveT vt et) = SendT vt (dual et)"
| "dual (IntChoiceT et et') = ExtChoiceT (dual et) (dual et')"
| "dual (ExtChoiceT et et') = IntChoiceT (dual et) (dual et')"

lemma dual_dual:
  "dual(dual t) = t"
  oops

lemma progress:
  assumes "type_proc Map.empty p ty"
      and "type_proc Map.empty q (dual ty)"
      and "p \<noteq> Done"
    shows "\<exists>r s. semantics (p,q) (r,s)"
  oops

primrec reduce :: "stype \<Rightarrow> stype set" where
  "reduce DoneT = {DoneT}"
| "reduce (SendT vt et) = {et}"
| "reduce (ReceiveT vt et) = {et}"
| "reduce (IntChoiceT et et') = {et, et'}"
| "reduce (ExtChoiceT et et') = {et, et'}"

lemma subject_reduction:
  assumes "semantics (p,q) (r,s)"
      and "type_proc Map.empty p ty"
      and "type_proc Map.empty q (dual ty)"
    shows "\<exists>ty'. ty' \<in> reduce ty \<and> type_proc Map.empty r ty' \<and> type_proc Map.empty s (dual ty')"
  oops

section "Q3. Compiling Internal Choice (43 marks)"


inductive semantics' :: "process \<times> process \<Rightarrow> process \<times> process \<Rightarrow> bool" where
   com_l':
   "\<lbrakk>eval exp = Some d\<rbrakk> \<Longrightarrow>
     semantics' (Send exp p,Receive x q) (p, subst_proc q x d)"
 | com_r':
   "\<lbrakk>eval exp = Some d\<rbrakk> \<Longrightarrow>
     semantics' (Receive x p,Send exp q) (subst_proc p x d, q)"
 | if_l':
   "\<lbrakk>eval exp = Some(Boolv b)\<rbrakk> \<Longrightarrow>
     semantics' (IfThen exp p q,r) (if b then p else q, r)"
 | if_r':
   "\<lbrakk>eval exp = Some(Boolv b)\<rbrakk> \<Longrightarrow>
     semantics' (p, IfThen exp q r) (p, if b then q else r)"

primrec compile :: "process \<Rightarrow> process" where
  "compile(Done) = Done"
| "compile(Send exp p) = Send exp (compile p)"
| "compile(Receive x p) = Receive x (compile p)"
| "compile(IfThen s p q) =
   IfThen s
     (Send (Bool True) (compile p))
     (Send (Bool False) (compile q))"
| "compile(ExtChoice p q) =
   Receive ''x''
     (IfThen (Var ''x'') (compile p) (compile q))"

lemma semantics_pres:
  assumes "semantics (p,q) (r,s)"
      and "''x'' \<notin> varsp p"
      and "''x'' \<notin> varsp q"
  shows "semantics'\<^sup>*\<^sup>* (compile p, compile q) (compile r, compile s)"
  oops

text \<open> Explain why the side-conditions @{term "''x'' \<notin> varsp p"}
      on the aforementioned theorem are necessary.\<close>

text \<open> Your answer \<close>

text \<open> What changes to the @{term "compile"} function would be necessary to
      make the theorem hold without the side condition?
      Define an alternative @{term "compile'"} by uncommenting and completing the following. \<close>  

(*
primrec compile' :: process \<Rightarrow> process where
  "compile' ..."
*)

text \<open> Explain why it solves the problem. You do not have to prove it correct.\<close>

text \<open>Your answer \<close>


end