Implementing non-focussed generic arguments.

Kind of enhances the situation of bug #4409. Now arguments can be interpreted
globally or focussedly in a dynamic fashion because the interpretation function
returns a Ftactic.t. The bug is not fixed yet because we should tweak the
interpretation of tactic arguments.

6 files changed, 105 insertions, 129 deletions

diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index a688b9487..f8437b559 100644
--- a/tactics/ftactic.ml
+++ b/tactics/ftactic.ml
@@ -84,3 +84,9 @@ module Ftac = Monad.Make(Self)
 module List = Ftac.List
 
 let debug_prompt = Tactic_debug.debug_prompt
+
+module Notations =
+struct
+  let (>>=) = bind
+  let (<*>) = fun m n -> bind m (fun () -> n)
+end
diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli
index 449649922..a20d8a9c3 100644
--- a/tactics/ftactic.mli
+++ b/tactics/ftactic.mli
@@ -67,3 +67,11 @@ module List : Monad.ListS with type 'a t := 'a t
 
 val debug_prompt :
   int -> Tacexpr.glob_tactic_expr -> (Tactic_debug.debug_info -> 'a t) -> 'a t
+
+(** {5 Notations} *)
+
+module Notations :
+sig
+  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+  val (<*>) : unit t -> 'a t -> 'a t
+end
diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
index 3da1d542b..dff87d3a8 100644
--- a/tactics/geninterp.ml
+++ b/tactics/geninterp.ml
@@ -15,8 +15,7 @@ type interp_sign = {
   lfun : Val.t Id.Map.t;
   extra : TacStore.t }
 
-type ('glb, 'top) interp_fun = interp_sign ->
-    Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top
+type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
 
 module InterpObj =
 struct
@@ -30,9 +29,10 @@ module Interp = Register(InterpObj)
 let interp = Interp.obj
 let register_interp0 = Interp.register0
 
-let generic_interp ist gl v =
+let generic_interp ist v =
+  let open Ftactic.Notations in
   let unpacker wit v =
-    let (sigma, ans) = interp wit ist gl (glb v) in
-    (sigma, Val.Dyn (val_tag (topwit wit), ans))
+    interp wit ist (glb v) >>= fun ans ->
+    Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
   in
   unpack { unpacker; } v
diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli
index 472ff1090..34261c507 100644
--- a/tactics/geninterp.mli
+++ b/tactics/geninterp.mli
@@ -17,8 +17,7 @@ type interp_sign = {
   lfun : Val.t Id.Map.t;
   extra : TacStore.t }
 
-type ('glb, 'top) interp_fun = interp_sign ->
-    Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top
+type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
 
 val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ff6662809..5e5b2be24 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1123,6 +1123,15 @@ let rec read_match_rule lfun ist env sigma = function
 let mk_hyp_value ist env sigma c =
   (mkVar (interp_hyp ist env sigma c))
 
+let interp_focussed wit f v =
+  Ftactic.nf_enter begin fun gl ->
+    let v = Genarg.out_gen (glbwit wit) v in
+    let env = Proofview.Goal.env gl in
+    let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+    let v = in_gen (topwit wit) (f env sigma v) in
+    Ftactic.return v
+  end
+
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t =
   (* The name [appl] of applied top-level Ltac names is ignored in
@@ -1239,14 +1248,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       | ConstrArgType
       | ListArgType ConstrArgType
       | OptArgType _ | PairArgType _ -> (** generic handler *)
-        Ftactic.nf_enter begin fun gl ->
-          let sigma = Tacmach.New.project gl in
-          let env = Proofview.Goal.env gl in
-          let concl = Proofview.Goal.concl gl in
-          let goal = Proofview.Goal.goal gl in
-          let (sigma, arg) = interp_genarg ist env sigma concl goal x in
-          Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return arg)
-        end
+        interp_genarg ist x
       | _ as tag -> (** Special treatment. TODO: use generic handler  *)
         Ftactic.nf_enter begin fun gl ->
           let sigma = Tacmach.New.project gl in
@@ -1280,9 +1282,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
                 let tac = Genarg.out_gen (glbwit wit_tactic) x in
                 val_interp ist tac
               else
-                let goal = Proofview.Goal.goal gl in
-                let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in
-                Ftactic.(lift (Proofview.Unsafe.tclEVARS newsigma) <*> return v)
+                Geninterp.generic_interp ist x
           | _ -> assert false
         end
       in
@@ -1311,43 +1311,18 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       in
       Ftactic.run tac (fun () -> Proofview.tclUNIT ())
 
-  | TacML (loc,opn,l) when List.for_all global_genarg l ->
-      let trace = push_trace (loc,LtacMLCall tac) ist in
-      let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
-      (* spiwack: a special case for tactics (from TACTIC EXTEND) when
-         every argument can be interpreted without a
-         [Proofview.Goal.nf_enter]. *)
-      let tac = Tacenv.interp_ml_tactic opn in
-      (* dummy values, will be ignored *)
-      let env = Environ.empty_env in
-      let sigma = Evd.empty in
-      let concl = Term.mkRel (-1) in
-      let goal = Evar.unsafe_of_int (-1) in
-      (* /dummy values *)
-      let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in
-      let l = List.map2 (print_top_val env) l args in
-      let name () = Pptactic.pr_extend_gen (fun x -> x) 0 opn l in
-      Proofview.Trace.name_tactic name
-        (catch_error_tac trace (tac args ist))
   | TacML (loc,opn,l) ->
+      let open Ftactic.Notations in
       let trace = push_trace (loc,LtacMLCall tac) ist in
       let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
-      Proofview.Goal.nf_enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let goal_sigma = Tacmach.New.project gl in
-        let concl = Proofview.Goal.concl gl in
-        let goal = Proofview.Goal.goal gl in
-        let tac = Tacenv.interp_ml_tactic opn in
-        let (sigma,args) =
-          Evd.MonadR.List.map_right
-            (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma
-        in
-        Proofview.Unsafe.tclEVARS sigma <*>
-        let l = List.map2 (print_top_val env) l args in
+      let tac = Tacenv.interp_ml_tactic opn in
+      let args = Ftactic.List.map_right (fun a -> interp_genarg ist a) l in
+      let tac args =
+        let l = List.map2 (print_top_val ()) l args in
         let name () = Pptactic.pr_extend_gen (fun x -> x) 0 opn l in
-        Proofview.Trace.name_tactic name
-          (catch_error_tac trace (tac args ist))
-      end }
+        Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist))
+      in
+      Ftactic.run args tac
 
 and force_vrec ist v : Val.t Ftactic.t =
   let v = Value.normalize v in
