From: Claudio Sacerdoti Coen Date: Fri, 8 Dec 2006 17:36:24 +0000 (+0000) Subject: EXPERIMENTAL: X-Git-Tag: 0.4.95@7852~740 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=76c2d13b7641cdffae2759b511cbecbd91afa14e;p=helm.git EXPERIMENTAL: 1. the disambiguation domain is now a tree that partially reflects the applicative structure of the term 2. disambiguation now classifies errors according to the following criterium: an error E is considered not significant when it belongs to the set A of results (obtained interpreting a symbol and its subterms in every possible way) and there exists at least a result in A that is either OK or Uncertain. A "subterm" is implicitly defined by the tree structure of the disambiguation domain. 3. WARNING: there used to be an (important ????) optimization that has not been ported (yet ???): if the next item in the disambiguation domain can be interpreted in just one way, we skip the current refinement step. According to tests on my laptop the optimization does not seem to be really so significant (sometimes it even slow down???). We will decide on monday whether porting it or not. Porting it is not very simple because of the new data structures involved. --- diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index d334c72fe..9dc19c7c6 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/components/cic_disambiguation/disambiguate.ml @@ -30,6 +30,8 @@ open Printf open DisambiguateTypes open UriManager +module Ast = CicNotationPt + (* the integer is an offset to be added to each location *) exception NoWellTypedInterpretation of int * @@ -44,6 +46,46 @@ exception Try_again of string Lazy.t type aliases = bool * DisambiguateTypes.environment type 'a disambiguator_input = string * int * 'a +type domain = domain_tree list +and domain_tree = Node of Token.flocation list * domain_item * domain + +let rec string_of_domain = + function + [] -> "" + | Node (_,domain_item,l)::tl -> + DisambiguateTypes.string_of_domain_item domain_item ^ + " [ " ^ string_of_domain l ^ " ] " ^ string_of_domain tl + +let rec filter_map_domain f = + function + [] -> [] + | Node (locs,domain_item,l)::tl -> + match f locs domain_item with + None -> filter_map_domain f l @ filter_map_domain f tl + | Some res -> res :: filter_map_domain f l @ filter_map_domain f tl + +let rec map_domain f = + function + [] -> [] + | Node (locs,domain_item,l)::tl -> + f locs domain_item :: map_domain f l @ map_domain f tl + +let uniq_domain dom = + let rec aux seen = + function + [] -> seen,[] + | Node (locs,domain_item,l)::tl -> + if List.mem domain_item seen then + let seen,l = aux seen l in + let seen,tl = aux seen tl in + seen, l @ tl + else + let seen,l = aux (domain_item::seen) l in + let seen,tl = aux seen tl in + seen, Node (locs,domain_item,l)::tl + in + snd (aux [] dom) + let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () @@ -532,65 +574,74 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = let bo' = Some (interpretate_term [] env None false bo) in Cic.Constant (name,bo',ty',[],attrs)) - - (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *) -let rev_uniq = - let module SortedItem = - struct - type t = DisambiguateTypes.domain_item - let compare = Pervasives.compare - end - in - let module Map = Map.Make (SortedItem) in - fun l -> - let rev_l = List.rev l in - let (members, uniq_rev_l) = - List.fold_left - (fun (members, rev_l) (loc,elt) -> - try - let locs = Map.find elt members in - if List.mem loc locs then - members, rev_l - else - Map.add elt (loc::locs) members, rev_l - with - | Not_found -> Map.add elt [loc] members, elt :: rev_l) - (Map.empty, []) rev_l - in - List.rev_map - (fun e -> try Map.find e members,e with Not_found -> assert false) - uniq_rev_l - -(* "aux" keeps domain in reverse order and doesn't care about duplicates. - * Domain item more in deep in the list will be processed first. - *) -let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function - | CicNotationPt.AttributedTerm (`Loc loc, term) -> - domain_rev_of_term ~loc context term - | CicNotationPt.AttributedTerm (_, term) -> - domain_rev_of_term ~loc context term - | CicNotationPt.Appl terms -> - List.fold_left - (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms - | CicNotationPt.Binder (kind, (var, typ), body) -> - let kind_dom = - match kind with - | `Exists -> [ loc, Symbol ("exists", 0) ] - | _ -> [] +let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function + | Ast.AttributedTerm (`Loc loc, term) -> + domain_of_term ~loc ~context term + | Ast.AttributedTerm (_, term) -> + domain_of_term ~loc ~context term + | Ast.Symbol (symbol, instance) -> + [ Node ([loc], Symbol (symbol, instance), []) ] + (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *) + | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args) + -> + let args_dom = + List.fold_right + (fun term acc -> domain_of_term ~loc ~context term @ acc) + args [] in + let loc = + match hd with + Ast.AttributedTerm (`Loc loc,_) -> loc + | _ -> loc in - let type_dom = domain_rev_of_term_option ~loc context typ in - let body_dom = - domain_rev_of_term ~loc - (CicNotationUtil.cic_name_of_name var :: context) body + [ Node ([loc], Symbol (symbol, instance), args_dom) ] + | Ast.Appl (Ast.Ident (name, subst) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) -> + let args_dom = + List.fold_right + (fun term acc -> domain_of_term ~loc ~context term @ acc) + args [] in + let loc = + match hd with + Ast.AttributedTerm (`Loc loc,_) -> loc + | _ -> loc in - body_dom @ type_dom @ kind_dom - | CicNotationPt.Case (term, indty_ident, outtype, branches) -> - let term_dom = domain_rev_of_term ~loc context term in - let outtype_dom = domain_rev_of_term_option loc context outtype in + (try + (* the next line can raise Not_found *) + ignore(find_in_context name context); + if subst <> None then + Ast.fail loc "Explicit substitutions not allowed here" + else + args_dom + with Not_found -> + (match subst with + | None -> [ Node ([loc], Id name, args_dom) ] + | Some subst -> + let terms = + List.fold_left + (fun dom (_, term) -> + let dom' = domain_of_term ~loc ~context term in + dom @ dom') + [] subst in + [ Node ([loc], Id name, terms @ args_dom) ])) + | Ast.Appl terms -> + List.fold_right + (fun term acc -> domain_of_term ~loc ~context term @ acc) + terms [] + | Ast.Binder (kind, (var, typ), body) -> + let type_dom = domain_of_term_option ~loc ~context typ in + let body_dom = + domain_of_term ~loc + ~context:(CicNotationUtil.cic_name_of_name var :: context) body in + (match kind with + | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ] + | _ -> type_dom @ body_dom) + | Ast.Case (term, indty_ident, outtype, branches) -> + let term_dom = domain_of_term ~loc ~context term in + let outtype_dom = domain_of_term_option ~loc ~context outtype in let get_first_constructor = function | [] -> [] - | ((head, _, _), _) :: _ -> [ loc, Id head ] - in + | ((head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ] in let do_branch ((head, _, args), term) = let (term_context, args_domain) = List.fold_left @@ -598,37 +649,35 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function (CicNotationUtil.cic_name_of_name name :: cont, (match typ with | None -> dom - | Some typ -> domain_rev_of_term ~loc cont typ @ dom))) + | Some typ -> dom @ domain_of_term ~loc ~context:cont typ))) (context, []) args in - args_domain @ domain_rev_of_term ~loc term_context term + domain_of_term ~loc ~context:term_context term @ args_domain in let branches_dom = - List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches - in - branches_dom @ outtype_dom @ term_dom @ + List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in (match indty_ident with | None -> get_first_constructor branches - | Some (ident, _) -> [ loc, Id ident ]) - | CicNotationPt.Cast (term, ty) -> - let term_dom = domain_rev_of_term ~loc context term in - let ty_dom = domain_rev_of_term ~loc context ty in - ty_dom @ term_dom - | CicNotationPt.LetIn ((var, typ), body, where) -> - let body_dom = domain_rev_of_term ~loc context body in - let type_dom = domain_rev_of_term_option loc context typ in + | Some (ident, _) -> [ Node ([loc], Id ident, []) ]) + @ term_dom @ outtype_dom @ branches_dom + | Ast.Cast (term, ty) -> + let term_dom = domain_of_term ~loc ~context term in + let ty_dom = domain_of_term ~loc ~context ty in + term_dom @ ty_dom + | Ast.LetIn ((var, typ), body, where) -> + let body_dom = domain_of_term ~loc ~context body in + let type_dom = domain_of_term_option ~loc ~context typ in let where_dom = - domain_rev_of_term ~loc - (CicNotationUtil.cic_name_of_name var :: context) where - in - where_dom @ type_dom @ body_dom - | CicNotationPt.LetRec (kind, defs, where) -> + domain_of_term ~loc + ~context:(CicNotationUtil.cic_name_of_name var :: context) where in + body_dom @ type_dom @ where_dom + | Ast.LetRec (kind, defs, where) -> let add_defs context = List.fold_left (fun acc (_, (var, _), _, _) -> CicNotationUtil.cic_name_of_name var :: acc ) context defs in - let where_dom = domain_rev_of_term ~loc (add_defs context) where in + let where_dom = domain_of_term ~loc ~context:(add_defs context) where in let defs_dom = List.fold_left (fun dom (params, (_, typ), body, _) -> @@ -638,112 +687,108 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc) context params) in - domain_rev_of_term ~loc context' body @ - domain_rev_of_term_option ~loc context typ @ List.rev (snd (List.fold_left (fun (context,res) (var,ty) -> CicNotationUtil.cic_name_of_name var :: context, - res @ domain_rev_of_term_option ~loc context ty) + domain_of_term_option ~loc ~context ty @ res) (add_defs context,[]) params)) + @ domain_of_term_option ~loc ~context typ + @ domain_of_term ~loc ~context:context' body ) [] defs in - where_dom @ defs_dom - | CicNotationPt.Ident (name, subst) -> + defs_dom @ where_dom + | Ast.Ident (name, subst) -> (try (* the next line can raise Not_found *) ignore(find_in_context name context); if subst <> None then - CicNotationPt.fail loc "Explicit substitutions not allowed here" + Ast.fail loc "Explicit substitutions not allowed here" else [] with Not_found -> (match subst with - | None -> [loc, Id name] + | None -> [ Node ([loc], Id name, []) ] | Some subst -> - List.fold_left - (fun dom (_, term) -> - let dom' = domain_rev_of_term ~loc context term in - dom' @ dom) - [loc, Id name] subst)) - | CicNotationPt.Uri _ -> [] - | CicNotationPt.Implicit -> [] - | CicNotationPt.Num (num, i) -> [loc, Num i ] - | CicNotationPt.Meta (index, local_context) -> + let terms = + List.fold_left + (fun dom (_, term) -> + let dom' = domain_of_term ~loc ~context term in + dom @ dom') + [] subst in + [ Node ([loc], Id name, terms) ])) + | Ast.Uri _ -> [] + | Ast.Implicit -> [] + | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ] + | Ast.Meta (index, local_context) -> List.fold_left - (fun dom term -> domain_rev_of_term_option loc context term @ dom) [] - local_context - | CicNotationPt.Sort _ -> [] - | CicNotationPt.Symbol (symbol, instance) -> [loc, Symbol (symbol, instance) ] - | CicNotationPt.UserInput - | CicNotationPt.Literal _ - | CicNotationPt.Layout _ - | CicNotationPt.Magic _ - | CicNotationPt.Variable _ -> assert false + (fun dom term -> dom @ domain_of_term_option ~loc ~context term) + [] local_context + | Ast.Sort _ -> [] + | Ast.UserInput + | Ast.Literal _ + | Ast.Layout _ + | Ast.Magic _ + | Ast.Variable _ -> assert false -and domain_rev_of_term_option ~loc context = function +and domain_of_term_option ~loc ~context = function | None -> [] - | Some t -> domain_rev_of_term ~loc context t + | Some t -> domain_of_term ~loc ~context t -let domain_of_term ~context ast = rev_uniq (domain_rev_of_term context ast) +let domain_of_term ~context term = + uniq_domain (domain_of_term ~context term) let domain_of_obj ~context ast = assert (context = []); - let domain_rev = match ast with - | CicNotationPt.Theorem (_,_,ty,bo) -> - (match bo with + | Ast.Theorem (_,_,ty,bo) -> + domain_of_term [] ty + @ (match bo with None -> [] - | Some bo -> domain_rev_of_term [] bo) @ - domain_rev_of_term [] ty - | CicNotationPt.Inductive (params,tyl) -> - let dom = - List.flatten ( - List.rev_map - (fun (_,_,ty,cl) -> - List.flatten ( - List.rev_map - (fun (_,ty) -> domain_rev_of_term [] ty) cl) @ - domain_rev_of_term [] ty) tyl) in - let dom = + | Some bo -> domain_of_term [] bo) + | Ast.Inductive (params,tyl) -> + let context, dom = List.fold_left - (fun dom (_,ty) -> + (fun (context, dom) (var, ty) -> + let context' = CicNotationUtil.cic_name_of_name var :: context in match ty with - None -> dom - | Some ty -> domain_rev_of_term [] ty @ dom - ) dom params - in - List.filter - (fun (_,name) -> - not ( List.exists (fun (name',_) -> - match CicNotationUtil.cic_name_of_name name' with - Cic.Anonymous -> false - | Cic.Name name' -> name = Id name') params - || List.exists (fun (name',_,_,_) -> name = Id name') tyl) - ) dom - | CicNotationPt.Record (params,_,ty,fields) -> - let dom = - List.flatten - (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in - let dom = - List.fold_right - (fun (_,ty) dom -> + None -> context', dom + | Some ty -> context', dom @ domain_of_term context ty + ) ([], []) params in + let context_w_types = + List.rev_map + (fun (var, _, _, _) -> Cic.Name var) tyl + @ context in + dom + @ List.flatten ( + List.map + (fun (_,_,ty,cl) -> + domain_of_term context ty + @ List.flatten ( + List.map + (fun (_,ty) -> domain_of_term context_w_types ty) cl)) + tyl) + | CicNotationPt.Record (params,var,ty,fields) -> + let context, dom = + List.fold_left + (fun (context, dom) (var, ty) -> + let context' = CicNotationUtil.cic_name_of_name var :: context in match ty with - None -> dom - | Some ty -> dom @ domain_rev_of_term [] ty - ) params (dom @ domain_rev_of_term [] ty) - in - List.filter - (fun (_,name) -> - not ( List.exists (fun (name',_) -> - match CicNotationUtil.cic_name_of_name name' with - Cic.Anonymous -> false - | Cic.Name name' -> name = Id name') params - || List.exists (fun (name',_,_,_) -> name = Id name') fields) - ) dom - in - rev_uniq domain_rev + None -> context', dom + | Some ty -> context', dom @ domain_of_term context ty + ) ([], []) params in + let context_w_types = Cic.Name var :: context in + dom + @ domain_of_term context ty + @ snd + (List.fold_left + (fun (context,res) (name,ty,_,_) -> + Cic.Name name::context, res @ domain_of_term context ty + ) (context_w_types,[]) fields) + +let domain_of_obj ~context obj = + uniq_domain (domain_of_obj ~context obj) (* dom1 \ dom2 *) let domain_diff dom1 dom2 = @@ -762,7 +807,13 @@ let domain_diff dom1 dom2 = | item -> elt = item ) dom2 in - List.filter (fun (_,elt) -> not (is_in_dom2 elt)) dom1 + let rec aux = + function + [] -> [] + | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl) + | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl) + in + aux dom1 module type Disambiguator = sig @@ -846,8 +897,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" in debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); let thing_dom = domain_of_thing ~context:disambiguate_context thing in - debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s" - (string_of_domain (List.map snd thing_dom)))); + debug_print + (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom))); (* debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s" (DisambiguatePp.pp_environment aliases))); @@ -855,9 +906,10 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" (match universe with None -> "None" | Some _ -> "Some _"))); *) let current_dom = - Environment.fold (fun item _ dom -> item :: dom) aliases [] - in + Environment.fold (fun item _ dom -> item :: dom) aliases [] in let todo_dom = domain_diff thing_dom current_dom in + debug_print + (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom))); (* (2) lookup function for any item (Id/Symbol/Num) *) let lookup_choices = fun item -> @@ -916,16 +968,19 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" (* (3) test an interpretation filling with meta uninterpreted identifiers *) let test_env aliases todo_dom ugraph = - let filled_env = - List.fold_left - (fun env (_,item) -> - Environment.add item - ("Implicit", - (match item with - | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed)) - | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env) - aliases todo_dom - in + let rec aux env = function + | [] -> env + | Node (_, item, l) :: tl -> + let env = + Environment.add item + ("Implicit", + (match item with + | Id _ | Num _ -> + (fun _ _ _ -> Cic.Implicit (Some `Closed)) + | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) + env in + aux (aux env l) tl in + let filled_env = aux aliases todo_dom in try let localization_tbl = Cic.CicHash.create 503 in let cic_thing = @@ -943,17 +998,21 @@ in refine_profiler.HExtlib.profile foo () | Invalid_choice msg -> Ko (None,msg), ugraph in (* (4) build all possible interpretations *) - let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in - let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ = + let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in + (* aux returns triples Ok/Uncertain/Ko *) + (* rem_dom is the concatenation of all the remainin domains *) + let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ = + debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); match todo_dom with | [] -> assert (lookup_in_todo_dom = None); - (match test_env aliases [] base_univ with + (match test_env aliases rem_dom base_univ with | Ok (thing, metasenv),new_univ -> - [ aliases, diff, metasenv, thing, new_univ ], [] - | Ko (loc,msg),_ - | Uncertain (loc,msg),_ -> [],[aliases,diff,loc,msg,true]) - | (locs,item) :: remaining_dom -> + [ aliases, diff, metasenv, thing, new_univ ], [], [] + | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] + | Uncertain (loc,msg),new_univ -> + [],[aliases,diff,loc,msg,new_univ],[]) + | Node (locs,item,inner_dom) :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); let choices = @@ -962,10 +1021,11 @@ in refine_profiler.HExtlib.profile foo () | Some choices -> choices in match choices with [] -> - [], [aliases, diff, - Some (List.hd locs), - lazy ("No choices for " ^ string_of_domain_item item), - true] + [], [], + [aliases, diff, Some (List.hd locs), + 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 @@ -999,76 +1059,88 @@ in refine_profiler.HExtlib.profile foo () aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true]) +*) | _::_ -> - let mark_not_significant (successes, failures) = - successes, + let mark_not_significant failures = 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 classify_errors ((ok_l,uncertain_l,error_l) as outcome) = + if ok_l <> [] || uncertain_l <> [] then + ok_l,uncertain_l,mark_not_significant error_l + else + 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 + (match + test_env new_env (inner_dom@remaining_dom@rem_dom) univ + with | Ok (thing, metasenv),new_univ -> let res = - (match remaining_dom with - | [] -> [new_env,new_diff,metasenv,thing,new_univ], [] + (match inner_dom with + | [] -> + [new_env,new_diff,metasenv,thing,new_univ], [], [] | _ -> - aux new_env new_diff None remaining_dom new_univ + aux new_env new_diff None inner_dom + (remaining_dom@rem_dom) new_univ ) in - `Ok res :: filter univ tl + res @@ filter univ tl | Uncertain (loc,msg),new_univ -> let res = - (match remaining_dom with - | [] -> [],[new_env,new_diff,loc,msg,true] + (match inner_dom with + | [] -> [],[new_env,new_diff,loc,msg,new_univ],[] | _ -> - aux new_env new_diff None remaining_dom new_univ + aux new_env new_diff None inner_dom + (remaining_dom@rem_dom) new_univ ) in - `Ok res :: filter univ tl + res @@ filter univ tl | Ko (loc,msg),_ -> - let res = [],[new_env,new_diff,loc,msg,true] in - `Ko res :: filter univ tl) + let res = [],[],[new_env,new_diff,loc,msg,true] in + res @@ filter univ tl) in - classify_errors (filter base_univ choices) + let ok_l,uncertain_l,error_l = + classify_errors (filter base_univ choices) + in + let res_after_ok_l = + List.fold_right + (fun (env,diff,_,_,univ) res -> + aux env diff None remaining_dom rem_dom univ @@ res + ) ok_l ([],[],error_l) + in + List.fold_right + (fun (env,diff,_,_,univ) res -> + aux env diff None remaining_dom rem_dom univ @@ res + ) uncertain_l res_after_ok_l 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 + 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 -> + | [],uncertain,errors -> + let errors = + List.map + (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true) + ) uncertain @ errors + in let errors = List.map (fun (env,diff,loc,msg,significant) -> let env' = - HExtlib.filter_map - (fun (locs,domain_item) -> + filter_map_domain + (fun locs domain_item -> try let description = fst (Environment.find domain_item env) @@ -1082,17 +1154,17 @@ in refine_profiler.HExtlib.profile foo () ) errors in raise (NoWellTypedInterpretation (0,errors)) - | [_,diff,metasenv,t,ugraph],_ -> + | [_,diff,metasenv,t,ugraph],_,_ -> debug_print (lazy "SINGLE INTERPRETATION"); [diff,metasenv,t,ugraph], false - | l,_ -> + | l,_,_ -> debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); let choices = List.map (fun (env, _, _, _, _) -> - List.map - (fun (locs,domain_item) -> + map_domain + (fun locs domain_item -> let description = fst (Environment.find domain_item env) in @@ -1121,7 +1193,8 @@ in refine_profiler.HExtlib.profile foo () in disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term - ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term + ~domain_of_thing:domain_of_term + ~interpretate_thing:interpretate_term ~refine_thing:refine_term (text,prefix_len,term) let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri