Pass sigma functionally in newring.ml.

1 files changed, 119 insertions, 127 deletions

diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 9c75175889..b38062a127 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -135,15 +135,11 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 
 (****************************************************************************)
 
-let ic c =
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
+let ic env sigma c =
   let c, uctx = Constrintern.interp_constr env sigma c in
   (Evd.from_ctx uctx, c)
 
-let ic_unsafe c = (*FIXME remove *)
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
+let ic_unsafe env sigma c = (*FIXME remove *)
   fst (Constrintern.interp_constr env sigma c)
 
 let decl_constant name univs c =
@@ -222,10 +218,9 @@ let coq_nil = gen_reference "core.list.nil"
 
 let lapp f args = mkApp(Lazy.force f,args)
 
-let plapp evdref f args =
-  let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in
-  evdref := evd;
-  mkApp(fc,args)
+let plapp sigma f args =
+  let sigma, fc = Evarutil.new_global sigma (Lazy.force f) in
+  sigma, mkApp(fc,args)
 
 let dest_rel0 sigma t =
   match EConstr.kind sigma t with
@@ -411,14 +406,12 @@ let theory_to_obj : ring_info -> obj =
     ~cache:cache_th
     ~subst:(Some subst_th)
 
-let setoid_of_relation env evd a r =
+let setoid_of_relation env sigma a r =
   try
-    let evm = !evd in
-    let evm, refl = Rewrite.get_reflexive_proof env evm a r in
-    let evm, sym = Rewrite.get_symmetric_proof env evm a r in
-    let evm, trans = Rewrite.get_transitive_proof env evm a r in
-      evd := evm;
-      lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
+    let sigma, refl = Rewrite.get_reflexive_proof env sigma a r in
+    let sigma, sym = Rewrite.get_symmetric_proof env sigma a r in
+    let sigma, trans = Rewrite.get_transitive_proof env sigma a r in
+    sigma, lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
   with Not_found ->
     error "cannot find setoid relation"
 
@@ -428,21 +421,19 @@ let op_morph r add mul opp req m1 m2 m3 =
 let op_smorph r add mul req m1 m2 =
   lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
 
-let ring_equality env evd (r,add,mul,opp,req) =
-  match EConstr.kind !evd req with
-    | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
-        let setoid = plapp evd coq_eq_setoid [|r|] in
-        let op_morph =
+let ring_equality env sigma (r,add,mul,opp,req) =
+  match EConstr.kind sigma req with
+    | App (f, [| _ |]) when eq_constr_nounivs sigma f (Lazy.force coq_eq) ->
+        let sigma, setoid = plapp sigma coq_eq_setoid [|r|] in
+        let sigma, 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 sigma = !evd in
+              Some opp -> plapp sigma coq_eq_morph [|r;add;mul;opp|]
+          | None -> plapp sigma coq_eq_smorph [|r;add;mul|] 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 sigma, setoid = setoid_of_relation env sigma r req in
         let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
         let add_m, add_m_lem =
           try Rewrite.default_morphism signature add
@@ -463,19 +454,19 @@ let ring_equality env evd (r,add,mul,opp,req) =
                   op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
                   Flags.if_verbose
                     Feedback.msg_info
-                    (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++
-                        str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
-                        str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++
-                        str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++
+                    (str"Using setoid \""++ pr_econstr_env env sigma req++str"\""++spc()++
+                        str"and morphisms \""++pr_econstr_env env sigma add_m_lem ++
+                        str"\","++spc()++ str"\""++pr_econstr_env env sigma mul_m_lem++
+                        str"\""++spc()++str"and \""++pr_econstr_env env sigma opp_m_lem++
                         str"\"");
                   op_morph)
             | None ->
                 (Flags.if_verbose
                     Feedback.msg_info
-                    (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++
-                        str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
+                    (str"Using setoid \""++pr_econstr_env env sigma req ++str"\"" ++ spc() ++
+                        str"and morphisms \""++pr_econstr_env env sigma add_m_lem ++
                         str"\""++spc()++str"and \""++
-                        pr_econstr_env env !evd mul_m_lem++str"\"");
+                        pr_econstr_env env sigma mul_m_lem++str"\"");
                  op_smorph r add mul req add_m_lem mul_m_lem) in
           (setoid,op_morph)
 
