Commit 4cc3a7e0 authored by Ralf Jung's avatar Ralf Jung

use nice record syntax to instantiate language

parent 13fdd51e
...@@ -406,19 +406,26 @@ Section Language. ...@@ -406,19 +406,26 @@ Section Language.
Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) := Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef. exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef.
Instance heap_lang : Language expr value state := Build_Language v2e e2v atomic ectx_step. Program Instance heap_lang : Language expr value state := {|
Proof. of_val := v2e;
- exact v2v. to_val := e2v;
- exact e2e. language.atomic := atomic;
- intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2. language.prim_step := ectx_step;
eapply fill_not_value. eapply reducible_not_value. do 4 eexists; eassumption. to_of_val := v2v;
- exact atomic_not_value. of_to_val := e2e;
- intros ? ? ? ? ? Hatomic (K & e1' & e2' & Heq1 & Heq2 & Hstep). language.atomic_not_value := atomic_not_value
subst. move: (Hatomic). rewrite (atomic_fill e1' K). (* RJ: this is kind of annoying. *) |}.
+ rewrite !fill_empty. eauto using atomic_step. Next Obligation.
+ assumption. intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2.
+ clear Hatomic. eapply reducible_not_value. do 4 eexists; eassumption. eapply fill_not_value. eapply reducible_not_value. do 4 eexists; eassumption.
Defined. Qed.
Next Obligation.
intros ? ? ? ? ? Hatomic (K & e1' & e2' & Heq1 & Heq2 & Hstep).
subst. move: (Hatomic). rewrite (atomic_fill e1' K).
- rewrite !fill_empty. eauto using atomic_step.
- assumption.
- clear Hatomic. eapply reducible_not_value. do 4 eexists; eassumption.
Qed.
(** We can have bind with arbitrary evaluation contexts **) (** We can have bind with arbitrary evaluation contexts **)
Lemma fill_is_ctx K: is_ctx (fill K). Lemma fill_is_ctx K: is_ctx (fill K).
......
...@@ -14,7 +14,6 @@ Class Language (E V St : Type) := { ...@@ -14,7 +14,6 @@ Class Language (E V St : Type) := {
prim_step e1 σ1 e2 σ2 ef prim_step e1 σ1 e2 σ2 ef
is_Some (to_val e2) is_Some (to_val e2)
}. }.
Arguments Build_Language {_ _ _} _ _ _ _ {_ _ _ _ _}.
Section language. Section language.
Context `{Language E V St}. Context `{Language E V St}.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment