add examples of type annotations

.gitignore

@@ -11,3 +11,5 @@ _build
 TODO
 
 /_snapshots/
+
+!input/annot/*.annot

input/annot/array_init.annot

@@ -0,0 +1,6 @@
+%TYPE
+INIT :
+  i:int ->
+  n:int ->
+  (j:int -> ((v:int -> *[j<0 \/ i<=j \/ v=1]) -> *)) ->
+  ((j:int -> (v:int -> *[j<0 \/ n<=j \/ v=1]) -> *) -> *) -> *

input/annot/array_init.ml

@@ -0,0 +1,11 @@
+let mk_array n i = if 0<=i && i<n then 0 else -1
+let update i a x j = if j=i then x else a(j)
+let rec init i n a =
+  if i>=n then a
+  else init (i+1) n (update i a 1)
+
+let main n i =
+  let x = init 0 n (mk_array n) in
+   if 0<=i && i<n then
+    assert (x i >=1) (* check that the array has been initialized *)
+  else ()

input/annot/kmp.loop.annot

@@ -0,0 +1,12 @@
+%TYPE
+
+LOOP:
+  (plen: int ->
+  (slen: int ->
+  ((i: int -> ((int -> *) -> *[(0 <= i /\ i < plen)])) ->
+  ((i: int -> ((v: int -> *[(0 <= v + 1 /\ v + 1 < plen)]) -> *[(0 <= i /\ i < plen)])) ->
+  ((i: int -> ((int -> *) -> *[(0 <= i /\ i < slen)])) ->
+  (s: int ->
+  (p: int ->
+  ((int -> *) ->
+  *[0<plen /\ 0<slen /\ 0<=p /\ 0<=s]))))))))

input/annot/kmp.loopShift.annot

@@ -0,0 +1,11 @@
+%TYPE
+
+LOOPSHIFT :
+  (plen: int ->
+  (slen: int ->
+  ((i: int -> ((int -> *) -> *[0 <= i /\ i < plen])) ->
+  (i: int ->
+  (j: int ->
+  ((ain_i: int -> ((ain_v: int -> *[(-1<=ain_v /\ ain_v<=ain_i - 1)]) -> *[(0<=ain_i /\ ain_i<plen)])) ->
+  (((aout_i: int -> ((aout_v: int -> *[(-1<=aout_v /\ aout_v<=aout_i - 1)]) -> *[(0<=aout_i /\ aout_i<plen)])) -> *) ->
+  *[0<plen /\ -1<=i /\ i<=plen - 2 /\ i + 1<=j /\ j<=plen])))))))

input/annot/kmp.ml

@@ -0,0 +1,39 @@
+
+let make_array n s i = assert (0 <= i && i < n); s
+let update i n a x = a i; let a j = if i=j then x else a j in a
+
+let kmpMatch slen str plen pat =
+  let shiftArray0 = make_array plen (-1) in
+
+  let rec loopShift i j shiftArray1 =
+    if j = plen then shiftArray1 else
+      if not (pat j = pat (i+1)) then
+        if (i >= 0) then
+          loopShift (shiftArray1 i) j shiftArray1
+        else loopShift (-1) (j+1) shiftArray1
+      else
+        let shiftArray2 = if i+1 < j then update j plen shiftArray1 (i+1) else shiftArray1 in
+          loopShift (shiftArray1 j) (j+1) shiftArray2
+  in
+
+  let shiftArray3 = loopShift (-1) 1 shiftArray0 in
+
+  let rec loop s p =
+    if p < plen then
+      if  s < slen then
+        if str s = pat p then
+          loop (s+1) (p+1)
+        else
+          if p = 0 then
+            loop (s+1) p
+          else
+            loop s (shiftArray3 (p-1) + 1)
+        else (-1)
+    else (s - plen)
+  in
+    loop 0 0
+
+let main n a m b =
+  let array1 = make_array n a in
+  let array2 = make_array m b in
+  if n>0 && m>0 then (kmpMatch n array1 m array2; ()) else ()

input/annot/memoization.fib.annot

@@ -0,0 +1,8 @@
+%TYPE
+
+F :
+int ->
+int ->
+(int -> (int -> int -> *) -> *) ->
+n:int ->
+(int -> (int -> (int -> int -> *) -> *) -> r:int -> *[1 <= r /\ n-1 <= r]) -> *

input/annot/memoization.ml

@@ -0,0 +1,34 @@
+
+let new_tbl (n:int) : (int*int) list = []
+let get_tbl t (n:int) : int =
+  let rec aux (ts:(int*int) list) =
+    match ts with
+        [] -> let rec loop u : int = loop () in loop ()
+      | (k,x)::ts' -> if k=n then x else aux ts'
+  in
+    aux t
+let mem_tbl t (n:int) =
+  let rec aux (ts:(int*int) list) =
+    match ts with
+        [] -> false
+      | (k,x)::ts' -> if k=n then true else aux ts'
+  in
+    aux t
+let set_tbl t (n:int) (x:int) = (n,x)::t
+
+let fib i =
+  let rec f t0 n =
+    if mem_tbl t0 n then
+      (t0, get_tbl t0 n)
+    else if n <= 2 then
+      (t0, 1)
+    else
+      let (t1,r1) = f t0 (n-1) in
+      let (t2,r2) = f t1 (n-2) in
+      let r = r1 + r2 in
+        (set_tbl t2 n r, r)
+  in
+  let _,r = f (new_tbl 17) i in
+    assert (1 <= r && i-1 <= r)
+
+

input/annot/merge.merge.annot

@@ -0,0 +1,7 @@
+%TYPE
+
+MERGE :
+  (int -> int -> (int -> *) -> *) ->
+  l1:int -> (int -> (int -> *) -> *) ->
+  l2:int -> (int -> (int -> *) -> *) ->
+  (l3:int -> (int -> (int -> *) -> *) -> *[l1 < 0 \/ l2 < 0 \/ l3 = l1 + l2]) -> *

input/annot/merge.ml

@@ -0,0 +1,24 @@
+let rec merge order l1 l2 =
+  match l1,l2 with
+      [],_ -> l2
+    | _,[] -> l1
+    | h1::t1, h2::t2 ->
+      if order h1 h2 then h1 :: merge order t1 l2 else h2 :: merge order l1 t2
+
+let rec length xs =
+  match xs with
+      [] -> 0
+    | _::xs' -> 1 + length xs'
+
+let rec make_list n =
+  if n = 0
+  then []
+  else n :: make_list (n-1)
+
+let order (x:int) y = x > y
+
+let main n m =
+  let xs = make_list n in
+  let ys = make_list m in
+    assert (length (merge order xs ys) = length xs + length ys)
+

input/annot/soli.annot

@@ -0,0 +1,9 @@
+%TYPE
+
+SOLVE :
+  * ->
+  int ->
+  (int -> int -> (int -> *) -> *) ->
+  (int -> (int -> int -> int -> int -> *) -> *) ->
+  (int -> *) ->
+  (e:int -> *[ff]) -> *

input/annot/soli.ml

@@ -0,0 +1,125 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Caml examples                                *)
+(*                                                                     *)
+(*            Pierre Weis                                              *)
+(*                                                                     *)
+(*                        INRIA Rocquencourt                           *)
+(*                                                                     *)
+(*  Copyright (c) 1994-2011, INRIA                                     *)
+(*  All rights reserved.                                               *)
+(*                                                                     *)
+(*  Distributed under the BSD license.                                 *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* $Id: soli.ml,v 1.5 2011-08-08 19:31:17 weis Exp $ *)
+
+(** This program solves the famous game ``Le solitaire'', using a
+   trivial brute force algorithm (exhaustive exploration of the possible
+   games, until a solution is found).
+
+   No graphics involved here: the results are just printed out as ASCII
+   characters! *)
+
+type peg =
+   | Out
+   | Empty
+   | Peg
+;;
+
+let print_peg = function
+  | Out -> print_string ""
+  | Empty -> print_string " "
+  | Peg -> print_string "$"
+;;
+
+let print_board board =
+ for i = 0 to 8 do
+   for j = 0 to 8 do
+    print_peg @@board(i)(j)
+   done;
+   print_newline ()
+ done
+;;
+
+type direction = { dx : int; dy : int }
+
+type move = { x1 : int; y1 : int; x2 : int; y2 : int }
+
+exception Found
+;;
+
+let rec solve counter m board moves =
+  let dir i = List.nth
+    [ {dx = 0; dy = 1}; {dx = 1; dy = 0};
+       {dx = 0; dy = -1}; {dx = -1; dy = 0} ] i
+  in
+  counter := !counter + 1;
+  if m = 31 then
+    begin
+      match board(4)(4) with
+      | Peg -> true
+      | Out | Empty -> false
+    end
+  else
+    try
+      if !counter mod 500 = 0 then begin
+        print_int !counter; print_newline ()
+      end;
+      for i = 1 to 7 do
+        for j = 1 to 7 do
+          match board(i)(j) with
+          | Out | Empty -> ()
+          | Peg ->
+            for k = 0 to 3 do
+              let d1 = (dir(k)).dx in
+              let d2 = (dir(k)).dy in
+              let i1 = i + d1 in
+              let i2 = i1 + d1 in
+              let j1 = j + d2 in
+              let j2 = j1 + d2 in
+              match board(i1)(j1) with
+              | Out | Empty -> ()
+              | Peg ->
+                begin match board(i2)(j2) with
+                | Out | Peg -> ()
+                | Empty ->
+                    board(i)(j);
+                    board(i1)(j1);
+                    board(i2)(j2);
+                    if solve counter (m + 1) board moves then begin
+                      moves(m);
+                      raise Found
+                    end;
+                    board(i)(j);
+                    board(i1)(j1);
+                    board(i2)(j2); ()
+                end
+            done
+        done
+      done;
+      false with
+    | Found -> true
+;;
+
+let solve_solitaire () =
+  let board i j = List.nth (List.nth [
+    [ Out; Out; Out; Out; Out; Out; Out; Out; Out];
+    [ Out; Out; Out; Peg; Peg; Peg; Out; Out; Out];
+    [ Out; Out; Out; Peg; Peg; Peg; Out; Out; Out];
+    [ Out; Peg; Peg; Peg; Peg; Peg; Peg; Peg; Out];
+    [ Out; Peg; Peg; Peg; Empty; Peg; Peg; Peg; Out];
+    [ Out; Peg; Peg; Peg; Peg; Peg; Peg; Peg; Out];
+    [ Out; Out; Out; Peg; Peg; Peg; Out; Out; Out];
+    [ Out; Out; Out; Peg; Peg; Peg; Out; Out; Out];
+    [ Out; Out; Out; Out; Out; Out; Out; Out; Out];
+  ] i) j
+  in
+  let counter = ref 0 in
+  let moves i = {x1 = 0; y1 = 0; x2 = 0; y2 = 0} in
+  if solve counter 0 board moves then (print_string "\n"; print_board board)
+;;
+
+let main _ = if !Sys.interactive then () else solve_solitaire ()
+;;

input/annot/up3.loopa.annot

@@ -0,0 +1,3 @@
+%TYPE
+
+LOOPA : i:int -> k:int -> n:int -> (r:int -> *[(n < 0 \/ i >= n \/ 2 * r >= (n - i) + 2 * k) /\ (i < n \/ r = k)]) -> *

input/annot/up3.loopb.annot

@@ -0,0 +1,3 @@
+%TYPE
+
+LOOPB : j:int -> k:int -> n:int -> (* -> *) -> *[2*k >= n-j]

input/annot/up3.ml

@@ -0,0 +1,19 @@
+let rec loopa i k n =
+  if ( 2*i < 2*n ) then
+    loopa (i + 2) (k + 1) n
+  else k
+
+let rec loopb j k n =
+  if ( 2*j < 2*n ) then
+    let _ = assert (k > 0) in
+    loopb (j + 2) (k-1) n
+  else ()
+
+let main n =
+  let i = 0 in
+  let k = 0 in
+  if (n >= 0) then
+    let k = loopa i k n in
+    let j = 0 in
+    loopb j k n
+  else ()