From 33bdd7e8c67299d34f05ac587488dd324fc6ba42 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 21 Nov 2008 16:00:06 +0000 Subject: [PATCH] loc * lazy string -> (loc * string) lazy --- .../cic_disambiguation/disambiguate.ml | 60 ++++++++++--------- .../cic_disambiguation/disambiguate.mli | 6 +- .../grafite_parser/grafiteDisambiguator.ml | 2 +- .../grafite_parser/grafiteDisambiguator.mli | 2 +- .../ng_disambiguation/nDisambiguate.ml | 21 +++---- .../components/ng_kernel/nCicUntrusted.mli | 2 +- .../components/ng_refiner/nCicRefiner.mli | 4 +- helm/software/matita/matitaExcPp.ml | 31 +++++----- helm/software/matita/matitaExcPp.mli | 8 ++- helm/software/matita/matitaGui.ml | 6 +- 10 files changed, 74 insertions(+), 68 deletions(-) diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 45186669d..9d42899c6 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -37,7 +37,7 @@ exception NoWellTypedInterpretation of int * ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Stdpp.location option * string Lazy.t * bool) list + (Stdpp.location * string) Lazy.t * bool) list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) @@ -105,8 +105,8 @@ let descr_of_domain_item = function type ('term,'metasenv,'subst,'graph) test_result = | Ok of 'term * 'metasenv * 'subst * 'graph - | Ko of Stdpp.location option * string Lazy.t - | Uncertain of Stdpp.location option * string Lazy.t + | Ko of (Stdpp.location * string) Lazy.t + | Uncertain of (Stdpp.location * string) Lazy.t let refine_term metasenv subst context uri term ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) @@ -120,17 +120,17 @@ let refine_term metasenv subst context uri term ugraph ~localization_tbl = exn -> let rec process_exn loc = function - HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn + HExtlib.Localized (loc,exn) -> process_exn loc exn | CicRefine.Uncertain msg -> debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; - Uncertain (loc,msg) + Uncertain (lazy (loc,Lazy.force msg)) | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppterm term) (Lazy.force msg))); - Ko (loc,msg) + Ko (lazy (loc,Lazy.force msg)) | exn -> raise exn in - process_exn None exn + process_exn Stdpp.dummy_loc exn let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = assert (context = []); @@ -146,18 +146,18 @@ let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = exn -> let rec process_exn loc = function - HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn + HExtlib.Localized (loc,exn) -> process_exn loc exn | CicRefine.Uncertain msg -> debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; - Uncertain (loc,msg) + Uncertain (lazy (loc,Lazy.force msg)) | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppobj obj) (Lazy.force msg))) ; - Ko (loc,msg) + Ko (lazy (loc,Lazy.force msg)) | exn -> raise exn in - process_exn None exn + process_exn Stdpp.dummy_loc exn let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try @@ -1146,8 +1146,9 @@ let foo () = k in refine_profiler.HExtlib.profile foo () with - | Try_again msg -> Uncertain (None,msg) - | Invalid_choice (loc,msg) -> Ko (loc,msg) + | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) + | Invalid_choice (None,msg) -> Ko(lazy (Stdpp.dummy_loc,Lazy.force msg)) + | Invalid_choice (Some loc,msg) -> Ko (lazy (loc,Lazy.force msg)) in (* (4) build all possible interpretations *) let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in @@ -1161,9 +1162,9 @@ in refine_profiler.HExtlib.profile foo () (match test_env aliases rem_dom base_univ with | Ok (thing, metasenv,subst,new_univ) -> [ aliases, diff, metasenv, subst, thing, new_univ ], [], [] - | Ko (loc,msg) -> [],[],[aliases,diff,loc,msg,true] - | Uncertain (loc,msg) -> - [],[aliases,diff,loc,msg],[]) + | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true] + | Uncertain loc_msg -> + [],[aliases,diff,loc_msg],[]) | Node (locs,item,inner_dom) :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); @@ -1174,8 +1175,9 @@ in refine_profiler.HExtlib.profile foo () match choices with [] -> [], [], - [aliases, diff, Some (List.hd locs), - lazy ("No choices for " ^ string_of_domain_item item), + [aliases, diff, + (lazy (List.hd locs, + "No choices for " ^ string_of_domain_item item)), true] (* | [codomain_item] -> @@ -1215,8 +1217,8 @@ in refine_profiler.HExtlib.profile foo () | _::_ -> let mark_not_significant failures = List.map - (fun (env, diff, loc, msg, _b) -> - env, diff, loc, msg, false) + (fun (env, diff, loc_msg, _b) -> + env, diff, loc_msg, false) failures in let classify_errors ((ok_l,uncertain_l,error_l) as outcome) = if ok_l <> [] || uncertain_l <> [] then @@ -1245,18 +1247,18 @@ in refine_profiler.HExtlib.profile foo () ) in res @@ filter tl - | Uncertain (loc,msg) -> + | Uncertain loc_msg -> let res = (match inner_dom with - | [] -> [],[new_env,new_diff,loc,msg],[] + | [] -> [],[new_env,new_diff,loc_msg],[] | _ -> aux new_env new_diff None inner_dom (remaining_dom@rem_dom) ) in res @@ filter tl - | Ko (loc,msg) -> - let res = [],[],[new_env,new_diff,loc,msg,true] in + | Ko loc_msg -> + let res = [],[],[new_env,new_diff,loc_msg,true] in res @@ filter tl) in let ok_l,uncertain_l,error_l = @@ -1269,7 +1271,7 @@ in refine_profiler.HExtlib.profile foo () ) ok_l ([],[],error_l) in List.fold_right - (fun (env,diff,_,_) res -> + (fun (env,diff,_) res -> aux env diff None remaining_dom rem_dom @@ res ) uncertain_l res_after_ok_l in @@ -1278,19 +1280,19 @@ in refine_profiler.HExtlib.profile foo () | Ok _ | Uncertain _ -> aux aliases diff lookup_in_todo_dom todo_dom [] - | Ko (loc,msg) -> [],[],[aliases,diff,loc,msg,true] in + | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in try let res = match aux' aliases [] None todo_dom with | [],uncertain,errors -> let errors = List.map - (fun (env,diff,loc,msg) -> (env,diff,loc,msg,true) + (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true) ) uncertain @ errors in let errors = List.map - (fun (env,diff,loc,msg,significant) -> + (fun (env,diff,loc_msg,significant) -> let env' = filter_map_domain (fun locs domain_item -> @@ -1303,7 +1305,7 @@ in refine_profiler.HExtlib.profile foo () Not_found -> None) thing_dom in - env',diff,loc,msg,significant + env',diff,loc_msg,significant ) errors in raise (NoWellTypedInterpretation (0,errors)) diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli index b21c2bbe0..bb4c72640 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.mli +++ b/helm/software/components/cic_disambiguation/disambiguate.mli @@ -37,7 +37,7 @@ exception NoWellTypedInterpretation of int * ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Stdpp.location option * string Lazy.t * bool) list + (Stdpp.location * string) Lazy.t * bool) list exception PathNotWellFormed val interpretate_path : @@ -51,8 +51,8 @@ and domain_tree = type ('term,'metasenv,'subst,'graph) test_result = | Ok of 'term * 'metasenv * 'subst * 'graph - | Ko of Stdpp.location option * string Lazy.t - | Uncertain of Stdpp.location option * string Lazy.t + | Ko of (Stdpp.location * string) Lazy.t + | Uncertain of (Stdpp.location * string) Lazy.t exception Try_again of string Lazy.t diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml index 46b8397ba..5d803e979 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml @@ -37,7 +37,7 @@ exception DisambiguationError of int * ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Stdpp.location option * string Lazy.t * bool) list list + (Stdpp.location * string) Lazy.t * bool) list list (** parameters are: option name, error message *) exception Unbound_identifier of string diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.mli b/helm/software/components/grafite_parser/grafiteDisambiguator.mli index 88940c2c3..d6ff0be4c 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguator.mli @@ -31,7 +31,7 @@ exception DisambiguationError of int * ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Stdpp.location option * string Lazy.t * bool) list list + (Stdpp.location * string) Lazy.t * bool) list list (** parameters are: option name, error message *) (** initially false; for debugging only (???) *) diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml index 40ed34b5f..2aa873724 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nDisambiguate.ml @@ -34,27 +34,27 @@ module Ast = CicNotationPt let debug_print _ = ();; -let refine_term metasenv subst context uri term ugraph ~localization_tbl = +let refine_term metasenv subst context uri term _ ~localization_tbl = assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (NCicPp.ppterm ~metasenv ~subst ~context term))); try let localise t = - try NCic.NCicHash.find localization_tbl t + try NCicUntrusted.NCicHash.find localization_tbl t with Not_found -> assert false in - let metasenv, subst, term, ty = - NCicRefine.typeof metasenv subst context term None ~localise + let metasenv, subst, term, _ = + NCicRefiner.typeof metasenv subst context term None ~localise in Disambiguate.Ok (term, metasenv, subst, ()) with - | NCicRefine.Uncertain (loc, msg) -> - debug_print (lazy ("UNCERTAIN: [" ^ Lazy.force msg ^ "] " ^ + | NCicRefiner.Uncertain (msg) -> + debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force msg) ^ "] " ^ NCicPp.ppterm ~metasenv ~subst ~context term)) ; - Disambiguate.Uncertain (loc,msg,()) - | NCicRefine.RefineFailure (loc,msg) -> + Disambiguate.Uncertain (loc,msg) + | NCicRefiner.RefineFailure (msg) -> debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s" - (NCicPp.ppterm ~metasenv ~subst ~context term) (Lazy.force msg))); + (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force msg)))); Disambiguate.Ko (loc,msg,()) ;; @@ -458,12 +458,9 @@ let interpretate_term let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl = - assert false -(* let context = List.map (function None -> NCic.Anonymous | Some (n,_) -> n) context in interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast ~localization_tbl -*) ;; let domain_of_term ~context = diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli index f752c01dc..b195760cb 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.mli +++ b/helm/software/components/ng_kernel/nCicUntrusted.mli @@ -17,5 +17,5 @@ val map_term_fold_a: val metas_of_term : NCic.substitution -> NCic.context -> NCic.term -> int list -module NCicHash : Hashtbl.S +module NCicHash : Hashtbl.S with type key = NCic.term diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli index 5d845eb1f..9b10e3448 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.mli +++ b/helm/software/components/ng_refiner/nCicRefiner.mli @@ -11,8 +11,8 @@ (* $Id$ *) -exception RefineFailure of Stdpp.location * (string Lazy.t);; -exception Uncertain of Stdpp.location * (string Lazy.t);; +exception RefineFailure of (Stdpp.location * string) Lazy.t;; +exception Uncertain of (Stdpp.location * string) Lazy.t;; exception AssertFailure of string Lazy.t;; val typeof : diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index 076a5d763..17cc7c942 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -33,8 +33,9 @@ let compact_disambiguation_errors all_passes errorll = (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 @@ -152,13 +153,16 @@ let rec to_string = | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> 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 + | ((_,_,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 @@ -182,11 +186,10 @@ let rec to_string = 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, diff --git a/helm/software/matita/matitaExcPp.mli b/helm/software/matita/matitaExcPp.mli index 419b04c73..77a5a3ce9 100644 --- a/helm/software/matita/matitaExcPp.mli +++ b/helm/software/matita/matitaExcPp.mli @@ -27,7 +27,11 @@ val compact_disambiguation_errors : bool -> (int * ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Stdpp.location option * string Lazy.t * bool) list) list -> - (Stdpp.location option * (int list * (int list * (Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list) list * string Lazy.t * bool) list) list + (Stdpp.location * string) Lazy.t * bool) list) list -> + (Stdpp.location * + (int list * + (int list * (Stdpp.location list * string * string) list * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list) list * + string Lazy.t * bool) list) list val to_string: exn -> Stdpp.location option * string diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 8bc226ed4..ac34052c1 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -220,7 +220,7 @@ let rec interactive_error_interp ~all_passes assert (List.flatten errorll <> []); let errorll' = let remove_non_significant = - List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in + List.filter (fun (_env,_diff,_loc_msg,significant) -> significant) in let annotated_errorll () = List.rev (snd @@ -264,7 +264,7 @@ let rec interactive_error_interp ~all_passes let _,env,diff = List.hd envs_and_diffs in notify_exn (GrafiteDisambiguator.DisambiguationError - (offset,[[env,diff,loffset,msg,significant]])); + (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]])); | _::_ -> let dialog = new disambiguationErrors () in dialog#check_widgets (); @@ -299,7 +299,7 @@ let rec interactive_error_interp ~all_passes ~stop:source_buffer#end_iter; notify_exn (GrafiteDisambiguator.DisambiguationError - (offset,[[env,diff,loffset,msg,significant]])) + (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]])) )); let return _ = dialog#disambiguationErrors#destroy (); -- 2.39.2