% -*- mode: beluga; indent-tabs-mode: nil -*- % Type-preserving CPS on System F % adapted from Danvy and Filinski, Representing Control, 1992 % and Guillemette and Monnier, A Type-Preserving Compiler In Haskell, 2008 % author: Olivier Savary-Belanger % date: 2012-2013 % % Types T % LF tp: type = | nat : tp | arr : tp -> tp -> tp | code : tp -> tp -> tp | cross : tp -> tp -> tp | unit : tp | all : (tp -> tp) -> tp ; %name tp T. LF source : tp -> type = | app : source (arr S T) -> source S -> source T | fst : source (cross S T) -> source S | rst : source (cross S T) -> source T | lam : (source S -> source T) -> source (arr S T) | cons: source S -> source T -> source (cross S T) | letv : (source S) -> (source S -> source T) -> source T | nilv : source unit | z : source nat | suc : source nat -> source nat | tlam : ({t:tp} source (T t)) -> source (all (\t.T t)) | tapp: {a:tp} (source (all (\t.T t))) -> source (T a) ; LF exp : type = | kapp : value (arr S T) -> value S -> (value T -> exp) -> exp | klet : value S -> (value S -> exp) -> exp | kfst : value (cross S T) -> (value S -> exp) -> exp | krst : value (cross S T) -> (value T -> exp) -> exp | halt : value S -> exp | ktapp : {a:tp} value (all (\t. T t)) -> (value (T a) -> exp) -> exp and value : tp -> type = | klam : (value S -> (value T -> exp) -> exp) -> value (arr S T) | kcons : value S -> value T -> value (cross S T) | knil : value unit | kz : value nat | ksuc : value nat -> value nat | ktlam : ({t:tp} (value (T t) -> exp) -> exp) -> value (all (\t.T t)) ; schema ctx = some [s:tp] block (x:source s, _t:value s) + tp ; rec cpse : (g:ctx)[g |- source S] -> [g, c: value S -> exp |- exp] = / total e (cpse g s e) / fn e => case e of | [g |- #p.1] => [g,c:value _ -> exp |- c (#p.2[..])] | [g |- z] => [g,c:value nat -> exp |- c kz] | [g |- nilv] => [g,c:value unit -> exp |- c knil] | [g |- suc N] => let [g,c:value nat -> exp |- P] = cpse [g |- N] in [g,k:value nat -> exp |- P [..,\p. k (ksuc p)] ] | [g |- cons M N] => let [g,k1:value S -> exp |- P] = cpse [g |- M] in let [g,k2:value T -> exp |- Q] = cpse [g |- N] in [g,k:value (cross S T) -> exp |- P[ .., \p. Q[..,\q. k (kcons p q)]] ] | {M:[g, x:source S |- source T[..]]} [g |- lam \x. M] => let [g, b:block (x:source S, _t:value S[..]), c:value T[..] -> exp |- P[..,b.2,c] ] = cpse [g,b:block (x:source S , _t:value S[..]) |- M[..,b.1 ] ] in [g, k:value (arr S T) -> exp |- k (klam \x.\c. P[..,x,c]) ] | {N:[g, x:source S |- source T[..]]} [g |- letv M \x. N] => let [g,k1:value S -> exp |- P] = cpse [g |- M] in let [g,b:block (x:source S, _t:value S[..]), c:value T[..] -> exp |- Q[..,b.2,c]] = cpse [g,b:block (x:source S , _t:value S[..]) |- N[..,b.1] ] in [g,k:value T -> exp |- P[..,(\p. klet p (\x. Q[..,x,k]))] ] | [g |- app E1 E2] => let [g, c:value (arr S T) -> exp |- E1' ] = cpse [g |- E1 ] in let [g, c:value S -> exp |- E2' ] = cpse [g |- E2 ] in [g,c:value T -> exp |- E1' [..,\f. E2'[ .. , \x. kapp f x c]] ] | [g |- fst E] => let [g, c:value (cross S T) -> exp |- E'] = cpse [g |- E] in [g,c:value S -> exp |- E' [..,\x. kfst x c] ] | [g |- rst E] => let [g, c:value (cross S T) -> exp |- E'] = cpse [g |- E] in [g,c:value T -> exp |- E' [..,\x. krst x c]] | [g |- tlam \t.E] => let [g,t:tp, c:value T -> exp |- E'] = cpse [g,t:tp |- E] in [g, k:value (all \t.T) -> exp |- k (ktlam \t.\c. E'[..,t,c]) ] | [g |- tapp A E] => let [g, c:value (all \t. T) -> exp |- E'] = cpse [g |- E] in [g,k:value (T [..,A]) -> exp |- E'[..,(\y. ktapp A[..] y k)] ] ;