]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Updated simple with current parser
authoracondolu <andrea.condoluci@unibo.it>
Thu, 31 May 2018 21:38:31 +0000 (23:38 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Thu, 31 May 2018 21:38:31 +0000 (23:38 +0200)
- Removed parser_andrea
- Generalized problems.ml
- Moved sample problems from simple.ml to problems/simple.0

ocaml/Makefile
ocaml/lambda4.ml
ocaml/parser_andrea.ml [deleted file]
ocaml/parser_andrea.mli [deleted file]
ocaml/problems.ml
ocaml/problems.mli
ocaml/problems/simple.0 [new file with mode: 0644]
ocaml/simple.ml
ocaml/simple.mli
ocaml/simple_test.ml

index fae0449c2c5cdf2e311c140b2b0d2f8d2944c43e..3a94a7ac8174006d075c6cf3b883276c814a6a0c 100644 (file)
@@ -1,13 +1,13 @@
 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
+UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx problems.cmx
 
 all: a.out test4.out simple.out simple_test.out
 
 run: test4.out
        bash run
 
-a.out: $(UTILS) lambda4.cmx problems.cmx
+a.out: $(UTILS) lambda4.cmx
        $(OCAMLC) -o a.out $(LIB) $^
 
 test4.out: $(UTILS) lambda4.cmx test.ml
index 9395daa7e0998eca7c8f9bd2a3ccca8be25f164e..90a91e048b26c88a403f5de22103581f8497cb89 100644 (file)
@@ -719,3 +719,14 @@ let problem_of (label, div, conv, ps, var_names) =
    [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
  {freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK; var_names; label}
 ;;
+
+(* assert_depends solves the problem, and checks if the result was expected *)
+let assert_depends x =
+ let c = String.sub (label_of_problem x) 0 1 in
+ match solve x with
+ | `Unseparable s when c = "!" ->
+    failwith ("assert_depends: unseparable because: " ^ s ^ ".")
+ | `Separable _  when c = "?" ->
+    failwith ("assert_depends: separable.")
+ | _ -> () in
+Problems.main (assert_depends ++ problem_of);
diff --git a/ocaml/parser_andrea.ml b/ocaml/parser_andrea.ml
deleted file mode 100644 (file)
index fbce730..0000000
+++ /dev/null
@@ -1,266 +0,0 @@
-type term =\r
-  | Var of int\r
-  | App of term * term\r
-  | Lam of term\r
-;;\r
-\r
-let mk_app x y = App(x, y);;\r
-let mk_lam x = Lam x;;\r
-let mk_var x = Var x;;\r
-\r
-exception ParsingError of string;;\r
-\r
-let isAlphaNum c = let n = Char.code c in\r
- (48 <= n && n <= 90) || (95 <= n && n <= 122) ;;\r
-let isSpace c = c = ' ' || c = '\n' || c = '\t' ;;\r
-\r
-(* FIXME *)\r
-let mk_var' (bound, free) x =\r
-  if x <> "@" && List.mem x bound\r
-  then free, mk_var (Util.index_of x bound)\r
-  else if x <> "@" && List.mem x free\r
-       then free, mk_var (List.length bound + Util.index_of x free)\r
-       else (free @ [x]), mk_var (List.length bound + List.length free)\r
-;;\r
-\r
-let mk_app' = function\r
-  | [] ->  assert false\r
-  | t :: ts -> List.fold_left mk_app t ts\r
-;;\r
-\r
-let explode s =\r
- let len = String.length s in\r
-  let rec aux i l =\r
-    if i >= len || s.[i] = '#' then l else aux (i+1) (s.[i] :: l)\r
-  in List.rev (aux 0 [])\r
-;;\r
-\r
-let implode l =\r
-  let res = String.create (List.length l) in\r
-  let rec aux i = function\r
-    | [] -> res\r
-    | c :: l -> String.set res i c; aux (i + 1) l in\r
-  aux 0 l\r
-;;\r
-\r
-let rec strip_spaces = function\r
-  | c::cs when isSpace c -> strip_spaces cs\r
-  | cs -> cs\r
-;;\r
-\r
-let read_var s =\r
-  let rec aux = function\r
-  | [] -> None, []\r
-  | c::cs as x ->\r
-    if c = '@' then\r
-     (if cs <> [] && (let hd = List.hd cs in hd = '@' || isAlphaNum hd)\r
-     then raise (ParsingError ("Unexpected `"^String.make 1 (List.hd cs)^"` after `@`."))\r
-     else Some['@'], cs)\r
-    else if isAlphaNum c\r
-    then match aux cs with\r
-         | (Some x), cs' -> Some (c :: x), cs'\r
-         | None, cs' -> (Some [c]), cs'\r
-    else None, x\r
-  in match aux s with\r
-    | None, y -> None, y\r
-    | Some x, y -> Some (implode x), y\r
-;;\r
-\r
-let read_var' (bound, free as vars) s =\r
-  match read_var s with\r
-  | Some varname, cs ->\r
-    let free, v = mk_var' vars varname in\r
-    Some [v], cs, (bound, free)\r
-  | None, _ -> raise (ParsingError ("Can't read variable"))\r
-;;\r
-\r
-let rec read_smt vars =\r
-  let check_if_lambda cs = match read_var cs with\r
-    | None, _ -> false\r
-    | Some x, cs -> match strip_spaces cs with\r
-      | [] -> false\r
-      | c::_ -> c = '.'\r
-  in let read_lambda (bound, free) cs = (\r
-    match read_var (strip_spaces cs) with\r
-      | Some varname, cs ->\r
-      let vars' = (varname::bound, free) in\r
-      (match strip_spaces cs with\r
-        | [] -> raise (ParsingError "Lambda expression incomplete")\r
-        | c::cs -> (if c = '.' then (match read_smt vars' cs with\r
-          | None, _, _ -> raise (ParsingError "Lambda body expected")\r
-          | Some [x], y, (_, free) -> Some [mk_lam x], y, (bound, free)\r
-          | Some _, _, _ -> assert false\r
-          ) else raise (ParsingError "Expected `.` after variable in lambda")\r
-        ))\r
-      | _, _ -> assert false\r
- ) in let rec aux vars cs =\r
-  match strip_spaces cs with\r
-  | [] -> None, [], vars\r
-  | c::_ as x ->\r
-      let tms, cs, vars = (\r
-           if c = '(' then read_pars vars x\r
-      else if c = ')' then (None, x, vars)\r
-      else if check_if_lambda x then read_lambda vars x\r
-      else read_var' vars x) in\r
-      match tms with\r
-      | Some [tm] -> (\r
-        match aux vars cs with\r
-          | None, cs, vars -> Some [tm], cs, vars\r
-          | Some ts, cs, vars -> Some (tm :: ts), cs, vars\r
-        )\r
-      | Some _ -> assert false\r
-      | None -> None, x, vars\r
-  in fun cs -> match aux vars cs with\r
-    | None, cs, vars -> None, cs, vars\r
-    | Some ts, cs, vars -> Some [mk_app' ts], cs, vars\r
-and read_pars vars = function\r
-  | [] -> None, [], vars\r
-  | c::cs -> if c = '(' then (\r
-    let tm, cs, vars = read_smt vars cs in\r
-    let cs = strip_spaces cs in\r
-    match cs with\r
-      | [] -> None, [], vars\r
-      | c::cs -> if c = ')' then tm, cs, vars else raise (ParsingError "Missing `)`")\r
-    ) else assert false\r
-;;\r
-\r
-let parse x =\r
-  match read_smt ([],[]) (explode x) with\r
-  | Some [y], [], _ -> y\r
-  | _, _, _ -> assert false\r
-;;\r
-\r
-let parse_many strs =\r
-  let f (x, y) z = match read_smt y (explode z) with\r
-  | Some[tm], [], vars -> (tm :: x, vars)\r
-  | _, _, _ -> assert false\r
-  in let aux = List.fold_left f ([], ([], []))\r
-  in let (tms, (_, free)) = aux strs\r
-  in (List.rev tms, free)\r
-;;\r
-\r
-(**********************************************************************\r
-\r
-let rec string_of_term = function\r
-  | Tvar n -> string_of_int n\r
-  | Tapp(t1, t2) -> "(" ^ string_of_term t1 ^ " " ^ string_of_term t2 ^ ")"\r
-  | Tlam(t1) -> "(\\" ^ string_of_term t1 ^ ")"\r
-;;\r
-\r
-let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j"));;\r
-\r
-\r
-*******************************************************************************)\r
-\r
-(* let problem_of_string s =\r
- let lines = Str.split (Str.regexp "[\n\r\x0c\t;]+") s in\r
- let head, lines = List.hd lines, List.tl lines in\r
- let name = String.trim (String.sub head 1 (String.length head - 1)) in\r
- let lines = List.filter ((<>) "") lines in\r
- let aux (last, div, conv, ps) line =\r
-  let chr = String.sub line 0 1 in\r
-  let line = String.trim (String.sub line 1 (String.length line - 1)) in\r
-  if line = "" then chr, div, conv, ps else\r
-  let rec aux' chr line =\r
-   if chr = "#"\r
-    then chr, div, conv, ps\r
-   else if chr = "D"\r
-    then chr, line, conv, ps\r
-   else if chr = "C"\r
-    then chr, div, line::conv, ps\r
-   else if chr = "N"\r
-    then chr, div, conv, line::ps\r
-   else if chr = " "\r
-    then aux' last line\r
-   else raise (ParsingError\r
-     ("Unexpected at beginning of problem: `" ^ chr ^ "` " ^ line)) in\r
-  aux' chr line in\r
- let _, div, conv, ps = List.fold_left aux ("#", "", [], []) lines in\r
- let div_provided = div <> "" in\r
- let div = if div_provided then div else "BOT" in\r
- let strs = [div] @ ps @ conv in\r
-\r
- if List.length ps = 0 && List.length conv = 0\r
-  then raise (ParsingError "Parsed empty problem");\r
-\r
- (* parse' *)\r
- let (tms, free) = parse_many strs in\r
- (* Replace pacmans and bottoms *)\r
- let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in\r
- let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in\r
- let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in\r
- let fix lev v =\r
-  if v = lev + n_bot then `Bottom\r
-   else if v = lev + n_pac then `Pacman\r
-    else if v = lev + n_bomb then `Lam(true, `Bottom)\r
-    else if v = lev then `Var(v, min_int) (* zero *)\r
-     else `Var(v,1) in (* 1 by default when variable not applied *)\r
- (* Fix arity *)\r
- let open Num in\r
- let exclude_bottom = function\r
- | #nf_nob as t -> t\r
- (* actually, the following may be assert false *)\r
- | `Bottom -> raise (ParsingError "Input term not in normal form") in\r
- let rec aux_nob lev : nf_nob -> nf = function\r
- | `I((n,_), args) -> `I((n,(if lev = 0 then 0 else 1) + Listx.length args), Listx.map (fun t -> exclude_bottom (aux_nob lev t)) args)\r
- | `Var(n,_) -> fix lev n\r
- | `Lam(_,t) -> `Lam (true, aux (lev+1) t)\r
- | `Match _ | `N _ -> assert false\r
- | `Pacman -> `Pacman\r
- and aux lev : Num.nf -> Num.nf = function\r
-  | #nf_nob as t -> aux_nob lev t\r
-  | `Bottom -> assert false in\r
-let all_tms = List.map (aux 0) (tms :> Num.nf list) in\r
-\r
-(* problem_of *)\r
-let div, (ps, conv) = List.hd all_tms, Util.list_cut (List.length ps, List.tl all_tms) in\r
-\r
-let div = if not div_provided || div = `Bottom\r
- then None\r
- else match div with\r
-  | `I _ as t -> Some t\r
-  | _ -> raise (ParsingError "D is not an inert in the initial problem") in\r
-let conv = Util.filter_map (\r
- function\r
- | #i_n_var as t -> Some t\r
- | `Lam _ -> None\r
- | _ -> raise (ParsingError "A C-term is not i_n_var")\r
- ) conv in\r
-let ps = List.map (\r
- function\r
-  | #i_n_var as y -> y\r
-  | _ -> raise (ParsingError "An N-term is not i_n_var")\r
- ) ps in\r
- name, div, conv, ps, free\r
-;;\r
-\r
-\r
-let from_file path =\r
- let lines = ref ["#"] in\r
- let chan = open_in path in\r
- let _ = try\r
-  while true; do\r
-    lines := input_line chan :: !lines\r
-  done\r
- with End_of_file ->\r
-  close_in chan in\r
- let txt = String.concat "\n" (List.rev !lines) in\r
- let problems = Str.split (Str.regexp "[\n\r]+\\$") txt in\r
- List.map problem_of_string (List.tl (List.map ((^) "$") problems))\r
-;; *)\r
-\r
-let parse x =\r
-  match read_smt ([],[]) (explode x) with\r
-  | Some [y], [], _ -> y\r
-  | _, _, _ -> assert false\r
-;;\r
-\r
-\r
-let parse_many strs =\r
-  let f (x, y) z = match read_smt y (explode z) with\r
-  | Some[tm], [], vars -> (tm :: x, vars)\r
-  | _, _, _ -> assert false\r
-  in let aux = List.fold_left f ([], ([], []))\r
-  in let (tms, (_, free)) = aux strs\r
-  in (List.rev tms, free)\r
-;;\r
diff --git a/ocaml/parser_andrea.mli b/ocaml/parser_andrea.mli
deleted file mode 100644 (file)
index 8dba854..0000000
+++ /dev/null
@@ -1,25 +0,0 @@
-type term =\r
-  | Var of int\r
-  | App of term * term\r
-  | Lam of term\r
-\r
-exception ParsingError of string\r
-\r
-(* val problem_of_string:\r
- string ->\r
-  string (* problem label *)\r
-  * Num.i_var option (* div *)\r
-  * Num.i_n_var list (* conv *)\r
-  * Num.i_n_var list (* ps *)\r
-  * string list (* names of free variables *)\r
-val from_file : string ->\r
- (string (* problem label *)\r
- * Num.i_var option (* div *)\r
- * Num.i_n_var list (* conv *)\r
- * Num.i_n_var list (* ps *)\r
- * string list (* names of free variables *)) list *)\r
-\r
- (* parses a string to a term *)\r
- val parse: string -> term\r
- (* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *)\r
- val parse_many: string list -> term list * string list\r
index 9ff47787f995e34bf7222d6d495dc7c1ba7a9da9..28edcebd64cdffb4a1c8c8c0301aa74f071753c1 100644 (file)
@@ -1,4 +1,3 @@
-open Lambda4;;
 open Util;;
 
 (* Syntax for problem files in problem/ folder:
@@ -17,23 +16,12 @@ open Util;;
 
 *)
 
-(* assert_depends solves the problem, and checks if the result was expected *)
-let assert_depends x =
- let c = String.sub (label_of_problem x) 0 1 in
- match solve x with
- | `Unseparable s when c = "!" ->
-    failwith ("assert_depends: unseparable because: " ^ s ^ ".")
- | `Separable _  when c = "?" ->
-    failwith ("assert_depends: separable.")
- | _ -> ()
-;;
-
-(* TODO *)
-(* div under a lambda in conv *)
-
-if Array.length Sys.argv = 1
- then failwith "no command line args. Please use e.g. ./a.out problems/*"
-else Array.iteri (fun i filename -> if i > 0 then
- List.iter (assert_depends ++ problem_of) (Parser.from_file filename)
- ) Sys.argv
+let main f =
+ print_endline Sys.executable_name;
+ try ignore (Str.search_forward (Str.regexp_string "test") Sys.executable_name 0)
+ with Not_found ->
+  (if Array.length Sys.argv = 1
+   then failwith "no command line args. Please use e.g. ./cmd.out problems/*"
+   else Array.iteri (fun i filename -> if i > 0 then
+    List.iter f (Parser.from_file filename)) Sys.argv)
 ;;
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..5315cc7903cf5325898edcfd71918385add6716f 100644 (file)
@@ -0,0 +1,4 @@
+val main :
+  (string * Num.i_var option * Num.i_n_var list * Num.i_n_var list *
+   string list -> unit) ->
+  unit
diff --git a/ocaml/problems/simple.0 b/ocaml/problems/simple.0
new file mode 100644 (file)
index 0000000..4942099
--- /dev/null
@@ -0,0 +1,46 @@
+$ simple.0/0\r
+D x x\r
+C x y\r
+C y y\r
+C y x\r
+\r
+$ simple.0/1\r
+D x y\r
+C x (_. x)\r
+C y z\r
+C y x\r
+\r
+$ simple.0/2\r
+D a (x. x b) (x. x c)\r
+C a (x. b b) @\r
+C a @ c\r
+C a (x. x x) a\r
+C a (a a a) (a c c)\r
+\r
+$ simple.0/3\r
+D x (y. x y y)\r
+C x (y. x y x)\r
+\r
+$ simple.0/4\r
+D x a a a a\r
+C x b a a a\r
+C x a b a a\r
+C x a a b a\r
+C x a a a b\r
+\r
+$ simple.0/5\r
+# Controesempio ad usare un conto dei lambda che non considera le permutazioni\r
+D x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b\r
+C x a a a a (_. a) b b b\r
+C x a a a a (_. _. _. _. x. y. x y)\r
+\r
+$ simple.0/6\r
+# bug in eat that was erasing terms in convergent that then diverged\r
+D x y z\r
+C x @ @\r
+C z (y @ (y @))\r
+\r
+$ simple.0/7\r
+# bug in no_leading_lambdas where x in j-th position\r
+D v0 (v1 v2) (x. y. v0 v3 v4 v2)\r
+C v5 (v6 (x. v6) v7 v8 (x. v9) (x. v9 (v10 v10))) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y))) (v9 (x. v11) (v4 v8) (x. y. z. v12) (v4 v6 (x. v7 v11) v12) (x. x v8)) (v0 v3 v4 v9 (v7 v11) (v0 v3 v4 v2) v10) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y)) (v9 (x. v11) (v4 v8)))\r
index efa5c25d88fd47912ed7b5d656074a1c9bc685f9..991779e7ac995f5f980a174b43c292689cac1ce6 100644 (file)
@@ -287,19 +287,10 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")")
  let p = subst_in_problem subst p in\r
  sanity p\r
 ;;\r
