Commit 2ad7eef7 authored by Hai Dang's avatar Hai Dang
Browse files

remove field

parent e75234b9
......@@ -114,7 +114,7 @@ Fixpoint expr_wf (e: expr) : bool :=
| Free e => expr_wf e
| Deref e T => expr_wf e
| Ref e => expr_wf e
| Field e path => expr_wf e
(* | Field e path => expr_wf e *)
| Retag e kind => expr_wf e
| Let x1 e1 e2 => expr_wf e1 && expr_wf e2
| Case e el => expr_wf e && forallb expr_wf el
......
......@@ -31,7 +31,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
(* | AtomRead e => AtomRead (subst x es e) *)
| Deref e T => Deref (subst x es e) T
| Ref e => Ref (subst x es e)
| Field e path => Field (subst x es e) path
(* | Field e path => Field (subst x es e) path *)
| Retag e kind => Retag (subst x es e) kind
| Let x1 e1 e2 =>
Let x1 (subst x es e1)
......@@ -118,7 +118,7 @@ Inductive ectx_item :=
(* | AtWrRCtx (r : result) *)
| DerefCtx (T: type)
| RefCtx
| FieldCtx (path : list nat)
(* | FieldCtx (path : list nat) *)
| RetagCtx (kind: retag_kind)
| LetCtx (x: binder) (e2: expr)
| CaseCtx (el : list expr).
......@@ -148,7 +148,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
(* | AtWrRCtx v1 => AtomWrite (of_result v1) e *)
| DerefCtx T => Deref e T
| RefCtx => Ref e
| FieldCtx path => Field e path
(* | FieldCtx path => Field e path *)
| RetagCtx kind => Retag e kind
| LetCtx x e2 => Let x e e2
| CaseCtx el => Case e el
......@@ -300,10 +300,10 @@ Inductive pure_expr_step (FNs: fn_env) (h: mem) : expr → event → expr → Pr
| DerefBS l lbor T
(DEFINED: (i: nat), (i < tsize T)%nat l + i dom (gset loc) h) :
pure_expr_step FNs h (Deref #[ScPtr l lbor] T) SilentEvt (Place l lbor T)
| FieldBS l lbor T path off T'
(* | FieldBS l lbor T path off T'
(FIELD: field_access T path = Some (off, T')) :
pure_expr_step FNs h (Field (Place l lbor T) path)
SilentEvt (Place (l + off) lbor T')
SilentEvt (Place (l + off) lbor T') *)
| LetBS x e1 e2 e' :
is_Some (to_result e1)
subst x e1 e2 = e'
......
......@@ -159,7 +159,7 @@ Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
| Proj e1 e2, Proj e1' e2' | Conc e1 e2, Conc e1' e2'
| Write e1 e2, Write e1' e2' (* | AtomWrite e1 e2, AtomWrite e1' e2' *) =>
expr_beq e1 e1' && expr_beq e2 e2'
| Field e path, Field e' path' => expr_beq e e' && bool_decide (path = path')
(* | Field e path, Field e' path' => expr_beq e e' && bool_decide (path = path') *)
(* | CAS e0 e1 e2, CAS e0' e1' e2' =>
expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2' *)
(* | Fork e, Fork e' => expr_beq e e' *)
......@@ -172,8 +172,8 @@ Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
Lemma expr_beq_correct (e1 e2 : expr) : expr_beq e1 e2 e1 = e2.
Proof.
revert e1 e2; fix FIX 1;
destruct e1 as [| |? el1| | | | | | | | | | | | | | | |? el1],
e2 as [| |? el2| | | | | | | | | | | | | | | |? el2];
destruct e1 as [| |? el1| | | | | | | | | | (* | *) | | | | |? el1],
e2 as [| |? el2| | | | | | | | | | (* | *) | | | | |? el2];
simpl; try done;
rewrite ?andb_True ?bool_decide_spec ?FIX;
try (split; intro; [destruct_and?|split_and?]; congruence).
......@@ -216,10 +216,10 @@ Proof.
| Alloc T => GenNode 12 [GenLeaf $ inl $ inr $ inr $ inl T]
| Deref e T => GenNode 13 [GenLeaf $ inl $ inr $ inr $ inr T; go e]
| Ref e => GenNode 14 [go e]
| Field e path => GenNode 15 [GenLeaf $ inr $ inl $ inl (* $ inl *) path; go e]
| Retag e kind => GenNode 16 [GenLeaf $ inr $ inl (* $ inr *) $ inr kind; go e]
| Let x e1 e2 => GenNode 17 [GenLeaf $ inr $ inr x; go e1; go e2]
| Case e el => GenNode 18 (go e :: (go <$> el))
(* | Field e path => GenNode 15 [GenLeaf $ inr $ inl $ inl (* $ inl *) path; go e] *)
| Retag e kind => GenNode 15 [GenLeaf $ inr $ inl (* $ inr $ inr *) kind; go e]
| Let x e1 e2 => GenNode 16 [GenLeaf $ inr $ inr x; go e1; go e2]
| Case e el => GenNode 17 (go e :: (go <$> el))
(* | Fork e => GenNode 23 [go e]
| SysCall id => GenNode 24 [GenLeaf $ inr $ inr id] *)
end)
......@@ -244,11 +244,11 @@ Proof.
| GenNode 12 [GenLeaf (inl (inr (inr (inl T))))] => Alloc T
| GenNode 13 [GenLeaf (inl (inr (inr (inr T)))); e] => Deref (go e) T
| GenNode 14 [e] => Ref (go e)
| GenNode 15 [GenLeaf (inr (inl (inl (* (inl *) path(* ) *)))); e] => Field (go e) path
| GenNode 16 [GenLeaf (inr (inl (* (inr *) (inr kind)(* ) *))); e] =>
(* | GenNode 15 [GenLeaf (inr (inl (inl (* (inl *) path(* ) *)))); e] => Field (go e) path *)
| GenNode 15 [GenLeaf (inr (inl (* (inr (inr *) kind (* ) ) *))); e] =>
Retag (go e) kind
| GenNode 17 [GenLeaf (inr (inr x)); e1; e2] => Let x (go e1) (go e2)
| GenNode 18 (e :: el) => Case (go e) (go <$> el)
| GenNode 16 [GenLeaf (inr (inr x)); e1; e2] => Let x (go e1) (go e2)
| GenNode 17 (e :: el) => Case (go e) (go <$> el)
(* | GenNode 23 [e] => Fork (go e)
| GenNode 24 [GenLeaf (inr (inr id))] => SysCall id *)
| _ => (#[])%E
......@@ -317,8 +317,8 @@ Lemma fill_item_no_result_inj Ki1 Ki2 e1 e2 :
to_result e1 = None to_result e2 = None
fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2.
Proof.
destruct Ki1 as [|v1 vl1 el1| | | | | | | | | | | | | | | | |],
Ki2 as [|v2 vl2 el2| | | | | | | | | | | | | | | | |];
destruct Ki1 as [|v1 vl1 el1| | | | | | | | | | | (* | *) | | | | |],
Ki2 as [|v2 vl2 el2| | | | | | | | | | | (* | *) | | | | |];
intros He1 He2 EQ; try discriminate; simplify_eq/=;
repeat match goal with
| H : to_result (of_result _) = None |- _ => by rewrite to_of_result in H
......
......@@ -165,9 +165,9 @@ Inductive expr :=
presenting the location that `e` points to.
The location has type `T`. *)
| Ref (e: expr) (* Turn a place `e` into a pointer value. *)
| Field (e: expr) (path: list nat)(* Create a place that points to a component
(* | Field (e: expr) (path: list nat)(* Create a place that points to a component
of the place `e`. `path` defines the path
through the type. *)
through the type. *) *)
(* mem op *)
| Copy (e : expr) (* Read from the place `e` *)
| Write (e1 e2: expr) (* Write the value `e2` to the place `e1` *)
......@@ -201,7 +201,7 @@ Arguments Proj _%E _%E.
Arguments Conc _%E _%E.
Arguments Deref _%E _%T.
Arguments Ref _%E.
Arguments Field _%E _.
(* Arguments Field _%E _. *)
Arguments Copy _%E.
Arguments Write _%E _%E.
Arguments Alloc _%T.
......@@ -225,7 +225,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
| Let x e1 e2 => is_closed X e1 && is_closed (x :b: X) e2
| Case e el | Call e el (* | App e el *)
=> is_closed X e && forallb (is_closed X) el
| Copy e | Retag e _ | Deref e _ | Ref e | Field e _
| Copy e | Retag e _ | Deref e _ | Ref e (* | Field e _ *)
| Free e | InitCall e | EndCall e (* | AtomRead e | Fork e *)
=> is_closed X e
(* | CAS e0 e1 e2 => is_closed X e0 && is_closed X e1 && is_closed X e2 *)
......
Supports Markdown
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