Started update on lifting.v

parent f70759be
Pipeline #6197 failed with stages
in 0 seconds
......@@ -14,7 +14,7 @@ Inductive side : Set :=
| Left
| Right.
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) | LitChan (l : loc) (s : side) (* | LitBuf (l : list Z) (r : list Z) *).
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) | LitChan (l : loc) (s : side).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
......@@ -66,14 +66,11 @@ Inductive expr :=
| CAS (e0 : expr) (e1 : expr) (e2 : expr)
| FAA (e1 : expr) (e2 : expr)
(* Process *)
| Start (e : expr)
| Start (c e : expr)
(* Channels *)
| NewChan
| Send (c e : expr)
| Recv (c : expr).
(* (* Lists *) *)
(* | Cons (x : expr) (xs : expr) *)
(* | Nil. *)
Bind Scope expr_scope with expr.
......@@ -81,10 +78,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Var x => bool_decide (x X)
| Rec f x e => is_closed (f :b: x :b: X) e
| Lit _ | NewChan (* | Nil *) => true
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e | Start e | Recv e =>
| Lit _ | NewChan => true
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e | Recv e =>
is_closed X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | Send e1 e2 (* | Cons e1 e2 *) =>
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | Send e1 e2 | Start e1 e2 =>
is_closed X e1 && is_closed X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
is_closed X e0 && is_closed X e1 && is_closed X e2
......@@ -101,8 +98,7 @@ Inductive val :=
| LitV (l : base_lit)
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val)
(* | ListV (l : list val) *).
| InjRV (v : val).
Bind Scope val_scope with val.
......@@ -113,10 +109,6 @@ Fixpoint of_val (v : val) : expr :=
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
(* | ListV l => match l with *)
(* | [] => Nil *)
(* | x::xs => Cons (of_val x) (of_val xs) *)
(* end *)
end.
Fixpoint to_val (e : expr) : option val :=
......@@ -158,8 +150,6 @@ Proof.
eapply (Build_Countable _ _ encode decode).
by intros [|].
Qed.
(* Global Instance list_eq_dec' : (forall x y:A, Decision (x = y)) -> forall xs ys : list A, Decision (xs = ys). *)
(* Proof. solve_decision. Qed. *)
Instance base_lit_eq_dec : EqDecision base_lit.
Proof. solve_decision. Defined.
......@@ -231,7 +221,7 @@ Proof.
| Store e1 e2 => GenNode 14 [go e1; go e2]
| CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
| FAA e1 e2 => GenNode 16 [go e1; go e2]
| Start e => GenNode 17 [go e] (* Added *)
| Start e1 e2 => GenNode 17 [go e1; go e2] (* Added *)
| NewChan => GenNode 18 []
| Send e1 e2 => GenNode 19 [go e1; go e2]
| Recv e => GenNode 20 [go e]
......@@ -257,7 +247,7 @@ Proof.
| GenNode 14 [e1; e2] => Store (go e1) (go e2)
| GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
| GenNode 16 [e1; e2] => FAA (go e1) (go e2)
| GenNode 17 [e] => Start (go e) (* Added *)
| GenNode 17 [e1; e2] => Start (go e1) (go e2) (* Added *)
| GenNode 18 [] => NewChan
| GenNode 19 [e1; e2] => Send (go e1) (go e2)
| GenNode 20 [e] => Recv (go e)
......@@ -299,7 +289,8 @@ Inductive ectx_item :=
| CasRCtx (v0 : val) (v1 : val)
| FaaLCtx (e2 : expr)
| FaaRCtx (v1 : val)
| StartCtx
| StartLCtx (e2 : expr)
| StartRCtx (v1 : val)
| SendLCtx (e2 : expr)
| SendRCtx (v1 : val)
| RecvCtx.
......@@ -328,7 +319,8 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
| FaaLCtx e2 => FAA e e2
| FaaRCtx v1 => FAA (of_val v1) e
| StartCtx => Start e
| StartLCtx e2 => Start e e2
| StartRCtx v1 => Start (of_val v1) e
| SendLCtx e2 => Send e e2
| SendRCtx v1 => Send (of_val v1) e
| RecvCtx => Recv e
......@@ -357,7 +349,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Store e1 e2 => Store (subst x es e1) (subst x es e2)
| CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
| FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
| Start e => Start (subst x es e)
| Start e1 e2 => Start (subst x es e1) (subst x es e2)
| NewChan => NewChan
| Send e1 e2 => Send (subst x es e1) (subst x es e2)
| Recv e => Recv (subst x es e)
......@@ -574,6 +566,8 @@ Fixpoint forPairs (i : loc) (pes : list pexpr) (es : list expr) : Prop :=
| (_,_) => False
end.
Definition inv_side (s : side) : side := match s with Left => Right | Right => Left end.
Inductive head_step'' : pexpr state'' pexpr state'' list (pexpr) Prop :=
| ExprS' p pσs pσc e σ
pσs' pσc' e' σ'
......@@ -583,10 +577,10 @@ Inductive head_step'' : pexpr → state'' → pexpr → state'' → list (pexpr)
forPairs p pes es
head_step' e (σ,pσc) e' (σ',pσc') es
head_step'' (p,e) (pσs, pσc) (p,e') (pσs', pσc') pes
| StartS p e σp σc p' v :
| StartS p l s e x σp σc p' :
σp !! p' = None
to_val e = Some $ v
head_step'' (p, (Start e)) (σp,σc) (p, (Lit $ LitUnit)) (<[p':=]>σp, σc) [(p', e)].
Closed (BAnon :b: x :b: []) e
head_step'' (p, Start (Lit $ LitChan l s) (Rec BAnon x e)) (σp,σc) (p, Lit LitUnit) (<[p':=]>σp, σc) [(p', App (Rec BAnon x e) (Lit $ LitChan l (inv_side s)))].
(** Basic properties about the language *)
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
......@@ -637,7 +631,7 @@ Lemma head_ctx_step_val'' Ki e σ1 e2 σ2 efs :
Proof.
inversion 1.
- apply to_val_val''. generalize dependent H9. apply head_ctx_step_val'.
- apply to_val_val''. generalize dependent H; destruct Ki; inversion_clear 1; unfold pexpr_to_expr; simplify_option_eq; by eauto.
- apply to_val_val''. generalize dependent H; destruct Ki; inversion_clear 1; unfold pexpr_to_expr; destruct e; simplify_option_eq; by eauto.
Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
......@@ -747,19 +741,19 @@ Lemma subst_rec_ne' f y e x es :
subst' x es (Rec f y e) = Rec f y (subst' x es e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma dist_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
Proof.
split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
Qed.
(* Lemma dist_lang_mixin_orig : EctxiLanguageMixin of_val to_val fill_item head_step. *)
(* Proof. *)
(* split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck, *)
(* fill_item_val, fill_item_no_val_inj, head_ctx_step_val. *)
(* Qed. *)
Lemma dist_lang_mixin' : EctxiLanguageMixin of_val to_val fill_item head_step'.
Proof.
split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck',
fill_item_val, fill_item_no_val_inj, head_ctx_step_val'.
Qed.
(* Lemma dist_lang_mixin_chan : EctxiLanguageMixin of_val to_val fill_item head_step'. *)
(* Proof. *)
(* split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck', *)
(* fill_item_val, fill_item_no_val_inj, head_ctx_step_val'. *)
(* Qed. *)
Lemma dist_lang_mixin'' : EctxiLanguageMixin of_val'' to_val'' fill_item'' head_step''.
Lemma dist_lang_mixin : EctxiLanguageMixin of_val'' to_val'' fill_item'' head_step''.
Proof.
split; apply _ || eauto using to_of_val'', of_to_val'', val_head_stuck'',
fill_item_val'', fill_item_no_val_inj'', head_ctx_step_val''.
......@@ -767,20 +761,20 @@ Qed.
End dist_lang.
(** Language *)
Canonical Structure dist_ectxi_lang := EctxiLanguage dist_lang.dist_lang_mixin.
Canonical Structure dist_ectx_lang := EctxLanguageOfEctxi dist_ectxi_lang.
Canonical Structure dist_lang := LanguageOfEctx dist_ectx_lang.
(* (** Language *) *)
(* Canonical Structure dist_ectxi_lang_orig := EctxiLanguage dist_lang.dist_lang_mixin_orig. *)
(* Canonical Structure dist_ectx_lang_orig := EctxLanguageOfEctxi dist_ectxi_lang_orig. *)
(* Canonical Structure dist_lang_orig := LanguageOfEctx dist_ectx_lang_orig. *)
(** Language' *)
Canonical Structure dist_ectxi_lang' := EctxiLanguage dist_lang.dist_lang_mixin'.
Canonical Structure dist_ectx_lang' := EctxLanguageOfEctxi dist_ectxi_lang'.
Canonical Structure dist_lang' := LanguageOfEctx dist_ectx_lang'.
(* (** Language' *) *)
(* Canonical Structure dist_ectxi_lang_chan := EctxiLanguage dist_lang.dist_lang_mixin_chan. *)
(* Canonical Structure dist_ectx_lang_chan := EctxLanguageOfEctxi dist_ectxi_lang_chan. *)
(* Canonical Structure dist_lang_chan := LanguageOfEctx dist_ectx_lang_chan. *)
(** Language'' *)
Canonical Structure dist_ectxi_lang'' := EctxiLanguage dist_lang.dist_lang_mixin''.
Canonical Structure dist_ectx_lang'' := EctxLanguageOfEctxi dist_ectxi_lang''.
Canonical Structure dist_lang'' := LanguageOfEctx dist_ectx_lang''.
Canonical Structure dist_ectxi_lang := EctxiLanguage dist_lang.dist_lang_mixin.
Canonical Structure dist_ectx_lang := EctxLanguageOfEctxi dist_ectxi_lang.
Canonical Structure dist_lang := LanguageOfEctx dist_ectx_lang.
(* Prefer dist_lang names over ectx_language names. *)
Export dist_lang.
......@@ -794,3 +788,4 @@ Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx BAnon e2).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
Notation StartC e := (Let (BNamed "c") NewChan (Seq (Start (Snd (BNamed "c")) e) ((Fst (BNamed "c"))))).
\ No newline at end of file
From iris.algebra Require Import auth gmap frac agree.
From iris.base_logic Require Export gen_heap.
From iris.program_logic Require Export weakestpre lifting.
From iris.program_logic Require Import ectx_lifting.
......@@ -10,14 +11,90 @@ Import uPred.
(** Basic rules for language operations. *)
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc val Σ
(* Definition heapUR : ucmraT := *)
(* gen_heapUR loc val. *)
(* (* gmapUR loc (prodR fracR (agreeR (leibnizC val))). *) *)
(* Class heapG Σ := HeapG { *)
(* heapG_invG : invG Σ; *)
(* heapG_gen_heapG :> gen_heapG loc val Σ *)
(* }. *)
(* Definition procUR : ucmraT := *)
(* gen_heapUR loc heapUR. *)
(* (* gmapUR loc heapUR. *) *)
(* Definition chanUR : ucmraT := *)
(* gen_heapUR loc (exclR (prodC (listC valC) (listC valC))). *)
(* Definition distUR : ucmraT := *)
(* prodUR procUR chanUR. *)
(* --------- Concrete definition of dist CMRA --------- *)
(* Definition gen_distUR (L V : Type) `{Countable L} : ucmraT := *)
(* prodUR *)
(* (gmapUR L (gmapUR L (prodR fracR (agreeR (leibnizC V))))) *)
(* (gmapUR L (exclR (prodC (listC (leibnizC V)) (listC (leibnizC V))))). *)
(* Definition to_gen_dist {L V} `{Countable L} (σ : ((gmap L (gmap L V)) * (gmap L (list V * list V)))) : gen_distUR L V := *)
(* ((fmap (λ v, *)
(* (((fmap (λ v', *)
(* (1%Qp, to_agree (v' : leibnizC V))) v)))) (σ.1)), *)
(* (fmap (λ c, (Excl (c.1 : listC (leibnizC V), c.2 : listC (leibnizC V)))) (σ.2))). *)
(* Class gen_distG (L V : Type) (Σ :gFunctors) `{Countable L} := Gen_DistG { *)
(* gen_dist_inG :> inG Σ (authR (gen_distUR L V)); (* Why authR? *) *)
(* gen_dist_name : gname *)
(* }. *)
(* Arguments gen_dist_name {_ _ _ _ _} _ : assert. *)
(* Section definitions. *)
(* Context `{dG : gen_distG L V Σ}. *)
(* Definition gen_dist_ctx (σ : (gmap L (gmap L V)) * (gmap L (list V * list V))) : iProp Σ := *)
(* own (gen_dist_name dG) (● (to_gen_dist σ)) (* ∗ gen_heap_ctx (snd σ) *). *)
(* End definitions. *)
(* Class distG Σ := DistG { *)
(* distG_invG : invG Σ; *)
(* distG_gen_distG :> gen_distG loc val Σ *)
(* }. *)
(* Instance distG_irisG `{distG Σ} : irisG dist_lang Σ := { *)
(* iris_invG := distG_invG; *)
(* state_interp := gen_dist_ctx *)
(* }. *)
(* Global Opaque iris_invG. *)
(* ---------- Definition of dist CMRA based on heap CMRA ------------------- *)
Definition gen_distUR (L V : Type) `{Countable L} : ucmraT :=
prodUR (gen_heapUR L (gen_heapUR L V)) (gen_heapUR L (list V * list V)).
Definition to_gen_dist {L V} `{Countable L} (σ : ((gmap L (gmap L V)) * (gmap L (list V * list V)))) : gen_distUR L V :=
((fmap (λ v, (1%Qp, to_agree (to_gen_heap v))) σ.1),
(to_gen_heap σ.2)).
Class gen_distG (L V : Type) (Σ :gFunctors) `{Countable L} := Gen_DistG {
gen_dist_inG :> inG Σ (authR (gen_distUR L V)); (* Why authR? *)
gen_dist_name : gname
}.
Arguments gen_dist_name {_ _ _ _ _} _ : assert.
Section definitions.
Context `{dG : gen_distG L V Σ}.
Definition gen_dist_ctx (σ : (gmap L (gmap L V)) * (gmap L (list V * list V))) : iProp Σ :=
own (gen_dist_name dG) ( (to_gen_dist σ)) (* ∗ gen_heap_ctx (snd σ) *).
End definitions.
Class distG Σ := DistG {
distG_invG : invG Σ;
distG_gen_distG :> gen_distG loc val Σ
}.
Instance heapG_irisG `{heapG Σ} : irisG dist_lang Σ := {
iris_invG := heapG_invG;
state_interp := gen_heap_ctx
Instance distG_irisG `{distG Σ} : irisG dist_lang Σ := {
iris_invG := distG_invG;
state_interp := gen_dist_ctx
}.
Global Opaque iris_invG.
......@@ -55,7 +132,7 @@ Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
Section lifting.
Context `{heapG Σ}.
Context `{distG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types efs : list expr.
......
......@@ -152,9 +152,4 @@ Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Definition tmptmp := true && false.
Definition tmp := 'let:' x := #1 in #1.
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
\ No newline at end of file
......@@ -35,7 +35,15 @@ Inductive expr :=
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| CAS (e0 : expr) (e1 : expr) (e2 : expr)
| FAA (e1 : expr) (e2 : expr).
| FAA (e1 : expr) (e2 : expr)
(* Process *)
| Start (c e : expr)
(* Channels *)
| NewChan
| Send (c e : expr)
| Recv (c : expr).
Definition pexpr := prod loc expr.
Fixpoint to_expr (e : expr) : dist_lang.expr :=
match e with
......@@ -60,8 +68,14 @@ Fixpoint to_expr (e : expr) : dist_lang.expr :=
| Store e1 e2 => dist_lang.Store (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 => dist_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
| FAA e1 e2 => dist_lang.FAA (to_expr e1) (to_expr e2)
| Start c e => dist_lang.Start (to_expr c) (to_expr e)
| NewChan => dist_lang.NewChan
| Send c e => dist_lang.Send (to_expr c) (to_expr e)
| Recv c => dist_lang.Recv (to_expr c)
end.
Definition to_expr'' (p : pexpr) : dist_lang.pexpr := (p.1, to_expr p.2).
Ltac of_expr e :=
lazymatch e with
| dist_lang.Var ?x => constr:(Var x)
......@@ -102,15 +116,17 @@ Ltac of_expr e :=
end
end.
(* Ltac of_expr'' e := constr:(e.1, of_expr e.2). *)
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Val _ _ _ | ClosedExpr _ => true
| Var x => bool_decide (x X)
| Rec f x e => is_closed (f :b: x :b: X) e
| Lit _ => true
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
| Lit _ | NewChan => true
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e | Recv e =>
is_closed X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | Start e1 e2 | Send e1 e2=>
is_closed X e1 && is_closed X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
is_closed X e0 && is_closed X e1 && is_closed X e2
......@@ -172,6 +188,10 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Store e1 e2 => Store (subst x es e1) (subst x es e2)
| CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
| FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
| Start e1 e2 => Start (subst x es e1) (subst x es e2)
| NewChan => NewChan
| Send e1 e2 => Send (subst x es e1) (subst x es e2)
| Recv e => Recv (subst x es e)
end.
Lemma to_expr_subst x er e :
to_expr (subst x er e) = dist_lang.subst x (to_expr er) (to_expr e).
......@@ -191,12 +211,52 @@ Definition is_atomic (e : expr) :=
| Fork _ => true
(* Make "skip" atomic *)
| App (Rec _ _ (Lit _)) (Lit _) => true
| NewChan => true
| Start c _ => bool_decide (is_Some (to_val c))
| Send c e => bool_decide (is_Some (to_val c) is_Some (to_val e))
| Recv c => bool_decide (is_Some (to_val c))
| _ => false
end.
Lemma is_atomic_correct s e : is_atomic e Atomic s (to_expr e).
Definition is_atomic'' (e : pexpr) := is_atomic e.2.
Lemma is_atomic_correct s e : is_atomic'' e Atomic s (to_expr'' e).
Proof.
intros He. apply strongly_atomic_atomic, ectx_language_atomic.
- intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
(* - intros σ e' σ' ef Hstep. simpl in *. revert Hstep. *)
(* destruct e=> //=. *)
(* intros He. apply strongly_atomic_atomic, ectx_language_atomic. *)
- intros σ e' σ' ef Hstep. simpl in *. unfold is_atomic'' in He. apply to_val_val''.
revert Hstep. inversion 1.
+ revert H8. inversion 1;
first(revert H16; destruct e; simpl in *;
destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto;
unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto).
revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
revert H8; destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
revert H8. (* Prove absurdity *) destruct e. destruct e. simpl in *. subst. destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
* revert H8. destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
revert H8. inversion 1. simplify_eq.
revert H10.
repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto;
revert H10;
destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
......
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