Commit cd2f9a5d authored by Robbert Krebbers's avatar Robbert Krebbers

Better naming for binop stuff.

parent 09ef8477
......@@ -20,8 +20,8 @@ Inductive context_item : Type :=
| CTX_CaseM (e0 : expr) (e2 : expr)
| CTX_CaseR (e0 : expr) (e1 : expr)
(* Nat bin op *)
| CTX_NBOPL (op : NatBinOP) (e2 : expr)
| CTX_NBOPR (op : NatBinOP) (e1 : expr)
| CTX_BinOpL (op : binop) (e2 : expr)
| CTX_BinOpR (op : binop) (e1 : expr)
(* If *)
| CTX_IfL (e1 : expr) (e2 : expr)
| CTX_IfM (e0 : expr) (e2 : expr)
......@@ -58,8 +58,8 @@ Fixpoint fill_ctx_item (ctx : context_item) (e : expr) : expr :=
| CTX_CaseL e1 e2 => Case e e1 e2
| CTX_CaseM e0 e2 => Case e0 e e2
| CTX_CaseR e0 e1 => Case e0 e1 e
| CTX_NBOPL op e2 => NBOP op e e2
| CTX_NBOPR op e1 => NBOP op e1 e
| CTX_BinOpL op e2 => BinOp op e e2
| CTX_BinOpR op e1 => BinOp op e1 e
| CTX_IfL e1 e2 => If e e1 e2
| CTX_IfM e0 e2 => If e0 e e2
| CTX_IfR e0 e1 => If e0 e1 e
......@@ -126,12 +126,12 @@ Inductive typed_context_item :
| TP_CTX_IfR (e0 : expr) (e1 : expr) : Γ τ,
typed Γ e0 (TBool) typed Γ e1 τ
typed_context_item (CTX_IfR e0 e1) Γ τ Γ τ
| TP_CTX_NBOPL op (e2 : expr) : Γ,
| TP_CTX_BinOpL op (e2 : expr) : Γ,
typed Γ e2 TNat
typed_context_item (CTX_NBOPL op e2) Γ TNat Γ (NatBinOP_res_type op)
| TP_CTX_NBOPR op (e1 : expr) : Γ,
typed_context_item (CTX_BinOpL op e2) Γ TNat Γ (binop_res_type op)
| TP_CTX_BinOpR op (e1 : expr) : Γ,
typed Γ e1 TNat
typed_context_item (CTX_NBOPR op e1) Γ TNat Γ (NatBinOP_res_type op)
typed_context_item (CTX_BinOpR op e1) Γ TNat Γ (binop_res_type op)
| TP_CTX_Fold : Γ τ,
typed_context_item CTX_Fold Γ τ.[(TRec τ)/] Γ (TRec τ)
| TP_CTX_Unfold : Γ τ,
......
......@@ -10,7 +10,7 @@ Section CG_Counter.
(* Coarse-grained increment *)
Definition CG_increment (x : expr) : expr :=
Lam ((Store x.[ren (+ 2)] (NBOP Add ( 1) (Load x.[ren (+ 2)])))).
Lam ((Store x.[ren (+ 2)] (BinOp Add ( 1) (Load x.[ren (+ 2)])))).
Lemma CG_increment_type x Γ :
typed Γ x (Tref TNat)
......@@ -36,7 +36,7 @@ Section CG_Counter.
Proof.
iIntros {HNE} "[#Hspec [Hx Hj]]". unfold CG_increment.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_load _ _ _ j (K ++ [StoreRCtx (LocV _); NBOPRCtx _ (v _)])
iPvs (step_load _ _ _ j (K ++ [StoreRCtx (LocV _); BinOpRCtx _ (v _)])
_ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial.
......@@ -202,7 +202,7 @@ Section CG_Counter.
Definition FG_increment (x : expr) : expr :=
Lam (App (Lam
(* try increment *)
(If (CAS x.[ren (+4)] (Var 1) (NBOP Add ( 1) (Var 1)))
(If (CAS x.[ren (+4)] (Var 1) (BinOp Add ( 1) (Var 1)))
Unit (* increment succeeds we return unit *)
(App (Var 2) (Var 3)) (* increment fails, we try again *)
)
......
......@@ -189,13 +189,13 @@ Section typed_interp.
Lemma typed_binary_interp_nat_bin_op Δ Γ op e1 e2 e1' e2' {HΔ : ✓✓ Δ}
(IHHtyped1 : Δ Γ e1 log e1' TNat)
(IHHtyped2 : Δ Γ e2 log e2' TNat) :
Δ Γ NBOP op e1 e2 log NBOP op e1' e2' NatBinOP_res_type op.
Δ Γ BinOp op e1 e2 log BinOp op e1' e2' binop_res_type op.
Proof.
iIntros {vs Hlen ρ j K} "(#Hheap & #Hspec & #HΓ & Htr)"; cbn.
smart_wp_bind (NBOPLCtx _ _) v v' "[Hv #Hiv]"
(IHHtyped1 _ _ _ j (K ++ [NBOPLCtx _ _])); cbn.
smart_wp_bind (NBOPRCtx _ _) w w' "[Hw #Hiw]"
(IHHtyped2 _ _ _ j (K ++ [NBOPRCtx _ _])); cbn.
smart_wp_bind (BinOpLCtx _ _) v v' "[Hv #Hiv]"
(IHHtyped1 _ _ _ j (K ++ [BinOpLCtx _ _])); cbn.
smart_wp_bind (BinOpRCtx _ _) w w' "[Hw #Hiw]"
(IHHtyped2 _ _ _ j (K ++ [BinOpRCtx _ _])); cbn.
iDestruct "Hiv" as {n} "[% %]"; subst; simpl.
iDestruct "Hiw" as {n'} "[% %]"; subst; simpl.
iPvs (step_nat_bin_op _ _ _ j K _ _ _ _ with "* [-]") as "Hz".
......
......@@ -42,8 +42,8 @@ Section typed_interp.
- (* nat *) value_case; iExists _ ; trivial.
- (* bool *) value_case; iExists _ ; trivial.
- (* nat bin op *)
smart_wp_bind (NBOPLCtx _ e2.[env_subst vs]) v "#Hv" IHHtyped1.
smart_wp_bind (NBOPRCtx _ v) v' "# Hv'" IHHtyped2.
smart_wp_bind (BinOpLCtx _ e2.[env_subst vs]) v "#Hv" IHHtyped1.
smart_wp_bind (BinOpRCtx _ v) v' "# Hv'" IHHtyped2.
iDestruct "Hv" as {n} "%"; iDestruct "Hv'" as {n'} "%"; subst. simpl.
iApply wp_nat_bin_op. iNext; destruct op; simpl;
try destruct eq_nat_dec; try destruct le_dec; try destruct lt_dec;
......
......@@ -8,14 +8,14 @@ Module lang.
Global Instance loc_dec_eq (l l' : loc) : Decision (l = l') := _.
Inductive NatBinOP :=
Inductive binop :=
| Add
| Sub
| Eq
| Le
| Lt.
Global Instance Natbinop_dec_eq (op op' : NatBinOP) : Decision (op = op').
Global Instance Natbinop_dec_eq (op op' : binop) : Decision (op = op').
Proof. unfold Decision. decide equality. Qed.
Inductive expr :=
......@@ -26,7 +26,7 @@ Module lang.
| Unit
| Nat (n : nat)
| Bool (b : bool)
| NBOP (op : NatBinOP) (e1 e2 : expr)
| BinOp (op : binop) (e1 e2 : expr)
(* If then else *)
| If (e0 e1 e2 : expr)
(* Products *)
......@@ -85,7 +85,7 @@ Module lang.
Notation "'♭v' b" := (BoolV b) (at level 200).
Notation "'♯v' n" := (NatV n) (at level 200).
Fixpoint NatBinOP_meaning (op : NatBinOP) : nat nat val :=
Fixpoint binop_meaning (op : binop) : nat nat val :=
match op with
| Add => λ a b, v(a + b)
| Sub => λ a b, v(a - b)
......@@ -140,8 +140,8 @@ Module lang.
| TAppCtx
| PairLCtx (e2 : expr)
| PairRCtx (v1 : val)
| NBOPLCtx (op : NatBinOP) (e2 : expr)
| NBOPRCtx (op : NatBinOP) (v1 : val)
| BinOpLCtx (op : binop) (e2 : expr)
| BinOpRCtx (op : binop) (v1 : val)
| FstCtx
| SndCtx
| InjLCtx
......@@ -167,8 +167,8 @@ Module lang.
| TAppCtx => TApp e
| PairLCtx e2 => Pair e e2
| PairRCtx v1 => Pair (of_val v1) e
| NBOPLCtx op e2 => NBOP op e e2
| NBOPRCtx op v1 => NBOP op (of_val v1) e
| BinOpLCtx op e2 => BinOp op e e2
| BinOpRCtx op v1 => BinOp op (of_val v1) e
| FstCtx => Fst e
| SndCtx => Snd e
| InjLCtx => InjL e
......@@ -210,8 +210,8 @@ Module lang.
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
(* nat bin op *)
| NBOPS op a b σ :
head_step (NBOP op ( a) (b)) σ (of_val (NatBinOP_meaning op a b)) σ None
| BinOpS op a b σ :
head_step (BinOp op ( a) (b)) σ (of_val (binop_meaning op a b)) σ None
(* If then else *)
| IfFalse e1 e2 σ :
head_step (If ( false) e1 e2) σ e2 σ None
......
......@@ -466,10 +466,10 @@ Section lang_rules.
Qed.
Lemma wp_nat_bin_op E op a b Φ :
Φ (NatBinOP_meaning op a b) WP (NBOP op ( a) ( b)) @ E {{Φ}}.
Φ (binop_meaning op a b) WP (BinOp op ( a) ( b)) @ E {{Φ}}.
Proof.
rewrite -(wp_lift_pure_det_step
(NBOP _ _ _) (of_val (NatBinOP_meaning op a b)) None) //=.
(BinOp _ _ _) (of_val (binop_meaning op a b)) None) //=.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
- intros. inv_step; auto.
Qed.
......
......@@ -605,8 +605,8 @@ Section lang_rules.
Lemma step_nat_bin_op N E ρ j K op a b :
nclose N E
Spec_ctx N ρ j fill K (NBOP op ( a) ( b))
={E}=> j fill K (of_val (NatBinOP_meaning op a b)).
Spec_ctx N ρ j fill K (BinOp op ( a) ( b))
={E}=> j fill K (of_val (binop_meaning op a b)).
Proof. apply step_pure => σ; econstructor. Qed.
Lemma step_fork_base k j K e h ρ :
......
......@@ -19,7 +19,7 @@ Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
Fixpoint NatBinOP_res_type (op : NatBinOP) : type :=
Fixpoint binop_res_type (op : binop) : type :=
match op with
| Add => TNat | Sub => TNat
| Eq => TBool | Le => TBool | Lt => TBool
......@@ -38,9 +38,9 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
| Unit_typed : typed Γ Unit TUnit
| Nat_typed n : typed Γ ( n) TNat
| Bool_typed b : typed Γ ( b) TBool
| NBOP_typed op e1 e2 :
| BinOp_typed op e1 e2 :
typed Γ e1 TNat typed Γ e2 TNat
typed Γ (NBOP op e1 e2) (NatBinOP_res_type op)
typed Γ (BinOp op e1 e2) (binop_res_type op)
| Pair_typed e1 e2 τ1 τ2 :
typed Γ e1 τ1 typed Γ e2 τ2 typed Γ (Pair e1 e2) (TProd τ1 τ2)
| Fst_typed e τ1 τ2 : typed Γ e (TProd τ1 τ2) typed Γ (Fst e) τ1
......
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