New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr

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

6 files changed, 65 insertions, 64 deletions

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index aed71c3ae..2047b5326 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -10,7 +10,7 @@ open Util
 open Term
 open Names
 open Pp
-open Topconstr
+open Constrexpr
 open Indfun_common
 open Indfun
 open Genarg
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index ccf2caaf5..95c6a6d99 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1256,13 +1256,13 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
 
 let rec rebuild_return_type rt =
   match rt with
-    | Topconstr.CProdN(loc,n,t') ->
-	Topconstr.CProdN(loc,n,rebuild_return_type t')
-    | Topconstr.CLetIn(loc,na,t,t') ->
-	Topconstr.CLetIn(loc,na,t,rebuild_return_type t')
-    | _ -> Topconstr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous],
-				       Topconstr.Default Decl_kinds.Explicit,rt],
-			    Topconstr.CSort(dummy_loc,GType None))
+    | Constrexpr.CProdN(loc,n,t') ->
+	Constrexpr.CProdN(loc,n,rebuild_return_type t')
+    | Constrexpr.CLetIn(loc,na,t,t') ->
+	Constrexpr.CLetIn(loc,na,t,rebuild_return_type t')
+    | _ -> Constrexpr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous],
+				       Constrexpr.Default Decl_kinds.Explicit,rt],
+			    Constrexpr.CSort(dummy_loc,GType None))
 
 
 let do_build_inductive
@@ -1302,10 +1302,10 @@ let do_build_inductive
 	(fun (n,t,is_defined) acc ->
 	   if is_defined
 	   then
-	     Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t,
+	     Constrexpr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t,
 			      acc)
 	   else
-	     Topconstr.CProdN
+	     Constrexpr.CProdN
 	       (dummy_loc,
 		[[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
 		acc
@@ -1368,10 +1368,10 @@ let do_build_inductive
       (fun (n,t,is_defined) acc ->
 	 if is_defined
 	 then
-	   Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t,
+	   Constrexpr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t,
 			    acc)
 	 else
-	   Topconstr.CProdN
+	   Constrexpr.CProdN
 	   (dummy_loc,
 	   [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
 	    acc
@@ -1390,9 +1390,9 @@ let do_build_inductive
       (fun (n,t,is_defined) ->
 	 if is_defined
 	 then
-	   Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t)
+	   Constrexpr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t)
 	 else
-	 Topconstr.LocalRawAssum
+	 Constrexpr.LocalRawAssum
 	   ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t)
       )
       rels_params
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 5c91292ba..b8e7b3ab4 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -10,7 +10,7 @@
 val build_inductive :
   Names.identifier list -> (* The list of function name *)
   (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
-  Topconstr.constr_expr list -> (* The list of function returned type *)
+  Constrexpr.constr_expr list -> (* The list of function returned type *)
   Glob_term.glob_constr list -> (* the list of body *)
   unit
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 1c2509f6e..2eb2fb3ed 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -130,8 +130,8 @@ let functional_induction with_clean c princl pat =
 
 let rec abstract_glob_constr c = function
   | [] -> c
-  | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_glob_constr c bl)
-  | Topconstr.LocalRawAssum (idl,k,t)::bl ->
+  | Constrexpr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_glob_constr c bl)
+  | Constrexpr.LocalRawAssum (idl,k,t)::bl ->
       List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl
         (abstract_glob_constr c bl)
 
@@ -220,8 +220,8 @@ let rec is_rec names =
 let rec local_binders_length = function
   (* Assume that no `{ ... } contexts occur *)
   | [] -> 0
-  | Topconstr.LocalRawDef _::bl -> 1 + local_binders_length bl
-  | Topconstr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
+  | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl
+  | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
 
 let prepare_body ((name,_,args,types,_),_) rt =
   let n = local_binders_length args in
@@ -395,7 +395,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   in
   let unbounded_eq =
     let f_app_args =
-      Topconstr.CAppExpl
+      Constrexpr.CAppExpl
 	(dummy_loc,
 	 (None,(Ident (dummy_loc,fname))) ,
 	 (List.map
@@ -407,7 +407,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 )
 	)
     in
-    Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
+    Constrexpr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Topconstr.prod_constr_expr unbounded_eq args in
@@ -439,7 +439,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  begin
 	    match args with
-	      | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x
+	      | [Constrexpr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x
 	      | _ -> error "Recursive argument must be specified"
 	  end
       | Some wf_args ->
@@ -447,7 +447,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	    match
 	      List.find
 		(function
-		   | Topconstr.LocalRawAssum(l,k,t) ->
+		   | Constrexpr.LocalRawAssum(l,k,t) ->
 		       List.exists
 			 (function (_,Name id) -> id =  wf_args | _ -> false)
 			 l
@@ -455,7 +455,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 		)
 		args
 	    with
-	      | Topconstr.LocalRawAssum(_,k,t)  ->	    t,wf_args
+	      | Constrexpr.LocalRawAssum(_,k,t)  ->	    t,wf_args
 	      | _ -> assert false
 	  with Not_found -> assert false
   in
@@ -482,7 +482,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	    let b = Names.id_of_string "___b" in 
 	    Topconstr.mkLambdaC(
 	      [dummy_loc,Name a;dummy_loc,Name b],
-	      Topconstr.Default Explicit,
+	      Constrexpr.Default Explicit,
 	      wf_arg_type,
 	      Topconstr.mkAppC(wf_rel_expr,
 			       [
@@ -505,23 +505,23 @@ let decompose_lambda_n_assum_constr_expr =
   if n = 0 then (List.rev acc,e)
   else
     match e with 
-      | Topconstr.CLambdaN(_, [],e') -> decompose_lambda_n_assum_constr_expr acc n e'
-      | Topconstr.CLambdaN(lambda_loc,(nal,bk,nal_type)::bl,e') ->
+      | Constrexpr.CLambdaN(_, [],e') -> decompose_lambda_n_assum_constr_expr acc n e'
+      | Constrexpr.CLambdaN(lambda_loc,(nal,bk,nal_type)::bl,e') ->
 	let nal_length = List.length nal in 
 	if nal_length <= n 
 	then
 	  decompose_lambda_n_assum_constr_expr 
-	    (Topconstr.LocalRawAssum(nal,bk,nal_type)::acc) 
+	    (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc)
 	    (n - nal_length) 
-	    (Topconstr.CLambdaN(lambda_loc,bl,e')) 
+	    (Constrexpr.CLambdaN(lambda_loc,bl,e'))
   	else
 	  let nal_keep,nal_expr = list_chop n nal in 
-	  (List.rev (Topconstr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
-	   Topconstr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
+	  (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
+	   Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
 	  )
-      | Topconstr.CLetIn(_, na,nav,e') -> 
+      | Constrexpr.CLetIn(_, na,nav,e') ->
 	decompose_lambda_n_assum_constr_expr 
-	  (Topconstr.LocalRawDef(na,nav)::acc) (pred n) e'
+	  (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e'
       | _ -> error "Not enough product or assumption"
   in
   decompose_lambda_n_assum_constr_expr []
@@ -535,29 +535,30 @@ let decompose_prod_n_assum_constr_expr =
       (List.rev acc,e)
   else
     match e with 
-      | Topconstr.CProdN(_, [],e') -> decompose_prod_n_assum_constr_expr acc n e'
-      | Topconstr.CProdN(lambda_loc,(nal,bk,nal_type)::bl,e') ->
+      | Constrexpr.CProdN(_, [],e') -> decompose_prod_n_assum_constr_expr acc n e'
+      | Constrexpr.CProdN(lambda_loc,(nal,bk,nal_type)::bl,e') ->
 	let nal_length = List.length nal in 
 	if nal_length <= n 
 	then
 	  (* let _ = Pp.msgnl (str "first case") in  *)
 	  decompose_prod_n_assum_constr_expr 
-	    (Topconstr.LocalRawAssum(nal,bk,nal_type)::acc) 
+	    (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc)
 	    (n - nal_length) 
-	    (if bl = [] then e' else (Topconstr.CLambdaN(lambda_loc,bl,e')))
+	    (if bl = [] then e' else (Constrexpr.CLambdaN(lambda_loc,bl,e')))
   	else
 	  (* let _ = Pp.msgnl (str "second case") in  *)
 	  let nal_keep,nal_expr = list_chop n nal in 
-	  (List.rev (Topconstr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
-	   Topconstr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
+	  (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
+	   Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
 	  )
-      | Topconstr.CLetIn(_, na,nav,e') -> 
+      | Constrexpr.CLetIn(_, na,nav,e') ->
 	decompose_prod_n_assum_constr_expr 
-	  (Topconstr.LocalRawDef(na,nav)::acc) (pred n) e'
+	  (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e'
       | _ -> error "Not enough product or assumption"
   in
   decompose_prod_n_assum_constr_expr []
 
+open Constrexpr
 open Topconstr
 
 let rec make_assoc = List.fold_left2 (fun l a b ->
@@ -569,10 +570,10 @@ match a, b with
 let rec rebuild_bl (aux,assoc) bl typ = 
 	match bl,typ with 
 	  | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
-	  | (Topconstr.LocalRawAssum(nal,bk,_))::bl',typ -> 
+	  | (Constrexpr.LocalRawAssum(nal,bk,_))::bl',typ ->
 	     rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ
-	  | (Topconstr.LocalRawDef(na,_))::bl',CLetIn(_,_,nat,typ') ->
-	    rebuild_bl ((Topconstr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc)
+	  | (Constrexpr.LocalRawDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') ->
+	    rebuild_bl ((Constrexpr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc)
 	      bl' typ'
 	  | _ -> assert false
       and rebuild_nal (aux,assoc) bk bl' nal lnal typ = 
@@ -619,7 +620,7 @@ let do_generate_principle on_error register_built interactive_proof
   List.iter (fun (_,l) -> if l <> [] then error "Function does not support notations for now") fixpoint_exprl;
   let _is_struct =
     match fixpoint_exprl with
-      | [((_,(wf_x,Topconstr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
+      | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
  	  let ((((_,name),_,args,types,body)),_)  as fixpoint_expr =
 	    match recompute_binder_list [fixpoint_expr] with 
 	      | [e] -> e
@@ -641,7 +642,7 @@ let do_generate_principle on_error register_built interactive_proof
 	  if register_built
 	  then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook;
 	  false
-      |[((_,(wf_x,Topconstr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
+      |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
  	  let ((((_,name),_,args,types,body)),_)  as fixpoint_expr =
 	    match recompute_binder_list [fixpoint_expr] with 
 	      | [e] -> e
@@ -666,7 +667,7 @@ let do_generate_principle on_error register_built interactive_proof
       | _ ->
 	  List.iter (function ((_na,(_,ord),_args,_body,_type),_not) ->
 		       match ord with 
-			 | Topconstr.CMeasureRec _ | Topconstr.CWfRec _ -> 
+			 | Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _ ->
 			     error
 			       ("Cannot use mutual definition with well-founded recursion or measure")
 			 | _ -> ()
@@ -757,18 +758,18 @@ let rec add_args id new_args b =
   | CGeneralization _ -> anomaly "add_args : CGeneralization"
   | CPrim _ -> b
   | CDelimiters _ -> anomaly "add_args : CDelimiters"
-exception Stop of  Topconstr.constr_expr
+exception Stop of  Constrexpr.constr_expr
 
 
 (* [chop_n_arrow n t] chops the [n] first arrows in [t]
-   Acts on Topconstr.constr_expr
+   Acts on Constrexpr.constr_expr
 *)
 let rec chop_n_arrow n t =
   if n <= 0
   then t (* If we have already removed all the arrows then return the type *)
   else (* If not we check the form of [t] *)
     match t with
-      | Topconstr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible :
+      | Constrexpr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible :
 					     either we need to discard more than the number of arrows contained
 					     in this product declaration then we just recall [chop_n_arrow] on
 					     the remaining number of arrow to chop and [t'] we discard it and
@@ -787,7 +788,7 @@ let rec chop_n_arrow n t =
 		      aux (n - nal_l) nal_ta'
 		    else
 		      let new_t' =
-			Topconstr.CProdN(dummy_loc,
+			Constrexpr.CProdN(dummy_loc,
 					((snd (list_chop n nal)),k,t'')::nal_ta',t')
 		      in
 		      raise (Stop new_t')
@@ -800,10 +801,10 @@ let rec chop_n_arrow n t =
       | _ -> anomaly "Not enough products"
 
 
-let rec get_args b t : Topconstr.local_binder list *
-    Topconstr.constr_expr * Topconstr.constr_expr =
+let rec get_args b t : Constrexpr.local_binder list *
+    Constrexpr.constr_expr * Constrexpr.constr_expr =
   match b with
-    | Topconstr.CLambdaN (loc, (nal_ta), b') ->
+    | Constrexpr.CLambdaN (loc, (nal_ta), b') ->
 	begin
 	  let n =
 	    (List.fold_left (fun n (nal,_,_) ->
@@ -811,7 +812,7 @@ let rec get_args b t : Topconstr.local_binder list *
 	  in
 	  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
 	  (List.map (fun (nal,k,ta) ->
-		       (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
+		       (Constrexpr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
 	end
     | _ -> [],b,t
 
@@ -845,7 +846,7 @@ let make_graph (f_ref:global_reference) =
 	 let (nal_tas,b,t)  = get_args extern_body extern_type in
 	 let expr_list =
 	   match b with
-	     | Topconstr.CFix(loc,l_id,fixexprl) ->
+	     | Constrexpr.CFix(loc,l_id,fixexprl) ->
 		 let l =
 		   List.map
 		     (fun (id,(n,recexp),bl,t,b) ->
@@ -854,8 +855,8 @@ let make_graph (f_ref:global_reference) =
 			  List.flatten
 			    (List.map
 			       (function
- 				  | Topconstr.LocalRawDef (na,_)-> []
-			      	  | Topconstr.LocalRawAssum (nal,_,_) ->
+				  | Constrexpr.LocalRawDef (na,_)-> []
+				  | Constrexpr.LocalRawAssum (nal,_,_) ->
 				      List.map
 					(fun (loc,n) ->
 					   CRef(Libnames.Ident(loc, Nameops.out_name n)))
@@ -872,7 +873,7 @@ let make_graph (f_ref:global_reference) =
 		 l
 	     | _ ->
 		 let id = id_of_label (con_label c) in
-		 [((dummy_loc,id),(None,Topconstr.CStructRec),nal_tas,t,Some b),[]]
+		 [((dummy_loc,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
 	 do_generate_principle error_error false false expr_list;
 	 (* We register the infos *)
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 0ec5f7bce..4ca23a295 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -13,7 +13,7 @@ open Tactics
 open Indfun_common
 open Errors
 open Util
-open Topconstr
+open Constrexpr
 open Vernacexpr
 open Pp
 open Names
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index aa4493821..1117e2597 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -10,11 +10,11 @@ val recursive_definition :
 bool ->
            Names.identifier ->
            Constrintern.internalization_env ->
-           Topconstr.constr_expr ->
-           Topconstr.constr_expr ->
-           int -> Topconstr.constr_expr -> (Names.constant ->
+           Constrexpr.constr_expr ->
+           Constrexpr.constr_expr ->
+           int -> Constrexpr.constr_expr -> (Names.constant ->
             Term.constr option ref ->
             Names.constant ->
-            Names.constant -> int -> Term.types -> int -> Term.constr -> 'a) -> Topconstr.constr_expr list -> unit
+            Names.constant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit