diff options
-rw-r--r-- | kernel/closure.ml | 1 | ||||
-rw-r--r-- | kernel/closure.mli | 3 | ||||
-rw-r--r-- | plugins/setoid_ring/newring.ml | 19 |
3 files changed, 8 insertions, 15 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 65123108f..960bdb649 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -363,6 +363,7 @@ let set_norm v = v.norm <- Norm let is_val v = match v.norm with Norm -> true | _ -> false let mk_atom c = {norm=Norm;term=FAtom c} +let mk_red f = {norm=Red;term=f} (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) diff --git a/kernel/closure.mli b/kernel/closure.mli index 07176cb7d..8e172290f 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -164,6 +164,9 @@ val inject : constr -> fconstr (** mk_atom: prevents a term from being evaluated *) val mk_atom : constr -> fconstr +(** mk_red: makes a reducible term (used in newring) *) +val mk_red : fterm -> fconstr + val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 7af72b07c..57ef92032 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -34,15 +34,6 @@ open Proofview.Notations (****************************************************************************) (* controlled reduction *) -(** ppedrot: something dubious here, we're obviously using evars the wrong - way. FIXME! *) - -let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|]) -let unmark_arg f c = - match destEvar c with - | (i,[|c|]) -> f (Evar.repr i) c - | _ -> assert false - type protect_flag = Eval|Prot|Rec let tag_arg tag_rec map subs i c = @@ -75,12 +66,10 @@ and mk_clos_app_but f_map subs f args n = let fargs, args' = Array.chop n args in let f' = mkApp(f,fargs) in match f_map (global_of_constr_nofail f') with - Some map -> - mk_clos_deep - (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) - subs - (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) - | None -> mk_clos_app_but f_map subs f args (n+1) + | Some map -> + let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in + mk_red (FApp (f (-1) f', Array.mapi f args')) + | None -> mk_atom (mkApp (f, args)) let interp_map l t = try Some(List.assoc_f eq_gr t l) with Not_found -> None |