| Target language of allocation explicitation |
Require Import Arith Eqdep List.
Require Import LambdaTamer.ListUtil.
Require Import LambdaTamer.LambdaTamer.
Require Import CTPC.AllocMonad.
Require Import CTPC.Trace.
Set Implicit Arguments.
Type language |
Inductive aty : Set :=
| ANat : aty
| ARef : aty
| ACode : list aty -> aty.
Definition atys := list aty.
Definition atyDenote (t : aty) := nat.
Definition aty_eq_dec (x y : aty) : {x = y} + {x <> y}.
Definition atys_eq_dec (x y : atys) : {x = y} + {x <> y}.
Term language |
Syntax |
Inductive aargs : list aty -> atys -> Set :=
| AANil : forall G, aargs G nil
| AACons : forall G t ts,
Var G t
-> aargs G ts
-> aargs G (t :: ts)
with aprimop : list aty -> aty -> Set :=
| AVar : forall G t,
Var G t
-> aprimop G t
| AConst : forall G,
nat
-> aprimop G ANat
| ACodeptr : forall G args,
nat
-> aprimop G (ACode args)
| ANew : forall G ts,
aargs G ts
-> aprimop G ARef
| AProj : forall G t,
Var G ARef
-> nat
-> aprimop G t
with alinear : list aty -> unit -> Set :=
| AApply : forall G args,
Var G (ACode args)
-> aargs G args
-> alinear G tt
| ABind : forall G t,
aprimop G t
-> alinear (t :: G) tt
-> alinear G tt.
Inductive afunc : list aty -> atys -> Set :=
| AFBody : forall G,
alinear G tt
-> afunc G nil
| AFLam : forall G t ctx,
afunc (t :: G) ctx
-> afunc G (t :: ctx).
Denotational semantics |
Inductive tag : Set :=
| Traced
| Untraced.
Definition tagof t :=
match t with
| ARef => Traced
| _ => Untraced
end.
Definition tag_eq_dec (x y : tag) : {x = y} + {x <> y}.
Definition adom := prod tag nat.
Definition aargsTy (ts : atys) := list adom.
Definition aprimopTy (t : aty) := allocM adom (atyDenote t).
Definition alinearTy (_ : unit) := allocM adom (nat * atys * list adom)%type.
Definition checkTag (tg : tag) (d : adom) (A : Set) (e1 : nat -> A) (e2 : A) : A :=
if tag_eq_dec tg (fst d)
then e1 (snd d)
else e2.
Fixpoint aargsDenote G ctx (e : aargs G ctx) {struct e}
: Subst atyDenote G -> aargsTy ctx :=
match e in (aargs G ctx) return (Subst atyDenote G -> aargsTy ctx) with
| AANil _ => fun _ => nil
| AACons _ t _ v e' => fun s => (tagof t, VarDenote v s) :: aargsDenote e' s
end
with aprimopDenote (G : list aty) (t : aty) (op : aprimop G t) {struct op}
: Subst atyDenote G -> aprimopTy t :=
match op in (aprimop G t) return (Subst atyDenote G -> aprimopTy t) with
| AVar _ _ v => fun s => aReturn (VarDenote v s)
| AConst _ n => fun _ => aReturn n
| ACodeptr _ _ n => fun _ => aReturn (S n)
| ANew _ _ fs => fun s => aNew (aargsDenote fs s)
| AProj _ t v n => fun s =>
d <- aRead (VarDenote v s) n;
checkTag (tagof t) d
(fun x => aReturn x)
(aBottom _)
end
with alinearDenote (G : list aty) (t : unit) (lin : alinear G t) {struct lin}
: Subst atyDenote G -> alinearTy t :=
match lin in (alinear G t) return (Subst atyDenote G -> alinearTy t) with
| AApply _ argsT func args => fun s =>
aReturn (VarDenote func s, argsT, aargsDenote args s)
| ABind _ _ op lin' => fun s =>
v <- aprimopDenote op s;
alinearDenote lin' (SCons _ v s)
end.
Fixpoint aformalsDenote (ts : atys) : Set :=
match ts with
| nil => unit
| t :: ts' => (atyDenote t * aformalsDenote ts')%type
end.
Definition afuncTy (ts : atys) := aformalsDenote ts -> allocM adom (nat * atys * list adom)%type.
Fixpoint afuncDenote (G : list aty) (ts : atys) (f : afunc G ts) {struct f}
: Subst atyDenote G -> afuncTy ts :=
match f in (afunc G ts)
return (Subst atyDenote G -> afuncTy ts) with
| AFBody _ lin => fun s _ => alinearDenote lin s
| AFLam _ _ _ f' => fun s env => afuncDenote f' (SCons _ (fst env) s) (snd env)
end.
Programs |
Syntax |
Record aprog (G : list aty) : Set := {
aFuncTys : list atys;
aFuncs : listI (afunc nil) aFuncTys;
aBody : alinear G tt
}.
Co-inductive trace semantics |
Definition makeActuals : forall (ts : atys) (args : list adom),
length ts = length args
-> aformalsDenote ts.
Section Traces.
Variable G : list aty.
Variable pr : aprog G.
CoFixpoint amakeTrace (m : mem adom) (pc : nat) (argsT : atys) (args : list adom) : trace nat :=
match pc with
| O =>
match argsT, args with
| _ :: ANat :: nil, _ :: (_, output) :: nil => Output output
| _, _ => Crash
end
| S pc =>
match nthI (aFuncs pr) pc with
| None => Crash
| Some (existS ts f) =>
if atys_eq_dec argsT ts
then match eq_nat_dec (length ts) (length args) with
| left Heq =>
match afuncDenote f (SNil _) (makeActuals ts args Heq) m with
| None => Crash
| Some (m', (pc', argsT', args')) => Call (amakeTrace m' pc' argsT' args')
end
| right _ => Crash
end
else Crash
end
end.
Definition aprogDenote (s : Subst atyDenote G) (m : mem adom) :=
match alinearDenote (aBody pr) s m with
| None => Crash
| Some (m', (pc, argsT, args)) => amakeTrace m' pc argsT args
end.
Theorem amakeTrace_unfold_external : forall m t1 env tg output,
amakeTrace m O (t1 :: ANat :: nil) (env :: (tg, output) :: nil)
= Output output.
Theorem amakeTrace_unfold_internal : forall m pc argsT args ts f,
nthI (aFuncs pr) pc = Some (existS _ ts f)
-> argsT = ts
-> forall (Heq : length ts = length args) m' pc' argsT' args',
afuncDenote f (SNil _) (makeActuals ts args Heq) m = Some (m', (pc', argsT', args'))
-> amakeTrace m (S pc) argsT args
= Call (amakeTrace m' pc' argsT' args').
End Traces.
Generate syntactic support code |
Syntactify aargs.
Syntactify aargsDenote.