Code simplification + Bugfix

In case (match x ... with ...) and we are eating x,
 so we need to substitute
See problems/bugs1

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 5ff78661f5cd8377e8ee489cf09edafc1f0c4d94..44ca43b046058aff3b45e335f9d0232afc0c6294 100644 (file)
--- 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 (file)
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 (file)
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 (file)
index 0000000..43b3be5
--- /dev/null
+++ b/ocaml/problems/bugs2
@@ -0,0 +1,5 @@
+$! bugs 2\r
+# algorithm tries to step on z, but should first step on x, w\r
+D z PAC\r
+C x y PAC PAC\r
+N x (@ z) @\r