From 2dc40f471a59b3e192d5c9db14746292958315db Mon Sep 17 00:00:00 2001 From: acondolu Date: Mon, 24 Jul 2017 14:55:04 +0200 Subject: [PATCH] Added exception Lambda, which may be caught when a conv becomes a lambda --- ocaml/lambda4.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 -> -- 2.39.2