From da49d2dca60a85abe54e0e549b290fa28a8127ba Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 1 Jul 2004 14:10:27 +0000 Subject: [PATCH] added (commented) benchmarking code for the disambiguation paper --- helm/ocaml/cic_disambiguation/disambiguate.ml | 111 +++++++++++++----- 1 file changed, 80 insertions(+), 31 deletions(-) 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 + +(* + (* *) + 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 + (* *) +*) + (* (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?"); -- 2.39.2