Module Compiler

Compilation to the Modern SECD abstract machine and its proof of correctness.

Require Omega.
Require Import List.
Require Import Sequences.

Source language


Syntax with de Bruijn indices.

Definition const: Type := nat.

Inductive term: Type :=
  | Var: nat -> term (* de Bruijn index *)
  | Const: const -> term
  | Fun: term -> term
  | Let: term -> term -> term
  | App: term -> term -> term.

Big-step semantics with environments and closures.


A value is either an integer or a closure of a term by an environment.

Inductive value: Type :=
  | Int: const -> value
  | Clos: term -> list value -> value.

An environment is a list of values. Element number N of the list is the value of variable having de Bruijn index N.

Definition env := list value.

Looking up the N-th element of an environment.

Fixpoint lookup {A: Type} (n: nat) (l: list A) {struct l}: option A :=
  match l, n with
  | nil, _ => None
  | x :: l', O => Some x
  | x :: l', S n' => lookup n' l'
  end.

eval e a v means "in environment e, term a evaluates to value v".

Inductive eval: env -> term -> value -> Prop :=
  | eval_Var: forall e n v,
      lookup n e = Some v ->
      eval e (Var n) v
  | eval_Const: forall e i,
      eval e (Const i) (Int i)
  | eval_Fun: forall e a,
      eval e (Fun a) (Clos a e)
  | eval_Let: forall e a b va vb,
      eval e a va -> eval (va :: e) b vb ->
      eval e (Let a b) vb
  | eval_App: forall e a b ca ea vb v,
      eval e a (Clos ca ea) ->
      eval e b vb ->
      eval (vb :: ea) ca v ->
      eval e (App a b) v.

evalinf e a v means "in environment e, term a diverges".

CoInductive evalinf: env -> term -> Prop :=
  | evalinf_Let_l: forall e a b,
      evalinf e a ->
      evalinf e (Let a b)
  | evalinf_Let_r: forall e a b va,
      eval e a va -> evalinf (va :: e) b ->
      evalinf e (Let a b)
  | evalinf_App_l: forall e a b,
      evalinf e a ->
      evalinf e (App a b)
  | evalinf_App_r: forall e a b v,
      eval e a v ->
      evalinf e b ->
      evalinf e (App a b)
  | evalinf_App_f: forall e a b ca ea vb,
      eval e a (Clos ca ea) ->
      eval e b vb ->
      evalinf (vb :: ea) ca ->
      evalinf e (App a b).

Abstract machine: the Modern SECD


Instruction set.

Inductive instr: Type :=
  | IAccess: nat -> instr
  | IConst: const -> instr
  | IClosure: list instr -> instr
  | IApp: instr
  | ITailApp: instr
  | ILet: instr
  | IEndLet: instr
  | IReturn: instr.

Definition code := list instr.

Machine values and environments.

Inductive mvalue: Type :=
  | MInt: const -> mvalue
  | MClos: code -> list mvalue -> mvalue.

Definition menv := list mvalue.

Stacks.

Inductive slot: Type :=
  | Value: mvalue -> slot (* a value on the stack *)
  | Return: code -> menv -> slot. (* a return frame *)

Definition stack := list slot.

A state of the machine is a triple of a piece of code, a machine environment, and a stack.

Definition state : Type := (code * menv * stack)%type.

One transition of the machine.

Inductive transition: state -> state -> Prop :=
  | trans_IAccess: forall n k e s v,
      lookup n e = Some v ->
      transition (IAccess n :: k, e, s)
                 (k, e, Value v :: s)
  | trans_IConst: forall n k e s,
      transition (IConst n :: k, e, s)
                 (k, e, Value (MInt n) :: s)
  | trans_IClosure: forall c k e s,
      transition (IClosure c :: k, e, s)
                 (k, e, Value (MClos c e) :: s)
  | trans_IApp: forall k e v k' e' s,
      transition (IApp :: k, e, Value v :: Value (MClos k' e') :: s)
                 (k', v :: e', Return k e :: s)
  | trans_ITailApp: forall k e v k' e' s,
      transition (ITailApp :: k, e, Value v :: Value (MClos k' e') :: s)
                 (k', v :: e', s)
  | trans_ILet: forall k e v s,
      transition (ILet :: k, e, Value v :: s)
                 (k, v :: e, s)
  | trans_IEndLet: forall k e v s,
      transition (IEndLet :: k, v :: e, s)
                 (k, e, s)
  | trans_IReturn: forall k e v k' e' s,
      transition (IReturn :: k, e, Value v :: Return k' e' :: s)
                 (k', e', Value v :: s).

