Moving Ftactic and Geninterp to the engine folder.

5 files changed, 249 insertions, 0 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index 70b74edca..9ce5af819 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -7,3 +7,5 @@ Sigma
 Proofview_monad
 Evarutil
 Proofview
+Ftactic
+Geninterp
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
new file mode 100644
index 000000000..588709873
--- /dev/null
+++ b/engine/ftactic.ml
@@ -0,0 +1,106 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Proofview.Notations
+
+(** Focussing tactics *)
+
+type 'a focus =
+| Uniform of 'a
+| Depends of 'a list
+
+(** Type of tactics potentially goal-dependent. If it contains a [Depends],
+    then the length of the inner list is guaranteed to be the number of
+    currently focussed goals. Otherwise it means the tactic does not depend
+    on the current set of focussed goals. *)
+type 'a t = 'a focus Proofview.tactic
+
+let return (x : 'a) : 'a t = Proofview.tclUNIT (Uniform x)
+
+let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
+| Uniform x -> f x
+| Depends l ->
+  let f arg = f arg >>= function
+  | Uniform x ->
+    (** We dispatch the uniform result on each goal under focus, as we know
+        that the [m] argument was actually dependent. *)
+    Proofview.Goal.goals >>= fun l ->
+    let ans = List.map (fun _ -> x) l in
+    Proofview.tclUNIT ans
+  | Depends l -> Proofview.tclUNIT l
+  in
+  Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
+  Proofview.tclUNIT (Depends (List.concat l))
+
+let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
+let set_sigma r =
+  let Sigma.Sigma (ans, sigma, _) = r in
+  Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () -> ans
+
+let nf_enter f =
+  bind goals
+    (fun gl ->
+      gl >>= fun gl ->
+      Proofview.Goal.normalize gl >>= fun nfgl ->
+      Proofview.V82.wrap_exceptions (fun () -> f.enter nfgl))
+
+let nf_s_enter f =
+  bind goals
+    (fun gl ->
+      gl >>= fun gl ->
+      Proofview.Goal.normalize gl >>= fun nfgl ->
+      Proofview.V82.wrap_exceptions (fun () -> set_sigma (f.s_enter nfgl)))
+
+let enter f =
+  bind goals
+    (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f.enter gl))
+
+let s_enter f =
+  bind goals
+    (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> set_sigma (f.s_enter gl)))
+
+let with_env t =
+  t >>= function
+    | Uniform a ->
+        Proofview.tclENV >>= fun env -> Proofview.tclUNIT (Uniform (env,a))
+    | Depends l ->
+        Proofview.Goal.goals >>= fun gs ->
+        Proofview.Monad.(List.map (map Proofview.Goal.env) gs) >>= fun envs ->
+        Proofview.tclUNIT (Depends (List.combine envs l))
+
+let lift (type a) (t:a Proofview.tactic) : a t =
+  Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x))
+
+(** If the tactic returns unit, we can focus on the goals if necessary. *)
+let run m k = m >>= function
+| Uniform v -> k v
+| Depends l ->
+  let tacs = List.map k l in
+  Proofview.tclDISPATCH tacs
+
+let (>>=) = bind
+
+let (<*>) = fun m n -> bind m (fun () -> n)
+
+module Self =
+struct
+  type 'a t = 'a focus Proofview.tactic
+  let return = return
+  let (>>=) = bind
+  let (>>) = (<*>)
+  let map f x = x >>= fun a -> return (f a)
+end
+
+module Ftac = Monad.Make(Self)
+module List = Ftac.List
+
+module Notations =
+struct
+  let (>>=) = bind
+  let (<*>) = fun m n -> bind m (fun () -> n)
+end
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
new file mode 100644
index 000000000..19041f169
--- /dev/null
+++ b/engine/ftactic.mli
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Proofview.Notations
+
+(** Potentially focussing tactics *)
+
+type +'a focus
+
+type +'a t = 'a focus Proofview.tactic
+(** The type of focussing tactics. A focussing tactic is like a normal tactic,
+    except that it is able to remember it have entered a goal. Whenever this is
+    the case, each subsequent effect of the tactic is dispatched on the
+    focussed goals. This is a monad. *)
+
+(** {5 Monadic interface} *)
+
+val return : 'a -> 'a t
+(** The unit of the monad. *)
+
+val bind : 'a t -> ('a -> 'b t) -> 'b t
+(** The bind of the monad. *)
+
+(** {5 Operations} *)
+
+val lift : 'a Proofview.tactic -> 'a t
+(** Transform a tactic into a focussing tactic. The resulting tactic is not
+    focussed. *)
+
+val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
+(** Given a continuation producing a tactic, evaluates the focussing tactic. If
+    the tactic has not focussed, then the continuation is evaluated once.
+    Otherwise it is called in each of the currently focussed goals. *)
+
+(** {5 Focussing} *)
+
+val nf_enter : ([ `NF ], 'a t) enter -> 'a t
+(** Enter a goal. The resulting tactic is focussed. *)
+
+val enter : ([ `LZ ], 'a t) enter -> 'a t
+(** Enter a goal, without evar normalization. The resulting tactic is
+    focussed. *)
+
+val s_enter : ([ `LZ ], 'a t) s_enter -> 'a t
+(** Enter a goal and put back an evarmap. The resulting tactic is focussed. *)
+
+val nf_s_enter : ([ `NF ], 'a t) s_enter -> 'a t
+(** Enter a goal, without evar normalization and put back an evarmap. The
+    resulting tactic is focussed. *)
+
+val with_env : 'a t -> (Environ.env*'a) t
+(** [with_env t] returns, in addition to the return type of [t], an
+    environment, which is the global environment if [t] does not focus on
+    goals, or the local goal environment if [t] focuses on goals. *)
+
+(** {5 Notations} *)
+
+val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+(** Notation for {!bind}. *)
+
+val (<*>) : unit t -> 'a t -> 'a t
+(** Sequence. *)
+
+(** {5 List operations} *)
+
+module List : Monad.ListS with type '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/engine/geninterp.ml b/engine/geninterp.ml
new file mode 100644
index 000000000..008075800
--- /dev/null
+++ b/engine/geninterp.ml
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Genarg
+
+module TacStore = Store.Make(struct end)
+
+type interp_sign = {
+  lfun : Val.t Id.Map.t;
+  extra : TacStore.t }
+
+type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
+
+module InterpObj =
+struct
+  type ('raw, 'glb, 'top) obj = ('glb, 'top) interp_fun
+  let name = "interp"
+  let default _ = None
+end
+
+module Interp = Register(InterpObj)
+
+let interp = Interp.obj
+let register_interp0 = Interp.register0
+
+let generic_interp ist (GenArg (Glbwit wit, v)) =
+  let open Ftactic.Notations in
+  interp wit ist v >>= fun ans ->
+  Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
new file mode 100644
index 000000000..0992db7a2
--- /dev/null
+++ b/engine/geninterp.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Interpretation functions for generic arguments. *)
+
+open Names
+open Genarg
+
+module TacStore : Store.S
+
+type interp_sign = {
+  lfun : Val.t Id.Map.t;
+  extra : TacStore.t }
+
+type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
+
+val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun
+
+val generic_interp : (glob_generic_argument, Val.t) interp_fun
+
+val register_interp0 :
+  ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit