Simpl_behaviour becomes Reductionops.ReductionBehaviour

syntax mentionning simpl remains

1 files changed, 10 insertions, 81 deletions

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) =