Merge remote-tracking branch 'upstream/trunk' into trunk

6 files changed, 199 insertions, 44 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 79e0e61646..396dde0465 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -45,8 +45,11 @@ let names_of_local_binders bl =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
+(* Note: redundant Numeral representations such as -0 and +0 (or different
+   numbers of leading zeros) are considered different here. *)
+
 let prim_token_eq t1 t2 = match t1, t2 with
-| Numeral i1, Numeral i2 -> Bigint.equal i1 i2
+| Numeral (n1,s1), Numeral (n2,s2) -> String.equal n1 n2 && s1 == s2
 | String s1, String s2 -> String.equal s1 s2
 | _ -> false
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d254520e0e..8a798bfb00 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -66,22 +66,138 @@ let print_universes = Detyping.print_universes
 (* This suppresses printing of primitive tokens (e.g. numeral) and notations *)
 let print_no_symbol = ref false
 
-(* This tells which notations still not to used if print_no_symbol is true *)
-let print_non_active_notations = ref ([] : interp_rule list)
+(**********************************************************************)
+(* Turning notations and scopes on and off for printing *)
+module IRuleSet = Set.Make(struct
+    type t = interp_rule
+    let compare x y = Pervasives.compare x y
+  end)
+
+let inactive_notations_table =
+  Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty)
+let inactive_scopes_table    =
+  Summary.ref ~name:"inactive_scopes_table" CString.Set.empty
+
+let show_scope scopt =
+  match scopt with
+  | None -> str ""
+  | Some sc -> spc () ++ str "in scope" ++ spc () ++ str sc
+
+let _show_inactive_notations () =
+  begin
+    if CString.Set.is_empty !inactive_scopes_table
+    then
+      Feedback.msg_notice (str "No inactive notation scopes.")
+    else
+      let _ = Feedback.msg_notice (str "Inactive notation scopes:") in
+      CString.Set.iter (fun sc -> Feedback.msg_notice (str "  " ++ str sc))
+        !inactive_scopes_table
+  end;
+  if IRuleSet.is_empty !inactive_notations_table
+  then
+    Feedback.msg_notice (str "No individual inactive notations.")
+  else
+    let _ = Feedback.msg_notice (str "Inactive notations:") in
+    IRuleSet.iter
+      (function
+       | NotationRule (scopt, ntn) ->
+         Feedback.msg_notice (str ntn ++ show_scope scopt)
+       | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn)))
+      !inactive_notations_table
+
+let deactivate_notation nr =
+  match nr with
+  | SynDefRule kn ->
+     (* shouldn't we check wether it is well defined? *)
+     inactive_notations_table := IRuleSet.add nr !inactive_notations_table
+  | NotationRule (scopt, ntn) ->
+     match availability_of_notation (scopt, ntn) (scopt, []) with
+     | None -> user_err ~hdr:"Notation"
+                        (str ntn ++ spc () ++ str "does not exist"
+                         ++ (match scopt with
+                             | None -> spc () ++ str "in the empty scope."
+                             | Some _ -> show_scope scopt ++ str "."))
+     | Some _ ->
+        if IRuleSet.mem nr !inactive_notations_table then
+          Feedback.msg_warning
+            (str "Notation" ++ spc () ++ str ntn ++ spc ()
+             ++ str "is already inactive" ++ show_scope scopt ++ str ".")
+        else inactive_notations_table := IRuleSet.add nr !inactive_notations_table
+
+let reactivate_notation nr =
+  try
+    inactive_notations_table :=
+      IRuleSet.remove nr !inactive_notations_table
+  with Not_found ->
+    match nr with
+    | NotationRule (scopt, ntn) ->
+       Feedback.msg_warning (str "Notation" ++ spc () ++ str ntn ++ spc ()
+                             ++ str "is already active" ++ show_scope scopt ++
+  str ".")
+    | SynDefRule kn ->
+       Feedback.msg_warning
+         (str "Notation" ++ spc () ++ str (Names.KerName.to_string kn)
+          ++ spc () ++ str "is already active.")
+
+
+let deactivate_scope sc =
+  ignore (find_scope sc); (* ensures that the scope exists *)
+  if CString.Set.mem sc !inactive_scopes_table
+  then
+    Feedback.msg_warning (str "Notation Scope" ++ spc () ++ str sc ++ spc ()
+                          ++ str "is already inactive.")
+  else
+    inactive_scopes_table := CString.Set.add sc !inactive_scopes_table
+
+let reactivate_scope sc =
+  try
+    inactive_scopes_table := CString.Set.remove sc !inactive_scopes_table
+  with Not_found ->
+    Feedback.msg_warning (str "Notation Scope" ++ spc () ++ str sc ++ spc ()
+                          ++ str "is already active.")
+
+let is_inactive_rule nr =
+  IRuleSet.mem nr !inactive_notations_table ||
+  match nr with
+    | NotationRule (Some sc, ntn) -> CString.Set.mem sc !inactive_scopes_table
+    | NotationRule (None, ntn) -> false
+    | SynDefRule _ -> false
+
+(* args: notation, scope, activate/deactivate *)
+let toggle_scope_printing ~scope ~activate =
+  if activate then
+    reactivate_scope scope
+  else
+    deactivate_scope scope
+
+let toggle_notation_printing ?scope ~notation ~activate =
+  if activate then
+    reactivate_notation (NotationRule (scope, notation))
+  else
+    deactivate_notation (NotationRule (scope, notation))
 
 (* This governs printing of projections using the dot notation symbols *)
 let print_projections = ref false
 
 let print_meta_as_hole = ref false
 
-let with_arguments f = Flags.with_option print_arguments f
-let with_implicits f = Flags.with_option print_implicits f
-let with_coercions f = Flags.with_option print_coercions f
 let with_universes f = Flags.with_option print_universes f
 let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
 let without_symbols f = Flags.with_option print_no_symbol f
-let without_specific_symbols l f =
-  Flags.with_extra_values print_non_active_notations l f
+
+(* XXX: Where to put this in the library? Util maybe? *)
+let protect_ref r nf f x =
+  let old_ref = !r in
+  r := nf !r;
+  try let res = f x in r := old_ref; res
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    r := old_ref;
+    Exninfo.iraise reraise
+
+let without_specific_symbols l =
+  protect_ref inactive_notations_table
+    (fun tbl -> IRuleSet.(union (of_list l) tbl))
 
 (**********************************************************************)
 (* Control printing of records *)
@@ -239,23 +355,31 @@ let expand_curly_brackets loc mknot ntn l =
 let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
 let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
 
+let is_number s =
+  let rec aux i =
+    Int.equal (String.length s) i ||
+    match s.[i] with '0'..'9' -> aux (i+1) | _ -> false
+  in aux 0
+
+let is_zero s =
+  let rec aux i =
+    Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
+  in aux 0
+
 let make_notation_gen loc ntn mknot mkprim destprim l =
   if has_curly_brackets ntn
   then expand_curly_brackets loc mknot ntn l
   else match ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
-    | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p ->
+    | "- _", [Some (Numeral (p,true))] when not (is_zero p) ->
         mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
     | _ ->
 	match decompose_notation_key ntn, l with
-	| [Terminal "-"; Terminal x], [] ->
-	    (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
-	     with Failure _ -> mknot (loc,ntn,[]))
-	| [Terminal x], [] ->
-	    (try mkprim (loc, Numeral (Bigint.of_string x))
-	     with Failure _ -> mknot (loc,ntn,[]))
-	| _ ->
-	    mknot (loc,ntn,l)
+	| [Terminal "-"; Terminal x], [] when is_number x ->
+	   mkprim (loc, Numeral (x,false))
+	| [Terminal x], [] when is_number x ->
+	   mkprim (loc, Numeral (x,true))
+	| _ -> mknot (loc,ntn,l)
 
 let make_notation loc ntn (terms,termlists,binders as subst) =
   if not (List.is_empty termlists) || not (List.is_empty binders) then
@@ -390,7 +514,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
-      if List.mem keyrule !print_non_active_notations then raise No_match;
+      if is_inactive_rule keyrule then raise No_match;
       let loc = t.loc in
       match t.v with
 	| PatCstr (cstr,_,na) ->
@@ -406,8 +530,8 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
-      if List.mem keyrule !print_non_active_notations then raise No_match;
-      apply_notation_to_pattern  (IndRef ind)
+      if is_inactive_rule keyrule then raise No_match;
+      apply_notation_to_pattern (IndRef ind)
 	(match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
     with
 	No_match -> extern_notation_ind_pattern allscopes vars ind args rules
@@ -877,7 +1001,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
   | (keyrule,pat,n as _rule)::rules ->
       let loc = Glob_ops.loc_of_glob_constr t in
       try
-        if List.mem keyrule !print_non_active_notations then raise No_match;
+        if is_inactive_rule keyrule then raise No_match;
 	(* Adjusts to the number of arguments expected by the notation *)
 	let (t,args,argsscopes,argsimpls) = match t.v ,n with
 	  | GApp (f,args), Some n
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index ea627cff11..6c82168e48 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -59,16 +59,6 @@ val set_extern_reference :
 val get_extern_reference :
   unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
 
-(** This governs printing of implicit arguments. If [with_implicits] is
-   on and not [with_arguments] then implicit args are printed prefixed
-   by "!"; if [with_implicits] and [with_arguments] are both on the
-   function and not the arguments is prefixed by "!" *)
-val with_implicits : ('a -> 'b) -> 'a -> 'b
-val with_arguments : ('a -> 'b) -> 'a -> 'b
-
-(** This forces printing of coercions *)
-val with_coercions : ('a -> 'b) -> 'a -> 'b
-
 (** This forces printing universe names of Type\{.\} *)
 val with_universes : ('a -> 'b) -> 'a -> 'b
 
@@ -80,3 +70,13 @@ val without_specific_symbols : interp_rule list -> ('a -> 'b) -> 'a -> 'b
 
 (** This prints metas as anonymous holes *)
 val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
+
+(** Fine-grained activation and deactivation of notation printing.
+ *)
+val toggle_scope_printing :
+  scope:Notation_term.scope_name -> activate:bool -> unit
+
+val toggle_notation_printing :
+  ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit
+
+
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3d484a02da..89827300c4 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -786,7 +786,7 @@ let find_appl_head_data c =
     let scopes = find_arguments_scope ref in
       c, impls, scopes, []
   | GApp ({ v = GRef (ref,_) },l)
-      when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
+      when l != [] ->
       let n = List.length l in
       let impls = implicits_of_global ref in 
       let scopes = find_arguments_scope ref in
@@ -1219,6 +1219,11 @@ let alias_of als = match als.alias_ids with
 
 *)
 
+let is_zero s =
+  let rec aux i =
+    Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
+  in aux 0
+
 let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
 
 let product_of_cases_patterns aliases idspl =
@@ -1331,9 +1336,9 @@ let drop_notations_pattern looked_for genv =
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
         CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
-    | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[])
-	when Bigint.is_strictly_pos p ->
-      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in
+    | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral (p,true)) }],[]),[])
+	when not (is_zero p) ->
+      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in
       rcp_of_glob pat
     | CPatNotation ("( _ )",([a],[]),[]) ->
       in_pat top scopes a
