% lambda-circle with shift/reset: stage calculus with delimited control % The calculus has arbitrarily many stages, and is an extension of % lambda-circle with delimited control. % The calculus is designed so that we could write Gibonacci, % staged Gibonacci, and let-insertion. % We use the intrinsic encoding of \Meta in LF. The code in this file is % the extension of % Mechanized proofs of type soundness of delimited control % http://okmij.org/ftp/formalizations/index.html#shift % to staging. For simplicity, we don't consider the answer-type modification % however. % We do not distinguish between `pure' and `impure' computations % and types. Therefore, the answer-type is always present. % Sometimes, we may have to insert `reset' to emulate % the answer-type polymorphism. % Notational conventions: % we use suffix 0 to indicate the present stage; and suffix + % for the future stage. For very popular terms and term constructors % such as l (lambda), ? (reset) and @ (application), we drop the suffix 0. % So l means a present-stage lambda and l+ means a future-stage % lambda. Some term constructors like cons are level-polymorphic; % (cons e1 e2) may refer to either present or future computation, depending % on the context. % Primitive types: one so far, integer. % A term N of type nat is a nonnegative integer. % Constructors: 0, 1. nat: type. %name nat N. 0: nat. 1: nat -> nat. %prefix 200 1. % implementation of the addition of two naturals plus : nat -> nat -> nat -> type. %mode plus +N1 +N2 -N3. -: plus 0 N N. -: plus (1 N1) N2 (1 N3) <- plus N1 N2 N3. %worlds () (plus _ _ _). %total {N} (plus N _ _). % predecessor % We make the predecessor total by setting pred 0 to 0 pred : nat -> nat -> type. %mode pred +N1 -N2. -: pred 0 0. -: pred (1 N) N. %worlds () (pred _ _). %total {} (pred _ _). % Types tp: type. %name tp T. int: tp. % one single primitive type for now. % the arrow type: arr t1 t2 t3 is written t1 -> t2/t3 in the paper. % t3 is the answer-type of the body of the function. arr: tp -> tp -> tp -> tp. % product type *: tp -> tp -> tp. %infix none 225 *. % code type ; Ta is the answer-type & : tp -> tp -> tp. % Expressions % Expressions are tagged with the stage level: present stage or future % stage. % We use the intrinsic encoding of the \Meta language in LF, and so % our expressions are typed and bear the explicit type. % Since all expressions are potentially effectful, they are % marked with an answer-type, usually denoted Ta or Ua. % Furthermore, future-stage expressions have several answer-types, one for each % stage. Therefore, we distinguish present vs. future stage expressions % by the number of the answer-types. We do not need any further % stage level annotations. % The definitions below specify not only the syntax of the language, % but also its type system. Type inference is syntax-directed, and % it is indeed tied to syntax. Type judgements are literally specified % alongside the syntax. % fix is an applicative fixpoint combinator, defined as a _polymorphic_ % constant, with the type forall TV. (TV -> TV) -> TV. % Here TV is generally a an arrow type. % The decrement is not in the paper (and is generally expressible via addition) % but we add it anyway. It is convenient, letting us avoid introducing % negative numbers. % Answer type or types; their number indicates the staging level % The present-stage answer-type is at the bottom of the sequence. atp: type. %name atp A. at0: tp -> atp. % present stage %prefix 170 at0. at: tp -> atp -> atp. % future stage exp: tp -> atp -> type. %name exp E. value: exp T A -> type. %name value V. n : nat -> exp int A. %prefix 170 n. % Integer literal + : exp int A -> exp int A -> exp int A. %infix left 100 +. dec: exp int A -> exp int A. % Decrement % Types for bound variables % Variables represent values, in CBV, and hence are % answer-type polymorphic. % Therefore, we abstract the answer-types away and keep % only the level of the value. arg: tp -> nat -> type. arg0: value (_:exp T (at0 _)) -> arg T 0. % present-stage argument arg+: arg T N -> arg T (1 N). % This rule seems bizarre. First of all, we never substitute % for future-stage variables because applications at the future stage % are not evaluated. In the calculus, we use (arg T N) hypothetically, % in the lambda form and hence during the type-checking. % Substitutions in future-stage lambda becomes possible only when % we `demote' them to the present stage, see compile below. % In that case, we will substitute a present-stage value. % present-stage lambda l : (arg T1 0 -> exp T2 (at0 T2a)) -> exp (arr T1 T2 T2a) (at0 _). % future-stage lambda. The present-stage answer-type polymorphism % betrays an explicit reset % A future-stage binder of level N implies reset on all levels % up to and including N-1. % That is, we assume that the body E of the second-stage lambda is % wrapped as ~(? ^ E). % The reset implies (see below) that ^ E : exp TC (at0 TC) % where TC is some code type (& T U). Thus E must be an expression % of the type (exp T (at U (at0 (& T U)))). % % The body E of the third stage lambda is implicitly wrapped as % ~(? ~(? ^ ^ E)). % The innermost reset forces the type of ^^E to be % exp TC (at0 TC). % The type of ~(? ^ ^ E) becomes TC1 (at U1 (at0 _)) % where TC = (& TC1 U1). % Again, the (outermost) reset forces U1 and TC1 to be the same. % Thus we obtain for the type of ^^E: % exp (& TC1 TC1) (at0 (& TC1 TC1)). % Here, TC1 is a code type (& T U), now with no limitation on U. % Thus the type of E : exp T (at U (at TC1 (at0 (& TC1 TC1)))). % The following type family enforces the constraint. l+-cnt: nat -> tp -> atp -> type. l+-cnt1: l+-cnt (1 0) TC (at0 TC). l+-cnt+: l+-cnt (1 N) TC (at TC A) <- l+-cnt N (& TC TC) A. % polyA N A holds if A has exactly N components and N >=1. % The particular answer-types in A are not important -- only % their number. % The polyA is used as a constraint in v+ and l+ below % to relate the level N and the `polymorphic' A (whose answer-types % are all polymorphic). % Since polyA is a constraint on a type of a term, % the term (such as v+ below) includes an object of polyA type % as a witness. The type family polyA has no mode declaration since % the proof object is always needed anyway. polyA : nat -> atp -> type. polyA-0: polyA 0 (at0 _). % The answer-type is arbitrary polyA-+: polyA (1 N) (at _ A) <- polyA N A. % Ditto polyA-1 = polyA-+ polyA-0. % Useful abbreviation l+ : l+-cnt N (& T2 T2a) A -> polyA N AR -> (arg T1 N -> exp T2 (at T2a A)) -> exp (arr T1 T2 T2a) AR. % Variable rules: Implicit answer-type polymorphism v : arg T 0 -> exp T (at0 _). %prefix 170 v. v+ : polyA (1 N) A -> arg T (1 N) -> exp T A. % fix: the polymorphic constant fix: exp (arr (arr (arr T T1 T2) (arr T T1 T2) T2) (arr T T1 T2) _) A. % present-stage application @ : exp (arr T1 T2 Ta) (at0 Ta) -> exp T1 (at0 Ta) -> exp T2 (at0 Ta). %infix left 154 @. % future-stage application @+ : exp (arr T1 T2 Ta) (at Ta A) -> exp T1 (at Ta A) -> exp T2 (at Ta A). %infix left 154 @+. cons: exp T1 A -> exp T2 A -> exp (T1 * T2) A. % standard pair stuff fst : exp (arr (T1 * T2) T1 Ta) A. % constants snd : exp (arr (T1 * T2) T2 Ta) A. % constants ifz: exp int A -> exp T1 A -> exp T1 A -> exp T1 A. % if zero % Staging constructs: brackets and escape ^ : exp T1 (at Ta A) -> exp (& T1 Ta) A. %prefix 170 ^. % aka next ~ : exp (& T1 Ta) A -> exp T1 (at Ta A). %prefix 150 ~. % aka prev % `Iterated' staging constructs % time-shift T1 A1 T2 A2 relates types T1 T2 and answer-type % sequences A1 A2 as if there were two expressions % e1 : exp T1 A1 and e2 : exp T2 A2 and % e1 = ~n e2 (or, equivalently, e2 = ^n e1) % where ~n is the n-time iterated escape ~ (n =0..) % Here are the example of related types % time-shift T A T A % time-shift T (at Ta1 A) (& T Ta1) A % time-shift T (at Ta1 (at Ta2 A)) (& (& T Ta1) Ta2) A % etc. % Proposals for a better name for time-shift are welcome. % The literal implementation % time-shift : exp T1 A1 -> exp T2 A2 -> type. % time-shift-0: time-shift E E. % time-shift-+: time-shift E1 E2 <- time-shift (^ E1) E2. % Now only at the type level % The advantage is that time-shift below no longer depends % on exp. This helps avoid insubordination. time-shift : {T1:tp} {A1:atp} {T2:tp} {A2:atp} type. time-shift-0: time-shift T1 A1 T1 A1. time-shift-+: time-shift T1 (at T2 A1) T3 A2 <- time-shift (& T1 T2) A1 T3 A2. % t1 = time-shift-+ time-shift-0. % t1 : {T1:tp} {T2:tp} {A1:atp} time-shift T1 (at T2 A1) (& T1 T2) A1 % = [T1:tp] [T2:tp] [A1:atp] time-shift-+ time-shift-0. % t2 = time-shift-+ (time-shift-+ time-shift-0). % t2 : % {T1:tp} {T2:tp} {T3:tp} {A1:atp} % time-shift T1 (at T2 (at T3 A1)) (& (& T1 T2) T3) A1 % = [T1:tp] [T2:tp] [T3:tp] [A1:atp] time-shift-+ (time-shift-+ time-shift-0). % Delimited control % deru is used in the bubble-up semantics, internally % The user normally uses 'de' defined below % The typing rule is more general than common because deru % describes the current `bubble'. % Deru exists only at the present-stage, the stage at which % evaluation is happening. deru : time-shift TWH AH TW (at0 Ta) -> (arg T 0 -> exp TW (at0 Ta)) -> % continuation being captured. exp (arr (arr T Ta Ta) Ta Ta) (at0 Ta) -> exp TWH AH. % In the user code, shift is a polymorphic constant de : exp (arr (arr (arr T Ta Ta) Ta Ta) T Ta) A. ? : exp T (at0 T) -> exp T (at0 _). %prefix 150 ?. % reset ?+ : exp T (at T A) -> exp T (at _ A). %prefix 150 ?+. % reset % Abbreviations n0 = n 0. n1 = n 1 0. n2 = n 1 1 0. n3 = n 1 1 1 0. n4 = n 1 1 1 1 0. n5 = n 1 1 1 1 1 0. n6 = n 1 1 1 1 1 1 0. n7 = n 1 1 1 1 1 1 1 0. n8 = n 1 1 1 1 1 1 1 1 0. % second-stage lambda l2 : (arg T1 (1 0) -> exp T2 (at Ta (at0 & T2 Ta))) -> exp (arr T1 T2 Ta) (at _ _) = [body] l+ l+-cnt1 polyA-1 body. v2 = v+ polyA-1. %prefix 170 v2. % third-stage lambda l3 : (arg T1 (1 1 0) -> exp T2 (at Ta (at (& T2 Ta) (at0 & (& T2 Ta) (& T2 Ta))))) -> exp (arr T1 T2 Ta) (at _ _) = [body] l+ (l+-cnt+ l+-cnt1) (polyA-+ polyA-1) body. v3 = v+ (polyA-+ polyA-1). %prefix 170 v3. %abbrev let = [e] [body:arg T1 0 -> exp T2 (at0 T3)] (l body) @ e. % ======================================================================== % examples % dec x + 1> tt11 = (^ (l2 [x] dec (v2 x) + n1)). % < dec x + 1>> tt12 : exp (& (& (arr int int T1) T2) T3) (at0 T4) = ^ ((^ (l3 [x] dec (v3 x) + n1))). % Various fragments of Gibonacci, to test typing tt20 : exp (arr (arr int int T1) (arr int int T1) T2) (at0 T3) = (l [self] l [k] (v self @ (dec (dec (v k))) + v self @ (dec (v k)))). tt2 : exp (arr int int T1) (at0 T2) = (fix @ l [self] l [k] (v self @ (dec (dec (v k))) + v self @ (dec (v k)))). tt2+ : exp (arr int (& int T1) T2) (at0 T3) = (fix @ l [self] l [k] ^ ((~ (v self @ dec (dec (v k)))) + ~ (v self @ dec (v k)))). tt3 : exp (arr int (arr int (arr int int T1) T2) T3) (at0 T4) = l [x] l [y] fix @ l [self] l [k] ifz (v k) (v x) (ifz (dec (v k)) (v y) n0). % The Gibonacci function gib = l [x] l [y] fix @ l [self] l [k] (ifz (v k) (v x) (ifz (dec (v k)) (v y) (v self @ dec (dec (v k)) + v self @ dec (v k)))). % Staged Gibonacci % The same code as in circle-shift-1.elf gibs = l [x] l [y] fix @ l [self] l [k] (ifz (v k) (v x) (ifz (dec (v k)) (v y) (^ (~ (v self @ dec (dec (v k))) + ~ (v self @ dec (v k)))))). % The inferred type: % gibs : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} {T5:tp} % exp (arr (& int T1) (arr (& int T1) (arr int (& int T1) T2) T3) T4) % (at0 T5) gibs3 : exp (& (arr int (arr int int T1) T2) T3) (at0 T4) = ^ (l2 [x] l2 [y] ~ (gibs @ ^ (v2 x) @ ^ (v2 y) @ n3)). % Example from the paper `Closing the Stage': % computing a staged power function while tracking how many % multiplications the generated code performs. % Instead of multiplication, we use addition (so, strictly speaking, % power computes multiplication) % let rec powerc = function % | 0 -> (. 1>.,0) % | 1 -> (. x>.,1) % | m -> let (c,k) = powerc (pred m) in % (. (.~c x) * x>.,succ k) %% val powerc : int -> ('a, int -> int) code * int = powerc : exp (arr int (& (arr int int T1) T1 * int) T2) (at0 T3) = fix @ l [self] l [m] (ifz (v m) (cons (^ (l2 [x] n0)) n0) (let ((v self) @ (dec (v m))) [ck] (cons (^ (l2 [x] ((~(fst @ v ck)) @+ (v2 x)) + (v2 x))) ((snd @ v ck) + n1)))). % Using several levels, to avoid beta-redices in the code % eventually generated % let mul x y = .<.<.~.~x * .~.~y>.>.;; % val mul : % ('a, ('b, int) code) code -> % ('a, ('b, int) code) code -> ('a, ('b, int) code) code = addss : exp (arr (& (& int T1) T2) (arr (& (& int T1) T2) (& (& int T1) T2) T3) T4) (at0 T5) = l [x] l [y] ^ ^ ((~ ~ (v x)) + (~ ~ (v y))). % let rec powerd = function % | 0 -> (. .<1>.>.,0) % | 1 -> (. x>.,1) % | m -> let (c,k) = powerd (pred m) in % (. .~(mul .<.~c x>. ..)>.,succ k) % val powerd : int -> ('a, ('b, int) code -> ('b, int) code) code * int = powerd : exp (arr int (& (arr (& int T1) (& int T1) T2) T2 * int) T3) (at0 T4) = fix @ l [self] l [m] (ifz (v m) (cons (^ (l2 [x] ^ n0)) n0) (let ((v self) @ (dec (v m))) [ck] (cons (^ (l2 [x] ~(addss @ (^((~(fst @ v ck)) @+ (v2 x))) @ ^(v2 x)))) ((snd @ v ck) + n1)))). % Staging and delimited control sst1 : exp (& (& int T1) T2) (at0 T3) = ? (^ ^ (n1 + ~ ~ (de @ l [sk] (v sk) @ ^ ^ n2))). % The type is pure with no outer reset... sst2 : exp (& (& (arr T1 int T2) T3) T4) (at0 _) = (^ ^ (l3 [x] ~ ~ (de @ l [sk] (v sk) @ ^ ^ n2))). % ======================================================================== % Dynamic Semantics % ---------------------------------------------------------------------- % Some expressions are classified as values. See the figure % ``Values and contexts'' of the paper. The valuehood depends on the % stage. % value: exp T A -> type. %name value V. %mode value +E. %block bl-ev : some {T:tp} {N:nat} block {e:arg T (1 N)}. val-n: value (n _). % Literals are values at any level val-f: value fix. % A constant: trivially a value val-r: value de. % A constant: trivially a value val-F: value fst. % A constant: trivially a value val-S: value snd. % A constant: trivially a value % values at the present level val-l0: value (l _). val-c: value (cons E1 E2) % A pair of values is a value, at <- value E2 % every level. <- value E1. % Homomorphisms at any level val-^: value (^ E) <- value E. val-V+: value (v+ _ _). % Future variable references aren't % evaluated at the present stage % Values at the non-empty level: basically, the absence of 0-level escapes % homomorphisms... val-l+: value (l+ _ _ E) <- {x:arg T1 (1 _)} value (E x). val-@+: value (E1 @+ E2) <- value E2 <- value E1. val-++: value ((E1 + E2) : exp _ (at _ _)) <- value E2 <- value E1. val-d+: value ((dec E) : exp _ (at _ _)) <- value E. val-i+: value ((ifz E1 E2 E3) : exp _ (at _ _)) <- value E3 <- value E2 <- value E1. val-?+: value (?+ E) <- value E. % 0-level escape is certainly not a value. However, an escape from % level 2 to level 1 is a value. val-~+: value (~ (E : exp _ (at _ _))) <- value E. %worlds (bl-ev) (value _). %terminates {E} (value E). % Since values aren't further evaluated, they can't cause any effect % and so are (present-stage) answer-type polymorphic. % In other words, we can change the present-stage answer-type % to some other one. The following function does the conversion, % witnessing the answer-type polymorphism. % Update the level-0 type in the stack of answer-types atp to a given % type tp. at-new-at0: atp -> tp -> atp -> type. %mode at-new-at0 +A1 +T -A2. at-new-at0-0: at-new-at0 (at0 _) TN (at0 TN). at-new-at0-+: at-new-at0 (at T A) TN (at T A') <- at-new-at0 A TN A'. %worlds (bl-ev) (at-new-at0 _ _ _). %total {A} (at-new-at0 A _ _). % apply at-new-at0 to polyA proof object. Since it doesn't constrain % the answer types themselves (only their number), the application % is straightforward. at-new-at0-polyA: polyA (1 N) (at T1 A) -> at-new-at0 A T A1 -> polyA (1 N) (at T1 A1) -> type. %mode at-new-at0-polyA +P1 +A -P2. -: at-new-at0-polyA polyA-1 _ polyA-1. -: at-new-at0-polyA (polyA-+ P) (at-new-at0-+ A) (polyA-+ P') <- at-new-at0-polyA P A P'. %worlds (bl-ev) (at-new-at0-polyA _ _ _). %total {P} (at-new-at0-polyA P _ _). val-new-at+: value (_:exp T (at Ta A)) -> at-new-at0 A TN AN -> exp T (at Ta AN) -> type. %mode val-new-at+ +V +PA -E. -: val-new-at+ (val-n: value (n N)) _ (n N). -: val-new-at+ val-f _ fix. -: val-new-at+ val-r _ de. -: val-new-at+ val-F _ fst. -: val-new-at+ val-S _ snd. -: val-new-at+ (val-V+ : value (v+ P V)) AN (v+ P1 V) <- at-new-at0-polyA P AN P1. -: val-new-at+ (val-c VE1 VE2) AN (cons E1 E2) <- val-new-at+ VE1 AN E1 <- val-new-at+ VE2 AN E2. -: val-new-at+ ((val-l+ _): value (l+ LC P E)) AN (l+ LC P1 E) <- at-new-at0-polyA P AN P1. -: val-new-at+ (val-@+ VE1 VE2) AN (E1 @+ E2) <- val-new-at+ VE1 AN E1 <- val-new-at+ VE2 AN E2. -: val-new-at+ (val-d+ VE) AN (dec E) <- val-new-at+ VE AN E. -: val-new-at+ (val-++ VE1 VE2) AN (E1 + E2) <- val-new-at+ VE1 AN E1 <- val-new-at+ VE2 AN E2. -: val-new-at+ (val-i+ VE1 VE2 VE3) AN (ifz E1 E2 E3) <- val-new-at+ VE1 AN E1 <- val-new-at+ VE2 AN E2 <- val-new-at+ VE3 AN E3. -: val-new-at+ (val-?+ VE) AN (?+ E) <- val-new-at+ VE AN E. -: val-new-at+ (val-^ VE) AN (^ E) <- val-new-at+ VE (at-new-at0-+ AN) E. -: val-new-at+ (val-~+ VE) (at-new-at0-+ AN) (~ E) <- val-new-at+ VE AN E. %worlds (bl-ev) (val-new-at+ _ _ _). %total {V} (val-new-at+ V _ _). val-new-at: value (_:exp T (at0 Ta)) -> {TaN:tp} exp T (at0 TaN) -> type. %mode val-new-at +V +T -E. -: val-new-at (val-n: value (n N)) _ (n N). -: val-new-at val-f _ fix. -: val-new-at val-r _ de. -: val-new-at val-F _ fst. -: val-new-at val-S _ snd. -: val-new-at (val-l0 : value (l E)) _ (l E). -: val-new-at (val-c VE1 VE2) TaN (cons E1 E2) <- val-new-at VE1 TaN E1 <- val-new-at VE2 TaN E2. -: val-new-at (val-^ VE) TaN (^ E) <- val-new-at+ VE at-new-at0-0 E. %worlds (bl-ev) (val-new-at _ _ _). %total {V} (val-new-at V _ _). % Making sure the generated code is correct % Shorten the sequence of answer-types by chopping off the at0 % (present stage) answer-type, that is, the answer type at the far right. % In other words, we convert (at T A) to A' such that A' is obtained % from (at T A) by chopping off the right-most answer-type. chop-at0 : tp -> atp -> atp -> type. %mode chop-at0 +T +A -A'. chat0-0: chop-at0 T (at0 _) (at0 T). chat0-+: chop-at0 T (at U A) (at T A') <- chop-at0 U A A'. %worlds () (chop-at0 _ _ _). %total {A} (chop-at0 _ A _). % If the answer-type sequence A has the length (1 N) and the % sequence A' is obtained from A by chopping off the right-most % answer-type, then A' has the length N. % We produce the proof that A' has the length N, in the form % of a proof object polyA N A'. decr-polyA: polyA (1 N) (at U (at U1 A1)) -> chop-at0 U (at U1 A1) A' -> polyA N A' -> type. %mode decr-polyA +P1 +C -P2. -: decr-polyA (polyA-+ polyA-1) (chat0-+ chat0-0) polyA-1. -: decr-polyA (polyA-+ (polyA-+ P)) (chat0-+ C) (polyA-+ P') <- decr-polyA (polyA-+ P) C P'. %worlds () (decr-polyA _ _ _). %total {P} (decr-polyA P _ _). % ---------------------------------------------------------------------- % Some expressions are classified as non-values. The present-stage % deru (the continuation bubble) is neither a value nor a non-value. % Naming conventions for the rules in the code below: % suffix: C is for a congruence rule % R for bubble propagating through the present-stage code non-value: exp T A -> type. %name non-value R. %mode non-value +E. nv-d: non-value ((dec E): exp _ (at0 _)) <- value E. nv-dC: non-value (dec E) <- non-value E. nv-dR: non-value (dec (deru TS C E)). nv-+: non-value ((E1 + E2): exp _ (at0 _)) <- value E2 <- value E1. nv-+C1: non-value (E1 + E2) <- non-value E1. nv-+C2: non-value (E1 + E2) <- non-value E2 <- value E1. nv-+R1: non-value ((deru TS C1 E1) + E2). nv-+R2: non-value (E1 + (deru TS C2 E2)).% This is the last clause: no need % to ensure that E1 is a value % because the cases of E1 being % a non-value or deru have been covered % already. % nv-+R2: non-value (E1 + (deru TS C2 E2)) % This clause is better (non- % <- value E1. % overlapping), but slower. nv-V: non-value (v _). nv-cC1: non-value (cons E1 E2) <- non-value E1. nv-cC2: non-value (cons E1 E2) <- non-value E2 <- value E1. nv-cR1: non-value (cons (deru TS C1 E1) E2). nv-cR2: non-value (cons E1 (deru TS C2 E2)). nv-i: non-value ((ifz E E1 E2): exp _ (at0 _)) <- value E. nv-iC: non-value (ifz E E1 E2) <- non-value E. nv-iC1: non-value ((ifz E E1 E2): exp _ (at _ _)) <- non-value E1 <- value E. nv-iC2: non-value ((ifz E E1 E2): exp _ (at _ _)) <- non-value E2 <- value E1 <- value E. nv-iR: non-value (ifz (deru TS C E) E1 E2). nv-iR1: non-value (ifz E ((deru TS C1 E1) : exp _ (at _ _)) E2). nv-iR2: non-value (ifz E E1 ((deru TS C2 E2) : exp _ (at _ _))). nv-@: non-value (E1 @ E2) <- value E2 <- value E1. nv-@C1: non-value (E1 @ E2) <- non-value E1. nv-@C2: non-value (E1 @ E2) <- non-value E2 <- value E1. nv-@R1: non-value ((deru TS C1 E1) @ E2). nv-@R2: non-value (E1 @ (deru TS C2 E2)). nv-?: non-value ((? E): exp _ (at0 _)) <- value E. nv-?C: non-value (? E) <- non-value E. nv-?R: non-value (? (deru TS C E)). nv-~: non-value (~ E) <- value (E : exp _ (at0 _)). nv-~C: non-value (~ E) <- non-value E. nv-~R: non-value (~ (deru TS C E)). nv-^C: non-value (^ E) <- non-value E. nv-^R: non-value (^ (deru TS C E)). nv-?+C: non-value (?+ E) <- non-value E. nv-?+R: non-value (?+ (deru TS C E)). nv-l+C: non-value (l+ _ _ E) <- {x:arg T (1 _)} non-value (E x). nv-l+R: non-value (l+ LC _ [x] (deru TS ([x1:arg TC 0] _) _)). % Inferred type: % nv-l+R : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} {A1:atp} {N1:nat} {A2:atp} % {LC:l+-cnt N1 T2 T3 A2} {T5:tp} {T6:tp} {TC:tp} % {TS:time-shift T2 (at T3 A2) T5 (at0 T6)} % {E1:arg T1 N1 -> arg TC 0 -> exp T5 (at0 T6)} % {E2:arg T1 N1 -> exp (arr (arr TC T6 T6) T6 T6) (at0 T6)} % non-value (l+ LC ([x:arg T1 N1] deru TS ([x1:arg TC 0] E1 x x1) (E2 x))). % E1 and E2 depend on x! That's important for the coverage of vclassify % The underscores (rather than implicit names) in the above expression % are critically important! nv-@+C1: non-value (E1 @+ E2) <- non-value E1. nv-@+C2: non-value (E1 @+ E2) <- non-value E2 <- value E1. nv-@+R1: non-value ((deru TS C1 E1) @+ E2). nv-@+R2: non-value (E1 @+ (deru TS C2 E2)). %worlds (bl-ev) (non-value _). %terminates {E} (non-value E). % ---------------------------------------------------------------------- % The following constructively proves that each expression is % either a value, deru, or non-value. % The following is purely automatic, and auxiliary % relations vclassify-@ and vclassify-z are defined only because % Twelf's output coverage checker can't deal with pattern-matching % on output arguments . vhood: exp T A -> type. a-value : vhood E <- value E. a-deru : vhood (deru TS C E). a-non-value : vhood E <- non-value E. vclassify: {E:exp T A} vhood E -> type. %mode vclassify +E -P. -: vclassify _ a-deru. -: vclassify _ (a-value val-n). % Classify the constants -: vclassify _ (a-value val-f). -: vclassify _ (a-value val-r). -: vclassify _ (a-value val-F). -: vclassify _ (a-value val-S). -: vclassify _ (a-value val-l0). -: vclassify _ (a-non-value nv-V). -: vclassify _ (a-value val-V+). vclassify-dec: vhood E -> vhood (dec E) -> type. %mode vclassify-dec +VE1 -VE. -: vclassify-dec (a-value V) (a-value (val-d+ V)). -: vclassify-dec (a-value V) (a-non-value (nv-d V)). -: vclassify-dec (a-non-value NV) (a-non-value (nv-dC NV)). -: vclassify-dec a-deru (a-non-value nv-dR). %worlds (bl-ev) (vclassify-dec _ _). %total {} (vclassify-dec _ _). -: vclassify (dec E) VH <- vclassify E VE <- vclassify-dec VE VH. vclassify-?: vhood E -> {Ta:tp} non-value ((? E): exp _ (at0 Ta)) -> type. %mode vclassify-? +VE1 +Ta -VE. -: vclassify-? (a-value V) _ (nv-? V). -: vclassify-? (a-non-value NV) _ (nv-?C NV). -: vclassify-? a-deru _ nv-?R. %worlds (bl-ev) (vclassify-? _ _ _). %total {} (vclassify-? _ _ _). -: vclassify ((? E): exp _ (at0 Ta)) (a-non-value NV) <- vclassify E VE <- vclassify-? VE Ta NV. vclassify-?+: vhood E -> {Ua:tp} vhood ((?+ E): exp _ (at Ua _)) -> type. %mode vclassify-?+ +VE1 +Ua -VE. -: vclassify-?+ (a-value V) _ (a-value (val-?+ V)). -: vclassify-?+ (a-non-value NV) _ (a-non-value (nv-?+C NV)). -: vclassify-?+ a-deru _ (a-non-value nv-?+R). %worlds (bl-ev) (vclassify-?+ _ _ _). %total {} (vclassify-?+ _ _ _). -: vclassify (?+ E) VH <- vclassify E VE <- vclassify-?+ VE _ VH. vclassify-@0: vhood E1 -> vhood E2 -> non-value (E1 @ E2) -> type. %mode vclassify-@0 +VE1 +VE2 -VE. -: vclassify-@0 (a-value V1) (a-value V2) (nv-@ V1 V2). -: vclassify-@0 a-deru _ nv-@R1. -: vclassify-@0 _ a-deru nv-@R2. -: vclassify-@0 (a-non-value NV1) _ (nv-@C1 NV1). -: vclassify-@0 (a-value V1) (a-non-value NV2) (nv-@C2 V1 NV2). %worlds (bl-ev) (vclassify-@0 _ _ _). %total {} (vclassify-@0 _ _ _). -: vclassify (E1 @ E2) (a-non-value NV) <- vclassify E1 VE1 <- vclassify E2 VE2 <- vclassify-@0 VE1 VE2 NV. vclassify-@+: vhood E1 -> vhood E2 -> vhood (E1 @+ E2) -> type. %mode vclassify-@+ +VE1 +VE2 -VE. -: vclassify-@+ (a-non-value NV1) _ (a-non-value (nv-@+C1 NV1)). -: vclassify-@+ (a-value V1) (a-non-value NV2) (a-non-value (nv-@+C2 V1 NV2)). -: vclassify-@+ (a-value V1) (a-value V2) (a-value (val-@+ V1 V2)). -: vclassify-@+ a-deru _ (a-non-value nv-@+R1). -: vclassify-@+ _ a-deru (a-non-value nv-@+R2). %worlds (bl-ev) (vclassify-@+ _ _ _). %total {} (vclassify-@+ _ _ _). -: vclassify (E1 @+ E2) VH <- vclassify E1 VE1 <- vclassify E2 VE2 <- vclassify-@+ VE1 VE2 VH. vclassify-+: vhood E1 -> vhood E2 -> vhood (E1 + E2) -> type. %mode vclassify-+ +VE1 +VE2 -VE. -: vclassify-+ (a-value V1) (a-value V2) (a-non-value (nv-+ V1 V2)). -: vclassify-+ (a-non-value NV1) _ (a-non-value (nv-+C1 NV1)). -: vclassify-+ (a-value V1) (a-non-value NV2) (a-non-value (nv-+C2 V1 NV2)). -: vclassify-+ (a-value V1) (a-value V2) (a-value (val-++ V1 V2)). -: vclassify-+ a-deru _ (a-non-value nv-+R1). -: vclassify-+ _ a-deru (a-non-value nv-+R2). %worlds (bl-ev) (vclassify-+ _ _ _). %total {} (vclassify-+ _ _ _). -: vclassify (E1 + E2) VH <- vclassify E1 VE1 <- vclassify E2 VE2 <- vclassify-+ VE1 VE2 VH. vclassify-c: vhood E1 -> vhood E2 -> vhood (cons E1 E2) -> type. %mode vclassify-c +VE1 +VE2 -VE. -: vclassify-c (a-value V1) (a-value V2) (a-value (val-c V1 V2)). -: vclassify-c (a-non-value NV1) _ (a-non-value (nv-cC1 NV1)). -: vclassify-c (a-value V1) (a-non-value NV2) (a-non-value (nv-cC2 V1 NV2)). -: vclassify-c a-deru _ (a-non-value nv-cR1). -: vclassify-c _ a-deru (a-non-value nv-cR2). %worlds (bl-ev) (vclassify-c _ _ _). %total {} (vclassify-c _ _ _). -: vclassify (cons E1 E2) VH <- vclassify E1 VE1 <- vclassify E2 VE2 <- vclassify-c VE1 VE2 VH. vclassify-i: vhood E -> vhood E1 -> vhood E2 -> vhood (ifz E E1 E2) -> type. %mode vclassify-i +VE +VE1 +VE2 -VER. -: vclassify-i (a-value V) _ _ (a-non-value (nv-i V)). -: vclassify-i (a-non-value NV) _ _ (a-non-value (nv-iC NV)). -: vclassify-i (a-value V) (a-value V1) (a-value V2) (a-value (val-i+ V V1 V2)). -: vclassify-i (a-value V) (a-non-value NV1) _ (a-non-value (nv-iC1 V NV1)). -: vclassify-i (a-value V) (a-value V1) (a-non-value NV2) (a-non-value (nv-iC2 V V1 NV2)). -: vclassify-i a-deru _ _ (a-non-value nv-iR). -: vclassify-i _ a-deru _ (a-non-value nv-iR1). -: vclassify-i _ _ a-deru (a-non-value nv-iR2). %worlds (bl-ev) (vclassify-i _ _ _ _). %total {} (vclassify-i _ _ _ _). -: vclassify (ifz E E1 E2) VH <- vclassify E VE <- vclassify E1 VE1 <- vclassify E2 VE2 <- vclassify-i VE VE1 VE2 VH. vclassify-~: vhood E -> vhood (~ E) -> type. %mode vclassify-~ +VE1 -VE. -: vclassify-~ ((a-value V) : vhood (_: exp _ (at0 _))) (a-non-value (nv-~ V)). -: vclassify-~ ((a-value V) : vhood (_: exp _ (at _ _))) (a-value (val-~+ V)). -: vclassify-~ a-deru (a-non-value nv-~R). -: vclassify-~ (a-non-value NV) (a-non-value (nv-~C NV)). %worlds (bl-ev) (vclassify-~ _ _). %total {} (vclassify-~ _ _). -: vclassify (~ E) VH <- vclassify E VE <- vclassify-~ VE VH. vclassify-^: vhood E -> vhood (^ E) -> type. %mode vclassify-^ +VE1 -VE. -: vclassify-^ (a-value V) (a-value (val-^ V)). -: vclassify-^ a-deru (a-non-value nv-^R). -: vclassify-^ (a-non-value NV) (a-non-value (nv-^C NV)). %worlds (bl-ev) (vclassify-^ _ _). %total {} (vclassify-^ _ _). -: vclassify (^ E) VH <- vclassify E VE <- vclassify-^ VE VH. vclassify-l+: ({x:arg T (1 _)} vhood (E x)) -> {LC:l+-cnt (1 N) _ _} {P:polyA (1 N) A} vhood (l+ LC P E) -> type. %mode vclassify-l+ +VE1 +LC +P -VE. -: vclassify-l+ ([x] (a-value (V x))) _ _ (a-value (val-l+ V)). -: vclassify-l+ ([x] (a-non-value (NV x))) _ _ (a-non-value (nv-l+C NV)). -: vclassify-l+ ([x] a-deru) _ _ (a-non-value nv-l+R). %worlds (bl-ev) (vclassify-l+ _ _ _ _). %total {} (vclassify-l+ _ _ _ _). -: vclassify (l+ LC P E) VH <- ({x:arg T (1 _)} vclassify (E x) (VE x)) <- vclassify-l+ VE LC _ VH. %worlds (bl-ev) (vclassify _ _). %total {E} (vclassify E _). % ---------------------------------------------------------------------- % Transitions % The function eval is only defined on non-values. Since deru is % not a non-value, the naked shift cannot be reduced. % Since we use the intrinsic encoding, the type of eval expresses % the subject reduction property. % If the relation time-shift T1 A1 T2 A2 holds, then % we can for each expression of the type exp T1 A1 we can compute % the expression of the type exp T2 A2 (by applying a number of ^ operations) % and conversely. The following type family computes these conversions % (coercions) and constructively proves the claim. ts-coercions : time-shift T1 A1 T2 A2 -> (exp T1 A1 -> exp T2 A2) -> (exp T2 A2 -> exp T1 A1) -> type. %mode ts-coercions +TS -C1 -C2. -: ts-coercions time-shift-0 ([x] x) ([x] x). -: ts-coercions (time-shift-+ TS) ([x] (C1 ^ x)) ([x] ~ (C2 x)) <- ts-coercions TS C1 C2. %worlds (bl-ev) (ts-coercions _ _ _). %total {TS} (ts-coercions TS _ _). % if (T1,A1) and (T2,A2) are stage-related, % impose the same relationship on (T1',A1) and (T2',A2') % That is, replace the other-than-the-answer-type type ts-copy : time-shift T1 A1 T2 A2 -> {T1':tp} time-shift T1' A1 T2' A2 -> type. %mode ts-copy +TS1 +T1' -TS2. -: ts-copy time-shift-0 _ time-shift-0. -: ts-copy ((time-shift-+ TS1) : time-shift _ (at Ta _) _ _) T1 (time-shift-+ TS2) <- ts-copy TS1 (& T1 Ta) TS2. %worlds () (ts-copy _ _ _). %total {TS1} (ts-copy TS1 _ _). eval : {E: exp T A} non-value E -> exp T A -> type. %mode eval +E1 +NV -E2. ev-dZ: eval (dec (n 0)) (nv-d _) (n 0). % to keep dec total, we assume ev-dN: eval (dec (n (1 N))) (nv-d _) (n N). % that dec 0 is 0 ev-dC: eval (dec E) (nv-dC NV) (dec E') <- eval E NV E'. ev-dR: eval (dec (deru TS C E)) nv-dR (deru TS ([x] Down (dec (Up (C x)))) E) <- ts-coercions TS Down Up. % When a bound variable is used in an expression, we assign % expression's answer-type to the value being substituted. ev-V: eval (v (arg0 V)) nv-V E' <- val-new-at V _ E'. % beta-rule ev-@: eval ((l E1) @ E2) (nv-@ _ V2) (E1 (arg0 V2)). % delta-rules ev-@F: eval (fst @ cons E1 _) (nv-@ _ _) E1. ev-@S: eval (snd @ cons _ E2) (nv-@ _ _) E2. % the following darn subtle example shows the need for val-new-at % in the ev-@f rule below: % ti = (? (fix @ (l [self] l [_] n1))). % ev-@f: eval (fix @ E) (nv-@ _ V) (l [x] E' @ (fix @ E') @ (v x)) % <- val-new-at V _ E'. % ev-@f: eval (fix @ l E) (nv-@ _ _) ((l E) @ (l [x] fix @ (l E) @ (v x))). % Inferred type: % ev-@f : % {T1:tp} {T2:tp} {T3:tp} % {E:arg0 (arr T1 T2 T3) -> exp (arr T1 T2 T3) (at0 T3)} {V1:value fix} % {V2:value (l ([x:arg0 (arr T1 T2 T3)] E x))} % eval (fix @ l ([x:arg0 (arr T1 T2 T3)] E x)) (nv-@ V1 V2) % (l ([x:arg0 (arr T1 T2 T3)] E x) % @ l ([x:arg0 T1] fix @ l ([x1:arg0 (arr T1 T2 T3)] E x1) @ v x)). % However, we get around the problem of implicit types being entangled % by using (l E) instead of E % ev-@f: eval (fix @ l E) (nv-@ _ _) (l [x] (l E) @ (fix @ (l E)) @ (v x)). % Now % ev-@f : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} % {E:arg0 (arr T1 T2 T3) -> exp (arr T1 T2 T3) (at0 T3)} {V1:value fix} % {V2:value (l ([x:arg0 (arr T1 T2 T3)] E x))} % eval (fix @ l ([x:arg0 (arr T1 T2 T3)] E x)) (nv-@ V1 V2) % (l % ([x:arg0 T1] % l ([x1:arg0 (arr T1 T2 T3)] E x1) % @ (fix @ l ([x1:arg0 (arr T1 T2 T3)] E x1)) @ v x)). % Notice {T4:tp}, which was not present before. We need it! ev-@f: eval (fix @ l E) (nv-@ _ _) (l [x] (l E) @ (l [x] fix @ (l E) @ v x) @ (v x)). % The initial bubble ev-@r: eval (de @ E) (nv-@ _ _) (deru time-shift-0 ([x] (v x)) E). ev-@C1: eval (E1 @ E2) (nv-@C1 NV1) (E1' @ E2) <- eval E1 NV1 E1'. ev-@C2: eval (E1 @ E2) (nv-@C2 _ NV2) (E1 @ E2') <- eval E2 NV2 E2'. ev-@R1: eval ((deru TS C E) @ E2) nv-@R1 (deru time-shift-0 ([x] (C x) @ E2) E). ev-@R2: eval (E1 @ (deru TS C E)) nv-@R2 (deru time-shift-0 ([x] E1 @ (C x)) E). ev-+: eval ((n N1) + (n N2)) (nv-+ _ _) (n N3) <- plus N1 N2 N3. ev-+C1: eval (E1 + E2) (nv-+C1 NV1) (E1' + E2) <- eval E1 NV1 E1'. ev-+C2: eval (E1 + E2) (nv-+C2 _ NV2) (E1 + E2') <- eval E2 NV2 E2'. ev-+R1: eval ((deru TS C E) + E2) nv-+R1 (deru TS ([x] Down (Up (C x) + E2)) E) <- ts-coercions TS Down Up. ev-+R2: eval (E1 + (deru TS C E)) nv-+R2 (deru TS ([x] Down (E1 + Up (C x))) E) <- ts-coercions TS Down Up. ev-cC1: eval (cons E1 E2) (nv-cC1 NV1) (cons E1' E2) <- eval E1 NV1 E1'. ev-cC2: eval (cons E1 E2) (nv-cC2 _ NV2) (cons E1 E2') <- eval E2 NV2 E2'. ev-cR1: eval (cons (deru TS C E) E2) nv-cR1 (deru TS1 ([x] Down1 (cons (Up (C x)) E2)) E) <- ts-copy TS _ TS1 <- ts-coercions TS Down Up <- ts-coercions TS1 Down1 Up1. ev-cR2: eval (cons E1 (deru TS C E)) nv-cR2 (deru TS1 ([x] Down1 (cons E1 (Up (C x)))) E) <- ts-copy TS _ TS1 <- ts-coercions TS Down Up <- ts-coercions TS1 Down1 Up1. ev-iZ: eval (ifz (n 0) E1 E2) (nv-i _) E1. ev-iN: eval (ifz (n 1 _) E1 E2) (nv-i _) E2. ev-iC: eval (ifz E E1 E2) (nv-iC NV) (ifz E' E1 E2) <- eval E NV E'. ev-iC1: eval (ifz E E1 E2) (nv-iC1 _ NV1) (ifz E E1' E2) <- eval E1 NV1 E1'. ev-iC2: eval (ifz E E1 E2) (nv-iC2 _ _ NV2) (ifz E E1 E2') <- eval E2 NV2 E2'. ev-iR: eval (ifz (deru TS C E) E1 E2) nv-iR (deru TS1 ([x] Down1 (ifz (Up (C x)) E1 E2)) E) <- ts-copy TS _ TS1 <- ts-coercions TS _ Up <- ts-coercions TS1 Down1 _. ev-iR1: eval (ifz E (deru TS C1 E1) E2) nv-iR1 (deru TS1 ([x] Down1 (ifz E (Up (C1 x)) E2)) E1) <- ts-copy TS _ TS1 <- ts-coercions TS _ Up <- ts-coercions TS1 Down1 _. ev-iR2: eval (ifz E E1 (deru TS C2 E2)) nv-iR2 (deru TS1 ([x] Down1 (ifz E E1 (Up (C2 x)))) E2) <- ts-copy TS _ TS1 <- ts-coercions TS _ Up <- ts-coercions TS1 Down1 _. % Reset brings answer-type polymorphism, constructively ev-?: eval (? E) (nv-? V) E' <- val-new-at V _ E'. ev-?C: eval (? E) (nv-?C NV) (? E') <- eval E NV E'. ev-?R: eval (? (deru _ C E)) nv-?R (? (E @ (l [x] (? (C x))))). ev-~: eval (~ ^ E) (nv-~ _) E. ev-~C: eval (~ E) (nv-~C NV) (~ E') <- eval E NV E'. ev-~R: eval (~ (deru TS C E)) nv-~R (deru (time-shift-+ TS) C E). ev-^C: eval (^ E) (nv-^C NV) (^ E') <- eval E NV E'. ev-^R: eval (^ (deru (time-shift-+ TS) C E)) nv-^R (deru TS C E). ev-?+C: eval (?+ E) (nv-?+C NV) (?+ E') <- eval E NV E'. ev-?+R: eval (?+ (deru (time-shift-+ TS) C E)) nv-?+R (deru (time-shift-+ TS1) ([x] Down1 (?+ Up (C x))) E) <- ts-copy TS _ TS1 <- ts-coercions (time-shift-+ TS) _ Up <- ts-coercions (time-shift-+ TS1) Down1 _. ev-@+C1: eval (E1 @+ E2) (nv-@+C1 NV1) (E1' @+ E2) <- eval E1 NV1 E1'. ev-@+C2: eval (E1 @+ E2) (nv-@+C2 _ NV2) (E1 @+ E2') <- eval E2 NV2 E2'. ev-@+R1: eval ((deru TS C E) @+ E2) nv-@+R1 (deru TS1 ([x] Down1 ((Up (C x)) @+ E2)) E) <- ts-copy TS _ TS1 <- ts-coercions TS _ Up <- ts-coercions TS1 Down1 _. ev-@+R2: eval (E1 @+ (deru TS C E)) nv-@+R2 (deru TS1 ([x] Down1 (E1 @+ Up (C x))) E) <- ts-copy TS _ TS1 <- ts-coercions TS _ Up <- ts-coercions TS1 Down1 _. ev-l+C: eval (l+ LC P E) (nv-l+C NV) (l+ LC P E') <- {x:arg T (1 _)} eval (E x) (NV x) (E' x). % Now we recall that a future-stage lambda implies reset on all lower % stages. The type family l+-cnt enforced that constraint. % Therefore, if (l+-cnt N (& T Ta) A) holds and if % (time-shift T (at Ta A) Tl (at0 Ta1)) holds, we can conclude % that Ta1 is the same as Tl and furthermore, we can splice % exp Tl (at0 Ta1) into exp T (at Ta A) with the right number of % escapes. The following construction proves the claim. % The claim is necessary to evaluate the escapes in the body of the % future-stage lambda. ts-escape : l+-cnt N (& T Ta) A -> time-shift T (at Ta A) Tl (at0 Ta1) -> (exp Tl (at0 Ta1) -> exp Tl (at0 Tl)) -> (exp Tl (at0 Ta1) -> exp T (at Ta A)) -> type. %mode ts-escape +LC +TS -Eq -C. -: ts-escape l+-cnt1 (time-shift-+ time-shift-0) ([x] x) ([x] ~ x). -: ts-escape (l+-cnt+ LC) (time-shift-+ TS) Eq ([x] ~ (C x)) <- ts-escape LC TS Eq C. %worlds (bl-ev) (ts-escape _ _ _ _). %total (LC) (ts-escape LC _ _ _). ev-l+R: eval (l+ LC P [x] (deru TS (C x) (E x))) nv-l+R (l+ LC P [x] (Up (? (Eq (deru time-shift-0 (C x) (E x)))))) <- ts-escape LC TS Eq Up. %worlds (bl-ev) (eval _ _ _). %total {E} (eval E _ _). %% Eval is total! we have proven progress: %% Every typed non-value can be reduced. % transitive reflexive closure of eval eval* : exp E (at0 T) -> exp E (at0 T) -> type. %mode eval* +E1 -E2. -: eval* E E <- value E. -: eval* E1 E2 <- vclassify E1 (a-non-value NV) <- eval E1 NV E1' <- eval* E1' E2. % ------------------------------------------------------------------------ % Running sample code %query 1 2 eval* (gib @ n1 @ n1 @ n1) n1. %query 1 2 eval* (gib @ n1 @ n1 @ n3) n3. % %query 1 2 eval* (gib @ n1 @ n1 @ n4) n5. % %query 1 2 eval* (gib @ n1 @ n1 @ n5) n8. % takes a bit of time % takes a while % %query 1 1 eval* (gibs @ ^ n2 @ ^ n3 @ n3) R. % R = ^ (n3 + (n2 + n3)). % takes too long!! % %query 1 1 eval* gibs3 % (^ l2 ([x:arg+ int] l2 ([x1:arg+ int] v+ x1 + (v+ x + v+ x1)))). % tests of shift ts1 = ? n0. ts2 = ? (de @ (l [f] (v f @ n0))). ts3 = ? ((de @ (l [f] (v f @ (l [x] (v x + n1))))) @ (n 0)). %query 1 2 eval* ts1 n0. %query 1 2 eval* ts2 n0. %query 1 2 eval* ts3 n1. % Danvy/Filinski's famous example ts4 = ? (n1 + (? (n1 + (de @ (l [f] (n1 + (n1 + (v f @ (v f @ n0)))))) + n1))). %query 1 2 eval* ts4 n7. % Checking CBV: the argument must be evaluated before the substitution ts6' = (l [x] n1) @ (de @ (l [f] n0)). %%query 1 2 eval* ts6' R. %query 1 2 eval* (? ts6') n0. % checking that our shift is shift indeed % We have to fix the answer-type in g, to anything, because there % is no context to determine it, and Twelf doesn't like the remaining variable. ts01 = ? (de @ (l [f] (de @ (l [g:arg (arr _ _ int) 0] n0)))). %query 1 2 eval* ts01 n0. ts02 = ? ((de @ (l [f] (n2 + (v f @ (l [x] v x + n1))))) @ (de @ (l [_] n1))). %query 1 2 eval* ts02 n3. % This also shows the change in the answer-type... ts03 = ? ((de @ (l [f] (v f @ (l [x] v x + n1)))) @ (de @ (l [g] (v g @ n1)))). %query 1 2 eval* ts03 n2. ts04 = ? ((de @ (l [f] (v f @ (de @ (l [f] (l [x] v x + n1)))))) @ (de @ (l [g] (v g @ n0)))). %query 1 2 eval* ts04 (l [x] v x + n1). ts05 = ? ((de @ (l [f] (v f @ (de @ (l [f] v f @ (l [x] v x + n1)))))) @ (de @ (l [g] (v g @ n0)))). %query 1 2 eval* ts05 n1. % patent changing of the answer-type... % Therefore, it does not type-check %% tc01 = ? (n1 + (de @ (l [f] (l [x] (v f @ v x))))). %% %query 1 2 eval* tc01 R. % R = l U1 ([x:exp q0] l U2 ([x1:exp q0] ? (n1 + x1)) @ x). ts8 = ? (n1 + ((l [f] (v f @ n0)) @ (de @ (l [k] (v k @ (l [x] v x + n1)) + n1)))). % %define ti = R %solve _ : (eval t8 R). % %define ti = R %solve _ : (eval ti R). %query 1 2 eval* ts8 (n 1 1 1 0). ts10 = ? (n1 + ((l [f] (v f @ n0)) @ (de @ (l [k] n1 + (v k @ (de @ (l [_: arg (arr (arr int int int) int int) 0] n0))))))). %query 1 2 eval* ts10 n0. % In CBN: (n 1 0). % shift across stages % The following requires the change in the answer-type % It won't type-check %% tss1 = ? ^ (dec ~(de @ (l [f] v f))). %% tss2 = tss1 @ ^ n2. %% %query 1 2 eval* tss1 R. %% R = l U1 ([x:exp q0] ? ^ (~ ^ dec (~ x))). %% %query 1 2 eval* tss2 (^ dec n2). tss21 = ? ^ (dec ~(de @ (l [f] v f @ ^ n2))). % tss21 : {T1:tp} {T2:tp} exp (& int T1) (at0 T2) %query 1 3 eval* tss21 (^ dec n2). tss3 = ^ (l2 [x] dec ~(de @ (l [f] ^((~ (v f @ ^ v2 x)) + (~ (v f @ ^ v2 x)))))). %% tss3 : {T1:tp} {T2:tp} {T3:tp} exp (& (arr int int T1) T2) (at0 T3) %query 1 2 eval* tss3 R. % R = ^ l2 ([x:arg int (1 0)] dec (v2 x) + dec (v2 x)). % Delimited control and more than two stages % sst1 : exp (& (& int T1) T2) (at0 T3) % = ? (^ ^ (n1 + ~ ~ (de @ l [sk] (v sk) @ ^ ^ n2))). %query 1 2 eval* sst1 (^ ^ (n 1 0 + ~ ^ n 1 1 0)). % The type is pure with no outer reset... % sst2 : exp (& (& (arr T1 int T2) T3) T4) A1 % = (^ ^ (l3 [x] ~ ~ (de @ l [sk] (v sk) @ ^ ^ n2))). %query 1 2 eval* sst2 (^ ^ l3 ([x:arg T1 (1 1 0)] ~ ^ n 1 1 0)). % Making the (pure) function polymorphic in the answer-type of % its body, by doing eta-expansion and introducing reset. % Note the type of f below and the resulting type % of the expression. The result is fully answer-type % polymorphic! % We could use the abbreviation below: % %abbrev % eta-poly1 : {f:exp (arr T1 T2 T2) (at0 T2)} exp (arr T1 T2 T3) (at0 T4) % = [f] l [y] ? f @ v y. % However, the following definition as an (object level) constant % improves the performance, since abbreviations are expanded but % definitions are not. Therefore, definitions are shared. % That means a lot in Twelf repeatedly rebuilding of terms. eta-poly1 = l [f] l [y] ? v f @ v y. % The same for the function of two arguments % %abbrev % eta-poly2 : {f:exp (arr T1 (arr T2 T3 T3) (arr T2 T3 T3)) (at0 arr T2 T3 T3)} % exp (arr T1 (arr T2 T3 T4) T5) (at0 T6) % = [f] l [x] l [y] ? (? f @ v x) @ v y. eta-poly2 = l [f] l [x] l [y] ? (? v f @ v x) @ v y. % realistic example seemingly requiring answer-type polymorphism tpoly = de @ (l [k] l [table] (? v k @ (eta-poly1 @ (? v table @ n1))) @ (eta-poly2 @ (v table))). % tpoly : % {T1:tp} {T2:tp} {T3:tp} {T4:tp} {T5:tp} % exp (arr T1 T2 T3) (at0 arr (arr int (arr T1 T2 T2) (arr T1 T2 T2)) T4 T5) % the result is the pure function, whose body is pure: arr T1 T2 T3. % The answer-type T3 can be instantiated to anything. % Therefore, tpoly1 and tpoly2 below type-check. tpoly1 = tpoly @ n2. % tpoly1 : % {T1:tp} {T2:tp} {T3:tp} % exp T1 (at0 arr (arr int (arr int T1 T1) (arr int T1 T1)) T2 T3) tpoly2 = (? ((l [x] l [table] v x) @ (tpoly1))) @ (l [u1] l [u2] v u1 + v u2). % tpoly2 : {T1:tp} exp int (at0 T1) %query 1 2 eval* tpoly2 n3. % A few examples demonstrating congruences, suggested by Ken tcong1 = fix @ ((l [f] v f) @ (l [self] l [_] n1)). %% %query 1 2 eval* tcong1 R. %query 1 2 eval* (tcong1 @ n7) n1. % The subtle example %query 1 2 eval* (? (fix @ (l [self] l [_] n1))) R. tcong2 = ? fix @ (de @ (l [k] v k @ (l [self] l [x] v x + n1))). % %define tn = R %solve _ : vclassify tcong2 (a-non-value R). % %define ti = R %solve _ : (eval tcong2 tn R). % %define tn = R %solve _ : vclassify ti (a-non-value R). % %define ti = R %solve _ : (eval ti tn R). %query 1 2 eval* (tcong2 @ n7) n8. % pairs tpair1 = ? (fst @ (cons (de @ (l [k] v k @ n1)) (de @ (l [k] v k @ n2)))). %query 1 2 eval* tpair1 n1. tpair2 = ? (snd @ (cons (de @ (l [k] v k @ n1)) (de @ (l [k] v k @ n2)))). %query 1 2 eval* tpair2 n2. % Examples from the paper % Section on delimited continuations and staging %% We need an extra ? in (? v k @ v u) to ensure the answer-type %% `polymorphism' paper_ex1 = (? ((l [r] l [_] v r) @ ^ (~ (de @ (l [k] l [u] (? v k @ v u) @ v u)) + ~ (de @ (l [k] l [u] (? v k @ v u) @ v u))))) @ ^(n1 + n4). %% paper_ex1 : {T1:tp} {T2:tp} exp (& int T1) (at0 T2) %query 1 1 eval* paper_ex1 (^ (n1 + n4 + (n1 + n4))). paper_ex2 = (? ((l [r] l [_] v r) @ ^ (~ (de @ (l [k] l [u] ^((l2 [t] ~((? v k @ ^ v2 t) @ ^ v2 t)) @+ ~ v u))) + ~ (de @ (l [k] l [u] (? v k @ v u) @ v u))))) @ ^(n1 + n4). %% %query 1 2 teval* paper_ex2 (apure &int). %query 1 1 eval* paper_ex2 (^ (l2 ([x:arg int (1 0)] v2 x + v2 x) @+ (n1 + n4))). % paper_ex1 with a binding. The binding `cuts' the mutation and makes the % state inaccessible. The example becomes stuck and won't type either. %{ paper_ex3 = (? ((l [r] l [_] v r) @ ^ (l2 [x] %% the only change ~ (de @ (l [k] l [u] (? v k @ v u) @ v u)) + ~ (de @ (l [k] l [u] (? v k @ v u) @ v u))))) @ ^(n1 + n4). }% % Example from the paper `Closing the Stage' (see the beginning of this file) %query 1 1 eval* (powerc @ n3) (cons (^ l2 ([x:arg int (1 0)] l2 ([x1:arg int (1 0)] l2 ([x2:arg int (1 0)] l2 ([x3:arg int (1 0)] n0) @+ v2 x2 + v2 x2) @+ v2 x1 + v2 x1) @+ v2 x + v2 x)) n3). %query 1 1 eval* (powerd @ n3) R. %{ R = cons (^ l2 ([x:arg (& int T1) (1 0)] ^ (~ l2 ([x1:arg (& int T1) (1 0)] ^ (~ l2 ([x2:arg (& int T1) (1 0)] ^ (~ l2 ([x3:arg (& int T1) (1 0)] ^ n0) @+ v2 x2 + ~ v2 x2)) @+ v2 x1 + ~ v2 x1)) @+ v2 x + ~ v2 x))) (n 1 1 1 0). }%