@@ -515,71 +506,69 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
         let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in
               TacArg(CAst.make (TacCall(CAst.make (t,[]))))
 
-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 env sigma c =
+  let t = Retyping.get_type_of env sigma c in
+  plapp sigma coq_mkhypo [|t;c|]
 
-let make_hyp_list env evdref lH =
-  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
-  evdref := evd;
-  let l =
+let make_hyp_list env sigma lH =
+  let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in
+  let sigma, l =
     List.fold_right
-      (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH
-      (plapp evdref coq_nil [|carrier|])
+      (fun c (sigma,l) ->
+        let sigma, c = make_hyp env sigma c in
+        plapp sigma coq_cons [|carrier; c; l|]) lH
+        (plapp sigma coq_nil [|carrier|])
   in
-  let sigma, l' = Typing.solve_evars env !evdref l in
-  evdref := sigma;
+  let sigma, l' = Typing.solve_evars env sigma l in
   let l' = EConstr.Unsafe.to_constr l' in
-    Evarutil.nf_evars_universes !evdref l'
+  sigma, Evarutil.nf_evars_universes sigma l'
 
-let interp_power env evdref pow =
-  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
-  evdref := evd;
+let interp_power env sigma pow =
+  let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in
   match pow with
   | None ->
       let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
-      (TacArg(CAst.make (TacCall(CAst.make (t,[])))), plapp evdref coq_None [|carrier|])
+      let sigma, c = plapp sigma coq_None [|carrier|] in
+      sigma, (TacArg(CAst.make (TacCall(CAst.make (t,[])))), c)
   | 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 evdref (ic_unsafe spec) in
-      (tac, plapp evdref coq_Some [|carrier; spec|])
+      let spec = ic_unsafe env sigma spec in
+      let sigma, spec = make_hyp env sigma spec in
+      let sigma, pow = plapp sigma coq_Some [|carrier; spec|] in
+      sigma, (tac, pow)
 
-let interp_sign env evdref sign =
-  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
-  evdref := evd;
+let interp_sign env sigma sign =
+  let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in
   match sign with
-  | None -> plapp evdref coq_None [|carrier|]
+  | None -> plapp sigma coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env evdref (ic_unsafe spec) in
-      plapp evdref coq_Some [|carrier;spec|]
+      let sigma, spec = make_hyp env sigma (ic_unsafe env sigma spec) in
+      plapp sigma coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
-let interp_div env evdref div =
-  let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
-  evdref := evd;
+let interp_div env sigma div =
+  let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in
   match div with
-  | None -> plapp evdref coq_None [|carrier|]
+  | None -> plapp sigma coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env evdref (ic_unsafe spec) in
-      plapp evdref coq_Some [|carrier;spec|]
+      let sigma, spec = make_hyp env sigma (ic_unsafe env sigma spec) in
+      plapp sigma 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 =
+let add_theory0 env sigma name rth eqth morphth cst_tac (pre,post) power sign div =
   check_required_library (cdir@["Ring_base"]);
-  let env = Global.env() in
   let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
-  let evd = ref sigma in
-  let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
-  let (pow_tac, pspec) = interp_power env evd power in
-  let sspec = interp_sign env evd sign in
-  let dspec = interp_div env evd div in
+  let (sth,ext) = build_setoid_params env sigma r add mul opp req eqth in
+  let sigma, (pow_tac, pspec) = interp_power env sigma power in
+  let sigma, sspec = interp_sign env sigma sign in
+  let sigma, dspec = interp_div env sigma div in
   let rk = reflect_coeff morphth in
   let params,ctx =
-    exec_tactic env !evd 5 (zltac "ring_lemmas")
+    exec_tactic env sigma 5 (zltac "ring_lemmas")
       [sth;ext;rth;pspec;sspec;dspec;rk] in
   let lemma1 = params.(3) in
   let lemma2 = params.(4) in
@@ -619,16 +608,16 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div
           ring_post_tac = posttac }) in
   ()
 
-let ic_coeff_spec = function
-  | Computational t -> Computational (ic_unsafe t)
-  | Morphism t -> Morphism (ic_unsafe t)
+let ic_coeff_spec env sigma = function
+  | Computational t -> Computational (ic_unsafe env sigma t)
+  | Morphism t -> Morphism (ic_unsafe env sigma t)
   | Abstract -> Abstract
 
 
 let set_once s r v =
   if Option.is_empty !r then r := Some v else error (s^" cannot be set twice")
 
