Basic stuff about constr_expr migrated from topconstr to constrexpr_ops

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

8 files changed, 200 insertions, 155 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
new file mode 100644
index 0000000000..18f0a38d4e
--- /dev/null
+++ b/interp/constrexpr_ops.ml
@@ -0,0 +1,142 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Libnames
+open Misctypes
+open Term
+open Mod_subst
+open Constrexpr
+open Decl_kinds
+
+(***********************)
+(* For binders parsing *)
+
+let default_binder_kind = Default Explicit
+
+let names_of_local_assums bl =
+  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
+
+let names_of_local_binders bl =
+  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
+
+(**********************************************************************)
+(* Functions on constr_expr *)
+
+let constr_loc = function
+  | CRef (Ident (loc,_)) -> loc
+  | CRef (Qualid (loc,_)) -> loc
+  | CFix (loc,_,_) -> loc
+  | CCoFix (loc,_,_) -> loc
+  | CProdN (loc,_,_) -> loc
+  | CLambdaN (loc,_,_) -> loc
+  | CLetIn (loc,_,_,_) -> loc
+  | CAppExpl (loc,_,_) -> loc
+  | CApp (loc,_,_) -> loc
+  | CRecord (loc,_,_) -> loc
+  | CCases (loc,_,_,_,_) -> loc
+  | CLetTuple (loc,_,_,_,_) -> loc
+  | CIf (loc,_,_,_,_) -> loc
+  | CHole (loc, _) -> loc
+  | CPatVar (loc,_) -> loc
+  | CEvar (loc,_,_) -> loc
+  | CSort (loc,_) -> loc
+  | CCast (loc,_,_) -> loc
+  | CNotation (loc,_,_) -> loc
+  | CGeneralization (loc,_,_,_) -> loc
+  | CPrim (loc,_) -> loc
+  | CDelimiters (loc,_,_) -> loc
+
+let cases_pattern_expr_loc = function
+  | CPatAlias (loc,_,_) -> loc
+  | CPatCstr (loc,_,_) -> loc
+  | CPatCstrExpl (loc,_,_) -> loc
+  | CPatAtom (loc,_) -> loc
+  | CPatOr (loc,_) -> loc
+  | CPatNotation (loc,_,_) -> loc
+  | CPatRecord (loc, _) -> loc
+  | CPatPrim (loc,_) -> loc
+  | CPatDelimiters (loc,_,_) -> loc
+
+let local_binder_loc = function
+  | LocalRawAssum ((loc,_)::_,_,t)
+  | LocalRawDef ((loc,_),t) -> join_loc loc (constr_loc t)
+  | LocalRawAssum ([],_,_) -> assert false
+
+let local_binders_loc bll =
+  if bll = [] then dummy_loc else
+  join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
+
+(** Pseudo-constructors *)
+
+let mkIdentC id  = CRef (Ident (dummy_loc, id))
+let mkRefC r     = CRef r
+let mkCastC (a,k)  = CCast (dummy_loc,a,k)
+let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
+let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
+let mkProdC (idl,bk,a,b)   = CProdN (dummy_loc,[idl,bk,a],b)
+
+let mkAppC (f,l) =
+  let l = List.map (fun x -> (x,None)) l in
+  match f with
+  | CApp (_,g,l') -> CApp (dummy_loc, g, l' @ l)
+  | _ -> CApp (dummy_loc, (None, f), l)
+
+let rec mkCProdN loc bll c =
+  match bll with
+  | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+      CProdN (loc,[idl,bk,t],mkCProdN (join_loc loc1 loc) bll c)
+  | LocalRawDef ((loc1,_) as id,b) :: bll ->
+      CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
+  | [] -> c
+  | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
+
+let rec mkCLambdaN loc bll c =
+  match bll with
+  | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+      CLambdaN (loc,[idl,bk,t],mkCLambdaN (join_loc loc1 loc) bll c)
+  | LocalRawDef ((loc1,_) as id,b) :: bll ->
+      CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
+  | [] -> c
+  | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
+
+let rec abstract_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
+  | LocalRawAssum (idl,bk,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
+      (abstract_constr_expr c bl)
+
+let rec prod_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+  | LocalRawAssum (idl,bk,t)::bl ->
+      List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
+      (prod_constr_expr c bl)
+
+let coerce_reference_to_id = function
+  | Ident (_,id) -> id
+  | Qualid (loc,_) ->
+      Errors.user_err_loc (loc, "coerce_reference_to_id",
+        str "This expression should be a simple identifier.")
+
+let coerce_to_id = function
+  | CRef (Ident (loc,id)) -> (loc,id)
+  | a -> Errors.user_err_loc
+        (constr_loc a,"coerce_to_id",
+         str "This expression should be a simple identifier.")
+
+let coerce_to_name = function
+  | CRef (Ident (loc,id)) -> (loc,Name id)
+  | CHole (loc,_) -> (loc,Anonymous)
+  | a -> Errors.user_err_loc
+        (constr_loc a,"coerce_to_name",
+         str "This expression should be a name.")
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
new file mode 100644
index 0000000000..868d53f33f
--- /dev/null
+++ b/interp/constrexpr_ops.mli
@@ -0,0 +1,53 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Libnames
+open Misctypes
+open Term
+open Mod_subst
+open Constrexpr
+
+(** Constrexpr_ops: utilities on [constr_expr] *)
+
+val constr_loc : constr_expr -> loc
+
+val cases_pattern_expr_loc : cases_pattern_expr -> loc
+
+val local_binders_loc : local_binder list -> loc
+
+val default_binder_kind : binder_kind
+
+val mkIdentC : identifier -> constr_expr
+val mkRefC : reference -> constr_expr
+val mkAppC : constr_expr * constr_expr list -> constr_expr
+val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
+val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
+val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
+val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
+
+val coerce_reference_to_id : reference -> identifier
+val coerce_to_id : constr_expr -> identifier located
+val coerce_to_name : constr_expr -> name located
+
+val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
+
+(** Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
+val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr
+val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr
+
+(** For binders parsing *)
+
+(** With let binders *)
+val names_of_local_assums : local_binder list -> name located list
+
+(** Does not take let binders into account *)
+val names_of_local_binders : local_binder list -> name located list
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c8a43c866c..87a5ce73b1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -22,6 +22,7 @@ open Environ
 open Libnames
 open Impargs
 open Constrexpr
+open Constrexpr_ops
 open Notation_term
 open Notation_ops
 open Topconstr
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7b5a8ebbb5..480dc6ce26 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -22,6 +22,7 @@ open Patternops
 open Pretyping
 open Cases
 open Constrexpr
+open Constrexpr_ops
 open Notation_term
 open Notation_ops
 open Topconstr
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a39347d556..d6e7485dc3 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -246,7 +246,7 @@ let combine_params avoid fn applied needed =
 	    aux (t' :: ids) avoid' app need
 
       | (x,_) :: _, [] ->
-	  user_err_loc (Topconstr.constr_loc x,"",str "Typeclass does not expect more arguments")
+	  user_err_loc (Constrexpr_ops.constr_loc x,"",str "Typeclass does not expect more arguments")
   in aux [] avoid applied needed
 
 let combine_params_freevar =
diff --git a/interp/interp.mllib b/interp/interp.mllib
index ff2549a039..ad3350f916 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,5 +1,6 @@
 Tok
 Lexer
+Constrexpr_ops
 Notation_ops
 Topconstr
 Ppextend
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index f3bec1d0b8..824b7f59af 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -20,6 +20,7 @@ open Mod_subst
 open Misctypes
 open Decl_kinds
 open Constrexpr
+open Constrexpr_ops
 open Notation_term
 (*i*)
 
@@ -34,17 +35,6 @@ let write_oldfashion_patterns = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> oldfashion_patterns:=a);
 }
 
-(***********************)
-(* For binders parsing *)
-
-let default_binder_kind = Default Explicit
-
-let names_of_local_assums bl =
-  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
-
-let names_of_local_binders bl =
-  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
-
 (**********************************************************************)
 (* Miscellaneous *)
 
@@ -54,50 +44,6 @@ let error_invalid_pattern_notation loc =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
-let constr_loc = function
-  | CRef (Ident (loc,_)) -> loc
-  | CRef (Qualid (loc,_)) -> loc
-  | CFix (loc,_,_) -> loc
-  | CCoFix (loc,_,_) -> loc
-  | CProdN (loc,_,_) -> loc
-  | CLambdaN (loc,_,_) -> loc
-  | CLetIn (loc,_,_,_) -> loc
-  | CAppExpl (loc,_,_) -> loc
-  | CApp (loc,_,_) -> loc
-  | CRecord (loc,_,_) -> loc
-  | CCases (loc,_,_,_,_) -> loc
-  | CLetTuple (loc,_,_,_,_) -> loc
-  | CIf (loc,_,_,_,_) -> loc
-  | CHole (loc, _) -> loc
-  | CPatVar (loc,_) -> loc
-  | CEvar (loc,_,_) -> loc
-  | CSort (loc,_) -> loc
-  | CCast (loc,_,_) -> loc
-  | CNotation (loc,_,_) -> loc
-  | CGeneralization (loc,_,_,_) -> loc
-  | CPrim (loc,_) -> loc
-  | CDelimiters (loc,_,_) -> loc
-
-let cases_pattern_expr_loc = function
-  | CPatAlias (loc,_,_) -> loc
-  | CPatCstr (loc,_,_) -> loc
-  | CPatCstrExpl (loc,_,_) -> loc
-  | CPatAtom (loc,_) -> loc
-  | CPatOr (loc,_) -> loc
-  | CPatNotation (loc,_,_) -> loc
-  | CPatRecord (loc, _) -> loc
-  | CPatPrim (loc,_) -> loc
-  | CPatDelimiters (loc,_,_) -> loc
-
-let local_binder_loc = function
-  | LocalRawAssum ((loc,_)::_,_,t)
-  | LocalRawDef ((loc,_),t) -> join_loc loc (constr_loc t)
-  | LocalRawAssum ([],_,_) -> assert false
-
-let local_binders_loc bll =
-  if bll = [] then dummy_loc else
-  join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
-
 let ids_of_cases_indtype =
   let rec vars_of ids = function
     (* We deal only with the regular cases *)
@@ -202,70 +148,6 @@ let free_vars_of_constr_expr c =
 
 let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c)
 
