the current interpretation to re-obtain the refinement errors).
(* the integer is an offset to be added to each location *)
exception NoWellTypedInterpretation of
(* the integer is an offset to be added to each location *)
exception NoWellTypedInterpretation of
- int * (Token.flocation option * string Lazy.t) list
+ int * ((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 *)
exception PathNotWellFormed
(** raised when an environment is not enough informative to decide *)
(match test_env aliases [] base_univ with
| Ok (thing, metasenv),new_univ ->
[ aliases, diff, metasenv, thing, new_univ ], []
(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),_ -> [],[diff,loc,msg])
| (locs,item) :: remaining_dom ->
debug_print (lazy (sprintf "CHOOSED ITEM: %s"
(string_of_domain_item item)));
| (locs,item) :: remaining_dom ->
debug_print (lazy (sprintf "CHOOSED ITEM: %s"
(string_of_domain_item item)));
| Some choices -> choices in
match choices with
[] ->
| Some choices -> choices in
match choices with
[] ->
- [], [Some (List.hd locs),
+ [], [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
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
remaining_dom new_univ)
| Uncertain (loc,msg),new_univ ->
(match remaining_dom with
+ | [] -> [], [diff,loc,msg]
| _ ->
aux new_env new_diff lookup_in_todo_dom
remaining_dom new_univ)
| _ ->
aux new_env new_diff lookup_in_todo_dom
remaining_dom new_univ)
- | Ko (loc,msg),_ -> [], [loc,msg])
+ | Ko (loc,msg),_ -> [], [diff,loc,msg])
| _::_ ->
let rec filter univ = function
| [] -> [],[]
| _::_ ->
let rec filter univ = function
| [] -> [],[]
(match test_env new_env remaining_dom univ with
| Ok (thing, metasenv),new_univ ->
(match remaining_dom with
(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
| _ -> aux new_env new_diff None remaining_dom new_univ
) @@
filter univ tl
| Uncertain (loc,msg),new_univ ->
(match remaining_dom with
+ | [] -> [],[diff,loc,msg]
| _ -> aux new_env new_diff None remaining_dom new_univ
) @@
filter univ tl
| _ -> aux new_env new_diff None remaining_dom new_univ
) @@
filter univ tl
- | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl)
+ | Ko (loc,msg),_ -> ([],[diff,loc,msg]) @@ filter univ tl)
in
filter base_univ choices
in
in
filter base_univ choices
in
(* the integer is an offset to be added to each location *)
exception NoWellTypedInterpretation of
(* the integer is an offset to be added to each location *)
exception NoWellTypedInterpretation of
- int * (Token.flocation option * string Lazy.t) list
+ int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Token.flocation option * string Lazy.t) list
exception PathNotWellFormed
val interpretate_path :
exception PathNotWellFormed
val interpretate_path :
metasenv,(GrafiteAst.Type (uri, tyno) :: types)
| _ ->
raise (GrafiteDisambiguator.DisambiguationError
metasenv,(GrafiteAst.Type (uri, tyno) :: types)
| _ ->
raise (GrafiteDisambiguator.DisambiguationError
- (0,[[None,lazy "Decompose works only on inductive types"]])))
+ (0,[[[],None,lazy "Decompose works only on inductive types"]])))
in
let metasenv,types =
List.fold_left disambiguate (metasenv,[]) types
in
let metasenv,types =
List.fold_left disambiguate (metasenv,[]) types
exception Ambiguous_input
(* the integer is an offset to be added to each location *)
exception DisambiguationError of
exception Ambiguous_input
(* the integer is an offset to be added to each location *)
exception DisambiguationError of
- int * (Token.flocation option * string Lazy.t) list list
+ int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ Token.flocation option * string Lazy.t) list list
(** parameters are: option name, error message *)
exception Unbound_identifier of string
(** parameters are: option name, error message *)
exception Unbound_identifier of string
exception Ambiguous_input
(* the integer is an offset to be added to each location *)
exception DisambiguationError of
exception Ambiguous_input
(* the integer is an offset to be added to each location *)
exception DisambiguationError of
- int * (Token.flocation option * string Lazy.t) list list
+ int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ Token.flocation option * string Lazy.t) list list
(** initially false; for debugging only (???) *)
val only_one_pass: bool ref
(** initially false; for debugging only (???) *)
val only_one_pass: bool ref
| phase::tl ->
let msg =
String.concat "\n\n\n"
| phase::tl ->
let msg =
String.concat "\n\n\n"
- (List.map (fun (floc,msg) ->
+ (List.map (fun (_,floc,msg) ->
let loc_descr =
match floc with
None -> ""
let loc_descr =
match floc with
None -> ""
(aux (n+1) (msg,[n]) tl) in
let loc =
match errorll with
(aux (n+1) (msg,[n]) tl) in
let loc =
match errorll with
- ((Some floc,_)::_)::_ ->
+ ((_,Some floc,_)::_)::_ ->
let (x, y) = HExtlib.loc_of_floc floc in
let x = x + offset in
let y = y + offset in
let (x, y) = HExtlib.loc_of_floc floc in
let x = x + offset in
let y = y + offset in