Handlers.ott

embed {{ coq Require String.  Require Import ott_list. }}
embed {{ coq-lib list_mem list_minus }}

metavar termvar, x, p, k ::=
  {{ ocaml string }} {{ isa string }} {{ isavar ''[[termvar]]'' }}
  {{ coq String.string }} {{ lex alphanum }}

% careful now, Isabelle 2011 doesn't seem to like op as the type name
metavar oper ::= 
  {{ ocaml string }} {{ isa string }} {{ isavar ''[[oper]]'' }}
  {{ coq String.string }} {{ lex alphanum }}

embed {{ coq
  Definition eq_termvar := String.string_dec.
  Definition eq_oper := String.string_dec.
}}

% Can I use numbers for left/right?

% Something bad is happening with the substitution function generation for
% Isabelle - when I union binders (or even if I give them separately) it
% generates x : set [y] @ [z] (for y,z bound), but I need to add parentheses
% for Isabelle 2011 to accept it.

grammar
value, v :: 'v_' ::=  {{ com values }}
  | x           :: :: Var
  | ()          :: :: Unit
  | ( v1 , v2 ) :: :: Pair
  | inl v       :: :: InL
  | inr v       :: :: InR
  | { m }       :: :: Thunk
%  | ( v )       ::S:: ParenV

compt, m :: 'm_' ::=  {{ com computations }}
  | split ( v , x1 , x2 , m )      ::  :: PairElim (+ bind x1 union x2 in m +)
  | case0 ( v )                    ::  :: NilElim
% Should be x1.m1?
  | case ( v , x1 , m1 , x2 , m2 ) ::  :: SumElim (+ bind x1 in m1 bind x2 in m2 +)
  | v !                            ::  :: Force
  | return v                       ::  :: Return
  | let x <- m in m'               ::  :: Let (+ bind x in m' +)
  | \ x . m                        ::  :: Lambda (+ bind x in m +)
  | m v                            ::  :: App
  | < >                            ::  :: Unit
  | < m1 , m2 >                    ::  :: CPair
  | prjl m                         ::  :: ProjL
  | prjr m                         ::  :: ProjR
  | oper v ( \ x . m )             ::  :: Op (+ bind x in m +)
  | handle m with h                ::  :: Handle
  | ( m )                          :: S:: ParenS   {{ icho [[m]] }}
  | m [ v / x ]                    :: M:: Msub
      {{ icho (subst_compt [[v]] [[x]] [[m]]) }}
  | H . m                          :: M:: MctxH
      {{ icho (appctx_hoisting_frame_compt [[H]] [[m]]) }}
      {{ tex [[H]][m] }}
  | CC . m                         :: M:: MctxC
      {{ icho (appctx_compt_frame_compt [[CC]] [[m]]) }}
      {{ tex [[CC]][m] }}

% Can I make it a proper set rather than a list?
handlers, h :: 'h_' ::=  {{ com handlers }}
  | { return x -> m }       ::  :: Return (+ bind x in m +)
  | h + { oper p k -> m }   ::  :: Handler (+ bind p union k in m +)

% I wanted mathcal H here, but it'll try to format hoisting_frame in that, too,
% which it doesn't have symbols for.

hoisting_frame, H :: 'H_' ::=
  | let x <- __ in m  :: :: Let (+ bind x in m +)
  | __ v              :: :: App
  | prjl __           :: :: ProjL
  | prjr __           :: :: ProjR

% Can I avoid duplicating H?
compt_frame, CC :: 'CC_' ::=
  | let x <- __ in m  :: :: Let (+ bind x in m +)
  | __ v              :: :: App
  | prjl __           :: :: ProjL
  | prjr __           :: :: ProjR
  | handle __ with h  :: :: Handle

terminals :: 'terminals_' ::=
  | \         :: :: lambda  {{ tex \lambda }}
  | ->        :: :: rarr    {{ tex \rightarrow }}
  | <-        :: :: larr    {{ tex \leftarrow }}
  | -->       :: :: red     {{ tex \longrightarrow }}
  | case0     :: :: case0   {{ tex \ottkw{case_0} }}
  | <         :: :: lang    {{ tex \langle }}
  | >         :: :: rang    {{ tex \rangle }}
  | <>        :: :: neq     {{ tex \neq }}
  | |-        :: :: turnst  {{ tex \vdash }}
  | =>        :: :: RArr    {{ tex \Rightarrow }}