@@ -1381,12 +1356,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t =
 and interp_tacarg ist arg : Val.t Ftactic.t =
   match arg with
   | TacGeneric arg ->
-      Ftactic.nf_enter begin fun gl ->
-        let sigma = Tacmach.New.project gl in
-        let goal = Proofview.Goal.goal gl in
-        let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in
-        Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
-      end
+      Geninterp.generic_interp ist arg
   | Reference r -> interp_ltac_reference dloc false ist r
   | ConstrMayEval c ->
       Ftactic.enter begin fun gl ->
@@ -1595,93 +1565,79 @@ and interp_match_goal ist lz lr lmr =
     end
 
 (* Interprets extended tactic generic arguments *)
-(* spiwack: interp_genarg has an argument [concl] for the case of
-   "casted open constr". And [gl] for [Geninterp]. I haven't changed
-   the interface for geninterp yet as it is used by ARGUMENT EXTEND
-   (in turn used by plugins). At the time I'm writing this comment
-   though, the only concerned plugins are the declarative mode (which
-   needs the [extra] field of goals to interprete rules) and ssreflect
-   (a handful of time). I believe we'd need to address "casted open
-   constr" and the declarative mode rules to provide a reasonable
-   interface. *)
-and interp_genarg ist env sigma concl gl x =
-  let evdref = ref sigma in
-  let rec interp_genarg x =
+and interp_genarg ist x : Val.t Ftactic.t =
+    let open Ftactic.Notations in
     match genarg_tag x with
     | IdentArgType ->
