diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 549 |
1 files changed, 335 insertions, 214 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a61671f8..8caeca57 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -4,7 +4,7 @@ open Term open Pp open Indfun_common open Libnames -open Rawterm +open Glob_term open Declarations let is_rec_info scheme_info = @@ -19,13 +19,11 @@ let is_rec_info scheme_info = in Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) - let choose_dest_or_ind scheme_info = if is_rec_info scheme_info then Tactics.new_induct false else Tactics.new_destruct false - let functional_induction with_clean c princl pat = Dumpglob.pause (); let res = let f,args = decompose_app c in @@ -65,9 +63,8 @@ let functional_induction with_clean c princl pat = errorlabstrm "" (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in - (princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ) + (princ,Glob_term.NoBindings, Tacmach.pf_type_of g princ) | _ -> raise (UserError("",str "functional induction must be used with a function" )) - end | Some ((princ,binding)) -> princ,binding,Tacmach.pf_type_of g princ @@ -78,7 +75,7 @@ let functional_induction with_clean c princl pat = if princ_infos.Tactics.farg_in_concl then [c] else [] in - List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list) + List.map (fun c -> Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list) in let princ' = Some (princ,bindings) in let princ_vars = @@ -104,9 +101,9 @@ let functional_induction with_clean c princl pat = (Tacmach.pf_ids_of_hyps g) in let flag = - Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; } in Tacticals.tclTHEN @@ -114,7 +111,6 @@ let functional_induction with_clean c princl pat = (Hiddentac.h_reduce flag Tacticals.allHypsAndConcl) g else Tacticals.tclIDTAC g - in Tacticals.tclTHEN (choose_dest_or_ind @@ -129,56 +125,43 @@ let functional_induction with_clean c princl pat = Dumpglob.continue (); res - - - -type annot = - Struct of identifier - | Wf of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list - | Mes of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list - - -type newfixpoint_expr = - identifier * annot * Topconstr.local_binder list * Topconstr.constr_expr * Topconstr.constr_expr - -let rec abstract_rawconstr c = function +let rec abstract_glob_constr c = function | [] -> c - | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl) + | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_glob_constr c bl) | Topconstr.LocalRawAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl - (abstract_rawconstr c bl) + (abstract_glob_constr c bl) let interp_casted_constr_with_implicits sigma env impls c = -(* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *) Constrintern.intern_gen false sigma env ~impls ~allow_patvar:false ~ltacvars:([],[]) c - (* - Construct a fixpoint as a Rawterm + Construct a fixpoint as a Glob_term and not as a constr *) + let build_newrecursive -(lnameargsardef) = + lnameargsardef = let env0 = Global.env() and sigma = Evd.empty in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) ((_,recname),_,bl,arityc,_) -> + (fun (env,impls) ((_,recname),bl,arityc,_) -> let arityc = Topconstr.prod_constr_expr arityc bl in let arity = Constrintern.interp_type sigma env0 arityc in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in - (Environ.push_named (recname,None,arity) env, (recname, impl) :: impls)) - (env0,[]) lnameargsardef in + (Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls)) + (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) let fs = States.freeze() in let def = try List.map - (fun (_,_,bl,_,def) -> - let def = abstract_rawconstr def bl in + (fun (_,bl,_,def) -> + let def = abstract_glob_constr def bl in interp_casted_constr_with_implicits sigma rec_sign rec_impls def ) @@ -189,34 +172,31 @@ let build_newrecursive in recdef,rec_impls - -let compute_annot (name,annot,args,types,body) = - let names = List.map snd (Topconstr.names_of_local_assums args) in - match annot with - | None -> - if List.length names > 1 then - user_err_loc - (dummy_loc,"Function", - Pp.str "the recursive argument needs to be specified"); - let new_annot = (id_of_name (List.hd names)) in - (name,Struct new_annot,args,types,body) - | Some r -> (name,r,args,types,body) - +let build_newrecursive l = + let l' = List.map + (fun ((fixna,_,bll,ar,body_opt),lnot) -> + match body_opt with + | Some body -> + (fixna,bll,ar,body) + | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") + ) l + in + build_newrecursive l' (* Checks whether or not the mutual bloc is recursive *) let rec is_rec names = let names = List.fold_right Idset.add names Idset.empty in let check_id id names = Idset.mem id names in let rec lookup names = function - | RVar(_,id) -> check_id id names - | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false - | RCast(_,b,_) -> lookup names b - | RRec _ -> error "RRec not handled" - | RIf(_,b,_,lhs,rhs) -> + | GVar(_,id) -> check_id id names + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false + | GCast(_,b,_) -> lookup names b + | GRec _ -> error "GRec not handled" + | GIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) -> + | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Idset.remove na names) b - | RLetTuple(_,nal,_,t,b) -> lookup names t || + | GLetTuple(_,nal,_,t,b) -> lookup names t || lookup (List.fold_left (fun acc na -> Nameops.name_fold Idset.remove na acc) @@ -224,8 +204,8 @@ let rec is_rec names = nal ) b - | RApp(_,f,args) -> List.exists (lookup names) (f::args) - | RCases(_,_,_,el,brl) -> + | GApp(_,f,args) -> List.exists (lookup names) (f::args) + | GCases(_,_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl and lookup_br names (_,idl,_,rt) = @@ -240,9 +220,9 @@ let rec local_binders_length = function | Topconstr.LocalRawDef _::bl -> 1 + local_binders_length bl | Topconstr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl -let prepare_body (name,annot,args,types,body) rt = +let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in -(* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *) +(* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_glob_constr rt); *) let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') @@ -251,7 +231,7 @@ let derive_inversion fix_names = try (* we first transform the fix_names identifier into their corresponding constant *) let fix_names_as_constant = - List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names + List.map (fun id -> destConst (Constrintern.global_reference id)) fix_names in (* Then we check that the graphs have been defined @@ -268,20 +248,22 @@ let derive_inversion fix_names = Ensures by : register_built i*) (List.map - (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id))) + (fun id -> destInd (Constrintern.global_reference (mk_rel_id id))) fix_names ) with e -> + let e' = Cerrors.process_vernac_interp_error e in msg_warning - (str "Cannot built inversion information" ++ - if do_observe () then Cerrors.explain_exn e else mt ()) + (str "Cannot build inversion information" ++ + if do_observe () then (fnl() ++ Errors.print e') else mt ()) with _ -> () let warning_error names e = + let e = Cerrors.process_vernac_interp_error e in let e_explain e = match e with - | ToShow e -> spc () ++ Cerrors.explain_exn e - | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt () + | ToShow e -> spc () ++ Errors.print e + | _ -> if do_observe () then (spc () ++ Errors.print e) else mt () in match e with | Building_graph e -> @@ -297,10 +279,11 @@ let warning_error names e = | _ -> raise e let error_error names e = + let e = Cerrors.process_vernac_interp_error e in let e_explain e = match e with - | ToShow e -> spc () ++ Cerrors.explain_exn e - | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt () + | ToShow e -> spc () ++ Errors.print e + | _ -> if do_observe () then (spc () ++ Errors.print e) else mt () in match e with | Building_graph e -> @@ -311,16 +294,16 @@ let error_error names e = | _ -> raise e let generate_principle on_error - is_general do_built fix_rec_l recdefs interactive_proof + is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function ((_, name),_,_,_,_) -> name) fix_rec_l in + let names = List.map (function ((_, name),_,_,_,_),_ -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in - let funs_types = List.map (function (_,_,_,types,_) -> types) fix_rec_l in + let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in try (* We then register the Inductive graphs of the functions *) - Rawterm_to_relation.build_inductive names funs_args funs_types recdefs; + Glob_term_to_relation.build_inductive names funs_args funs_types recdefs; if do_built then begin @@ -334,7 +317,7 @@ let generate_principle on_error locate_ind f_R_mut) in - let fname_kn (fname,_,_,_,_) = + let fname_kn ((fname,_,_,_,_),_) = let f_ref = Ident fname in locate_with_msg (pr_reference f_ref++str ": Not an inductive type!") @@ -366,21 +349,18 @@ let generate_principle on_error with e -> on_error names e -let register_struct is_rec fixpoint_exprl = +let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> + let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in let ce,imps = - Command.interp_definition - (Flags.boxed_definitions ()) bl None body (Some ret_type) + Command.interp_definition bl None body (Some ret_type) in Command.declare_definition fname (Decl_kinds.Global,Decl_kinds.Definition) ce imps (fun _ _ -> ()) | _ -> - let fixpoint_exprl = - List.map (fun ((name,annot,bl,types,body),ntn) -> - ((name,annot,bl,types,Some body),ntn)) fixpoint_exprl in - Command.do_fixpoint fixpoint_exprl (Flags.boxed_definitions()) + Command.do_fixpoint fixpoint_exprl let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation @@ -402,8 +382,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas in match wf_arg with | None -> - if List.length names = 1 then 1 - else error "Recursive argument must be specified" + if List.length names = 1 then 1 + else error "Recursive argument must be specified" | Some wf_arg -> list_index (Name wf_arg) names in @@ -447,7 +427,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas using_lemmas -let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type body = +let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body = let wf_arg_type,wf_arg = match wf_arg with | None -> @@ -473,28 +453,186 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b | _ -> assert false with Not_found -> assert false in - let ltof = - let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in - Libnames.Qualid (dummy_loc,Libnames.qualid_of_path - (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof"))) - in - let fun_from_mes = - let applied_mes = - Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in - Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) - in - let wf_rel_from_mes = - Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes]) - in - register_wf ~is_mes:true fname rec_impls wf_rel_from_mes (Some wf_arg) + let wf_rel_from_mes,is_mes = + match wf_rel_expr_opt with + | None -> + let ltof = + let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in + Libnames.Qualid (dummy_loc,Libnames.qualid_of_path + (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof"))) + in + let fun_from_mes = + let applied_mes = + Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in + Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) + in + let wf_rel_from_mes = + Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes]) + in + wf_rel_from_mes,true + | Some wf_rel_expr -> + let wf_rel_with_mes = + let a = Names.id_of_string "___a" in + let b = Names.id_of_string "___b" in + Topconstr.mkLambdaC( + [dummy_loc,Name a;dummy_loc,Name b], + Topconstr.Default Lib.Explicit, + wf_arg_type, + Topconstr.mkAppC(wf_rel_expr, + [ + Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC a]); + Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC b]) + ]) + ) + in + wf_rel_with_mes,false + in + register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes (Some wf_arg) using_lemmas args ret_type body +let map_option f = function + | None -> None + | Some v -> Some (f v) + +let decompose_lambda_n_assum_constr_expr = + let rec decompose_lambda_n_assum_constr_expr acc n e = + 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') -> + 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) + (n - nal_length) + (Topconstr.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') + ) + | Topconstr.CLetIn(_, na,nav,e') -> + decompose_lambda_n_assum_constr_expr + (Topconstr.LocalRawDef(na,nav)::acc) (pred n) e' + | _ -> error "Not enough product or assumption" + in + decompose_lambda_n_assum_constr_expr [] + +let decompose_prod_n_assum_constr_expr = + let rec decompose_prod_n_assum_constr_expr acc n e = + (* Pp.msgnl (str "n := " ++ int n ++ fnl ()++ *) + (* str "e := " ++ Ppconstr.pr_lconstr_expr e); *) + if n = 0 then + (* let _ = Pp.msgnl (str "return_type := " ++ Ppconstr.pr_lconstr_expr e) in *) + (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') -> + 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) + (n - nal_length) + (if bl = [] then e' else (Topconstr.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') + ) + | Topconstr.CArrow(_,premisse,concl) -> + (* let _ = Pp.msgnl (str "arrow case") in *) + decompose_prod_n_assum_constr_expr + (Topconstr.LocalRawAssum([dummy_loc,Names.Anonymous], + Topconstr.Default Lib.Explicit,premisse) + ::acc) + (pred n) + concl + | Topconstr.CLetIn(_, na,nav,e') -> + decompose_prod_n_assum_constr_expr + (Topconstr.LocalRawDef(na,nav)::acc) (pred n) e' + | _ -> error "Not enough product or assumption" + in + decompose_prod_n_assum_constr_expr [] -let do_generate_principle on_error register_built interactive_proof fixpoint_exprl = - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in +open Topconstr + +let id_of_name = function + | Name id -> id + | _ -> assert false + + 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 -> + 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) + bl' typ' + | _ -> assert false + and rebuild_nal (aux,assoc) bk bl' nal lnal typ = + match nal,typ with + | [], _ -> rebuild_bl (aux,assoc) bl' typ + | na::nal,CArrow(_,nat,typ') -> + rebuild_nal + ((LocalRawAssum([na],bk,replace_vars_constr_expr assoc nat))::aux,assoc) + bk bl' nal (pred lnal) typ' + | _,CProdN(_,[],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ + | _,CProdN(_,(nal',bk',nal't)::rest,typ') -> + let lnal' = List.length nal' in + if lnal' >= lnal + then + let old_nal',new_nal' = list_chop lnal nal' in + rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(List.rev_append (List.combine (List.map id_of_name (List.map snd old_nal')) (List.map id_of_name (List.map snd nal))) assoc)) bl' + (if new_nal' = [] && rest = [] + then typ' + else if new_nal' = [] + then CProdN(dummy_loc,rest,typ') + else CProdN(dummy_loc,((new_nal',bk',nal't)::rest),typ')) + else + let captured_nal,non_captured_nal = list_chop lnal' nal in + rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (List.rev_append (List.combine (List.map id_of_name (List.map snd captured_nal)) ((List.map id_of_name (List.map snd nal)))) assoc)) + bk bl' non_captured_nal (lnal - lnal') (CProdN(dummy_loc,rest,typ')) + | _ -> assert false + +let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ + +let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = + let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in + let ((_,_,typel),_) = Command.interp_fixpoint fixl ntns in + let constr_expr_typel = + with_full_print (List.map (Constrextern.extern_constr false (Global.env ()))) typel in + let fixpoint_exprl_with_new_bl = + List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> + + let new_bl',new_ret_type,_ = rebuild_bl ([],[]) bl fix_typ in + (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + ) + fixpoint_exprl constr_expr_typel + in + fixpoint_exprl_with_new_bl + + +let do_generate_principle on_error register_built interactive_proof + (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) :unit = + List.iter (fun (_,l) -> if l <> [] then error "Function does not support notations for now") fixpoint_exprl; let _is_struct = match fixpoint_exprl with - | [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> + | [((_,(wf_x,Topconstr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> + let ((((_,name),_,args,types,body)),_) as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in let pre_hook = generate_principle on_error @@ -505,9 +643,18 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp true in if register_built - then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook; + then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook; false - | [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> + |[((_,(wf_x,Topconstr.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 + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in let pre_hook = generate_principle on_error @@ -518,56 +665,35 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp true in if register_built - then register_mes name rec_impls wf_mes wf_x using_lemmas args types body pre_hook; + then register_mes name rec_impls wf_mes wf_rel_opt (map_option snd wf_x) using_lemmas args types body pre_hook; true | _ -> - let fix_names = - List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl - in - let is_one_rec = is_rec fix_names in - let old_fixpoint_exprl = - List.map - (function - | (name,Some (Struct id),args,types,body),_ -> - let annot = - try Some (dummy_loc, id), Topconstr.CStructRec - with Not_found -> - raise (UserError("",str "Cannot find argument " ++ - Ppconstr.pr_id id)) - in - (name,annot,args,types,body),([]:Vernacexpr.decl_notation list) - | (name,None,args,types,body),recdef -> - let names = (Topconstr.names_of_local_assums args) in - if is_one_rec recdef && List.length names > 1 then - user_err_loc - (dummy_loc,"Function", - Pp.str "the recursive argument needs to be specified in Function") - else - let loc, na = List.hd names in - (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body), - ([]:Vernacexpr.decl_notation list) - | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> - error - ("Cannot use mutual definition with well-founded recursion or measure") - ) - (List.combine fixpoint_exprl recdefs) - in + List.iter (function ((_na,(_,ord),_args,_body,_type),_not) -> + match ord with + | Topconstr.CMeasureRec _ | Topconstr.CWfRec _ -> + error + ("Cannot use mutual definition with well-founded recursion or measure") + | _ -> () + ) + fixpoint_exprl; + let fixpoint_exprl = recompute_binder_list fixpoint_exprl in + let fix_names = + List.map (function (((_,name),_,_,_,_),_) -> name) fixpoint_exprl + in (* ok all the expressions are structural *) - let fix_names = - List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl - in - let is_rec = List.exists (is_rec fix_names) recdefs in - if register_built then register_struct is_rec old_fixpoint_exprl; - generate_principle - on_error - false - register_built - fixpoint_exprl - recdefs - interactive_proof - (Functional_principles_proofs.prove_princ_for_struct interactive_proof); - if register_built then derive_inversion fix_names; - true; + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let is_rec = List.exists (is_rec fix_names) recdefs in + if register_built then register_struct is_rec fixpoint_exprl; + generate_principle + on_error + false + register_built + fixpoint_exprl + recdefs + interactive_proof + (Functional_principles_proofs.prove_princ_for_struct interactive_proof); + if register_built then derive_inversion fix_names; + true; in () @@ -638,7 +764,6 @@ let rec add_args id new_args b = | CGeneralization _ -> anomaly "add_args : CGeneralization" | CPrim _ -> b | CDelimiters _ -> anomaly "add_args : CDelimiters" - | CDynamic _ -> anomaly "add_args : CDynamic" exception Stop of Topconstr.constr_expr @@ -701,75 +826,71 @@ let rec get_args b t : Topconstr.local_binder list * let make_graph (f_ref:global_reference) = - let c,c_body = - match f_ref with - | ConstRef c -> - begin try c,Global.lookup_constant c - with Not_found -> - raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) - end - | _ -> raise (UserError ("", str "Not a function reference") ) - + let c,c_body = + match f_ref with + | ConstRef c -> + begin try c,Global.lookup_constant c + with Not_found -> + raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) + end + | _ -> raise (UserError ("", str "Not a function reference") ) in - Dumpglob.pause (); - (match c_body.const_body with - | None -> error "Cannot build a graph over an axiom !" - | Some b -> - let env = Global.env () in - let body = (force b) in - let extern_body,extern_type = - with_full_print - (fun () -> - (Constrextern.extern_constr false env body, - Constrextern.extern_type false env - (Typeops.type_of_constant_type env c_body.const_type) - ) - ) - () - in - let (nal_tas,b,t) = get_args extern_body extern_type in - let expr_list = - match b with - | Topconstr.CFix(loc,l_id,fixexprl) -> - let l = - List.map - (fun (id,(n,recexp),bl,t,b) -> - let loc, rec_id = Option.get n in - let new_args = - List.flatten - (List.map - (function - | Topconstr.LocalRawDef (na,_)-> [] - | Topconstr.LocalRawAssum (nal,_,_) -> - List.map - (fun (loc,n) -> - CRef(Libnames.Ident(loc, Nameops.out_name n))) - nal - ) - nal_tas - ) - in - let b' = add_args (snd id) new_args b in - (id, Some (Struct rec_id),nal_tas@bl,t,b') - ) - fixexprl - in - l - | _ -> - let id = id_of_label (con_label c) in - [((dummy_loc,id),None,nal_tas,t,b)] - in - do_generate_principle error_error false false expr_list; - (* We register the infos *) - let mp,dp,_ = repr_con c in - List.iter - (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) - expr_list); + Dumpglob.pause (); + (match body_of_constant c_body with + | None -> error "Cannot build a graph over an axiom !" + | Some b -> + let env = Global.env () in + let body = (force b) in + let extern_body,extern_type = + with_full_print + (fun () -> + (Constrextern.extern_constr false env body, + Constrextern.extern_type false env + (Typeops.type_of_constant_type env c_body.const_type) + ) + ) + () + in + let (nal_tas,b,t) = get_args extern_body extern_type in + let expr_list = + match b with + | Topconstr.CFix(loc,l_id,fixexprl) -> + let l = + List.map + (fun (id,(n,recexp),bl,t,b) -> + let loc, rec_id = Option.get n in + let new_args = + List.flatten + (List.map + (function + | Topconstr.LocalRawDef (na,_)-> [] + | Topconstr.LocalRawAssum (nal,_,_) -> + List.map + (fun (loc,n) -> + CRef(Libnames.Ident(loc, Nameops.out_name n))) + nal + ) + nal_tas + ) + in + let b' = add_args (snd id) new_args b in + (((id, ( Some (dummy_loc,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + ) + fixexprl + in + l + | _ -> + let id = id_of_label (con_label c) in + [((dummy_loc,id),(None,Topconstr.CStructRec),nal_tas,t,Some b),[]] + in + do_generate_principle error_error false false expr_list; + (* We register the infos *) + let mp,dp,_ = repr_con c in + List.iter + (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (label_of_id id))) + expr_list); Dumpglob.continue () - -(* let make_graph _ = assert false *) - let do_generate_principle = do_generate_principle warning_error true |