| Continuation-only language |
Require Import List.
Require Import LambdaTamer.LambdaTamer.
Require Import CTPC.Continuation.
Set Implicit Arguments.
Type language |
Syntax |
Inductive oty : Set :=
| ONat : oty
| OCont : list oty -> oty.
Definition otys := list oty.
Denotational semantics |
Definition result := nat.
Fixpoint otyDenote (t : oty) : Set :=
match t with
| ONat => nat
| OCont ts =>
(fix otysDenote (ts : list oty) : Set :=
match ts with
| nil => unit
| t :: ts' => (otyDenote t * otysDenote ts')%type
end) ts -> result
end.
Fixpoint otysDenote (ts : list oty) : Set :=
match ts with
| nil => unit
| t :: ts' => (otyDenote t * otysDenote ts')%type
end.
Term language |
Syntax |
Inductive oprimop : list oty -> oty -> Set :=
| OVar : forall G t,
Var G t
-> oprimop G t
| OLam : forall G dom,
ocont G dom
-> oprimop G (OCont dom)
| OConst : forall G, nat -> oprimop G ONat
with olinear : list oty -> unit -> Set :=
| OApply : forall G dom,
Var G (OCont dom)
-> oargs G dom
-> olinear G tt
| OBind : forall G t,
oprimop G t
-> olinear (t :: G) tt
-> olinear G tt
with ocont : list oty -> otys -> Set :=
| OCNil : forall G,
olinear G tt
-> ocont G nil
| OCCons : forall G t ts,
ocont (t :: G) ts
-> ocont G (t :: ts)
with oargs : list oty -> otys -> Set :=
| OANil : forall G, oargs G nil
| OACons : forall G t ts,
Var G t
-> oargs G ts
-> oargs G (t :: ts).
Denotational semantics |
Definition oresultDenote (_ : unit) := result.
Definition ocontTy (ts : otys) := otysDenote ts -> result.
Fixpoint oprimopDenote (G : list oty) (t : oty) (op : oprimop G t) {struct op}
: Subst otyDenote G -> otyDenote t :=
match op in (oprimop G t) return (Subst otyDenote G -> otyDenote t) with
| OVar _ _ v => VarDenote v
| OConst _ n => fun _ => n
| OLam _ _ cont => ocontDenote cont
end
with olinearDenote (G : list oty) (t : unit) (lin : olinear G t) {struct lin}
: Subst otyDenote G -> oresultDenote t :=
match lin in (olinear G t) return (Subst otyDenote G -> oresultDenote t) with
| OApply _ _ func args => fun s =>
(VarDenote func s) (oargsDenote args s)
| OBind _ _ op lin' => fun s =>
withCont_bind
(oprimopDenote op s)
(fun res => olinearDenote lin' (SCons _ res s))
end
with ocontDenote (G : list oty) (ts : otys) (cont : ocont G ts) {struct cont}
: Subst otyDenote G -> ocontTy ts :=
match cont in (ocont G ts) return (Subst otyDenote G -> ocontTy ts) with
| OCNil _ lin => fun s _ => olinearDenote lin s
| OCCons _ _ _ cont' => fun s args => ocontDenote cont' (SCons _ (fst args) s) (snd args)
end
with oargsDenote (G : list oty) (ts : otys) (args : oargs G ts) {struct args}
: Subst otyDenote G -> otysDenote ts :=
match args in (oargs G ts) return (Subst otyDenote G -> otysDenote ts) with
| OANil _ => fun _ => tt
| OACons _ _ _ v args' => fun s => (VarDenote v s, oargsDenote args' s)
end.
Build syntactic support code |
Syntactify oprimop.
Syntactify oprimopDenote.