X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=77449b4681a7887cde71c8cbd170588b8a53241a;hb=08d2b663e5089ed046ef771bfb2555a31e525f1c;hp=8a5cc37f12e4abdf075cf96b9dd52f58eda46905;hpb=a083188139e0ae7c4db8e6f0d7b7c913006fa148;p=fireball-separation.git diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 8a5cc37..77449b4 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -12,42 +12,13 @@ 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 problem_measure p = 0 ;; @@ -84,17 +55,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 +81,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 +111,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 +125,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 +138,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 +152,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; @@ -449,16 +420,19 @@ 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,n+2),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 ;; @@ -493,11 +467,13 @@ let auto_instantiate (n,p) = | 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 + 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 +709,7 @@ in (********************** problems *******************) -let zero = `Var(0,-1);; +let zero = `Var(0,0);; let append_zero = function @@ -754,7 +730,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 +745,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;;