Cutting the dependency of Genarg in constr_expr, glob_constr

related types. This will ultimately allow putting genargs into
these ASTs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 147 insertions, 123 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
new file mode 100644
index 0000000000..540bca62e6
--- /dev/null
+++ b/interp/constrarg.ml
@@ -0,0 +1,67 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Loc
+open Pp
+open Names
+open Term
+open Libnames
+open Globnames
+open Glob_term
+open Genredexpr
+open Pattern
+open Constrexpr
+open Term
+open Misctypes
+open Genarg
+
+(** This is a hack for now, to break the dependency of Genarg on constr-related
+    types. We should use dedicated functions someday. *)
+
+let loc_of_or_by_notation f = function
+  | AN c -> f c
+  | ByNotation (loc,s,_) -> loc
+
+let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type =
+  Obj.magic t
+
+let wit_int_or_var = unsafe_of_type IntOrVarArgType
+
+let wit_intro_pattern = unsafe_of_type IntroPatternArgType
+
+let wit_ident_gen b = unsafe_of_type (IdentArgType b)
+
+let wit_ident = wit_ident_gen true
+
+let wit_pattern_ident = wit_ident_gen false
+
+let wit_var = unsafe_of_type VarArgType
+
+let wit_ref = unsafe_of_type RefArgType
+
+let wit_quant_hyp = unsafe_of_type QuantHypArgType
+
+let wit_genarg = unsafe_of_type GenArgType
+
+let wit_sort = unsafe_of_type SortArgType
+
+let wit_constr = unsafe_of_type ConstrArgType
+
+let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
+
+let wit_open_constr_gen b = unsafe_of_type (OpenConstrArgType b)
+
+let wit_open_constr = wit_open_constr_gen false
+
+let wit_casted_open_constr = wit_open_constr_gen true
+
+let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
+
+let wit_bindings = unsafe_of_type BindingsArgType
+
+let wit_red_expr = unsafe_of_type RedExprArgType
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
new file mode 100644
index 0000000000..548bd66905
--- /dev/null
+++ b/interp/constrarg.mli
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Generic arguments based on [constr]. We put them here to avoid a dependency
+    of Genarg in [constr]-related interfaces. *)
+
+open Loc
+open Pp
+open Names
+open Term
+open Libnames
+open Globnames
+open Glob_term
+open Genredexpr
+open Pattern
+open Constrexpr
+open Tacexpr
+open Term
+open Misctypes
+open Evd
+open Genarg
+
+(** FIXME: nothing to do there. *)
+val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
+
+(** {5 Additional generic arguments} *)
+
+val wit_int_or_var : int or_var uniform_genarg_type
+
+val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
+
+val wit_ident : Id.t uniform_genarg_type
+
+val wit_pattern_ident : Id.t uniform_genarg_type
+
+val wit_ident_gen : bool -> Id.t uniform_genarg_type
+
+val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
+
+val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
+
+val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
+
+val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) genarg_type
+
+val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
+
+val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
+
+val wit_constr_may_eval :
+  ((constr_expr,reference or_by_notation,constr_expr) may_eval,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
+  constr) genarg_type
+
+val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
+
+val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
+
+val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
+
+val wit_constr_with_bindings :
+  (constr_expr with_bindings,
+  glob_constr_and_expr with_bindings,
+  constr with_bindings sigma) genarg_type
+
+val wit_bindings :
+  (constr_expr bindings,
+  glob_constr_and_expr bindings,
+  constr bindings sigma) genarg_type
+
+val wit_red_expr :
+  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 83038c8ba0..c0526d5085 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -9,9 +9,6 @@
 open Pp
 open Util
 open Names
-open Glob_term
-open Constrexpr
-open Misctypes
 
 type argument_type =
   (* Basic types *)
@@ -59,16 +56,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2
 | _ -> false
 
-let loc_of_or_by_notation f = function
-  | AN c -> f c
-  | ByNotation (loc,s,_) -> loc
-
-type glob_constr_and_expr = glob_constr * constr_expr option
-type open_constr_expr = unit * constr_expr
-type open_glob_constr = unit * glob_constr_and_expr
-
-type glob_constr_pattern_and_expr = glob_constr_and_expr * Pattern.constr_pattern
-
 type ('raw, 'glob, 'top) genarg_type = argument_type
 
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
@@ -89,42 +76,6 @@ let rawwit t = t
 let glbwit t = t
 let topwit t = t
 
-let wit_int_or_var = IntOrVarArgType
-
-let wit_intro_pattern = IntroPatternArgType
-
-let wit_ident_gen b = IdentArgType b
-
-let wit_ident = wit_ident_gen true
-
-let wit_pattern_ident = wit_ident_gen false
-
-let wit_var = VarArgType
-
-let wit_ref = RefArgType
-
-let wit_quant_hyp = QuantHypArgType
-
-let wit_genarg = GenArgType
-
-let wit_sort = SortArgType
-
-let wit_constr = ConstrArgType
-
-let wit_constr_may_eval = ConstrMayEvalArgType
-
-let wit_open_constr_gen b = OpenConstrArgType b
-
-let wit_open_constr = wit_open_constr_gen false
-
-let wit_casted_open_constr = wit_open_constr_gen true
-
-let wit_constr_with_bindings = ConstrWithBindingsArgType
-
-let wit_bindings = BindingsArgType
-
-let wit_red_expr = RedExprArgType
-
 let wit_list0 t = List0ArgType t
 
 let wit_list1 t = List1ArgType t
diff --git a/interp/genarg.mli b/interp/genarg.mli
index bbd783047c..629bd62a78 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -9,28 +9,6 @@
 open Loc
 open Pp
 open Names
-open Term
-open Libnames
-open Globnames
-open Glob_term
-open Genredexpr
-open Pattern
-open Constrexpr
-open Term
-open Misctypes
-
-(** FIXME: nothing to do there. *)
-val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
-
-(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
-   in the environment by the effective calls to Intro, Inversion, etc 
-   The [constr_expr] field is [None] in TacDef though *)
-type glob_constr_and_expr = glob_constr * constr_expr option
-
-type open_constr_expr = unit * constr_expr
-type open_glob_constr = unit * glob_constr_and_expr
-
-type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 
 (** The route of a generic argument, from parsing to evaluation.
 In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
@@ -303,58 +281,6 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type
 
 (** {5 Basic generic type constructors} *)
 
-(** {6 Ground types} *)
-
-open Evd
-
-val wit_int_or_var : int or_var uniform_genarg_type
-
-val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
-
-val wit_ident : Id.t uniform_genarg_type
-
-val wit_pattern_ident : Id.t uniform_genarg_type
-
-val wit_ident_gen : bool -> Id.t uniform_genarg_type
-
-val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
-
-val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
-
-val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-
-val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) genarg_type
-
-val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
-
-val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
-
-val wit_constr_may_eval :
-  ((constr_expr,reference or_by_notation,constr_expr) may_eval,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
-  constr) genarg_type
-
-val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
-val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
-val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
-val wit_constr_with_bindings :
-  (constr_expr with_bindings,
-  glob_constr_and_expr with_bindings,
-  constr with_bindings sigma) genarg_type
-
-val wit_bindings :
-  (constr_expr bindings,
-  glob_constr_and_expr bindings,
-  constr bindings sigma) genarg_type
-
-val wit_red_expr :
-  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
-  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
-
 (** {6 Parameterized types} *)
 
 val wit_list0 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 86440bc297..77e2e5c00e 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -17,3 +17,4 @@ Constrextern
 Coqlib
 Discharge
 Declare
+Constrarg