Commit 4a3579b2 authored by Armaël Guéneau's avatar Armaël Guéneau

Whitespace cleanup

parent 95663185
This diff is collapsed.
......@@ -108,7 +108,7 @@ Definition null : loc := 0%nat.
Definition field : Type := nat.
(** Representation of the address of a memory cell,
as a pair of the location at which the object
as a pair of the location at which the object
is allocated and the field within this object. *)
Definition address : Type := (loc * field)%type.
......@@ -193,7 +193,7 @@ Proof using.
intros [f1 F1] [f2 F2] [f3 F3].
unfolds state_disjoint, state_union. simpls.
unfolds pfun_disjoint, pfun_union. extens. iff M [M1 M2].
split; intros x; specializes M x;
split; intros x; specializes M x;
destruct (f2 x); destruct M; auto_false.
intros x. specializes M1 x. specializes M2 x.
destruct (f2 x); destruct M1; auto_false.
......@@ -687,8 +687,8 @@ Proof using.
Qed. (* later: exploit symmetry in the proof *)
Lemma star_comm_assoc : comm_assoc heap_is_star.
Proof using.
apply comm_assoc_of_comm_and_assoc. apply star_comm. apply star_assoc.
Proof using.
apply comm_assoc_of_comm_and_assoc. apply star_comm. apply star_assoc.
Qed.
Lemma starpost_neutral : forall B (Q:B->hprop),
......@@ -2443,7 +2443,7 @@ Proof using.
asserts: (M \-- x \# x \:= M[x]).
rewrite LibMap.disjoint_eq_disjoint_dom. rewrite dom_single.
rewrite dom_remove. rewrite disjoint_single_r_eq.
unfold notin. rewrite in_remove_eq.
unfold notin. rewrite in_remove_eq.
rewrite notin_single_eq. rew_logic*.
applys pred_incl_antisym.
(* left to right *)
......
This diff is collapsed.
Require Export CFLibCredits.
Ltac xpay_core tt ::= xpay_nat_core tt.
Notation "'\$' x" := (\$_nat x)
(at level 40, format "\$ x") : heap_scope.
......@@ -1067,7 +1067,7 @@ Qed.
Ltac xlet_core cont0 cont1 cont2 :=
apply local_erase;
match goal with |- cf_let ?F1 (fun x => _) ?H ?Q =>
match goal with |- cf_let ?F1 (fun x => _) ?H ?Q =>
cont0 tt;
split; [ | cont1 x; cont2 tt ];
xtag_pre_post
......@@ -3853,10 +3853,10 @@ Ltac xcredit goal :=
(** [xpay] applys to a goal of the form [(Pay_ ;; F1) H Q].
It is used to eliminate the call to Pay, by spending one credit.
[xpay (n + m)] where [n] and [m] are numbers such that:
where [n] denotes the remainder, and [m] denotes the
payment that need to be performed (e.g. 1).
payment that need to be performed (e.g. 1).
WARNING: the interface of the latter might change.
LATER: add demos for this tactic. *)
......@@ -3886,8 +3886,8 @@ Tactic Notation "xpay" constr(goal) :=
(* ** [xpay_skip] *)
(** [xpay_skip] is used to skip the paying of one credit;
use it for development purposes only.
use it for development purposes only.
LATER: add demos for this tactic. *)
Ltac xpay_fake tt :=
......@@ -3903,11 +3903,11 @@ Tactic Notation "xpay_skip" := xpay_fake tt.
(*--------------------------------------------------------*)
(* ** [xgc_credit] *)
(* [xgc_credit_core HP] applies to a term [HP] that is an inequality
between two credit expressions, e.g. [m <= n].
(* [xgc_credit_core HP] applies to a term [HP] that is an inequality
between two credit expressions, e.g. [m <= n].
This inequality is used to change [\$n] to [\$m] in the
precondition of the goal.
LATER: add demos for this tactic. *)
Ltac xgc_credit_core HP :=
......@@ -3927,8 +3927,8 @@ Tactic Notation "xgc_credit" constr(HP) :=
in the goal, by replacing [\$ x] with the empty heap predicate \[].
Implementing using [skip_credits] then [hsimpl].
Should only be used for development purpose.
Should only be used for development purpose.
LATER: add demos for this tactic. *)
Ltac xskip_credits_base :=
......
......@@ -25,8 +25,8 @@ Hint Extern 1 (RegisterSpec not) => Provide not_spec.
- [==] at type [loc] implements comparison of locations
- [==] in general, if it returns true, then implies logical equality.
The first specification is used by default.
Use [xapp_spec infix_eq_eq_gen_spec] for the latter.
The first specification is used by default.
Use [xapp_spec infix_eq_eq_gen_spec] for the latter.
*)
Parameter infix_eq_eq_loc_spec : curried 2%nat infix_eq_eq__ /\
......@@ -142,9 +142,9 @@ Hint Extern 1 (RegisterSpec infix_star__) => Provide infix_star_spec.
Hint Extern 1 (RegisterSpec infix_slash__) => Provide infix_slash_spec.
Hint Extern 1 (RegisterSpec Pervasives_ml.mod) => Provide mod_spec.
Notation "x `/` y" := (Z.quot x y)
Notation "x `/` y" := (Z.quot x y)
(at level 69, right associativity) : charac.
Notation "x `mod` y" := (Z.rem x y)
Notation "x `mod` y" := (Z.rem x y)
(at level 69, no associativity) : charac.
(* TODO: check levels for these notations *)
......@@ -240,7 +240,7 @@ Hint Extern 1 (RegisterSpec asr) => Provide asr_spec.
(************************************************************)
(** References *)
Definition Ref {A} (v:A) (r:loc) :=
Definition Ref {A} (v:A) (r:loc) :=
r ~> `{ contents' := v }.
Axiom Ref_Heapdata : forall A,
......@@ -251,9 +251,9 @@ Existing Instance Ref_Heapdata.
(*
Proof using.
intros. applys Heapdata_prove. intros x X1 X2.
xunfold @Ref.
xunfold @Ref.
lets: star_is_single_same_loc.
hchange (@star_is_single_same_loc x). hsimpl.
hchange (@star_is_single_same_loc x). hsimpl.
Qed.
*)
......@@ -261,13 +261,13 @@ Notation "r '~~>' v" := (hdata (Ref v) r)
(at level 32, no associativity) : heap_scope.
Lemma ref_spec : forall A (v:A),
app ref [v]
PRE \[]
app ref [v]
PRE \[]
POST (fun r => r ~~> v).
Proof using. xcf_go~. Qed.
Lemma infix_emark_spec : forall A (v:A) r,
app infix_emark__ [r]
app infix_emark__ [r]
INV (r ~~> v)
POST \[= v].
Proof using. xunfold @Ref. xcf_go~. Qed.
......@@ -289,8 +289,8 @@ Notation "'App'' r `:= x" := (App infix_colon_eq__ r x;)
format "'App'' r `:= x") : charac.
Lemma incr_spec : forall (n:int) r,
app incr [r]
PRE (r ~~> n)
app incr [r]
PRE (r ~~> n)
POST (# r ~~> (n+1)).
Proof using. xcf_go~. Qed.
......@@ -309,7 +309,7 @@ Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.
(** Group of References *)
Axiom ref_spec_group : forall A (M:map loc A) (v:A),
app Pervasives_ml.ref [v]
app Pervasives_ml.ref [v]
PRE (Group Ref M)
POST (fun (r:loc) => Group Ref (M[r:=v]) \* \[r \notindom M]).
(* TODO: proof *)
......@@ -325,10 +325,10 @@ Qed.
Lemma infix_colon_eq_spec_group : forall `{Inhab A} (M:map loc A) (v:A) r,
r \indom M ->
app Pervasives_ml.infix_colon_eq__ [r v]
app Pervasives_ml.infix_colon_eq__ [r v]
PRE (Group Ref M)
POST (# Group Ref (M[r:=v])).
Proof using.
Proof using.
intros. rewrite~ (Group_rem r M). xapp. intros tt.
hchanges~ (Group_add' r M).
Qed.
......@@ -338,14 +338,14 @@ Qed.
(** Pairs *)
Lemma fst_spec : forall A B (x:A) (y:B),
app fst [(x,y)]
PRE \[]
app fst [(x,y)]
PRE \[]
POST \[= x].
Proof using. xcf_go~. Qed.
Lemma snd_spec : forall A B (x:A) (y:B),
app snd [(x,y)]
PRE \[]
app snd [(x,y)]
PRE \[]
POST \[= y].
Proof using. xcf_go~. Qed.
......@@ -356,9 +356,9 @@ Hint Extern 1 (RegisterSpec snd) => Provide snd_spec.
(************************************************************)
(** Unit *)
Lemma ignore_spec :
app ignore [tt]
PRE \[]
Lemma ignore_spec :
app ignore [tt]
PRE \[]
POST \[= tt].
Proof using. xcf_go~. Qed.
......@@ -392,7 +392,7 @@ Instance Ref_Heapdata : forall a A (T:htype A a),
Proof using.
intros. applys Heapdata_prove. intros x X1 X2.
unfold Ref. hdata_simpl. hextract as x1 x2.
hchange (@star_is_single_same_loc x). hsimpl.
hchange (@star_is_single_same_loc x). hsimpl.
Qed.
Open Local Scope heap_scope_advanced.
......@@ -402,7 +402,7 @@ Notation "'~~>' v" := (~> Ref (@Id _) v)
(*
Notation "l '~~>' v" := (r ~> Ref (@Id _) v)
(at level 32, no associativity) : heap_scope.
(at level 32, no associativity) : heap_scope.
*)
Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) r)
(at level 32, no associativity) : heap_scope.
......
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