formula :: formula_ ::=
  | judgement ::  :: judgement
  | x in fv ( H ) :: M :: infv
      {{ coq In x (fv_hoisting_frame [[H]]) }}
      {{ isa x : set (fv_hoisting_frame [[H]]) }}
      {{ tex [[x]] \in \text{fv}([[H]]) }}
  | x in fv ( h ) :: M :: infvh
      {{ coq In x (fv_handlers [[h]]) }}
      {{ isa x : set (fv_handlers [[h]]) }}
      {{ tex [[x]] \in \text{fv}([[h]]) }}
  | x not in fv ( H ) :: M :: notinfv
      {{ coq not (In x (fv_hoisting_frame [[H]])) }}
      {{ isa \<not> (x : set (fv_hoisting_frame [[H]])) }}
      {{ tex [[x]] \not\in \text{fv}([[H]]) }}
  | x not in fv ( h ) :: M :: notinfvh
      {{ coq not (In x (fv_handlers [[h]])) }}
      {{ isa \<not> (x : set (fv_handlers [[h]])) }}
      {{ tex [[x]] \not\in \text{fv}([[h]]) }}
  | x <> x' :: M :: termvarne
      {{ coq [[x]] <> [[x']] }}
      {{ isa [[x]] \<noteq> [[x']] }}
  | oper <> oper' :: M :: operne
      {{ coq [[oper]] <> [[oper']] }}
      {{ isa [[oper]] \<noteq> [[oper']] }}

contextrules
  H _:: m :: m
  CC _:: m :: m

% Same problem as freevars - need to ask for v x to get m x
substitutions
  single v x :: subst

% Seems that you have to mention the non-terminal that x appears in to
% generate the free variables functions, even if you want one further out
% (i.e., I want a function for H, but need to ask for one for v)
freevars
  v x :: fv
  m x :: fv
  H x :: fv
  h x :: fv

% Don't try to use "funs" to give you definitions for terms unless you add a
% throwaway parameter - it'll generate bad output.

defns
ProjReturn :: '' ::=

 defn
 h Returns \ x . m :: ::hreturns::''
   {{ tex [[h]]^{\text{\bf return} } = \lambda [[x]].[[m]] }} by

   ------------------------------- :: hReturns1
   { return x -> m } Returns \x. m

   h Returns \x. m
   ---------------------------------- :: hReturns2
   h + {oper p k -> m'} Returns \x. m

defns
ProjOp :: '' ::=

 defn
 h For oper \ p k . m :: ::hfor::''
   {{ tex [[h]]^{[[oper]]} = \lambda [[p]]\,[[k]].[[m]] }} by

   ------------------------------------ :: hFor1
   h + {oper p k -> m} For oper \p k. m

   oper <> oper'
   h For oper \p k. m
   ---------------------------------------- :: hFor2
   h + {oper' p' k' -> m'} For oper \p k. m

defns
Jop :: '' ::=

 defn
 m --> m' :: ::reduce::'' by

   ------------------------------------------ :: betatimes
   split((v1,v2),x1,x2,m) --> m[v1/x1][v2/x2]

   ------------------------------------ :: betaplusl
   case(inl v,x1,m1,x2,m2) --> m1[v/x1]

   ------------------------------------ :: betaplusr
   case(inr v,x1,m1,x2,m2) --> m2[v/x2]

   ---------- :: betaU
   {m}! --> m

   --------------------------------- :: betaF
   let x <- return v in m --> m[v/x]

   ------------------- :: betaApp
   (\x.m) v --> m[v/x]

   ------------------- :: betaAmpL
   prjl <m1,m2> --> m1

   ------------------- :: betaAmpR
   prjr <m1,m2> --> m2

% I hoped I could drop the free variable restriction, but the frame rule means
% that we're not necessarily dealing with closed terms
% e.g.   let x <- handle let y <- oper v (\x.x) in x with h in m
%       -/-> let x <- handle oper v (\x. let y <- x in x) with h in m
   x not in fv(H)
   ------------------------------------- :: hoistop
   H.(oper v (\x.m)) --> oper v (\x.H.m)

   h Returns \x. m
   ----------------------------------- :: handleF
   handle (return v) with h --> m[v/x]

   x not in fv(h)
   h For oper \p k. m'
   ---------------------------------------------------------------- :: handleOp
   handle oper v (\x. m) with h --> m'[v/p][{\x.handle m with h}/k]

   m --> m'
   -------------- :: frame
   CC.m --> CC.m'

% Cases in which reduction can get stuck due to a lack of alpha conversion.

defns
  Needs_alpha_conv :: '' ::=
defn needs_alpha_conv m :: ::needs_alpha_conv::'AC_'
  {{ tex \text{needs\_alpha\_conv}\ [[m]] }} by

   x in fv(H)
   ------------------------------------- :: hoistop
   needs_alpha_conv H.(oper v (\x.m))

   x in fv(h)
   ---------------------------------------------------------------- :: handleOp
   needs_alpha_conv handle oper v (\x. m) with h

   needs_alpha_conv m
   --------------------- :: frame
   needs_alpha_conv CC.m