Library CTPC.Compile
Require Import List.
Require Import LambdaTamer.LambdaTamer.
Require Import LambdaTamer.Tactics.
Require Import CTPC.Continuation.
Require Import CTPC.Source.
Require Import CTPC.CPS.
Require Import CTPC.Cont.
Require Import CTPC.CC.
Require Import CTPC.Trace.
Require Import CTPC.AllocMonad.
Require Import CTPC.Alloc.
Require Import CTPC.Flat.
Require Import CTPC.Asm.
Require Import CTPC.CPSify.
Require Import CTPC.Contify.
Require Import CTPC.CCify.
Require Import CTPC.Allocify.
Require Import CTPC.Flatify.
Require Import CTPC.Safety.
Require Import CTPC.Asmify.
Set Implicit Arguments.
Definition compile_term' (G : list sty) (t : sty) (e : sterm G t)
: program :=
asmProg (flatProg (allocProg (ccLinear (contifyLinear (cps e))))).
Definition compile_term : forall (t : sty) (e : sterm nil t), program
:= compile_term' (G:= nil).
Lemma cont_lr : CCify.Subst_lr
(SCons (denote:= otyDenote) (OCont (ONat :: nil)) (fun n => fst n) (SNil otyDenote))
(SCons (denote:= ctyDenote) (CCont (CNat :: nil)) (fun n => fst n) (SNil ctyDenote)).
Hint Resolve cont_lr.
Definition mem0 : mem adom := ((Untraced, 0) :: (Traced, 1) :: nil) :: nil :: nil.
Lemma cc_lr : forall Gpr (pr : cprog Gpr tt), Allocify.Subst_lr pr mem0
(SCons (denote:= ctyDenote) (CCont (CNat :: nil)) (fun n : nat * unit => fst n) (SNil ctyDenote))
(SCons (denote:= atyDenote) ARef 0 (SNil atyDenote)).
Hint Resolve cc_lr.
Ltac my_simpl := repeat progress (subst;
repeat match goal with
| [ H : _ |- _ ] => rewrite NatDict.sel_empty in H
end).
Section runtime.
Variable rt : runtime.
Lemma compile_slots_lr : forall args,
flatContext
(ListUtil.revApp
(map allocTy
(map ccTy
(OCont (contifyTy SNat :: nil) :: map contifyTy nil)))
nil) = flatContext (ListUtil.revApp args nil)
-> slots_lr rt (init_bound (length args)) mem0
(flatContext (ListUtil.revApp args nil)) (NatDict.empty 0) (NatDict.empty (ptrComp rt mem0 0)).
Theorem compile_correct : forall (e : sterm nil SNat),
runTrace
(programDenote rt (compile_term e)
(NatDict.empty (ptrComp rt mem0 0))
(heapComp rt mem0))
(stermDenote e (SNil _)).
End runtime.
Index
This page has been generated by coqdoc