forked from JasonGross/iris-coq
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathectxi_language.v
More file actions
152 lines (128 loc) · 6.24 KB
/
Copy pathectxi_language.v
File metadata and controls
152 lines (128 loc) · 6.24 KB
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
(** An axiomatization of languages based on evaluation context items, including
a proof that these are instances of general ectx-based languages. *)
From iris.algebra Require Export base.
From iris.program_logic Require Import language ectx_language.
Set Default Proof Using "Type".
(* 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 head_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 : Type}.
Context (of_val : val → expr).
Context (to_val : expr → option val).
Context (fill_item : ectx_item → expr → expr).
Context (head_step : expr → state → 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 : head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
mixin_fill_item_inj Ki : Inj (=) (=) (fill_item Ki);
mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
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;
mixin_head_ctx_step_val Ki e σ1 e2 σ2 efs :
head_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;
of_val : val → expr;
to_val : expr → option val;
fill_item : ectx_item → expr → expr;
head_step : expr → state → expr → state → list expr → Prop;
ectxi_language_mixin :
EctxiLanguageMixin of_val to_val fill_item head_step
}.
Arguments EctxiLanguage {_ _ _ _ _ _ _ _} _.
Arguments of_val {_} _%V.
Arguments to_val {_} _%E.
Arguments fill_item {_} _ _%E.
Arguments head_step {_} _%E _ _%E _ _.
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 head_ctx_step_val Ki e σ1 e2 σ2 efs :
head_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 head_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.
- by intros [] [].
- 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 head_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_head_stuck.
apply fill_not_val. revert Hstep. apply ectxi_language_mixin. }
simplify_eq. destruct (IH K') as [K'' ->]; auto.
exists K''. by rewrite assoc.
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.
Arguments fill {_} _ _%E.
Arguments ectxi_lang_ectx : clear implicits.
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 of_val to_val fill head mix := Λ in
@EctxLanguage E V (list C) St of_val to_val _ _ _ _
(@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St of_val to_val fill head mix)).