Skip to content

Commit

Permalink
comment explaining the problem related to CDefault
Browse files Browse the repository at this point in the history
  • Loading branch information
@adelaett
adelaett committed Jan 17, 2024
1 parent cc484b7 commit c49fd65
Showing 1 changed file with 106 additions and 49 deletions.
155 changes: 106 additions & 49 deletions theories/trans.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -237,7 +237,7 @@ Proof.
induction sigma; econstructor; eauto.
Qed.

Lemma correction_trans_value_op:
Lemma trans_value_op_correct:
forall v op v1 v2,
Some v = get_op op v1 v2 ->
Some (trans_value v) = get_op op (trans_value v1) (trans_value v2).
Expand All @@ -246,7 +246,6 @@ Proof.
Qed.



Theorem correction_small_steps:
forall s1 s2,
(exists GGamma Gamma T, jt_term GGamma Gamma s1 T) ->
Expand Down Expand Up @@ -294,7 +293,7 @@ Proof.
{ eexists; split; asimpl; eapply star_trans; eauto with sred; eapply star_refl. }
{ eexists; split; asimpl; eapply star_trans; eauto with sred; eapply star_refl. }
{ eexists; split; simpl trans; [|eapply star_refl; fail].
eapply star_step; [econstructor|]. { eapply correction_trans_value_op; eauto. }
eapply star_step; [econstructor|]. { eapply trans_value_op_correct; eauto. }
eapply star_refl.
}
{ eexists; split; asimpl; eapply star_trans; eauto with sred; eapply star_refl. }
Expand Down Expand Up @@ -359,6 +358,11 @@ Proof.
Qed.


(** Translation correctness using continuations. *)


(* To prove the translation correctness using continuations, we first need to extend the trans statement to states. This require to expand the definition to `cont`, `state`, `return` as welle as `environements`. *)

Require Import continuations.

Definition option_map {A B} (f: A -> B) (o: option A) :=
Expand All @@ -367,27 +371,105 @@ Definition option_map {A B} (f: A -> B) (o: option A) :=
| Some v => Some (f v)
end.

Fixpoint trans_conts (kappa: list cont) : list cont :=

(* Naively, we would think that translating cont would be simply. In ocaml, we would have a function
map_cont: (term -> term) -> (value -> value) -> cont -> cont
Then, [trans_cont] would be simply be [map_cont trans_term trans_value] and [trans_conts] would be simply [List.map trans_cont].
This is mostly the case, except for the default related continuations.
*)

Definition trans_cont (kappa: cont) : cont :=
match kappa with
| nil => nil
| CAppR t2 :: kappa => CAppR (trans t2) :: trans_conts kappa
| CBinopL op v1 :: kappa => CBinopL op (trans_value v1) :: trans_conts kappa
| CBinopR op t2 :: kappa => CBinopR op (trans t2) :: trans_conts kappa
| CClosure t_cl sigma_cl :: kappa => CClosure (trans t_cl) (List.map trans_value sigma_cl) :: trans_conts kappa
| CReturn sigma' :: kappa => CReturn (List.map trans_value sigma') :: trans_conts kappa
| CDefaultBase tc :: kappa => CIf (trans tc) ENone :: trans_conts kappa
| CMatch t1 t2 :: kappa => CMatch (trans t1) (trans t2) :: trans_conts kappa
| CSome :: kappa => CSome :: trans_conts kappa
| CIf t1 t2 :: kappa => CIf (trans t1) (trans t2) :: trans_conts kappa
| CErrorOnEmpty :: kappa => CMatch Conflict (Var 0) :: trans_conts kappa
| CDefaultPure :: kappa => CSome :: trans_conts kappa

| CDefault b None ts tj tc :: kappa =>
CMatch (monad_handle_zero (List.map trans ts) (trans tj) (trans tc)) (monad_handle_one (Var 0) (List.map trans ts)) :: trans_conts kappa
| CDefault b (Some v) ts tj tc :: kappa =>
CMatch (monad_handle_one' (Value (trans_value v)) (List.map trans ts)) (Conflict) :: trans_conts kappa
(* map_cont, inlined (lambda calculus cases) *)
| CAppR t2 => CAppR (trans t2)
| CBinopL op v1 => CBinopL op (trans_value v1)
| CBinopR op t2 => CBinopR op (trans t2)
| CClosure t_cl sigma_cl => CClosure (trans t_cl) (List.map trans_value sigma_cl)
| CReturn sigma' => CReturn (List.map trans_value sigma')
| CMatch t1 t2 => CMatch (trans t1) (trans t2)
| CSome => CSome
| CIf t1 t2 => CIf (trans t1) (trans t2)

