abstract machines:
C ~ compile
rule name | ||
C (ef ea) | C ea; push; C ef; apply | ct_apply |
C (λ e) | closure (C e; return) | c_abs |
C v | var_c v | c_var |
C (cons t e0 e1) | C e1; push; C e0; push; cons_result t | ct_cons |
C (match ec e0 e1) | C ec; match_call (C e0; pop_env_match) (C e1; pop_env_match) | c_match |
C (ef va) | C ef; apply_var va | cv_apply |
C (eager_let e0 e1) | C e0; eager_let_c; C e1; pop_env_let | cv_let |
C (cons t v0 v1) | cons_result_var t v0 v1 | cv_cons |
Krivine with eager evaluation | ||
C (ef va) | push_var va; C ef | |
C (λ e) | pop; C e | |
C v | enter v | |
C (eager_let e0 e1) | delay (eager_let_c; C e1); C e0 | s_eager_let |
C (cons t) | cons_return t | |
C (match ec e0 e1) | delay (match (C e0) (C e1)); C ec | |
C (lazy_let e0 e1) | lazy_let_c (C e0); C e1 |
Krivine: “Krivine with eager evaluation” without s_eager_let
categorical, terms in argument:
categorical:
categorical without closures: categorical
re e v = an element of the environment e at the index v
$t = substitute the value of t into the name
old state | new state |
condition | rule name | ||||||
code | environment | stack | result | code | environment | stack | result | ||
push; c | e | s | Some x | c | e | V x :: s | None | ||
apply; c | e | V a :: s | Some (Cl c' e') | c' | a :: e' | R c e :: s | None | ||
closure c'; c | e | s | None | c | e | s | Some (Cl c' e) | e_closure | |
return | _ | R c e :: s | Some x | c | e | s | Some x | ||
var_c v; c | e | s | None | c | e | s | Some (re e v) | ||
cons_result t; c | e | V a0 :: V a1 :: s | None | c | e | s | Some (Cons t a0 a1) | ||
cons_result_var t v0 v1; c | e | s | None | c | e | s | Some (Cons t (re e v0) (re e v1)) |
||
match_call c0 c1; c | e | s | Some (Cons t a0 a1) | c$t; c | a0 :: a1 :: e | s | None | ||
pop_env_match; c | _ :: _ :: e | s | Some x | c | e | s | Some x | ||
pop_env_let; c | _ :: e | s | Some x | c | e | s | Some x | ||
apply_var v; c | e | s | Some (Cl c' e') | c' | re e v :: e' | R c e :: s | None | e_apply_var | |
eager_let_c; c | e | s | Some x | c | x :: e | s | None | ||
closure c'; c | e | s | None | c | e | s | Some (Cl c') | a_closure | |
apply_var v; c | e | s | Some (Cl c') | c' | re e v :: nil | R c e :: s | None | a_apply_var | |
Krivine with eager evaluation | |||||||||
push_var v; c | e | s | None | c | e | V (re e v) :: s | None | ||
pop; c | e | V a :: s | None | c | a :: e | s | None | pop_value | |
c | e | R c' e' :: s | None | c' | e' | s | Some (Cl c e) | c=(pop; _) | pop_return |
enter v | e | s | None | c' | e' | s | None | re e v = Cl c' e' | enter_closure |
enter v | e | R c' e' :: s | None | c' | e' | s | Some x | re e v = x ∧ x = Cons t _ _ |
enter_cons |
delay c'; c | e | s | None | c | e | R c' e :: s | None | ||
cons_return t | _ | V a0 :: V a1 :: R c' e' :: s |
None | c' | e' | s | Some (Cons t a0 a1) | ||
match c0 c1 | e | s | Some (Cons t a0 a1) | c$t | a0 :: a1 :: e | s | None | ||
lazy_let_c c'; c | e | s | None | c | Cl c' e :: e | s | None |
categorical, terms in argument:
categorical:
categorical without closures:
Krivine with eager evaluation:
Krivine: (never has Cons in its environment or stack)