X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=d334c72fe9c5c24dd757d7d15eec21030c30addd;hb=8b20a402003f57320cb9f0cc2eedebbceb16d3fc;hp=352b043a4df4704ff8d6b288efbfca16ac77e418;hpb=79f497094d49963fe9f335e00b58aecc79cbc461;p=helm.git diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 352b043a4..d334c72fe 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -32,7 +32,10 @@ open UriManager (* the integer is an offset to be added to each location *) exception NoWellTypedInterpretation of - int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Token.flocation option * string Lazy.t) list + int * + ((Token.flocation list * string * string) list * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + Token.flocation option * string Lazy.t * bool) list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) @@ -724,12 +727,12 @@ let domain_of_obj ~context ast = List.flatten (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in let dom = - List.fold_left - (fun dom (_,ty) -> + List.fold_right + (fun (_,ty) dom -> match ty with None -> dom - | Some ty -> domain_rev_of_term [] ty @ dom - ) (dom @ domain_rev_of_term [] ty) params + | Some ty -> dom @ domain_rev_of_term [] ty + ) params (dom @ domain_rev_of_term [] ty) in List.filter (fun (_,name) -> @@ -863,8 +866,11 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" match item with | Id id -> choices_of_id dbd id | Symbol (symb, _) -> - List.map DisambiguateChoices.mk_choice + (try + List.map DisambiguateChoices.mk_choice (TermAcicContent.lookup_interpretations symb) + with + TermAcicContent.Interpretation_not_found -> []) | Num instance -> DisambiguateChoices.lookup_num_choices () in @@ -945,7 +951,8 @@ in refine_profiler.HExtlib.profile foo () (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> [ aliases, diff, metasenv, thing, new_univ ], [] - | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[diff,loc,msg]) + | Ko (loc,msg),_ + | Uncertain (loc,msg),_ -> [],[aliases,diff,loc,msg,true]) | (locs,item) :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); @@ -955,9 +962,10 @@ in refine_profiler.HExtlib.profile foo () | Some choices -> choices in match choices with [] -> - [], [diff, + [], [aliases, diff, Some (List.hd locs), - lazy ("No choices for " ^ string_of_domain_item item)] + lazy ("No choices for " ^ string_of_domain_item item), + true] | [codomain_item] -> (* just one choice. We perform a one-step look-up and if the next set of choices is also a singleton we @@ -986,40 +994,94 @@ in refine_profiler.HExtlib.profile foo () remaining_dom new_univ) | Uncertain (loc,msg),new_univ -> (match remaining_dom with - | [] -> [], [new_diff,loc,msg] + | [] -> [], [new_env,new_diff,loc,msg,true] | _ -> aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) - | Ko (loc,msg),_ -> [], [new_diff,loc,msg]) + | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true]) | _::_ -> + let mark_not_significant (successes, failures) = + successes, + List.map + (fun (env, diff, loc, msg, _b) -> + env, diff, loc, msg, false) + failures in + let classify_errors outcome = + if List.exists (function `Ok _ -> true | _ -> false) outcome + then + List.fold_right + (fun res acc -> + match res with + | `Ok res -> res @@ acc + | `Ko res -> mark_not_significant res @@ acc) + outcome ([],[]) + else + List.fold_right + (fun res acc -> + match res with + | `Ok res | `Ko res -> res @@ acc) + outcome ([],[]) 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 None remaining_dom new_univ - ) @@ - filter univ tl + let res = + (match remaining_dom with + | [] -> [new_env,new_diff,metasenv,thing,new_univ], [] + | _ -> + aux new_env new_diff None remaining_dom new_univ + ) + in + `Ok res :: filter univ tl | Uncertain (loc,msg),new_univ -> - (match remaining_dom with - | [] -> [],[new_diff,loc,msg] - | _ -> aux new_env new_diff None remaining_dom new_univ - ) @@ - filter univ tl - | Ko (loc,msg),_ -> ([],[new_diff,loc,msg]) @@ filter univ tl) + let res = + (match remaining_dom with + | [] -> [],[new_env,new_diff,loc,msg,true] + | _ -> + aux new_env new_diff None remaining_dom new_univ + ) + in + `Ok res :: filter univ tl + | Ko (loc,msg),_ -> + let res = [],[new_env,new_diff,loc,msg,true] in + `Ko res :: filter univ tl) in - filter base_univ choices + classify_errors (filter base_univ choices) in + let aux' aliases diff lookup_in_todo_dom todo_dom base_univ = + match test_env aliases todo_dom base_univ with + | Ok _,_ + | Uncertain _,_ -> + aux aliases diff lookup_in_todo_dom todo_dom base_univ + | Ko (loc,msg),_ -> ([],[aliases,diff,loc,msg,true]) in let base_univ = initial_ugraph in try let res = - match aux aliases [] None todo_dom base_univ with - | [],errors -> raise (NoWellTypedInterpretation (0,errors)) + match aux' aliases [] None todo_dom base_univ with + | [],errors -> + let errors = + List.map + (fun (env,diff,loc,msg,significant) -> + let env' = + HExtlib.filter_map + (fun (locs,domain_item) -> + try + let description = + fst (Environment.find domain_item env) + in + Some (locs,descr_of_domain_item domain_item,description) + with + Not_found -> None) + thing_dom + in + env',diff,loc,msg,significant + ) errors + in + raise (NoWellTypedInterpretation (0,errors)) | [_,diff,metasenv,t,ugraph],_ -> debug_print (lazy "SINGLE INTERPRETATION"); [diff,metasenv,t,ugraph], false