-
Notifications
You must be signed in to change notification settings - Fork 0
/
MemoTable.v
58 lines (51 loc) · 2.04 KB
/
MemoTable.v
1
2
3
4
5
6
7
8
9
10
11
12
13
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
Require Import RGref.DSL.DSL.
Require Import Coq.Arith.Arith.
Section MemoTable.
(* Apparently the instances below stick around after the section ends... *)
Variable B : nat -> Set.
Variable f : forall (x:nat), B x.
Parameter safe_f : Safe f.
Existing Instance safe_f.
Parameter safe_B : Safe B.
Existing Instance safe_B.
Definition prefernat {P:nat->Set}(g:forall x:nat, P x)(a:nat) : forall x:nat, P x.
refine(let v := g a in
(fun x => if eq_nat_dec x a then _ else g x)).
subst. exact v.
Defined.
Print prefernat.
Definition obs_equiv {A:Set}{P:A->Set}(f g:forall x, P x)(_ _:heap) :=
forall x, f x = g x.
Lemma obs_eq_refl : forall A P, hreflexive (@obs_equiv A P).
Proof. intros; red. compute. eauto. Qed.
Hint Resolve obs_eq_refl.
Lemma precise_obs_equiv : precise_rel (@obs_equiv nat (fun _ => nat)).
Proof. compute. intuition. Qed.
Hint Resolve precise_obs_equiv.
Instance safe_prefernat : Safe (@prefernat).
(* Instance prior_safe (r:ref{forall x:nat,B x|any}[obs_equiv,obs_equiv]) (n:nat)
: Safe (@prefernat B (@deref _ _ _ _ _ _ (obs_eq_refl _ _) eq_refl r) n). *)
Instance prior_safe (r:ref{forall x:nat,B x|any}[obs_equiv,obs_equiv]) (n:nat)
: ESafe 0 (@prefernat B f n).
repeat solve_applications.
Defined.
Program Definition prioritize {Γ} (r:ref{forall x:nat,B x|any}[obs_equiv,obs_equiv]) (n:nat) : rgref Γ unit Γ :=
[r]:= prefernat (!r) n.
Next Obligation.
repeat solve_applications.
Qed.
Next Obligation.
red. unfold prefernat. intros. induction (eq_nat_dec x n); intuition; eauto.
subst. compute. eauto.
Qed.
(* Doesn't (and shouldn't!) typecheck *)
Program Example should_not_typecheck {Γ} (r:ref{nat|any}[havoc,havoc]) : rgref Γ (ref{nat->nat|any}[havoc,havoc]) Γ :=
Alloc (fun x => !r). (*;
prioritize _ r 0.
(*Print should_not_typecheck.*)
*)
Next Obligation. compute; eauto. Defined.
Next Obligation.
(* Cannot typecheck because (λ x:N. !r) is in fact not safe! *)
Admitted.
End MemoTable.