%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Cost semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% grammar heap :: 'Heap_' ::= {{ com Values on the heap }} | cl :: :: HeapClosure {{ com Closure }} | K args :: :: HeapConstructor {{ com Data constructor }} | x :: :: HeapIndirection {{ com Indirection }} cost :: 'cost_' ::= | alloc K :: :: AllocateCon | alloc cl :: :: AllocateClosure | alloc PAP :: :: AllocatePAP t {{ tex \theta }} :: 't_' ::= | {} :: :: empty | { ccs |-> cost } :: :: inject | t <> t' :: :: append G {{ tex \Gamma }}, D {{ tex \Delta }}, T {{ tex \Theta }} :: 'G_' ::= {{ com Heap }} | G [ Gp ] :: :: vn {{ com Heap with assignment }} Gp :: 'Gp_' ::= {{ com Heap assignment }} | x |- ccs -> heap :: :: prod {{ tex [[x]] \overset{[[ccs]]}{\mapsto} [[heap]] }} formula :: 'formula_' ::= | judgement :: :: judgement % all the random extra stuff we didn't want to gunk up the inductive % types with... | alt' = alt :: :: Galt | ccs' /= ccs :: :: Gccsneq | Gp in G :: :: Gin | x fresh :: :: Gfresh v :: 'v_' ::= | cl :: :: HClosureReentrant | K args :: :: HConstructor ret :: 'ret_' ::= {{ com Return values }} | a :: :: Return {{ com Normal return }} | { x args } :: :: LetNoEscape {{ com Jump to let-no-escape }} subrules v <:: heap defns Jcost :: '' ::= defn ccs , G : e >- t -> D : ret , ccs' :: :: cost :: '' {{tex [[ccs]] [[,]] [[G]] [[:]] [[e]]\ \Downarrow_{[[t]]}\ [[D]] [[:]] [[ret]] [[,]] [[ccs']] }} by --------------------------------------- :: Lit ccs, G : lit >-{}-> G : lit, ccs x |- ccs0 -> v in G --------------------------------------- :: Whnf ccs, G : x nil >-{}-> G : x, ccs ccs0, G : e >-t-> D : z, ccs' --------------------------------------- :: Thunk ccs, G [ x |- ccs0 -> \ u _ nil . e ] : x nil >-t-> D [ x |- ccs0 -> z ] : z, ccs' f |- ccs0 -> \ r ccs1 . e in G z fresh --------------------------------------- :: AppUnder ccs, G : f >- { ccs |-> alloc PAP } -> G [ z |- ccs -> \ r _ . f ] : z, ccs % NB: PAPs not charged! ccs ^ ccs0, G : e >-t-> D : z, ccs' ------------------------------------------------- :: App ccs, G [ f |- ccs0 -> \ r CCCS . e ] : f >-t-> D : z, ccs' ccs, G : e >-t-> D : z, ccs' ccs1 /= CCCS ------------------------------------------------- :: AppTop ccs, G [ f |- _ -> \ r ccs1 . e ] : f >-t-> D : z, ccs' ccs, G : f >-t-> D : f', ccs' ccs, D : f' >-t'-> T : z, ccs'' ---------------------------------------- :: AppOver ccs, G : f >-t <> t'-> T : z, ccs'' z fresh ---------------------------------------- :: ConApp ccs, G : K >- { ccs |-> alloc K } -> G [ z |- ccs -> K ] : z, ccs altj = Kk -> e' ccs, G : e >- t -> D [ y |- _ -> Kk ] : y, ccs' ccs, D [ y |- _ -> Kk ] : e' [ y / x ] >- t' -> T : z, ccs'' --------------------------------------------------------------- :: Case ccs, G : case e as x of >- t <> t' -> T : z, ccs'' y fresh ccs, G [ y |- ccs -> cl ] : e [ x / y ] >- t -> D : z, ccs' ------------------------------------------------------------ :: LetClosure ccs, G : let x = cl in e >- { ccs |-> alloc cl } <> t -> D : z, ccs' y fresh ccs, G [ y |- ccs -> K ] : e [ x / y ] >- t -> D : z, ccs' ------------------------------------------------------------ :: LetCon ccs, G : let x = K CCCS in e >- { ccs |-> alloc K } <> t -> D : z, ccs' ccs, G : e >- t -> D : { f } , ccs' ccs, D : e' >- t' -> T : z, ccs'' ------------------------------------------------------------ :: LneClosure ccs, G : lne f = \ upd _ . e' in e >- t <> t' -> T : z, ccs'' ccs, G : e >- t -> D : x , ccs' ccs, D : K >- t' -> T : z, ccs'' --------------------------------------------------------------- :: LneCon ccs, G : lne x = K _ in e >- t <> t' -> T : z, ccs'' ccs # cc, G : e >- t -> D : z, ccs' --------------------------------------- :: SCC ccs, G : scc cc e >- t -> D : z, ccs'