% -*- mode: beluga; indent-tabs-mode: nil -*- % Type-preserving closure conversion and hoisting. % author: Olivier Savary-Belanger % date: 2012-2013 % PRAGMA FOR CHECKING COVERAGE %coverage % ---------------------------------------------------------- % Types T LF tp: type = | nat : tp | arr : tp -> tp -> tp | code : tp -> tp -> tp | cross : tp -> tp -> tp | unit : tp ; %name tp T. % ---------------------------------------------------------- % Source language M,N LF source: tp -> type = | lam : (source T -> source S) -> source (arr T S) | app : source (arr T S) -> source T -> source S | letv : source T -> (source T -> source S) -> source S | z : source nat | suc : source nat -> source nat | nil : source unit | fst : source (cross T S) -> source T | rst : source (cross T S) -> source S | cons : source T -> source S -> source (cross T S) ; %name source M. % ---------------------------------------------------------- % Target language P,Q LF target: tp -> type = | cnil : target unit | ccons : target T -> target L -> target (cross T L) | cfst : target (cross T L) -> target T | crst : target (cross T L) -> target L | capp : target (code T S) -> target T -> target S | clam : (target T -> target S) -> target (code T S) | clet : target T -> (target T -> target S) -> target S | cpack : target (code (cross T E) S) -> target E -> target (arr T S) % We write E for the type of the environment | copen : target (arr T S) -> ({e:tp} target (code (cross T e) S) -> target e -> target S) -> target S | cz : target nat | csuc : target nat -> target nat ; %name target P. % ---------------------------------------------------------- % Context schema declarations for source and target context schema sctx = source T; schema tctx = target T; % ---------------------------------------------------------- % SubCtx Γ' Γ ⇔ Γ' ⊆ Γ % This is in fact a weakening substitution between % Γ and Γ'. We can in fact use substitution variables in % Beluga to give a witness for this relationship. % However, since substitution variables are more general, % i.e. they do not guarantee that variables are mapped to % variables, one would need to carry a proof that the % strengthening substitution is indeed just a variable % to variable substitution. inductive SubCtx: {g':sctx} {g:sctx} ctype = | WInit: SubCtx [] [] | WDrop: SubCtx [g'] [g] -> SubCtx [g'] [g,x:source T[]] | WKeep: SubCtx [g'] [g] -> SubCtx [g',x:source T[]] [g,x:source T[]] ; % ---------------------------------------------------------- % Term Strengthening: % % Given a source term M in a context Γ, % we compute a strengthened version of M which only depends on % the free variables occurring in M. % To accomplish this efficiently, we use an auxiliary datatype % wrap T N which describes a source term with N free variables. % If M has type S and has N free variables x1:T1, ... xn:Tn, % then wrap T N intuitively denotes a term of type % T1 -> T2 -> ... -> Tn -> S . % LF nat: type = | nz : nat | nsuc : nat -> nat ; LF wrap: tp -> nat -> type = | init: (source T) -> wrap T nz | abs: (source S -> wrap T N) -> wrap (arr S T) (nsuc N) ; % StrTerm [Γ] [ |- T] ⇔ ∃ Γ' M, Γ' ⊆ Γ ∧ and Γ' ⊢ M : T inductive StrTerm': {g:sctx} [ |- tp] -> [|- nat] -> ctype = | STm': [g' |- wrap T[] N[]] -> SubCtx [g'] [g] -> StrTerm' [g] [ |- T] [|- N] ; rec str: {g:sctx}[g |- wrap T[] N[]] -> StrTerm' [g] [ |- T] [|- N] = / total g (str g) / mlam g => fn e => case [g] of | [] => let [|- M] = e in STm' [|- M] WInit | [g, x:source _] => case e of | [g,x:source _ |- M[..] ] => let STm' [h |- M'] rel = str [g] [g |- M] in STm' [h |- M'] (WDrop rel) | [g,x:source _ |- M] => let STm' [h |- abs \x.M'] rel = str [g] [g |- abs \x. M] in STm' [h,x:source _ |- M'] (WKeep rel) ; inductive StrTerm: {g:sctx} [ |- tp] -> ctype = | STm: [g',x:source S[] |- source T[]] -> SubCtx [g'] [g] -> StrTerm [g,x:source S[]] [ |- T] ; rec strengthen: [g,x:source S[] |- source T[]] -> StrTerm [g, x:source S[]] [|- T] = / total (strengthen) / fn m => let [g,x:source _ |- M] = m in let STm' [g' |- abs \x. init M'[ .., x]] wk = str [g] [g |- abs \x. init M[ .. ,x]] in STm [g',x:source _ |- M'] wk ; % ---------------------------------------------------------- % Map [Δ] [Γ] ⇔ Δ ⊢ ρ : Γ inductive Map:{h:tctx}{g:sctx} ctype = | M_id:{h:tctx} Map [h] [] | M_dot: Map [h] [g] -> [h |- target S[]] -> Map [h] [g,x:source S[]] ; rec weaken: Map [h] [g] -> Map [h,x:target S[]] [g] = % / total m (weaken _ _ _ m) / fn sigma => case sigma of | M_id [h] => M_id [h,x:target _] | M_dot sigma' [h |- M] => M_dot (weaken sigma') [h,x:target _ |- M[..] ] ; rec extend: Map [h] [g] -> Map [h,x:target S[]] [g,x:source S[]] = % / total m (extend _ _ _ m) / fn sigma => let (sigma : Map [h] [g]) = sigma in M_dot (weaken sigma) [h,x:target _ |- x] ; % ---------------------------------------------------------- % Variable lookups rec lookup: Map [h] [g] -> {#q:[g |- source T[]]}[h |- target T[]] = % / total m (lookup _ _ _ m) / fn sigma => mlam #q => case sigma of | M_dot sigma' [h |- M] => let (sigma : Map [h] [g',x:source S[]]) = sigma in (case [g', x:source S[] |- #q] of | [g', x:source T |- x ] => [h |- M] | [g', x:source S |- #p[..]] => lookup sigma' [g' |- #p] ) | M_id [h] => impossible [ |- #q] in [] ; % This definition may be thought of a tuple of type T which is known to consist only % of variables inductive VarTup: (g:sctx) {T:[ |- tp]} [g |- source T[]] -> ctype = | Emp : VarTup [|- unit] [|- nil] | Nex : VarTup [|- L] [g |- R] -> VarTup [|- cross T L] [g,x:source T[] |- cons x R[..] ] ; % lookuVars replaces each variable contained in the VarTup by their respective target term from Map. rec lookupVars: SubCtx [g'] [g] -> VarTup [|- G] [g' |- M] -> Map [h] [g] -> [h |- target G[]] = %/ total s (lookupVars _ _ _ _ _ s ) / fn r => fn vt => fn sigma => let (sigma : Map [h] [g]) = sigma in case r of | WInit => let Emp = vt in % g' = g = . [h |- cnil] | WDrop r' => let M_dot sigma' [h |- P] = sigma in lookupVars r' vt sigma' | WKeep r' => let (Nex vt') = vt in let (M_dot sigma' [h |- P]) = sigma in let [h |- M] = lookupVars r' vt' sigma' in [h |- ccons P M] ; % ---------------------------------------------------------- % Context reification % CtxAsTup Γ ⇔ ∃ ρ, (x1,...,xn):(t1 × ... × tn) ⊢ ρ : Γ where Γ = x1:t1,...,xn:tn inductive CtxAsTup: {g:sctx} ctype = | EnvClo: VarTup [|- G] [g |- M] -> Map [x:target G] [g] -> CtxAsTup [g] ; rec extendEnv: Map [x:target S] [g] -> Map [x:target (cross Y S)] [g] = % / total m (extendEnv _ _ _ m) / fn sigma => case sigma of | M_id [x:target S] => M_id [x:target _] | M_dot sigma' [x:target S |- M] => M_dot (extendEnv sigma') [x:target _ |- M[crst x] ] ; rec reify : {g:sctx} CtxAsTup [g] = % / total g (reify g) / mlam g => case [g] of | [ ] => EnvClo Emp (M_id [x:target unit]) | [g,x:source S[]] => let EnvClo vt sigma = reify [g] in let rho' = extendEnv sigma in let rho = M_dot rho' [xenv:target (cross S[] _) |- cfst xenv] in EnvClo (Nex vt) rho ; % ---------------------------------------------------------- % NEW PART FOR HOISTING LF env: {Lf:tp}target Lf -> type = | env_nil: env unit cnil | env_cons: {P:target T} env L E -> env (cross T L) (ccons P E) ; % Result of Hoisting: Result [Δ] [|- T] ⇔ ∃ P L, Δ,l : L ⊢ M : T and · ⊢ E : L inductive Result:{h:tctx} [ |- tp] -> ctype = | Result : [h,l:target Lf[] |- target T[]] -> [ |- env Lf E] -> Result [h] [ |- T] ; inductive Append: [|- env T E1] -> [ |- env S E2] -> [ |- env TS E3] -> ctype = | App_nil: Append [ |- env_nil] [ |- E] [ |- E] | App_cons: Append [|- E1] [|- E2] [|- E3] -> Append [|- env_cons P E1] [|- E2] [|- env_cons P E3] ; inductive ExAppend: [ |- env T E1] -> [ |- env S E2] -> ctype = | ExEnv : Append [ |- E1] [ |- E2] [ |- E3] -> ExAppend [ |- E1] [ |- E2] ; rec append: {Env1: [ |- env L1 E1]}{Env2: [ |- env L2 E2]} ExAppend [ |- Env1] [ |- Env2] = % / total p1 (append _ _ _ _ p1) / mlam Env1, Env2 => case [|- Env1] of | [|- env_nil] => ExEnv App_nil | [|- env_cons P Env1'] => let ExEnv a = append [|- Env1'] [|- Env2] in ExEnv (App_cons a) ; LF eq: env L E -> env L' E' -> type = | refl : eq Env Env; %{ Lemma: If Append Env1 env_nil Env3 then Env1 = Env3 }% rec append_nil: Append [ |- Env1] [ |- env_nil] [ |- Env3] -> [ |- eq Env1 Env3] = % / total a (append_nil _ _ _ _ a) / fn a => case a of | App_nil => [ |- refl] | App_cons a' => let [ |- refl] = append_nil a' in [ |- refl] ; rec weakenEnv1:(g:tctx) {Env1 : [ |- env L1 E1]}{Env2: [|- env L2 E2]}{Env3: [|- env L3 E3]} Append [|- Env1] [|- Env2] [|- Env3] -> [g, l:target L2[] |- target T[]] -> [g, l: target L3[] |- target T[]] = % / total p (weakenEnv1 _ _ _ _ _ _ _ _ p) / mlam Env1, Env2, Env3 => fn prf => fn m => case prf of | App_nil => m | App_cons p => let [g,l: target _ |- M'] = weakenEnv1 [|- _ ] [|- _ ] [|- _] p m in [g,l:target _ |- M' [.., crst l] ] ; rec weakenEnv2:(g:tctx) {Env1 : [ |- env L1 E1]}{Env2:[|- env L2 E2]}{Env3: [|- env L3 E3]} Append [|- Env1] [|- Env2] [|- Env3] -> [g, l:target L1[] |- target T[]] -> [g, l: target L3[] |- target T[]] = % / total p (weakenEnv2 _ _ _ _ _ _ _ _ p) / mlam Env1, Env2, Env3 => fn prf => fn n => case prf of | App_nil => let ExEnv a = append [|- Env2] [|- env_nil] in let [ |- refl] = append_nil a in weakenEnv1 [|- _ ] [|- _ ] [ |- _ ] a n | App_cons p => let [g,l:target (cross S[] L1'[]) |- N] = n in let [g,x:target S[], l:target L3'[] |- N'[..,x,l]] = weakenEnv2 [|- _ ] [|- _ ][|- _ ] p [g,x:target S[],l:target L1'[] |- N[ .. , (ccons x l)]] in [g,l:target (cross S[] L3'[]) |- N'[ .. , cfst l , crst l] ] ; % ---------------------------------------------------------- rec hcc: [g |- source T[]] -> Map [h] [g] -> Result [h] [|- T[]] = % / total e (hcc _ _ _ e)/ fn e => fn sigma => let (sigma : Map [h] [g]) = sigma in case e of | [g |- z] => Result [h,l:target unit |- cz] [|- env_nil] | [g |- suc M] => let Result [h,l:target L[] |- P'] e = hcc [g |- M] sigma in Result [h,l:target L[] |- csuc P'] e | [g |- #p] => let [h |- M] = lookup sigma [g |- #p] in Result [h,l:target unit |- M[..] ] [ |- env_nil] | [g |- app M N] => let Result r1 [|- Env1] = hcc [g |- M ] sigma in let Result r2 [|- Env2] = hcc [g |- N ] sigma in let ExEnv (a12 : Append [|- _ ] [|- _ ] [|- Env3]) = append [|- Env1] [|- Env2] in let [h, l:target L |- P] = weakenEnv2 [|- _ ] [|- _ ] [|- _ ] a12 r1 in let [h, l:target L |- Q] = weakenEnv1 [|- _ ] [|- _ ] [|- _ ] a12 r2 in Result [h, l:target L |- copen P \e.\xf.\xenv. capp xf (ccons Q [..,l] xenv)] [|- Env3] | [g |- letv M \x. N] => let Result r1 [|- Env1] = hcc [g |- M] sigma in let Result r2 [|- Env2] = hcc [g,x: source _ |- N] (extend sigma) in let ExEnv (a12 : Append [|- _] [|- _] [|- Env3]) = append [|- Env1] [|- Env2] in let [h, l:target L[] |- P] = weakenEnv2 [|- _ ] [|- _ ] [|- _ ] a12 r1 in let [h,x:target T1[], l:target L[] |- Q] = weakenEnv1 [|- _ ] [|- _ ] [|- _ ] a12 r2 in Result [h, l:target L[] |- clet P (\x. Q[..,x,l])] [|- Env3] | [g |- lam \x.M] => let STm [g',x:source S[] |- M' ] wk = strengthen [g, x:source _ |- M ] in let EnvClo env rho = reify [g'] in let Result r1 [|- Env1] = hcc [g',x:source _ |- M' ] (extend rho) in let [h |- C] = lookupVars wk env sigma in let [xenv:target Lg[],x:target T[],l:target L[] |- P [xenv, x, l] ] = r1 in Result [h,l:target (cross (code L[] (code (cross T[] Lg[]) _ )) L[]) |- cpack (capp (cfst l) (crst l)) C[..] ] [|- env_cons (clam \l. clam (\clo. clet (cfst clo) \x. clet (crst clo) \xenv. P[xenv, x, l])) Env1 ] | [g |- cons M N] => let Result r1 [|- Env1] = hcc [g |- M] sigma in let Result r2 [|- Env2] = hcc [g |- N] sigma in let ExEnv (a12 : Append [|- _] [|- _] [|- Env3]) = append [|- Env1] [|- Env2] in let [h, l:target L[] |- P] = weakenEnv2 [|- _ ] [|- _ ] [|- _ ] a12 r1 in let [h, l:target L[] |- Q] = weakenEnv1 [|- _ ] [|- _ ] [|- _ ] a12 r2 in Result [h, l:target L[] |- ccons P Q] [|- Env3] | [g |- fst M] => let Result r [|- Env] = hcc [g |- M ] sigma in let [h, l:target L[] |- P] = r in Result [h, l:target L[] |- cfst P] [|- Env] | [g |- rst M] => let Result r [|- Env] = hcc [g |- M] sigma in let [h, l:target L |- P] = r in Result [h, l:target L |- crst P] [|- Env] | [g |- nil] => Result [h, l:target unit |- cnil] [|- env_nil] ; rec hoist_cc: [ |- source T] -> [ |- target T] = fn m => let Result [l:target _ |- M] (e : [|- env _ E]) = hcc m (M_id []) in [ |- clet E (\l. M)] ; % Examples let t0 = hoist_cc [ |- app (lam \x.x) z ]; let t1 = hoist_cc [ |- app (lam \x.(app (lam \y.y) x)) z];