trying to apply the #31 trick. still see leftovers

au-ts · Jan 10, 2018 · 599519d · 599519d
1 parent e28b542
commit 599519d
Show file tree

Hide file tree

Showing 3 changed files with 41 additions and 14 deletions.
diff --git a/cogent/lib/gum/common/common.cogent b/cogent/lib/gum/common/common.cogent
@@ -16,6 +16,12 @@ type LRR acc brk = (acc, <Iterate ()|Break brk>)
 type R a b = <Success a|Error b>
 type Result a b = R a b
 
+success : all (a, b). a -> R a b
+success a = Success a
+
+error : all (a, b). b -> R a b
+error b = Error b
+
 type RR c a b = (c, <Success a | Error b>)
 
 type ErrCode = U32

diff --git a/cogent/tests/pass_ticket-e31.cogent b/cogent/tests/pass_ticket-e31.cogent
@@ -1,18 +1,39 @@
+type MountState
+
 type Buffer
-type OstoreState = { rbuf : Buffer }
+type UbiVol
+type OstoreState = {
+  next_inum : U32
+, rbuf : Buffer
+, wbuf_eb : U32
+, ubi_vol : UbiVol
+}
 
+type ObjId = U64
 type Obj
 
-type RR c a b = (c, <Success a | Error b>)
+type R a b = <Success a | Error b>
+type RR c a b = (c, R a b)
 
+type BufOffs = U32
 deep_freeObj: Obj -> ()
-deserialise_Obj: () -> Obj
+deserialise_Obj: (Buffer!, BufOffs) -> (Obj, BufOffs)
+read_obj_pages_in_buf: (MountState!, UbiVol!, Buffer, ObjAddr!) -> Buffer
+
+type ObjAddr = #{ ebnum : U32, offs : U32, len : U32, sqnum : U64 }
+index_get_addr : () -> ObjAddr
+
+success : all (a, b). a -> R a b
+success a = Success a
 
-ostore_read: OstoreState -> RR OstoreState Obj ()
-ostore_read ostore_st =
-  let (ostore_st, r) = 
-     let obj = deserialise_Obj ()
-      in (ostore_st, Success obj)
+ostore_read: (MountState!, OstoreState, ObjId) -> RR OstoreState Obj ()
+ostore_read (mount_st, ostore_st, oid) =
+  let addr = index_get_addr ()
+  and (ostore_st, r) = 
+     let ostore_st {rbuf} = ostore_st
+     and rbuf = read_obj_pages_in_buf (mount_st, ostore_st.ubi_vol, rbuf, addr) !ostore_st
+     and (obj, sz) = deserialise_Obj (rbuf, 1) !rbuf
+      in (ostore_st {rbuf}, success obj)
   in r
   | Success obj -> let _ = deep_freeObj obj in (ostore_st, Error)
   | Error -> (ostore_st, Error)

diff --git a/impl/fs/bilby/cogent/src/ostore.cogent b/impl/fs/bilby/cogent/src/ostore.cogent
@@ -867,7 +867,7 @@ ostore_read (ex, mount_st, ostore_st, oid) =
     _cogent_debug "Obj not found in index " ;
     _cogent_debug_u64_hex oid ;
     _cogent_debug "\n" ;
-    ((ex, ostore_st), Error err) 
+    ((ex, ostore_st), error err) 
   | Success addr ->
     let wbuf_eb = ostore_st.wbuf_eb !ostore_st
     -- if we are trying to read an object that is in the current write-buffer
@@ -878,24 +878,24 @@ ostore_read (ex, mount_st, ostore_st, oid) =
       | Error (e, ex) ->
         _cogent_debug "ostore_read: deserialise_Obj_crc from buffer failed\n" ;
         let wbuf = wbuf {bound=mount_st.super.eb_size}
-        in ((ex, ostore_st {wbuf}), Error e)
+        in ((ex, ostore_st {wbuf}), error e)
       | Success (ex, obj, sz) ->
         let wbuf = wbuf {bound=mount_st.super.eb_size}
-        in ((ex, ostore_st {wbuf}), Success obj)
+        in ((ex, ostore_st {wbuf}), success obj)
      else
     -- We need to read the object from medium
        let ostore_st {rbuf} = ostore_st
        and ((ex, rbuf), r) = read_obj_pages_in_buf (ex, mount_st, ostore_st.ubi_vol, rbuf, addr) !ostore_st
        in r
        | Error e ->
          _cogent_debug "ostore_read: read_obj_pages_in_buf failed.\n" ;
-         ((ex, ostore_st {rbuf}), Error e)
+         ((ex, ostore_st {rbuf}), error e)
        | Success () ->
          deserialise_Obj (ex, rbuf, addr.offs) !rbuf
          | Error (e, ex) ->
            _cogent_debug "ostore_read: deserialise_Obj_crc from flash failed.\n" ;
-           ((ex, ostore_st {rbuf}), Error e)
-         | Success (ex, obj, sz) -> ((ex, ostore_st {rbuf}), Success obj)
+           ((ex, ostore_st {rbuf}), error e)
+         | Success (ex, obj, sz) -> ((ex, ostore_st {rbuf}), success obj)
     )
     in r
     | Success obj ->