From 8d8ac4a42998970114e43c2fb13ff2c98f7c259a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 26 Nov 2005 15:49:23 +0000 Subject: [PATCH] Experimental localization of errors during refinement and disambiguation. --- helm/matita/matitaDisambiguator.ml | 3 +- helm/matita/matitaDisambiguator.mli | 3 +- helm/matita/matitaEngine.ml | 2 +- helm/matita/matitaExcPp.ml | 18 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 108 +++++---- .../ocaml/cic_disambiguation/disambiguate.mli | 3 +- helm/ocaml/cic_unification/cicRefine.ml | 210 +++++------------- helm/ocaml/cic_unification/cicRefine.mli | 10 +- 8 files changed, 155 insertions(+), 202 deletions(-) diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index 0f4dc67db..d46f9a1bf 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -28,7 +28,8 @@ open Printf open MatitaTypes exception Ambiguous_input -exception DisambiguationError of string Lazy.t list list +exception DisambiguationError of + (Token.flocation option * string Lazy.t) list list type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli index 7e207e12f..64cd5563b 100644 --- a/helm/matita/matitaDisambiguator.mli +++ b/helm/matita/matitaDisambiguator.mli @@ -28,7 +28,8 @@ open MatitaTypes (** raised when ambiguous input is found but not expected (e.g. in the batch * compiler) *) exception Ambiguous_input -exception DisambiguationError of string Lazy.t list list +exception DisambiguationError of + (Token.flocation option * string Lazy.t) list list type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list type choose_interp_callback = (string * string) list list -> int list diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index b62dd23de..72b252140 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -253,7 +253,7 @@ let disambiguate_tactic status goal tactic = with | Cic.MutInd (uri, tyno, _) -> (GrafiteAst.Type (uri, tyno) :: types) - | _ -> raise (MatitaDisambiguator.DisambiguationError [[lazy "Decompose works only on inductive types"]])) + | _ -> raise (MatitaDisambiguator.DisambiguationError [[None,lazy "Decompose works only on inductive types"]])) in let types = List.fold_left disambiguate [] types in GrafiteAst.Decompose (loc, types, what, names) diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index 2d0f60c9e..38951713e 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -69,10 +69,22 @@ let rec to_string = aux (n+1) tl ^ "***** Errors obtained during phase " ^ string_of_int n ^": *****\n"^ String.concat "\n\n" - (List.map (fun msg -> "*Error: " ^ Lazy.force msg) phase) ^ - "\n\n\n" + (List.map (fun (floc,msg) -> + let loc_descr = + match floc with + None -> "" + | Some floc -> + let (x, y) = HExtlib.loc_of_floc floc in + sprintf " at %d-%d" x y + in + "*Error" ^ loc_descr ^ ": " ^ Lazy.force msg) phase) ^ + "\n\n\n" in + let loc = + match errorll with + ((Some _ as loc,_)::_)::_ -> loc + | _ -> None in - None, + loc, "********** DISAMBIGUATION ERRORS: **********\n" ^ aux 1 errorll | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 41025ee3a..ce26f9351 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -28,7 +28,8 @@ open Printf open DisambiguateTypes open UriManager -exception NoWellTypedInterpretation of string Lazy.t list +exception NoWellTypedInterpretation of + (Token.flocation option * string Lazy.t) list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) @@ -55,40 +56,56 @@ let descr_of_domain_item = function type 'a test_result = | Ok of 'a * Cic.metasenv - | Ko of string Lazy.t - | Uncertain of string Lazy.t + | Ko of Token.flocation option * string Lazy.t + | Uncertain of Token.flocation option * string Lazy.t -let refine_term metasenv context uri term ugraph = +let refine_term metasenv context uri term ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); try let term', _, metasenv',ugraph1 = - CicRefine.type_of_aux' metasenv context term ugraph in + CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in (Ok (term', metasenv')),ugraph1 with - | CicRefine.Uncertain msg -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; - Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) (Lazy.force msg))); - Ko (msg (*lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph + exn -> + let rec process_exn loc = + function + HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; + Uncertain (loc,msg),ugraph + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppterm term) (Lazy.force msg))); + Ko (loc,msg),ugraph + | exn -> raise exn + in + process_exn None exn -let refine_obj metasenv context uri obj ugraph = +let refine_obj metasenv context uri obj ugraph ~localization_tbl = assert (context = []); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; try - let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in + let obj', metasenv,ugraph = + CicRefine.typecheck metasenv uri obj ~localization_tbl + in (Ok (obj', metasenv)),ugraph with - | CicRefine.Uncertain msg -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; - Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) (Lazy.force msg))) ; - Ko (msg (*lazy ("Error trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph + exn -> + let rec process_exn loc = + function + HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; + Uncertain (loc,msg),ugraph + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppobj obj) (Lazy.force msg))) ; + Ko (loc,msg),ugraph + | exn -> raise exn + in + process_exn None exn let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try @@ -106,11 +123,15 @@ let find_in_context name (context: Cic.name list) = in aux 1 context -let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = +let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast + ~localization_tbl += assert (uri = None); let rec aux loc (context: Cic.name list) = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> - aux loc context term + let res = aux loc context term in + Cic.CicHash.add localization_tbl res loc; + res | CicNotationPt.AttributedTerm (_, term) -> aux loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux loc context) args in @@ -352,16 +373,19 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | None -> Cic.Implicit annotation | Some term -> aux loc context term in - match ast with - | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term - | term -> aux dummy_floc context term + aux dummy_floc context ast let interpretate_path ~context path = - interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true path + let localization_tbl = Cic.CicHash.create 23 in + (* here we are throwing away useful localization informations!!! *) + fst ( + interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true + path ~localization_tbl, localization_tbl) -let interpretate_obj ~context ~env ~uri ~is_path obj = +let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = assert (context = []); assert (is_path = false); + let interpretate_term = interpretate_term ~localization_tbl in match obj with | CicNotationPt.Inductive (params,tyl) -> let uri = match uri with Some uri -> uri | None -> assert false in @@ -808,17 +832,20 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" aliases todo_dom in try + let localization_tbl = Cic.CicHash.create 503 in let cic_thing = interpretate_thing ~context:disambiguate_context ~env:filled_env - ~uri ~is_path:false thing + ~uri ~is_path:false thing ~localization_tbl in let foo () = - let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in + let k,ugraph1 = + refine_thing metasenv context uri cic_thing ugraph ~localization_tbl + in (k , ugraph1 ) in refine_profiler.HExtlib.profile foo () with - | Try_again msg -> Uncertain msg, ugraph - | Invalid_choice msg -> Ko msg, ugraph + | Try_again msg -> Uncertain (None,msg), ugraph + | Invalid_choice msg -> Ko (None,msg), ugraph in (* (4) build all possible interpretations *) let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in @@ -829,7 +856,7 @@ in refine_profiler.HExtlib.profile foo () (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> [ aliases, diff, metasenv, thing, new_univ ], [] - | Ko msg,_ | Uncertain msg,_ -> [],[msg]) + | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg]) | item :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); @@ -838,7 +865,8 @@ in refine_profiler.HExtlib.profile foo () None -> lookup_choices item | Some choices -> choices in match choices with - [] -> [], [lazy ("No choices for " ^ string_of_domain_item item)] + [] -> + [], [None,lazy ("No choices for " ^ string_of_domain_item item)] | [codomain_item] -> (* just one choice. We perform a one-step look-up and if the next set of choices is also a singleton we @@ -865,13 +893,13 @@ in refine_profiler.HExtlib.profile foo () | _ -> aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) - | Uncertain msg,new_univ -> + | Uncertain (loc,msg),new_univ -> (match remaining_dom with - | [] -> [], [msg] + | [] -> [], [loc,msg] | _ -> aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) - | Ko msg,_ -> [], [msg]) + | Ko (loc,msg),_ -> [], [loc,msg]) | _::_ -> let rec filter univ = function | [] -> [],[] @@ -886,13 +914,13 @@ in refine_profiler.HExtlib.profile foo () | _ -> aux new_env new_diff None remaining_dom new_univ ) @@ filter univ tl - | Uncertain msg,new_univ -> + | Uncertain (loc,msg),new_univ -> (match remaining_dom with - | [] -> [],[msg] + | [] -> [],[loc,msg] | _ -> aux new_env new_diff None remaining_dom new_univ ) @@ filter univ tl - | Ko msg,_ -> ([],[msg]) @@ filter univ tl) + | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl) in filter base_univ choices in diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index f0ca92db0..fc88b6cf8 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -25,7 +25,8 @@ (** {2 Disambiguation interface} *) -exception NoWellTypedInterpretation of string Lazy.t list +exception NoWellTypedInterpretation of + (Token.flocation option * string Lazy.t) list exception PathNotWellFormed val interpretate_path : diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index d3a297d43..ccf662f18 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -43,11 +43,25 @@ in profiler.HExtlib.profile foo () | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; -let enrich f = - function - RefineFailure msg -> raise (RefineFailure (f msg)) - | Uncertain msg -> raise (Uncertain (f msg)) - | _ -> assert false +let enrich loc f exn = + let exn' = + match exn with + RefineFailure msg -> RefineFailure (f msg) + | Uncertain msg -> Uncertain (f msg) + | _ -> assert false + in + match loc with + None -> raise exn' + | Some loc -> raise (HExtlib.Localized (loc,exn')) + +let relocalize localization_tbl oldt newt = + try + let infos = Cic.CicHash.find localization_tbl oldt in + Cic.CicHash.remove localization_tbl oldt; + Cic.CicHash.add localization_tbl newt infos; + with + Not_found -> () +;; let rec split l n = match (l,n) with @@ -56,128 +70,20 @@ let rec split l n = | (_,_) -> raise (AssertFailure (lazy "split: list too short")) ;; -let exp_impl metasenv subst context term = - let rec aux metasenv context = function - | (Cic.Rel _) as t -> metasenv, t - | (Cic.Sort _) as t -> metasenv, t - | Cic.Const (uri, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.Const (uri, subst') - | Cic.Var (uri, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.Var (uri, subst') - | Cic.MutInd (uri, i, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.MutInd (uri, i, subst') - | Cic.MutConstruct (uri, i, j, subst) -> - let metasenv', subst' = do_subst metasenv context subst in - metasenv', Cic.MutConstruct (uri, i, j, subst') - | Cic.Meta (n,l) -> - let metasenv', l' = do_local_context metasenv context l in - metasenv', Cic.Meta (n, l') - | Cic.Implicit (Some `Type) -> +let exp_impl metasenv subst context = + function + | Some `Type -> let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in metasenv', Cic.Meta (idx, irl) - | Cic.Implicit (Some `Closed) -> + | Some `Closed -> let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in metasenv', Cic.Meta (idx, []) - | Cic.Implicit None -> + | None -> let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in metasenv', Cic.Meta (idx, irl) - | Cic.Implicit _ -> assert false - | Cic.Cast (te, ty) -> - let metasenv', ty' = aux metasenv context ty in - let metasenv'', te' = aux metasenv' context te in - metasenv'', Cic.Cast (te', ty') - | Cic.Prod (name, s, t) -> - let metasenv', s' = aux metasenv context s in - metasenv', Cic.Prod (name, s', t) - | Cic.Lambda (name, s, t) -> - let metasenv', s' = aux metasenv context s in - metasenv', Cic.Lambda (name, s', t) - | Cic.LetIn (name, s, t) -> - let metasenv', s' = aux metasenv context s in - metasenv', Cic.LetIn (name, s', t) - | Cic.Appl l when List.length l > 1 -> - let metasenv', l' = - List.fold_right - (fun term (metasenv, terms) -> - let new_metasenv, term = aux metasenv context term in - new_metasenv, term :: terms) - l (metasenv, []) - in - metasenv', Cic.Appl l' - | Cic.Appl _ -> assert false - | Cic.MutCase (uri, i, outtype, term, patterns) -> - let metasenv', l' = - List.fold_right - (fun term (metasenv, terms) -> - let new_metasenv, term = aux metasenv context term in - new_metasenv, term :: terms) - (outtype :: term :: patterns) (metasenv, []) - in - let outtype', term', patterns' = - match l' with - | outtype' :: term' :: patterns' -> outtype', term', patterns' - | _ -> assert false - in - metasenv', Cic.MutCase (uri, i, outtype', term', patterns') - | Cic.Fix (i, funs) -> - let metasenv', types = - List.fold_right - (fun (name, _, typ, _) (metasenv, types) -> - let new_metasenv, new_type = aux metasenv context typ in - (new_metasenv, (name, new_type) :: types)) - funs (metasenv, []) - in - let rec combine = function - | ((name, index, _, body) :: funs_tl), - ((_, typ) :: typ_tl) -> - (name, index, typ, body) :: combine (funs_tl, typ_tl) - | [], [] -> [] - | _ -> assert false - in - let funs' = combine (funs, types) in - metasenv', Cic.Fix (i, funs') - | Cic.CoFix (i, funs) -> - let metasenv', types = - List.fold_right - (fun (name, typ, _) (metasenv, types) -> - let new_metasenv, new_type = aux metasenv context typ in - (new_metasenv, (name, new_type) :: types)) - funs (metasenv, []) - in - let rec combine = function - | ((name, _, body) :: funs_tl), - ((_, typ) :: typ_tl) -> - (name, typ, body) :: combine (funs_tl, typ_tl) - | [], [] -> [] - | _ -> assert false - in - let funs' = combine (funs, types) in - metasenv', Cic.CoFix (i, funs') - and do_subst metasenv context subst = - List.fold_right - (fun (uri, term) (metasenv, substs) -> - let metasenv', term' = aux metasenv context term in - (metasenv', (uri, term') :: substs)) - subst (metasenv, []) - and do_local_context metasenv context local_context = - List.fold_right - (fun term (metasenv, local_context) -> - let metasenv', term' = - match term with - | None -> metasenv, None - | Some term -> - let metasenv', term' = aux metasenv context term in - metasenv', Some term' - in - metasenv', term' :: local_context) - local_context (metasenv, []) - in - aux metasenv context term + | _ -> assert false ;; let rec type_of_constant uri ugraph = @@ -294,8 +200,9 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) -and type_of_aux' metasenv context t ugraph = - let metasenv, t = exp_impl metasenv [] context t in +and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t + ugraph += let rec type_of_aux subst metasenv context t ugraph = let module C = Cic in let module S = CicSubstitution in @@ -358,7 +265,9 @@ and type_of_aux' metasenv context t ugraph = t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 | C.Sort _ -> t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph - | C.Implicit _ -> raise (AssertFailure (lazy "21")) + | C.Implicit infos -> + let metasenv',t' = exp_impl metasenv subst context infos in + type_of_aux subst metasenv' context t' ugraph | C.Cast (te,ty) -> let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph @@ -416,7 +325,6 @@ and type_of_aux' metasenv context t ugraph = s' sort1 subst' context metasenv' ugraph1 in let context_for_t = ((Some (name,(C.Decl s')))::context) in - let metasenv',t = exp_impl metasenv' subst' context_for_t t in let t',sort2,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context_for_t t ugraph1 @@ -452,7 +360,6 @@ and type_of_aux' metasenv context t ugraph = "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1)))) in let context_for_t = ((Some (n,(C.Decl s')))::context) in - let metasenv',t = exp_impl metasenv' subst' context_for_t t in let t',type2,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context_for_t t ugraph1 in @@ -464,7 +371,6 @@ and type_of_aux' metasenv context t ugraph = type_of_aux subst metasenv context s ugraph in let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in - let metasenv',t = exp_impl metasenv' subst' context_for_t t in let t',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' @@ -486,20 +392,13 @@ and type_of_aux' metasenv context t ugraph = let x',ty,subst',metasenv',ugraph1 = type_of_aux subst metasenv context x ugraph in - (x', ty)::res,subst',metasenv',ugraph1 + relocalize localization_tbl x x'; + (x', ty)::res,subst',metasenv',ugraph1 ) tl ([],subst',metasenv',ugraph1) in let tl',applty,subst''',metasenv''',ugraph3 = - try eat_prods true subst'' metasenv'' context hetype tlbody_and_type ugraph2 - with - exn -> - enrich - (fun msg -> - lazy ("The application " ^ - CicMetaSubst.ppterm_in_context subst'' t context ^ - " is not well typed:\n" ^ Lazy.force msg)) exn in C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments")) @@ -819,7 +718,6 @@ and type_of_aux' metasenv context t ugraph = let fl_bo',subst,metasenv,ugraph2 = List.fold_left (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) -> - let metasenv, bo = exp_impl metasenv subst context' bo in let bo',ty_of_bo,subst,metasenv,ugraph1 = type_of_aux subst metasenv context' bo ugraph in @@ -861,7 +759,6 @@ and type_of_aux' metasenv context t ugraph = let fl_bo',subst,metasenv,ugraph2 = List.fold_left (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) -> - let metasenv, bo = exp_impl metasenv subst context' bo in let bo',ty_of_bo,subst,metasenv,ugraph1 = type_of_aux subst metasenv context' bo ugraph in @@ -1125,7 +1022,9 @@ and type_of_aux' metasenv context t ugraph = CicMetaSubst.ppterm_in_context subst s context (* "\nReason: " ^ Lazy.force e*)) in - enrich msg exn + enrich + (try Some (Cic.CicHash.find localization_tbl hete) with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm hete); None) + msg exn | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy "Coercions on meta")) | CoercGraph.SomeCoercion c -> @@ -1192,9 +1091,9 @@ and type_of_aux' metasenv context t ugraph = (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) ;; -let type_of_aux' metasenv context term ugraph = +let type_of_aux' ?localization_tbl metasenv context term ugraph = try - type_of_aux' metasenv context term ugraph + type_of_aux' ?localization_tbl metasenv context term ugraph with CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg)) @@ -1273,25 +1172,31 @@ let are_all_occurrences_positive metasenv ugraph uri tys leftno = in metasenv,ugraph,substituted_tys -let typecheck metasenv uri obj = +let typecheck metasenv uri obj ~localization_tbl = let ugraph = CicUniv.empty_ugraph in match obj with Cic.Constant (name,Some bo,ty,args,attrs) -> - let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in - let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let bo',boty,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] bo ugraph in + let ty',_,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] ty ugraph in let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in let bo' = CicMetaSubst.apply_subst subst bo' in let ty' = CicMetaSubst.apply_subst subst ty' in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph | Cic.Constant (name,None,ty,args,attrs) -> - let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let ty',_,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] ty ugraph + in Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) -> assert (metasenv' = metasenv); (* Here we do not check the metasenv for correctness *) - let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in - let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let bo',boty,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] bo ugraph in + let ty',sort,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] ty ugraph in begin match sort with Cic.Sort _ @@ -1316,7 +1221,9 @@ let typecheck metasenv uri obj = let metasenv,ugraph,tys = List.fold_right (fun (name,b,ty,cl) (metasenv,ugraph,res) -> - let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let ty',_,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] ty ugraph + in metasenv,ugraph,(name,b,ty',cl)::res ) tys (metasenv,ugraph,[]) in let con_context = @@ -1330,7 +1237,7 @@ let typecheck metasenv uri obj = (fun (name,ty) (metasenv,ugraph,res) -> let ty = CicTypeChecker.debrujin_constructor uri typesno ty in let ty',_,metasenv,ugraph = - type_of_aux' metasenv con_context ty ugraph in + type_of_aux' ~localization_tbl metasenv con_context ty ugraph in let ty' = undebrujin uri typesno tys ty' in metasenv,ugraph,(name,ty')::res ) cl (metasenv,ugraph,[]) @@ -1364,8 +1271,9 @@ let type_of_aux' metasenv context term = let profiler2 = HExtlib.profile "CicRefine" -let type_of_aux' metasenv context term ugraph = - profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph +let type_of_aux' ?localization_tbl metasenv context term ugraph = + profiler2.HExtlib.profile + (type_of_aux' ?localization_tbl metasenv context term) ugraph -let typecheck metasenv uri obj = - profiler2.HExtlib.profile (typecheck metasenv uri) obj +let typecheck ~localization_tbl metasenv uri obj = + profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli index ef089cabf..97417f7f6 100644 --- a/helm/ocaml/cic_unification/cicRefine.mli +++ b/helm/ocaml/cic_unification/cicRefine.mli @@ -31,13 +31,15 @@ exception AssertFailure of string Lazy.t;; (* refines [term] and returns the refined form of [term], *) (* its type, the new metasenv and universe graph. *) val type_of_aux': - Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph -> - Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph + ?localization_tbl:Token.flocation Cic.CicHash.t -> + Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph -> + Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph (* typecheck metasenv uri obj graph *) (* refines [obj] and returns the refined form of [obj], *) (* the new metasenv and universe graph. *) (* the [uri] is required only for inductive definitions *) val typecheck : - Cic.metasenv -> UriManager.uri option -> Cic.obj -> - Cic.obj * Cic.metasenv * CicUniv.universe_graph + localization_tbl:Token.flocation Cic.CicHash.t -> + Cic.metasenv -> UriManager.uri option -> Cic.obj -> + Cic.obj * Cic.metasenv * CicUniv.universe_graph -- 2.39.2