Added exception Lambda, which may be caught when a conv becomes a lambda

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 21cd5cad24220009184b0e5b5e8b4e1784e372bb..336f6b15286c380227626c07db772733738f76dd 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -6,6 +6,7 @@ open Num
 (* exceptions *)
 exception Pacman
 exception Bottom
+exception Lambda
 exception Backtrack of string
 
 (*
@@ -208,7 +209,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 +258,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 ->