(* 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) list
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 ], []
- | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[diff,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
[] ->
- [], [diff,
+ [], [aliases, diff,
Some (List.hd locs),
lazy ("No choices for " ^ string_of_domain_item item)]
| [codomain_item] ->
remaining_dom new_univ)
| Uncertain (loc,msg),new_univ ->
(match remaining_dom with
- | [] -> [], [new_diff,loc,msg]
+ | [] -> [], [new_env,new_diff,loc,msg]
| _ ->
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])
| _::_ ->
let rec filter univ = function
| [] -> [],[]
filter univ tl
| Uncertain (loc,msg),new_univ ->
(match remaining_dom with
- | [] -> [],[new_diff,loc,msg]
+ | [] -> [],[new_env,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)
+ | Ko (loc,msg),_ -> ([],[new_env,new_diff,loc,msg]) @@ filter univ tl)
in
filter base_univ choices
in
try
let res =
match aux aliases [] None todo_dom base_univ with
- | [],errors -> raise (NoWellTypedInterpretation (0,errors))
+ | [],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
(* 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) list
exception PathNotWellFormed
val interpretate_path :
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
exception Ambiguous_input
(* the integer is an offset to be added to each location *)
exception DisambiguationError of
- int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- Token.flocation option * string Lazy.t) list list
+ int *
+ ((Token.flocation list * string * string) list *
+ (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
exception Ambiguous_input
(* the integer is an offset to be added to each location *)
exception DisambiguationError of
- int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- Token.flocation option * string Lazy.t) list list
+ int *
+ ((Token.flocation list * string * string) list *
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ Token.flocation option * string Lazy.t) list list
+ (** parameters are: option name, error message *)
(** initially false; for debugging only (???) *)
val only_one_pass: bool ref
| 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 -> ""
(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 idx = ref 0 in
fun interp ->
try
- List.assoc "0" interp
+ let _,_,y = List.find (fun (_,x,y) -> x="0") interp in y
with Not_found ->
incr idx; string_of_int !idx
in
tree_store#clear ();
let idx = ref ~-1 in
List.iter
- (fun _,interp,_,_ ->
+ (fun pass,env,_,_,_ ->
incr idx;
let interp_row = tree_store#append () in
tree_store#set ~row:interp_row ~column:id_col
- (name_of_interp interp);
+ ("Pass " ^ string_of_int pass ^
+ "; Interpretation " ^ name_of_interp env);
tree_store#set ~row:interp_row ~column:interp_no_col !idx;
List.iter
- (fun (id, dsc) ->
+ (fun (_, id, dsc) ->
let row = tree_store#append ~parent:interp_row () in
tree_store#set ~row ~column:id_col id;
tree_store#set ~row ~column:dsc_col dsc;
tree_store#set ~row ~column:interp_no_col !idx)
- interp)
+ env)
choices
method get_interp_no tree_path =
let errorll' =
if all_passes then errorll else List.rev (List.tl (List.tl (List.rev errorll))) in
let choices =
+ let pass = ref 0 in
List.flatten
(List.map
- (List.map
- (fun (choices,offset,msg) ->
- let textual_choices =
- List.map
- (fun (dom,(descr,_)) ->
- DisambiguateTypes.string_of_domain_item dom, descr
- ) choices
- in
- choices, textual_choices, offset, msg
- )
+ (fun l ->
+ incr pass;
+ List.map (fun (env,diff,offset,msg) -> !pass, env, diff, offset, msg) l
) errorll') in
- let choices_eq (_,c1,_,_) (_,c2,_,_) = c1 = c2 in
- let choices_compare (_,c1,_,_) (_,c2,_,_) = compare c1 c2 in
+ let choices_eq (_,e1,_,_,_) (_,e2,_,_,_) = e1 = e2 in
+ let choices_compare (_,e1,_,_,_) (_,e2,_,_,_) = compare e1 e2 in
(* Here we are doing a stable sort and list_uniq returns the latter
"equal" element. I.e. we are showing the error corresponding to the
most advanced disambiguation pass *)
in
match choices with
[] -> assert false
- | [interp,_,loffset,msg] ->
+ | [_,env,diff,loffset,msg] ->
notify_exn
(GrafiteDisambiguator.DisambiguationError
- (offset,[[interp,loffset,msg]]));
+ (offset,[[env,diff,loffset,msg]]));
| _::_ ->
let dialog = new disambiguationErrors () in
dialog#check_widgets ();
None -> assert false
| Some tp -> tp in
let idx = model#get_interp_no tree_path in
- let interp,_,loffset,msg = List.nth choices idx in
+ let _,env,diff,loffset,msg = List.nth choices idx in
let script = MatitaScript.current () in
let error_tag = script#error_tag in
source_buffer#remove_tag error_tag
~stop:source_buffer#end_iter;
notify_exn
(GrafiteDisambiguator.DisambiguationError
- (offset,[[interp,loffset,msg]]))
+ (offset,[[env,diff,loffset,msg]]))
));
let return _ =
dialog#disambiguationErrors#destroy ();
projects / helm.git / commitdiff