Theory DeclSemAsNDInterpFSet

section "Declarative semantics as a non-deterministic interpreter"
  
theory DeclSemAsNDInterpFSet
  imports Lambda ValuesFSet
begin
  
subsection "Non-determinism monad"

type_synonym 'a M = "'a set"

definition set_bind :: "'a M ⇒ ('a ⇒ 'b M) ⇒ 'b M" where
  "set_bind m f ≡ { v. ∃ v'. v' ∈ m ∧ v ∈ f v' }"
declare set_bind_def[simp]

syntax "_set_bind" :: "[pttrns,'a M,'b] ⇒ 'c" (‹(_ ← _;//_)› 0)
syntax_consts "_set_bind" ⇌ set_bind
translations "P ← E; F" ⇌ "CONST set_bind E (λP. F)"

definition return :: "'a ⇒ 'a M" where
  "return v ≡ {v}"
declare return_def[simp]

definition zero :: "'a M" where
  "zero ≡ {}"
declare zero_def[simp]

no_notation "binomial" (infix ‹choose› 64)

definition choose :: "'a set ⇒ 'a M" where
  "choose S ≡ S"
declare choose_def[simp]
 
definition down :: "val ⇒ val M" where
  "down v ≡ (v' ← UNIV; if v' ⊑ v then return v' else zero)"
declare down_def[simp]

definition mapM :: "'a fset ⇒ ('a ⇒ 'b M) ⇒ ('b fset) M" where
  "mapM as f ≡ ffold (λa. λr. (b ← f a; bs ← r; return (finsert b bs))) (return ({||})) as"
  
subsection "Non-deterministic interpreter"

abbreviation apply_fun :: "val M ⇒ val M ⇒ val M" where
  "apply_fun V1 V2 ≡ (v1 ← V1; v2 ← V2;
                       case v1 of VFun f ⇒ 
                          (v2',v3') ← choose (fset f);
                          if v2' ⊑ v2 then return v3' else zero
                       | _ ⇒ zero)"

fun E :: "exp ⇒ env ⇒ val set" where
  Enat2: "E (ENat n) ρ = return (VNat n)" |
  Evar2: "E (EVar x) ρ = (case lookup ρ x of None ⇒ zero | Some v ⇒ down v)" |
  Elam2: "E (ELam x e) ρ = (vs ← choose UNIV; 
                           t ← mapM vs (λ v. (v' ← E e ((x,v)#ρ); return (v, v')));
                           return (VFun t))" |
  Eapp2: "E (EApp e1 e2) ρ = apply_fun (E e1 ρ) (E e2 ρ)" |
  Eprim2: "E (EPrim f e1 e2) ρ = (v⇩1 ← E e1 ρ; v⇩2 ← E e2 ρ;
                                 case (v⇩1,v⇩2) of
                                   (VNat n⇩1, VNat n⇩2) ⇒ return (VNat (f n⇩1 n⇩2))
                                | (VNat n⇩1, VFun t⇩2) ⇒ zero
                                | (VFun t⇩1, v⇩2) ⇒ zero)" |
  Eif2[eta_contract = false]: "E (EIf e1 e2 e3) ρ = (v⇩1 ← E e1 ρ;
                              case v⇩1 of
                                (VNat n) ⇒ if n ≠ 0 then E e2 ρ else E e3 ρ
                              | (VFun t) ⇒ zero)"

end