git status! separation problem seems now undecidable git status!

diff --git a/ocaml_new/lambda4.ml b/ocaml_new/lambda4.ml
index 95dec1f94b22220f1dd2eaec5ca60325ec8de363..08b71541362f145841600c44afd277b7786ed246 100644 (file)
--- a/ocaml_new/lambda4.ml
+++ b/ocaml_new/lambda4.ml
@@ -39,16 +39,16 @@ let string_of_term p t = print ~l:p.var_names (t :> nf);;
 
 
 let first args p var f =
- let rec aux = function
+ let rec aux k = function
  | [] ->
    raise (Backtrack ("no more alternatives for " ^ string_of_var p.var_names var))
- | i::is -> try
-    f p i
+ | i::is as ii -> try
+    f p i k
    with Backtrack s ->
 prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ ");
-prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1));
-     aux is
- in aux args
+(* prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1)); *)
+     if k = 0 then aux p.initialSpecialK is else aux (k-1) ii
+ in aux p.initialSpecialK args
 
 let all_terms p = p.div :: p.conv ;;
 
@@ -107,14 +107,13 @@ let fixpoint f =
 
 let subst_in_problem x inst ({div; conv} as p) =
 prerr_endline ("# INST0: " ^ string_of_var p.var_names x ^ " := " ^ string_of_term p inst);
- let aux t = match t with
- | #i_var as t -> t
- | `Lam _ | `Bottom | `Pacman -> assert false (* ??? *) in
- let div = (aux ++ (subst false false x inst)) (div :> nf) in
+ let div = subst false false x inst (div :> nf) in
  let conv = List.map (subst false false x inst) (conv :> nf list) in
- let conv = List.filter (function `Lam _ -> false | _ -> true) conv in
- let conv = List.map aux conv in
- {p with div; conv}
+ let conv = Util.filter_map (function `Lam _ | `Pacman -> None | `Bottom -> raise (Backtrack "bottom in conv") | #i_var as t -> Some t) conv in
+ match div with
+  | `Lam _ | `Pacman | `Var _ -> raise (Backtrack "lam in div")
+  | `Bottom -> `Finished p
+  | `I _ as div -> `Continue {p with div; conv}
 ;;
 
 exception Dangerous;;
@@ -356,8 +355,8 @@ let safe_arity_of_var p x =
  List.fold_left (fun acc t -> Pervasives.min acc (aux t)) max_int tms
 ;; *)
 
-let instantiate p x perm =
- let n = (prerr_endline ("WARNING: using constant initialSpecialK=" ^ string_of_int p.initialSpecialK)); p.initialSpecialK in
+let instantiate p x perm n =
+ (* let n = (prerr_endline ("WARNING: using constant initialSpecialK=" ^ string_of_int p.initialSpecialK)); p.initialSpecialK in *)
  let arities = Array.to_list (Array.make (n+1) min_int) in
  let p,vars = make_fresh_vars p arities in
  (* manual lifting of vars by perm in next line *)
@@ -437,7 +436,7 @@ let eat p =
      if x = hd then
       if Listx.length args' >= n then
        (let diff = intersect args args' in
-       if diff <> [] then raise (Difference diff));
+       raise (if diff = [] then Backtrack "div in conv" else Difference diff));
      List.iter aux ((Listx.to_list args') :> nf list) in
  try
   List.iter aux (p.conv :> nf list) ;
@@ -448,21 +447,23 @@ let eat p =
 
 let rec auto_eat p =
  prerr_endline (string_of_problem "auto_eat" p);
- prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}";
+ (* prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}"; *)
  match eat p with
  | `Finished p -> prerr_endline "finished"; p
  | `Continue (x,positions) ->
  let m = problem_measure p in
- first positions p x (fun p j ->
-  let p = instantiate p x j in
-  prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}";
+ first positions p x (fun p j k ->
+  match instantiate p x j k with
+  `Continue p ->
+  (* prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}"; *)
   let delta = problem_measure p - m in
   if delta >= 0
    then
     (prerr_endline
     ("Measure did not decrease (+=" ^ string_of_int delta ^ ")"))
    else prerr_endline ("$ Measure decreased: " ^ string_of_int delta);
-   auto_eat p)
+   auto_eat p
+  | `Finished p -> p)
 ;;
 
 (******************************************************************************)

diff --git a/ocaml_new/problems.ml b/ocaml_new/problems.ml
index eda359ae00d08dc3b92c19eba633c44d1bec1ee1..c521afa7808f3171f960f77c7e38965b24d2e33d 100644 (file)
--- a/ocaml_new/problems.ml
+++ b/ocaml_new/problems.ml
@@ -23,6 +23,7 @@ let assert_depends x =
  match solve x with
  | _, `Unseparable s when c = "!" ->
     failwith ("assert_depends: unseparable because: " ^ s ^ ".")
+ | _, `Unseparable _ -> prerr_endline "Problem failed correctly."
  | _, `Separable _  when c = "?" ->
     failwith ("assert_depends: separable.")
  | _ -> ()

diff --git a/ocaml_new/problems/1 b/ocaml_new/problems/1
index ae0bb441b0837c567801789bb40a35b4fac47f90..1c6b12a8b4b70aa6c3dabd69b42079ec326ba737 100644 (file)
--- a/ocaml_new/problems/1
+++ b/ocaml_new/problems/1
@@ -29,5 +29,12 @@ C y x
 \r
 $? 1 6\r
 D x x\r
+C y x\r
+  x z\r
+  y (x x)\r
+\r
+\r
+$? 1 7\r
+D x x\r
 C y x\r
   y (x x)\r

diff --git a/ocaml_new/problems/2 b/ocaml_new/problems/2
new file mode 100644 (file)
index 0000000..0f3d6b1
--- /dev/null
+++ b/ocaml_new/problems/2
@@ -0,0 +1,38 @@
+$! 2 1\r
+D x BOMB\r
+C x a\r
+\r
+$! 2 2\r
+D x _. BOT\r
+C x _._. BOT\r
+\r
+$! 2 3\r
+D x (_.PAC) y\r
+C x a z\r
+\r
+# qui mancano le proiezioni!!1!!!\r
+$? 2 4\r
+D x (_.  BOT) a a a a a a\r
+C x (_._.BOT) a a a a a a\r
+\r
+# qui mancano le `proiezioni`\r
+$? 2.5\r
+D x (y y)\r
+C x BOMB z\r
+\r
+$? 2.5'\r
+D x (_. y y)\r
+C x (_. BOMB) z\r
+\r
+???????????????\r
+D x a1 a2 a3\r
+C y x a\r
+C y (_._.BOMB)\r
+C ?????????????\r
+???????????????\r
+\r
+$? 2.6\r
+D x (_.      a) b cc dd ee\r
+C x (_.      a) c cc dd ee\r
+  x (_.      d) b cc dd ee\r
+  x (_._._.BOT) b cc dd ee\r