blob: aa0b7f3f5ed727512117e8238c56c54290e49de7 (
about) (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
From mininix Require Export lambda.interp_proofs dynlang.interp_proofs.
From stdpp Require Import options.
Class Lift A B := lift : A → B.
Global Hint Mode Lift ! - : typeclass_instances.
Arguments lift {_ _ _} !_ /.
Notation "⌜ x ⌝" := (lift x) (at level 0).
Notation "⌜* x ⌝" := (fmap lift x) (at level 0).
Module lambda.
Global Instance lambda_expr_lift : Lift lambda.expr dynlang.expr :=
fix go e := let _ : Lift _ _ := go in
match e with
| lambda.EString s => dynlang.EString s
| lambda.EId x => dynlang.EId ∅ (dynlang.EString x)
| lambda.EAbs x e => dynlang.EAbs (dynlang.EString x) ⌜e⌝
| lambda.EApp e1 e2 => dynlang.EApp ⌜e1⌝ ⌜e2⌝
end.
Global Instance lambda_thunk_lift : Lift lambda.thunk dynlang.thunk :=
fix go t := let _ : Lift _ _ := go in
dynlang.Thunk ⌜*lambda.thunk_env t⌝ ⌜lambda.thunk_expr t⌝.
Global Instance lambda_val_lift : Lift lambda.val dynlang.val := λ v,
match v with
| lambda.VString s => dynlang.VString s
| lambda.VClo x E e => dynlang.VClo x ⌜*E⌝ ⌜e⌝
end.
End lambda.
Lemma interp_open_lambda_dynlang E e mv n :
lambda.closed_env E → lambda.closed (dom E) e →
lambda.interp n E e = Res mv →
∃ m, dynlang.interp m ⌜*E⌝ ⌜e⌝ = Res ⌜*mv⌝.
Proof.
revert E e mv. induction n as [|n IH]; [done|]; intros E e mv HE He Hinterp.
rewrite lambda.interp_S in Hinterp. destruct e as [s|z|ex e|e1 e2]; simplify_res.
- (* EString *) by exists 1.
- (* EId *)
apply elem_of_dom in He as [[Et et] Hz]. rewrite Hz /= in Hinterp.
apply lambda.closed_env_lookup in Hz as He; last done.
rewrite lambda.closed_thunk_eq/= in He. destruct He as [HEtclosed Hetclosed].
apply IH in Hinterp as [m Hinterp]; [|done..].
exists (S (S m)). rewrite !dynlang.interp_S /= -dynlang.interp_S.
rewrite lookup_empty /= right_id_L lookup_fmap Hz /=.
eauto using dynlang.interp_le with lia.
- (* EAbs *) by exists 2.
- (* EApp *)
destruct He as [He1 He2].
destruct (lambda.interp _ _ e1) as [mw|] eqn:Hinterp1; simplify_res.
pose proof Hinterp1 as Hinterp1'.
apply lambda.interp_closed in Hinterp1' as Hmw; [|done..].
eapply IH in Hinterp1 as [m1 Hinterp1]; [|done..].
destruct mw as [w|]; simplify_res; last first.
{ exists (S m1). by rewrite dynlang.interp_S /= Hinterp1. }
destruct (maybe3 lambda.VClo w) eqn:?; simplify_res; last first.
{ exists (S m1). rewrite dynlang.interp_S /= Hinterp1 /=. by destruct w. }
destruct w; simplify_res.
apply IH in Hinterp as [m2 Hinterp2].
+ exists (S (m1 + m2)). rewrite dynlang.interp_S /=.
rewrite (dynlang.interp_le Hinterp1) /=; last lia.
rewrite fmap_insert /= in Hinterp2.
rewrite (dynlang.interp_le Hinterp2) /=; last lia. done.
+ apply lambda.closed_env_insert; [by split|naive_solver].
+ rewrite dom_insert_L. set_solver.
Qed.
Lemma interp_lambda_dynlang e mv n :
lambda.closed ∅ e →
lambda.interp n ∅ e = Res mv →
∃ m, dynlang.interp m ∅ ⌜e⌝ = Res ⌜*mv⌝.
Proof. intro. by apply interp_open_lambda_dynlang. Qed.
Lemma interp_open_dynlang_lambda E e mv n :
lambda.closed_env E → lambda.closed (dom E) e →
dynlang.interp n ⌜*E⌝ ⌜e⌝ = Res mv →
∃ mw, lambda.interp n E e = Res mw ∧ mv = ⌜*mw⌝.
Proof.
revert E e mv. induction n as [|n IH]; [done|]; intros E e mv HE He Hinterp.
rewrite dynlang.interp_S in Hinterp. destruct e as [s|z|ex e|e1 e2]; simplify_res.
- (* EString *) rewrite lambda.interp_S /=. by eexists.
- (* EId *)
destruct n as [|n]; [done|].
rewrite dynlang.interp_S /= -dynlang.interp_S in Hinterp.
apply elem_of_dom in He as [[Et et] Hz].
pose proof (f_equal (fmap lift) Hz) as Hz'.
rewrite -lookup_fmap /= in Hz'. rewrite Hz' lookup_empty /= {Hz'} in Hinterp.
pose proof Hz as Hz'.
apply lambda.closed_env_lookup in Hz' as [HEt Het]; simpl in *; last done.
apply IH in Hinterp as (mw & Hinterp & ->); [|done..].
exists mw. rewrite lambda.interp_S /= Hz /=. done.
- (* EAbs *)
destruct n as [|n]; [done|].
rewrite dynlang.interp_S /= in Hinterp; simplify_res.
rewrite lambda.interp_S /=. by eexists.
- (* EApp *)
destruct He as [He1 He2].
destruct (dynlang.interp _ _ _) as [mw1|] eqn:Hinterp1; simplify_res.
eapply IH in Hinterp1 as (mv1 & Hinterp1 & ->); [|done..].
destruct mv1 as [v1|]; simplify_res; last first.
{ exists None. by rewrite lambda.interp_S /= Hinterp1. }
destruct (maybe3 dynlang.VClo _) eqn:?; simplify_res; last first.
{ exists None. rewrite lambda.interp_S /= Hinterp1 /=. by destruct v1. }
destruct v1; simplify_res.
change (dynlang.Thunk ⌜*E⌝ ⌜e2⌝) with ⌜lambda.Thunk E e2⌝ in Hinterp.
rewrite -fmap_insert in Hinterp.
apply lambda.interp_closed in Hinterp1 as Hmw; [|done..].
apply IH in Hinterp as (mv2 & Hinterp2 & ->).
+ exists mv2. rewrite lambda.interp_S /= Hinterp1 /=. done.
+ apply lambda.closed_env_insert; [by split|]. naive_solver.
+ rewrite dom_insert_L. set_solver.
Qed.
Lemma interp_dynlang_lambda e mv n :
lambda.closed ∅ e →
dynlang.interp n ∅ ⌜e⌝ = Res mv →
∃ mw, lambda.interp n ∅ e = Res mw ∧ mv = ⌜*mw⌝.
Proof. intros. by apply interp_open_dynlang_lambda. Qed.
(* The following equivalences about the semantics trivially follow: *)
Theorem interp_equiv_ret_string e s :
lambda.closed ∅ e →
rtc lambda.step e (lambda.EString s)
↔ rtc dynlang.step ⌜e⌝ (dynlang.EString s).
Proof.
intros. rewrite -lambda.interp_sound_complete_ret_string //.
rewrite -dynlang.interp_sound_complete_ret_string. split; intros [n Hinterp].
+ by apply interp_lambda_dynlang in Hinterp.
+ apply interp_dynlang_lambda in Hinterp as ([[]|] & ?); naive_solver.
Qed.
Theorem interp_equiv_fail e :
lambda.closed ∅ e →
(∃ e', rtc lambda.step e e' ∧ lambda.stuck e')
↔ (∃ e', rtc dynlang.step ⌜e⌝ e' ∧ dynlang.stuck e').
Proof.
intros. rewrite -lambda.interp_sound_complete_fail //.
rewrite -dynlang.interp_sound_complete_fail. split; intros [n Hinterp].
+ by apply interp_lambda_dynlang in Hinterp.
+ apply interp_dynlang_lambda in Hinterp as ([] & ?); naive_solver.
Qed.
Theorem interp_equiv_no_fuel e :
lambda.closed ∅ e →
all_loop lambda.step e ↔ all_loop dynlang.step ⌜e⌝.
Proof.
intros He. rewrite -lambda.interp_sound_complete_no_fuel; last done.
rewrite -dynlang.interp_sound_complete_no_fuel. split; intros Hnofuel n.
- destruct (dynlang.interp n ∅ _) as [mv|] eqn:Hinterp; [|done].
apply interp_dynlang_lambda in Hinterp as (? & Hinterp & _); [|done].
by rewrite Hnofuel in Hinterp.
- destruct (lambda.interp n ∅ _) as [mv|] eqn:Hinterp; [|done].
apply interp_lambda_dynlang in Hinterp as [m Hinterp]; [|done..].
by rewrite Hnofuel in Hinterp.
Qed.
|
