Ultime modifiche. Andrea scappa all'estero. Au revoir

diff --git a/ocaml_new/lambda4.ml b/ocaml_new/lambda4.ml
index 08b71541362f145841600c44afd277b7786ed246..c5fe7242e009f8cbcda28623ccbde1d95b12ef7f 100644 (file)
--- a/ocaml_new/lambda4.ml
+++ b/ocaml_new/lambda4.ml
@@ -47,14 +47,14 @@ let first args p var f =
    with Backtrack s ->
 prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ ");
 (* prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1)); *)
-     if k = 0 then aux p.initialSpecialK is else aux (k-1) ii
+     if k = 0 || true then aux p.initialSpecialK is else aux (k-1) ii
  in aux p.initialSpecialK args
 
 let all_terms p = p.div :: p.conv ;;
 
 let measure_of_term, measure_of_terms =
  let rec aux = function
- | `Bottom | `Pacman -> 0
+ | `Bottom | `Pacman _ -> 0
  | `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*)
  | `Lam(_,t) -> aux t
  | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list)
@@ -109,9 +109,10 @@ let subst_in_problem x inst ({div; conv} as p) =
 prerr_endline ("# INST0: " ^ string_of_var p.var_names x ^ " := " ^ string_of_term p inst);
  let div = subst false false x inst (div :> nf) in
  let conv = List.map (subst false false x inst) (conv :> nf list) in
- let conv = Util.filter_map (function `Lam _ | `Pacman -> None | `Bottom -> raise (Backtrack "bottom in conv") | #i_var as t -> Some t) conv in
+ let conv = List.concat (Util.filter_map (function
+  | `Lam _ -> None | `Pacman ts -> Some ts | `Bottom -> raise (Backtrack "bottom in conv") | #i_var as t -> Some [t]) conv) in
  match div with
-  | `Lam _ | `Pacman | `Var _ -> raise (Backtrack "lam in div")
+  | `Lam _ | `Pacman _ | `Var _ -> raise (Backtrack "lam in div")
   | `Bottom -> `Finished p
   | `I _ as div -> `Continue {p with div; conv}
 ;;
@@ -378,7 +379,7 @@ let compute_special_k tms =
  | `Lam(b,t) -> aux (k + if b then 1 else 0) t
  | `I(n, tms) -> Listx.max (Listx.map (aux 0) (tms :> nf Listx.listx))
  | `Bottom
- | `Pacman
+ | `Pacman _
  | `Var _ -> 0
  ) in
  let rec aux' top t = match t with
@@ -386,7 +387,7 @@ let compute_special_k tms =
  | `I((_,ar), tms) -> max ar
      (Listx.max (Listx.map (aux' false) (tms :> nf Listx.listx)))
  | `Bottom
