language.v 4.14 KB
Newer Older
 Ralf Jung committed Nov 22, 2016 1 ``````From iris.algebra Require Export ofe. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Ralf Jung committed Jan 04, 2016 3 `````` `````` Robbert Krebbers committed Feb 01, 2016 4 5 6 7 8 9 ``````Structure language := Language { expr : Type; val : Type; state : Type; of_val : val → expr; to_val : expr → option val; `````` Robbert Krebbers committed Aug 08, 2016 10 `````` prim_step : expr → state → expr → state → list expr → Prop; `````` Robbert Krebbers committed Jan 17, 2016 11 12 `````` to_of_val v : to_val (of_val v) = Some v; of_to_val e v : to_val e = Some v → of_val v = e; `````` Robbert Krebbers committed Aug 08, 2016 13 `````` val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs → to_val e = None `````` Ralf Jung committed Jan 04, 2016 14 ``````}. `````` Janno committed Aug 25, 2016 15 16 17 ``````Delimit Scope expr_scope with E. Delimit Scope val_scope with V. Bind Scope expr_scope with expr. `````` Jacques-Henri Jourdan committed Jan 04, 2017 18 ``````Bind Scope val_scope with val. `````` Robbert Krebbers committed Feb 01, 2016 19 20 21 22 23 ``````Arguments of_val {_} _. Arguments to_val {_} _. Arguments prim_step {_} _ _ _ _ _. Arguments to_of_val {_} _. Arguments of_to_val {_} _ _ _. `````` Robbert Krebbers committed Mar 02, 2016 24 ``````Arguments val_stuck {_} _ _ _ _ _ _. `````` Robbert Krebbers committed Feb 01, 2016 25 `````` `````` Robbert Krebbers committed Mar 18, 2016 26 27 28 ``````Canonical Structure stateC Λ := leibnizC (state Λ). Canonical Structure valC Λ := leibnizC (val Λ). Canonical Structure exprC Λ := leibnizC (expr Λ). `````` Robbert Krebbers committed Feb 01, 2016 29 30 `````` Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type. `````` Ralf Jung committed Jan 04, 2016 31 `````` `````` Robbert Krebbers committed Mar 15, 2017 32 33 34 35 36 37 38 39 40 41 42 ``````Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := { fill_not_val e : to_val e = None → to_val (K e) = None; fill_step e1 σ1 e2 σ2 efs : prim_step e1 σ1 e2 σ2 efs → prim_step (K e1) σ1 (K e2) σ2 efs; fill_step_inv e1' σ1 e2 σ2 efs : to_val e1' = None → prim_step (K e1') σ1 e2 σ2 efs → ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 efs }. `````` Robbert Krebbers committed Sep 21, 2017 43 44 45 ``````Instance language_ctx_id Λ : LanguageCtx Λ id. Proof. constructor; naive_solver. Qed. `````` Robbert Krebbers committed Jan 16, 2016 46 ``````Section language. `````` Robbert Krebbers committed Feb 01, 2016 47 48 `````` Context {Λ : language}. Implicit Types v : val Λ. `````` Ralf Jung committed Jan 04, 2016 49 `````` `````` Robbert Krebbers committed Feb 01, 2016 50 `````` Definition reducible (e : expr Λ) (σ : state Λ) := `````` Robbert Krebbers committed Aug 08, 2016 51 `````` ∃ e' σ' efs, prim_step e σ e' σ' efs. `````` 52 `````` Definition irreducible (e : expr Λ) (σ : state Λ) := `````` Robbert Krebbers committed Mar 15, 2017 53 54 `````` ∀ e' σ' efs, ¬prim_step e σ e' σ' efs. `````` Jacques-Henri Jourdan committed Jul 20, 2016 55 `````` Definition atomic (e : expr Λ) : Prop := `````` 56 `````` ∀ σ e' σ' efs, prim_step e σ e' σ' efs → irreducible e' σ'. `````` Robbert Krebbers committed Mar 15, 2017 57 `````` `````` Robbert Krebbers committed Feb 01, 2016 58 `````` Inductive step (ρ1 ρ2 : cfg Λ) : Prop := `````` Robbert Krebbers committed Aug 08, 2016 59 `````` | step_atomic e1 σ1 e2 σ2 efs t1 t2 : `````` Robbert Krebbers committed Feb 01, 2016 60 `````` ρ1 = (t1 ++ e1 :: t2, σ1) → `````` Robbert Krebbers committed Aug 08, 2016 61 62 `````` ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) → prim_step e1 σ1 e2 σ2 efs → `````` Robbert Krebbers committed Feb 01, 2016 63 64 `````` step ρ1 ρ2. `````` Robbert Krebbers committed Apr 19, 2016 65 66 `````` Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v. Proof. intros <-. by rewrite to_of_val. Qed. `````` Robbert Krebbers committed Mar 15, 2017 67 68 69 `````` Lemma not_reducible e σ : ¬reducible e σ ↔ irreducible e σ. Proof. unfold reducible, irreducible. naive_solver. Qed. `````` Robbert Krebbers committed Jan 19, 2016 70 `````` Lemma reducible_not_val e σ : reducible e σ → to_val e = None. `````` Robbert Krebbers committed Mar 02, 2016 71 `````` Proof. intros (?&?&?&?); eauto using val_stuck. Qed. `````` 72 73 `````` Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ. Proof. intros [??] ??? ?%val_stuck. by destruct (to_val e). Qed. `````` Robbert Krebbers committed Aug 08, 2016 74 `````` Global Instance of_val_inj : Inj (=) (=) (@of_val Λ). `````` Robbert Krebbers committed Feb 11, 2016 75 `````` Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. `````` Ralf Jung committed Jan 05, 2016 76 `````` `````` Robbert Krebbers committed Mar 15, 2017 77 78 79 80 81 82 83 84 85 `````` Lemma reducible_fill `{LanguageCtx Λ K} e σ : to_val e = None → reducible (K e) σ → reducible e σ. Proof. intros ? (e'&σ'&efs&Hstep); unfold reducible. apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto. Qed. Lemma irreducible_fill `{LanguageCtx Λ K} e σ : to_val e = None → irreducible e σ → irreducible (K e) σ. Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed. `````` Robbert Krebbers committed Sep 24, 2017 86 87 88 89 90 91 92 93 94 95 `````` Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 : t1 ≡ₚ t1' → step (t1,σ1) (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) (t2',σ2). Proof. intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=. move: Ht; rewrite -Permutation_middle (symmetry_iff (≡ₚ)). intros (tl'&tr'&->&Ht)%Permutation_cons_inv. exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor]. by rewrite -!Permutation_middle !assoc_L Ht. Qed. `````` Dan Frumin committed Sep 25, 2017 96 97 98 99 100 101 102 103 `````` Class PureExec (P : Prop) (e1 e2 : expr Λ) := { pure_exec_safe σ : P → reducible e1 σ; pure_exec_puredet σ1 e2' σ2 efs : P → prim_step e1 σ1 e2' σ2 efs → σ1 = σ2 ∧ e2 = e2' ∧ efs = []; }. `````` Robbert Krebbers committed Oct 05, 2017 104 `````` Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) : `````` Dan Frumin committed Sep 25, 2017 105 106 107 `````` (P → PureExec True e1 e2) → PureExec P e1 e2. Proof. intros HPE. split; intros; eapply HPE; eauto. Qed. `````` Dan Frumin committed Sep 25, 2017 108 109 110 111 `````` (* This is a family of frequent assumptions for PureExec *) Class IntoVal (e : expr Λ) (v : val Λ) := into_val : to_val e = Some v. `````` Robbert Krebbers committed Mar 15, 2017 112 ``End language.``