(List.map
(fun (pass,l) ->
List.map
- (fun (env,diff,offset,msg,significant) ->
- offset, [[pass], [[pass], env, diff], msg, significant]) l
+ (fun (env,diff,offset_msg,significant) ->
+ let offset, msg = Lazy.force offset_msg in
+ offset, [[pass], [[pass], env, diff], lazy msg, significant]) l
) errorll) 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
let _,msg = to_string exn in
let (x, y) = HExtlib.loc_of_floc floc in
Some floc, sprintf "Error at %d-%d: %s" x y msg
- | GrafiteTypes.Option_error ("baseuri", "not found" ) ->
- None,
- "Baseuri not set for this script. "
- ^ "Use 'set \"baseuri\" \"<uri>\".' to set it."
| GrafiteTypes.Command_error msg -> None, "Error: " ^ msg
| CicNotationParser.Parse_error err ->
None, sprintf "Parse error: %s" err
| CicRefine.RefineFailure msg
| CicRefine.AssertFailure msg ->
None, "Refiner error: " ^ Lazy.force msg
+ | NCicRefiner.RefineFailure msg ->
+ None, "NRefiner failure: " ^ snd (Lazy.force msg)
+ | NCicRefiner.Uncertain msg ->
+ None, "NRefiner uncertain: " ^ snd (Lazy.force msg)
+ | NCicMetaSubst.Uncertain msg ->
+ None, "NCicMetaSubst uncertain: " ^ Lazy.force msg
+ | NCicTypeChecker.TypeCheckerFailure msg ->
+ None, "NTypeChecker failure: " ^ Lazy.force msg
+ | NCicTypeChecker.AssertFailure msg ->
+ None, "NTypeChecker assert failure: " ^ Lazy.force msg
+ | NCicRefiner.AssertFailure msg ->
+ None, "NRefiner assert failure: " ^ Lazy.force msg
+ | NCicEnvironment.BadDependency (msg,e) ->
+ None, "NCicEnvironment bad dependency: " ^ Lazy.force msg ^
+ snd (to_string e)
+ | NCicEnvironment.BadConstraint msg ->
+ None, "NCicEnvironment bad constraint: " ^ Lazy.force msg
| CicTypeChecker.TypeCheckerFailure msg ->
None, "Type checking error: " ^ Lazy.force msg
| CicTypeChecker.AssertFailure msg ->
None, "Type checking assertion failed: " ^ Lazy.force msg
| LibrarySync.AlreadyDefined s ->
None, "Already defined: " ^ UriManager.string_of_uri s
- | CoercDb.EqCarrNotImplemented msg ->
- None, ("EqCarrNotImplemented: " ^ Lazy.force msg)
- | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+ | DisambiguateChoices.Choice_not_found msg ->
+ None, ("Disambiguation choice not found: " ^ Lazy.force msg)
+ | MatitaEngine.EnrichedWithStatus (exn,_,_) ->
+ None, "EnrichedWithStatus "^snd(to_string exn)
+ | NTacStatus.Error msg ->
+ None, "NTactic error: " ^ Lazy.force msg
+ | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+ let loc =
+ match errorll with
+ | ((_,_,loc_msg,_)::_)::_ ->
+ let floc, _ = Lazy.force loc_msg in
+ if floc = Stdpp.dummy_loc then None else
+ let (x, y) = HExtlib.loc_of_floc floc in
+ let x = x + offset in
+ let y = y + offset in
+ let floc = HExtlib.floc_of_loc (x,y) in
+ Some floc
+ | _ -> assert false
+ in
+ let annotated_errorll =
+ List.rev
+ (snd
+ (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res)
+ (0,[]) errorll)) in
+ let choices = compact_disambiguation_errors true annotated_errorll in
+ let errorll =
+ (List.map
+ (function (loffset,l) ->
+ List.map
+ (function
+ passes,envs_and_diffs,msg,significant ->
+ let _,env,diff = List.hd envs_and_diffs in
+ passes,env,diff,loffset,msg,significant
+ ) l
+ ) choices) in
let rec aux =
function
[] -> []
let msg =
(List.map (fun (passes,_,_,floc,msg,significant) ->
let loc_descr =
- match floc with
- None -> ""
- | Some floc ->
- let (x, y) = HExtlib.loc_of_floc floc in
- sprintf " at %d-%d" (x+offset) (y+offset)
+ if floc = HExtlib.dummy_floc then ""
+ else
+ let (x, y) = HExtlib.loc_of_floc floc in
+ sprintf " at %d-%d" (x+offset) (y+offset)
in
"*" ^ (if not significant then "(Spurious?) " else "")
^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg,
passes) phase)
in
msg@aux tl in
- let loc =
- match errorll with
- ((_,_,Some floc,_,_)::_)::_ ->
- let (x, y) = HExtlib.loc_of_floc floc in
- let x = x + offset in
- let y = y + offset in
- let floc = HExtlib.floc_of_loc (x,y) in
- Some floc
- | _ -> None in
let rec explain =
function
[] -> ""
String.concat "," (List.map string_of_int phases) ^": *****\n"^
msg ^ "\n\n"
in
- (* --- *)
- let annotated_errorll =
- List.rev
- (snd
- (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res) (0,[])
- errorll)) in
- let choices = compact_disambiguation_errors true annotated_errorll in
- (* --- *)
- let errorll =
- (List.map
- (function (loffset,l) ->
- List.map
- (function
- passes,envs_and_diffs,msg,significant ->
- let _,env,diff = List.hd envs_and_diffs in
- passes,env,diff,loffset,msg,significant
- ) l
- ) choices) in
- (* --- *)
-
loc,
"********** DISAMBIGUATION ERRORS: **********\n" ^
explain (aux errorll)