From: acondolu <andrea.condoluci@unibo.it>
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 ;