From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 1 Jul 2004 14:10:27 +0000 (+0000)
Subject: added (commented) benchmarking code for the disambiguation paper
X-Git-Tag: pre_subst_in_kernel~13
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=da49d2dca60a85abe54e0e549b290fa28a8127ba;p=helm.git

added (commented) benchmarking code for the disambiguation paper
---

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index d627c76e1..93795f96e 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -37,6 +37,15 @@ exception Try_again
 let debug = true
 let debug_print = if debug then prerr_endline else ignore
 
+(*
+  (** print benchmark information *)
+let benchmark = true
+let max_refinements = ref 0       (* benchmarking is not thread safe *)
+let actual_refinements = ref 0
+let domain_size = ref 0
+let choices_avg = ref 0.
+*)
+
 let descr_of_domain_item = function
  | Id s -> s
  | Symbol (s, _) -> s
@@ -48,7 +57,8 @@ type test_result =
   | Uncertain
 
 let refine metasenv context term =
-  let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
+(*   if benchmark then incr actual_refinements; *)
+  let metasenv, term = CicMkImplicit.expand_implicits metasenv [] context term in
   debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
   try
     let term', _, metasenv' = CicRefine.type_of_aux' metasenv context term in
@@ -471,6 +481,32 @@ module Make (C: Callbacks) =
         if choices = [] then raise (No_choices item);
         choices
       in
+
+(*
+      (* <benchmark> *)
+      let _ =
+        if benchmark then begin
+          let per_item_choices =
+            List.map
+              (fun dom_item ->
+                try
+                  let len = List.length (lookup_choices dom_item) in
+                  prerr_endline (sprintf "BENCHMARK %s: %d"
+                    (string_of_domain_item dom_item) len);
+                  len
+                with No_choices _ -> 0)
+              term_dom
+          in
+          max_refinements := List.fold_left ( * ) 1 per_item_choices;
+          actual_refinements := 0;
+          domain_size := List.length term_dom;
+          choices_avg :=
+            (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
+        end
+      in
+      (* </benchmark> *)
+*)
+
       (* (3) test an interpretation filling with meta uninterpreted identifiers
        *)
       let test_env current_env todo_dom univ = 
@@ -532,36 +568,49 @@ module Make (C: Callbacks) =
       in
        let base_univ = CicUniv.get_working () in
       try
-       match aux current_env todo_dom base_univ with
-       | [] -> raise NoWellTypedInterpretation
-       | [ e,me,t,u ] as l ->
-           debug_print "UNA SOLA SCELTA";
-           CicUniv.set_working u;
-           [ e,me,t ]
-       | l ->
-           debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
-           let choices =
-             List.map
-               (fun (env, _, _, _) ->
-                 List.map
-                   (fun domain_item ->
-                     let description =
-                       fst (Environment.find domain_item env)
-                     in
-                     (descr_of_domain_item domain_item, description))
-                   term_dom)
-               l
-           in
-           let choosed = C.interactive_interpretation_choice choices in
-           let l' = List.map (List.nth l) choosed in
-           match l' with
-             [] -> assert false
-           | [e,me,t,u] -> 
-               CicUniv.set_working u;
-               (*CicUniv.print_working_graph ();*)
-               [e,me,t]
-           | hd::tl -> (* ok, testlibrary... cosi' stampa MANY... bah *)
-               List.map (fun (e,me,t,u) -> (e,me,t)) l'
+        let res =
+         match aux current_env todo_dom base_univ with
+         | [] -> raise NoWellTypedInterpretation
+         | [ e,me,t,u ] as l ->
+             debug_print "UNA SOLA SCELTA";
+             CicUniv.set_working u;
+             [ e,me,t ]
+         | l ->
+             debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
+             let choices =
+               List.map
+                 (fun (env, _, _, _) ->
+                   List.map
+                     (fun domain_item ->
+                       let description =
+                         fst (Environment.find domain_item env)
+                       in
+                       (descr_of_domain_item domain_item, description))
+                     term_dom)
+                 l
+             in
+             let choosed = C.interactive_interpretation_choice choices in
+             let l' = List.map (List.nth l) choosed in
+             match l' with
+               [] -> assert false
+             | [e,me,t,u] -> 
+                 CicUniv.set_working u;
+                 (*CicUniv.print_working_graph ();*)
+                 [e,me,t]
+             | hd::tl -> (* ok, testlibrary... cosi' stampa MANY... bah *)
+                 List.map (fun (e,me,t,u) -> (e,me,t)) l'
+        in
+(*
+        (if benchmark then
+          let res_size = List.length res in
+          prerr_endline (sprintf
+            ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
+            "BENCHMARK:   estimated %.2f")
+            !actual_refinements !max_refinements !domain_size res_size
+            !choices_avg
+            (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
+*)
+        res
      with
       CicEnvironment.CircularDependency s -> 
         raise (Failure "e chi la becca sta CircularDependency?");