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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
(** An axiomatization of languages based on evaluation context items, including
a proof that these are instances of general ectx-based languages. *)
From iris.prelude Require Export prelude.
From iris.program_logic Require Import language ectx_language.
From iris.prelude Require Import options.
(** TAKE CARE: When you define an [ectxiLanguage] canonical structure for your
language, you need to also define a corresponding [language] and [ectxLanguage]
canonical structure for canonical structure inference to work properly. You
should use the coercion [EctxLanguageOfEctxi] and [LanguageOfEctx] for that, and
not [ectxi_lang] and [ectxi_lang_ectx], otherwise the canonical projections will
not point to the right terms.
A full concrete example of setting up your language can be found in [heap_lang].
Below you can find the relevant parts:
Module heap_lang.
(* Your language definition *)
Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item base_step.
Proof. (* ... *) Qed.
End heap_lang.
Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
*)
Section ectxi_language_mixin.
Context {expr val ectx_item state observation : Type}.
Context (of_val : val → expr).
Context (to_val : expr → option val).
Context (fill_item : ectx_item → expr → expr).
Context (base_step : expr → state → list observation → expr → state → list expr → Prop).
Record EctxiLanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
mixin_of_to_val e v : to_val e = Some v → of_val v = e;
mixin_val_stuck e1 σ1 κ e2 σ2 efs : base_step e1 σ1 κ e2 σ2 efs → to_val e1 = None;
mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
(** [fill_item] is always injective on the expression for a fixed
context. *)
mixin_fill_item_inj Ki : Inj (=) (=) (fill_item Ki);
(** [fill_item] with (potentially different) non-value expressions is
injective on the context. *)
mixin_fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None → to_val e2 = None →
fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2;
(** If [fill_item Ki e] takes a base step, then [e] is a value (unlike for
[ectx_language], an empty context is impossible here). In other words,
if [e] is not a value then wrapping it in a context does not add new
base redex positions. *)
mixin_base_ctx_step_val Ki e σ1 κ e2 σ2 efs :
base_step (fill_item Ki e) σ1 κ e2 σ2 efs → is_Some (to_val e);
}.
End ectxi_language_mixin.
Structure ectxiLanguage := EctxiLanguage {
expr : Type;
val : Type;
ectx_item : Type;
state : Type;
observation : Type;
of_val : val → expr;
to_val : expr → option val;
fill_item : ectx_item → expr → expr;
base_step : expr → state → list observation → expr → state → list expr → Prop;
ectxi_language_mixin :
EctxiLanguageMixin of_val to_val fill_item base_step
}.
Bind Scope expr_scope with expr.
Bind Scope val_scope with val.
Global Arguments EctxiLanguage {_ _ _ _ _ _ _ _ _} _.
Global Arguments of_val {_} _.
Global Arguments to_val {_} _.
Global Arguments fill_item {_} _ _.
Global Arguments base_step {_} _ _ _ _ _ _.
Section ectxi_language.
Context {Λ : ectxiLanguage}.
Implicit Types (e : expr Λ) (Ki : ectx_item Λ).
Notation ectx := (list (ectx_item Λ)).
(* Only project stuff out of the mixin that is not also in ectxLanguage *)
Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. apply ectxi_language_mixin. Qed.
Lemma fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
Proof. apply ectxi_language_mixin. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None → to_val e2 = None →
fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
Proof. apply ectxi_language_mixin. Qed.
Lemma base_ctx_step_val Ki e σ1 κ e2 σ2 efs :
base_step (fill_item Ki e) σ1 κ e2 σ2 efs → is_Some (to_val e).
Proof. apply ectxi_language_mixin. Qed.
Definition fill (K : ectx) (e : expr Λ) : expr Λ := foldl (flip fill_item) e K.
Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K2 (fill K1 e).
Proof. apply foldl_app. Qed.
Definition ectxi_lang_ectx_mixin :
EctxLanguageMixin of_val to_val [] (flip (++)) fill base_step.
Proof.
assert (fill_val : ∀ K e, is_Some (to_val (fill K e)) → is_Some (to_val e)).
{ intros K. induction K as [|Ki K IH]=> e //=. by intros ?%IH%fill_item_val. }
assert (fill_not_val : ∀ K e, to_val e = None → to_val (fill K e) = None).
{ intros K e. rewrite !eq_None_not_Some. eauto. }
split.
- apply ectxi_language_mixin.
- apply ectxi_language_mixin.
- apply ectxi_language_mixin.
- done.
- intros K1 K2 e. by rewrite /fill /= foldl_app.
- intros K; induction K as [|Ki K IH]; rewrite /Inj; naive_solver.
- done.
- intros K K' e1 κ e1' σ1 e2 σ2 efs Hfill Hred Hstep; revert K' Hfill.
induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
{ rewrite fill_app in Hstep. apply base_ctx_step_val in Hstep.
apply fill_val in Hstep. by apply not_eq_None_Some in Hstep. }
rewrite !fill_app /= in Hfill.
assert (Ki = Ki') as ->.
{ eapply fill_item_no_val_inj, Hfill; eauto using val_base_stuck.
apply fill_not_val. revert Hstep. apply ectxi_language_mixin. }
simplify_eq. destruct (IH K') as [K'' ->]; auto.
exists K''. by rewrite assoc.
- intros K e1 σ1 κ e2 σ2 efs.
destruct K as [|Ki K _] using rev_ind; simpl; first by auto.
rewrite fill_app /=.
intros ?%base_ctx_step_val; eauto using fill_val.
Qed.
Canonical Structure ectxi_lang_ectx := EctxLanguage ectxi_lang_ectx_mixin.
Canonical Structure ectxi_lang := LanguageOfEctx ectxi_lang_ectx.
Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
Lemma ectxi_language_sub_redexes_are_values e :
(∀ Ki e', e = fill_item Ki e' → is_Some (to_val e')) →
sub_redexes_are_values e.
Proof.
intros Hsub K e' ->. destruct K as [|Ki K _] using @rev_ind=> //=.
intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
Qed.
Global Instance ectxi_lang_ctx_item Ki : LanguageCtx (fill_item Ki).
Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
End ectxi_language.
Global Arguments ectxi_lang_ectx : clear implicits.
Global Arguments ectxi_lang : clear implicits.
Coercion ectxi_lang_ectx : ectxiLanguage >-> ectxLanguage.
Coercion ectxi_lang : ectxiLanguage >-> language.
Definition EctxLanguageOfEctxi (Λ : ectxiLanguage) : ectxLanguage :=
let '@EctxiLanguage E V C St K of_val to_val fill base mix := Λ in
@EctxLanguage E V (list C) St K of_val to_val _ _ _ _
(@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St K of_val to_val fill base mix)).
Global Arguments EctxLanguageOfEctxi : simpl never.
|
