module DijkstraTick
let tick (a: Type) = int -> M (a * int)
val return_tick: a:Type -> x:a -> tick a
let return_tick a x = fun _ -> x, 0
val bind_tick: a:Type -> b:Type -> f:tick a -> g:(a -> tick b) -> tick b
let bind_tick a b f g = fun t0 ->
let x, t1 = f t0 in
g x (t1 + 1)
let get (_:unit): tick int =
fun x -> x, x
let put (x: int): tick unit =
fun _ -> (), x
total reifiable reflectable new_effect {
TICK : a:Type -> Effect
with repr = tick
; bind = bind_tick
; return = return_tick
; get = get
; put = put
}
effect Tick (a:Type) (req:TICK?.pre) (ens: int -> a -> int -> GTot Type0) =
TICK a (fun (t0:int) (p:TICK?.post a) -> req t0 /\
(forall (r:a) (t1:int). (req t0 /\ ens t0 r t1) ==> p (r, t1)))
val length: list 'a -> Tot nat
let rec length l = match l with
| [] -> 0
| _ :: tl -> 1 + length tl
val append : xs:list 'a -> ys:list 'a -> zs:list 'a{length zs = length xs + length ys}
let rec append xs ys =
match xs with
| [] -> ys
| x :: xs -> x :: (append xs ys)
val tappend : xs:list 'a -> ys:list 'a ->
Tick (list 'a)
(fun _ -> True)
(fun t0 _ t1 -> t1 = t0 + length xs)
let rec tappend xs ys =
match xs with
| [] -> ys
| x :: xs -> x :: (tappend xs ys)