-      in_gen (topwit wit_ident)
-        (interp_ident ist env sigma (Genarg.out_gen (glbwit wit_ident) x))
+      interp_focussed wit_ident (interp_ident ist) x
     | VarArgType ->
-      in_gen (topwit wit_var) (interp_hyp ist env sigma (Genarg.out_gen (glbwit wit_var) x))
+      interp_focussed wit_var (interp_hyp ist) x
     | ConstrArgType ->
-      let (sigma,c_interp) =
-        interp_constr ist env !evdref (Genarg.out_gen (glbwit wit_constr) x)
-      in
-      evdref := sigma;
-      in_gen (topwit wit_constr) c_interp
+      Ftactic.nf_enter begin fun gl ->
+        let c = Genarg.out_gen (glbwit wit_constr) x in
+        let env = Proofview.Goal.env gl in
+        let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+        let (sigma, c) = interp_constr ist env sigma c in
+        let c = in_gen (topwit wit_constr) c in
+        Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return c)
+      end
     | ListArgType ConstrArgType ->
-        let (sigma,v) = interp_genarg_constr_list ist env !evdref x in
-	evdref := sigma;
-	v
-    | ListArgType VarArgType -> interp_genarg_var_list ist env sigma x
+      interp_genarg_constr_list ist x
+    | ListArgType VarArgType ->
+      interp_genarg_var_list ist x
     | ListArgType _ ->
       let list_unpacker wit l =
         let map x =
-          let x = interp_genarg (Genarg.in_gen (glbwit wit) x) in
-          Value.cast (topwit wit) x
+          interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
+          Ftactic.return (Value.cast (topwit wit) x)
         in
-        Value.of_list (val_tag wit) (List.map map (glb l))
+        Ftactic.List.map map (glb l) >>= fun l ->
+        Ftactic.return (Value.of_list (val_tag wit) l)
       in
       list_unpack { list_unpacker } x
     | OptArgType _ ->
       let opt_unpacker wit o = match glb o with
-      | None -> Value.of_option (val_tag wit) None
+      | None -> Ftactic.return (Value.of_option (val_tag wit) None)
       | Some x ->
-        let x = interp_genarg (Genarg.in_gen (glbwit wit) x) in
+        interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
         let x = Value.cast (topwit wit) x in
-        Value.of_option (val_tag wit) (Some x)
+        Ftactic.return (Value.of_option (val_tag wit) (Some x))
       in
       opt_unpack { opt_unpacker } x
     | PairArgType _ ->
       let pair_unpacker wit1 wit2 o =
         let (p, q) = glb o in
-        let p = interp_genarg (Genarg.in_gen (glbwit wit1) p) in
-        let q = interp_genarg (Genarg.in_gen (glbwit wit2) q) in
+        interp_genarg ist (Genarg.in_gen (glbwit wit1) p) >>= fun p ->
+        interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q ->
         let p = Value.cast (topwit wit1) p in
         let q = Value.cast (topwit wit2) q in
-        Val.Dyn (Val.Pair (val_tag wit1, val_tag wit2), (p, q))
+        Ftactic.return (Val.Dyn (Val.Pair (val_tag wit1, val_tag wit2), (p, q)))
       in
       pair_unpack { pair_unpacker } x
-    | ExtraArgType s ->
-        let (sigma,v) = Geninterp.generic_interp ist { Evd.it=gl;sigma=(!evdref) } x in
-	evdref:=sigma;
-	v
-  in
-  let v = interp_genarg x in
-  !evdref , v
-
+    | ExtraArgType _ ->
+      Geninterp.generic_interp ist x
 
 (** returns [true] for genargs which have the same meaning
     independently of goals. *)
 
-and global_genarg =
-  let rec global_tag = function
-    | ExtraArgType "int_or_var" -> true (** FIXME *)
-    | ListArgType t | OptArgType t -> global_tag t
-    | PairArgType (t1,t2) -> global_tag t1 && global_tag t2
-    | _ -> false
-  in
-  fun x -> global_tag (genarg_tag x)
-
-and interp_genarg_constr_list ist env sigma x =
+and interp_genarg_constr_list ist x =
+  Ftactic.nf_enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in
   let (sigma,lc) = interp_constr_list ist env sigma lc in
