From: Claudio Sacerdoti Coen Date: Thu, 29 Sep 2005 09:10:37 +0000 (+0000) Subject: Further speed-up in the disambiguation algorithm. X-Git-Tag: V_0_7_2_3~280 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0a17483072707b5a460a6c04571c6ddfc5875ce2;p=helm.git Further speed-up in the disambiguation algorithm. The case |choices| = 1 is handled in a special way: if |choices| = 1 also for the next ambiguous symbol, then the current refinement step is skipped NOTE: this suggests that pre-setting all the interpretations with cardinality 1 (as it used to be) could greatly speed up things in certain cases --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 05a15691e..51c124a9b 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -706,10 +706,12 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let thing_dom = domain_of_thing ~context:disambiguate_context thing in debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s" (string_of_domain thing_dom))); +(* debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s" (DisambiguatePp.pp_environment aliases))); debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s" (match universe with None -> "None" | Some _ -> "Some _"))); +*) let current_dom = Environment.fold (fun item _ dom -> item :: dom) aliases [] in @@ -790,9 +792,10 @@ in refine_profiler.HExtlib.profile foo () | Invalid_choice -> Ko, ugraph in (* (4) build all possible interpretations *) - let rec aux aliases diff todo_dom base_univ = + let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ = match todo_dom with | [] -> + assert (lookup_in_todo_dom = None); (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> [ aliases, diff, metasenv, thing, new_univ ] @@ -800,32 +803,72 @@ in refine_profiler.HExtlib.profile foo () | item :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); - let choices = lookup_choices item in - let rec filter univ = function - | [] -> [] - | codomain_item :: tl -> - debug_print (lazy (sprintf "%s CHOSEN" (fst codomain_item))) ; - let new_env = Environment.add item codomain_item aliases in - let new_diff = (item,codomain_item)::diff in - (match test_env new_env remaining_dom univ with - | Ok (thing, metasenv),new_univ -> - (match remaining_dom with - | [] -> [ new_env, new_diff, metasenv, thing, new_univ ] - | _ -> aux new_env new_diff remaining_dom new_univ )@ - filter univ tl - | Uncertain,new_univ -> - (match remaining_dom with - | [] -> [] - | _ -> aux new_env new_diff remaining_dom new_univ )@ - filter univ tl - | Ko,_ -> filter univ tl) - in - filter base_univ choices + let choices = + match lookup_in_todo_dom with + None -> lookup_choices item + | Some choices -> choices in + match choices with + [] -> [] + | [codomain_item] -> + (* just one choice. We perform a one-step look-up and + if the next set of choices is also a singleton we + skip this refinement step *) + debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); + let new_env = Environment.add item codomain_item aliases in + let new_diff = (item,codomain_item)::diff in + let lookup_in_todo_dom,next_choice_is_single = + match remaining_dom with + [] -> None,false + | he::_ -> + let choices = lookup_choices he in + Some choices,List.length choices = 1 + in + if next_choice_is_single then + aux new_env new_diff lookup_in_todo_dom remaining_dom + base_univ + else + (match test_env new_env remaining_dom base_univ with + | Ok (thing, metasenv),new_univ -> + (match remaining_dom with + | [] -> [ new_env, new_diff, metasenv, thing, new_univ ] + | _ -> + aux new_env new_diff lookup_in_todo_dom + remaining_dom new_univ) + | Uncertain,new_univ -> + (match remaining_dom with + | [] -> [] + | _ -> + aux new_env new_diff lookup_in_todo_dom + remaining_dom new_univ) + | Ko,_ -> []) + | _::_ -> + let rec filter univ = function + | [] -> [] + | codomain_item :: tl -> + debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); + let new_env = Environment.add item codomain_item aliases in + let new_diff = (item,codomain_item)::diff in + (match test_env new_env remaining_dom univ with + | Ok (thing, metasenv),new_univ -> + (match remaining_dom with + | [] -> [ new_env, new_diff, metasenv, thing, new_univ ] + | _ -> aux new_env new_diff None remaining_dom new_univ + ) @ + filter univ tl + | Uncertain,new_univ -> + (match remaining_dom with + | [] -> [] + | _ -> aux new_env new_diff None remaining_dom new_univ + ) @ + filter univ tl + | Ko,_ -> filter univ tl) + in + filter base_univ choices in let base_univ = initial_ugraph in try let res = - match aux aliases [] todo_dom base_univ with + match aux aliases [] None todo_dom base_univ with | [] -> raise NoWellTypedInterpretation | [_,diff,metasenv,t,ugraph] -> debug_print (lazy "SINGLE INTERPRETATION");