(* Default handling stuff *)
| CDefaultBase tc => CIf (trans tc) ENone
| CErrorOnEmpty => CMatch Conflict (Var 0)
| CDefaultPure => CSome
| CDefault b None ts tj tc =>
CMatch (monad_handle_zero (List.map trans ts) (trans tj) (trans tc)) (monad_handle_one (Var 0) (List.map trans ts))

(* For the case where CDefault holds an value, we could naivly implement in this way : *)

| CDefault b (Some v) ts tj tc =>
CMatch (
monad_handle_one'
(Value (trans_value v))
(List.map trans ts)
) (Conflict)

(*
However, when trying to prove the simulation theorem, this leads to the following diagram:
exists target : state,
star cred
(mode_eval
(monad_handle_one (Var 0) (List.map trans ts))
(CReturn (List.map trans_value sigma) :: trans_conts kappa)
(trans_value v :: List.map trans_value sigma))
target /\
star cred
(mode_eval
(monad_handle_one' (Value (trans_value v)) (List.map trans ts))
(trans_conts kappa)
(List.map trans_value sigma))
target
To move on, we could do an induction over ts. If the initizalisation is straightforward, the induction step is more hairy:
exists target : state,
star cred
(mode_eval
(monad_handle_one (Var 0) (List.map trans ts))
(CReturn (List.map trans_value sigma) :: trans_conts kappa)
(trans_value v :: List.map trans_value sigma))
target /\
star cred
(mode_eval
(monad_handle_one' (Value (trans_value v)) (List.map trans ts))
(trans_conts kappa)
(List.map trans_value sigma))
target
--------------------------------------------------------------------
exists target : state,
star cred
(mode_eval
(lift 1 (trans a))
(CMatch (monad_handle_one (Var 0) (List.map trans ts)) Conflict
:: CReturn (List.map trans_value sigma)
:: trans_conts kappa)
(trans_value v :: List.map trans_value sigma))
target /\
star cred
(mode_eval
(trans a)
(CMatch (monad_handle_one' (Value (trans_value v)) (List.map trans ts)) Conflict
:: trans_conts kappa)
(List.map trans_value sigma))
target
While this is still true (assuming terminating execution), it requires multiple lemmas related to the behavior of lift on continuation semantics, and substitution within continuation (supposed to not have any free variables outside of the current sigma)
Hence, it is easier to modify the definition, so it modify the stack to have the same informations.
*)
end.

Definition trans_conts := List.map trans_cont.

Definition trans_return (r: result): result:=
match r with
| RValue v => RValue (trans_value v)
Expand All @@ -404,14 +486,6 @@ Definition trans_state (s: state) : state :=
end
.

Lemma trans_value_op op v v1 v2:
Some v = get_op op v1 v2 ->
Some (trans_value v) = get_op op (trans_value v1) (trans_value v2).
Proof.
intros.
induction op, v1, v2, v; simpl in *; tryfalse; eauto.
Qed.

Lemma step_left {A: Type} {R: A -> A -> Prop} {a1 a2 b}:
R a1 a2 ->
(exists target,
Expand Down Expand Up @@ -468,23 +542,6 @@ Qed.
Import List.ListNotations.


(* not true sadly *)
(* Goal forall s1,
trans (apply_state s1) = apply_state (trans_state s1).
Proof.
induction s1; induction kappa using List.rev_ind; simpl.
3: { induction result; simpl. } *)

Lemma lift_preserved:
forall t sigma a v,
(star cred (mode_eval t [] sigma) a) ->
(star cred (mode_eval (lift 1 t) [CReturn sigma] (v::sigma)) a).
Proof.
Admitted.

Lemma magic {A}: A.
Admitted.

Theorem correction_continuations:
forall s1 s2,
(exists GGamma Gamma T, jt_state GGamma Gamma s1 T) ->
Expand Down Expand Up @@ -539,13 +596,13 @@ Proof.
{ repeat step. unpack.
pose proof (IHts H2).
unpack.
eapply magic.
admit.
}
}
{ eexists; split; asimpl; [|eapply star_refl].
eapply star_step; [econstructor|]. { eapply trans_value_op; eauto. }
eapply star_step; [econstructor|]. { eapply trans_value_op_correct; eauto. }
eapply star_refl.
}
Fail next goal.
Qed.
Admitted.

0 comments on commit c49fd65

Please sign in to comment.