ectxi_language.v 6.99 KB
Newer Older
1
2
3
4
(** 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.
5
Set Default Proof Using "Type".
6

Ralf Jung's avatar
Ralf Jung committed
7
(** TAKE CARE: When you define an [ectxiLanguage] canonical structure for your
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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.
*)

29
Section ectxi_language_mixin.
30
  Context {expr val ectx_item state observation : Type}.
31
32
33
  Context (of_val : val  expr).
  Context (to_val : expr  option val).
  Context (fill_item : ectx_item  expr  expr).
34
  Context (head_step : expr  state  list observation  expr  state  list expr  Prop).
35
36
37
38

  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;
39
    mixin_val_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None;
40
41

    mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e))  is_Some (to_val e);
Ralf Jung's avatar
Ralf Jung committed
42
43
44
45
46
    (** [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. *)
47
48
49
50
    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;

Ralf Jung's avatar
Ralf Jung committed
51
52
53
54
    (** If [fill_item Ki e] takes a head 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
        head redex positions. *)
55
56
    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);
57
58
59
60
61
62
63
64
  }.
End ectxi_language_mixin.

Structure ectxiLanguage := EctxiLanguage {
  expr : Type;
  val : Type;
  ectx_item : Type;
  state : Type;
65
  observation : Type;
66

67
68
69
  of_val : val  expr;
  to_val : expr  option val;
  fill_item : ectx_item  expr  expr;
70
  head_step : expr  state  list observation  expr  state  list expr  Prop;
71

72
73
  ectxi_language_mixin :
    EctxiLanguageMixin of_val to_val fill_item head_step
74
75
}.

76
77
78
Bind Scope expr_scope with expr.
Bind Scope val_scope with val.

79
Arguments EctxiLanguage {_ _ _ _ _ _ _ _ _} _.
80
81
82
83
Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments fill_item {_} _ _.
Arguments head_step {_} _ _ _ _ _ _.
84
85

Section ectxi_language.
86
87
88
89
90
91
92
93
94
95
96
97
98
  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.
99
100
  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).
101
  Proof. apply ectxi_language_mixin. Qed.
102

103
  Definition fill (K : ectx) (e : expr Λ) : expr Λ := foldl (flip fill_item) e K.
104

105
106
  Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K2 (fill K1 e).
  Proof. apply foldl_app. Qed.
107

108
109
  Definition ectxi_lang_ectx_mixin :
    EctxLanguageMixin of_val to_val [] (flip (++)) fill head_step.
110
  Proof.
111
112
113
114
115
116
117
118
119
120
121
122
    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.
123
    - intros K K' e1 κ e1' σ1 e2 σ2 efs Hfill Hred Hstep; revert K' Hfill.
124
125
126
127
128
129
130
131
132
133
      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.
Amin Timany's avatar
Amin Timany committed
134
135
136
137
    - intros K e1 σ1 κ e2 σ2 efs.
      destruct K as [|Ki K _] using rev_ind; simpl; first by auto.
      rewrite fill_app /=.
      intros ?%head_ctx_step_val; eauto using fill_val.
138
139
  Qed.

140
141
142
  Canonical Structure ectxi_lang_ectx := EctxLanguage ectxi_lang_ectx_mixin.
  Canonical Structure ectxi_lang := LanguageOfEctx ectxi_lang_ectx.

143
144
145
  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.

146
147
148
  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.
149
  Proof.
150
151
    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.
152
  Qed.
153

154
155
  Global Instance ectxi_lang_ctx_item Ki : LanguageCtx (fill_item Ki).
  Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
156
End ectxi_language.
157

158
159
160
161
162
163
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 :=
164
165
166
  let '@EctxiLanguage E V C St K of_val to_val fill head 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 head mix)).