1 files changed, 93 insertions, 103 deletions

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 99bb8440..a736eec5 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -20,6 +20,7 @@ open Environ
 open Libnames
 open Globnames
 open Glob_term
+open Locus
 open Tacexpr
 open Coqlib
 open Mod_subst
@@ -29,7 +30,6 @@ open Printer
 open Declare
 open Decl_kinds
 open Entries
-open Misctypes
 open Newring_ast
 open Proofview.Notations
 
@@ -40,11 +40,7 @@ let error msg = CErrors.user_err Pp.(str msg)
 
 type protect_flag = Eval|Prot|Rec
 
-let tag_arg tag_rec map subs i c =
-  match map i with
-      Eval -> mk_clos subs c
-    | Prot -> mk_atom c
-    | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c
+type protection = Evd.evar_map -> EConstr.t -> GlobRef.t -> (Int.t -> protect_flag) option
 
 let global_head_of_constr sigma c = 
   let f, args = decompose_app sigma c in
@@ -55,32 +51,24 @@ let global_of_constr_nofail c =
   try global_of_constr c
   with Not_found -> VarRef (Id.of_string "dummy")
 
-let rec mk_clos_but f_map subs t =
-  let open Term in
-  match f_map (global_of_constr_nofail t) with
-    | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t
-    | None ->
-        (match Constr.kind t with
-            App(f,args) -> mk_clos_app_but f_map subs f args 0
-          | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t
-          | _ -> mk_atom t)
+let rec mk_clos_but f_map n t =
+  let (f, args) = Constr.decompose_appvect t in
+  match f_map (global_of_constr_nofail f) with
+  | Some tag ->
+      let map i t = tag_arg f_map n (tag i) t in
+      if Array.is_empty args then map (-1) f
+      else mk_red (FApp (map (-1) f, Array.mapi map args))
+  | None -> mk_atom t
 
-and mk_clos_app_but f_map subs f args n =
-  let open Constr in
-  if n >= Array.length args then mk_atom(mkApp(f, args))
-  else
-    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 ->
-       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))
+and tag_arg f_map n tag c = match tag with
+| Eval -> mk_clos (Esubst.subs_id n) c
+| Prot -> mk_atom c
+| Rec -> mk_clos_but f_map n c
 
 let interp_map l t =
-  try Some(List.assoc_f eq_gr t l) with Not_found -> None
+  try Some(List.assoc_f GlobRef.equal t l) with Not_found -> None
 
-let protect_maps = ref String.Map.empty
+let protect_maps : protection String.Map.t ref = ref String.Map.empty
 let add_map s m = protect_maps := String.Map.add s m !protect_maps
 let lookup_map map =
   try String.Map.find map !protect_maps
@@ -90,8 +78,14 @@ let lookup_map map =
 let protect_red map env sigma c0 =
   let evars ev = Evarutil.safe_evar_value sigma ev in
   let c = EConstr.Unsafe.to_constr c0 in
-  EConstr.of_constr (kl (create_clos_infos ~evars all env) (create_tab ())
-    (mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));;
+  let tab = create_tab () in
+  let infos = create_clos_infos ~evars all env in
+  let map = lookup_map map sigma c0 in
+  let rec eval n c = match Constr.kind c with
+  | Prod (na, t, u) -> Constr.mkProd (na, eval n t, eval (n + 1) u)
+  | _ -> kl infos tab (mk_clos_but map n c)
+  in
+  EConstr.of_constr (eval 0 c)
 
 let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None
@@ -102,34 +96,36 @@ let protect_tac_in map id =
 
 (****************************************************************************)
 
-let closed_term t l =
-  let open Quote_plugin in
+let rec closed_under sigma cset t =
+  try
+    let (gr, _) = Termops.global_of_constr sigma t in
+    Refset_env.mem gr cset
+  with Not_found ->
+    match EConstr.kind sigma t with
+    | Cast(c,_,_) -> closed_under sigma cset c
+    | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l
+    | _ -> false
+
+let closed_term args _ = match args with
+| [t; l] ->
+  let t = Option.get (Value.to_constr t) in
+  let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in
   Proofview.tclEVARMAP >>= fun sigma ->
