Skip to content

Commit

Permalink
yes_reify OK
Browse files Browse the repository at this point in the history
  • Loading branch information
Nicolas Nardino committed Jan 18, 2024
1 parent ef6848f commit 1b6ede9
Show file tree
Hide file tree
Showing 2 changed files with 89 additions and 37 deletions.
113 changes: 80 additions & 33 deletions theories/input_lang_delim/interp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -491,10 +491,24 @@ Section interp.
Program Definition interp_nat (n : nat) {A} : A -n> IT :=
λne env, Ret n.

(* Program Definition interp_cont {A} (K : A -n> (IT -n> IT)) : A -n> IT := *)
(* λne env, (Fun (Next (λne x, Tau (laterO_map (K env) (Next x))))). *)
(* Solve All Obligations with solve_proper_please. *)
Program Definition interp_cont {S} (e : @interp_scope F R _ (inc S) -n> IT) :
interp_scope S -n> IT :=
λne env, (Fun (Next (λne x, Tick $ e (@extend_scope F R _ _ env x)))).
Next Obligation.
solve_proper_prepare. repeat f_equiv.
intros [|a]; eauto.
Qed.
Next Obligation.
solve_proper_prepare.
repeat f_equiv.
intro. simpl. repeat f_equiv.
intros [|z]; eauto.
Qed.

(* (e : @interp_scope F R _ (inc S) -n> IT) : interp_scope S -n> IT := *)
(* λne env, SHIFT (λne (k : laterO IT -n> laterO IT), *)
(* (Next (e (@extend_scope F R _ _ env *)
(* (Fun (Next (λne x, Tau (k (Next x))))))))). *)



Expand Down Expand Up @@ -531,7 +545,7 @@ Section interp.
match v with
| LitV n => interp_nat n
| RecV e => interp_rec (interp_expr e)
(* | ContV K => interp_cont (interp_ectx K) *)
| ContV e => interp_cont (interp_expr e)
end
with
interp_expr {S} (e : expr S) : interp_scope S -n> IT :=
Expand Down Expand Up @@ -606,18 +620,37 @@ Section interp.