-  sigma , Value.of_list (val_tag wit_constr) lc
+  let lc = Value.of_list (val_tag wit_constr) lc in
+  Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return lc)
+  end
 
-and interp_genarg_var_list ist env sigma x =
+and interp_genarg_var_list ist x =
+  Ftactic.nf_enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in
   let lc = interp_hyp_list ist env sigma lc in
-  Value.of_list (val_tag wit_var) lc
+  Ftactic.return (Value.of_list (val_tag wit_var) lc)
+  end
 
 (* Interprets tactic expressions : returns a "constr" *)
 and interp_ltac_constr ist e : constr Ftactic.t =
@@ -2226,7 +2182,7 @@ let hide_interp global t ot =
 
 let def_intern ist x = (ist, x)
 let def_subst _ x = x
-let def_interp ist gl x = (project gl, x)
+let def_interp ist x = Ftactic.return x
 
 let declare_uniform t =
   Genintern.register_intern0 t def_intern;
@@ -2248,26 +2204,36 @@ let () =
 let () =
   declare_uniform wit_pre_ident
 
-let lift f = (); fun ist gl x -> (project gl, f ist (pf_env gl) (project gl) x)
-let lifts f = (); fun ist gl x -> f ist (pf_env gl) (project gl) x
+let lift f = (); fun ist x -> Ftactic.nf_enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+  Ftactic.return (f ist env sigma x)
+end
+
+let lifts f = (); fun ist x -> Ftactic.nf_enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+  let (sigma, v) = f ist env sigma x in
+  Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
+end
 
-let interp_bindings' ist gl bl = (project gl, { delayed = fun env sigma ->
+let interp_bindings' ist bl = Ftactic.return { delayed = fun env sigma ->
   let (sigma, bl) = interp_bindings ist env (Sigma.to_evar_map sigma) bl in
   Sigma.Unsafe.of_pair (bl, sigma)
-  })
+  }
 
-let interp_constr_with_bindings' ist gl c = (project gl, { delayed = fun env sigma ->
+let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma ->
   let (sigma, c) = interp_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in
   Sigma.Unsafe.of_pair (c, sigma)
-  })
+  }
 
 let () =
-  Geninterp.register_interp0 wit_int_or_var (fun ist gl n -> project gl, interp_int_or_var ist n);
+  Geninterp.register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
   Geninterp.register_interp0 wit_ref (lift interp_reference);
   Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
   Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause);
   Geninterp.register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s));
-  Geninterp.register_interp0 wit_tacvalue (fun ist gl c -> project gl, c);
+  Geninterp.register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v);
   Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr);
   Geninterp.register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis);
   Geninterp.register_interp0 wit_open_constr (lifts interp_open_constr);
@@ -2277,16 +2243,16 @@ let () =
   ()
 
 let () =
-  let interp ist gl tac =
+  let interp ist tac =
     let f = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
-    (project gl, TacArg (dloc, TacGeneric (Genarg.in_gen (glbwit wit_tacvalue) f)))
+    Ftactic.return (TacArg (dloc, TacGeneric (Genarg.in_gen (glbwit wit_tacvalue) f)))
   in
   Geninterp.register_interp0 wit_tactic interp
 
 let () =
-  Geninterp.register_interp0 wit_uconstr (fun ist gl c ->
-     project gl , interp_uconstr ist (pf_env gl) c
-  )
+  Geninterp.register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter begin fun gl ->
+    Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c)
+  end)
 
 (***************************************************************************)
 (* Other entry points *)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 5b81da74a..47a16a3bc 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -54,10 +54,7 @@ val get_debug : unit -> debug_info
 
 (** Adds an interpretation function for extra generic arguments *)
 
-(* spiwack: the [Term.constr] argument is the conclusion of the goal,
-   for "casted open constr" *)
-val interp_genarg : interp_sign -> Environ.env -> Evd.evar_map -> Term.constr -> Goal.goal ->
-  glob_generic_argument -> Evd.evar_map * Value.t
+val interp_genarg : interp_sign -> glob_generic_argument -> Value.t Ftactic.t
 
 (** Interprets any expression *)
 val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tactic) -> unit Proofview.tactic