diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/impargs.ml | 6 | ||||
| -rw-r--r-- | interp/notation.ml | 47 | ||||
| -rw-r--r-- | interp/notation.mli | 3 | ||||
| -rw-r--r-- | interp/reserve.ml | 2 |
4 files changed, 40 insertions, 18 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml index e542b818f6..3603367cf1 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -508,11 +508,11 @@ type implicit_discharge_request = | ImplInteractive of GlobRef.t * implicits_flags * implicit_interactive_request -let implicits_table = Summary.ref Refmap.empty ~name:"implicits" +let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits" let implicits_of_global ref = try - let l = Refmap.find ref !implicits_table in + let l = GlobRef.Map.find ref !implicits_table in try let rename_l = Arguments_renaming.arguments_names ref in let rec rename implicits names = match implicits, names with @@ -527,7 +527,7 @@ let implicits_of_global ref = with Not_found -> [DefaultImpArgs,[]] let cache_implicits_decl (ref,imps) = - implicits_table := Refmap.add ref imps !implicits_table + implicits_table := GlobRef.Map.add ref imps !implicits_table let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l diff --git a/interp/notation.ml b/interp/notation.ml index 55ead946cb..a6a14efc87 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -98,21 +98,40 @@ let init_scope_map () = (**********************************************************************) (* Operations on scopes *) +let warn_undeclared_scope = + CWarnings.create ~name:"undeclared-scope" ~category:"deprecated" + (fun (scope) -> + strbrk "Declaring a scope implicitly is deprecated; use in advance an explicit " + ++ str "\"Declare Scope " ++ str scope ++ str ".\".") + let declare_scope scope = try let _ = String.Map.find scope !scope_map in () with Not_found -> -(* Flags.if_warn message ("Creating scope "^scope);*) scope_map := String.Map.add scope empty_scope !scope_map let error_unknown_scope sc = user_err ~hdr:"Notation" (str "Scope " ++ str sc ++ str " is not declared.") -let find_scope scope = +let find_scope ?(tolerant=false) scope = try String.Map.find scope !scope_map - with Not_found -> error_unknown_scope scope + with Not_found -> + if tolerant then + (* tolerant mode to be turn off after deprecation phase *) + begin + warn_undeclared_scope scope; + scope_map := String.Map.add scope empty_scope !scope_map; + empty_scope + end + else + error_unknown_scope scope + +let check_scope ?(tolerant=false) scope = + let _ = find_scope ~tolerant scope in () + +let ensure_scope scope = check_scope ~tolerant:true scope -let check_scope sc = let _ = find_scope sc in () +let find_scope scope = find_scope scope (* [sc] might be here a [scope_name] or a [delimiter] (now allowed after Open Scope) *) @@ -245,7 +264,7 @@ type key = | Oth let key_compare k1 k2 = match k1, k2 with -| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2 +| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 | RefKey _, Oth -> -1 | Oth, RefKey _ -> 1 | Oth, Oth -> 0 @@ -376,7 +395,7 @@ let prim_token_interp_infos = (* Table from global_reference to backtrack-able informations about prim_token uninterpretation (in particular uninterpreter unique id). *) let prim_token_uninterp_infos = - ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t) + ref (GlobRef.Map.empty : (scope_name * prim_token_uid * bool) GlobRef.Map.t) let hashtbl_check_and_set allow_overwrite uid f h eq = match Hashtbl.find h uid with @@ -418,11 +437,11 @@ type prim_token_infos = { let cache_prim_token_interpretation (_,infos) = let sc = infos.pt_scope in let uid = infos.pt_uid in - declare_scope sc; + check_scope ~tolerant:true sc; prim_token_interp_infos := String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos; List.iter (fun r -> prim_token_uninterp_infos := - Refmap.add r (sc,uid,infos.pt_in_match) + GlobRef.Map.add r (sc,uid,infos.pt_in_match) !prim_token_uninterp_infos) infos.pt_refs @@ -764,7 +783,7 @@ let uninterp_prim_token c = | None -> raise Notation_ops.No_match | Some r -> try - let (sc,uid,_) = Refmap.find r !prim_token_uninterp_infos in + let (sc,uid,_) = GlobRef.Map.find r !prim_token_uninterp_infos in let uninterp = Hashtbl.find prim_token_uninterpreters uid in match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with | None -> raise Notation_ops.No_match @@ -905,7 +924,7 @@ let rec update_scopes cls scl = match cls, scl with | _, [] -> List.map find_scope_class_opt cls | cl :: cls, sco :: scl -> update_scope cl sco :: update_scopes cls scl -let arguments_scope = ref Refmap.empty +let arguments_scope = ref GlobRef.Map.empty type arguments_scope_discharge_request = | ArgsScopeAuto @@ -915,7 +934,7 @@ type arguments_scope_discharge_request = let load_arguments_scope _ (_,(_,r,n,scl,cls)) = List.iter (Option.iter check_scope) scl; let initial_stamp = ScopeClassMap.empty in - arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope + arguments_scope := GlobRef.Map.add r (scl,cls,initial_stamp) !arguments_scope let cache_arguments_scope o = load_arguments_scope 1 o @@ -996,13 +1015,13 @@ let declare_arguments_scope local r scl = let find_arguments_scope r = try - let (scl,cls,stamp) = Refmap.find r !arguments_scope in + let (scl,cls,stamp) = GlobRef.Map.find r !arguments_scope in let cur_stamp = !scope_class_map in if stamp == cur_stamp then scl else (* Recent changes in the Bind Scope base, we re-compute the scopes *) let scl' = update_scopes cls scl in - arguments_scope := Refmap.add r (scl',cls,cur_stamp) !arguments_scope; + arguments_scope := GlobRef.Map.add r (scl',cls,cur_stamp) !arguments_scope; scl' with Not_found -> [] @@ -1331,7 +1350,7 @@ let init () = notations_key_table := KeyMap.empty; scope_class_map := initial_scope_class_map; prim_token_interp_infos := String.Map.empty; - prim_token_uninterp_infos := Refmap.empty + prim_token_uninterp_infos := GlobRef.Map.empty let _ = Summary.declare_summary "symbols" diff --git a/interp/notation.mli b/interp/notation.mli index e5478eff48..6e59c0fd70 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -41,6 +41,9 @@ type scopes (** = [scope_name list] *) val declare_scope : scope_name -> unit +(* To be removed after deprecation phase *) +val ensure_scope : scope_name -> unit + val current_scopes : unit -> scopes (** Check where a scope is opened or not in a scope list, or in diff --git a/interp/reserve.ml b/interp/reserve.ml index 071248f01f..edbdf1dbba 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -28,7 +28,7 @@ type key = (** TODO: share code from Notation *) let key_compare k1 k2 = match k1, k2 with -| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2 +| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 | RefKey _, Oth -> -1 | Oth, RefKey _ -> 1 | Oth, Oth -> 0 |