-  let l = List.map Universes.constr_of_global l in
-  let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
-  if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
-
-(* TACTIC EXTEND echo
-| [ "echo" constr(t) ] ->
-  [ Pp.msg (Termops.print_constr t);  Tacinterp.eval_tactic (TacId []) ]
-END;;*)
+  let cs = List.fold_right Refset_env.add l Refset_env.empty in
+  if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
+| _ -> assert false
 
-(*
-let closed_term_ast l =
-  TacFun([Some(Id.of_string"t")],
-  TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
-  [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t"));
-   Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l])))
-*)
-let closed_term_ast l =
+let closed_term_ast =
   let tacname = {
     mltac_plugin = "newring_plugin";
     mltac_tactic = "closed_term";
   } in
+  let () = Tacenv.register_ml_tactic tacname [|closed_term|] in
   let tacname = {
     mltac_name = tacname;
     mltac_index = 0;
   } in
+  fun l ->
   let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
   TacFun([Name(Id.of_string"t")],
   TacML(Loc.tag (tacname,
@@ -154,8 +150,7 @@ let ic_unsafe c = (*FIXME remove *)
 
 let decl_constant na univs c =
   let open Constr in
-  let env = Global.env () in
-  let vars = Univops.universes_of_constr env c in
+  let vars = Univops.universes_of_constr c in
   let univs = Univops.restrict_universe_context univs vars in
   let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 
@@ -166,28 +161,13 @@ let decl_constant na univs c =
 let ltac_call tac (args:glob_tactic_arg list) =
   TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args)))
 
-(* Calling a locally bound tactic *)
-let ltac_lcall tac args =
-  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args)))
-
-let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
-  let fold arg (i, vars, lfun) =
-    let id = Id.of_string ("x" ^ string_of_int i) in
-    let x = Reference (ArgVar CAst.(make id)) in
-    (succ i, x :: vars, Id.Map.add id arg lfun)
-  in
-  let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
-  let lfun = Id.Map.add (Id.of_string "F") f lfun in
-  let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
-  Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)
-
 let dummy_goal env sigma =
   let (gl,_,sigma) = 
     Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in
   {Evd.it = gl; Evd.sigma = sigma}
 
-let constr_of v = match Value.to_constr v with
-  | Some c -> EConstr.Unsafe.to_constr c
+let constr_of evd v = match Value.to_constr v with
+  | Some c -> EConstr.to_constr evd c
   | None -> failwith "Ring.exec_tactic: anomaly"
 
 let tactic_res = ref [||]
@@ -221,8 +201,8 @@ let exec_tactic env evd n f args =
   (** Evaluate the whole result *)
   let gl = dummy_goal env evd in
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
-  let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
-  let nf c = nf (constr_of c) in
+  let evd = Evd.minimize_universes (Refiner.project gls) in
+  let nf c = constr_of evd c in
   Array.map nf !tactic_res, Evd.universe_context_set evd
 
 let stdlib_modules =
@@ -233,7 +213,7 @@ let stdlib_modules =
   ]
 
 let coq_constant c =
-  lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c))
+  lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c))
 let coq_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
 
@@ -247,9 +227,10 @@ let coq_nil = coq_reference "nil"
 
 let lapp f args = mkApp(Lazy.force f,args)
 
-let plapp evd f args = 
-  let fc = Evarutil.e_new_global evd (Lazy.force f) in
-    mkApp(fc,args)
+let plapp evdref f args =
+  let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in
+  evdref := evd;
+  mkApp(fc,args)
 
 let dest_rel0 sigma t =
   match EConstr.kind sigma t with
@@ -278,7 +259,7 @@ let plugin_modules =
     ]
 
 let my_constant c =
-  lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
+  lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
 let my_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
@@ -504,10 +485,12 @@ let ring_equality env evd (r,add,mul,opp,req) =
 	let op_morph =
 	  match opp with
               Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
