(* the integer is an offset to be added to each location *)
exception NoWellTypedInterpretation of
- int * (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) list
exception PathNotWellFormed
(** raised when an environment is not enough informative to decide *)
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) ->
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
(match test_env aliases [] base_univ with
| Ok (thing, metasenv),new_univ ->
[ aliases, diff, metasenv, thing, new_univ ], []
- | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
+ | Ko (loc,msg),_
+ | Uncertain (loc,msg),_ -> [],[aliases,diff,loc,msg])
| (locs,item) :: remaining_dom ->
debug_print (lazy (sprintf "CHOOSED ITEM: %s"
(string_of_domain_item item)));
| Some choices -> choices in
match choices with
[] ->
- [], [Some (List.hd locs),
+ [], [aliases, diff,
+ Some (List.hd locs),
lazy ("No choices for " ^ string_of_domain_item item)]
| [codomain_item] ->
(* just one choice. We perform a one-step look-up and
remaining_dom new_univ)
| Uncertain (loc,msg),new_univ ->
(match remaining_dom with
- | [] -> [], [loc,msg]
+ | [] -> [], [new_env,new_diff,loc,msg]
| _ ->
aux new_env new_diff lookup_in_todo_dom
remaining_dom new_univ)
- | Ko (loc,msg),_ -> [], [loc,msg])
+ | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg])
| _::_ ->
let rec filter univ = function
| [] -> [],[]
(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 ], []
+ | [] -> [new_env,new_diff,metasenv,thing,new_univ], []
| _ -> aux new_env new_diff None remaining_dom new_univ
) @@
filter univ tl
| Uncertain (loc,msg),new_univ ->
(match remaining_dom with
- | [] -> [],[loc,msg]
+ | [] -> [],[new_env,new_diff,loc,msg]
| _ -> aux new_env new_diff None remaining_dom new_univ
) @@
filter univ tl
- | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl)
+ | Ko (loc,msg),_ -> ([],[new_env,new_diff,loc,msg]) @@ filter univ tl)
in
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]) 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) ->
+ 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
+ ) errors
+ in
+ raise (NoWellTypedInterpretation (0,errors))
| [_,diff,metasenv,t,ugraph],_ ->
debug_print (lazy "SINGLE INTERPRETATION");
[diff,metasenv,t,ugraph], false