From 6d9e673e3a6896f487988d897f927d07104d6a73 Mon Sep 17 00:00:00 2001 From: acondolu Date: Tue, 25 Jul 2017 17:16:57 +0200 Subject: [PATCH] Code for critical eat reimplemented x is now critical eat iff it is the head of a num and it occurs unprotected in other numbers or in divergent terms where unprotected means - as the scrutinee of a match, with wrong arity - everywhere else with too great arity The new definition fixes problems/bugs2 (renamed to problems/bomb) --- ocaml/lambda4.ml | 86 ++++++++++++++++++++++------------ ocaml/problems/{bugs2 => bomb} | 0 ocaml/problems/q | 4 ++ ocaml/util.ml | 8 ++++ ocaml/util.mli | 1 + 5 files changed, 68 insertions(+), 31 deletions(-) rename ocaml/problems/{bugs2 => bomb} (100%) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 6a534cd..82d5046 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -387,24 +387,55 @@ let rec edible p arities showstoppers = 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 -> @@ -415,33 +446,20 @@ 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 + 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 = 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 @@ -474,6 +492,10 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p. | 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 := @@ -485,7 +507,7 @@ 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 @@ -552,7 +574,9 @@ let compute_special_k 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::_ -> diff --git a/ocaml/problems/bugs2 b/ocaml/problems/bomb similarity index 100% rename from ocaml/problems/bugs2 rename to ocaml/problems/bomb diff --git a/ocaml/problems/q b/ocaml/problems/q index a641409..89b9493 100644 --- a/ocaml/problems/q +++ b/ocaml/problems/q @@ -64,3 +64,7 @@ N b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b ( b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. m. n. o. p. o) (e (f g) (k. g) (c f) (k. i) f) Z b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b) Z e (f g) (k. g) (c f) (k. e) (k. b (l. c)) (c f (k. b (l. c)) (k. l. b (m. k))) (k. b (l. k)) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e))) Z + +$! q11 +D b (k. c) d z (b (k. c) (k. e)) +N b (k. c) d e diff --git a/ocaml/util.ml b/ocaml/util.ml index a87b96f..472c4cc 100644 --- a/ocaml/util.ml +++ b/ocaml/util.ml @@ -9,6 +9,14 @@ let findi p = in aux 0 ;; +let find_alli p = + let rec aux n = function + | [] -> [] + | x::xs when p x -> (n,x)::aux (n+1) xs + | _::xs -> aux (n+1) xs + in aux 0 +;; + let option_map f = function | None -> None | Some x -> Some (f x) diff --git a/ocaml/util.mli b/ocaml/util.mli index 96f03ed..d366c81 100644 --- a/ocaml/util.mli +++ b/ocaml/util.mli @@ -1,5 +1,6 @@ val ( ++ ) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b val findi : ('a -> bool) -> 'a list -> (int * 'a) +val find_alli : ('a -> bool) -> 'a list -> (int * 'a) list val option_map : ('a -> 'b) -> 'a option -> 'b option val option_get : ('a option) -> 'a val find_opt : ('a -> 'b option) -> 'a list -> 'b option -- 2.39.2