From 27ea35bafdf0aefe1dcf49dfed1a18c3f158efa5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Apr 2007 13:56:03 +0000
Subject: Ajout de la possibilité de faire référence dans certains cas à un nom
 par sa notation (p.ex. pour unfold ou pour lazy delta). Ex: Goal 3+4 = 7.
 unfold "+".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9804 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/genarg.ml    |  2 ++
 interp/genarg.mli   |  6 ++++--
 interp/notation.ml  | 42 +++++++++++++++++++++++++++++++++++++-----
 interp/notation.mli |  3 +++
 4 files changed, 46 insertions(+), 7 deletions(-)

(limited to 'interp')

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 303278f18d..2e057e438b 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -44,6 +44,8 @@ type argument_type =
   | ExtraArgType of string
 
 type 'a and_short_name = 'a * identifier located option
+type 'a or_by_notation = AN of 'a | ByNotation of loc * string
+
 type rawconstr_and_expr = rawconstr * constr_expr option
 
 (* Dynamics but tagged by a type expression *)
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 3530bd27ce..db078bfc1e 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -18,6 +18,8 @@ open Term
 
 type 'a and_short_name = 'a * identifier located option
 
+type 'a or_by_notation = AN of 'a | ByNotation of loc * string
+
 (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
 (* in the environment by the effective calls to Intro, Inversion, etc *)
 (* The [constr_expr] field is [None] in TacDef though *)
@@ -156,7 +158,7 @@ val rawwit_constr : (constr_expr,rlevel) abstract_argument_type
 val globwit_constr : (rawconstr_and_expr,glevel) abstract_argument_type
 val wit_constr : (constr,tlevel) abstract_argument_type
 
-val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,rlevel) abstract_argument_type
+val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation) may_eval,rlevel) abstract_argument_type
 val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel) abstract_argument_type
 val wit_constr_may_eval : (constr,tlevel) abstract_argument_type
 
@@ -180,7 +182,7 @@ val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type
 val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type
 val wit_bindings : (constr bindings,tlevel) abstract_argument_type
 
-val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel) abstract_argument_type
+val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type
 val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type
 val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel) abstract_argument_type
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 614c87a0cf..c31ef54ec8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -408,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 *)
 
@@ -602,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 filter_some 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
diff --git a/interp/notation.mli b/interp/notation.mli
index 776db1a502..8bdd8b5863 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -130,6 +130,9 @@ val level_of_notation : notation -> level (* raise [Not_found] if no level *)
 
 (*s** Miscellaneous *)
 
+val interp_notation_as_global_reference : loc -> (global_reference -> bool) -> 
+      notation -> global_reference
+
 (* Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
       interpretation -> bool
-- 
cgit v1.2.3