-            | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
-	let setoid = Typing.e_solve_evars env evd setoid in
-	let op_morph = Typing.e_solve_evars env evd op_morph in
-	  (setoid,op_morph)
+          | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
+        let sigma = !evd in
+        let sigma, setoid = Typing.solve_evars env sigma setoid in
+        let sigma, op_morph = Typing.solve_evars env sigma op_morph in
+        evd := sigma;
+        (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) evd r req in
 	let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
@@ -586,48 +569,53 @@ let make_hyp env evd c =
   let t = Retyping.get_type_of env !evd c in
    plapp evd coq_mkhypo [|t;c|]
 
-let make_hyp_list env evd lH =
-  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let make_hyp_list env evdref lH =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
   let l = 
     List.fold_right
-      (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
-      (plapp evd coq_nil [|carrier|])
+      (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH
+      (plapp evdref coq_nil [|carrier|])
   in 
-  let l' = Typing.e_solve_evars env evd l in
+  let sigma, l' = Typing.solve_evars env !evdref l in
+  evdref := sigma;
   let l' = EConstr.Unsafe.to_constr l' in
-    Evarutil.nf_evars_universes !evd l'
+    Evarutil.nf_evars_universes !evdref l'
 
-let interp_power env evd pow =
-  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_power env evdref pow =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
   match pow with
   | None ->
       let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
-      (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evd coq_None [|carrier|])
+      (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evdref coq_None [|carrier|])
   | Some (tac, spec) ->
       let tac =
         match tac with
         | CstTac t -> Tacintern.glob_tactic t
         | Closed lc ->
             closed_term_ast (List.map Smartlocate.global_with_alias lc) in
-      let spec = make_hyp env evd (ic_unsafe spec) in
-      (tac, plapp evd coq_Some [|carrier; spec|])
+      let spec = make_hyp env evdref (ic_unsafe spec) in
+      (tac, plapp evdref coq_Some [|carrier; spec|])
 
-let interp_sign env evd sign =
-  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_sign env evdref sign =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
   match sign with
-  | None -> plapp evd coq_None [|carrier|]
+  | None -> plapp evdref coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env evd (ic_unsafe spec) in
-      plapp evd coq_Some [|carrier;spec|]
+      let spec = make_hyp env evdref (ic_unsafe spec) in
+      plapp evdref coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
-let interp_div env evd div =
-  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_div env evdref div =
+  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+  evdref := evd;
   match div with
-  | None -> plapp evd coq_None [|carrier|]
+  | None -> plapp evdref coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env evd (ic_unsafe spec) in
-      plapp evd coq_Some [|carrier;spec|]
+      let spec = make_hyp env evdref (ic_unsafe spec) in
+      plapp evdref coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
 let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div =
@@ -728,7 +716,9 @@ let make_term_list env evd carrier rl =
   let l = List.fold_right
     (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
     (plapp evd coq_nil [|carrier|])
-  in Typing.e_solve_evars env evd l
+  in
+  let sigma, l = Typing.solve_evars env !evd l in
+  evd := sigma; l
 
 let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
 let tacarg expr =
@@ -760,7 +750,7 @@ let ring_lookup (f : Value.t) lH rl t =
       let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
       let lH = carg (make_hyp_list env evdref lH) in
       let ring = ltac_ring_structure e in
-      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
@@ -917,7 +907,7 @@ let ftheory_to_obj : field_info -> obj =
 let field_equality evd r inv req =
   match EConstr.kind !evd req with
     | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
-        let c = Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr in
+        let c = UnivGen.constr_of_global (Coqlib.build_coq_eq_data()).congr in
         let c = EConstr.of_constr c in
         mkApp(c,[|r;r;inv|])
     | _ ->
@@ -1046,6 +1036,6 @@ let field_lookup (f : Value.t) lH rl t =
       let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
       let lH = carg (make_hyp_list env evdref lH) in
       let field = ltac_field_structure e in
-      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end