/Users/q9_user

open Crdts module BankAccount_Types = struct type account = {id:Uuid.t; name:string; mutable bal:CRInt.t} type accounts_table = account CRTable.t type ba_db = {accounts_table: accounts_table} end open BankAccount_Types module Account(S:sig val t: accounts_table end) = struct open S let get_balance (acc_id:Uuid.t) = CRTable.find (fun {bal} -> CRInt.get bal) (fun {id} -> id = acc_id) t let deposit (acc_id:Uuid.t) amt = CRTable.update (fun {bal} -> CRInt.add amt bal) (fun {id} -> id = acc_id) t let withdraw (acc_id:Uuid.t) amt = if get_balance acc_id >= amt then begin CRTable.update (fun {bal} -> CRInt.add (0-amt) bal) (fun {id} -> id = acc_id) t; true end else false let inv_non_neg_bal (acc_id:Uuid.t) = let bal = get_balance acc_id in bal >= 0 end
module BA = struct type id = Uuid.t type eff = Deposit of {amt:int} | Withdraw of {amt:int} | GetBalance end module BA_table = struct include Store_interface.Make(BA) end let compute_bal eff = match eff with | Some e -> (match e with | BA.Withdraw {amt=a} -> 0-a | BA.Deposit {amt=a} -> a | _ -> 0) | None -> 0 let add_bals b acc = b + acc let get_balance acc_id = let ctxt = BA_table.get acc_id (BA.GetBalance) in let bals = List.map compute_bal ctxt in let bal = List.fold_right add_bals bals 0 in bal let do_withdraw acc_id a = let cur_bal = get_balance acc_id in if (cur_bal >= a) then (BA_table.append acc_id (BA.Withdraw {amt=a}); true) else false let do_deposit acc_id a = BA_table.append acc_id (BA.Deposit{amt=a}) let inv_non_neg_bal acc_id' = let bal = get_balance acc_id' in bal >= 0
open Crdts module Microblog_Types = struct type user = {id:Uuid.t; name:string; mutable followers:Uuid.t CRSet.t} type users_table = user CRTable.t type tweet = {id:Uuid.t; author_id: Uuid.t; content: string CRSet.t} type tweets_table = tweet CRTable.t type line_item = {id:Uuid.t; tweet_id:Uuid.t} type userline_table = line_item CRTable.t type timeline_table = line_item CRTable.t type mb_db = {users_table:users_table; tweets_table: tweets_table; userline_table: userline_table; timeline_table: timeline_table} end open Microblog_Types module User(S:sig val t: users_table end) = struct open S let add_follower (user_id:Uuid.t) (follower_id: Uuid.t) = CRTable.update (fun {followers} -> CRSet.add follower_id followers) (fun {id} -> id=user_id) t let remove_follower (user_id:Uuid.t) (follower_id: Uuid.t) = CRTable.update (fun {followers} -> CRSet.remove follower_id followers) (fun {id} -> id=user_id) t let get_followers (user_id:Uuid.t) : Uuid.t list = CRTable.find (fun {followers} -> CRSet.get followers) (fun {id} -> id = user_id) t end module Userline(S:sig val t: userline_table end) = struct open S let add (user_id:Uuid.t) (tweet_id:Uuid.t) = CRTable.insert {id=user_id; tweet_id=tweet_id} t let get (user_id:Uuid.t) = CRTable.find (fun {tweet_id} -> tweet_id) (fun {id} -> id = user_id) t end module Timeline(S:sig val t: timeline_table end) = struct open S let add (user_id:Uuid.t) (tweet_id:Uuid.t) = CRTable.insert {id=user_id; tweet_id=tweet_id} t let get (user_id:Uuid.t) = CRTable.find (fun {tweet_id} -> tweet_id) (fun {id} -> id = user_id) t end module Tweet(S:sig val t: tweets_table end) = struct open S let add tweet_id author_id content = CRTable.insert {id=tweet_id; author_id=author_id; content=CRSet.singleton content} t let get tweet_id = CRTable.find (fun {content} -> CRSet.get content) (fun {id} -> id = tweet_id) t end module MicroblogApp(S:sig val db: mb_db end) = struct open S module User = User(struct let t = db.users_table end) module Userline = Userline(struct let t = db.userline_table end) module Timeline = Timeline(struct let t = db.userline_table end) module Tweet = Tweet(struct let t = db.tweets_table end) let do_new_tweet (uid:Uuid.t) (str:string) = let tweet_id = Uuid.create () in let fols = User.get_followers uid in begin Tweet.add tweet_id uid str; Userline.add uid tweet_id; List.iter (fun fid -> Timeline.add fid tweet_id) fols; end let inv_referential_integrity uid' = let ul_tweet_ids = Userline.get uid' in let exists_in_tweet_table tid = match Tweet.get tid with | tweet::_ -> true | _ -> false in List.for_all (exists_in_tweet_table) ul_tweet_ids end
module User = struct type id = Uuid.t type eff = Add of {username: string; pwd: string} | AddFollower of {follower_id: id; timestamp: int} | RemFollower of {follower_id: id;timestamp: int} | GetFollowers end module User_table = struct include Store_interface.Make(User) end module UserName = struct type id = string type eff = Add of {user_id: User.id} | GetId end module UserName_table = struct include Store_interface.Make(UserName) end module Tweet = struct type id = Uuid.t type eff = New of {author_id:User.id; content:string} | Get end module Tweet_table = struct include Store_interface.Make(Tweet) end module Timeline = struct type id = User.id type eff = NewTweet of {tweet_id:Tweet.id} | Get end module Timeline_table = struct include Store_interface.Make(Timeline) end module Userline = struct type id = User.id type eff = NewTweet of {tweet_id:Tweet.id} | Get end module Userline_table = struct include Store_interface.Make(Userline) end let rec first f b l = match l with | [] -> b | x::xs -> match x with | Some y -> if f y then y else first f b xs | None -> first f b xs let is_gte ts tsop' = match tsop' with | Some ts' -> ts' <= ts | None -> true let is_max_in (ts_list : int option list) (ts:int) = List.forall ts_list (is_gte ts) let rec max_ts (ts_list: int option list) : int= first (is_max_in ts_list) (0-1) ts_list let if_af_get_ts (fid:User.id) (eff: User.eff option) = match eff with | Some x -> (match x with | User.AddFollower {follower_id=fid'; timestamp=ts} -> if fid'=fid then Some ts else None | _ -> None) | None -> None let if_rf_get_ts (fid:User.id) (eff: User.eff option) = match eff with | Some x -> (match x with | User.RemFollower {follower_id=fid'; timestamp=ts} -> if fid'=fid then Some ts else None | _ -> None) | None -> None let is_follower fid ctxt = let af_ts = List.map (if_af_get_ts fid) ctxt in let rf_ts = List.map (if_rf_get_ts fid) ctxt in let max_af_ts = max_ts af_ts in let max_rf_ts = max_ts rf_ts in max_af_ts >= max_rf_ts let get_fid ctxt' eff = match eff with | Some x -> (match x with | User.AddFollower {follower_id=fid; timestamp=ts} -> if (is_follower fid ctxt') then Some fid else None | _ -> None) | _ -> None let new_tweet tweet_id' fidop = match fidop with | Some fid -> Timeline_table.append fid (Timeline.NewTweet {tweet_id=tweet_id'}) | None -> () let do_new_tweet (uid:Uuid.t) (str:string) = let ctxt = User_table.get uid (User.GetFollowers) in let fids = List.map (get_fid ctxt) ctxt in let tweet_id = Uuid.create() in begin Tweet_table.append tweet_id (Tweet.New {author_id=uid; content=str}); Userline_table.append uid (Userline.NewTweet {tweet_id=tweet_id}); List.iter (new_tweet tweet_id) fids; end let exists_tweet e' = match e' with | Some y -> (match y with | (Tweet.New _) -> true | _ -> false) | _ -> false let exists_in_tweet_table e = match e with | Some x -> (match x with | Userline.NewTweet {tweet_id=tid} -> List.exists (Tweet_table.get tid Tweet.Get) exists_tweet | _ -> false) | _ -> true let inv_referential_integrity uid' = List.forall (Userline_table.get uid' (Userline.Get)) exists_in_tweet_table