Skip to content

Commit

Permalink
trying to apply the #31 trick. still see leftovers
Browse files Browse the repository at this point in the history
  • Loading branch information
Zilin Chen authored and Zilin Chen committed Mar 6, 2018
1 parent 54327c5 commit 11881a3
Show file tree
Hide file tree
Showing 3 changed files with 41 additions and 14 deletions.
6 changes: 6 additions & 0 deletions cogent/lib/gum/common/common.cogent
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
37 changes: 29 additions & 8 deletions cogent/tests/pass_ticket-e31.cogent
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
12 changes: 6 additions & 6 deletions impl/fs/bilby/cogent/src/ostore.cogent
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 ->
Expand Down

0 comments on commit 11881a3

Please sign in to comment.