| Target language of CPS transform |
Require Import List.
Require Import LambdaTamer.LambdaTamer.
Require Import CTPC.Source.
Require Import CTPC.Continuation.
Set Implicit Arguments.
Term language |
pprimop is the language of primitive operations, roughly corresponding to
atomic operations of a reasonable abstract machine.
plinear is linearized expressions, consisting of a series of bindings of
primitive operations followed by a control flow operation, either throwing to
a continuation directly or calling a function.
|
Syntax |
Inductive pprimop : list sty -> sty -> Set :=
| PVar : forall G t,
Var G t
-> pprimop G t
| PLam : forall G dom ran,
plinear (dom :: G) ran
-> pprimop G (SArrow dom ran)
| PConst : forall G, nat -> pprimop G SNat
with plinear : list sty -> sty -> Set :=
| PThrow : forall G t,
pprimop G t
-> plinear G t
| PApply : forall G dom ran t,
Var G (SArrow dom ran)
-> Var G dom
-> Var G (SArrow ran t)
-> plinear G t
| PBind : forall G t t',
pprimop G t'
-> plinear (t' :: G) t
-> plinear G t.
Denotational semantics |
Fixpoint ptyDenote (t : sty) : Set :=
match t with
| SNat => nat
| SArrow t1 t2 => ptyDenote t1 -> withCont (ptyDenote t2)
end.
Definition pexpDenote (t : sty) := withCont (ptyDenote t).
Fixpoint pprimopDenote (G : list sty) (t : sty) (op : pprimop G t) {struct op}
: Subst ptyDenote G -> ptyDenote t :=
match op in (pprimop G t) return (Subst ptyDenote G -> ptyDenote t) with
| PVar _ _ v => VarDenote v
| PConst _ n => fun _ => n
| PLam _ _ _ lin => fun s => fun x => plinearDenote lin (SCons _ x s)
end
with plinearDenote (G : list sty) (t : sty) (lin : plinear G t) {struct lin}
: Subst ptyDenote G -> pexpDenote t :=
match lin in (plinear G t) return (Subst ptyDenote G -> pexpDenote t) with
| PThrow _ _ op => fun s =>
withCont_const
(pprimopDenote op s)
| PApply _ _ _ _ func arg cont => fun s =>
withCont_compose
((VarDenote func s) (VarDenote arg s))
(VarDenote cont s)
| PBind _ _ _ op lin' => fun s =>
withCont_bind
(pprimopDenote op s)
(fun res => plinearDenote lin' (SCons _ res s))
end.
Build syntactic support code |
Syntactify pprimop.
Syntactify pprimopDenote.