module Ast = NotationPt
-(* hard errors, spurious errors *)
-exception NoWellTypedInterpretation of
- ((Stdpp.location * string) list *
- (Stdpp.location * string) list)
+exception NoWellTypedInterpretation of (Stdpp.location * string)
exception PathNotWellFormed
* node; each ast is associated with the actual instantiation of the node,
* the refinement error, and the location at which refinement fails *)
| Disamb_failure of
- (* hard errors, spurious errors *)
- (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list *
(('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list
let resolve ~env ~universe ~mk_choice item interpr arg =
(*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
| Invalid_choice loc_msg -> Ko loc_msg*)
| Invalid_choice x ->
- let loc,err = Lazy.force x in Some (loc,err)
- | _ -> None
+ let loc,err = Lazy.force x in
+ debug_print (lazy ("test_interpr invalid choice: " ^ err));
+ Some (loc,err)
+ | e -> debug_print (lazy ("uncaught error: "^ Printexc.to_string e));None
;;
exception Not_ambiguous;;
"\nin " ^ pp_thing (ctx t)));
(* get possible instantiations of t *)
let instances = get_instances ctx t in
+ if instances = [] then
+ raise (NoWellTypedInterpretation (loc_t, "No choices for " ^ astpp t));
debug_print (lazy "-- possible instances:");
(* List.iter
(fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0))))
match refine_thing metasenv subst context uri ~use_coercions t' expty
base_univ ~localization_tbl with
| Ok (t',m',s',u') -> t,m',s',t',u'
- | Uncertain x ->
- let _,err = Lazy.force x in
+ | Uncertain x | Ko x ->
+ let loc,err = Lazy.force x in
debug_print (lazy ("refinement uncertain after disambiguation: " ^ err));
- assert false
- | _ -> assert false
+ raise (NoWellTypedInterpretation (loc,err))
in
match (test_interpr thing) with
| Some (loc,err) ->
-(* debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); *)
- Disamb_failure ([[thing,None,loc,err],loc],[])
+ debug_print (lazy ("preliminary test fail: " ^ pp_thing thing));
+ Disamb_failure ([[thing,None,loc,err],loc])
| None ->
let res,errors = aux [thing] in
- let res =
- HExtlib.filter_map (fun t ->
- try Some (refine t)
- with _ ->
-(* debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));*)
- None) res
+ let res,inner_errors =
+ List.split
+ (List.map (fun t ->
+ try (Some (refine t), None)
+ (* this error is actually a singleton *)
+ with NoWellTypedInterpretation loc_err ->
+ debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));
+ None, Some loc_err) res) in
+ let res = HExtlib.filter_map (fun x -> x) res in
+ let inner_errors =
+ HExtlib.filter_map
+ (function Some (loc,err) -> Some (thing,None,loc,err) | None -> None)
+ inner_errors
+ in
+ let errors =
+ if inner_errors <> [] then (inner_errors,Stdpp.dummy_loc)::errors
+ else errors
in
(match res with
- | [] -> Disamb_failure (errors,[])
+ | [] -> prerr_endline ((string_of_int (List.length errors)) ^ " error frames");Disamb_failure errors
| _ -> Disamb_success res)
;;