| Target language of binding flattening |
Require Import Arith List.
Require Import LambdaTamer.ListUtil.
Require Import LambdaTamer.LambdaTamer.
Require Import CTPC.AllocMonad.
Require Import CTPC.Trace.
Require Import CTPC.Dict.
Require Import CTPC.Alloc.
Set Implicit Arguments.
Instantiating some maps |
Module NatKey <: DICT_DOMAIN.
Definition A := nat.
Definition A_eq_dec := eq_nat_dec.
End NatKey.
Module NatDict := Dict(NatKey).
Type language |
Definition ftyping := NatDict.dict aty.
Term language |
Syntax |
Inductive fargs : ftyping -> atys -> Set :=
| FANil : forall G, fargs G nil
| FACons : forall G ts sl,
fargs G ts
-> fargs G (NatDict.sel G sl :: ts).
Inductive fprimop : ftyping -> aty -> Set :=
| FSlot : forall G sl,
fprimop G (NatDict.sel G sl)
| FConst : forall G,
nat
-> fprimop G ANat
| FCodeptr : forall G args,
nat
-> fprimop G (ACode args)
| FNew : forall G ts,
fargs G ts
-> fprimop G ARef
| FProj : forall G t sl,
NatDict.sel G sl = ARef
-> nat
-> fprimop G t.
Section fprecondition.
Variable tp : ftyping.
Variable ts : atys.
Definition fprecondition :=
forall n t,
nth_error ts n = Some t
-> NatDict.sel tp n = t.
End fprecondition.
Inductive flinear : ftyping -> Set :=
| FJump : forall G args sl,
NatDict.sel G sl = ACode args
-> fprecondition G args
-> flinear G
| FSet : forall G sl t,
fprimop G t
-> flinear (NatDict.upd G sl t)
-> flinear G.
Denotational semantics |
Definition slots := NatDict.dict nat.
Fixpoint fargsDenote G ctx (e : fargs G ctx) (sls : slots) {struct e} : list adom :=
match e with
| FANil _ => nil
| FACons _ _ v e' => (tagof (NatDict.sel G v), NatDict.sel sls v) :: fargsDenote e' sls
end.
Definition fprimopDenote G t (op : fprimop G t) (sls : slots)
: allocM adom nat :=
match op with
| FSlot _ v => aReturn (NatDict.sel sls v)
| FConst _ n => aReturn n
| FCodeptr _ _ n => aReturn (S n)
| FNew _ _ fs => aNew (fargsDenote fs sls)
| FProj _ _ v _ n =>
d <- aRead (NatDict.sel sls v) n;
checkTag (tagof t) d
(fun x => aReturn x)
(aBottom _)
end.
Fixpoint flinearDenote G (lin : flinear G) (sls : slots) {struct lin}
: allocM adom (nat * atys * slots)%type :=
match lin with
| FJump _ argsT func _ _ =>
aReturn (NatDict.sel sls func, argsT, sls)
| FSet _ sl _ op lin' =>
v <- fprimopDenote op sls;
flinearDenote lin' (NatDict.upd sls sl v)
end.
Programs |
Syntax |
Record fprog (G : ftyping) : Set := {
fFuncTys : list ftyping;
fFuncs : listI flinear fFuncTys;
fBody : flinear G
}.
Co-inductive trace semantics |
Section flatContext'.
Variable tp0 : ftyping.
Fixpoint flatContext' (G : list aty) : ftyping :=
match G with
| nil => tp0
| t :: G' => NatDict.upd (flatContext' G') (length G') t
end.
End flatContext'.
Definition flatContext := flatContext' (NatDict.empty ANat).
Section Traces.
Variable G : ftyping.
Variable pr : fprog G.
CoFixpoint fmakeTrace (m : mem adom) (pc : nat) (argsT : atys) (sls : slots) : trace nat :=
match pc with
| O =>
match argsT with
| _ :: ANat :: nil => Output (NatDict.sel sls 1)
| _ => Crash
end
| S pc =>
match nthI (fFuncs pr) pc with
| None => Crash
| Some (existS ts f) =>
if NatDict.dict_eq_dec aty_eq_dec ts (flatContext (argsT +++ nil))
then match flinearDenote f sls m with
| None => Crash
| Some (m', (pc', argsT', sls')) => Call (fmakeTrace m' pc' argsT' sls')
end
else Crash
end
end.
Definition fprogDenote (sls : slots) (m : mem adom) :=
match flinearDenote (fBody pr) sls m with
| None => Crash
| Some (m', (pc, argsT', sls')) => fmakeTrace m' pc argsT' sls'
end.
Theorem fmakeTrace_unfold_external : forall m t1 sls,
fmakeTrace m O (t1 :: ANat :: nil) sls
= Output (NatDict.sel sls 1).
Theorem fmakeTrace_unfold_internal : forall pc argsT ts f,
nthI (fFuncs pr) pc = Some (existS _ ts f)
-> ts = flatContext (argsT +++ nil)
-> forall m sls m' pc' argsT' sls', flinearDenote f sls m = Some (m', (pc', argsT', sls'))
-> fmakeTrace m (S pc) argsT sls
= Call (fmakeTrace m' pc' argsT' sls').
End Traces.