Change the toplevel representation of Ltac values to an untyped one.

This brings the evaluation model of Ltac closer to those of usual languages, and
further allows the integration of static typing in the long run. More precisely,
toplevel constructed values such as lists and the like do not carry anymore the
type of the underlying data they contain.

This is mostly an API change, as it did not break any contrib outside of mathcomp.

5 files changed, 352 insertions, 0 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index 70b74edca3..9ce5af8195 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 0000000000..588709873e
--- /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 0000000000..19041f1698
--- /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 0000000000..45b0aa2316
--- /dev/null
+++ b/engine/geninterp.ml
@@ -0,0 +1,98 @@
+(************************************************************************)
+(*  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)
+
+(** Dynamic toplevel values *)
+
+module ValT = Dyn.Make(struct end)
+
+module Val =
+struct
+
+  type 'a typ = 'a ValT.tag
+
+  type _ tag =
+  | Base : 'a typ -> 'a tag
+  | List : 'a tag -> 'a list tag
+  | Opt : 'a tag -> 'a option tag
+  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
+
+  type t = Dyn : 'a typ * 'a -> t
+
+  let eq = ValT.eq
+  let repr = ValT.repr
+  let create = ValT.create
+
+  let rec pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t)
+
+  let typ_list = ValT.create "list"
+  let typ_opt = ValT.create "option"
+  let typ_pair = ValT.create "pair"
+
+  let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with
+  | Base t -> Dyn (t, x)
+  | List tag -> Dyn (typ_list, List.map (fun x -> inject tag x) x)
+  | Opt tag -> Dyn (typ_opt, Option.map (fun x -> inject tag x) x)
+  | Pair (tag1, tag2) ->
+    Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x)))
+
+end
+
+module ValReprObj =
+struct
+  type ('raw, 'glb, 'top) obj = 'top Val.tag
+  let name = "valrepr"
+  let default _ = None
+end
+
+module ValRepr = Register(ValReprObj)
+
+let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
+| ListArg t -> Val.List (val_tag t)
+| OptArg t -> Val.Opt (val_tag t)
+| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2)
+| ExtraArg s -> ValRepr.obj (ExtraArg s)
+
+let val_tag = function Topwit t -> val_tag t
+
+let register_val0 wit tag =
+  let tag = match tag with
+  | None ->
+    let name = match wit with
+    | ExtraArg s -> ArgT.repr s
+    | _ -> assert false
+    in
+    Val.Base (Val.create name)
+  | Some tag -> tag
+  in
+  ValRepr.register0 wit tag
+
+(** Interpretation functions *)
+
+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, Val.t) interp_fun
+  let name = "interp"
+  let default _ = None
+end
+
+module Interp = Register(InterpObj)
+
+let interp = Interp.obj
+
+let register_interp0 = Interp.register0
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
new file mode 100644
index 0000000000..42e1e3784c
--- /dev/null
+++ b/engine/geninterp.mli
@@ -0,0 +1,67 @@
+(************************************************************************)
+(*  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
+
+(** {6 Dynamic toplevel values} *)
+
+module Val :
+sig
+  type 'a typ
+
+  val create : string -> 'a typ
+
+  type _ tag =
+  | Base : 'a typ -> 'a tag
+  | List : 'a tag -> 'a list tag
+  | Opt : 'a tag -> 'a option tag
+  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
+
+  type t = Dyn : 'a typ * 'a -> t
+
+  val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option
+  val repr : 'a typ -> string
+  val pr : 'a typ -> Pp.std_ppcmds
+
+  val typ_list : t list typ
+  val typ_opt : t option typ
+  val typ_pair : (t * t) typ
+
+  val inject : 'a tag -> 'a -> t
+
+end
+(** Dynamic types for toplevel values. While the generic types permit to relate
+    objects at various levels of interpretation, toplevel values are wearing
+    their own type regardless of where they came from. This allows to use the
+    same runtime representation for several generic types. *)
+
+val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
+(** Retrieve the dynamic type associated to a toplevel genarg. *)
+
+val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit
+(** Register the representation of a generic argument. If no tag is given as
+    argument, a new fresh tag with the same name as the argument is associated
+    to the generic type. *)
+
+(** {6 Interpretation functions} *)
+
+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, Val.t) interp_fun
+
+val register_interp0 :
+  ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit