Constraining refine to monotonic functions.

9 files changed, 89 insertions, 49 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index d8c5b8a95..1741df533 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -29,6 +29,7 @@ open Termops
 open Namegen
 open Goptions
 open Misctypes
+open Sigma.Notations
 
 (* Strictness option *)
 
@@ -1305,7 +1306,11 @@ let understand_my_constr env sigma c concl =
   Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc)
 
 let my_refine c gls =
-  let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
+  let oc = { run = begin fun sigma ->
+    let sigma = Sigma.to_evar_map sigma in
+    let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
+    Sigma.Unsafe.of_pair (c, sigma)
+  end } in
   Proofview.V82.of_tactic (Tactics.New.refine oc) gls
 
 (* end focus/claim *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 11b7d07d0..f549913f2 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -16,6 +16,7 @@
 open Pp
 open Util
 open Proofview_monad
+open Sigma.Notations
 
 (** Main state of tactics *)
 type proofview = Proofview_monad.proofview
@@ -1031,7 +1032,7 @@ struct
     let prev_future_goals = Evd.future_goals sigma in
     let prev_principal_goal = Evd.principal_future_goal sigma in
     (** Create the refinement term *)
-    let (sigma, c) = f (Evd.reset_future_goals sigma) in
+    let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
     let evs = Evd.future_goals sigma in
     let evkmain = Evd.principal_future_goal sigma in
     (** Check that the introduced evars are well-typed *)
@@ -1074,7 +1075,11 @@ struct
   let refine_casted ?unsafe f = Goal.enter begin fun gl ->
     let concl = Goal.concl gl in
     let env = Goal.env gl in
-    let f h = let (h, c) = f h in with_type env h c concl in
+    let f = { run = fun h ->
+      let Sigma (c, h, p) = f.run h in
+      let sigma, c = with_type env (Sigma.to_evar_map h) c concl in
+      Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
+    } in
     refine ?unsafe f
   end
 end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 98e1477ff..04ca01ec4 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -487,7 +487,7 @@ module Refine : sig
 
   (** {7 Refinement primitives} *)
 
-  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic
+  val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
   (** In [refine ?unsafe t], [t] is a term with holes under some
       [evar_map] context. The term [t] is used as a partial solution
       for the current goal (refine is a goal-dependent tactic), the
@@ -503,7 +503,7 @@ module Refine : sig
   (** [with_type env sigma c t] ensures that [c] is of type [t]
       inserting a coercion if needed. *)
 
-  val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*Constr.t) -> unit tactic
+  val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
   (** Like {!refine} except the refined term is coerced to the conclusion of the
       current goal. *)
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1a3f46039..d7d82111c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -21,6 +21,7 @@ open Util
 open Evd
 open Equality
 open Misctypes
+open Sigma.Notations
 
 DECLARE PLUGIN "extratactics"
 
@@ -355,7 +356,11 @@ let refine_tac {Glob_term.closure=closure;term=term} =
       Pretyping.ltac_uconstrs = closure.Glob_term.untyped;
       Pretyping.ltac_idents = closure.Glob_term.idents;
     } in
-    let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in
+    let update = { run = begin fun sigma ->
+      let sigma = Sigma.to_evar_map sigma in
+      let (sigma, c) = Pretyping.understand_ltac flags env sigma lvar tycon term in
+      Sigma.Unsafe.of_pair (c, sigma)
+    end } in
     Tactics.New.refine ~unsafe:false update
   end
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ef115aea0..0acaeb44c 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -27,6 +27,7 @@ open Elim
 open Equality
 open Misctypes
 open Tacexpr
+open Sigma.Notations
 open Proofview.Notations
 
 let clear hyps = Proofview.V82.tactic (clear hyps)
@@ -457,7 +458,7 @@ let raw_inversion inv_kind id status names =
     in
     let refined id =
       let prf = mkApp (mkVar id, args) in
-      Proofview.Refine.refine (fun h -> h, prf)
+      Proofview.Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
     in
     let neqns = List.length realargs in
     let as_mode = names != None in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 081170869..1b6ba56e6 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -34,6 +34,7 @@ open Elimschemes
 open Environ
 open Termops
 open Libnames
+open Sigma.Notations
 
 (** Typeclass-based generalized rewriting. *)
 
@@ -1508,13 +1509,14 @@ let assert_replacing id newt tac =
     | (id, b, _) :: rem -> insert_dependent env (id, b, newt) [] after @ rem
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
-    Proofview.Refine.refine ~unsafe:false begin fun sigma ->
+    Proofview.Refine.refine ~unsafe:false { run = begin fun sigma ->
+      let sigma = Sigma.to_evar_map sigma in
       let sigma, ev = Evarutil.new_evar env' sigma concl in
       let sigma, ev' = Evarutil.new_evar env sigma newt in
       let map (n, _, _) = if Id.equal n id then ev' else mkVar n in
       let (e, _) = destEvar ev in
-      sigma, mkEvar (e, Array.map_of_list map nc)
-    end
+      Sigma.Unsafe.of_pair (mkEvar (e, Array.map_of_list map nc), sigma)
+    end }
   end in
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
 
@@ -1533,7 +1535,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
         let gls = List.rev (Evd.fold_undefined fold undef []) in
 	match clause, prf with
 	| Some id, Some p ->
-            let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in
+            let tac = Proofview.Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
             Proofview.Unsafe.tclEVARS undef <*>
 	    assert_replacing id newt tac
 	| Some id, None ->
@@ -1543,10 +1545,11 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
             Proofview.Unsafe.tclEVARS undef <*>
             Proofview.Goal.enter begin fun gl ->
             let env = Proofview.Goal.env gl in
-            let make sigma =
+            let make = { run = begin fun sigma ->
+              let sigma = Sigma.to_evar_map sigma in
               let (sigma, ev) = Evarutil.new_evar env sigma newt in
-              sigma, mkApp (p, [| ev |])
-            in
+              Sigma.Unsafe.of_pair (mkApp (p, [| ev |]), sigma)
+            end } in
             Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
             end
 	| None, None ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 27166bf48..90e4f8521 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,6 +43,7 @@ open Locus
 open Locusops
 open Misctypes
 open Proofview.Notations
+open Sigma.Notations
 
 let nb_prod x =
   let rec count n c =
@@ -171,15 +172,16 @@ let _ =
 (** This tactic creates a partial proof realizing the introduction rule, but
     does not check anything. *)
 let unsafe_intro env store (id, c, t) b =
-  Proofview.Refine.refine ~unsafe:true begin fun sigma ->
+  Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+    let sigma = Sigma.to_evar_map sigma in
     let ctx = named_context_val env in
     let nctx = push_named_context_val (id, c, t) ctx in
     let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar id) b in
     let sigma, ev = new_evar_instance nctx sigma nb ~store ninst in
-    sigma, mkNamedLambda_or_LetIn (id, c, t) ev
-  end
+    Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn (id, c, t) ev, sigma)
+  end }
 
 let introduction ?(check=true) id =
   Proofview.Goal.enter begin fun gl ->
@@ -206,7 +208,8 @@ let convert_concl ?(check=true) ty k =
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
     let conclty = Proofview.Goal.raw_concl gl in
-    Proofview.Refine.refine ~unsafe:true begin fun sigma ->
+    Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+      let sigma = Sigma.to_evar_map sigma in
       let sigma =
         if check then begin
           ignore (Typing.unsafe_type_of env sigma ty);
@@ -215,8 +218,9 @@ let convert_concl ?(check=true) ty k =
           sigma
         end else sigma in
       let (sigma,x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
-      (sigma, if k == DEFAULTcast then x else mkCast(x,k,conclty))
-    end
+      let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
+      Sigma.Unsafe.of_pair (ans, sigma)
+    end }
   end
 
 let convert_hyp ?(check=true) d =
@@ -227,7 +231,11 @@ let convert_hyp ?(check=true) d =
     let store = Proofview.Goal.extra gl in
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
-    Proofview.Refine.refine ~unsafe:true (fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty)
+    Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+      let sigma = Sigma.to_evar_map sigma in
+      let (sigma, c) = Evarutil.new_evar env sigma ~principal:true ~store ty in
+      Sigma.Unsafe.of_pair (c, sigma)
+    end }
   end
 
 let convert_concl_no_check = convert_concl ~check:false
@@ -345,9 +353,11 @@ let rename_hyp repl =
       let nconcl = subst concl in
       let nctx = Environ.val_of_named_context nhyps in
       let instance = List.map (fun (id, _, _) -> mkVar id) hyps in
-      Proofview.Refine.refine ~unsafe:true begin fun sigma ->
-        Evarutil.new_evar_instance nctx sigma nconcl ~store instance
-      end
+      Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+        let sigma = Sigma.to_evar_map sigma in
+        let (sigma, c) = Evarutil.new_evar_instance nctx sigma nconcl ~store instance in
+        Sigma.Unsafe.of_pair (c, sigma)
+      end }
     end
 
 (**************************************************************)
@@ -1047,12 +1057,13 @@ let cut c =
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
       (** Backward compat: normalize [c]. *)
       let c = local_strong whd_betaiota sigma c in
-      Proofview.Refine.refine ~unsafe:true begin fun h ->
+      Proofview.Refine.refine ~unsafe:true { run = begin fun h ->
+        let h = Sigma.to_evar_map h in
         let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
         let (h, x) = Evarutil.new_evar env h c in
         let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
-        (h, mkApp (f, [|x|]))
-      end
+        Sigma.Unsafe.of_pair (mkApp (f, [|x|]), h)
+      end }
     else
       Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
   end
@@ -1700,13 +1711,14 @@ let cut_and_apply c =
       | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
-        Proofview.Refine.refine begin fun sigma ->
+        Proofview.Refine.refine { run = begin fun sigma ->
+          let sigma = Sigma.to_evar_map sigma in
           let typ = mkProd (Anonymous, c2, concl) in
           let (sigma, f) = Evarutil.new_evar env sigma typ in
           let (sigma, x) = Evarutil.new_evar env sigma c1 in
           let ans = mkApp (f, [|mkApp (c, [|x|])|]) in
-          (sigma, ans)
-        end
+          Sigma.Unsafe.of_pair (ans, sigma)
+        end }
       | _ -> error "lapply needs a non-dependent product."
   end
 
@@ -1721,7 +1733,7 @@ let cut_and_apply c =
 (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
 
 let new_exact_no_check c =
-  Proofview.Refine.refine ~unsafe:true (fun h -> (h, c))
+  Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma (c, h, Sigma.refl) }
 
 let exact_check c =
   Proofview.Goal.enter begin fun gl ->
@@ -1763,7 +1775,7 @@ let assumption =
     in
     if is_same_type then
       (Proofview.Unsafe.tclEVARS sigma) <*>
-	Proofview.Refine.refine ~unsafe:true (fun h -> (h, mkVar id))
+	Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma (mkVar id, h, Sigma.refl) }
     else arec gl only_eq rest
   in
   let assumption_tac gl =
@@ -1845,9 +1857,11 @@ let clear_body ids =
       check_is_type env concl msg
     in
     check_hyps <*> check_concl <*>
-    Proofview.Refine.refine ~unsafe:true begin fun sigma ->
-      Evarutil.new_evar env sigma concl
-    end
+    Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+      let sigma = Sigma.to_evar_map sigma in
+      let (sigma, c) = Evarutil.new_evar env sigma concl in
+      Sigma.Unsafe.of_pair (c, sigma)
+    end }
   end
 
 let clear_wildcards ids =
@@ -2419,11 +2433,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let refl = applist (refl, [t;mkVar id]) in
       let newenv = insert_before [heq,None,eq;id,body,t] lastlhyp env in
       let (sigma,x) = new_evar newenv sigma ~principal:true ~store ccl in
-      (sigma,mkNamedLetIn id c t (mkNamedLetIn heq refl eq x))
+      Sigma.Unsafe.of_pair (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma)
   | None ->
       let newenv = insert_before [id,body,t] lastlhyp env in
       let (sigma,x) = new_evar newenv sigma ~principal:true ~store ccl in
-      (sigma,mkNamedLetIn id c t x)
+      Sigma.Unsafe.of_pair (mkNamedLetIn id c t x, sigma)
 
 let letin_tac with_eq id c ty occs =
   Proofview.Goal.nf_enter begin fun gl ->
@@ -2496,10 +2510,11 @@ let bring_hyps hyps =
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (instance_from_named_context hyps) in
-      Proofview.Refine.refine begin fun sigma ->
+      Proofview.Refine.refine { run = begin fun sigma ->
+        let sigma = Sigma.to_evar_map sigma in
         let (sigma, ev) = Evarutil.new_evar env sigma newcl in
-        (sigma, (mkApp (ev, args)))
-      end
+        Sigma.Unsafe.of_pair (mkApp (ev, args), sigma)
+      end }
     end
 
 let revert hyps = 
@@ -2608,10 +2623,11 @@ let new_generalize_gen_let lconstr =
 	0 lconstr ((concl, sigma), [])
     in
       Proofview.Unsafe.tclEVARS sigma <*>
-	Proofview.Refine.refine begin fun sigma ->
+	Proofview.Refine.refine { run = begin fun sigma ->
+          let sigma = Sigma.to_evar_map sigma in
           let (sigma, ev) = Evarutil.new_evar env sigma newcl in
-            (sigma, (applist (ev, args)))
-	end
+          Sigma.Unsafe.of_pair ((applist (ev, args)), sigma)
+	end }
   end
 
 let generalize_gen lconstr =
@@ -3951,11 +3967,13 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
           Tacticals.New.tclTHENLAST)
       (Tacticals.New.tclTHENLIST [
         Proofview.Unsafe.tclEVARS sigma;
-        Proofview.Refine.refine ~unsafe:true (fun sigma ->
+        Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+          let sigma = Sigma.to_evar_map sigma in
           let b = not with_evars && with_eq != None in
           let (sigma,c) = use_bindings env sigma elim b (c0,lbind) t0 in
           let t = Retyping.get_type_of env sigma c in
-          mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t));
+          mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t)
+        end };
         Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable);
         if is_arg_pure_hyp
         then Tacticals.New.tclTRY (Proofview.V82.tactic (thin [destVar c0]))
@@ -3971,8 +3989,10 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
       let env = reset_with_named_context sign env in
       Tacticals.New.tclTHENLIST [
         Proofview.Unsafe.tclEVARS sigma';
-        Proofview.Refine.refine ~unsafe:true (fun sigma ->
-          mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None);
+        Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+          let sigma = Sigma.to_evar_map sigma in
+          mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
+        end };
         tac
       ]
   end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ade89fc98..38e6ce0ea 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -430,7 +430,7 @@ end
 
 module New : sig
 
-  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*constr) -> unit Proofview.tactic
+  val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic
   (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c]
       followed by beta-iota-reduction of the conclusion. *)
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 805a29e39..439e20a86 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -20,6 +20,7 @@ open Libnames
 open Globnames
 open Constrintern
 open Constrexpr
+open Sigma.Notations
 (*i*)
 
 open Decl_kinds
@@ -322,7 +323,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 		if not (Option.is_empty term) then
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
-                      Proofview.Refine.refine (fun evm -> evm, Option.get term);
+                      Proofview.Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]