%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Dynamic semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % The definitions in this file do *not* strictly correspond to any specific % code in GHC. They are here to provide a reasonable operational semantic % interpretation to the typing rules presented in the other ott files. Thus, % your mileage may vary. In particular, there has been *no* attempt to % write any formal proofs over these semantics. % % With that disclaimer disclaimed, these rules are a reasonable jumping-off % point for an analysis of FC's operational semantics. If you don't want to % worry about mutual recursion (and who does?), you can even drop the % environment S. % % Join points are ignored here because operationally they work exactly the same % as regular bindings. Simply read "join" as "let" and "jump" as application to % see how a (well-typed!) program should run. grammar defns OpSem :: '' ::= defn e --> e' :: :: step :: 'S_' {{ com Single step semantics }} {{ tex \begin{array}{l} [[e]] [[-->]] [[e']] \end{array} }} by e1 --> e1' ------------------- :: App e1 e2 --> e1' e2 ----------------------------- :: Beta (\n.e1) e2 --> e1[n |-> e2] % g : (t1 -> t2) ~Rep# (t3 -> t4) % e2 : t3 % g0 : t3 ~Rep# t1 % g1 : t2 ~Rep# t4 g0 = sym (nth Rep 2 g) g1 = nth Rep 3 g not e2 is_a_type not e2 is_a_coercion ----------------------------------------------- :: Push ((\n.e1) |> g) e2 --> (\n.e1 |> g1) (e2 |> g0) % g : (forall (a : k1). t1) ~Rep# (forall (a : k2). t2) % t : k2 % g' : k2 ~# k1 % t' : k1 g' = sym (nth Nom 0 g) t' = t |> g' -------------------------------------------------------- :: TPush ((\n.e) |> g) t --> ((\n.e) t') |> (g @ (sym Nom MCo g')) % g : ((t1 ~rho# t2) -> t3) ~Rep# ((t4 ~rho# t5) -> t6) % g2 : t3 ~Rep# t6 % g' : t4 ~rho# t5 % g0 : t1 ~rho# t4 % g1 : t5 ~rho# t2 % recall that (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> Type % and that (~#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[]) % so pulling out the first visible argument for both is argument 2, % and the second visible argument for both is argument 3 R = coercionRole g' g0 = nth R 2 (nth Rep 2 g) g1 = sym (nth R 3 (nth Rep 2 g)) g2 = nth Rep 3 g ------------------------------- :: CPush ((\n.e) |> g) g' --> (\n.e |> g2) (g0 ; g' ; g1) --------------------------------------- :: Trans (e |> g1) |> g2 --> e |> (g1 ; g2) e --> e' ------------------------ :: Cast e |> g --> e' |> g e --> e' ------------------------------ :: Tick e { tick } --> e' { tick } e --> e' --------------------------------------- :: Case case e as n return t of --> case e' as n return t of altj = K -> u e = K u' = u[n |-> e] sbb] // bb /> ecc] // cc /> -------------------------------------------------------------- :: MatchData case e as n return t of --> u' altj = lit -> u ---------------------------------------------------------------- :: MatchLit case lit as n return t of --> u[n |-> lit] altj = _ -> u no other case matches ------------------------------------------------------------ :: MatchDefault case e as n return t of --> u[n |-> e] T k'~Rep# k T = coercionKind g = tyConRoles T forall . forall . $ -> T = dataConRepType K (t1cc $ nth Raa aa g] // aa /> ] // bb />) // cc /> --------------------------- :: CasePush case (K ) |> g as n return t2 of --> \\ case K as n return t2 of ----------------- :: LetNonRec let n = e1 in e2 --> e2[n |-> e1] ------------------------------------ :: LetRec let rec in u --> u let rec in ei ] // i />