X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=82d5046576a6853ac251a27a4bd8c72fe5bd08e7;hb=6d9e673e3a6896f487988d897f927d07104d6a73;hp=9ab675e6b95ab242efc8e138d3c62309a92328e7;hpb=6f8c64dcbe6b864cb0f9417bfab284e398337ae3;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 9ab675e..82d5046 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -6,15 +6,13 @@ open Num
 (* exceptions *)
 exception Pacman
 exception Bottom
+exception Lambda
 exception Backtrack of string
 
-(*
- The number of arguments which can applied to numbers
- safely, depending on the encoding of numbers.
- For Scott's encoding, two.
-*)
-let num_more_args = 2;;
+(* verbosity *)
 let _very_verbose = false;;
+(** Display measure of every term when printing problem *)
+let _measure_of_terms = false;;
 
 let verbose s =
  if _very_verbose then prerr_endline s
@@ -87,6 +85,7 @@ let problem_measure p = sum_arities p;;
 let string_of_measure = string_of_int;;
 
 let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
+ let aux_measure_terms t = if _measure_of_terms then "(" ^ string_of_int (measure_of_term t) ^ ") " else "" in
  let deltas = String.concat ("\n#  ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
  let l = p.var_names in
  String.concat "\n" ([
@@ -98,10 +97,10 @@ let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
    ) else "# ";
   "#";
   "$" ^ p.label;
-  (match div with None -> "# no D" | Some div -> "D ("^string_of_int (measure_of_term div)^")"^ print ~l (div :> nf));
+  (match div with None -> "# D" | Some div -> "D " ^ aux_measure_terms div ^ print ~l (div :> nf));
   ]
-  @ List.map (fun t -> if t = convergent_dummy then "#C" else "C ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) conv
-  @ List.mapi (fun i t -> string_of_int i ^ " ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) ps
+  @ List.map (fun t -> if t = convergent_dummy then "# C" else "C " ^ aux_measure_terms t ^ print ~l (t :> nf)) conv
+  @ List.mapi (fun i t -> string_of_int i ^ " " ^ aux_measure_terms t ^ print ~l (t :> nf)) ps
   @ [""])
 ;;
 
@@ -208,7 +207,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
       let freshno,new_t,acc_new_ps =
        try
         expand_match (freshno,ps,acc_new_ps) t
-       with Pacman -> freshno,convergent_dummy,acc_new_ps
+       with Pacman | Lambda -> freshno,convergent_dummy,acc_new_ps
           | Bottom -> raise (Backtrack "Bottom in conv") in
       aux_conv ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv
 
@@ -257,7 +256,7 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
          let t = mk_match (`N i) orig bs_lift bs (args :> nf list) in
 (*prerr_endline ("NUOVO t:" ^ print (fst t :> nf) ^ " more_args=" ^ string_of_int (snd t));*)
           expand_match (freshno,acc_ps,acc_new_ps) t
-   | `Lam _ -> assert false (* algorithm invariant/loose typing *)
+   | `Lam _ -> raise Lambda (* assert false (* algorithm invariant/loose typing *) *)
    | `Bottom -> raise Bottom
    | `Pacman -> raise Pacman
    | #i_n_var as x ->
@@ -278,11 +277,11 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
  );
  let p = {p with sigma = sigma@[x,inst]} in
  let p = super_simplify p in
- prerr_endline (string_of_problem "instantiate" p);
  p
 ;;
 
-exception Dangerous
+exception TriggerMatchReduction of int;;
+exception Dangerous;;
 
 let arity_of arities hd =
  let pos,_,nargs = List.find (fun (_,hd',_) -> hd=hd') arities in
@@ -300,8 +299,8 @@ let rec dangerous arities showstoppers =
       (match t with
           `N _ -> List.iter (dangerous arities showstoppers) args
         | `Match _ as t -> dangerous arities showstoppers t ; List.iter (dangerous arities showstoppers) args
-        | `Var(x,_) -> dangerous_inert arities showstoppers x args num_more_args
-        | `I((x,_),args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) num_more_args
+        | `Var(x,_) -> dangerous_inert arities showstoppers x args 2
+        | `I((x,_),args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) 2
       )
   | `I((k,_),args) -> dangerous_inert arities showstoppers k (Listx.to_list args) 0
 
@@ -317,93 +316,126 @@ and dangerous_inert arities showstoppers k args more_args =
 (* cut & paste from above *)
 let rec dangerous_conv p arities showstoppers =
  function
-    `N _
+  | `N _
   | `Var _
   | `Lam _
-  | `Pacman -> []
-  | `Match(t,_,liftno,bs,args) ->
+  | `Pacman -> ()
+  | `Match(t,_,liftno,bs,args) -> (
       (* CSC: XXX partial dependency on the encoding *)
-      (match t with
-          `N _ -> concat_map (dangerous_conv p arities showstoppers) args
-        | `Match _ as t -> dangerous_conv p arities showstoppers t @ concat_map (dangerous_conv p arities showstoppers) args
+       try (match t with
+        | `N _ -> List.iter (dangerous_conv p arities showstoppers) args
+        | `Match _ as t -> dangerous_conv p arities showstoppers t; List.iter (dangerous_conv p arities showstoppers) args
         | `Var(x,_) -> dangerous_inert_conv p arities showstoppers x [] args 2
         | `I((x,_),args') -> dangerous_inert_conv p arities showstoppers x (Listx.to_list args') args 2
-      )
+        ) with TriggerMatchReduction x -> (
+           match Util.find_opt (fun (n, t) -> if hd_of (List.nth p.ps n) = Some x then Some t else None) !bs with
+            | None -> ()
+            | Some t -> (
+               match t with
+                | `Bottom -> raise Dangerous
+                | #nf_nob as t -> dangerous_conv p arities showstoppers t
+               )
+           )
+       )
   | `I((k,_),args) -> dangerous_inert_conv p arities showstoppers k (Listx.to_list args) [] 0
 
 and dangerous_inert_conv p arities showstoppers k args match_args more_args =
  let all_args = args @ match_args in
- let dangerous_args = concat_map (dangerous_conv p arities showstoppers) all_args in
+ List.iter (dangerous_conv p arities showstoppers) all_args;
  let all_args = (all_args :> nf list) in
- if dangerous_args = [] then (
- if List.mem k showstoppers then k :: concat_map free_vars all_args else
- try
-  let arity = arity_of arities k in
-prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var p.var_names k ^ " listlenargs=" ^ (string_of_int (List.length args)) ^ " more_args=" ^ string_of_int more_args);
-  if more_args > 0 (* match argument*) && List.length args = arity then []
-  else if List.length all_args + more_args > arity then k :: concat_map free_vars all_args else []
- with
-  Not_found -> []
- ) else k :: concat_map free_vars all_args
+ if List.mem k showstoppers then raise Dangerous else
+  try
+   let arity = arity_of arities k in
+(* prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var p.var_names k ^ " listlenargs=" ^ (string_of_int (List.length args)) ^ " more_args=" ^ string_of_int more_args); *)
+   if more_args > 0 (* match argument*) && List.length args = arity then raise (TriggerMatchReduction k)
+    else if List.length all_args + more_args > arity then raise Dangerous else ()
+  with
+   Not_found -> ()
 
 (* inefficient algorithm *)
-let rec edible ({div; conv; ps} as p) arities showstoppers =
- let rec aux showstoppers =
-  function
-     [] -> showstoppers
+let rec edible p arities showstoppers =
+ let rec aux f showstoppers tms = function
+   | [] -> showstoppers
    | x::xs when List.exists (fun y -> hd_of x = Some y) showstoppers ->
       (* se la testa di x e' uno show-stopper *)
       let new_showstoppers = sort_uniq (showstoppers @ free_vars (x :> nf)) in
       (* aggiungi tutte le variabili libere di x *)
       if List.length showstoppers <> List.length new_showstoppers then
-       aux new_showstoppers ps
+       aux f new_showstoppers tms tms
       else
-       aux showstoppers xs
+       aux f showstoppers tms xs
    | x::xs ->
       match hd_of x with
-         None -> aux showstoppers xs
+         None -> aux f showstoppers tms xs
        | Some h ->
           try
-           dangerous arities showstoppers (x : i_n_var :> nf_nob) ;
-           aux showstoppers xs
+           f showstoppers (x :> nf_nob) ;
+           aux f showstoppers tms xs
           with
            Dangerous ->
-            aux (sort_uniq (h::showstoppers)) ps in
-
- let showstoppers = sort_uniq (aux showstoppers ps) in
- let dangerous_conv =
-  List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in
-
-prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
-List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
-
- let showstoppers' = showstoppers @ List.concat dangerous_conv in
- let showstoppers' = sort_uniq (match div with
-  | None -> showstoppers'
-  | Some div ->
-    if List.exists ((=) (hd_of_i_var div)) showstoppers'
-    then showstoppers' @ free_vars (div :> nf) else showstoppers') in
- if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
+            aux f (sort_uniq (h::showstoppers)) tms tms
+  in
+   let showstoppers = sort_uniq (aux (dangerous arities) showstoppers p.ps p.ps) in
+   let dangerous_conv = sort_uniq (aux (dangerous_conv p arities) showstoppers p.conv p.conv) in
+
+    let showstoppers' = showstoppers @ dangerous_conv in
+    let showstoppers' = sort_uniq (match p.div with
+     | None -> showstoppers'
+     | Some div ->
+       if List.exists ((=) (hd_of_i_var div)) showstoppers'
+       then showstoppers' @ free_vars (div :> nf) else showstoppers') in
+    if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers'
 ;;
 
-let precompute_edible_data {ps; div} xs =
+let precompute_edible_data {ps; div} =
+ let heads = uniq (List.sort compare ((match div with None -> [] | Some h -> [hd_of_i_var h]) @ filter_map hd_of ps)) in
  let aux t = match t with `Var _ -> 0 | `I(_, args) -> Listx.length args | `N _ -> assert false in
- (fun l -> match div with
-  | None -> l
-  | Some div -> (-1, hd_of_i_var div, aux div) :: l)
-  (List.map (fun hd ->
-   let i, tm = Util.findi (fun y -> hd_of y = Some hd) ps in
-    i, hd, aux tm
-   ) xs)
+ List.map (fun hd ->
+  let i_tm = Util.find_alli (fun y -> hd_of y = Some hd) ps in
+  let i_tm = match div with Some div when hd_of_i_var div = hd -> (-1, (div :> i_n_var))::i_tm | _ -> i_tm in
+  let i_ar = List.map (fun (i,tm) -> i,aux tm) i_tm in
+  (* let's compute the minimal arity *)
+  match List.sort (fun (_,tm1) (_,tm2) -> compare tm1 tm2) i_ar with
+     [] -> assert false
+   | (i,ar)::_ -> i, hd, ar
+  ) heads
 ;;
 
+let rec dangerous_for_showstoppers_eat arities =
+ function
+    `N _
+  | `Var _
+  | `Lam _
+  | `Pacman -> []
+  | `Match(t,_,liftno,bs,args) ->
+      (* CSC: XXX partial dependency on the encoding *)
+      (match t with
+          `N _ -> []
+        | `Match _ as t -> dangerous_for_showstoppers_eat arities t
+        | `Var(x,_) -> dangerous_for_showstoppers_eat_inert arities x [] true
+        | `I((x,_),args') -> dangerous_for_showstoppers_eat_inert arities x (Listx.to_list args') true
+      ) @ List.concat (List.map (dangerous_for_showstoppers_eat arities ) args)
+  | `I((k,_),args) -> dangerous_for_showstoppers_eat_inert arities k (Listx.to_list args) false
+
+and dangerous_for_showstoppers_eat_inert arities k args in_match =
+ List.concat (List.map (dangerous_for_showstoppers_eat arities ) args) @
+ try
+  let arity = arity_of arities k in
+  if in_match && List.length args <> arity then [k]
+  else if List.length args > arity then [k]
+  else []
+ with
+  Not_found -> []
+
+let multiple_arities p arities =
+  List.concat (List.map (dangerous_for_showstoppers_eat arities) ((p.ps :> nf_nob list) @ (p.conv :> nf_nob list)))
+
 (** Returns (p, showstoppers_step, showstoppers_eat) where:
     - showstoppers_step are the heads occurring twice
       in the same discriminating set
     - showstoppers_eat are the heads in ps having different number
       of arguments *)
-let critical_showstoppers p =
-  let p = super_simplify p in
+let critical_showstoppers p arities =
   let hd_of_div = match p.div with None -> [] | Some t -> [hd_of_i_var t] in
   let showstoppers_step =
   concat_map (fun bs ->
@@ -414,42 +446,29 @@ let critical_showstoppers p =
      if List.exists (fun t -> [hd_of t] = List.map (fun x -> Some x) hd_of_div) p.conv
      then hd_of_div else [] in
   let showstoppers_step = sort_uniq showstoppers_step in
-  let showstoppers_eat =
-   let heads_and_arities =
-    List.sort (fun (k,_) (h,_) -> compare k h)
-     (filter_map (function `Var(k,_) -> Some (k,0) | `I((k,_),args) -> Some (k,Listx.length args) | _ -> None ) p.ps) in
-   let rec multiple_arities =
-    function
-       []
-     | [_] -> []
-     | (x,i)::(y,j)::tl when x = y && i <> j ->
-         x::multiple_arities tl
-     | _::tl -> multiple_arities tl in
-   multiple_arities heads_and_arities in
-
+  let showstoppers_eat = multiple_arities p arities in
   let showstoppers_eat = sort_uniq showstoppers_eat in
-  let showstoppers_eat = List.filter
-    (fun x -> not (List.mem x showstoppers_step))
-    showstoppers_eat in
-List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
-List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
+  let showstoppers_eat =
+   List.filter (fun x -> not (List.mem x showstoppers_step)) showstoppers_eat in
+prerr_endline ("DANGEROUS STEP: " ^ String.concat " " (List.map (string_of_var p.var_names) showstoppers_step));
+prerr_endline ("DANGEROUS EAT: " ^ String.concat " " (List.map (string_of_var p.var_names) showstoppers_eat));
   p, showstoppers_step, showstoppers_eat
   ;;
 
 let eat p =
-  let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p in
+  let p = super_simplify p in
+  let arities = precompute_edible_data p in
+  let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p arities in
   let showstoppers = showstoppers_step @ showstoppers_eat in
-  let heads = List.sort compare (filter_map hd_of ps) in
-  let arities = precompute_edible_data p (uniq heads) in
-  let inedible, showstoppers_conv = edible p arities showstoppers in
+  let inedible = edible p arities showstoppers in
+  prerr_endline ("showstoppers (in eat)" ^ String.concat " " (List.map (string_of_var p.var_names) inedible));
   let l = List.filter (fun (_,hd,_) -> not (List.mem hd inedible)) arities in
-  let p =
-  List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else
-   let v = `N pos in
+  let new_sigma = List.map (fun (pos,hd,nargs) ->
+   let v = if pos = -1 then `Bottom else `N pos in
    let inst = make_lams v nargs in
 prerr_endline ("# [INST_IN_EAT] eating: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
-   { p with sigma = p.sigma @ [hd,inst] }
-   ) p l in
+    hd,inst
+   ) l in
   (* to avoid applied numbers in safe positions that
      trigger assert failures subst_in_problem x inst p*)
  let ps =
@@ -459,32 +478,24 @@ prerr_endline ("# [INST_IN_EAT] eating: " ^ string_of_var p.var_names hd ^ " :=
     `N j
    with Not_found -> t
   ) ps in
- let p = match p.div with
-  | None -> p
-  | Some div ->
-   if List.mem (hd_of_i_var div) inedible
-   then p
-   else
-    let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in
-    let x = hd_of_i_var div in
-    let inst = make_lams `Bottom n in
-    subst_in_problem x inst p in
- let dangerous_conv = showstoppers_conv in
+(*let dangerous_conv = showstoppers_conv in
 prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
-List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
+List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv; *)
  let conv =
-   List.map (function s,t ->
+   List.map (function t ->
     try
-     if s <> [] then t else (
      (match t with | `Var _ -> raise Not_found | _ -> ());
-     let _ = List.find (fun h -> hd_of t = Some h) inedible in
-      t)
-    with Not_found -> match hd_of t with
-     | None -> assert (t = convergent_dummy); t
-     | Some h ->
-      prerr_endline ("FREEZING " ^ string_of_var p.var_names h);
-      convergent_dummy
-   ) (List.combine showstoppers_conv p.conv) in
+     let _ = List.find (fun h -> hd_of t = Some h) inedible in t
+    with Not_found -> (
+     (match hd_of t with
+      | None -> assert (t = convergent_dummy)
+      | Some h -> prerr_endline ("FREEZING " ^ string_of_var p.var_names h));
+     convergent_dummy)
+   ) p.conv in
+ let div =
+  match p.div with
+     None -> None
+   | Some div -> if List.mem (hd_of_i_var div) inedible then Some div else None in
  List.iter
   (fun bs ->
     bs :=
@@ -496,7 +507,10 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.
       ) !bs
   ) p.deltas ;
  let old_conv = p.conv in
- let p = { p with ps; conv } in
+ let p = { p with ps; conv; div } in
+ (* In case (match x ... with ...) and we are eating x,
+    so we need to substitute *)
+ let p = List.fold_left (fun p (x,inst) -> subst_in_problem x inst p) p new_sigma in
  if l <> [] || old_conv <> conv
   then prerr_endline (string_of_problem "eat" p);
  if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then
@@ -556,11 +570,13 @@ let compute_special_k tms =
  | `Bottom
  | `Pacman
  | `Var _ -> 0 in
- Listx.max (Listx.map (fun t -> max (aux 0 t) (aux' true t)) tms)
+ Listx.max (Listx.map (aux 0) tms) + Listx.max (Listx.map (aux' true) tms)
 ;;
 
 let choose_step p =
- let p, showstoppers_step, showstoppers_eat = critical_showstoppers p in
+ let p = super_simplify p in
+ let arities = precompute_edible_data p in
+ let p, showstoppers_step, showstoppers_eat = critical_showstoppers p arities in
  let x =
   match showstoppers_step, showstoppers_eat with
   | [], y::_ ->
@@ -582,51 +598,22 @@ let choose_step p =
       | x::_ ->
          prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var p.var_names x);
          x) in
-(* Strategy that  decreases the special_k to 0 first (round robin)
-1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
- let x =
-  try
-   match
-    hd_of (List.find (fun t ->
-     compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t > 0
-     ) (all_terms p))
-   with
-    | None -> assert false
-    | Some x ->
-       prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var p.var_names x);
-       x
-  with
-   Not_found ->
-    let arity_of_x = max_arity_tms x (all_terms p) in
-    assert (Util.option_get arity_of_x > 0);
-    x in
-(* Instantiate in decreasing order of compute_special_k
-1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s
-let x =
- try
-  (match hd_of (snd (List.hd (List.sort (fun c1 c2 -> - compare (fst c1) (fst c2)) (filter_map (function `I _ as t -> Some (compute_special_k (Listx.Nil (t :> nf)),t) | _ -> None) (all_terms p))))) with
-      None -> assert false
-    | Some x ->
-       prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
-       x)
- with
-  Not_found -> x
-in*)
  let arity_of_x = Util.option_get (max_arity_tms x (all_terms p)) in
  let safe_arity_of_x = safe_arity_of_var p x in
  x, min arity_of_x safe_arity_of_x
 ;;
 
 let rec auto_eat p =
- prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}";
+(* prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}"; *)
  let m = problem_measure p in
  let x, arity_of = choose_step p in
  first arity_of p x (fun p j ->
   let p' = instantiate p x j in
+  prerr_endline (string_of_problem "after instantiate" p');
   match eat p' with
   | `Finished p -> p
   | `Continue p ->
-      prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}";
+(* prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}"; *)
       let delta = problem_measure p - m in
       if delta >= 0
        then
@@ -757,23 +744,27 @@ let solve (p, todo) =
        Backtrack _ -> `Unseparable "backtrack"
 ;;
 
+let no_bombs_pacmans p =
+    not (List.exists (eta_subterm `Bottom) (p.ps@p.conv))
+ && not (List.exists (eta_subterm `Pacman) p.ps)
+ && Util.option_map (eta_subterm `Pacman) p.div <> Some true
+;;
+
 let check p =
- (* TODO check if there are duplicates in p.ps
-     before it was: ps = sort_uniq ~compare:eta_compare (ps :> nf list) *)
- (* FIXME what about initial fragments? *)
  if (let rec f = function
      | [] -> false
      | hd::tl -> List.exists (eta_eq hd) tl || f tl in
-   f p.ps)
+   f p.ps) (* FIXME what about initial fragments of numbers? *)
   then `CompleteUnseparable "ps contains duplicates"
  (* check if div occurs somewhere in ps@conv *)
  else if (match p.div with
   | None -> true
   | Some div -> not (List.exists (eta_subterm div) (p.ps@p.conv))
-  ) && false (* TODO no bombs && pacmans *)
+  ) && no_bombs_pacmans p
   then `CompleteSeparable "no bombs, pacmans and div"
- else if false (* TODO bombs or div fuori da lambda in ps@conv *)
-  then `CompleteUnseparable "bombs or div fuori da lambda in ps@conv"
+  (* il check seguente e' spostato nel parser e lancia un ParsingError *)
+ (* else if false (* TODO bombs or div fuori da lambda in ps@conv *)
+  then `CompleteUnseparable "bombs or div fuori da lambda in ps@conv" *)
  else if p.div = None
   then `CompleteSeparable "no div"
  else `Uncomplete