@@ -1639,9 +1644,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	CAst.make ?loc @@
 	GLetIn (snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
-    | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[]))
-	when Bigint.is_strictly_pos p ->
-	intern env (CAst.make ?loc @@ CPrim (Numeral (Bigint.neg p)))
+    | CNotation ("- _",([{ CAst.v = CPrim (Numeral (p,true)) }],[],[]))
+         when not (is_zero p) ->
+       intern env (CAst.make ?loc @@ CPrim (Numeral (p,false)))
     | CNotation ("( _ )",([a],[],[])) -> intern env a
     | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
diff --git a/interp/notation.ml b/interp/notation.ml
index 23332f7c45..300f6b1dd0 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -10,7 +10,6 @@
 open CErrors
 open Util
 open Pp
-open Bigint
 open Names
 open Term
 open Libnames
@@ -319,16 +318,34 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
         (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table)
     patl
 
-let mkNumeral n = Numeral n
+let mkNumeral n =
+  if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
+  else Numeral (Bigint.to_string (Bigint.neg n), false)
+
+let ofNumeral n s =
+  if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+
 let mkString = function
 | None -> None
 | Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
 let delay dir int ?loc x = (dir, (fun () -> int ?loc x))
 
+type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+
+let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) =
+  declare_prim_token_interpreter sc
+    (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s)
+                            | p -> cont ?loc p)
+    (patl, (fun r -> match uninterp r with
+                     | None -> None
+                     | Some (n,s) -> Some (Numeral (n,s))), inpat)
+
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
+  let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in
   declare_prim_token_interpreter sc
