Simpl_behaviour becomes Reductionops.ReductionBehaviour

syntax mentionning simpl remains

9 files changed, 140 insertions, 134 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2df1f16333..d12204fec0 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -375,7 +375,7 @@ type vernac_expr =
       (explicitation * bool * bool) list list
   | VernacArguments of reference or_by_notation *
       ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list *
-      int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes
+      int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | `ExtraScopes
             | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
   | VernacArgumentsScope of reference or_by_notation *
       scope_name option list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d5ff2538c4..371dae6c81 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -629,10 +629,10 @@ GEXTEND Gram
            error "All arguments lists must have the same length";
          let err_incompat x y =
            error ("Options \""^x^"\" and \""^y^"\" are incompatible") in
-         if nargs > 0 && List.mem `SimplNeverUnfold mods then
+         if nargs > 0 && List.mem `ReductionNeverUnfold mods then
            err_incompat "simpl never" "/";
-         if List.mem `SimplNeverUnfold mods &&
-            List.mem `SimplDontExposeCase mods then
+         if List.mem `ReductionNeverUnfold mods &&
+            List.mem `ReductionDontExposeCase mods then
            err_incompat "simpl never" "simpl nomatch";
          VernacArguments (qid, impl, nargs, mods)
 
@@ -665,8 +665,8 @@ GEXTEND Gram
 	     VernacGeneralizable gen ] ]
   ;
   arguments_modifier:
-    [ [ IDENT "simpl"; IDENT "nomatch" -> [`SimplDontExposeCase]
-      | IDENT "simpl"; IDENT "never" -> [`SimplNeverUnfold]
+    [ [ IDENT "simpl"; IDENT "nomatch" -> [`ReductionDontExposeCase]
+      | IDENT "simpl"; IDENT "never" -> [`ReductionNeverUnfold]
       | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits]
       | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
       | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f033b10e9f..cba915d351 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -26,6 +26,113 @@ exception Elimconst
     their parameters in its stack.
 *)
 
+(** Machinery to custom the behavior of the reduction *)
+module ReductionBehaviour = struct
+  open Globnames
+  open Libobject
+
+  type t = {
+    b_nargs: int;
+    b_recargs: int list;
+    b_dont_expose_case: bool;
+  }
+
+  let table =
+    Summary.ref (Refmap.empty : t Refmap.t) ~name:"reductionbehaviour"
+
+  type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
+  type req =
+    | ReqLocal
+    | ReqGlobal of global_reference * (int list * int * flag list)
+
+  let load _ (_,(_,(r, b))) =
+    table := Refmap.add r b !table
+
+  let cache o = load 1 o
+
+  let classify = function
+    | ReqLocal, _ -> Dispose
+    | ReqGlobal _, _ as o -> Substitute o
+
+  let subst (subst, (_, (r,o as orig))) =
+    ReqLocal,
+    let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
+
+  let discharge = function
+    | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
+       let c' = pop_con c in
+       let vars = Lib.section_segment_of_constant c in
+       let extra = List.length vars in
+       let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
+       let recargs' = List.map ((+) extra) b.b_recargs in
+       let b' = { b with b_nargs = nargs'; b_recargs = recargs' } in
+       Some (ReqGlobal (ConstRef c', req), (ConstRef c', b'))
+    | _ -> None
+
+  let rebuild = function
+    | req, (ConstRef c, _ as x) -> req, x
+    | _ -> assert false
+
+  let inRedBehaviour = declare_object {
+			(default_object "REDUCTIONBEHAVIOUR") with
+			load_function = load;
+			cache_function = cache;
+			classify_function = classify;
+			subst_function = subst;
+			discharge_function = discharge;
+			rebuild_function = rebuild;
+		      }
+
+  let set local r (recargs, nargs, flags as req) =
+    let nargs = if List.mem `ReductionNeverUnfold flags then max_int else nargs in
+    let behaviour = {
+      b_nargs = nargs; b_recargs = recargs;
+      b_dont_expose_case = List.mem `ReductionDontExposeCase flags } in
+    let req = if local then ReqLocal else ReqGlobal (r, req) in
+    Lib.add_anonymous_leaf (inRedBehaviour (req, (r, behaviour)))
+  ;;
+
+  let get r =
+    try
+      let b = Refmap.find r !table in
+      let flags =
+	if Int.equal b.b_nargs max_int then [`ReductionNeverUnfold]
+	else if b.b_dont_expose_case then [`ReductionDontExposeCase] else [] in
+      Some (b.b_recargs, (if Int.equal b.b_nargs max_int then -1 else b.b_nargs), flags)
+    with Not_found -> None
+
+  let print ref =
+    let open Pp in
+    let pr_global = Nametab.pr_global_env Id.Set.empty in
+    match get ref with
+    | None -> mt ()
+    | Some (recargs, nargs, flags) ->
+       let never = List.mem `ReductionNeverUnfold flags in
+       let nomatch = List.mem `ReductionDontExposeCase flags in
+       let pp_nomatch = spc() ++ if nomatch then
+				   str "avoiding to expose match constructs" else str"" in
+       let pp_recargs = spc() ++ str "when the " ++
+			  pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (String.plural (List.length recargs) " argument") ++
+			  str (String.plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
+			  str " to a constructor" in
+       let pp_nargs =
+	 spc() ++ str "when applied to " ++ int nargs ++
+	   str (String.plural nargs " argument") in
+       hov 2 (str "The reduction tactics " ++
+		 match recargs, nargs, never with
+		 | _,_, true -> str "never unfold " ++ pr_global ref
+		 | [], 0, _ -> str "always unfold " ++ pr_global ref
+		 | _::_, n, _ when n < 0 ->
+		    str "unfold " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
+		 | _::_, n, _ when n > List.fold_left max 0 recargs ->
+		    str "unfold " ++ pr_global ref ++ pp_recargs ++
+		      str " and" ++ pp_nargs ++ pp_nomatch
+		 | _::_, _, _ ->
+		    str "unfold " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
+		 | [], n, _ when n > 0 ->
+		    str "unfold " ++ pr_global ref ++ pp_nargs ++ pp_nomatch
+		 | _ -> str "unfold " ++ pr_global ref ++ pp_nomatch )
+end
 
 (** The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
 module Stack = struct
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 11cfe95530..bb49c736b3 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -18,6 +18,18 @@ open Closure
 
 exception Elimconst
 
+(** Machinery to custom the behavior of the reduction *)
+module ReductionBehaviour : sig
+  type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
+
+(** [set is_local ref (recargs, nargs, flags)] *)
+  val set :
+    bool -> Globnames.global_reference -> (int list * int * flag list) -> unit
+  val get :
+    Globnames.global_reference -> (int list * int * flag list) option
+  val print : Globnames.global_reference -> Pp.std_ppcmds
+end
+
 module Stack : sig
   type 'a app_node
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index e252f0a7ef..46037e5eee 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -521,87 +521,16 @@ let special_red_case env sigma whfun (ci, p, c, lf)  =
   in
   redrec c
 
-(* data structure to hold the map kn -> rec_args for simpl *)
-
-type behaviour = {
-  b_nargs: int;
-  b_recargs: int list;
-  b_dont_expose_case: bool;
-}
-
-let behaviour_table =
-  Summary.ref (Refmap.empty : behaviour Refmap.t) ~name:"simplbehaviour"
-
-type simpl_flag = [ `SimplDontExposeCase | `SimplNeverUnfold ]
-type req =
-  | ReqLocal
-  | ReqGlobal of global_reference * (int list * int * simpl_flag list)
-
-let load_simpl_behaviour _ (_,(_,(r, b))) =
-  behaviour_table := Refmap.add r b !behaviour_table
-
-let cache_simpl_behaviour o = load_simpl_behaviour 1 o
-
-let classify_simpl_behaviour = function
-  | ReqLocal, _ -> Dispose
-  | ReqGlobal _, _ as o -> Substitute o
-
-let subst_simpl_behaviour (subst, (_, (r,o as orig))) =
-  ReqLocal,
-  let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
-
-let discharge_simpl_behaviour = function
-  | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
-     let c' = pop_con c in
-     let vars = Lib.section_segment_of_constant c in
-     let extra = List.length vars in
-     let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
-     let recargs' = List.map ((+) extra) b.b_recargs in
-     let b' = { b with b_nargs = nargs'; b_recargs = recargs' } in
-     Some (ReqGlobal (ConstRef c', req), (ConstRef c', b'))
-  | _ -> None
-
-let rebuild_simpl_behaviour = function
-  | req, (ConstRef c, _ as x) -> req, x
-  | _ -> assert false
-
-let inSimplBehaviour = declare_object { (default_object "SIMPLBEHAVIOUR") with
-  load_function = load_simpl_behaviour;
-  cache_function = cache_simpl_behaviour;
-  classify_function = classify_simpl_behaviour;
-  subst_function = subst_simpl_behaviour;
-  discharge_function = discharge_simpl_behaviour;
-  rebuild_function = rebuild_simpl_behaviour;
-}
-
-let set_simpl_behaviour local r (recargs, nargs, flags as req) =
-  let nargs = if List.mem `SimplNeverUnfold flags then max_int else nargs in
-  let behaviour = {
-    b_nargs = nargs; b_recargs = recargs;
-    b_dont_expose_case = List.mem `SimplDontExposeCase flags } in
-  let req = if local then ReqLocal else ReqGlobal (r, req) in
-  Lib.add_anonymous_leaf (inSimplBehaviour (req, (r, behaviour)))
-;;
-
-let get_simpl_behaviour r =
-  try
-    let b = Refmap.find r !behaviour_table in
-    let flags =
-      if Int.equal b.b_nargs max_int then [`SimplNeverUnfold]
-      else if b.b_dont_expose_case then [`SimplDontExposeCase] else [] in
-    Some (b.b_recargs, (if Int.equal b.b_nargs max_int then -1 else b.b_nargs), flags)
-  with Not_found -> None
-
-let get_behaviour = function
-  | EvalVar _ | EvalRel _ | EvalEvar _ -> raise Not_found
-  | EvalConst c -> Refmap.find (ConstRef c) !behaviour_table
-
-let recargs r =
-  try let b = get_behaviour r in Some (b.b_recargs, b.b_nargs)
-  with Not_found -> None
-
-let dont_expose_case r =
-  try (get_behaviour r).b_dont_expose_case with Not_found -> false
+let recargs = function
+  | EvalVar _ | EvalRel _ | EvalEvar _ -> None
+  | EvalConst c -> Option.map (fun (x,y,_) -> (x,y))
+			      (ReductionBehaviour.get (ConstRef c))
+
+let dont_expose_case = function
+  | EvalVar _ | EvalRel _ | EvalEvar _ -> false
+  | EvalConst c ->
+     Option.cata (fun (_,_,z) -> List.mem `ReductionDontExposeCase z)
+		 false (ReductionBehaviour.get (ConstRef c))
 
 let whd_nothing_for_iota env sigma s =
   let rec whrec (x, stack as s) =
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index c14b322aec..be92be51a0 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -45,14 +45,6 @@ val red_product : reduction_function
 (** Red (raise Redelimination if nothing reducible) *)
 val try_red_product : reduction_function
 
-(** Tune the behaviour of simpl for the given constant name *)
-type simpl_flag = [ `SimplDontExposeCase | `SimplNeverUnfold ]
-
-val set_simpl_behaviour :
-  bool -> global_reference -> (int list * int * simpl_flag list) -> unit
-val get_simpl_behaviour :
-  global_reference -> (int list * int * simpl_flag list) option
-
 (** Simpl *)
 val simpl : reduction_function
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2628f732b8..7bb1ceaa0d 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -858,8 +858,8 @@ let rec pr_vernac = function
       prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
       if not (List.is_empty mods) then str" : " else str"" ++
       prlist_with_sep (fun () -> str", " ++ spc()) (function
-        | `SimplDontExposeCase -> str "simpl nomatch"
-        | `SimplNeverUnfold -> str "simpl never"
+        | `ReductionDontExposeCase -> str "simpl nomatch"
+        | `ReductionNeverUnfold -> str "simpl never"
         | `DefaultImplicits -> str "default implicits"
         | `Rename -> str "rename"
         | `ExtraScopes -> str "extra scopes"
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 0d279c73b6..e8b0295cc4 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -153,40 +153,6 @@ let print_argument_scopes prefix = function
       str "]")]
   | _  -> []
 
-(*****************************)
-(** Printing simpl behaviour *)
-
-let print_simpl_behaviour ref =
-  match Tacred.get_simpl_behaviour ref with
-  | None -> []
-  | Some (recargs, nargs, flags) ->
-     let never = List.mem `SimplNeverUnfold flags in
-     let nomatch = List.mem `SimplDontExposeCase flags in
-     let pp_nomatch = spc() ++ if nomatch then
-       str "avoiding to expose match constructs" else str"" in
-     let pp_recargs = spc() ++ str "when the " ++
-       pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (String.plural (List.length recargs) " argument") ++
-       str (String.plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
-       str " to a constructor" in
-     let pp_nargs =
-       spc() ++ str "when applied to " ++ int nargs ++
-       str (String.plural nargs " argument") in
-     [hov 2 (str "The simpl tactic " ++
-     match recargs, nargs, never with
-     | _,_, true -> str "never unfolds " ++ pr_global ref
-     | [], 0, _ -> str "always unfolds " ++ pr_global ref
-     | _::_, n, _ when n < 0 ->
-        str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
-     | _::_, n, _ when n > List.fold_left max 0 recargs ->
-        str "unfolds " ++ pr_global ref ++ pp_recargs ++
-        str " and" ++ pp_nargs ++ pp_nomatch
-     | _::_, _, _ ->
-        str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
-     | [], n, _ when n > 0 ->
-        str "unfolds " ++ pr_global ref ++ pp_nargs ++ pp_nomatch
-     | _ -> str "unfolds " ++ pr_global ref ++ pp_nomatch )]
-;;
-
 (*********************)
 (** Printing Opacity *)
 
@@ -674,7 +640,7 @@ let print_about_any loc k =
       pr_infos_list
        (print_ref false ref :: blankline ::
 	print_name_infos ref @
-	print_simpl_behaviour ref @
+	Reductionops.ReductionBehaviour.print ref ::
 	print_opacity ref @
 	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 51fbbc47bb..cd2338dfe5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -993,13 +993,13 @@ let vernac_declare_arguments locality r l nargs flags =
   if nargs >= 0 && nargs < List.fold_left max 0 rargs then
     error "The \"/\" option must be placed after the last \"!\".";
   let rec narrow = function
-    | #Tacred.simpl_flag as x :: tl -> x :: narrow tl
+    | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl
     | [] -> [] | _ :: tl -> narrow tl in
   let flags = narrow flags in
   if not (List.is_empty rargs) || nargs >= 0 || not (List.is_empty flags) then
     match sr with
     | ConstRef _ as c ->
-       Tacred.set_simpl_behaviour
+       Reductionops.ReductionBehaviour.set
          (make_section_locality locality) c (rargs, nargs, flags)
     | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")