From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- interp/constrextern.ml | 33 ++++++++++++++++++--------------- interp/constrextern.mli | 9 ++++++--- interp/constrintern.ml | 14 +++++++------- interp/implicit_quantifiers.ml | 4 ++-- interp/notation.ml | 2 +- 5 files changed, 34 insertions(+), 28 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 20b9c2a3..ee529fe0 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -137,20 +137,21 @@ let insert_pat_alias loc p = function let extern_evar loc n l = if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None) -let debug_global_reference_printer = - ref (fun _ -> failwith "Cannot print a global reference") +(** We allow customization of the global_reference printer. + For instance, in the debugger the tables of global references + may be inaccurate *) -let in_debugger = ref false +let default_extern_reference loc vars r = + Qualid (loc,shortest_qualid_of_global vars r) -let set_debug_global_reference_printer f = - debug_global_reference_printer := f +let my_extern_reference = ref default_extern_reference -let extern_reference loc vars r = - if !in_debugger then - (* Debugger does not have the tables of global reference at hand *) - !debug_global_reference_printer loc r - else - Qualid (loc,shortest_qualid_of_global vars r) +let set_extern_reference f = my_extern_reference := f +let get_extern_reference () = !my_extern_reference + +let extern_reference loc vars l = !my_extern_reference loc vars l + +let in_debugger = ref false (************************************************************************) @@ -303,10 +304,10 @@ let make_notation_gen loc ntn mknot mkprim destprim l = match decompose_notation_key ntn, l with | [Terminal "-"; Terminal x], [] -> (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x))) - with _ -> mknot (loc,ntn,[])) + with e when Errors.noncritical e -> mknot (loc,ntn,[])) | [Terminal x], [] -> (try mkprim (loc, Numeral (Bigint.of_string x)) - with _ -> mknot (loc,ntn,[])) + with e when Errors.noncritical e -> mknot (loc,ntn,[])) | _ -> mknot (loc,ntn,l) @@ -816,12 +817,14 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function match f with | GRef (_,ref) -> let subscopes = - try list_skipn n (find_arguments_scope ref) with _ -> [] in + try list_skipn n (find_arguments_scope ref) + with e when Errors.noncritical e -> [] in let impls = let impls = select_impargs_size (List.length args) (implicits_of_global ref) in - try list_skipn n impls with _ -> [] in + try list_skipn n impls + with e when Errors.noncritical e -> [] in subscopes,impls | _ -> [], [] in diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 1a1560e5..55fababd 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -50,9 +50,12 @@ val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref -(** Debug printing options *) -val set_debug_global_reference_printer : - (loc -> global_reference -> reference) -> unit +(** Customization of the global_reference printer *) +val set_extern_reference : + (loc -> Idset.t -> global_reference -> reference) -> unit +val get_extern_reference : + unit -> (loc -> Idset.t -> global_reference -> reference) + val in_debugger : bool ref (** This governs printing of implicit arguments. If [with_implicits] is diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 81e4501a..e806686a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -650,7 +650,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = let scopes = find_arguments_scope ref in Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; GRef (loc, ref), impls, scopes, [] - with _ -> + with e when Errors.noncritical e -> (* [id] a goal variable *) GVar (loc,id), [], [], [] @@ -716,7 +716,7 @@ let intern_applied_reference intern env namedctx lvar args = function try let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in find_appl_head_data r, args2 - with e -> + with e when Errors.noncritical e -> (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (GVar (loc,id), [], [], []),args @@ -969,15 +969,15 @@ let sort_fields mode loc l completer = | [] -> anomaly "Number of projections mismatch" | (_, regular)::tm -> let boolean = not regular in - if ConstRef name = global_reference_of_reference refer - then + (match global_reference_of_reference refer with + | ConstRef name' when eq_constant name name' -> if boolean && mode then user_err_loc (loc, "", str"No local fields allowed in a record construction.") else build_patt b tm (i + 1) (i, snd acc) (* we found it *) - else + | _ -> build_patt b tm (if boolean&&mode then i else i + 1) (if boolean && mode then acc - else fst acc, (i, ConstRef name) :: snd acc)) + else fst acc, (i, ConstRef name) :: snd acc))) | None :: b-> (* we don't want anonymous fields *) if mode then user_err_loc (loc, "", str "This record contains anonymous fields.") @@ -1009,7 +1009,7 @@ let sort_fields mode loc l completer = (loc, "", str "This record contains fields of different records.") | (i, a) :: b-> - if glob_refer = a + if eq_gr glob_refer a then (i,List.rev_append acc l) else add_patt b ((i,a)::acc) in diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 9950178c..2c000258 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -88,8 +88,8 @@ let is_freevar ids env x = if Idset.mem x ids then false else try ignore(Environ.lookup_named x env) ; false - with _ -> not (is_global x) - with _ -> true + with e when Errors.noncritical e -> not (is_global x) + with e when Errors.noncritical e -> true (* Auxiliary functions for the inference of implicitly quantified variables. *) diff --git a/interp/notation.ml b/interp/notation.ml index e3fb5d5e..03fa23a3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -838,4 +838,4 @@ let _ = let with_notation_protection f x = let fs = freeze () in try let a = f x in unfreeze fs; a - with e -> unfreeze fs; raise e + with reraise -> unfreeze fs; raise reraise -- cgit v1.2.3