OCaml examples

OCaml Program

Checking:
Static Dynamic Hybrid

let not x = if x then false else true

let null xs = match xs with
    [] -> true
  | (h::t) -> false

contract length_aux = {n | n >=0} -> {xs | true} -> {y | y >=0}
let rec length_aux n (xs: int list) = match xs with
    [] -> n
  | a::l -> length_aux (n + 1) l

contract length = {xs | true} -> {y | y >=0}
let length l = length_aux 0 l

contract head = {xs | not (null xs)} -> {r | true} 
let head (xs: int list) = match xs with 
             | (h::t) -> h

contract tail = {xs | not (null xs)} -> {r | true} 
let tail (xs: int list) = match xs with 
             | (h::t) -> t

contract len = {xs | true} -> {n | n >= 0} 
let rec len (xs:int list) = match xs with
    [] -> 0
  | (h::t) -> 1 + len t

contract append = {xs | true} -> {ys | true} 
               -> {rs | len xs + len ys = len rs}
let rec append (xs: int list) (ys: int list) = match xs with
| [] -> ys
| x::l -> x :: append l ys

contract rev_append = {xs | true} -> {ys | true} 
                    -> {zs | len xs + len ys = len zs}
let rec rev_append (l1 : int list) (l2 : int list) =
  match l1 with
    [] -> l2
  | a :: l -> rev_append l (a :: l2)

contract rev = {xs | true} -> {ys | len xs = len ys} 
let rev l = rev_append l []

let rec sum_len (xs: (int list) list) = match xs with
  [] -> 0
| (a::l) -> len a + sum_len l

contract flatten = {xs | true} -> {ys | len ys = sum_len xs}
let rec flatten (xs : (int list) list) = match xs with
    [] -> []
  | l::r -> append l (flatten r)

let concat = flatten

contract map = {f | true} -> {xs | true} -> {ys | len xs = len ys} 
let rec map f (xs: int list) = match xs with
              | [] -> []
              | (h::t) -> f h :: map f t

contract rmap_f = {f | true} -> {xs | true} -> {ys | true} 
                -> {zs | len zs = len xs + len ys} 
let rec rmap_f f (accu : int list) (ys: int list) = match ys with
    | [] -> accu
    | a::l -> rmap_f f (f a :: accu) l

contract rev_map = {f | true} -> {xs | true} -> {ys | len xs = len ys} 
let rev_map f l = rmap_f f [] l

let min x y = if x < y then x else y
let rec for_all (p : int -> bool) (xs : int list) = match xs with
    [] -> true
  | a::l -> p a && for_all p l

contract filter = {p | true} -> {xs | true} -> {zs | for_all p xs}
let rec filter (p : int -> bool)  (xs : int list) = match xs with
| [] -> []
| (a::l) -> let res = filter p l in
            if p a then a::res
               else res

contract min = {x | true} -> {y | true} -> {z | z = x || z = y}
let min (x:int) y = if x < y then x else y

contract len2 = {xs | true} -> {y | y >=0}
let rec len2 (xs : (int * int) list) = match xs with
| [] -> 0
| (a::l) -> 1 + len2 l

contract zip = {xs | true} -> {ys | len ys = len xs} -> {zs | len2 zs = len ys}
let rec zip (l1 : int list) (l2 : int list) = match l1 with
| [] -> begin match l2 with
  | [] -> []
  | (a2::l2) -> []
  end
| (a1::l1) -> begin match l2 with
  | [] -> []
  | (a2::l2) -> (a1, a2) :: zip l1 l2
  end