-let mkIdentC id  = CRef (Ident (dummy_loc, id))
-let mkRefC r     = CRef r
-let mkCastC (a,k)  = CCast (dummy_loc,a,k)
-let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
-let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
-let mkProdC (idl,bk,a,b)   = CProdN (dummy_loc,[idl,bk,a],b)
-
-let mkAppC (f,l) =
-  let l = List.map (fun x -> (x,None)) l in
-  match f with
-  | CApp (_,g,l') -> CApp (dummy_loc, g, l' @ l)
-  | _ -> CApp (dummy_loc, (None, f), l)
-
-let rec mkCProdN loc bll c =
-  match bll with
-  | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CProdN (loc,[idl,bk,t],mkCProdN (join_loc loc1 loc) bll c)
-  | LocalRawDef ((loc1,_) as id,b) :: bll ->
-      CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
-  | [] -> c
-  | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
-
-let rec mkCLambdaN loc bll c =
-  match bll with
-  | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CLambdaN (loc,[idl,bk,t],mkCLambdaN (join_loc loc1 loc) bll c)
-  | LocalRawDef ((loc1,_) as id,b) :: bll ->
-      CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
-  | [] -> c
-  | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
-
-let rec abstract_constr_expr c = function
-  | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
-  | LocalRawAssum (idl,bk,t)::bl ->
-      List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
-      (abstract_constr_expr c bl)
-
-let rec prod_constr_expr c = function
-  | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
-  | LocalRawAssum (idl,bk,t)::bl ->
-      List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
-      (prod_constr_expr c bl)
-
-let coerce_reference_to_id = function
-  | Ident (_,id) -> id
-  | Qualid (loc,_) ->
-      user_err_loc (loc, "coerce_reference_to_id",
-        str "This expression should be a simple identifier.")
-
-let coerce_to_id = function
-  | CRef (Ident (loc,id)) -> (loc,id)
-  | a -> user_err_loc
-        (constr_loc a,"coerce_to_id",
-         str "This expression should be a simple identifier.")
-
-let coerce_to_name = function
-  | CRef (Ident (loc,id)) -> (loc,Name id)
-  | CHole (loc,_) -> (loc,Anonymous)
-  | a -> user_err_loc
-        (constr_loc a,"coerce_to_name",
-         str "This expression should be a name.")
-
 (* Interpret the index of a recursion order annotation *)
 
 let split_at_annot bl na =
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 7556f13856..482d409ba9 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -24,52 +24,17 @@ val oldfashion_patterns : bool ref
 
 (** Utilities on constr_expr                                           *)
 
