From edc8a9dacfdf59bc23570756f7d346f9cd28ae6b Mon Sep 17 00:00:00 2001 From: Date: Tue, 27 Jun 2017 15:16:43 +0200 Subject: [PATCH] still stepping on negative variables --- ocaml/lambda4.ml | 9 ++++++--- ocaml/listx.ml | 5 ++++- ocaml/listx.mli | 1 + ocaml/num.ml | 48 ++++++++++++++++++++++++++++++++++++++++++----- ocaml/num.mli | 2 ++ ocaml/problems.ml | 3 +-- 6 files changed, 57 insertions(+), 11 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 8a5cc37..c627151 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -451,7 +451,8 @@ let instantiate p x n = let arity_of_x = max_arity_tms x (all_terms p) in (if arity_of_x < 0 then failwithProblem p "step on a var of negative arity"); (* AC: FIXME compute arities correctly below! *) - let arities = Array.to_list (Array.make (n+1) 0) in + let arities = Num.compute_arities x (n+1) (all_terms p :> nf list) in + (* let arities = Array.to_list (Array.make (n+1) 0) in *) let p,vars = make_fresh_vars p arities in (* let p,zero = make_fresh_var p in *) (* let zero = Listx.Nil zero in *) @@ -497,7 +498,9 @@ let auto_instantiate (n,p) = 1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *) let x = try - match hd_of (List.find (fun t -> compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t >= 0) (all_terms p)) with + match hd_of (List.find (fun t -> + compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t >= 0 + ) (all_terms p)) with None -> assert false | Some x -> prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x); @@ -733,7 +736,7 @@ in (********************** problems *******************) -let zero = `Var(0,-1);; +let zero = `Var(0,0);; let append_zero = function diff --git a/ocaml/listx.ml b/ocaml/listx.ml index ecc8a92..821e281 100644 --- a/ocaml/listx.ml +++ b/ocaml/listx.ml @@ -56,6 +56,10 @@ let rec max = | Nil x -> x | Cons (x, l) -> Pervasives.max x (max l) +let rec last = + function + | Nil x -> x + | Cons (_, l) -> last l (* let rec nth i l = match l, i with | Cons (x, _), 1 -> x @@ -65,4 +69,3 @@ let rec nth i l = match l, i with | Nil _, _ -> raise (Invalid_argument "Listx.nth") ;; *) - diff --git a/ocaml/listx.mli b/ocaml/listx.mli index 97226ae..a43bc4e 100644 --- a/ocaml/listx.mli +++ b/ocaml/listx.mli @@ -9,3 +9,4 @@ val to_list : 'a listx -> 'a list val from_list : 'a list -> 'a listx val split_nth : int -> 'a listx -> 'a list val max : 'a listx -> 'a +val last : 'a listx -> 'a diff --git a/ocaml/num.ml b/ocaml/num.ml index 614dde8..81bb1da 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -157,6 +157,13 @@ let cast_to_i_num_var = prerr_endline (print (t :> nf)); assert false (* algorithm failed *) +let set_arity arity = function +| `Var(n,_) -> `Var(n,arity) +| `Lam(false, `N _) +| `Lam(false, `Lam _) as t -> t +| `Lam(false, `Match(t,(n,ar),bs_lift,bs,args)) -> `Lam(false, `Match(t,(n,arity),bs_lift,bs,args)) +| _ -> assert false + let rec mk_app (h : nf) (arg : nf) = (*let res =*) match h with @@ -174,29 +181,34 @@ and mk_appl h args = and mk_appx h args = Listx.fold_left mk_app h args -and mk_match t ar bs_lift bs args = +and mk_match t (n,ar) bs_lift bs args = (*prerr_endline ("MK_MATCH: ([" ^ print t ^ "] " ^ String.concat " " (Listx.to_list (Listx.map (fun (n,t) -> string_of_int n ^ " => " ^ print t) bs)) ^ ") " ^ String.concat " " (List.map print args));*) match t with `N m -> (try let h = List.assoc m !bs in + let h = set_arity (ar-1) h in let h = lift bs_lift h in mk_appl h args with Not_found -> - `Match (t,ar,bs_lift,bs,args)) - | `I _ | `Var _ | `Match _ -> `Match(t,ar,bs_lift,bs,args) + `Match (t,(n,ar),bs_lift,bs,args)) + | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args) and subst delift_by_one what (with_what : nf) (where : nf) = + let aux_propagate_arity ar = function + | `Lam(false,`Match(`I(v,args),(x,_),liftno,bs,args')) -> + `Lam(false,`Match(`I(v,args),(x,ar),liftno,bs,args')) + | _ as t -> t in let rec aux_i_num_var l = function `I((n,ar),args) -> if n = what + l then - mk_appx (lift l with_what) (Listx.map (aux l) args) + mk_appx (lift l (aux_propagate_arity ar with_what)) (Listx.map (aux l) args) else `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args) | `Var(n,ar) -> if n = what + l then - lift l with_what + lift l (aux_propagate_arity ar with_what) else `Var((if delift_by_one && n >= l then n-1 else n), ar) | `N _ as x -> x @@ -303,3 +315,29 @@ let max_arity_tms n = List.fold_left (fun acc t -> Pervasives.max acc (aux l t)) ~-1 in fun tms -> aux_tms 0 (tms :> nf list) ;; + +let get_first_args var = +let rec aux l = function +| `Lam(_,t) -> aux (l+1) t +| `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args +| `I((n,_), args) -> if n = var + l then [Listx.last args] else [] +| `N _ +| `Var _ -> [] +in aux 0 +;; + +let compute_arities m = + let rec aux n tms = + if n = 0 + then [] + else + let tms = Util.filter_map (function `Lam(_,t) -> Some t | _ -> None ) tms in + let arity = max 0 (max_arity_tms (m-n) tms) in (* FIXME: 0 or -1 ??? *) + arity :: (aux (n-1) tms) + in fun tms -> List.rev (aux m tms) +;; + +let compute_arities var special_k all_tms = + let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in + compute_arities special_k tms +;; diff --git a/ocaml/num.mli b/ocaml/num.mli index 5631382..e06a821 100644 --- a/ocaml/num.mli +++ b/ocaml/num.mli @@ -33,6 +33,7 @@ val string_of_nf : [ string val cast_to_i_var : [< nf > `I `Var] -> i_var val cast_to_i_n_var : [< nf > `I `N `Var] -> i_n_var val cast_to_i_num_var : [< nf > `I `N `Match `Var] -> i_num_var +val set_arity : int -> nf -> nf val mk_app : nf -> nf -> nf val mk_appl : nf -> nf list -> nf val mk_appx : nf -> nf Listx.listx -> nf @@ -43,3 +44,4 @@ val eta_compare : nf -> nf -> int val eta_eq : [< nf ] -> [< nf ] -> bool val eta_subterm : [< nf ] -> [< nf ] -> bool val max_arity_tms : int -> [< nf] list -> int +val compute_arities : int -> int -> nf list -> int list diff --git a/ocaml/problems.ml b/ocaml/problems.ml index e91c580..a0ff453 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -289,8 +289,7 @@ main ([ (* p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ; p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ; p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ; p34 ; p35 ; p36 ; p37 ; *) p24 ; p25 ; ] @ List.map ((|>) ()) [ - q1 ; q2; q3; q4 ; q5 ; - q6 ; + q1 ; q2; q3; q4 ; q5 ; q6 ; (* q7 ; *) q8 ; q9 ; -- 2.39.2