From: acondolu <andrea.condoluci@unibo.it>
Date: Fri, 15 Sep 2017 13:17:00 +0000 (+0200)
Subject: git status! separation problem seems now undecidable git status!
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6a029ea76d520364189f500b029e110e3d42e5dd;p=fireball-separation.git

git status! separation problem seems now undecidable git status!
---

diff --git a/ocaml_new/lambda4.ml b/ocaml_new/lambda4.ml
index 95dec1f..08b7154 100644
--- 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 eda359a..c521afa 100644
--- 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 ae0bb44..1c6b12a 100644
--- a/ocaml_new/problems/1
+++ b/ocaml_new/problems/1
@@ -29,5 +29,12 @@ C y x
 
 $? 1 6
 D x x
+C y x
+  x z
+  y (x x)
+
+
+$? 1 7
+D x x
 C y x
   y (x x)
diff --git a/ocaml_new/problems/2 b/ocaml_new/problems/2
new file mode 100644
index 0000000..0f3d6b1
--- /dev/null
+++ b/ocaml_new/problems/2
@@ -0,0 +1,38 @@
+$! 2 1
+D x BOMB
+C x a
+
+$! 2 2
+D x _. BOT
+C x _._. BOT
+
+$! 2 3
+D x (_.PAC) y
+C x a z
+
+# qui mancano le proiezioni!!1!!!
+$? 2 4
+D x (_.  BOT) a a a a a a
+C x (_._.BOT) a a a a a a
+
+# qui mancano le `proiezioni`
+$? 2.5
+D x (y y)
+C x BOMB z
+
+$? 2.5'
+D x (_. y y)
+C x (_. BOMB) z
+
+???????????????
+D x a1 a2 a3
+C y x a
+C y (_._.BOMB)
+C ?????????????
+???????????????
+
+$? 2.6
+D x (_.      a) b cc dd ee
+C x (_.      a) c cc dd ee
+  x (_.      d) b cc dd ee
+  x (_._._.BOT) b cc dd ee