- 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