timeline.fst

module Timeline


type timestamp = nat
type timespan = x:nat{x>0}
type count = nat

type bucket 'a = {
    time: timestamp;
    content: 'a;
}
type timeline 'a = {
    buckets: list (bucket 'a);
    timespan: timespan;
}

val create : timespan -> Tot (timeline 'a)
let create timespan =
    {
        buckets = [];
        timespan = timespan;
    }

val round : timestamp -> timespan -> Tot timestamp
let round t span = t - t % span

let assert_round1 = assert (forall y. round 0 y = 0)


val modify : timeline 'a -> timestamp -> (option 'a -> Tot 'a) -> Tot (timeline 'a)
let modify timeline current_time f =
    let new_buckets = match timeline.buckets with
        | [] ->
            [{ time = current_time; content = f None; }]
        | last :: remaining ->
            if round last.time timeline.timespan = round current_time timeline.timespan then
                { last with content = f (Some last.content); } :: remaining
            else
                { time = current_time; content = f None; } :: last :: remaining
    in
    {
        timeline with
        buckets = new_buckets;
    }


(* should be inner function of inc, blocked by https://github.com/FStarLang/FStar/issues/342
*)
val do_inc: option count -> Tot count
let do_inc x = match x with
    | None -> 1
    | Some x -> x + 1


val inc : timeline count -> timestamp -> Tot (timeline count)
let inc timeline current_time =
    modify timeline current_time do_inc

val fold_left : ('a -> 'b -> Tot 'a) -> 'a -> timeline 'b -> Tot 'a
let fold_left f init timeline = List.fold_leftT (fun a b -> f a b.content) init timeline.buckets

val remove_old : timeline 'a -> timestamp -> Tot (timeline 'a)
let remove_old timeline before =
    let f b = b.time >= before in
    {
        timeline with
        buckets = List.filterT f timeline.buckets;
    }