Executing code with the machine.

Definition mach_terminates (k: code) (v: mvalue) : Prop :=
  star transition (k, nil, nil) (nil, nil, Value v :: nil).

Definition mach_diverges (k: code) : Prop :=
  infseq transition (k, nil, nil).

Compilation and its correctness.


The compilation scheme. compile a k prepends the code for term a to the code k. The code for a evaluates a and deposits its value on top of the stack.

Fixpoint compile (a: term) (k: code) : code :=
  match a with
  | Var n => IAccess n :: k
  | Const i => IConst i :: k
  | Fun b => IClosure (compile b (IReturn :: nil)) :: k
  | Let b c => compile b (ILet :: compile c (IEndLet :: k))
  | App b c => compile b (compile c (IApp :: k))
  end.

Extension to values and environments

Fixpoint compile_value (v: value) : mvalue :=
  match v with
  | Int n => MInt n
  | Clos a e =>
      let fix compenv (e: env) : menv :=
        match e with
        | nil => nil
        | v :: e' => compile_value v :: compenv e'
        end in
      MClos (compile a (IReturn :: nil)) (compenv e)
  end.

Fixpoint compile_env (e: env) : menv :=
   match e with
   | nil => nil
   | v :: e' => compile_value v :: compile_env e'
   end.

Lemma lookup_compile:
  forall e n v,
  lookup n e = Some v ->
  lookup n (compile_env e) = Some (compile_value v).
Proof.
  induction e; destruct n; simpl; intros; auto; congruence.
Qed.

Compiler correctness for terminating programs.

Lemma compile_eval:
  forall e a v,
  eval e a v ->
  forall k s,
  plus transition (compile a k, compile_env e, s)
                  (k, compile_env e, Value (compile_value v) :: s).
Proof.
  induction 1; simpl; intros.
- (* Var *)
  apply plus_one. constructor. apply lookup_compile; auto.
- (* Const *)
  apply plus_one. constructor.
- (* Closure *)
  apply plus_one. constructor.
- (* Let *)
  eapply plus_trans; eauto.
  eapply plus_left. constructor.
  eapply star_trans. apply plus_star. eauto.
  apply star_one. constructor.
- (* App *)
  eapply plus_trans; eauto.
  eapply plus_trans; eauto.
  eapply plus_left.
    change (compile_value (Clos ca ea))
      with (MClos (compile ca (IReturn :: nil)) (compile_env ea)).
    constructor.
  eapply star_trans. apply plus_star. eauto.
  apply star_one. constructor.
Qed.

Theorem compile_terminates:
  forall a v,
  eval nil a v -> mach_terminates (compile a nil) (compile_value v).
Proof.
  intros. red. apply plus_star. apply compile_eval with (e := nil). auto.
Qed.

Compiler correctness for diverging programs.

Inductive diverging_state : state -> Prop :=
  | diverging_state_intro: forall e a k s,
      evalinf e a ->
      diverging_state (compile a k, compile_env e, s).

Lemma diverging_states_productive:
  forall S,
  diverging_state S ->
  exists S', plus transition S S' /\ diverging_state S'.
Proof.
  intros. inversion H; subst. clear H. revert a e k s H0.
  induction a; intros e k s EVALINF; inversion EVALINF; subst; simpl.
- (* divergence left of a Let *)
  apply IHa1. auto.
- (* divergence right of a Let *)
  econstructor; split.
  eapply plus_right. apply plus_star. apply compile_eval. eauto. constructor.
  apply diverging_state_intro with (e := va :: e). auto.
