From 599519dd6a9db390c754d55c1f72afde1a0aee9e Mon Sep 17 00:00:00 2001 From: Zilin Chen Date: Sun, 20 Nov 2016 20:56:05 +1100 Subject: [PATCH] trying to apply the #31 trick. still see leftovers --- cogent/lib/gum/common/common.cogent | 6 +++++ cogent/tests/pass_ticket-e31.cogent | 37 ++++++++++++++++++++------ impl/fs/bilby/cogent/src/ostore.cogent | 12 ++++----- 3 files changed, 41 insertions(+), 14 deletions(-) diff --git a/cogent/lib/gum/common/common.cogent b/cogent/lib/gum/common/common.cogent index b63113442..80eb96867 100644 --- a/cogent/lib/gum/common/common.cogent +++ b/cogent/lib/gum/common/common.cogent @@ -16,6 +16,12 @@ type LRR acc brk = (acc, ) type R a 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, ) type ErrCode = U32 diff --git a/cogent/tests/pass_ticket-e31.cogent b/cogent/tests/pass_ticket-e31.cogent index 7c0a9f9e3..f39d4e1d6 100644 --- 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, ) +type R a 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 index ea1644a05..35917d099 100644 --- 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,10 +878,10 @@ 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 @@ -889,13 +889,13 @@ ostore_read (ex, mount_st, ostore_st, oid) = 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 ->