From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 24 Jul 2017 12:55:04 +0000 (+0200)
Subject: Added exception Lambda, which may be caught when a conv becomes a lambda
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2dc40f471a59b3e192d5c9db14746292958315db;p=fireball-separation.git

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 21cd5ca..336f6b1 100644
--- 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 ->