-val constr_loc : constr_expr -> loc
-
-val cases_pattern_expr_loc : cases_pattern_expr -> loc
-
-val local_binders_loc : local_binder list -> loc
-
 val replace_vars_constr_expr :
   (identifier * identifier) list -> constr_expr -> constr_expr
 
 val free_vars_of_constr_expr : constr_expr -> Idset.t
 val occur_var_constr_expr : identifier -> constr_expr -> bool
 
-val default_binder_kind : binder_kind
-
 (** Specific function for interning "in indtype" syntax of "match" *)
 val ids_of_cases_indtype : cases_pattern_expr -> identifier list
 
-val mkIdentC : identifier -> constr_expr
-val mkRefC : reference -> constr_expr
-val mkAppC : constr_expr * constr_expr list -> constr_expr
-val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
-val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
-val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
-val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
-
-val coerce_reference_to_id : reference -> identifier
-val coerce_to_id : constr_expr -> identifier located
-val coerce_to_name : constr_expr -> name located
-
 val split_at_annot : local_binder list -> identifier located option -> local_binder list * local_binder list
 
-val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
-val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
-
-(** Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
-val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr
-val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr
-
-(** For binders parsing *)
-
-(** With let binders *)
-val names_of_local_binders : local_binder list -> name located list
-
-(** Does not take let binders into account *)
-val names_of_local_assums : local_binder list -> name located list
-
 (** Used in typeclasses *)
 
 val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->