Commit 96a1a9f6 authored by Robbert Krebbers's avatar Robbert Krebbers

Hook languages into the Iris parameter.

parent 1fbbd48c
...@@ -408,7 +408,12 @@ Section Language. ...@@ -408,7 +408,12 @@ 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. Instance heap_lang : Language expr value state := {|
to_expr := v2e;
of_expr := e2v;
atomic := atomic;
prim_step := ectx_step
|}.
Proof. Proof.
- exact v2v. - exact v2v.
- exact e2e. - exact e2e.
......
Require Import prelude.prelude. Require Import prelude.prelude.
Class Language (E V S : Type) := { Class Language (E V St : Type) := {
to_expr : V E; to_expr : V E;
of_expr : E option V; of_expr : E option V;
atomic : E Prop; atomic : E Prop;
prim_step : E S E S option E Prop; prim_step : E St E St option E Prop;
of_to_expr v : of_expr (to_expr v) = Some v; of_to_expr v : of_expr (to_expr v) = Some v;
to_of_expr e v : of_expr e = Some v to_expr v = e; to_of_expr e v : of_expr e = Some v to_expr v = e;
values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef of_expr e = None; values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef of_expr e = None;
...@@ -14,9 +14,8 @@ Class Language (E V S : Type) := { ...@@ -14,9 +14,8 @@ Class Language (E V S : Type) := {
prim_step e1 σ1 e2 σ2 ef prim_step e1 σ1 e2 σ2 ef
is_Some (of_expr e2) is_Some (of_expr e2)
}. }.
Arguments Build_Language {_ _ _} _ _ _ _ {_ _ _ _ _}.
Section Lang. Section language.
Context `{Language E V St}. Context `{Language E V St}.
Definition cfg : Type := (list E * St)%type. Definition cfg : Type := (list E * St)%type.
...@@ -30,11 +29,12 @@ Section Lang. ...@@ -30,11 +29,12 @@ Section Lang.
Definition steps := rtc step. Definition steps := rtc step.
Definition stepn := nsteps step. Definition stepn := nsteps step.
Definition is_ctx (ctx : E -> E) : Prop := Definition is_ctx (ctx : E E) : Prop :=
(forall e, is_Some (of_expr (ctx e)) -> is_Some (of_expr e)) /\ ( e, is_Some (of_expr (ctx e)) is_Some (of_expr e))
(forall e1 σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef -> prim_step (ctx e1) σ1 (ctx e2) σ2 ef) /\ ( e1 σ1 e2 σ2 ef,
(forall e1' σ1 e2 σ2 ef, of_expr e1' = None -> prim_step (ctx e1') σ1 e2 σ2 ef -> prim_step e1 σ1 e2 σ2 ef -> prim_step (ctx e1) σ1 (ctx e2) σ2 ef)
exists e2', e2 = ctx e2' /\ prim_step e1' σ1 e2' σ2 ef). ( e1' σ1 e2 σ2 ef,
of_expr e1' = None prim_step (ctx e1') σ1 e2 σ2 ef
End Lang. e2', e2 = ctx e2' prim_step e1' σ1 e2' σ2 ef).
End language.
Require Export modures.cmra. Require Export modures.cmra iris.language.
Record iParam := IParam { Record iParam := IParam {
iexpr : Type;
ival : Type;
istate : Type; istate : Type;
icmra : cofeT cmraT; icmra : cofeT cmraT;
ilanguage : Language iexpr ival istate;
icmra_empty A : Empty (icmra A); icmra_empty A : Empty (icmra A);
icmra_empty_spec A : RAIdentity (icmra A); icmra_empty_spec A : RAIdentity (icmra A);
icmra_map {A B} (f : A -n> B) : icmra A -n> icmra B; icmra_map {A B} (f : A -n> B) : icmra A -n> icmra B;
...@@ -12,6 +15,7 @@ Record iParam := IParam { ...@@ -12,6 +15,7 @@ Record iParam := IParam {
icmra_map (g f) x icmra_map g (icmra_map f x); icmra_map (g f) x icmra_map g (icmra_map f x);
icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f) icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f)
}. }.
Existing Instances ilanguage.
Existing Instances icmra_empty icmra_empty_spec icmra_map_ne icmra_map_mono. Existing Instances icmra_empty icmra_empty_spec icmra_map_ne icmra_map_mono.
Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m : Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
......
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