From: acondolu Date: Mon, 10 Jul 2017 13:48:25 +0000 (+0200) Subject: Experimenting with a combined measure X-Git-Tag: weak-reduction-separation~66 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ee425005e52a3cedad28698bc4611c99e1abefb5;p=fireball-separation.git Experimenting with a combined measure --- diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 77449b4..486af14 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -21,7 +21,33 @@ let all_terms p = @ p.ps ;; -let problem_measure p = 0 ;; +let sum_arities p = + let rec aux = function + | `N _ -> 0 + | `Var(_,ar) -> if ar = min_int then 0 else (assert (ar >= 0); ar) + | `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 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 = 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 (); @@ -29,7 +55,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 @@ -456,8 +482,9 @@ let auto_instantiate (n,p) = 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 @@ -501,7 +528,7 @@ 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 @@ -509,10 +536,13 @@ let rec auto_eat (n,({ps} as p)) = `Finished p -> p | `Continue p -> prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}"; - let delta = m - problem_measure p' in + let m' = problem_measure p in + let delta = compare m m' in + print_endline ("compare " ^ string_of_measure m' ^ " " ^ string_of_measure m ^ "= " ^ string_of_int delta); + (* let delta = m - problem_measure p' in *) if delta <= 0 then ( - (* failwithProblem p' *) - prerr_endline + failwith + (* prerr_endline *) ("Measure did not decrease (delta=" ^ string_of_int delta ^ ")")) else prerr_endline ("$ Measure decreased by " ^ string_of_int delta); auto_eat (n,p) diff --git a/ocaml/problems.ml b/ocaml/problems.ml index a0ff453..2dff11d 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -286,11 +286,11 @@ let m2 () = magic_conv None [] ;; 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 ; *) + 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 ; - (* q7 ; *) + q7 ; q8 ; q9 ; q10 ;