From eaa828c95315dcd1af183850b17fdd800661bc04 Mon Sep 17 00:00:00 2001 From: acondolu Date: Tue, 25 Jul 2017 13:43:18 +0200 Subject: [PATCH] Code simplification + Bugfix In case (match x ... with ...) and we are eating x, so we need to substitute See problems/bugs1 --- ocaml/lambda4.ml | 51 ++++++++++++++++++-------------------------- ocaml/problems/bugs | 10 --------- ocaml/problems/bugs1 | 16 ++++++++++++++ ocaml/problems/bugs2 | 5 +++++ 4 files changed, 42 insertions(+), 40 deletions(-) delete mode 100644 ocaml/problems/bugs create mode 100644 ocaml/problems/bugs1 create mode 100644 ocaml/problems/bugs2 diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 5ff7866..44ca43b 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -277,7 +277,6 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif ); let p = {p with sigma = sigma@[x,inst]} in let p = super_simplify p in - prerr_endline (string_of_problem "instantiate" p); p ;; @@ -379,8 +378,8 @@ let rec edible p arities showstoppers = let showstoppers = sort_uniq (aux (dangerous arities) showstoppers p.ps p.ps) in let dangerous_conv = sort_uniq (aux (dangerous_conv p arities) showstoppers p.conv p.conv) in -(* prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv)); -List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv; *) +prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv)); +prerr_endline (String.concat " " (List.map (string_of_var p.var_names) dangerous_conv)); let showstoppers' = showstoppers @ dangerous_conv in let showstoppers' = sort_uniq (match p.div with @@ -388,7 +387,7 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p. | Some div -> if List.exists ((=) (hd_of_i_var div)) showstoppers' then showstoppers' @ free_vars (div :> nf) else showstoppers') in - if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv + if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers' ;; let precompute_edible_data {ps; div} xs = @@ -446,15 +445,15 @@ let eat p = 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, showstoppers_conv = edible p arities showstoppers 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 - let p = - List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else - let v = `N pos in + let new_sigma = List.map (fun (pos,hd,nargs) -> + let v = if pos = -1 then `Bottom else `N pos in let inst = make_lams v nargs in prerr_endline ("# [INST_IN_EAT] eating: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst); - { p with sigma = p.sigma @ [hd,inst] } - ) p l in + hd,inst + ) l in (* to avoid applied numbers in safe positions that trigger assert failures subst_in_problem x inst p*) let ps = @@ -464,31 +463,19 @@ prerr_endline ("# [INST_IN_EAT] eating: " ^ string_of_var p.var_names hd ^ " := `N j with Not_found -> t ) ps in - let p = match p.div with - | None -> p - | Some div -> - if List.mem (hd_of_i_var div) inedible - then p - else - let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in - let x = hd_of_i_var div in - let inst = make_lams `Bottom n in - subst_in_problem x inst p in (*let dangerous_conv = showstoppers_conv in prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv)); List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv; *) let conv = List.map (function t -> try - if let hd = hd_of t in hd <> None && not (List.mem (Util.option_get hd) showstoppers_conv) then t else ( (match t with | `Var _ -> raise Not_found | _ -> ()); - let _ = List.find (fun h -> hd_of t = Some h) inedible in - t) - with Not_found -> match hd_of t with - | None -> assert (t = convergent_dummy); t - | Some h -> - prerr_endline ("FREEZING " ^ string_of_var p.var_names h); - convergent_dummy + let _ = List.find (fun h -> hd_of t = Some h) inedible in t + with Not_found -> ( + (match hd_of t with + | None -> assert (t = convergent_dummy) + | Some h -> prerr_endline ("FREEZING " ^ string_of_var p.var_names h)); + convergent_dummy) ) p.conv in List.iter (fun bs -> @@ -502,6 +489,9 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p. ) p.deltas ; let old_conv = p.conv in let p = { p with ps; conv } 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 if l <> [] || old_conv <> conv then prerr_endline (string_of_problem "eat" p); if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then @@ -593,15 +583,16 @@ let choose_step p = ;; let rec auto_eat p = - prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}"; +(* prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}"; *) let m = problem_measure p in let x, arity_of = choose_step p in first arity_of p x (fun p j -> let p' = instantiate p x j in + prerr_endline (string_of_problem "after instantiate" p'); match eat p' with | `Finished p -> p | `Continue p -> - prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}"; +(* prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}"; *) let delta = problem_measure p - m in if delta >= 0 then diff --git a/ocaml/problems/bugs b/ocaml/problems/bugs deleted file mode 100644 index 610b6b8..0000000 --- a/ocaml/problems/bugs +++ /dev/null @@ -1,10 +0,0 @@ -$! bugs 1 -# bug with eating firing reduction of matches -D z (_. (v y)) -C u (z (_. (v x))) - -$! bugs 2 -# algorithm tries to eat z, but should first step on x, w -D z PAC -C x y PAC PAC -N x (w z) Z diff --git a/ocaml/problems/bugs1 b/ocaml/problems/bugs1 new file mode 100644 index 0000000..dece410 --- /dev/null +++ b/ocaml/problems/bugs1 @@ -0,0 +1,16 @@ +# + $! bugs 1 + # bug with eating firing reduction of matches + D z (_. (v x1 x2)) (_. (v y1 y2)) + C u (z (_. (v xx1 x2)) (_. (v yy1 y2))) + + $! bugs 1'' + # bug with eating firing reduction of matches + D z (_. (v y)) (_. vv yy) + C z (_. (v y)) B + C u (z (_. (v x)) (_. vv xx)) + +$! bugs 1 +# bug with eating firing reduction of matches +D z (_. (v y)) +C u (z (_. (v x))) diff --git a/ocaml/problems/bugs2 b/ocaml/problems/bugs2 new file mode 100644 index 0000000..43b3be5 --- /dev/null +++ b/ocaml/problems/bugs2 @@ -0,0 +1,5 @@ +$! bugs 2 +# algorithm tries to step on z, but should first step on x, w +D z PAC +C x y PAC PAC +N x (@ z) @ -- 2.39.2