Merge PR #6186: [api] Miscellaneous consolidation.

9 files changed, 180 insertions, 8 deletions

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 3a139b7b03..43dbc31058 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -13,8 +13,8 @@ open Environ
 open EConstr
 open Inductiveops
 open Glob_term
-open Evarutil
 open Ltac_pretype
+open Evardefine
 
 (** {5 Compilation of pattern-matching } *)
 
@@ -116,7 +116,7 @@ type 'a pattern_matching_problem =
 val compile : 'a pattern_matching_problem -> unsafe_judgment
 
 val prepare_predicate : ?loc:Loc.t ->
-           (Evarutil.type_constraint ->
+           (type_constraint ->
             Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 681eb17d3c..18e0c31dd6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Names
-open Term
 open Constr
 open Termops
 open Environ
@@ -49,7 +48,7 @@ let _ = Goptions.declare_bool_option {
    "data.id.type" etc... *)
 let impossible_default_case () =
   let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
-  let (_, u) = Term.destConst c in
+  let (_, u) = Constr.destConst c in
   Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx)
 
 let coq_unit_judge =
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 18dbbea1bd..b646a37f8a 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Sorts
 open Util
 open Pp
 open Names
-open Term
 open Constr
 open Termops
 open EConstr
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index fba1542912..e6d1e59b3a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Sorts
 open Util
 open CErrors
 open Names
-open Term
 open Constr
 open Environ
 open Termops
diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml
new file mode 100644
index 0000000000..768ef3cfd9
--- /dev/null
+++ b/pretyping/geninterp.ml
@@ -0,0 +1,100 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \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 ()
+
+(** Dynamic toplevel values *)
+
+module ValT = Dyn.Make ()
+
+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 pr : type a. a typ -> Pp.t = 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 ValTMap = ValT.Map
+
+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/pretyping/geninterp.mli b/pretyping/geninterp.mli
new file mode 100644
index 0000000000..ae0b26e594
--- /dev/null
+++ b/pretyping/geninterp.mli
@@ -0,0 +1,72 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Interpretation functions for generic arguments and interpreted Ltac
+    values. *)
+
+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.t
+
+  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
+
+module ValTMap (M : Dyn.TParam) :
+  Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ
+
+(** 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
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index eb2b435bf6..b2735ee22c 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -17,8 +17,8 @@ open Environ
 open Evd
 open EConstr
 open Glob_term
-open Evarutil
 open Ltac_pretype
+open Evardefine
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 9904b73540..1da5b4567f 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,3 +1,4 @@
+Geninterp
 Ltac_pretype
 Locusops
 Pretype_errors
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e6d8a0af26..9ff9a75b3e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -213,7 +213,7 @@ let compute_canonical_projections warn (con,ind) =
   let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
   let t = EConstr.Unsafe.to_constr t in
   let lt = List.rev_map snd sign in
-  let args = snd (Term.decompose_app t) in
+  let args = snd (decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
     lookup_structure ind in
   let params, projs = List.chop p args in