From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 11 Jul 2017 12:00:34 +0000 (+0200)
Subject: Fix: conv : x:min_int (.... y:1 ...)  y was not considered for stepping
X-Git-Tag: weak-reduction-separation~61
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eb8bb784b35d303a1c239f30008cba79f658f4b3;p=fireball-separation.git

Fix: conv : x:min_int (.... y:1 ...)  y was not considered for stepping

When no other choice is available, step on any >0 variable that occurs in
a conv.
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 35f03ca..570691e 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -499,8 +499,12 @@ let auto_instantiate (n,p) =
        fun t -> match t with `Var _ -> None | x -> if arity_of_hd x <= 0 then None else hd_of x
       ) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
      (match heads with
-         [] ->
-         assert false
+         [] -> (
+          try
+           fst (List.find (((<) 0) ++ snd) (concat_map free_vars' (p.conv :> nf list)))
+          with
+           Not_found -> assert false
+          )
        | x::_ ->
           prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x);
           x)
diff --git a/ocaml/num.ml b/ocaml/num.ml
index d003985..85a2bfa 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -70,12 +70,12 @@ let rec make_lams t =
  | n when n > 0 -> `Lam (false, lift 1 (make_lams t (n-1)))
  | _ -> assert false
 
-let free_vars =
+let free_vars' =
  let rec aux n = function
     `N _ -> []
-  | `Var(x,_) -> if x < n then [] else [x-n]
-  | `I((x,_),args) ->
-      (if x < n then [] else [x-n]) @
+  | `Var(x,ar) -> if x < n then [] else [(x-n,ar)]
+  | `I((x,ar),args) ->
+      (if x < n then [] else [(x-n,ar)]) @
       List.concat (List.map (aux n) (Listx.to_list args))
   | `Lam(_,t) -> aux (n+1) t
   | `Match(t,_,liftno,bs,args) ->
@@ -84,6 +84,7 @@ let free_vars =
       List.concat (List.map (aux n) args)
   in aux 0
 ;;
+let free_vars = (List.map fst) ++ free_vars';;
 
 module ToScott =
 struct
diff --git a/ocaml/num.mli b/ocaml/num.mli
index 8c2ac2b..9cf81cc 100644
--- a/ocaml/num.mli
+++ b/ocaml/num.mli
@@ -22,6 +22,7 @@ val arity_of_hd : i_n_var -> int
 (* put t under n lambdas, lifting t accordingtly *)
 val make_lams : nf -> int -> nf
 val lift : int -> nf -> nf
+val free_vars' : nf -> var list
 val free_vars : nf -> int list
 module ToScott :
   sig
diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 7f6f76c..2a99a5c 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -318,6 +318,22 @@ let n2 () = magic_conv
 ] ["*"]
 ;;
 
+let n3 () = magic_conv
+(Some"b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n))")
+[
+"b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) (k. l. l (m. l))";
+"c d e (f i) (e e) (g e) (k. l. e) (k. c (g (k (l. i)))) (c d e (k. k))";
+"f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (c d e (f i) (e e) (f (k. h))) (g e (b (k. i)) (e e (e e)))";
+"f (k. f) (k. f) (k. e) (c d e (f i) (e e) (g e)) (k. e e) (k. l. m. e) (k. e)";
+"g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f)";
+][
+"b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) a";
+"c d e (f i) (e e) (g e) (b (g (k. e e)) (k. c (g (h (l. i))) (l. f l))) (k. f (l. f) (l. f)) a";
+"e e (k. k d e (l. l)) (g e) (c d e b (e e (c (c d e f)))) (d (e e (k. k d e (l. l))) (k. k i)) (k. i (l. c (c d e f))) (k. h) a";
+"f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) a";
+"g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f) (f (k. f) (k. f) (k. l. l) (c (k. i (l. c (c d e f))))) a";
+] ["*"];;
+
 (* main ([p34]);; *)
 
 main ([
@@ -340,5 +356,6 @@ main ([
  m2 ;
 ] @ [
  n1 ;
- n2
+ n2 ;
+ n3
 ]));;