- debug_print (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 (sprintf "%s CHOSEN" (fst codomain_item)) ;
- let new_env =
- Environment.add item codomain_item current_env
- in
- (match test_env new_env remaining_dom univ with
- | Ok (thing, metasenv),new_univ ->
- (match remaining_dom with
- | [] -> [ new_env, metasenv, thing, new_univ ]
- | _ -> aux new_env remaining_dom new_univ )@
- filter univ tl
- | Uncertain,new_univ ->
- (match remaining_dom with
- | [] -> []
- | _ -> aux new_env remaining_dom new_univ )@
- filter univ tl
- | Ko,_ -> filter univ tl)
- in
- filter base_univ choices
+ debug_print (lazy (sprintf "CHOOSED ITEM: %s"
+ (string_of_domain_item item)));
+ let choices =
+ match lookup_in_todo_dom with
+ None -> lookup_choices item
+ | Some choices -> choices in
+ match choices with
+ [] -> [], [lazy "No choices"]
+ | [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 msg,new_univ ->
+ (match remaining_dom with
+ | [] -> [], [msg]
+ | _ ->
+ aux new_env new_diff lookup_in_todo_dom
+ remaining_dom new_univ)
+ | Ko msg,_ -> [], [msg])
+ | _::_ ->
+ 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 msg,new_univ ->
+ (match remaining_dom with
+ | [] -> [],[msg]
+ | _ -> aux new_env new_diff None remaining_dom new_univ
+ ) @@
+ filter univ tl
+ | Ko msg,_ -> ([],[msg]) @@ filter univ tl)
+ in
+ filter base_univ choices