- | `Pacman
+ | `Pacman _
  | `Var _ -> 0 in
  Listx.max (Listx.map (aux 0) tms) + Listx.max (Listx.map (aux' true) tms)
 ;;
@@ -431,7 +432,8 @@ let eat p =
  let hd, args, n = match p.div with `Var _ -> assert false | `I((x,_), l) -> x, l, Listx.length l in
  let rec aux = function
  | `Var _ | `Lam _ -> ()
- | `Pacman | `Bottom -> assert false
+ | `Pacman ts -> List.iter aux (ts :> nf list)
+ | `Bottom -> ()
  | `I((x,_),args') ->
      if x = hd then
       if Listx.length args' >= n then
@@ -543,7 +545,7 @@ let solve (p, todo) =
 
 let no_bombs_pacmans p =
     not (List.exists (eta_subterm `Bottom) p.conv)
- && not (eta_subterm `Pacman p.div)
+ && not (eta_subterm (`Pacman[]) p.div)
 ;;
 
 let check p =

diff --git a/ocaml_new/num.ml b/ocaml_new/num.ml
index f6b9405712a899fb89c4c87401eadacce8f9694e..1e69d29cf6ef74437b35bfd382a3bf98d2c75228 100644 (file)
--- a/ocaml_new/num.ml
+++ b/ocaml_new/num.ml
@@ -20,7 +20,7 @@ and i =
 ;;*)
 type var = int * (* arity of variable*) int;;
 type 'nf_nob i_var_ = [ `I of var * 'nf_nob Listx.listx | `Var of var ]
-type 'nf nf_nob_ = [ `Lam of (* was_unpacked *) bool * 'nf | `Pacman | ('nf nf_nob_) i_var_ ]
+type 'nf nf_nob_ = [ `Lam of (* was_unpacked *) bool * 'nf | `Pacman of (('nf nf_nob_) i_var_) list | ('nf nf_nob_) i_var_ ]
 type nf = [ nf nf_nob_ | `Bottom  ]
 type nf_nob = nf nf_nob_
 type i_var = nf_nob i_var_;;
@@ -51,7 +51,7 @@ let lift m (t : nf) =
   function
      #i_var as x -> (aux_i_num_var l x :> nf_nob)
    | `Lam(b,nf) -> `Lam (b, aux (l+1) nf)
-   | `Pacman -> `Pacman
+   | `Pacman ts -> `Pacman(List.map (aux_i_num_var l) ts)
  and aux l =
   function
      #nf_nob as x -> (aux_nob l x :> nf)
@@ -74,7 +74,8 @@ let free_vars' =
       (if x < n then [] else [(x-n,ar)]) @
       List.concat (List.map (aux n) (Listx.to_list args :> nf list))
   | `Lam(_,t) -> aux (n+1) t
-  | `Bottom | `Pacman -> []
+  | `Bottom  -> []
+  | `Pacman _ -> assert false
   in aux 0
 ;;
 let free_vars = (List.map fst) ++ free_vars';;
@@ -87,7 +88,7 @@ let rec scott_of_nf = function
  | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) (Pure.V v) (args :> nf Listx.listx)
  | `Lam(_,t) -> Pure.L (scott_of_nf t)
  | `Bottom -> Pure.B
- | `Pacman -> let f x = Pure.A (x,x) in f (Pure.L (Pure.L (f (Pure.V 0))))
+ | `Pacman _ -> let f x = Pure.A (x,x) in f (Pure.L (Pure.L (f (Pure.V 0))))
 end
 
 
@@ -107,7 +108,7 @@ let rec string_of_term =
   | `Lam(_,`Bottom) -> "BOMB"
   | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam lev l t ^ ")"
   | `Bottom -> "BOT"
-  | `Pacman -> "PAC"
+  | `Pacman _ -> "PAC"
  and string_of_term_no_pars_app lev l  = function
   | `I((n,ar), args) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars lev l) (Listx.to_list args :> nf list))
   | #nf as t -> string_of_term_w_pars lev l t
@@ -137,7 +138,7 @@ let cast_to_i_var =
 let rec set_arity arity = function
 (* FIXME because onlt variables should be in branches of matches, one day *)
 | `Var(n,_) -> `Var(n,arity)
-| `Bottom | `Pacman as t -> (t : nf)
+| `Bottom | `Pacman _ as t -> (t : nf)
 | `Lam(false, t) -> `Lam(false, set_arity arity (t :> nf))
 | `I _ | `Lam _ -> assert false
 
@@ -151,7 +152,8 @@ let rec mk_app (h : nf) (arg : nf) =
      | `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
      | `Var v -> `I(v, Listx.Nil arg)
      | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
-     | `Bottom | `Pacman as t -> t
+     | `Bottom -> `Bottom
+     | `Pacman ts as t -> match arg with #i_var as u -> `Pacman(u::ts) | _ -> t
 (*in let l = ["v0";"v1";"v2"] in
 prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
 
@@ -165,7 +167,7 @@ and mk_appx h args = Listx.fold_left mk_app h args
 and subst truelam delift_by_one what (with_what : nf(*_nob*)) (where : nf) =
  let rec aux_propagate_arity ar = function
  | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t)
- | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)
+ | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int || true); ar) else oldar)
  | _ as t -> t in
  let rec aux_i_var l =
   function
