From a083188139e0ae7c4db8e6f0d7b7c913006fa148 Mon Sep 17 00:00:00 2001 From: Date: Mon, 26 Jun 2017 13:47:30 +0200 Subject: [PATCH] Problems pass, but still missing computation of arities of fresh applicative vars --- ocaml/lambda4.ml | 13 ++++++++----- ocaml/num.ml | 49 ++++++++++++++++++++++++++++------------------- ocaml/num.mli | 2 ++ ocaml/problems.ml | 3 ++- 4 files changed, 41 insertions(+), 26 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index f71f360..8a5cc37 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -448,8 +448,8 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l)) let instantiate p x n = (if hd_of_i_var (cast_to_i_var !bomb) = x then failwithProblem p ("BOMB (" ^ string_of_nf !bomb ^ ") cannot be instantiated!")); - (* ACL FIXME compute arity of x correctly below! *) - let arity_of_x = -666 in + 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 p,vars = make_fresh_vars p arities in @@ -481,7 +481,10 @@ let auto_instantiate (n,p) = | [], y::_ -> prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y | [], [] -> - let heads = List.sort compare (filter_map (fun t -> match t with `Var _ -> None | x -> hd_of x) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in + let heads = + List.sort compare (filter_map ( + 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 | x::_ -> @@ -494,7 +497,7 @@ 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) (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); @@ -757,7 +760,7 @@ let magic_conv ~div ~conv ~nums cmds = let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *) (* casts *) let div = option_map cast_to_i_var div in - let conv = List.map cast_to_i_n_var conv in + let conv = Util.filter_map (function #i_n_var as t -> Some (cast_to_i_n_var t) | _ -> None) conv in let tms = List.map cast_to_i_n_var tms in let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *) diff --git a/ocaml/num.ml b/ocaml/num.ml index 9d80313..614dde8 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -40,6 +40,12 @@ let hd_of = | `N _ -> None | `Match _ -> assert false +let arity_of_hd = +function + `I ((_,a),_) +| `Var(_,a) -> a +| _ -> 0 (* FIXME? *) + let lift m (t : nf) = let aux_var l (n, ar) = (if n < l then n else n+m), ar in let rec aux_i_num_var l = @@ -102,23 +108,9 @@ end (************ Pretty-printing ************************************) -let rec print ?(l=[]) = - function - `Var(n,_) -> print_name l n - | `N n -> string_of_int n - | `Match(t,_,bs_lift,bs,args) -> - "([" ^ print ~l (t :> nf) ^ - " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (lift bs_lift t)) !bs) ^ "] " ^ - String.concat " " (List.map (print ~l) args) ^ ")" - | `I((n,_),args) -> "(" ^ print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")" - | `Lam(_,nf) -> - let name = string_of_var (List.length l) in - "λ" ^ name ^ "." ^ print ~l:(name::l) (nf : nf) -;; - let rec string_of_term l = let rec string_of_term_w_pars l = function - | `Var(n,_) -> print_name l n + | `Var(n,ar) -> print_name l n ^ ":" ^ string_of_int ar | `N n -> string_of_int n | `I _ as t -> "(" ^ string_of_term_no_pars_app l (t :> nf) ^ ")" | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam l t ^ ")" @@ -127,7 +119,7 @@ let rec string_of_term l = " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift t)) !bs) ^ "] " ^ String.concat " " (List.map (string_of_term l) args) ^ ")" and string_of_term_no_pars_app l = function - | `I((n,_), args) -> print_name l n ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args)) + | `I((n,ar), args) -> print_name l n ^ ":" ^ string_of_int ar ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args)) | #nf as t -> string_of_term_w_pars l t and string_of_term_no_pars_lam l = function | `Lam(_,t) -> let name = string_of_var (List.length l) in @@ -230,12 +222,15 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool (************ Parsing ************************************) let parse' strs = + let fix_arity = function + | `I((n,_),args) -> `I((n,Listx.length args),args) + | _ -> assert false in let rec aux = function | Parser.Lam t -> `Lam (true, aux t) - | Parser.App (t1, t2) -> mk_app (aux t1) (aux t2) - | Parser.Var v -> `Var(v,-666) - in let (tms, free) = Parser.parse_many strs - in (List.map aux tms, free) + | Parser.App (t1, t2) -> fix_arity (mk_app (aux t1) (aux t2)) + | Parser.Var v -> `Var(v,0) in + let (tms, free) = Parser.parse_many strs in + List.map aux tms, free ;; (************** Algorithm(s) ************************) @@ -294,3 +289,17 @@ let rec eta_subterm sub t = ;; let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;; + + +let max_arity_tms n = + let aux_var l (m,a) = if n + l = m then a else -1 in + let rec aux l = function + | `Var v -> aux_var l v + | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms)) + | `Lam(_,t) -> aux (l+1) t + | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs)) + | `N _ -> -1 + and aux_tms l = + List.fold_left (fun acc t -> Pervasives.max acc (aux l t)) ~-1 in + fun tms -> aux_tms 0 (tms :> nf list) +;; diff --git a/ocaml/num.mli b/ocaml/num.mli index c1ad8f0..5631382 100644 --- a/ocaml/num.mli +++ b/ocaml/num.mli @@ -18,6 +18,7 @@ type i_n_var = nf i_n_var_ type i_num_var = nf i_num_var_ val hd_of_i_var : i_var -> int val hd_of : i_n_var -> int option +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 @@ -41,3 +42,4 @@ val parse' : string list -> nf list * string list 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 diff --git a/ocaml/problems.ml b/ocaml/problems.ml index a0ff453..e91c580 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -289,7 +289,8 @@ 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