From 392300a73bc4e57d2be865d9a8d77c608ef02f59 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:08:50 +0000 Subject: 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 --- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 26 +++++----- plugins/funind/glob_term_to_relation.mli | 2 +- plugins/funind/indfun.ml | 89 ++++++++++++++++---------------- plugins/funind/merge.ml | 2 +- plugins/funind/recdef.mli | 8 +-- 6 files changed, 65 insertions(+), 64 deletions(-) (limited to 'plugins/funind') 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 -- cgit v1.2.3