Simpl_behaviour becomes Reductionops.ReductionBehaviour

syntax mentionning simpl remains

4 files changed, 129 insertions, 89 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f033b10e9..cba915d35 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 11cfe9553..bb49c736b 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 e252f0a7e..46037e5ee 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 c14b322ae..be92be51a 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