(* reports the first source of ambiguity and its possible interpretations *)
exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec list)
+(* reports disambiguation errors *)
+exception Error of
+ (* location of a choice point *)
+ (Stdpp.location *
+ (* one possible choice (or no valid choice) *)
+ (GrafiteAst.alias_spec option *
+ (* list of asts together with the failing location and error msg *)
+ ((Stdpp.location * GrafiteAst.alias_spec) list *
+ Stdpp.location * string) list)
+ list)
+ list
+
let dump_aliases out msg status =
out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
{status#disambiguate_db with interpr = interpr }
in
status#set_disambiguate_db new_status
-
+
+(*
+let print_interpr status =
+ DisambiguateTypes.InterprEnv.iter
+ (fun loc alias ->
+ let start,stop = HExtlib.loc_of_floc loc in
+ let strpos = Printf.sprintf "@(%d,%d):" start stop in
+ match alias with
+ | GrafiteAst.Ident_alias (id,uri) ->
+ Printf.printf "%s [%s;%s]\n" strpos id uri
+ | GrafiteAst.Symbol_alias (name,_ouri,desc) ->
+ Printf.printf "%s <%s:%s>\n" strpos name desc
+ | GrafiteAst.Number_alias (_ouri,desc) ->
+ Printf.printf "%s <NUM:%s>\n" strpos desc)
+ status#disambiguate_db.interpr
+*)
+
let add_to_disambiguation_univ status new_aliases =
let multi_aliases =
List.fold_left (fun acc (d,c) ->
find_diffs tls
;;
+(* clusterize a list of errors according to the last chosen interpretation *)
+let clusterize diff (eframe,loc0) =
+ let rec aux = function
+ | [] -> []
+ | (_,choice,_,_ as x)::l0 ->
+ let matches,others = List.partition (fun (_,c,_,_) -> c = choice) l0 in
+ (choice,List.map (fun (a,_,l,e) -> diff a,l,e) (x::matches)) ::
+ aux others
+ in loc0, aux eframe
+
let disambiguate_nterm status expty context metasenv subst thing
=
- let choices, _ = NCicDisambiguate.disambiguate_term
+ let _,_,thing' = thing in
+ match NCicDisambiguate.disambiguate_term
status
~aliases:status#disambiguate_db.interpr
~expty
~mk_implicit ~fix_instance
~description_of_alias:GrafiteAst.description_of_alias
~context ~metasenv ~subst thing
- in
- let _,_,thing' = thing in
- match choices with
- | [newast, metasenv, subst, cic] ->
+ with
+ | Disambiguate.Disamb_success [newast,metasenv,subst,cic,_] ->
let diff = diff_term Stdpp.dummy_loc thing' newast in
let status = add_to_interpr status diff
in
metasenv, subst, status, cic
- | [] -> assert false
- | _ ->
+ | Disambiguate.Disamb_success (_::_ as choices) ->
let diffs =
- List.map (fun (ast,_,_,_) ->
+ List.map (fun (ast,_,_,_,_) ->
diff_term Stdpp.dummy_loc thing' ast) choices
- in
- raise (Ambiguous_input (find_diffs diffs))
+ in
+ raise (Ambiguous_input (find_diffs diffs))
+ | Disambiguate.Disamb_failure l ->
+ raise (Error (List.map (clusterize (diff_term Stdpp.dummy_loc thing')) l))
+ | _ -> assert false
;;
type pattern =
NUri.uri_of_string (baseuri ^ "/" ^ name)
in
- let choices, _ = NCicDisambiguate.disambiguate_obj
+ match NCicDisambiguate.disambiguate_obj
status
~lookup_in_library:(nlookup_in_library status)
~description_of_alias:GrafiteAst.description_of_alias
~aliases:status#disambiguate_db.interpr
~universe:(status#disambiguate_db.multi_aliases)
obj'
- in
- match choices with
- | [ast, _, _, cic] ->
- let diff = diff_obj Stdpp.dummy_loc obj ast in
- let status = add_to_interpr status diff
- in
- status, cic
- | [] -> assert false
- | _ ->
+ with
+ | Disambiguate.Disamb_success [newast,_,_,cic,_] ->
+ let diff = diff_obj Stdpp.dummy_loc obj newast in
+ let status = add_to_interpr status diff
+ in status, cic
+ | Disambiguate.Disamb_success (_::_ as choices) ->
let diffs =
- List.map (fun (ast,_,_,_) ->
+ List.map (fun (ast,_,_,_,_) ->
diff_obj Stdpp.dummy_loc obj ast) choices
in
- raise (Ambiguous_input (find_diffs diffs))
+ raise (Ambiguous_input (find_diffs diffs))
+ | Disambiguate.Disamb_failure l ->
+ raise (Error (List.map (clusterize (diff_obj Stdpp.dummy_loc obj)) l))
+ | _ -> assert false
;;
let disambiguate_cic_appl_pattern status args =