From e1177d88d7ff54d6cb16d711103c5c71aaccdcc6 Mon Sep 17 00:00:00 2001 From: acondolu Date: Wed, 12 Jul 2017 18:39:03 +0200 Subject: [PATCH] Added new (passing) problem with a bomb (o1) --- ocaml/lambda4.ml | 52 ++++++++++++++++++++++++----------------------- ocaml/num.ml | 37 +++++++++++++++++++++++---------- ocaml/num.mli | 2 +- ocaml/problems.ml | 14 ++++++++++--- 4 files changed, 65 insertions(+), 40 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 821da4c..927cfe6 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -26,6 +26,26 @@ type problem = ; trail: discriminating_set list list };; +exception Backtrack of string + +let first bound p var f = + let p = {p with trail = (List.map (!) p.deltas)::p.trail} in + let rec aux i = + if i > bound then + raise (Backtrack ("no more alternatives for " ^ string_of_var var)) + else + try + f p i + with + Backtrack s -> +prerr_endline ("!!BACKTRACK!! " ^ s); + List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ; +prerr_endline("Now trying var="^string_of_var var^" i="^string_of_int i); + aux (i+1) + in + aux 1 + + let all_terms p = (match p.div with None -> [] | Some t -> [(t :> i_n_var)]) @ p.conv @@ -54,14 +74,14 @@ let string_of_problem label ({freshno; div; conv; ps; deltas} as p) = let l = Array.to_list (Array.init (freshno + 1) string_of_var) in nl ^ "measure="^string_of_measure(problem_measure p)^" freshno = " ^ string_of_int freshno ^nl^"\b> DISCRIMINATING SETS (deltas)" - ^nl^deltas^(if deltas = "" then "" else nl) + ^nl^"(*"^deltas^(if deltas = "" then "" else "*)"^nl) ^"\b (* DIVERGENT *)" ^ nl ^" "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\" ") ^ nl ^"\b (* CONVERGENT *) [" ^ nl - ^ String.concat " " (List.map (fun t -> "_: " ^ (if t = `N (-1) then "_" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^ + ^ String.concat "\n " (List.map (fun t -> "(* _: *) " ^ (if t = `N (-1) then "PAC;" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^ (if conv = [] then "" else nl) - ^ "\b> NUMERIC" ^ nl - ^ String.concat "\n| " (List.mapi (fun i t -> string_of_int i ^ ": " ^ print ~l (t :> nf)) ps) + ^ "\b] (* NUMERIC *) [" ^ nl + ^ String.concat "\n " (List.mapi (fun i t -> " (* "^ string_of_int i ^" *) \"" ^ print ~l (t :> nf) ^ "\";") ps) ^ nl ;; @@ -90,7 +110,7 @@ let simple_expand_match ps = | `Pacman as t -> t and aux level = function | `Bottom as t -> t - | #nf_nob as t -> aux_nob level t + | #nf_nob as t -> aux_nob level t and aux_i_num_var level = function | `Match(u,v,bs_lift,bs,args) as torig -> let u = aux_i_num_var level u in @@ -195,8 +215,8 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif let t = mk_match (`N i) orig bs_lift bs (args :> nf list) in (*prerr_endline ("NUOVO t:" ^ print (fst t :> nf) ^ " more_args=" ^ string_of_int (snd t));*) expand_match (freshno,acc_ps,acc_new_ps) t - | `Lam _ | `Pacman -> assert false (* loose typing *) - | `Bottom -> assert false (* algorithm invariant *) + | `Lam _ -> assert false (* algorithm invariant/loose typing *) + | `Bottom | `Pacman -> raise (Backtrack "BOT or PAC in toplevel numeric positioon") | #i_n_var as x -> let x = simple_expand_match (acc_ps@acc_new_ps) x in freshno,cast_to_i_num_var x,acc_new_ps in @@ -547,24 +567,6 @@ in*) let arity_of_x = Util.option_get (max_arity_tms x (all_terms p)) in x,arity_of_x,special_k -exception Backtrack - -let first bound p var f = - let p = {p with trail = (List.map (!) p.deltas)::p.trail} in - let rec aux i = - if i > bound then - (prerr_endline (">>>>>>>>>>>>>>>>>> BACKTRACKING ON "^ string_of_var var ^" J="^ string_of_int i ^" <<<<<<<<<<<<<<<<<<"); - raise Backtrack) - else - try - f p i - with - Backtrack -> - List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ; - aux (i+1) - in - aux 1 - let rec auto_eat (n,p) = prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}"; let m = problem_measure p in diff --git a/ocaml/num.ml b/ocaml/num.ml index a3d9bcf..3e19864 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -126,7 +126,7 @@ let rec string_of_term l = "[match("^ string_of_var v ^":"^ string_of_int ar ^") " ^ string_of_term_no_pars l (t :> nf) ^ " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift (t :> nf))) !bs) ^ "] " ^ String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")" - | `Bottom -> "TNT" + | `Bottom -> "BOT" | `Pacman -> "PAC" and string_of_term_no_pars_app l = function | `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 list)) @@ -200,7 +200,7 @@ 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));*) let m = match t with - `N m -> + `N m as t -> (try let h = List.assoc m !bs in let h = set_arity (minus1 ar) h in @@ -208,7 +208,13 @@ and mk_match t (n,ar) bs_lift bs args = h with Not_found -> `Match (t,(n,ar),bs_lift,bs,[])) - | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,[]) in + (* We are assuming that the econding of matches is s.t.: + - match PAC.. --> PAC + - match BOT.. --> BOT *) + | `Bottom -> `Bottom + | `Pacman -> `Pacman + | `Lam _ -> assert false + | `I _ | `Var _ | `Match _ as t -> `Match(t,(n,ar),bs_lift,bs,[]) in mk_appl m args and subst truelam delift_by_one what (with_what : nf(*_nob*)) (where : nf) = @@ -239,7 +245,8 @@ and subst truelam delift_by_one what (with_what : nf(*_nob*)) (where : nf) = (* The following line should be the identity when delift_by_one = true because we are assuming the ts to not contain lambda-bound variables. *) bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ; - mk_match (cast_to_i_num_var (aux_i_num_var l t)) v bs_lift bs (List.map (aux l) (args :> nf list)) + let body = aux_i_num_var l t in + mk_match body v bs_lift bs (List.map (aux l) (args :> nf list)) and aux l(*lift*) = (*function iii -> let res = match iii with*) function @@ -257,14 +264,22 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool let parse' strs = let fix_arity = function - | `I((n,_),args) -> `I((n,1+Listx.length args),args) - | _ -> assert false in - let rec aux = function - | Parser.Lam t -> `Lam (true, aux t) - | Parser.App (t1, t2) -> fix_arity (mk_app (aux t1) (aux t2)) - | Parser.Var v -> `Var(v,1) in + | `I((n,_),args) -> `I((n,1+Listx.length args),args) + | _ -> assert false in let (tms, free) = Parser.parse_many strs in - List.map aux tms, free + (* Replace pacmans and bottoms *) + let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in + let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in + let fix lev v = + if v = lev + n_bot then `Bottom + else if v = lev + n_pac then `Pacman + else `Var(v,1) in (* 1 by default when variable not applied *) + (* Fix arity *) + let rec aux lev = function + | Parser.Lam t -> `Lam (true, aux (lev+1) t) + | Parser.App (t1, t2) -> fix_arity (mk_app (aux lev t1) (aux lev t2)) + | Parser.Var v -> fix lev v in + List.map (aux 0) tms, free ;; (************** Algorithm(s) ************************) diff --git a/ocaml/num.mli b/ocaml/num.mli index bf9cae5..6de2645 100644 --- a/ocaml/num.mli +++ b/ocaml/num.mli @@ -32,7 +32,7 @@ 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 -val mk_match : i_num_var -> var -> int -> (int * nf) list ref -> nf list -> nf +val mk_match : nf -> var -> int -> (int * nf) list ref -> nf list -> nf val subst : bool -> bool -> int -> nf -> nf -> nf val parse' : string list -> nf list * string list val eta_compare : nf -> nf -> int diff --git a/ocaml/problems.ml b/ocaml/problems.ml index 2a99a5c..15fe980 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -334,9 +334,17 @@ let n3 () = magic_conv "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 ([ +(* let o1 () = magic_conv (Some"BOT") [] [] ["*"];; *) + +let o1 () = magic_conv None [] ["x BOT"] ["*"];; + +let o1 () = magic_conv None [] ["x a b"; "x (_. BOT) c"] ["*"];; + +main [o1() ];; + +(* 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 ; @@ -358,4 +366,4 @@ main ([ n1 ; n2 ; n3 -]));; +]));; *) -- 2.39.2