From eb8bb784b35d303a1c239f30008cba79f658f4b3 Mon Sep 17 00:00:00 2001 From: acondolu Date: Tue, 11 Jul 2017 14:00:34 +0200 Subject: [PATCH] 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. --- ocaml/lambda4.ml | 8 ++++++-- ocaml/num.ml | 9 +++++---- ocaml/num.mli | 1 + ocaml/problems.ml | 19 ++++++++++++++++++- 4 files changed, 30 insertions(+), 7 deletions(-) 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 ]));; -- 2.39.2