Fields actually working with a general tie b/t field reads and getf

Author: csgordon

RGref/DSL/Fields.v

@@ -19,10 +19,17 @@ Axiom field_read : forall {T B F Res:Set}{P R G}`{rel_fold T}
                           (r:ref{T|P}[R,G]) (f:F)
                           `{FieldType B F f Res},
                           Res.
-Axiom field_write : forall {Γ}{T F Res:Set}{P R G}
+Check @getF. Check @fold. Check @setF.
+Axiom field_write : forall {Γ}{T F Res:Set}{P R G}{folder:rel_fold T}
                            (r:ref{T|P}[R,G]) (f:F) (e : Res)
-                           `{FieldType T F f Res}
-                           `{forall h v, P v h -> G v (setF v e) h (heap_write r (setF v e) h)},
+                           `{FieldTyping T F}
+                           {ft:FieldType T F f Res}
+                           `{forall h v, 
+                               P v h -> 
+                               (forall Post ft' fte' (pf1:rgfold R G = Post) pf2 x y,
+                                   @field_read T Post F Res P R G folder pf1 pf2 r f x y =
+                                   @getF (@rgfold T folder R G) F ft' f Res fte' (@fold T folder R G v)) ->
+                               G v (@setF T F _ f Res ft v e) h (heap_write r (@setF T F _ f Res ft v e) h)},
                            rgref Γ unit Γ.
 
 Section FieldDemo.
@@ -35,6 +42,7 @@ Section FieldDemo.
   Lemma refl_deltaD : hreflexive deltaD. Proof. red. intros. destruct x. apply incCount. eauto with arith. Qed.
   Hint Resolve refl_deltaD.
 
+  (* I feel like this is reinventing lenses... *)
   Inductive Dfield : Set := Count | Flag.
   Instance dfields : FieldTyping D Dfield.
   Instance dfield_count : FieldType D Dfield Count nat := {
@@ -46,41 +54,18 @@ Section FieldDemo.
     setF := fun v fv => match v with (mkD n b) => (mkD n fv) end
   }.
 
-  Definition getCount (d:D) := match d with (mkD n b) => n end.
-  Definition getFlag (d:D) := match d with (mkD n b) => b end.
-
-(* Print DAccess. (* <-- that is a terrible term due to dependent induction *) *)
   Instance pureD : pure_type D.
   Program Example demo {Γ} (r : ref{D|any}[deltaD,deltaD]) : rgref Γ unit Γ :=
-    @field_write Γ D Dfield nat _ _ _ r Count ((@field_read _ D Dfield _ _ _ _ _ _ _ r Count _ _)+1) _ _ _.
-(*    @field_write Γ D _ _ _ _ _ DAccess r Count (nat2DField ((Count2nat (@field_read _ _ _ _ _ _ _ _ _ _ _ DAccess r (DField2Fin Count) _)) + 1)) _.
+    @field_write Γ D Dfield nat _ _ _ _ r Count ((@field_read _ D Dfield _ _ _ _ _ _ _ r Count _ _)+1) _ _ _.
   Next Obligation.
-    cut (forall f p1 p2 p3, @eq (DFieldTypes f) (@field_read D D _ _ _ _ _ DFieldTypes _ p1 p2 DAccess r f p3)  (@fieldOf D _ DFieldTypes DAccess (@fold D _ deltaD deltaD v) f)).
-    intro Hcomp. rewrite Hcomp with (f := F1).
-    destruct v. compute [nat2DField Count2nat].
-    compute [fieldOf]. unfold DAccess. unfold DAccess_obligation_1. unfold fold.
-    unfold pure_fold. unfold getCount. unfold getFlag. unfold const_id_fold.
-    compute [t_rec t_rect]. (* Now pretty sure I screwed up the def of fieldUpdate *)
-    Check DAccess_obligation_3.
-    compute [DAccess_obligation_3].
-    compute -[fieldUpdate].
-    compute [fieldOf DFieldTypes DAccess DAccess_obligation_1 fold DAccess_obligation_3]. rewrite plus_comm.
-    (* At this point we *should* be done, but the use of dependent induction to work around
-       Coq's pattern matching has introduced some uses of JMeq to deal with *)
-    generalize (@JMeq_eq (t (S (S O))) (@F1 (S O)) (@F1 (S O)) (@JMeq_refl (t (S (S O))) (@F1 (S O)))).
-    intro e. elim e.*)
-
-  Next Obligation. unfold demo_obligation_1. unfold demo_obligation_2.
-    Check @getF.
-    cut (forall P R G pf1 pf2 r f fs fi, 
-           @field_read D D Dfield nat P R G (@pure_fold D pureD) pf1 pf2 r f fs fi = 
-                     @getF D Dfield _ f nat _ v).
-    intros Hfieldstuff.
+    unfold demo_obligation_1. unfold demo_obligation_2.
+(*    Check @getF.
+    cut (forall T B (v:B) F Res P R G folder pf1 pf2 r f fs fi ft ftb, 
+           @field_read T B F Res P R G folder pf1 pf2 r f fs fi = 
+                     @getF B F ft f Res ftb v).
+    intros Hfieldstuff.*)
     destruct v.
-    rewrite Hfieldstuff.
+(*    rewrite Hfieldstuff.*) erewrite H0.
     compute. fold plus. constructor. eauto with arith.
-    (* this should be abstracted to a general hypothesis supplied by
-       the write framework. *)
-    admit.
   Qed.
 End FieldDemo.