diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 912 |
1 files changed, 912 insertions, 0 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml new file mode 100644 index 0000000000..6494e90a03 --- /dev/null +++ b/plugins/funind/indfun.ml @@ -0,0 +1,912 @@ +open CErrors +open Sorts +open Util +open Names +open Constr +open Context +open EConstr +open Pp +open Indfun_common +open Libnames +open Globnames +open Glob_term +open Declarations +open Tactypes +open Decl_kinds + +module RelDecl = Context.Rel.Declaration + +let is_rec_info sigma scheme_info = + let test_branche min acc decl = + acc || ( + let new_branche = + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (RelDecl.get_type decl))) in + let free_rels_in_br = Termops.free_rels sigma new_branche in + let max = min + scheme_info.Tactics.npredicates in + Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br + ) + in + List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) + +let choose_dest_or_ind scheme_info args = + Proofview.tclBIND Proofview.tclEVARMAP (fun sigma -> + Tactics.induction_destruct (is_rec_info sigma scheme_info) false args) + +let functional_induction with_clean c princl pat = + let res = + fun g -> + let sigma = Tacmach.project g in + let f,args = decompose_app sigma c in + let princ,bindings, princ_type,g' = + match princl with + | None -> (* No principle is given let's find the good one *) + begin + match EConstr.kind sigma f with + | Const (c',u) -> + let princ_option = + let finfo = (* we first try to find out a graph on f *) + try find_Function_infos c' + with Not_found -> + user_err (str "Cannot find induction information on "++ + Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) + in + match Tacticals.elimination_sort_of_goal g with + | InSProp -> finfo.sprop_lemma + | InProp -> finfo.prop_lemma + | InSet -> finfo.rec_lemma + | InType -> finfo.rect_lemma + in + let princ,g' = (* then we get the principle *) + try + let g',princ = + Tacmach.pf_eapply (Evd.fresh_global) g (Globnames.ConstRef (Option.get princ_option )) in + princ,g' + with Option.IsNone -> + (*i If there is not default lemma defined then, + we cross our finger and try to find a lemma named f_ind + (or f_rec, f_rect) i*) + let princ_name = + Indrec.make_elimination_ident + (Label.to_id (Constant.label c')) + (Tacticals.elimination_sort_of_goal g) + in + try + let princ_ref = const_of_id princ_name in + let (a,b) = Tacmach.pf_eapply (Evd.fresh_global) g princ_ref in + (b,a) + (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) + with Not_found -> (* This one is neither defined ! *) + user_err (str "Cannot find induction principle for " + ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) + in + (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') + | _ -> raise (UserError(None,str "functional induction must be used with a function" )) + end + | Some ((princ,binding)) -> + princ,binding,Tacmach.pf_unsafe_type_of g princ,g + in + let sigma = Tacmach.project g' in + let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in + let args_as_induction_constr = + let c_list = + if princ_infos.Tactics.farg_in_concl + then [c] else [] + in + if List.length args + List.length c_list = 0 + then user_err Pp.(str "Cannot recognize a valid functional scheme" ); + let encoded_pat_as_patlist = + List.make (List.length args + List.length c_list - 1) None @ [pat] + in + List.map2 + (fun c pat -> + ((None, + Tactics.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))), + (None,pat), + None)) + (args@c_list) + encoded_pat_as_patlist + in + let princ' = Some (princ,bindings) in + let princ_vars = + List.fold_right + (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc) + args + Id.Set.empty + in + let old_idl = List.fold_right Id.Set.add (Tacmach.pf_ids_of_hyps g) Id.Set.empty in + let old_idl = Id.Set.diff old_idl princ_vars in + let subst_and_reduce g = + if with_clean + then + let idl = + List.filter (fun id -> not (Id.Set.mem id old_idl)) + (Tacmach.pf_ids_of_hyps g) + in + let flag = + Genredexpr.Cbv + {Redops.all_flags + with Genredexpr.rDelta = false; + } + in + Tacticals.tclTHEN + (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl ) + (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl)) + g + else Tacticals.tclIDTAC g + in + Tacticals.tclTHEN + (Proofview.V82.of_tactic (choose_dest_or_ind + princ_infos + (args_as_induction_constr,princ'))) + subst_and_reduce + g' + in res + +let rec abstract_glob_constr c = function + | [] -> c + | Constrexpr.CLocalDef (x,b,t)::bl -> Constrexpr_ops.mkLetInC(x,b,t,abstract_glob_constr c bl) + | Constrexpr.CLocalAssum (idl,k,t)::bl -> + List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl + (abstract_glob_constr c bl) + | Constrexpr.CLocalPattern _::bl -> assert false + +let interp_casted_constr_with_implicits env sigma impls c = + Constrintern.intern_gen Pretyping.WithoutTypeConstraint env sigma ~impls c + +(* + Construct a fixpoint as a Glob_term + and not as a constr +*) + +let build_newrecursive + lnameargsardef = + let env0 = Global.env() in + let sigma = Evd.from_env env0 in + let (rec_sign,rec_impls) = + List.fold_left + (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) -> + let arityc = Constrexpr_ops.mkCProdN bl arityc in + let arity,ctx = Constrintern.interp_type env0 sigma arityc in + let evd = Evd.from_env env0 in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in + let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in + let open Context.Named.Declaration in + let r = Sorts.Relevant in (* TODO relevance *) + (EConstr.push_named (LocalAssum (make_annot recname r,arity)) env, Id.Map.add recname impl impls)) + (env0,Constrintern.empty_internalization_env) lnameargsardef in + let recdef = + (* Declare local notations *) + let f (_,bl,_,def) = + let def = abstract_glob_constr def bl in + interp_casted_constr_with_implicits + rec_sign sigma rec_impls def + in + States.with_state_protection (List.map f) lnameargsardef + in + recdef,rec_impls + +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 ~hdr:"Function" (str "Body of Function must be given") + ) l + in + build_newrecursive l' + +let error msg = user_err Pp.(str msg) + +(* Checks whether or not the mutual bloc is recursive *) +let is_rec names = + let names = List.fold_right Id.Set.add names Id.Set.empty in + let check_id id names = Id.Set.mem id names in + let rec lookup names gt = match DAst.get gt with + | GVar(id) -> check_id id names + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> false + | GCast(b,_) -> lookup names b + | GRec _ -> error "GRec not handled" + | GIf(b,_,lhs,rhs) -> + (lookup names b) || (lookup names lhs) || (lookup names rhs) + | GProd(na,_,t,b) | GLambda(na,_,t,b) -> + lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b + | GLetIn(na,b,t,c) -> + lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c + | GLetTuple(nal,_,t,b) -> lookup names t || + lookup + (List.fold_left + (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc) + names + nal + ) + b + | 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 {CAst.v=(idl,_,rt)} = + let new_names = List.fold_right Id.Set.remove idl names in + lookup new_names rt + in + lookup names + +let rec local_binders_length = function + (* Assume that no `{ ... } contexts occur *) + | [] -> 0 + | Constrexpr.CLocalDef _::bl -> 1 + local_binders_length bl + | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl + | Constrexpr.CLocalPattern _::bl -> assert false + +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_glob_constr rt); *) + let fun_args,rt' = chop_rlambda_n n rt in + (fun_args,rt') + +let process_vernac_interp_error e = + fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)) + +let warn_funind_cannot_build_inversion = + CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind" + (fun e' -> strbrk "Cannot build inversion information" ++ + if do_observe () then (fnl() ++ CErrors.print e') else mt ()) + +let derive_inversion fix_names = + try + let evd' = Evd.from_env (Global.env ()) in + (* we first transform the fix_names identifier into their corresponding constant *) + let evd',fix_names_as_constant = + List.fold_right + (fun id (evd,l) -> + let evd,c = + Evd.fresh_global + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in + let (cst, u) = destConst evd c in + evd, (cst, EInstance.kind evd u) :: l + ) + fix_names + (evd',[]) + in + (* + Then we check that the graphs have been defined + If one of the graphs haven't been defined + we do nothing + *) + List.iter (fun c -> ignore (find_Function_infos (fst c))) fix_names_as_constant ; + try + let evd', lind = + List.fold_right + (fun id (evd,l) -> + let evd,id = + Evd.fresh_global + (Global.env ()) evd + (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id))) + in + evd,(fst (destInd evd id))::l + ) + fix_names + (evd',[]) + in + Invfun.derive_correctness + Functional_principles_types.make_scheme + fix_names_as_constant + lind; + with e when CErrors.noncritical e -> + let e' = process_vernac_interp_error e in + warn_funind_cannot_build_inversion e' + with e when CErrors.noncritical e -> + let e' = process_vernac_interp_error e in + warn_funind_cannot_build_inversion e' + +let warn_cannot_define_graph = + CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind" + (fun (names,error) -> strbrk "Cannot define graph(s) for " ++ + h 1 names ++ error) + +let warn_cannot_define_principle = + CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind" + (fun (names,error) -> strbrk "Cannot define induction principle(s) for "++ + h 1 names ++ error) + +let warning_error names e = + let e = process_vernac_interp_error e in + let e_explain e = + match e with + | ToShow e -> + let e = process_vernac_interp_error e in + spc () ++ CErrors.print e + | _ -> + if do_observe () + then + let e = process_vernac_interp_error e in + (spc () ++ CErrors.print e) + else mt () + in + match e with + | Building_graph e -> + let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in + warn_cannot_define_graph (names,e_explain e) + | Defining_principle e -> + let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in + warn_cannot_define_principle (names,e_explain e) + | _ -> raise e + +let error_error names e = + let e = process_vernac_interp_error e in + let e_explain e = + match e with + | ToShow e -> spc () ++ CErrors.print e + | _ -> if do_observe () then (spc () ++ CErrors.print e) else mt () + in + match e with + | Building_graph e -> + user_err + (str "Cannot define graph(s) for " ++ + h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ + e_explain e) + | _ -> raise e + +let generate_principle (evd:Evd.evar_map ref) pconstants on_error + is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof + (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> + Tacmach.tactic) : unit = + let names = List.map (function (({CAst.v=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 + try + (* We then register the Inductive graphs of the functions *) + Glob_term_to_relation.build_inductive !evd pconstants funs_args funs_types recdefs; + if do_built + then + begin + (*i The next call to mk_rel_id is valid since we have just construct the graph + Ensures by : do_built + i*) + let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in + let ind_kn = + fst (locate_with_msg + (pr_qualid f_R_mut++str ": Not an inductive type!") + locate_ind + f_R_mut) + in + let fname_kn (((fname,_),_,_,_,_),_) = + let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in + locate_with_msg + (pr_qualid f_ref++str ": Not an inductive type!") + locate_constant + f_ref + in + let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in + let _ = + List.map_i + (fun i x -> + let env = Global.env () in + let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in + let evd = ref (Evd.from_env env) in + let evd',uprinc = Evd.fresh_global env !evd princ in + let _ = evd := evd' in + let sigma, princ_type = Typing.type_of ~refresh:true env !evd uprinc in + evd := sigma; + let princ_type = EConstr.Unsafe.to_constr princ_type in + Functional_principles_types.generate_functional_principle + evd + interactive_proof + princ_type + None + None + (Array.of_list pconstants) + (* funs_kn *) + i + (continue_proof 0 [|funs_kn.(i)|]) + ) + 0 + fix_rec_l + in + Array.iter (add_Function is_general) funs_kn; + () + end + with e when CErrors.noncritical e -> + on_error names e + +let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = + match fixpoint_exprl with + | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + ComDefinition.do_definition ~ontop:pstate + ~program_mode:false + fname + (Decl_kinds.Global,false,Decl_kinds.Definition) pl + bl None body (Some ret_type); + let evd,rev_pconstants = + List.fold_left + (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> + let evd,c = + Evd.fresh_global + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + let (cst, u) = destConst evd c in + let u = EInstance.kind evd u in + evd,((cst, u) :: l) + ) + (Evd.from_env (Global.env ()),[]) + fixpoint_exprl + in + pstate, evd,List.rev rev_pconstants + | _ -> + let pstate = ComFixpoint.do_fixpoint ~ontop:pstate Global false fixpoint_exprl in + let evd,rev_pconstants = + List.fold_left + (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> + let evd,c = + Evd.fresh_global + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + let (cst, u) = destConst evd c in + let u = EInstance.kind evd u in + evd,((cst, u) :: l) + ) + (Evd.from_env (Global.env ()),[]) + fixpoint_exprl + in + pstate,evd,List.rev rev_pconstants + + +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 + (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic = + Functional_principles_proofs.prove_principle_for_gen + (f_ref,functional_ref,eq_ref) + tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation + + +let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body + pre_hook + = + let type_of_f = Constrexpr_ops.mkCProdN args ret_type in + let rec_arg_num = + let names = + List.map + CAst.(with_val (fun x -> x)) + (Constrexpr_ops.names_of_local_assums args) + in + List.index Name.equal (Name wf_arg) names + in + let unbounded_eq = + let f_app_args = + CAst.make @@ Constrexpr.CAppExpl( + (None,qualid_of_ident fname,None) , + (List.map + (function + | {CAst.v=Anonymous} -> assert false + | {CAst.v=Name e} -> (Constrexpr_ops.mkIdentC e) + ) + (Constrexpr_ops.names_of_local_assums args) + ) + ) + in + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")), + [(f_app_args,None);(body,None)]) + in + let eq = Constrexpr_ops.mkCProdN args unbounded_eq in + let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type + nb_args relation = + try + pre_hook [fconst] + (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes + functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation + ); + derive_inversion [fname] + with e when CErrors.noncritical e -> + (* No proof done *) + () + in + Recdef.recursive_definition + is_mes fname rec_impls + type_of_f + wf_rel_expr + rec_arg_num + eq + hook + using_lemmas + + +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 -> + begin + match args with + | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x + | _ -> error "Recursive argument must be specified" + end + | Some wf_args -> + try + match + List.find + (function + | Constrexpr.CLocalAssum(l,k,t) -> + List.exists + (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false) + l + | _ -> false + ) + args + with + | Constrexpr.CLocalAssum(_,k,t) -> t,wf_args + | _ -> assert false + with Not_found -> assert false + in + let wf_rel_from_mes,is_mes = + match wf_rel_expr_opt with + | None -> + let ltof = + let make_dir l = DirPath.make (List.rev_map Id.of_string l) in + Libnames.qualid_of_path + (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")) + in + let fun_from_mes = + let applied_mes = + Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in + Constrexpr_ops.mkLambdaC ([CAst.make @@ Name wf_arg],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) + in + let wf_rel_from_mes = + Constrexpr_ops.mkAppC(Constrexpr_ops.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 + Constrexpr_ops.mkLambdaC( + [CAst.make @@ Name a; CAst.make @@ Name b], + Constrexpr.Default Explicit, + wf_arg_type, + Constrexpr_ops.mkAppC(wf_rel_expr, + [ + Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC a]); + Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC b]) + ]) + ) + in + wf_rel_with_mes,false + in + register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg + using_lemmas args ret_type body + +let map_option f = function + | None -> None + | Some v -> Some (f v) + +open Constrexpr + +let rec rebuild_bl aux bl typ = + match bl,typ with + | [], _ -> List.rev aux,typ + | (CLocalAssum(nal,bk,_))::bl',typ -> + rebuild_nal aux bk bl' nal typ + | (CLocalDef(na,_,_))::bl',{ CAst.v = CLetIn(_,nat,ty,typ') } -> + rebuild_bl (Constrexpr.CLocalDef(na,nat,ty)::aux) + bl' typ' + | _ -> assert false +and rebuild_nal aux bk bl' nal typ = + match nal,typ with + | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ + | [], _ -> rebuild_bl aux bl' typ + | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } -> + if Name.equal (na.CAst.v) (na'.CAst.v) || Name.is_anonymous (na'.CAst.v) + then + let assum = CLocalAssum([na],bk,nal't) in + let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in + rebuild_nal + (assum::aux) + bk + bl' + nal + (CAst.make @@ CProdN(new_rest,typ')) + else + let assum = CLocalAssum([na'],bk,nal't) in + let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in + rebuild_nal + (assum::aux) + bk + bl' + (na::nal) + (CAst.make @@ CProdN(new_rest,typ')) + | _ -> + assert false + +let rebuild_bl aux bl typ = rebuild_bl aux bl typ + +let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = + let fixl,ntns = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in + let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in + let constr_expr_typel = + with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in + let fixpoint_exprl_with_new_bl = + List.map2 (fun ((lna,rec_order_opt,bl,ret_typ,opt_body),notation_list) fix_typ -> + + let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in + (((lna,rec_order_opt,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 ~pstate pconstants on_error register_built interactive_proof + (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = + List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; + let pstate, _is_struct = + match fixpoint_exprl with + | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] -> + let (((({CAst.v=name},pl),_,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 ~hdr:"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 pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built + then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false + else pstate, false + |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> + let (((({CAst.v=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 ~hdr:"Function" (str "Body of Function must be given") in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built + then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true + else pstate, true + | _ -> + List.iter (function ((_na,ord,_args,_body,_type),_not) -> + match ord with + | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.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 ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl + in + (* ok all the expressions are structural *) + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let is_rec = List.exists (is_rec fix_names) recdefs in + let pstate,evd,pconstants = + if register_built + then register_struct ~pstate is_rec fixpoint_exprl + else pstate, Evd.from_env (Global.env ()), pconstants + in + let evd = ref evd in + generate_principle + (ref !evd) + pconstants + on_error + false + register_built + fixpoint_exprl + recdefs + interactive_proof + (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof); + if register_built then + begin derive_inversion fix_names; end; + pstate, true + in + pstate + +let rec add_args id new_args = CAst.map (function + | CRef (qid,_) as b -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((None,qid,None),new_args) + else b + | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") + | CProdN(nal,b1) -> + CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) + | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) + | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, + add_args id new_args b1) + | CLambdaN(nal,b1) -> + CLambdaN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) + | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) + | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, + add_args id new_args b1) + | CLetIn(na,b1,t,b2) -> + CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) + | CAppExpl((pf,qid,us),exprl) -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl)) + else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl) + | CApp((pf,b),bl) -> + CApp((pf,add_args id new_args b), + List.map (fun (e,o) -> add_args id new_args e,o) bl) + | CCases(sty,b_option,cel,cal) -> + CCases(sty,Option.map (add_args id new_args) b_option, + List.map (fun (b,na,b_option) -> + add_args id new_args b, + na, b_option) cel, + List.map CAst.(map (fun (cpl,e) -> (cpl,add_args id new_args e))) cal + ) + | CLetTuple(nal,(na,b_option),b1,b2) -> + CLetTuple(nal,(na,Option.map (add_args id new_args) b_option), + add_args id new_args b1, + add_args id new_args b2 + ) + + | CIf(b1,(na,b_option),b2,b3) -> + CIf(add_args id new_args b1, + (na,Option.map (add_args id new_args) b_option), + add_args id new_args b2, + add_args id new_args b3 + ) + | CHole _ + | CPatVar _ + | CEvar _ + | CPrim _ + | CSort _ as b -> b + | CCast(b1,b2) -> + CCast(add_args id new_args b1, + Glob_ops.map_cast_type (add_args id new_args) b2) + | CRecord pars -> + CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) + | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") + | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.") + | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.") + ) +exception Stop of Constrexpr.constr_expr + + +(* [chop_n_arrow n t] chops the [n] first arrows in [t] + 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.CAst.v with + | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, two results 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 + recall [chop_n_arrow], either this product contains more arrows + than the number we need to chop and then we return the new type + *) + begin + try + let new_n = + let rec aux (n:int) = function + [] -> n + | CLocalAssum(nal,k,t'')::nal_ta' -> + let nal_l = List.length nal in + if n >= nal_l + then + aux (n - nal_l) nal_ta' + else + let new_t' = CAst.make @@ + Constrexpr.CProdN( + CLocalAssum((snd (List.chop n nal)),k,t'')::nal_ta',t') + in + raise (Stop new_t') + | _ -> anomaly (Pp.str "Not enough products.") + in + aux n nal_ta' + in + chop_n_arrow new_n t' + with Stop t -> t + end + | _ -> anomaly (Pp.str "Not enough products.") + + +let rec get_args b t : Constrexpr.local_binder_expr list * + Constrexpr.constr_expr * Constrexpr.constr_expr = + match b.CAst.v with + | Constrexpr.CLambdaN (CLocalAssum(nal,k,ta) as d::rest, b') -> + begin + let n = List.length nal in + let nal_tas,b'',t'' = get_args (CAst.make ?loc:b.CAst.loc @@ Constrexpr.CLambdaN (rest,b')) (chop_n_arrow n t) in + d :: nal_tas, b'',t'' + end + | Constrexpr.CLambdaN ([], b) -> [],b,t + | _ -> [],b,t + + +let make_graph ~pstate (f_ref : GlobRef.t) = + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in + let c,c_body = + match f_ref with + | ConstRef c -> + begin try c,Global.lookup_constant c + with Not_found -> + raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) ) + end + | _ -> raise (UserError (None, str "Not a function reference") ) + in + (match Global.body_of_constant_body c_body with + | None -> error "Cannot build a graph over an axiom!" + | Some (body, _) -> + let env = Global.env () in + let extern_body,extern_type = + with_full_print (fun () -> + (Constrextern.extern_constr false env sigma (EConstr.of_constr body), + Constrextern.extern_type false env sigma + (EConstr.of_constr (*FIXME*) c_body.const_type) + ) + ) + () + in + let (nal_tas,b,t) = get_args extern_body extern_type in + let expr_list = + match b.CAst.v with + | Constrexpr.CFix(l_id,fixexprl) -> + let l = + List.map + (fun (id,recexp,bl,t,b) -> + let { CAst.loc; v=rec_id } = match Option.get recexp with + | { CAst.v = CStructRec id } -> id + | { CAst.v = CWfRec (id,_) } -> id + | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid + in + let new_args = + List.flatten + (List.map + (function + | Constrexpr.CLocalDef (na,_,_)-> [] + | Constrexpr.CLocalAssum (nal,_,_) -> + List.map + (fun {CAst.loc;v=n} -> CAst.make ?loc @@ + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) + nal + | Constrexpr.CLocalPattern _ -> assert false + ) + nal_tas + ) + in + let b' = add_args id.CAst.v new_args b in + ((((id,None), ( Some (CAst.make (CStructRec (CAst.make rec_id)))),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + ) + fixexprl + in + l + | _ -> + let id = Label.to_id (Constant.label c) in + [((CAst.make id,None),None,nal_tas,t,Some b),[]] + in + let mp = Constant.modpath c in + let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error false false expr_list in + (* We register the infos *) + List.iter + (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) + expr_list; + pstate) + +let do_generate_principle = do_generate_principle [] warning_error true |