Fixpoint interp_ectx' {S} (K : ectx S) :
interp_scope S → IT → IT :=
interp_scope S -> IT -> IT :=
match K with
| [] => λ env, idfun
| C :: K => λ (env : interp_scope S) (t : IT),
| C :: K => λ (env : interp_scope S), λ (t : IT),
(interp_ectx' K env) (interp_ectx_el C (λne env, t) env)
end.
#[export] Instance interp_ectx_1_ne {S} (K : ectx S) (env : interp_scope S) :
NonExpansive (interp_ectx' K env : IT → IT).
Proof. induction K; solve_proper_please. Qed.

Definition interp_ectx {S} (K : ectx S) : interp_scope S → (IT -n> IT) :=
λ env, OfeMor (interp_ectx' K env).
Definition interp_ectx'' {S} (K : ectx S) (env : interp_scope S) : IT -n> IT :=
OfeMor (interp_ectx' K env).

Lemma interp_ectx''_cons {S} (env : interp_scope S)
(K : ectx S) (C : ectx_el S) (x : IT) (n : nat) :
interp_ectx'' (C :: K) env x ≡{n}≡ interp_ectx'' K env (interp_ectx_el C (λne _, x) env).
Proof. done. Qed.

#[export] Instance interp_ectx_2_ne {S} (K : ectx S) :
NonExpansive (interp_ectx'' K : interp_scope S → (IT -n> IT)).
Proof.
induction K; intros ????; try by intro.
intro.
rewrite !interp_ectx''_cons.
f_equiv.
- by apply IHK.
- by f_equiv.
Qed.

Definition interp_ectx {S} (K : ectx S) : interp_scope S -n> (IT -n> IT) :=
OfeMor (interp_ectx'' K).

Example test_ectx : ectx ∅ := [OutputK ; AppRK (RecV (Var VZ))].
(* Eval cbv[test_ectx interp_ectx interp_ectx' interp_ectx_el *)
Expand All @@ -641,6 +674,7 @@ Section interp.
destruct v; simpl.
- apply _.
- rewrite interp_rec_unfold. apply _.
- apply _.
Qed.

Global Instance ArrEquiv {A B : Set} : Equiv (A [→] B) :=
Expand Down Expand Up @@ -694,6 +728,10 @@ Section interp.
iIntros (y').
destruct y' as [| [| y]]; simpl; first done; last done.
by iRewrite - "IH".
+ repeat f_equiv.
intro. simpl.
rewrite interp_expr_ren. repeat f_equiv.
intros [|?]; eauto.
Qed.


Expand Down Expand Up @@ -780,6 +818,11 @@ Section interp.
iApply internal_eq_pointwise.
iIntros (z).
done.
+ repeat f_equiv. intro. simpl.
rewrite interp_expr_subst. repeat f_equiv.
intros [|?]; eauto. simpl.
rewrite interp_expr_ren. f_equiv.
by intro.
Qed.


Expand Down Expand Up @@ -948,6 +991,13 @@ Section interp.
rewrite interp_val_ren.
f_equiv.
intros ?; simpl; reflexivity.
- (* continuations *)
subst.
erewrite APP_APP'_ITV; last apply _.
rewrite APP_Fun. simpl. rewrite -Tick_eq. do 2 f_equiv.
rewrite interp_expr_subst.
f_equiv.
intros [|?]; eauto.
- (* the natop stuff *)
simplify_eq.
destruct v1,v2; try naive_solver. simpl in *.
Expand Down Expand Up @@ -975,6 +1025,8 @@ Section interp.
by rewrite H.
- rewrite <-hom_tick_n; last eauto. apply (interp_expr_head_step env) in H.
by rewrite H.
- rewrite <-hom_tick_n; last eauto. apply (interp_expr_head_step env) in H.
by rewrite H.
Qed.

Opaque INPUT OUTPUT_ SHIFT RESET.
Expand Down Expand Up @@ -1083,33 +1135,27 @@ Section interp.
}
clear f.
f_equiv.
trans ((Fun $ Next $ ir_unf (interp_expr e0) env)
⊙ (Fun $ Next $ ir_unf (interp_expr (shift (shift K) ⟪ Var VZ ⟫)%syn) env)
); last first.
{ repeat f_equiv; by rewrite interp_rec_unfold. }
rewrite APP'_Fun_r APP_Fun -!Tick_eq. simpl.
rewrite APP'_Fun_r.
match goal with
| |- context G [(ofe_mor_car _ _ (ofe_mor_car _ _ APP _) ?f)] =>
trans (APP (Fun $ Next $ ir_unf (interp_expr e0) env) f); last first
end.
{ repeat f_equiv; try by rewrite interp_rec_unfold. }
rewrite APP_Fun -!Tick_eq. simpl.
repeat f_equiv.
intro. simpl.
rewrite interp_comp.
(* rewrite laterO_map_Next. *)
(* Transparent extend_scope. *)
(* intros [| x]; term_simpl; last reflexivity. *)
(* rewrite interp_rec_unfold. *)
(* do 2 f_equiv. intro. *)
(* Opaque extend_scope. *)
(* rewrite laterO_map_Next -Tick_eq. *)
(* rewrite interp_comp. *)
symmetry. etrans; first by apply interp_ectx_ren.
rewrite interp_comp laterO_map_Next -Tick_eq. f_equiv.
symmetry.
Transparent extend_scope.
fold (@interp_ectx S K env).
Opaque interp_ectx.
simpl.
etrans; first by apply interp_ectx_ren.
(* rewrite -hom_tick. *)
match goal with
| |- context G [(interp_ectx K ?e)] => set (env' := e)
end.
rewrite laterO_map_Next -Tick_eq.
trans (interp_ectx K env' (Tick x)).
+ f_equiv. Transparent extend_scope.
simpl. admit.
+ simpl. admit.
repeat f_equiv.
unfold ren_scope. simpl.
apply ofe_mor_ext. done.
Transparent interp_ectx.
Opaque extend_scope.
- Transparent RESET. unfold RESET.
trans (reify (gReifiers_sReifier rs)
(RESET_ (laterO_map (λne y, interp_ectx' K' env y) ◎
Expand Down Expand Up @@ -1137,7 +1183,8 @@ Section interp.
f_equiv.
rewrite laterO_map_Next -Tick_eq. f_equiv.
rewrite interp_comp. f_equiv.
simpl. by rewrite get_val_ITV.
+ done.
+ simpl. by rewrite get_val_ITV.
Qed.

Lemma soundness {S} (e1 e2 : expr S) σ1 σ2 (σr : gState_rest sR_idx rs ♯ IT) n m (env : interp_scope S) :
Expand Down
13 changes: 9 additions & 4 deletions theories/input_lang_delim/lang.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,8 @@ Inductive expr {X : Set} :=
| Reset (e : expr) : expr
with val {X : Set} :=
| LitV (n : nat) : val
| RecV (e : @expr (inc (inc X))) : val.
| RecV (e : @expr (inc (inc X))) : val
| ContV (e : @expr (inc X)) : val.



Expand Down Expand Up @@ -71,7 +72,7 @@ vmap {A B : Set} (f : A [→] B) (v : val A) : val B :=
match v with
| LitV n => LitV n
| RecV e => RecV (emap ((f ↑) ↑) e)
(* | ContV K => ContV (kmap f K) *)
| ContV e => ContV (emap (f ↑) e)
end.

#[export] Instance FMap_expr : FunctorCore expr := @emap.
Expand Down Expand Up @@ -109,7 +110,7 @@ vbind {A B : Set} (f : A [⇒] B) (v : val A) : val B :=
match v with
| LitV n => LitV n
| RecV e => RecV (ebind ((f ↑) ↑) e)
(* | ContV K => ContV (kbind f K) *)
| ContV e => ContV (ebind (f ↑) e)
end.

#[export] Instance BindCore_expr : BindCore expr := @ebind.
Expand Down Expand Up @@ -414,7 +415,7 @@ Qed.

(* Only if no reset in K *)
Definition cont_to_rec {X : Set} (K : ectx X) : (val X) :=
RecV (fill (shift (shift K)) (Var VZ)).
ContV (fill (shift K) (Var VZ)).

Example test1 : val (inc ∅) := (cont_to_rec [OutputK; AppRK (Var VZ)]).

Expand Down Expand Up @@ -456,6 +457,10 @@ Variant head_step {S} : expr S → state -> ectx S →
(subst (Inc := inc) ((subst (F := expr) (Inc := inc) e1)
(Val (shift (Inc := inc) v2)))
(Val (RecV e1))) σ K (1,0)
| BetaContS e1 v2 σ K :
head_step (App (Val $ ContV e1) (Val v2)) σ K
(subst (Inc := inc) e1 (Val v2))
σ K (2,0)
| InputS σ n σ' K :
update_input σ = (n, σ') →
head_step Input σ K (Val (LitV n)) σ' K (1, 1)
Expand Down

0 comments on commit 1b6ede9

Please sign in to comment.