- (* divergence left of an App *)
  apply IHa1. auto.
- (* divergence right of an App *)
  econstructor; split.
  apply compile_eval. eauto.
  constructor. auto.
- (* divergence after beta reduction *)
  econstructor; split.
  eapply plus_trans. apply compile_eval. eauto.
  eapply plus_trans. apply compile_eval. eauto.
  apply plus_one.
  change (compile_value (Clos ca ea)) with (MClos (compile ca (IReturn :: nil)) (compile_env ea)).
  constructor.
  apply diverging_state_intro with (e := vb :: ea). auto.
Qed.

Theorem compile_diverges:
  forall a, evalinf nil a -> mach_diverges (compile a nil).
Proof.
  intros; red.
  apply infseq_coinduction_principle_2 with (X := diverging_state).
  exact diverging_states_productive.
  apply diverging_state_intro with (e := nil). auto.
Qed.

Adding tail call optimization


Module WithTailCalls.

The revised compilation scheme. Note mutual recursion: tailcompile uses compile for sub-terms that are not in tail position; compile uses tailcompile for the bodies of Fun abstractions.

Fixpoint compile (a: term) (k: code) : code :=
  match a with
  | Var n => IAccess n :: k
  | Const i => IConst i :: k
  | Fun b => IClosure (tailcompile b) :: k
  | Let b c => compile b (ILet :: compile c (IEndLet :: k))
  | App b c => compile b (compile c (IApp :: k))
  end

with tailcompile (a: term) : code :=
  match a with
  | Var n => IAccess n :: IReturn :: nil
  | Const i => IConst i :: IReturn :: nil
  | Fun b => IClosure (tailcompile b) :: IReturn :: nil
  | Let b c => compile b (ILet :: tailcompile c)
  | App b c => compile b (compile c (ITailApp :: nil))
  end.

Extension to values and environments.

Fixpoint compile_value (v: value) : mvalue :=
  match v with
  | Int n => MInt n
  | Clos a e =>
      let fix compenv (e: env) : menv :=
        match e with
        | nil => nil
        | v :: e' => compile_value v :: compenv e'
        end in
      MClos (tailcompile a) (compenv e)
  end.

Fixpoint compile_env (e: env) : menv :=
   match e with
   | nil => nil
   | v :: e' => compile_value v :: compile_env e'
   end.

Lemma lookup_compile:
  forall e n v,
  lookup n e = Some v ->
  lookup n (compile_env e) = Some (compile_value v).
Proof.
  induction e; destruct n; simpl; intros; auto; congruence.
Qed.

Compiler correctness for terminating programs.