-    (fun cont ?loc -> function Numeral n-> delay dir interp ?loc n | p -> cont ?loc p)
+    (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s)
+                            | p -> cont ?loc p)
     (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
@@ -440,8 +457,8 @@ let find_notation ntn sc =
   (n.not_interp, n.not_location)
 
 let notation_of_prim_token = function
-  | Numeral n when is_pos_or_zero n -> to_string n
-  | Numeral n -> "- "^(to_string (neg n))
+  | Numeral (n,true) -> n
+  | Numeral (n,false) -> "- "^n
   | String _ -> raise Not_found
 
 let find_prim_token check_allowed ?loc p sc =
@@ -466,7 +483,8 @@ let interp_prim_token_gen ?loc g p local_scopes =
   with Not_found ->
     user_err ?loc ~hdr:"interp_prim_token"
     ((match p with
-      | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
+      | Numeral _ ->
+         str "No interpretation for numeral " ++ str (notation_of_prim_token p)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token ?loc =
diff --git a/interp/notation.mli b/interp/notation.mli
index d271a88fe7..c739ec12fd 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -74,6 +74,11 @@ type 'a prim_token_interpreter =
 type 'a prim_token_uninterpreter =
     glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
 
+type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+
+val declare_rawnumeral_interpreter : scope_name -> required_module ->
+  rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit
+
 val declare_numeral_interpreter : scope_name -> required_module ->
   bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit