summaryrefslogtreecommitdiff
path: root/interp/notation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml86
1 files changed, 56 insertions, 30 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 08c6f31f..98a199ad 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: notation.ml 9694 2007-03-09 18:09:53Z herbelin $ *)
+(* $Id: notation.ml 10893 2008-05-07 09:20:43Z herbelin $ *)
(*i*)
open Util
@@ -73,7 +73,7 @@ let init_scope_map () =
let declare_scope scope =
try let _ = Gmap.find scope !scope_map in ()
with Not_found ->
-(* Options.if_verbose message ("Creating scope "^scope);*)
+(* Flags.if_verbose message ("Creating scope "^scope);*)
scope_map := Gmap.add scope empty_scope !scope_map
let find_scope scope =
@@ -133,7 +133,7 @@ let push_scopes = List.fold_right push_scope
type local_scopes = tmp_scope_name option * scope_name list
let make_current_scopes (tmp_scope,scopes) =
- option_fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
+ Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
(**********************************************************************)
(* Delimiters *)
@@ -142,16 +142,16 @@ let delimiters_map = ref Gmap.empty
let declare_delimiters scope key =
let sc = find_scope scope in
- if sc.delimiters <> None && Options.is_verbose () then begin
- let old = out_some sc.delimiters in
- Options.if_verbose
+ if sc.delimiters <> None && Flags.is_verbose () then begin
+ let old = Option.get sc.delimiters in
+ Flags.if_verbose
warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
end;
let sc = { sc with delimiters = Some key } in
scope_map := Gmap.add scope sc !scope_map;
if Gmap.mem key !delimiters_map then begin
let oldsc = Gmap.find key !delimiters_map in
- Options.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
+ Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
end;
delimiters_map := Gmap.add key scope !delimiters_map
@@ -187,10 +187,10 @@ let cases_pattern_key = function
| PatCstr (_,ref,_,_) -> RefKey (ConstructRef ref)
| _ -> Oth
-let aconstr_key = function
+let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
| AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
| AList (_,_,AApp (ARef ref,args),_,_) -> RefKey ref, Some (List.length args)
- | ARef ref -> RefKey ref, Some 0
+ | ARef ref -> RefKey ref, None
| _ -> Oth, None
let pattern_key = function
@@ -239,12 +239,12 @@ let delay dir int loc x = (dir, (fun () -> int loc x))
let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
declare_prim_token_interpreter sc
(fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
- (patl, (fun r -> option_map mkNumeral (uninterp r)), inpat)
+ (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
declare_prim_token_interpreter sc
(fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
- (patl, (fun r -> option_map mkString (uninterp r)), inpat)
+ (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
let check_required_module loc sc (sp,d) =
try let _ = Nametab.absolute_reference sp in ()
@@ -288,7 +288,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
let declare_notation_level ntn level =
if Gmap.mem ntn !notation_level_map then
- error ("Notation "^ntn^" is already assigned a level");
+ anomaly ("Notation "^ntn^" is already assigned a level");
notation_level_map := Gmap.add ntn level !notation_level_map
let level_of_notation ntn =
@@ -299,8 +299,8 @@ let level_of_notation ntn =
let declare_notation_interpretation ntn scopt pat df =
let scope = match scopt with Some s -> s | None -> default_scope in
let sc = find_scope scope in
- if Gmap.mem ntn sc.notations && Options.is_verbose () then
- msg_warning (str ("Notation "^ntn^" was already used"^
+ if Gmap.mem ntn sc.notations then
+ Flags.if_warn msg_warning (str ("Notation "^ntn^" was already used"^
(if scopt = None then "" else " in scope "^scope)));
let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in
scope_map := Gmap.add scope sc !scope_map;
@@ -393,16 +393,10 @@ let uninterp_prim_token_cases_pattern c =
| Some n -> (na,sc,n)
with Not_found -> raise No_match
-let availability_of_prim_token printer_scope local_scopes t =
- let f scope =
- try
- (* raise Not_found if no primitive interpreter for scope *)
- let interp = Hashtbl.find prim_token_interpreter_tab scope in
- (* raise Not_found if no primitive interpreter for this token in scope *)
- let _ = interp dummy_loc t in true
- with Not_found -> false in
+let availability_of_prim_token printer_scope local_scopes =
+ let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
let scopes = make_current_scopes local_scopes in
- option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
+ Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
(* Miscellaneous *)
@@ -414,6 +408,8 @@ let exists_notation_in_scope scopt ntn r =
r' = r
with Not_found -> false
+let isAVar = function AVar _ -> true | _ -> false
+
(**********************************************************************)
(* Mapping classes to scopes *)
@@ -458,7 +454,7 @@ type arguments_scope_discharge_request =
| ArgsScopeNoDischarge
let load_arguments_scope _ (_,(_,r,scl)) =
- List.iter (option_iter check_scope) scl;
+ List.iter (Option.iter check_scope) scl;
arguments_scope := Refmap.add r scl !arguments_scope
let cache_arguments_scope o =
@@ -471,7 +467,7 @@ 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) =
+let rebuild_arguments_scope (_,(req,r,l)) =
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
@@ -608,21 +604,51 @@ let factorize_entries = function
let is_ident s = (* Poor analysis *)
String.length s <> 0 & is_letter s.[0]
-let browse_notation ntn map =
+let browse_notation strict ntn map =
let find =
if String.contains ntn ' ' then (=) ntn
- else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
+ else fun ntn' ->
+ let toks = decompose_notation_key ntn' in
+ let trms = List.filter (function Terminal _ -> true | _ -> false) toks in
+ if strict then [Terminal ntn] = trms else List.mem (Terminal ntn) trms in
let l =
Gmap.fold
(fun scope_name sc ->
Gmap.fold (fun ntn ((_,r),df) l ->
if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
map [] in
- let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
- factorize_entries l
+ List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l
+
+let global_reference_of_notation test (ntn,(sc,c,_)) =
+ match c with
+ | ARef ref when test ref -> Some (ntn,sc,ref)
+ | AApp (ARef ref, l) when List.for_all isAVar l & test ref ->
+ Some (ntn,sc,ref)
+ | _ -> None
+
+let error_ambiguous_notation loc _ntn =
+ user_err_loc (loc,"",str "Ambiguous notation")
+
+let error_notation_not_reference loc ntn =
+ user_err_loc (loc,"",
+ str "Unable to interpret " ++ quote (str ntn) ++
+ str " as a reference")
+
+let interp_notation_as_global_reference loc test ntn =
+ let ntns = browse_notation true ntn !scope_map in
+ let refs = List.map (global_reference_of_notation test) ntns in
+ match Option.List.flatten refs with
+ | [_,_,ref] -> ref
+ | [] -> error_notation_not_reference loc ntn
+ | refs ->
+ let f (ntn,sc,ref) = find_default ntn !scope_stack = Some sc in
+ match List.filter f refs with
+ | [_,_,ref] -> ref
+ | [] -> error_notation_not_reference loc ntn
+ | _ -> error_ambiguous_notation loc ntn
let locate_notation prraw ntn =
- let ntns = browse_notation ntn !scope_map in
+ let ntns = factorize_entries (browse_notation false ntn !scope_map) in
if ntns = [] then
str "Unknown notation"
else
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 03:48:17 +0000