-let process_ring_mods l =
+let process_ring_mods env sigma l =
   let kind = ref None in
   let set = ref None in
   let cst_tac = ref None in
@@ -638,11 +627,11 @@ let process_ring_mods l =
   let power = ref None in
   let div = ref None in
   List.iter(function
-      Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k)
+      Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec env sigma k)
     | Const_tac t -> set_once "tactic recognizing constants" cst_tac t
     | Pre_tac t -> set_once "preprocess tactic" pre t
     | Post_tac t -> set_once "postprocess tactic" post t
-    | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
+    | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe env sigma sth,ic_unsafe env sigma ext)
     | Pow_spec(t,spec) -> set_once "power" power (t,spec)
     | Sign_spec t -> set_once "sign" sign t
     | Div_spec t -> set_once "div" div t) l;
@@ -650,9 +639,11 @@ let process_ring_mods l =
   (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
 
 let add_theory id rth l =
-  let (sigma, rth) = ic rth in
-  let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
-  add_theory0 id (sigma, rth) set k cst (pre,post) power sign div
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma, rth = ic env sigma rth in
+  let (k,set,cst,pre,post,power,sign, div) = process_ring_mods env sigma l in
+  add_theory0 env sigma id rth set k cst (pre,post) power sign div
 
 (*****************************************************************************)
 (* The tactics consist then only in a lookup in the ring database and
@@ -664,12 +655,11 @@ let make_args_list sigma rl t =
   | _ -> rl
 
 let make_term_list env evd carrier rl =
-  let l = List.fold_right
-    (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
+  let evd, l = List.fold_right
+    (fun x (evd,l) -> plapp evd coq_cons [|carrier;x;l|]) rl
     (plapp evd coq_nil [|carrier|])
   in
-  let sigma, l = Typing.solve_evars env !evd l in
-  evd := sigma; l
+  Typing.solve_evars env evd l
 
 let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
 let tacarg expr =
@@ -692,15 +682,16 @@ let ltac_ring_structure e =
 
 let ring_lookup (f : Value.t) lH rl t =
   Proofview.Goal.enter begin fun gl ->
-    let sigma = Tacmach.New.project gl in
+    let evd = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    let rl = make_args_list sigma rl t in
-    let evdref = ref sigma in
-    let e = find_ring_structure env sigma rl in
-    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 rl = make_args_list evd rl t in
+    let e = find_ring_structure env evd rl in
+    let evd, l = make_term_list env evd (EConstr.of_constr e.ring_carrier) rl in
+    let rl = Value.of_constr l in
+    let evd, l = make_hyp_list env evd lH in
+    let lH = carg l in
     let ring = ltac_ring_structure e in
-    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (Value.apply f (ring@[lH;rl]))
   end
 
 (***********************************************************************)
@@ -759,22 +750,22 @@ let af_ar = my_reference"AF_AR"
 let f_r = my_reference"F_R"
 let sf_sr = my_reference"SF_SR"
 let dest_field env evd th_spec =
-  let th_typ = Retyping.get_type_of env !evd th_spec in
-  match EConstr.kind !evd th_typ with
+  let th_typ = Retyping.get_type_of env evd th_spec in
+  match EConstr.kind evd th_typ with
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when isRefX !evd (Lazy.force afield_theory) f ->
-        let rth = plapp evd af_ar
+        when isRefX evd (Lazy.force afield_theory) f ->
+        let evd, rth = plapp evd af_ar
           [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when isRefX !evd (Lazy.force field_theory) f ->
-        let rth =
+        when isRefX evd (Lazy.force field_theory) f ->
+        let evd, rth =
           plapp evd f_r
             [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;div;inv;req|])
-        when isRefX !evd (Lazy.force sfield_theory) f ->
-        let rth = plapp evd sf_sr
+        when isRefX evd (Lazy.force sfield_theory) f ->
+        let evd, rth = plapp evd sf_sr
           [|r;zero;one;add;mul;div;inv;req;th_spec|] in
         (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
     | _ -> error "bad field structure"
@@ -860,14 +851,14 @@ let ftheory_to_obj : field_info -> obj =
     ~cache:cache_th
     ~subst:(Some subst_th)
 
-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 field_equality env sigma r inv req =
+  match EConstr.kind sigma req with
+    | App (f, [| _ |]) when eq_constr_nounivs sigma f (Lazy.force coq_eq) ->
         let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in
         let c = EConstr.of_constr c in
         mkApp(c,[|r;r;inv|])
     | _ ->
-        let _setoid = setoid_of_relation (Global.env ()) evd r req in
+        let _setoid = setoid_of_relation env sigma r req in
         let signature = [Some (r,Some req)],Some(r,Some req) in
         let inv_m, inv_m_lem =
           try Rewrite.default_morphism signature inv
@@ -875,24 +866,22 @@ let field_equality evd r inv req =
             error "field inverse should be declared as a morphism" in
           inv_m_lem
 
-let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
+let add_field_theory0 env sigma name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
   let open Constr in
   check_required_library (cdir@["Field_tac"]);
-  let (sigma,fth) = ic fth in
-  let env = Global.env() in
-  let evd = ref sigma in
+  let (sigma,fth) = ic env sigma fth in
   let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =
-    dest_field env evd fth in
-  let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
+    dest_field env sigma fth in
+  let (sth,ext) = build_setoid_params env sigma r add mul opp req eqth in
   let eqth = Some(sth,ext) in
-  let _ = add_theory0 name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in
-  let (pow_tac, pspec) = interp_power env evd power in
-  let sspec = interp_sign env evd sign in
-  let dspec = interp_div env evd odiv in
-  let inv_m = field_equality evd r inv req in
+  let _ = add_theory0 env sigma name rth eqth morphth cst_tac (None,None) power sign odiv in
+  let sigma, (pow_tac, pspec) = interp_power env sigma power in
+  let sigma, sspec = interp_sign env sigma sign in
+  let sigma, dspec = interp_div env sigma odiv in
+  let inv_m = field_equality env sigma r inv req in
   let rk = reflect_coeff morphth in
   let params,ctx =
-    exec_tactic env !evd 9 (field_ltac"field_lemmas")
+    exec_tactic env sigma 9 (field_ltac"field_lemmas")
       [sth;ext;inv_m;fth;pspec;sspec;dspec;rk] in
   let lemma1 = params.(3) in
   let lemma2 = params.(4) in
@@ -940,7 +929,7 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od
           field_pre_tac = pretac;
           field_post_tac = posttac }) in  ()
 
-let process_field_mods l =
+let process_field_mods env sigma l =
   let kind = ref None in
   let set = ref None in
   let cst_tac = ref None in
@@ -951,22 +940,24 @@ let process_field_mods l =
   let power = ref None in
   let div = ref None in
   List.iter(function
-      Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k)
+      Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec env sigma k)
     | Ring_mod(Const_tac t) ->
         set_once "tactic recognizing constants" cst_tac t
     | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t
     | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t
-    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
+    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe env sigma sth,ic_unsafe env sigma ext)
     | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec)
     | Ring_mod(Sign_spec t) -> set_once "sign" sign t
     | Ring_mod(Div_spec t) -> set_once "div" div t
-    | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l;
+    | Inject i -> set_once "infinite property" inj (ic_unsafe env sigma i)) l;
   let k = match !kind with Some k -> k | None -> Abstract in
-  (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
+  (env, sigma, k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
 
 let add_field_theory id t mods =
-  let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods mods in
-  add_field_theory0 id t set k cst_tac inj (pre,post) power sign div
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let (env,sigma,k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods env sigma mods in
+  add_field_theory0 env sigma id t set k cst_tac inj (pre,post) power sign div
 
 let ltac_field_structure e =
   let req = carg e.field_req in
@@ -987,10 +978,11 @@ let field_lookup (f : Value.t) lH rl t =
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     let rl = make_args_list sigma rl t in
-    let evdref = ref sigma in
     let e = find_field_structure env sigma rl in
-    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 sigma, c = make_term_list env sigma (EConstr.of_constr e.field_carrier) rl in
+    let rl = Value.of_constr c in
+    let sigma, l = make_hyp_list env sigma lH in
+    let lH = carg l in
     let field = ltac_field_structure e in
-    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Value.apply f (field@[lH;rl]))
   end