From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 31 May 2018 12:55:57 +0000 (+0200)
Subject: Added simple_test.ml
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e41340acff1c4e4439b44ce5437542c905c352f;p=fireball-separation.git

Added simple_test.ml
---

diff --git a/ocaml/Makefile b/ocaml/Makefile
index d5c830b..fae0449 100644
--- 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 8b47f88..534100d 100644
--- 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
  let env = Pure.env_of_sigma freshno sigma in
  assert (Pure.diverged (Pure.mwhd (env,div,[])));
+ print_endline " D diverged.";
  assert (not (Pure.diverged (Pure.mwhd (env,conv,[]))));
+ print_endline " C converged.";
  ()
 ;;
 
@@ -249,6 +251,7 @@ print_cmd "EAT" "";
   | `Two -> p, delta in
  let subst = var, mk_lams t k in
  let p = subst_in_problem subst p in
+ sanity p;
  let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in
  sanity p; p
 ;;
@@ -389,3 +392,5 @@ auto' "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [
 
 print_hline();
 print_endline "ALL DONE. "
+
+let solve = auto';;
diff --git a/ocaml/simple.mli b/ocaml/simple.mli
new file mode 100644
index 0000000..d914117
--- /dev/null
+++ b/ocaml/simple.mli
@@ -0,0 +1 @@
+val solve : string -> string list -> unit
diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml
new file mode 100644
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 ----"
+;;