OCaml driver: added stack.Stack and queue.Queue

parent b9fdc864
......@@ -134,6 +134,37 @@ module ref.Ref
syntax val (:=) "Pervasives.(:=)"
end
module stack.Stack
syntax type t "(%1 Stack.t)"
syntax val create "Stack.create"
syntax val push "Stack.push"
syntax exception Empty "Stack.Empty"
syntax val pop "Stack.pop"
syntax val top "Stack.top"
syntax val safe_pop "Stack.pop"
syntax val safe_top "Stack.top"
syntax val clear "Stack.clear"
syntax val copy "Stack.copy"
syntax val is_empty "Stack.is_empty"
syntax val length "Why3__IntAux.stack_length"
end
module queue.Queue
syntax type t "(%1 Queue.t)"
syntax val create "Queue.create"
syntax val push "Queue.push"
syntax exception Empty "Queue.Empty"
syntax val pop "Queue.pop"
syntax val peek "Queue.peek"
syntax val safe_pop "Queue.pop"
syntax val safe_peek "Queue.peek"
syntax val clear "Queue.clear"
syntax val copy "Queue.copy"
syntax val is_empty "Queue.is_empty"
syntax val length "Why3__IntAux.queue_length"
syntax val transfer "Queue.transfer"
end
module array.Array
syntax type array "(%1 Why3__Array.t)"
......
open Why3__BigInt
let rec fact n = if le n one then one else mul n (fact (pred n))
let rec fact n =
if le n one then one else mul n (fact (pred n))
let fib n =
let n = to_int n in
......@@ -21,3 +22,8 @@ let rec for_loop_downto x1 x2 body =
for_loop_downto (pred x1) x2 body
end
let stack_length s =
of_int (Stack.length s)
let queue_length s =
of_int (Queue.length s)
......@@ -48,5 +48,10 @@ module Queue
val length (q: t 'a) : int
ensures { result = L.length q.elts }
val transfer (q1 q2: t 'a) : unit
writes { q1, q2 }
ensures { q1.elts = Nil }
ensures { q2.elts = old q2.elts ++ old q1.elts }
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment