From 941130623a83c8c3f7e4afcce4189f12c2bd18e0 Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 13 Jul 2017 11:00:36 +0200 Subject: [PATCH] Fixed try in aux_conv + Added test in pure for divergence of conv --- ocaml/lambda4.ml | 29 ++++++++++++++++++----------- 1 file changed, 18 insertions(+), 11 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 583d99e..1be77d1 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -10,6 +10,8 @@ open Num *) let num_more_args = 2;; +let convergent_dummy = `N(-1);; + type discriminating_set = (int * nf) list;; type problem = @@ -35,9 +37,8 @@ let first bound p var f = if i > bound then raise (Backtrack ("no more alternatives for " ^ string_of_var var)) else - try(try + try f p i - with Pacman | Bottom -> raise (Backtrack "Pacman/Bottom")) with Backtrack s -> prerr_endline ("!!BACKTRACK!! " ^ s); List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ; @@ -79,7 +80,7 @@ let string_of_problem label ({freshno; div; conv; ps; deltas} as p) = ^"(* DIVERGENT *)" ^ nl ^" "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\")") ^ nl ^" (* CONVERGENT *) [" ^ nl ^ " " - ^ String.concat "\n " (List.map (fun t -> "(* _ *) " ^ (if t = `N (-1) then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^ + ^ String.concat "\n " (List.map (fun t -> "(* _ *) " ^ (if t = convergent_dummy then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^ (if conv = [] then "" else nl) ^ "] (* NUMERIC *) [" ^ nl ^ " " ^ String.concat "\n " (List.mapi (fun i t -> " (* "^ string_of_int i ^" *) \"" ^ print ~l (t :> nf) ^ "\";") ps) @@ -168,7 +169,9 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) let t = subst false false x inst (t :> nf) in (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) let freshno,new_t,acc_new_ps = - expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t + try + expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t + with Pacman | Bottom -> raise (Backtrack "Pacman/Bottom in ps") in aux_ps (freshno,acc_ps@[new_t],acc_new_ps) todo_ps @@ -178,11 +181,13 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) | [] -> acc | t::todo_conv -> (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) - let t = try - subst false false x inst (t :> nf) - with Pacman -> `N(-1) in (* DUMMY CONVERGENT *) + let t = subst false false x inst (t :> nf) in (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) - let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in + let freshno,new_t,acc_new_ps = + try + expand_match (freshno,ps,acc_new_ps) t + with Pacman -> 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 (* cut&paste from aux' above *) @@ -195,6 +200,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in freshno,Some(cast_to_i_var new_t),acc_new_ps with Bottom -> freshno, None, acc_new_ps + | Pacman -> raise (Backtrack "Pacman in div") and expand_match ((freshno,acc_ps,acc_new_ps) as acc) t = match t with @@ -444,10 +450,10 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l)) let _ = List.find (fun h -> hd_of t = Some h) showstoppers in t) with Not_found -> match hd_of t with - | None -> assert (t = `N ~-1); t + | None -> assert (t = convergent_dummy); t | Some h -> prerr_endline ("FREEZING " ^ string_of_var h); - `N ~-1 (* convergent dummy*) + convergent_dummy ) (List.combine showstoppers_conv p.conv) in List.iter (fun bs -> @@ -758,7 +764,8 @@ in List.iter (fun n -> prerr_endline ("_::: " ^ (Pure.print n)); let t = Pure.mwhd (e',n,[]) in - prerr_endline ("_:: " ^ (Pure.print t)) + prerr_endline ("_:: " ^ (Pure.print t)); + assert (t <> Pure.B) ) conv ; List.iteri (fun i n -> prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n)); -- 2.39.2