Lemma compile_eval_gen:
  forall e a v,
  eval e a v ->
  (forall k s,
   plus transition (compile a k, compile_env e, s)
                   (k, compile_env e, Value (compile_value v) :: s))
  /\
  (forall s k e',
   plus transition (tailcompile a, compile_env e, Return k e' :: s)
                   (k, e', Value (compile_value v) :: s)).
Proof.
  induction 1; split; simpl; intros.
- (* Var, non-tail *)
  apply plus_one. constructor. apply lookup_compile; auto.
- (* Var, tail *)
  eapply plus_left. constructor. apply lookup_compile; eauto.
  apply star_one. constructor.
- (* Const, non-tail *)
  apply plus_one. constructor.
- (* Const, tail *)
  eapply plus_left. constructor.
  apply star_one. constructor.
- (* Closure, non-tail *)
  apply plus_one. constructor.
- (* Const, tail *)
  eapply plus_left. constructor.
  apply star_one. constructor.
- (* Let, non-tail *)
  eapply plus_trans. eapply IHeval1.
  eapply plus_left. constructor.
  eapply star_trans. apply plus_star. eapply IHeval2.
  apply star_one. constructor.
- (* Let, tail *)
  eapply plus_trans. eapply IHeval1.
  eapply plus_left. constructor.
  apply plus_star. eapply IHeval2.
- (* App, non-tail *)
  eapply plus_trans. eapply IHeval1.
  eapply plus_trans. eapply IHeval2.
  eapply plus_left.
  change (compile_value (Clos ca ea))
    with (MClos (tailcompile ca) (compile_env ea)).
  constructor.
  apply plus_star. apply IHeval3.
- (* App, tail *)
  eapply plus_trans. eapply IHeval1.
  eapply plus_trans. eapply IHeval2.
  eapply plus_left.
  change (compile_value (Clos ca ea))
    with (MClos (tailcompile ca) (compile_env ea)).
  constructor.
  apply plus_star. apply IHeval3.
Qed.

Lemma compile_eval:
  forall e a v k s,
  eval e a v ->
  plus transition (compile a k, compile_env e, s)
                  (k, compile_env e, Value (compile_value v) :: s).
Proof.
  intros. apply (proj1 (compile_eval_gen _ _ _ H)).
Qed.

Lemma tailcompile_eval:
  forall e a v s k e',
  eval e a v ->
  plus transition (tailcompile a, compile_env e, Return k e' :: s)
                  (k, e', Value (compile_value v) :: s).
Proof.
  intros. apply (proj2 (compile_eval_gen _ _ _ H)).
Qed.

Theorem compile_terminates:
  forall a v,
  eval nil a v -> mach_terminates (compile a nil) (compile_value v).
Proof.
  intros. red. apply plus_star. apply compile_eval with (e := nil). auto.
Qed.

Compiler correctness for diverging programs.

Inductive diverging_state : state -> Prop :=
  | diverging_state_nontail: forall e a k s,
      evalinf e a ->
      diverging_state (compile a k, compile_env e, s)
  | diverging_state_tail: forall e a s,
      evalinf e a ->
      diverging_state (tailcompile a, compile_env e, s).

Lemma diverging_states_productive:
  forall S,
  diverging_state S ->
  exists S', plus transition S S' /\ diverging_state S'.
Proof.
  assert (NONTAIL: forall a e s k,
    evalinf e a ->
      exists S', plus transition (compile a k, compile_env e, s) S' /\ diverging_state S').
  induction a; intros e s k EVALINF; inversion EVALINF; subst; simpl.
  apply IHa1. auto.
  econstructor; split.
  eapply plus_right. apply plus_star. apply compile_eval. eauto. constructor.
  apply diverging_state_nontail with (e := va :: e). auto.
  apply IHa1. auto.
  econstructor; split.
  apply compile_eval. eauto.
  constructor. auto.
  econstructor; split.
  eapply plus_trans. apply compile_eval. eauto.
  eapply plus_trans. apply compile_eval. eauto.
  apply plus_one.
  change (compile_value (Clos ca ea)) with (MClos (tailcompile ca) (compile_env ea)).
  constructor.
  apply diverging_state_tail with (e := vb :: ea). auto.

  assert (TAIL: forall a e s,
    evalinf e a ->
      exists S', plus transition (tailcompile a, compile_env e, s) S' /\ diverging_state S').
  intros. inversion H; subst; clear H; simpl.
  apply NONTAIL. auto.
  econstructor; split.
  eapply plus_right. apply plus_star. apply compile_eval. eauto. constructor.
  apply diverging_state_tail with (e := va :: e). auto.
  apply NONTAIL. auto.
  econstructor; split.
  apply compile_eval. eauto.
  constructor. auto.
  econstructor; split.
  eapply plus_trans. apply compile_eval. eauto.
  eapply plus_trans. apply compile_eval. eauto.
  apply plus_one.
  change (compile_value (Clos ca ea)) with (MClos (tailcompile ca) (compile_env ea)).
  constructor.
  apply diverging_state_tail with (e := vb :: ea). auto.

  intros. inversion H; subst; auto.
Qed.

Theorem compile_diverges:
  forall a, evalinf nil a -> mach_diverges (compile a nil).
Proof.
  intros; red.
  apply infseq_coinduction_principle_2 with (X := diverging_state).
  exact diverging_states_productive.
  apply diverging_state_nontail with (e := nil). auto.
Qed.

End WithTailCalls.