@@ -186,7 +188,7 @@ and subst truelam delift_by_one what (with_what : nf(*_nob*)) (where : nf) =
    | #i_var as x -> aux_i_var l x
    | `Lam(b, nf) -> `Lam(b, aux (l+1) nf)
    | `Bottom -> `Bottom
-   | `Pacman -> `Pacman
+   | `Pacman ts -> `Pacman(Util.filter_map (fun x -> match aux_i_var l x with #i_var as u -> Some u | _ -> None) ts)
 (*in let ll = ["v0";"v1";"v2"] in
 prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool delift_by_one ^ " what:" ^ (List.nth ll what) ^ " with_what:" ^ print ~l:ll with_what ^ " where:" ^ print ~l:ll iii ^ " res:" ^ print ~l:ll res); res*)
  in
@@ -212,7 +214,7 @@ let eta_compare x y =
   | `I((n1,_), l1), `I((n2,_), l2) ->
     clex compare (lex aux) (n1, (Listx.to_list l1 :> nf list)) (n2, (Listx.to_list l2 :> nf list))
   | `Bottom, `Bottom
-  | `Pacman, `Pacman -> 0
+  | `Pacman _, `Pacman _ -> 0
   | `Bottom, `Lam(_,t) -> -1
   | `Lam(_,t), `Bottom ->  1
   | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
@@ -222,8 +224,8 @@ let eta_compare x y =
   | _, `I _ -> 1
   | `Bottom, _ -> -1
   | _, `Bottom -> 1
-  | `Pacman, _ -> -1
-  | _, `Pacman -> 1
+  | `Pacman _, _ -> -1
+  | _, `Pacman _ -> 1
   in aux x y
 ;;
 
@@ -234,7 +236,7 @@ let rec eta_subterm sub t =
   match t with
   | `Lam(_,t') -> eta_subterm (lift 1 sub) t'
   | `Bottom
-  | `Pacman  -> false
+  | `Pacman _ -> false
   | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
    | `Var(v',_) -> v = v'
    | `I((v',_), args') -> v = v'
@@ -258,7 +260,7 @@ let max_arity_tms n =
   | `Var v -> aux_var l v
   | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms :> nf list))
   | `Lam(_,t) -> aux (l+1) t
-  | `Bottom | `Pacman -> None
+  | `Bottom | `Pacman _ -> None
  and aux_tms l =
   List.fold_left (fun acc t -> max acc (aux l t)) None in
  fun tms -> aux_tms 0 (tms :> nf list)

diff --git a/ocaml_new/num.mli b/ocaml_new/num.mli
index 8b0bab458f799261fe45104764a41d367ae361a5..ed8e6c936a02eba231b6b1aaaff07674d1bd6c4b 100644 (file)
--- a/ocaml_new/num.mli
+++ b/ocaml_new/num.mli
@@ -4,13 +4,13 @@ type 'nf_nob i_var_ = [ `I of var * 'nf_nob Listx.listx | `Var of var ]
 type 'nf nf_nob_ =
     [ `I of var * 'nf nf_nob_ Listx.listx
     | `Lam of bool * 'nf
-    | `Pacman
+    | `Pacman of (('nf nf_nob_) i_var_) list
     | `Var of var ]
 type nf =
     [ `Bottom
     | `I of var * nf nf_nob_ Listx.listx
     | `Lam of bool * nf
-    | `Pacman
+    | `Pacman of ((nf nf_nob_) i_var_) list
     | `Var of var ]
 type nf_nob = nf nf_nob_
 type i_var = nf_nob i_var_

diff --git a/ocaml_new/parser.ml b/ocaml_new/parser.ml
index 487f0425bbee5e6687729e681cf2ea779087eaa1..9c36b4366087d00e1aefa49e1eab72bc6844b335 100644 (file)
--- a/ocaml_new/parser.ml
+++ b/ocaml_new/parser.ml
@@ -186,7 +186,7 @@ let problem_of_string s =
  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_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
@@ -200,7 +200,7 @@ let problem_of_string s =
  | `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
- | `Pacman -> `Pacman\r
+ | `Pacman _ as t -> t\r
  and aux lev : Num.nf -> Num.nf = function\r
   | #nf_nob as t -> aux_nob lev t\r
   | `Bottom -> assert false in\r

diff --git a/ocaml_new/problems/2 b/ocaml_new/problems/2
index 0f3d6b112cce3ede1f5d620c50ce3d0f8dd235f3..335d6357d726c82158537c5e227acc935f2a068a 100644 (file)
--- a/ocaml_new/problems/2
+++ b/ocaml_new/problems/2
@@ -23,6 +23,66 @@ C x BOMB z
 $? 2.5'\r
 D x (_. y y)\r
 C x (_. BOMB) z\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!    D x (_.    BOT)     !!!!!!!!!!!\r
+!!!!!!!!!!!!!!    C x (_. _. BOT)     !!!!!!!!!!!\r
+!!!!!!!!!!!!!!    C x (_. z. z u) t   !!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\r
 \r
 ???????????????\r
 D x a1 a2 a3\r

diff --git a/ocaml_new/problems/3 b/ocaml_new/problems/3
new file mode 100644 (file)
index 0000000..a586545
--- /dev/null
+++ b/ocaml_new/problems/3
@@ -0,0 +1,7 @@
+$????????????\r
+D x y\r
+C x PAC (x y)\r
+\r
+$!!!!!!!!!!!!!\r
+D x y z\r
+C x PAC (x y)\r

diff --git a/ocaml_new/problems/boh b/ocaml_new/problems/boh
new file mode 100644 (file)
index 0000000..bdd3ea2
--- /dev/null
+++ b/ocaml_new/problems/boh
@@ -0,0 +1,5 @@
+$test.out\r
+D z (λv0. v0) a (z (λv0. b)) (z (λv0. v0) v (λv0. v0)) (z PAC (a (λv0. w)) (λv0. λv1. v1)) (z (λv0. v0) a (z (λv0. b)) (z (λv0. v0) v (λv0. v0)) (z PAC (a (λv0. w)) (λv0. λv1. v1)) (w PAC w))\r
+C z (λv0. v0) a (y v (λv0. y)) (z b (z (λv0. v0) v)) (a (λv0. w) (z PAC (λv0. v0)) (z (λv0. v0) a))\r
+C z b (w PAC w) (z (λv0. v0) v) (λv0. w) (y v (λv0. y)) (λv0. λv1. v1)\r
+C z PAC (λv0. v0) (λv0. w PAC) (λv0. z (λv1. v1) v) (λv0. z (λv1. v1) a (z (λv1. b)) (z (λv1. v1) v (λv1. v1)) (z PAC (a(λv1. w)) (λv1. λv2. v2))) (x (z (λv0. v0) a))\r

diff --git a/ocaml_new/problems/pac b/ocaml_new/problems/pac
new file mode 100644 (file)
index 0000000..6b4e029
--- /dev/null
+++ b/ocaml_new/problems/pac
@@ -0,0 +1,3 @@
+$!\r
+D x PAC due tre\r
+C x uno due tre\r

diff --git a/ocaml_new/test.ml b/ocaml_new/test.ml
index 293c1e69c3e3dc62d29cfca782f922ac14c5f479..f345f05925e9865ab7e8ab0b0c579663edb66c3c 100644 (file)
--- a/ocaml_new/test.ml
+++ b/ocaml_new/test.ml
@@ -35,7 +35,7 @@ let test3 n vars =
       then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams\r
       else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams\r
     in aux (n-1) inerts lams\r
-  in aux (2*n) vars []\r
+  in aux (2*n) vars ["PAC"; "PAC"]\r
 ;;\r
 \r
 let test4 n vars =\r
@@ -71,7 +71,7 @@ let call_main4 div conv =
 let main =\r
   Random.self_init ();\r
   let num = 100 in\r
-  let complex = 1000 in\r
+  let complex = 100 in\r
   let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in\r
 \r
   (* let open Parser in *)\r