Commit 1769a63f authored by Dan Frumin's avatar Dan Frumin
Browse files

Computing `to_val e` in the reified syntax

parent 8d08daca
......@@ -189,8 +189,59 @@ Proof.
- case_match; eauto. congruence.
Qed.
(* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
constructors are only generated for closed expressions of which we know nothing
about apart from being closed. Notice that the reverse implication of
[to_val_Some] thus does not hold. *)
Fixpoint to_val (e : expr) : option val :=
match e with
| Val v => Some v
| Rec f x e =>
if decide (is_closed (x :b: f :b: ) e) is left H
then Some (@RecV f x (to_expr e) (is_closed_correct _ _ H)) else None
| TLam e =>
if decide (is_closed e) is left H
then Some (@TLamV (to_expr e) (is_closed_correct _ _ H)) else None
| Lit Unit => Some UnitV
| Lit (Nat n) => Some (NatV n)
| Lit (Bool b) => Some (BoolV b)
| Loc l => Some (LocV l)
| Pair e1 e2 => v1 to_val e1; v2 to_val e2; Some (PairV v1 v2)
| InjL e => InjLV <$> to_val e
| InjR e => InjRV <$> to_val e
| Pack e => v to_val e; Some (PackV v)
| Fold e => v to_val e; Some (FoldV v)
| _ => None
end.
Lemma to_val_Some e v :
to_val e = Some v lang.to_val (to_expr e) = Some v.
Proof.
revert v. induction e; intros; simplify_option_eq; rewrite ?to_of_val; auto.
- do 2 f_equal. apply proof_irrel.
- exfalso. unfold Closed in *; eauto using is_closed_correct.
- do 2 f_equal. apply proof_irrel.
- exfalso. unfold Closed in *; eauto using is_closed_correct.
Qed.
Lemma to_val_is_Some e :
is_Some (to_val e) is_Some (lang.to_val (to_expr e)).
Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
End R.
Ltac solve_to_val :=
try match goal with
| |- context E [language.to_val ?e] =>
let X := context E [to_val e] in change X
end;
match goal with
| |- to_val ?e = Some ?v =>
let e' := R.of_expr e in change (to_val (R.to_expr e') = Some v);
apply R.to_val_Some; simpl; unfold R.to_expr; unlock; reflexivity
| |- is_Some (to_val ?e) =>
let e' := R.of_expr e in change (is_Some (to_val (R.to_expr e')));
apply R.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
end.
Ltac solve_closed :=
match goal with
| [ |- Closed ?X ?e] =>
......
......@@ -190,7 +190,7 @@ Tactic Notation "rel_alloc_l" "under" constr(N) "as" constr(nam) constr(nam_cl)
|iAssumptionCore || fail "rel_alloc_l: cannot find inv " N " ?"
|try fast_done (* E2 = E1 \ N *)
|tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
|try fast_done (* to_val e' = Some v *)
|solve_to_val (* to_val e' = Some v *)
|try fast_done (* nam fresh *)
|try fast_done (* nam_cl fresh *)
|eauto (* nam =/= nam_cl *)
......@@ -214,7 +214,7 @@ Tactic Notation "rel_alloc_l" "as" ident(l) constr(H) :=
iStartProof;
eapply (tac_rel_alloc_l_simp);
[tac_bind_helper (* e = fill K' .. *)
|try fast_done (* to_val e' = Some v *)
|solve_to_val (* to_val e' = Some v *)
|iIntros (l) H (* new goal *)].
......@@ -313,7 +313,7 @@ Tactic Notation "rel_store_l" "under" constr(N) "as" constr(nam) constr(nam_cl)
|iAssumptionCore || fail "rel_store_l: cannot find inv " N " ?"
|try fast_done (* E2 = E1 \ N *)
|tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
|try fast_done (* to_val e' = Some v *)
|solve_to_val (* to_val e' = Some v *)
|try fast_done (* nam fresh *)
|try fast_done (* nam_cl fresh *)
|eauto (* nam =/= nam_cl *)
......@@ -343,7 +343,7 @@ Tactic Notation "rel_store_l" :=
iStartProof;
eapply (tac_rel_store_l_simp);
[tac_bind_helper (* e = fill K' .. *)
|try fast_done (* to_val e' = Some v' *)
|solve_to_val (* to_val e' = Some v' *)
|iAssumptionCore || fail "rel_store_l: cannot find '? ↦ᵢ ?'"
|env_cbv; reflexivity || fail "rel_store_l: this should not happen"
| (* new goal *)].
......@@ -401,8 +401,8 @@ Tactic Notation "rel_cas_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :=
|iAssumptionCore || fail "rel_store_l: cannot find inv " N " ?"
|try fast_done (* E2 = E1 \ N *)
|tac_bind_helper (* e = fill K' ... *)
|try fast_done (* to_val e1 = Some .. *)
|try fast_done (* to_val e2 = Some .. *)
|solve_to_val (* to_val e1 = Some .. *)
|solve_to_val (* to_val e2 = Some .. *)
|try fast_done (* nam fresh *)
|try fast_done (* nam_cl fresh *)
|eauto (* nam =/= nam_cl *)
......@@ -455,7 +455,7 @@ Tactic Notation "rel_store_r" :=
eapply (tac_rel_store_r);
[solve_ndisj || fail "rel_store_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
|try fast_done (* to_val e' = Some v *)
|solve_to_val (* to_val e' = Some v *)
|iAssumptionCore || fail "rel_store_l: cannot find ? ↦ₛ ?"
|env_cbv; reflexivity || fail "rel_store_r: this should not happen"
|(* new goal *)].
......@@ -477,7 +477,7 @@ Tactic Notation "rel_alloc_r" "as" ident(l) constr(H) :=
eapply (tac_rel_alloc_r);
[solve_ndisj || fail "rel_alloc_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_alloc_r: cannot find 'alloc'"
|try fast_done (* to_val t' = Some v' *)
|solve_to_val (* to_val t' = Some v' *)
|simpl; iIntros (l) H (* new goal *)].
Tactic Notation "rel_alloc_r" :=
......@@ -538,8 +538,8 @@ Tactic Notation "rel_cas_fail_r" :=
eapply (tac_rel_cas_fail_r);
[solve_ndisj || fail "rel_cas_fail_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_cas_fail_r: cannot find 'CAS ..'"
|try fast_done
|try fast_done
|solve_to_val
|solve_to_val
|iAssumptionCore || fail "rel_cas_fail_l: cannot find ? ↦ₛ ?"
|try fast_done (* v v1 *)
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
......@@ -572,8 +572,8 @@ Tactic Notation "rel_cas_suc_r" :=
eapply (tac_rel_cas_suc_r);
[solve_ndisj || fail "rel_cas_suc_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_cas_suc_r: cannot find 'CAS ..'"
|try fast_done
|try fast_done
|solve_to_val
|solve_to_val
|iAssumptionCore || fail "rel_cas_suc_l: cannot find ? ↦ₛ ?"
|try fast_done (* v = v1 *)
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
......@@ -607,7 +607,7 @@ Tactic Notation "rel_rec_r" :=
|tac_bind_helper (* e = fill K' _ *)
|solve_of_val_unlock
|try solve_closed
|fast_done (* to_val e' = Some v *)
|solve_to_val (* to_val e' = Some v *)
|try fast_done (* eres = subst ... *)
|try simpl_subst/= (* new goal *)]
end)
......@@ -637,8 +637,8 @@ Tactic Notation "rel_fst_r" :=
eapply (tac_rel_fst_r);
[solve_ndisj || fail "rel_fst_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K' _ *)
|try fast_done (* to_val e1 = Some .. *)
|try fast_done (* to_val e2 = Some .. *)
|solve_to_val (* to_val e1 = Some .. *)
|solve_to_val (* to_val e2 = Some .. *)
|simpl (* new goal *)].
Lemma tac_rel_snd_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e1 e2 v1 v2 t τ :
......@@ -662,8 +662,8 @@ Tactic Notation "rel_snd_r" :=
eapply (tac_rel_snd_r);
[solve_ndisj || fail "rel_snd_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K' _ *)
|try fast_done (* to_val e1 = Some .. *)
|try fast_done (* to_val e2 = Some .. *)
|solve_to_val (* to_val e1 = Some .. *)
|solve_to_val (* to_val e2 = Some .. *)
|simpl (* new goal *)].
Lemma tac_rel_tlam_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e' t τ :
......@@ -703,9 +703,11 @@ Tactic Notation "rel_fold_r" :=
eapply (tac_rel_fold_r);
[solve_ndisj || fail "rel_fold_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_fold_r: cannot find 'Unfold (Fold e)'"
|try fast_done (* to_val e' = Some .. *)
|solve_to_val (* to_val e' = Some .. *)
|simpl (* new goal *)].
Tactic Notation "rel_unfold_r" := rel_fold_r.
Lemma tac_rel_case_inl_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e0 e1 e2 v t τ :
nclose specN E1
e = fill K' (Case (InjL e0) e1 e2)
......@@ -727,7 +729,7 @@ Tactic Notation "rel_case_inl_r" :=
|tac_bind_helper || fail "rel_case_inl_r: cannot find 'match InjL e with ..'"
|solve_closed
|solve_closed
|try fast_done (* to_val e0 = Some .. *)
|solve_to_val (* to_val e0 = Some .. *)
|simpl (* new goal *)].
Lemma tac_rel_case_inr_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e0 e1 e2 v t τ :
......@@ -751,7 +753,7 @@ Tactic Notation "rel_case_inr_r" :=
|tac_bind_helper || fail "rel_case_inr_r: cannot find 'match InjR e with ..'"
|solve_closed
|solve_closed
|try fast_done (* to_val e0 = Some .. *)
|solve_to_val (* to_val e0 = Some .. *)
|simpl (* new goal *)].
Tactic Notation "rel_case_r" := rel_case_inl_r || rel_case_inr_r.
......@@ -848,7 +850,7 @@ Tactic Notation "rel_op_r" :=
Tactic Notation "rel_vals" :=
iStartProof;
iApply bin_log_related_val; [ try fast_done | try fast_done | ];
iApply bin_log_related_val; [ try solve_to_val | try solve_to_val | ];
let d := fresh "Δ" in
iIntros (d); simpl.
......
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