From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 13 Feb 2007 13:48:12 +0000 Subject: Imported Upstream version 8.1+dfsg --- interp/constrintern.ml | 11 +++++++++-- interp/notation.ml | 47 ++++++++++++++++++++++++++++++++++++----------- interp/notation.mli | 6 ++++-- 3 files changed, 49 insertions(+), 15 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d09430dc..4550518d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml 9226 2006-10-09 16:11:01Z herbelin $ *) +(* $Id: constrintern.ml 9611 2007-02-07 15:51:01Z herbelin $ *) open Pp open Util @@ -292,6 +292,12 @@ let intern_qualid loc qid = with Not_found -> error_global_not_found_loc loc qid +(* Rule out section vars since these should have been found by intern_var *) +let intern_non_secvar_qualid loc qid = + match intern_qualid loc qid with + | RRef (loc, VarRef id) -> error_global_not_found_loc loc qid + | r -> r + let intern_inductive r = let loc,qid = qualid_of_reference r in try match Nametab.extended_locate qid with @@ -312,7 +318,8 @@ let intern_reference env lvar = function | Ident (loc, id) -> try intern_var env lvar loc id with Not_found -> - try find_appl_head_data lvar (intern_qualid loc (make_short_qualid id)) + let qid = make_short_qualid id in + try find_appl_head_data lvar (intern_non_secvar_qualid loc qid) with e -> (* Extra allowance for non globalizing functions *) if !interning_grammar then RVar (loc,id), [], [], [] diff --git a/interp/notation.ml b/interp/notation.ml index 5b6692e9..7d70b296 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: notation.ml 9258 2006-10-23 07:15:04Z courtieu $ *) +(* $Id: notation.ml 9481 2007-01-11 19:17:56Z herbelin $ *) (*i*) open Util @@ -446,19 +446,36 @@ let rec compute_arguments_scope t = let arguments_scope = ref Refmap.empty -let load_arguments_scope _ (_,(r,scl)) = +type arguments_scope_discharge_request = + | ArgsScopeAuto + | ArgsScopeManual + | ArgsScopeNoDischarge + +let load_arguments_scope _ (_,(_,r,scl)) = List.iter (option_iter check_scope) scl; arguments_scope := Refmap.add r scl !arguments_scope let cache_arguments_scope o = load_arguments_scope 1 o -let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl) - -let discharge_arguments_scope (r,_) = - match r with - | VarRef _ -> None - | _ -> Some (r,compute_arguments_scope (Global.type_of_global r)) +let subst_arguments_scope (_,subst,(req,r,scl)) = + (ArgsScopeNoDischarge,fst (subst_global subst r),scl) + +let discharge_arguments_scope (_,(req,r,l)) = + if req = ArgsScopeNoDischarge then None + else Some (req,pop_global_reference r,l) + +let rebuild_arguments_scope (req,r,l) = + match req with + | ArgsScopeNoDischarge -> assert false + | ArgsScopeAuto -> + (req,r,compute_arguments_scope (Global.type_of_global r)) + | ArgsScopeManual -> + (* Add to the manually given scopes the one found automatically + for the extra parameters of the section *) + let l' = compute_arguments_scope (Global.type_of_global r) in + let l1,_ = list_chop (List.length l' - List.length l) l' in + (req,r,l1@l) let (inArgumentsScope,outArgumentsScope) = declare_object {(default_object "ARGUMENTS-SCOPE") with @@ -466,10 +483,17 @@ let (inArgumentsScope,outArgumentsScope) = load_function = load_arguments_scope; subst_function = subst_arguments_scope; classify_function = (fun (_,o) -> Substitute o); + discharge_function = discharge_arguments_scope; + rebuild_function = rebuild_arguments_scope; export_function = (fun x -> Some x) } -let declare_arguments_scope r scl = - Lib.add_anonymous_leaf (inArgumentsScope (r,scl)) +let declare_arguments_scope_gen req r scl = + Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl)) + +let declare_arguments_scope local ref scl = + let req = + if local or isVarRef ref then ArgsScopeNoDischarge else ArgsScopeManual in + declare_arguments_scope_gen req ref scl let find_arguments_scope r = try Refmap.find r !arguments_scope @@ -477,7 +501,8 @@ let find_arguments_scope r = let declare_ref_arguments_scope ref = let t = Global.type_of_global ref in - declare_arguments_scope ref (compute_arguments_scope t) + let req = if isVarRef ref then ArgsScopeNoDischarge else ArgsScopeAuto in + declare_arguments_scope_gen req ref (compute_arguments_scope t) (********************************) (* Encoding notations as string *) diff --git a/interp/notation.mli b/interp/notation.mli index 840274c5..7be1f9fe 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: notation.mli 9208 2006-10-05 07:45:01Z herbelin $ i*) +(*i $Id: notation.mli 9481 2007-01-11 19:17:56Z herbelin $ i*) (*i*) open Util @@ -135,7 +135,9 @@ val exists_notation_in_scope : scope_name option -> notation -> interpretation -> bool (* Declares and looks for scopes associated to arguments of a global ref *) -val declare_arguments_scope: global_reference -> scope_name option list -> unit +val declare_arguments_scope : + bool (* true=local *) -> global_reference -> scope_name option list -> unit + val find_arguments_scope : global_reference -> scope_name option list val declare_class_scope : scope_name -> Classops.cl_typ -> unit -- cgit v1.2.3