reflection.v 10.6 KB
Newer Older
1
From stdpp Require Import strings gmap mapset stringmap.
2
From iris_logrel.F_mu_ref_conc Require Export lang subst.
3 4 5
Import lang.

Module R.
6
Inductive expr :=
7
  | Val (v : lang.val) (e : lang.expr) (Hev : to_val e = Some v)
8
  | ClosedExpr (e : lang.expr) `{Closed  e}
9 10 11 12
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
  (* Base Types *)
13
  | Lit (l : literal)
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
  | BinOp (op : binop) (e1 e2 : expr)
  (* If then else *)
  | If (e0 e1 e2 : expr)
  (* Products *)
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
  (* Sums *)
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
  (* Recursive Types *)
  | Fold (e : expr)
  | Unfold (e : expr)
  (* Polymorphic Types *)
  | TLam (e : expr)
  | TApp (e : expr)
  (* Existential types *)
  | Pack (e : expr)
  | Unpack (e : expr) (e' : expr)
  (* Concurrency *)
  | Fork (e : expr)
  (* Reference Types *)
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  (* Compare and swap used for fine-grained concurrency *)
  | CAS (e0 : expr) (e1 : expr) (e2 : expr).

Fixpoint to_expr (e : expr) : lang.expr :=
  match e with
45
  | Val v e _ => e
Dan Frumin's avatar
Dan Frumin committed
46
  | ClosedExpr e => e
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
  | Var x => lang.Var x
  | Rec f x e => lang.Rec f x (to_expr e)
  | App e1 e2 => lang.App (to_expr e1) (to_expr e2)
  | Lit l => lang.Lit l
  | BinOp op e1 e2 => lang.BinOp op (to_expr e1) (to_expr e2)
  | If e0 e1 e2 => lang.If (to_expr e0) (to_expr e1) (to_expr e2)
  | Pair e1 e2 => lang.Pair (to_expr e1) (to_expr e2)
  | Fst e => lang.Fst (to_expr e)
  | Snd e => lang.Snd (to_expr e)
  | InjL e => lang.InjL (to_expr e)
  | InjR e => lang.InjR (to_expr e)
  | Case e0 e1 e2 => lang.Case (to_expr e0) (to_expr e1) (to_expr e2)
  | Fork e => lang.Fork (to_expr e)
  | Alloc e => lang.Alloc (to_expr e)
  | Load e => lang.Load (to_expr e)
  | Store e1 e2 => lang.Store (to_expr e1) (to_expr e2)
  | CAS e0 e1 e2 => lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
  | Fold e => lang.Fold (to_expr e)
  | Unfold e => lang.Unfold (to_expr e)
  | Pack e => lang.Pack (to_expr e)
  | Unpack e e' => lang.Unpack (to_expr e) (to_expr e')
  | TLam e => lang.TLam (to_expr e)
  | TApp e => lang.TApp (to_expr e)
  end.

Ltac of_expr e :=
  lazymatch e with
  | lang.Var ?x => constr:(Var x)
  | lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
  | lang.App ?e1 ?e2 =>
     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2)
  | lang.Lit ?l => constr:(Lit l)
  | lang.BinOp ?op ?e1 ?e2 =>
     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
  | lang.If ?e0 ?e1 ?e2 =>
     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
     constr:(If e0 e1 e2)
  | lang.Pair ?e1 ?e2 =>
     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2)
  | lang.Fst ?e => let e := of_expr e in constr:(Fst e)
  | lang.Snd ?e => let e := of_expr e in constr:(Snd e)
  | lang.InjL ?e => let e := of_expr e in constr:(InjL e)
  | lang.InjR ?e => let e := of_expr e in constr:(InjR e)
  | lang.Case ?e0 ?e1 ?e2 =>
     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
     constr:(Case e0 e1 e2)
  | lang.Fork ?e => let e := of_expr e in constr:(Fork e)
  | lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
  | lang.Load ?e => let e := of_expr e in constr:(Load e)
  | lang.Store ?e1 ?e2 =>
     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
  | lang.CAS ?e0 ?e1 ?e2 =>
     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
     constr:(CAS e0 e1 e2)
  | lang.Fold ?e => let e := of_expr e in constr:(Fold e)
  | lang.Unfold ?e => let e := of_expr e in constr:(Unfold e)
  | lang.Pack ?e => let e := of_expr e in constr:(Pack e)
104
  | lang.Unpack ?e ?e' =>
105 106 107 108
     let e := of_expr e in let e' := of_expr e' in constr:(Unpack e e')
  | lang.TLam ?e => let e := of_expr e in constr:(TLam e)
  | lang.TApp ?e => let e := of_expr e in constr:(TApp e)
  | to_expr ?e => e
109
  | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
110
  | _ =>
Dan Frumin's avatar
Dan Frumin committed
111
    lazymatch goal with
112
    | [H : to_val e = Some ?ev |- _] =>
113
      constr:(Val ev e H)
Dan Frumin's avatar
Dan Frumin committed
114 115
    | [H : Closed  e |- _] => constr:(@ClosedExpr e H)
    | [H : Is_true (is_closed  e) |- _] => constr:(@ClosedExpr e H)
116 117 118
    end
  end.

119
Fixpoint is_closed (X : stringset) (e : expr) : bool :=
120
  match e with
121
  | Val _ _ _ => true
Dan Frumin's avatar
Dan Frumin committed
122
  | ClosedExpr e => true
123 124 125 126 127 128 129
  | Var x => bool_decide (x  X)
  | Lit l => true
  | Rec f x e => is_closed (x :b: f :b: X) e
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | Unpack 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
130 131
  | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e
          | Load e  | Fold e | Unfold e | Pack e
132 133 134
          | TLam e | TApp e => is_closed X e
  end.

135 136
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
137
  | Val _ _ _ => e
Dan Frumin's avatar
Dan Frumin committed
138
  | ClosedExpr _ => e
139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168
  | Var y => if decide (x = y) then es else Var y
  | Rec f y e =>
    Rec f y $ if decide (BNamed x  f  BNamed x  y) then subst x es e else e
  | App e1 e2 => App (subst x es e1) (subst x es e2)
  | TLam e => TLam (subst x es e)
  | TApp e => TApp (subst x es e)
  | Lit l => Lit l
  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
  | Fst e => Fst (subst x es e)
  | Snd e => Snd (subst x es e)
  | Fold e => Fold (subst x es e)
  | Unfold e => Unfold (subst x es e)
  | Pack e => Pack (subst x es e)
  | Unpack e0 e =>
    Unpack (subst x es e0) (subst x es e)
  | InjL e => InjL (subst x es e)
  | InjR e => InjR (subst x es e)
  | Case e0 e1 e2 =>
    Case (subst x es e0)
         (subst x es e1)
         (subst x es e2)
  | Fork e => Fork (subst x es e)
  | Alloc e => Alloc (subst x es e)
  | Load e => Load (subst x es e)
  | 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)
  end.

169
Lemma is_closed_correct X e : is_closed X e  lang.is_closed X (to_expr e).
170
Proof.
171
  revert X.
172
  induction e; cbn; try naive_solver.
173 174
  - intros. rewrite -(of_to_val _ _ Hev). eapply of_val_closed'.
  - intros. eapply is_closed_weaken; eauto. set_solver.
175 176
Qed.

177 178 179 180 181 182
(* 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
183
  | Val v _ _ => Some v
184 185 186 187 188 189
  | 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
Dan Frumin's avatar
Dan Frumin committed
190
  | Lit l => Some (LitV l)
191 192 193 194 195 196 197
  | 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.
198 199 200 201 202 203 204 205 206 207 208 209

Lemma subst_correct x es e :
  lang.subst x (to_expr es) (to_expr e) = to_expr (subst x es e).
Proof.
  induction e; cbn; try (congruence || naive_solver).
  - rewrite -(of_to_val _ _ Hev).
    by rewrite (@Closed_subst_id _ _ _ (of_val_closed v)).
  - by rewrite (@Closed_subst_id _ _ _ H).
  - case_match; eauto.
  - case_match; eauto. congruence.
Qed.

210 211 212 213 214 215 216 217 218
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.
219

220 221 222
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.
223 224
End R.

225
Ltac solve_to_val :=
Dan Frumin's avatar
Dan Frumin committed
226
  rewrite /IntoVal;
227 228 229 230 231 232 233 234 235 236 237 238
  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.
Dan Frumin's avatar
Dan Frumin committed
239
Hint Extern 0 (IntoVal _ _) => solve_to_val : typeclass_instances.
240

Dan Frumin's avatar
Dan Frumin committed
241 242 243 244 245 246 247 248 249 250
(* TODO:
DF: this is also kind of a hack.
Basically, we canno't really solve goals of the form `Closed X e` for an abstract `X`.
`vm_compute` loops on goals like `bool_decide (x  {[x]}  X)`. *)
Ltac pre_solve_closed :=
  lazymatch goal with
  | [ |- Closed ?X ?e ] =>
    apply (Closed_mono e  X); [| apply empty_subseteq]
  end.

251
Ltac solve_closed :=
Dan Frumin's avatar
Dan Frumin committed
252
  pre_solve_closed;
253 254 255 256 257 258 259 260 261
  match goal with
  | [ |- Closed ?X ?e] =>
     let e' := R.of_expr e in change (is_closed X (R.to_expr e'));
     eapply R.is_closed_correct; vm_compute; exact I
  | [ |- Is_true (is_closed ?X ?e)] =>
     let e' := R.of_expr e in change (is_closed X (R.to_expr e'));
     eapply R.is_closed_correct; vm_compute; exact I
  end.
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
262
Hint Extern 0 (Closed _ _) => solve_closed.
263

264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
(* TODO: This is horrible, but it actually works. *)
(*    DF: *)
(*    The issue here is that some lemmas about Rec's depend on the *)
(*    specific assumption that [Closed (x :b: f :b: ) ebody] holds. *)
(*    This duplication leads to confusion and necessitates monstrosities likes this one. *)
Ltac solve_closed2 :=
  lazymatch goal with
  | [ H: Closed ?X (Rec ?f ?x ?e) |- Closed (?x :b: ?f :b: ?X) ?e ] =>
    change (Closed X (Rec f x e)); apply H
  | [ |- Closed (?x :b: ?f :b: ?X) ?e ] =>
    change (Closed X (Rec f x e)); solve_closed
  | [ H: Closed (?x :b: ?f :b: ?X) ?e |- Closed ?X (Rec ?f ?x ?e) ] =>
    change (Closed (x :b: f :b: X) e); apply H
  | _ => solve_closed
  end.
Hint Extern 1 (Closed _ _) => solve_closed2 : typeclass_instances.

281 282 283 284 285 286 287 288 289 290 291 292 293
Ltac simpl_subst :=
  cbn[subst'];
  repeat match goal with
  | |- context [subst ?x ?er ?e] =>
      let er' := R.of_expr er in let e' := R.of_expr e in
      change (subst x er e) with (subst x (R.to_expr er') (R.to_expr e'));
      rewrite (R.subst_correct x); simpl
  end;
  unfold R.to_expr.
Tactic Notation "simpl_subst/=" := simpl; simpl_subst.

(* TODO: the following breaks a lot of shit *)
(* Arguments subst : simpl never. *)
294
Arguments R.to_expr : simpl never.