X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=ee69a2143bd100f8c514e31e7a0137e11254f810;hb=6ad07982ed7b55405c91315320b747086ba41c0e;hp=8a5cc37f12e4abdf075cf96b9dd52f58eda46905;hpb=a083188139e0ae7c4db8e6f0d7b7c913006fa148;p=fireball-separation.git diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 8a5cc37..ee69a21 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -5,6 +5,13 @@ open Num let bomb = ref(`Var(-1,-666));; +(* + The number of arguments which can applied to numbers + safely, depending on the encoding of numbers. + For Scott's encoding, two. +*) +let num_more_args = 2;; + type problem = { freshno: int ; div: i_var option (* None = bomb *) @@ -12,45 +19,42 @@ type problem = ; ps: i_n_var list (* the n-th inert must become n *) ; sigma: (int * nf) list (* the computed substitution *) ; deltas: (int * nf) list ref list (* collection of all branches *) - } - - -(* let heads = Util.sort_uniq (List.map hd_of_i_var p.ps) in -for all head - List.map (fun (_, bs) -> List.map (fun (x,_) -> List.nth p.ps x) !bs) p.deltas *) - -(* let ($) f x = f x;; *) - -(* let subterms tms freshno = - let apply_var = - let no = ref freshno in - function t -> incr no; mk_app t (`Var !no) in - let applicative hd args = snd ( - List.fold_left (fun (hd, acc) t -> let hd = mk_app hd t in hd, hd::acc) (hd, []) args) in - let rec aux t = match t with - | `Var _ -> [] - | `I(v,ts) -> - (* applicative (`Var v) (Listx.to_list ts) @ *) - Util.concat_map aux (Listx.to_list ts) @ List.map apply_var (Listx.to_list ts) - | `Lam(_,_,t) -> aux (lift ~-1 t) - | `Match(u,_,bs_lift,bs,args) -> - aux (u :> nf) @ - (* applicative (`Match(u,bs_lift,bs,[])) args @ *) - Util.concat_map aux args @ List.map apply_var args - (* @ Util.concat_map (aux ++ (lift bs_lift) ++ snd) !bs *) - | `N _ -> [] - in let tms' = (* Util.sort_uniq ~compare:eta_compare*) (Util.concat_map aux tms) in - tms @ tms' - (* List.map (fun (t, v) -> match t with `N _ -> t | _ -> mk_app t v) (List.combine tms (List.mapi (fun i _ -> `Var(freshno+i)) tms)) *) -;; *) + ; initialSpecialK: int +};; let all_terms p = -(match p.div with None -> [] | Some t -> [(t :> i_n_var)]) -@ p.conv -@ p.ps + (match p.div with None -> [] | Some t -> [(t :> i_n_var)]) + @ p.conv + @ p.ps +;; + +let sum_arities p = + let rec aux = function + | `N _ -> 0 + | `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*) + | `Lam(_,t) -> aux t + | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args) + | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many args + and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in + aux_many (all_terms p :> nf list) + ;; + +let count_fakevars p = + let rec aux = function + | `N _ -> 0 + | `Var(_,ar) -> if ar = min_int then 1 else 0 + | `Lam(_,t) -> aux t + | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args) + | `Match(u,v,_,_,args) -> aux (u :> nf) + aux (`Var v) + aux_many args + and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in + aux_many (all_terms p :> nf list) ;; -let problem_measure p = 0 ;; +(* let problem_measure p = count_fakevars p, sum_arities p;; +let string_of_measure (a,b) = "(fakevars="^string_of_int a^",sum_arities="^string_of_int b^")" *) + +let problem_measure p = sum_arities p;; +let string_of_measure = string_of_int;; let print_problem label ({freshno; div; conv; ps; deltas} as p) = Console.print_hline (); @@ -58,7 +62,7 @@ let print_problem label ({freshno; div; conv; ps; deltas} as p) = let nl = "\n| " in let deltas = String.concat nl (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in let l = Array.to_list (Array.init (freshno + 1) string_of_var) in - nl ^ "measure="^string_of_int(problem_measure p)^" freshno = " ^ string_of_int freshno + 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) ^ "\b> DIVERGENT" ^ nl @@ -84,17 +88,16 @@ let make_fresh_var p arity = let make_fresh_vars p arities = List.fold_right - (* fold_left vs. fold_right hides/shows the bug in problem q7 *) (fun arity (p, vars) -> let p, var = make_fresh_var p arity in p, var::vars) arities (p, []) ;; let simple_expand_match ps = - let rec aux level = function + let rec aux level = function | #i_num_var as t -> aux_i_num_var level t | `Lam(b,t) -> `Lam(b,aux (level+1) t) - and aux_i_num_var level = function + 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 bs := List.map (fun (n, x) -> n, aux 0 x) !bs; @@ -111,7 +114,8 @@ let simple_expand_match ps = `Match(cast_to_i_num_var u,v,bs_lift,bs,List.map (aux level) args)) | `I(v,args) -> `I(v,Listx.map (aux level) args) | `N _ | `Var _ as t -> t -in aux_i_num_var 0;; + in aux_i_num_var 0 +;; let fixpoint f = let rec aux x = let x' = f x in if x <> x' then aux x' else x in aux @@ -140,7 +144,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) | [] -> acc | t::todo_ps -> (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) - let t = subst false x inst (t :> nf) in + let t = subst false false x inst (t :> nf) in (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) let freshno,new_t,acc_new_ps = expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t @@ -154,7 +158,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) | t::todo_conv -> (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) (* try *) - let t = subst false x inst (t :> nf) in + let t = subst false false x inst (t :> nf) in (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t @@ -167,7 +171,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) function | None -> freshno, None, acc_new_ps | Some t -> - let t = subst false x inst (t :> nf) in + let t = subst false false x inst (t :> nf) in let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in @@ -181,7 +185,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) match u with | `N i -> acc_new_ps,i | _ -> - let ps = List.map (fun t -> cast_to_i_num_var (subst false x inst (t:> nf))) (acc_ps@acc_new_ps) in + let ps = List.map (fun t -> cast_to_i_num_var (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in let super_simplified_ps = super_simplify_ps ps ps in (*prerr_endline ("CERCO u:" ^ print (fst u :> nf)); List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps; @@ -194,7 +198,7 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif if List.exists (fun (j,_) -> i=j) !bs then freshno else - let freshno,v = freshno+1, `Var (freshno+1, snd orig - 1) in (* make_fresh_var freshno in *) + let freshno,v = freshno+1, `Var (freshno+1, -666) in (* make_fresh_var freshno in *) bs := !bs @ [i, v] ; freshno in (*prerr_endlie ("t DA RIDURRE:" ^ print (`Match(`N i,arity,bs_lift,bs,args) :> nf) ^ " more_args=" ^ string_of_int more_args);*) @@ -217,7 +221,7 @@ prerr_endline ("# INST: " ^ string_of_var x ^ " := " ^ print ~l inst)); let p = {p with freshno; div; conv; ps} in ( (* check if double substituting a variable *) if List.exists (fun (x',_) -> x = x') sigma - then failwithProblem p "Variable replaced twice" + then failwithProblem p ("Variable "^ string_of_var x ^"replaced twice") ); let p = {p with sigma = sigma@[x,inst]} in let p = super_simplify p in @@ -243,8 +247,8 @@ let rec dangerous arities showstoppers = (match t with `N _ -> List.iter (dangerous arities showstoppers) args | `Match _ as t -> dangerous arities showstoppers t ; List.iter (dangerous arities showstoppers) args - | `Var(x,_) -> dangerous_inert arities showstoppers x args 2 (* 2 coming from Scott's encoding *) - | `I((x,_),args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *) + | `Var(x,_) -> dangerous_inert arities showstoppers x args num_more_args + | `I((x,_),args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) num_more_args ) | `I((k,_),args) -> dangerous_inert arities showstoppers k (Listx.to_list args) 0 @@ -268,20 +272,24 @@ let rec dangerous_conv arities showstoppers = (match t with `N _ -> concat_map (dangerous_conv arities showstoppers) args | `Match _ as t -> dangerous_conv arities showstoppers t @ concat_map (dangerous_conv arities showstoppers) args - | `Var(x,_) -> dangerous_inert_conv arities showstoppers x args 2 (* 2 coming from Scott's encoding *) - | `I((x,_),args') -> dangerous_inert_conv arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *) + | `Var(x,_) -> dangerous_inert_conv arities showstoppers x [] args 2 + | `I((x,_),args') -> dangerous_inert_conv arities showstoppers x (Listx.to_list args') args 2 ) - | `I((k,_),args) -> dangerous_inert_conv arities showstoppers k (Listx.to_list args) 0 + | `I((k,_),args) -> dangerous_inert_conv arities showstoppers k (Listx.to_list args) [] 0 -and dangerous_inert_conv arities showstoppers k args more_args = - concat_map (dangerous_conv arities showstoppers) args @ - if List.mem k showstoppers then k :: concat_map free_vars args else +and dangerous_inert_conv arities showstoppers k args match_args more_args = + let all_args = args @ match_args in + let dangerous_args = concat_map (dangerous_conv arities showstoppers) all_args in + if dangerous_args = [] then ( + if List.mem k showstoppers then k :: concat_map free_vars all_args else try let arity = arity_of arities k in - prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var k ^ " listlenargs=" ^ (string_of_int (List.length args)) ); - if List.length args + more_args > arity then k :: concat_map free_vars args else [] +prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var k ^ " listlenargs=" ^ (string_of_int (List.length args)) ^ " more_args=" ^ string_of_int more_args); + if more_args > 0 (* match argument*) && List.length args = arity then [] + else if List.length all_args + more_args > arity then k :: concat_map free_vars all_args else [] with Not_found -> [] + ) else k :: concat_map free_vars all_args (* inefficient algorithm *) let rec edible arities div ps conv showstoppers = @@ -311,8 +319,9 @@ let rec edible arities div ps conv showstoppers = let dangerous_conv = List.map (dangerous_conv arities showstoppers) (conv :> nf list) in - prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv)); - List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))) dangerous_conv; +prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv)); +List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))) dangerous_conv; + let showstoppers' = showstoppers @ List.concat dangerous_conv in let showstoppers' = sort_uniq (match div with | None -> showstoppers' @@ -449,62 +458,73 @@ 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!")); 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 + (if arity_of_x = None then failwithProblem p "step on var non occurring in problem"); + (if Util.option_get(arity_of_x) = min_int then failwithProblem p "step on fake variable"); + (if Util.option_get(arity_of_x) <= 0 then failwithProblem p "step on var of non-positive arity"); + let n = (prerr_endline "WARNING: using constant initialSpecialK"); p.initialSpecialK in + (* AC: Once upon a time, it was: + 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 arities = Array.to_list (Array.make (n+1) min_int) in let p,vars = make_fresh_vars p arities in - (* let p,zero = make_fresh_var p in *) - (* let zero = Listx.Nil zero in *) - (* let args = if n = 0 then zero else Listx.append zero (Listx.from_list vars) in *) let args = Listx.from_list (vars :> nf list) in let bs = ref [] in - let inst = `Lam(false,`Match(`I((0,0),Listx.map (lift 1) args),(x,arity_of_x),1,bs,[])) in + (* 666, since it will be replaced anyway during subst: *) + let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,666),1,bs,[])) in let p = {p with deltas=bs::p.deltas} in subst_in_problem x inst p ;; let compute_special_k tms = - let rec aux k (t: nf) = Pervasives.max k (match t with - | `Lam(b,t) -> aux (k + if b then 1 else 0) t - | `I(n, tms) -> Listx.max (Listx.map (aux 0) tms) - | `Match(t, _, liftno, bs, args) -> - List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs)) - | `N _ -> 0 - | `Var _ -> 0 - ) in Listx.max (Listx.map (aux 0) tms) + let rec aux k (t: nf) = Pervasives.max k (match t with + | `Lam(b,t) -> aux (k + if b then 1 else 0) t + | `I(n, tms) -> Listx.max (Listx.map (aux 0) tms) + | `Match(t, _, liftno, bs, args) -> + List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs)) + | `N _ + | `Var _ -> 0 + ) in Listx.max (Listx.map (aux 0) tms) ;; let auto_instantiate (n,p) = - let p, showstoppers_step, showstoppers_eat = critical_showstoppers p in + let p, showstoppers_step, showstoppers_eat = critical_showstoppers p in let x = match showstoppers_step, showstoppers_eat with - | [], y::_ -> - prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y - | [], [] -> + | [], y::_ -> + prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y + | [], [] -> let heads = + (* Choose only variables still alive (with arity > 0) *) 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 + 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::_ -> - prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x); - x) + | [] -> + (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) | x::_, _ -> prerr_endline ("INSTANTIATING " ^ string_of_var x); x in -(* Strategy that decreases the special_k to 0 first (round robin) +(* Strategy that decreases the special_k to 0 first (round robin) 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 - None -> assert false + 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 + | None -> assert false | Some x -> prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x); x - with - Not_found -> x -in + with + Not_found -> x in (* Instantiate in decreasing order of compute_special_k 1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s let x = @@ -525,27 +545,28 @@ in*) special_k,p -let rec auto_eat (n,({ps} as p)) = +let rec auto_eat (n,p) = prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}"; let m = problem_measure p in let (n,p') = auto_instantiate (n,p) in match eat p' with - `Finished p -> p + | `Finished p -> p | `Continue p -> prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}"; - let delta = m - problem_measure p' in - if delta <= 0 then ( - (* failwithProblem p' *) - prerr_endline - ("Measure did not decrease (delta=" ^ string_of_int delta ^ ")")) - else prerr_endline ("$ Measure decreased by " ^ string_of_int delta); + let delta = problem_measure p - m in + (* let delta = m - problem_measure p' in *) + if delta >= 0 + then + (failwith + ("Measure did not decrease (+=" ^ string_of_int delta ^ ")")) + else prerr_endline ("$ Measure decreased of " ^ string_of_int delta); auto_eat (n,p) ;; let auto p n = prerr_endline ("@@@@ FIRST INSTANTIATE PHASE (" ^ string_of_int n ^ ") @@@@"); match eat p with - `Finished p -> p + | `Finished p -> p | `Continue p -> auto_eat (n,p) ;; @@ -733,7 +754,7 @@ in (********************** problems *******************) -let zero = `Var(0,-1);; +let zero = `Var(0,0);; let append_zero = function @@ -754,7 +775,7 @@ let magic_conv ~div ~conv ~nums cmds = if match div with None -> false | Some div -> List.exists (eta_subterm div) (tms@conv) then ( prerr_endline "--- TEST SKIPPED ---"; - {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]}, 0, [] + {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; initialSpecialK=0}, 0, [] ) else let tms = sort_uniq ~compare:eta_compare tms in let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *) @@ -769,7 +790,7 @@ let magic_conv ~div ~conv ~nums cmds = let dummy = `Var (max_int / 2, -666) in [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in - {freshno; div; conv; ps; sigma=[] ; deltas}, special_k, cmds + {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k}, special_k, cmds ;; let magic strings cmds = magic_conv None [] strings cmds;;