Added simple_test.ml

diff --git a/ocaml/Makefile b/ocaml/Makefile
index d5c830bc09aa0205464b8c2610c62fbbbcdab8c2..fae0449c2c5cdf2e311c140b2b0d2f8d2944c43e 100644 (file)
--- a/ocaml/Makefile
+++ b/ocaml/Makefile
@@ -2,7 +2,7 @@ OCAMLC = ocamlopt -g -rectypes
 LIB = unix.cmxa str.cmxa
 UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx parser_andrea.cmx
 
-all: a.out test4.out simple.out
+all: a.out test4.out simple.out simple_test.out
 
 run: test4.out
        bash run
@@ -16,6 +16,9 @@ test4.out: $(UTILS) lambda4.cmx test.ml
 simple.out: $(UTILS) simple.ml
        $(OCAMLC) -o simple.out $(LIB) $(UTILS) simple.ml
 
+simple_test.out: $(UTILS) simple.cmx simple_test.ml
+       $(OCAMLC) -o simple_test.out $(LIB) $^
+
 %.cmi: %.mli
        $(OCAMLC) -c $<
 

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 8b47f88a5693153a630fdad73b9a20a2f3556226..534100d4f0787961fb688461dd34f52d82314bed 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -175,7 +175,9 @@ let check p sigma =
  let freshno = List.fold_right (fun (x,_) -> max x) sigma 0 in\r
  let env = Pure.env_of_sigma freshno sigma in\r
  assert (Pure.diverged (Pure.mwhd (env,div,[])));\r
+ print_endline " D diverged.";\r
  assert (not (Pure.diverged (Pure.mwhd (env,conv,[]))));\r
+ print_endline " C converged.";\r
  ()\r
 ;;\r
 \r
@@ -249,6 +251,7 @@ print_cmd "EAT" "";
   | `Two -> p, delta in\r
  let subst = var, mk_lams t k in\r
  let p = subst_in_problem subst p in\r
+ sanity p;\r
  let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in\r
  sanity p; p\r
 ;;\r
@@ -389,3 +392,5 @@ auto' "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [
 \r
 print_hline();\r
 print_endline "ALL DONE. "\r
+\r
+let solve = auto';;\r

diff --git a/ocaml/simple.mli b/ocaml/simple.mli
new file mode 100644 (file)
index 0000000..d914117
--- /dev/null
+++ b/ocaml/simple.mli
@@ -0,0 +1 @@
+val solve : string -> string list -> unit\r

diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml
new file mode 100644 (file)
index 0000000..9618113
--- /dev/null
+++ b/ocaml/simple_test.ml
@@ -0,0 +1,50 @@
+open Simple;;
+open Util;;
+
+let acaso l =
+    let n = Random.int (List.length l) in
+    List.nth l n
+;;
+
+let acaso2 l1 l2 =
+  let n1 = List.length l1 in
+  let n = Random.int (n1 + List.length l2) in
+  if n >= n1 then List.nth l2 (n - n1) else List.nth l1 n
+;;
+
+let gen n vars =
+  let rec take' l n =
+    if n = 0 then []
+    else match l with
+    | [] -> []
+    | [_] -> assert false
+    | x::_::xs -> x :: take' xs (n-1) in
+  let rec aux n inerts lams =
+    if n = 0 then List.hd inerts, take' (Util.sort_uniq (List.tl inerts)) 5
+    else let inerts, lams = if Random.int 2 = 0
+      then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams
+      else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams
+    in aux (n-1) inerts lams
+  in aux (2*n) vars []
+;;
+
+
+let rec repeat f n =
+  prerr_endline "\n########################### NEW TEST ###########################";
+  f () ;
+  if n > 0 then repeat f (n-1)
+;;
+
+let main =
+  Random.self_init ();
+  let num = 100 in
+  let complex = 200 in
+  let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in
+
+  repeat (fun _ ->
+    let div, convs = gen complex vars in
+    Simple.solve div convs
+  ) num ;
+
+  prerr_endline "\n---- ALL TESTS COMPLETED ----"
+;;