-;;\r
 \r
-let parse strs =\r
-  let rec aux level = function\r
-  | Parser_andrea.Lam t -> L (aux (level + 1) t)\r
-  | Parser_andrea.App (t1, t2) ->\r
-   if level = 0 then mk_app (aux level t1) (aux level t2)\r
-    else A(aux level t1, aux level t2)\r
-  | Parser_andrea.Var v -> V v in\r
-  let (tms, free) = Parser_andrea.parse_many strs in\r
-  (List.map (aux 0) tms, free)\r
 ;;\r
 \r
+\r
 let rec auto p =\r
  let hd_var, n_args = get_inert p.div in\r
  match get_subterm_with_head_and_args hd_var n_args p.conv with\r
@@ -320,13 +311,20 @@ let rec auto p =
   auto p\r
 ;;\r
 \r
-let problem_of div convs =\r
- let rec conv_join = function\r
-  | [] -> "@"\r
-  | x::xs -> conv_join xs ^ " ("^ x ^")" in\r
+let problem_of (label, div, convs, ps, var_names) =\r
  print_hline ();\r
- let conv = conv_join convs in\r
- let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
+ let rec aux = function\r
+ | `Lam(_, t) -> L (aux t)\r
+ | `I ((v,_), args) -> Listx.fold_left (fun x y -> mk_app x (aux y)) (V v) args\r
+ | `Var(v,_) -> V v\r
+ | `N _ | `Match _ -> assert false in\r
+ assert (List.length ps = 0);\r
+ let convs = List.rev convs in\r
+ let conv = List.fold_left (fun x y -> mk_app x (aux (y :> Num.nf))) (V (List.length var_names)) convs in\r
+ let var_names = "@" :: var_names in\r
+ let div = match div with\r
+ | Some div -> aux (div :> Num.nf)\r
+ | None -> assert false in\r
  let varno = List.length var_names in\r
  let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in\r
  (* initial sanity check *)\r
@@ -339,7 +337,7 @@ let solve p =
   else check p (auto p)\r
 ;;\r
 \r
-let run x y = solve (problem_of x y);;\r
+Problems.main (solve ++ problem_of);\r
 \r
 (* Example usage of interactive: *)\r
 \r
@@ -370,37 +368,3 @@ let run x y = solve (problem_of x y);;
 (* interactive "x y"\r
  "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]\r
 ;; *)\r
-\r
-run "x x" ["x y"; "y y"; "y x"] ;;\r
-run "x y" ["x (_. x)"; "y z"; "y x"] ;;\r
-run "a (x. x b) (x. x c)" ["a (x. b b) @"; "a @ c"; "a (x. x x) a"; "a (a a a) (a c c)"] ;;\r
-\r
-run "x (y. x y y)" ["x (y. x y x)"] ;;\r
-\r
-run "x a a a a" [\r
- "x b a a a";\r
- "x a b a a";\r
- "x a a b a";\r
- "x a a a b";\r
-] ;;\r
-\r
-(* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)\r
-run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [\r
- "x a a a a (_. a) b b b";\r
- "x a a a a (_. _. _. _. x. y. x y)";\r
-] ;;\r
-\r
-(* bug in eat that was erasing terms in convergent that then diverged *)\r
-run "x y z"\r
-[\r
-"x @ @";\r
-"z (y @ (y @))"\r
-] ;;\r
-\r
-(* bug in no_leading_lambdas where x in j-th position *)\r
-run "v0 (v1 v2) (x. y. v0 v3 v4 v2)"\r
-["v5 (v6 (x. v6) v7 v8 (x. v9) (x. v9 (v10 v10))) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y))) (v9 (x. v11) (v4 v8) (x. y. z. v12) (v4 v6 (x. v7 v11) v12) (x. x v8)) (v0 v3 v4 v9 (v7 v11) (v0 v3 v4 v2) v10) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y)) (v9 (x. v11) (v4 v8)))"]\r
-;;\r
-\r
-print_hline();\r
-print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<"\r
index 216e3810bb241679aa43734ceb38bade28b3fd7b..bdc632827889ffe4136c179ae95001f1f1854e92 100644 (file)
@@ -1,4 +1,5 @@
-(* type problem\r
-val problem_of : string -> string list -> problem\r
-val solve : problem -> unit *)\r
-val run : string -> string list -> unit\r
+type problem\r
+val solve : problem -> unit\r
+val problem_of :\r
+  string * Num.i_var option * Num.i_n_var list * Num.i_n_var list *\r
+  string list -> problem\r
index 8bdefdcb426939e42a192c7e7e0c079c0a9c6863..438b7b572f0a6ebc845a0a90514a2e3c19782664 100644 (file)
@@ -45,7 +45,10 @@ let main =
 
   repeat (fun _ ->
     let div, convs = gen complex vars in
-    Simple.run div convs
+    let str = "$ random simple test \nD " ^ div ^ String.concat "\nC " convs ^ "\n" in
+    print_endline str;
+    let open Simple in
+    (solve ++ problem_of ++ Parser.problem_of_string) str
   ) num ;
 
   prerr_endline "\n---- ALL TESTS COMPLETED ----"